1%%% use init_kb('gilppi_instances/rul_ex.pl',type) for loading 2%%% ~~~~~ 3 4matomic(X):- atomic(X). 5matom(X):- atom(X). 6mnumber(X):- number(X). 7/* 8ex(app([1,2]),'+'). 9ex(app([a]),'+'). 10ex(app([]),'+'). 11ex(app([p]),'+'). 12ex(app([r,s]),'+'). 13ex(app([g]),'+'). 14ex(app([9,8,7]),'+'). 15ex(app([4,3,5]),'+'). 16ex(app([r,w]),'+'). 17ex(app([j,k,l,m]),'+'). 18 19 20ex(split([3]),'+'). 21ex(split([4]),'+'). 22ex(split([1,2]),'+'). 23ex(split([55,66]),'+'). 24ex(split([7,8,9]),'+'). 25ex(split([11,12,13]),'+'). 26ex(split([14,15,16,17]),'+'). 27ex(split([18,19,20,21]),'+'). 28ex(split([22,23,24,25,26]),'+'). 29ex(split([27,28,29,30,31]),'+'). 30 31 32ex(obti([[],0,[]]),'+'). 33ex(obti([]),'+'). 34ex(obti([[],2,[]]),'+'). 35ex(obti([[[],1,[]],2,[[[],3,[]],4,[]]]),'+'). 36ex(obti([[[],6,[[],7,[]]],8,[[],9,[]]]),'+'). 37ex(obti([[[],89,[]],90,[[],91,[]]]),'+'). 38ex(obti([[[],91,[]],92,[[],93,[]]]),'+'). 39ex(obti([[],50,[[[],51,[]],52,[[],54,[]]]]),'+'). 40ex(obti([[[[],36,[]],37,[[],39,[]]],46,[]]),'+'). 41 42 43ex(plus(0),'+'). 44ex(plus(s(0)),'+'). 45ex(plus(s(s(0))),'+'). 46ex(plus(s(s(s(s(s(s(0))))))),'+'). 47ex(plus(s(s(s(0)))),'+'). 48ex(plus(s(s(s(s(0))))),'+'). 49 50 51 52ex(equiv(not(and([]))),'+'). 53ex(equiv(not(and([a]))),'+'). 54ex(equiv(not(and([b]))),'+'). 55ex(equiv(not(and([x,y]))),'+'). 56ex(equiv(not(and([r,s]))),'+'). 57ex(equiv(not(and([k,l,m]))),'+'). 58ex(equiv(not(and([kk,ll,mm]))),'+'). 59ex(equiv(not(and([h,i,j,k]))),'+'). 60ex(equiv(not(and([hh,ii,jj,kk]))),'+'). 61ex(equiv(not(and([c,d,e,f,g]))),'+'). 62ex(equiv(not(and([cc,dd,ee,ff,gg]))),'+'). 63ex(equiv(not(or([]))),'+'). 64ex(equiv(not(or([a1]))),'+'). 65ex(equiv(not(or([b1]))),'+'). 66ex(equiv(not(or([x1,y1]))),'+'). 67ex(equiv(not(or([r1,s1]))),'+'). 68ex(equiv(not(or([k1,l1,m1]))),'+'). 69ex(equiv(not(or([kk1,ll1,mm1]))),'+'). 70ex(equiv(not(or([h1,i1,j1,k1]))),'+'). 71ex(equiv(not(or([hh1,ii1,jj1,kk1]))),'+'). 72ex(equiv(not(or([c1,d1,e1,f1,g1]))),'+'). 73ex(equiv(not(or([cc1,dd1,ee1,ff1,gg1]))),'+'). 74ex(equiv(or([])),'+'). 75ex(equiv(or([not(a)])),'+'). 76ex(equiv(or([not(b)])),'+'). 77ex(equiv(or([not(x),not(y)])),'+'). 78ex(equiv(or([not(r),not(s)])),'+'). 79ex(equiv(or([not(k),not(l),not(m)])),'+'). 80ex(equiv(or([not(kk),not(ll),not(mm)])),'+'). 81ex(equiv(or([not(h),not(i),not(j),not(k)])),'+'). 82ex(equiv(or([not(hh),not(ii),not(jj),not(kk)])),'+'). 83ex(equiv(or([not(c),not(d),not(e),not(f),not(g)])),'+'). 84ex(equiv(or([not(cc),not(dd),not(ee),not(ff),not(gg)])),'+'). 85ex(equiv(and([])),'+'). 86ex(equiv(and([not(a1)])),'+'). 87ex(equiv(and([not(b1)])),'+'). 88ex(equiv(and([not(x1),not(y1)])),'+'). 89ex(equiv(and([not(r1),not(s1)])),'+'). 90ex(equiv(and([not(k1),not(l1),not(m1)])),'+'). 91ex(equiv(and([not(kk1),not(ll1),not(mm1)])),'+'). 92ex(equiv(and([not(h1),not(i1),not(j1),not(k1)])),'+'). 93ex(equiv(and([not(hh1),not(ii1),not(jj1),not(kk1)])),'+'). 94ex(equiv(and([not(c1),not(d1),not(e1),not(f1),not(g1)])),'+'). 95ex(equiv(and([not(cc1),not(dd1),not(ee1),not(ff1),not(gg1)])),'+'). 96 97 98ex(equiv(not(and([]))),'+'). 99ex(equiv(not(or([]))),'+'). 100ex(equiv(not(and([a]))),'+'). 101ex(equiv(not(or([b]))),'+'). 102ex(equiv(not(and([x,y]))),'+'). 103ex(equiv(not(or([r,s]))),'+'). 104ex(equiv(not(and([k,l,m]))),'+'). 105ex(equiv(not(or([kk,ll,mm]))),'+'). 106ex(equiv(and([])),'+'). 107ex(equiv(or([])),'+'). 108ex(equiv(and([not(a1)])),'+'). 109ex(equiv(or([not(b1)])),'+'). 110ex(equiv(and([not(x1),not(y1)])),'+'). 111ex(equiv(or([not(r1),not(s1)])),'+'). 112ex(equiv(and([not(k1),not(l1),not(m1)])),'+'). 113ex(equiv(or([not(kk1),not(ll1),not(mm1)])),'+'). 114 115 116newp4([A|B]):-matom(A),newp4(B). 117equiv(and(A)):-newp2(A). 118equiv(not A):-newp3(A). 119equiv(or(A)):-newp1(A). 120newp1([]). 121newp1([not A|B]):-matom(A),newp1(B). 122newp2([]). 123newp2([not A|B]):-matom(A),newp1(B). 124newp3(and(A)):-newp5(A). 125newp3(or(A)):-newp4(A). 126newp4([]). 127newp5([]). 128newp5([A|B]). 129 130 131 132ex(t(f(a,f(b,f(c,x)))),'+'). 133ex(t(f(d,f(e,f(f,f(g,x))))),'+'). 134ex(t(f(i,f(j,x))),'+'). 135ex(t(f(h,x)),'+'). 136ex(t(x),'+'). 137ex(t(f(k,g(y))),'+'). 138ex(t(f(m,g(g(y)))),'+'). 139ex(t(f(n,g(g(g(y))))),'+'). 140ex(t(f(o,g(g(g(g(y)))))),'+'). 141ex(t(f(p,y)),'+'). 142 143 144 145 146ex(r(x),'+'). 147ex(r(f(h,x)),'+'). 148ex(r(f(i,g(j,x))),'+'). 149ex(r(f(a,g(b,f(c,x)))),'+'). 150ex(r(f(d,g(e,f(f,g(g,x))))),'+'). 151ex(r(f(q,g(r,f(s,g(t,f(u,x)))))),'+'). 152ex(r(f(k,g(l,f(m,g(n,f(o,g(p,x))))))),'+'). 153ex(r(f(k1,g(l1,f(m1,g(n1,f(o1,g(p1,f(q1,x)))))))),'+'). 154 155 156 157 158ex(s(x),'+'). 159ex(s(f(h,x)),'+'). 160ex(s(f(g(j,x),g(j,x))),'+'). 161ex(s(f(g(b,h(c,x)),g(b,h(c,x)))),'+'). 162ex(s(f(g(e,h(f,f(g,x))),g(e,h(f,f(g,x))))),'+'). 163ex(s(f(g(r,h(s,f(t,g(u,x)))),g(r,h(s,f(t,g(u,x)))))),'+'). 164ex(s(f(g(l,h(m,f(n,g(o,h(p,x))))),g(l,h(m,f(n,g(o,h(p,x))))))),'+'). 165ex(s(f(g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,x)))))),g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,x)))))))),'+'). 166ex(s(f(g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(r1,x))))))), 167 g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(r1,x))))))))),'+'). 168ex(s(f(g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(t1,h(u1,x)))))))), 169 g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(t1,h(u1,x)))))))))),'+'). 170ex(s(f(g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(v1,h(w1,f(x1,x))))))))), 171 g(l1,h(m1,f(n1,g(o1,h(p1,f(q1,g(v1,h(w1,f(x1,x))))))))))),'+'). 172 173 174ex(i(not(not(and(a,a)))),'+'). 175ex(i(not(and(not(a),not(a)))),'+'). 176ex(i(not(and(not(a),and(a,a)))),'+'). 177ex(i(not(and(and(a,a),not(a)))),'+'). 178ex(i(not(and(and(a,a),and(a,a)))),'+'). 179ex(i(not(not(a))),'+'). 180ex(i(not(and(a,a))),'+'). 181ex(i(not(a)),'+'). 182ex(i(not(not(not(a)))),'+'). 183ex(i(and(not(not(a)),not(a))),'+'). 184ex(i(and(not(not(a)),and(not(a),not(a)))),'+'). 185ex(i(and(not(not(a)),and(not(a),and(a,a)))),'+'). 186ex(i(and(not(not(a)),and(not(a),a))),'+'). 187ex(i(and(not(and(a,a)),not(not(a)))),'+'). 188ex(i(and(not(and(a,a)),not(and(a,a)))),'+'). 189ex(i(and(not(and(a,a)),not(a))),'+'). 190ex(i(and(not(and(a,a)),and(not(a),not(a)))),'+'). 191ex(i(and(not(and(a,a)),and(not(a),and(a,a)))),'+'). 192ex(i(and(not(and(a,a)),and(not(a),a))),'+'). 193ex(i(and(not(not(a)),and(and(a,a),not(a)))),'+'). 194ex(i(and(not(not(a)),and(and(a,a),and(a,a)))),'+'). 195ex(i(and(and(not(a),not(a)),and(a,and(a,a)))),'+'). 196ex(i(and(and(not(a),not(a)),and(a,a))),'+'). 197ex(i(and(and(not(a),not(a)),a)),'+'). 198ex(i(and(and(not(a),and(a,a)),not(not(a)))),'+'). 199ex(i(and(not(a),not(a))),'+'). 200ex(i(and(not(a),and(a,a))),'+'). 201ex(i(and(not(a),a)),'+'). 202ex(i(and(and(a,a),not(a))),'+'). 203ex(i(and(and(a,a),and(a,a))),'+'). 204ex(i(and(and(a,a),a)),'+'). 205ex(i(and(a,not(a))),'+'). 206ex(i(and(a,and(a,a))),'+'). 207ex(i(and(a,a)),'+'). 208ex(i(a),'+'). 209*/ 210 211ex(t(nil),+). 212ex(t(tree(nil,0,nil)),+). 213ex(t(tree(nil,0,tree(nil,0,nil))),+). 214ex(t(tree(nil,0,tree(nil,s(0),nil))),+). 215ex(t(tree(nil,0,tree(nil,s(s(0)),nil))),+). 216ex(t(tree(nil,0,tree(nil,s(s(s(0))),nil))),+). 217ex(t(tree(nil,s(0),nil)),+). 218ex(t(tree(nil,s(0),tree(nil,0,nil))),+). 219ex(t(tree(nil,s(0),tree(nil,s(0),nil))),+). 220ex(t(tree(nil,s(0),tree(nil,s(s(0)),nil))),+). 221ex(t(tree(nil,s(0),tree(nil,s(s(s(0))),nil))),+). 222ex(t(tree(nil,s(s(0)),nil)),+). 223ex(t(tree(nil,s(s(0)),tree(nil,0,nil))),+). 224ex(t(tree(nil,s(s(0)),tree(nil,s(0),nil))),+). 225ex(t(tree(nil,s(s(0)),tree(nil,s(s(0)),nil))),+). 226ex(t(tree(nil,s(s(0)),tree(nil,s(s(s(0))),nil))),+). 227ex(t(tree(nil,s(s(s(0))),nil)),+). 228ex(t(tree(nil,s(s(s(0))),tree(nil,0,nil))),+). 229ex(t(tree(nil,s(s(s(0))),tree(nil,s(0),nil))),+). 230ex(t(tree(nil,s(s(s(0))),tree(nil,s(s(0)),nil))),+). 231ex(t(tree(nil,s(s(s(0))),tree(nil,s(s(s(0))),nil))),+). 232ex(t(tree(tree(nil,0,nil),0,nil)),+). 233ex(t(tree(tree(nil,0,nil),0,tree(nil,0,nil))),+). 234ex(t(tree(tree(nil,0,nil),0,tree(nil,s(0),nil))),+). 235ex(t(tree(tree(nil,0,nil),0,tree(nil,s(s(0)),nil))),+). 236ex(t(tree(tree(nil,0,nil),0,tree(nil,s(s(s(0))),nil))),+). 237ex(t(tree(tree(nil,0,nil),s(0),nil)),+). 238ex(t(tree(tree(nil,0,nil),s(0),tree(nil,0,nil))),+). 239ex(t(tree(tree(nil,0,nil),s(0),tree(nil,s(0),nil))),+). 240ex(t(tree(tree(nil,0,nil),s(0),tree(nil,s(s(0)),nil))),+). 241ex(t(tree(tree(nil,0,nil),s(0),tree(nil,s(s(s(0))),nil))),+). 242ex(t(tree(tree(nil,0,nil),s(s(0)),nil)),+). 243ex(t(tree(tree(nil,0,nil),s(s(0)),tree(nil,0,nil))),+). 244ex(t(tree(tree(nil,0,nil),s(s(0)),tree(nil,s(0),nil))),+). 245ex(t(tree(tree(nil,0,nil),s(s(0)),tree(nil,s(s(0)),nil))),+). 246ex(t(tree(tree(nil,0,nil),s(s(0)),tree(nil,s(s(s(0))),nil))),+). 247ex(t(tree(tree(nil,0,nil),s(s(s(0))),nil)),+). 248ex(t(tree(tree(nil,0,nil),s(s(s(0))),tree(nil,0,nil))),+). 249ex(t(tree(tree(nil,0,nil),s(s(s(0))),tree(nil,s(0),nil))),+). 250ex(t(tree(tree(nil,0,nil),s(s(s(0))),tree(nil,s(s(0)),nil))),+). 251ex(t(tree(tree(nil,0,nil),s(s(s(0))),tree(nil,s(s(s(0))),nil))),+). 252ex(t(tree(tree(nil,s(0),nil),0,nil)),+). 253ex(t(tree(tree(nil,s(0),nil),0,tree(nil,0,nil))),+). 254ex(t(tree(tree(nil,s(0),nil),0,tree(nil,s(0),nil))),+). 255ex(t(tree(tree(nil,s(0),nil),0,tree(nil,s(s(0)),nil))),+). 256ex(t(tree(tree(nil,s(0),nil),0,tree(nil,s(s(s(0))),nil))),+). 257ex(t(tree(tree(nil,s(0),nil),s(0),nil)),+). 258ex(t(tree(tree(nil,s(0),nil),s(0),tree(nil,0,nil))),+). 259ex(t(tree(tree(nil,s(0),nil),s(0),tree(nil,s(0),nil))),+). 260ex(t(tree(tree(nil,s(0),nil),s(0),tree(nil,s(s(0)),nil))),+). 261ex(t(tree(tree(nil,s(0),nil),s(0),tree(nil,s(s(s(0))),nil))),+). 262ex(t(tree(tree(nil,s(0),nil),s(s(0)),nil)),+). 263ex(t(tree(tree(nil,s(0),nil),s(s(0)),tree(nil,0,nil))),+). 264ex(t(tree(tree(nil,s(0),nil),s(s(0)),tree(nil,s(0),nil))),+). 265ex(t(tree(tree(nil,s(0),nil),s(s(0)),tree(nil,s(s(0)),nil))),+). 266ex(t(tree(tree(nil,s(0),nil),s(s(0)),tree(nil,s(s(s(0))),nil))),+). 267ex(t(tree(tree(nil,s(0),nil),s(s(s(0))),nil)),+). 268ex(t(tree(tree(nil,s(0),nil),s(s(s(0))),tree(nil,0,nil))),+). 269ex(t(tree(tree(nil,s(0),nil),s(s(s(0))),tree(nil,s(0),nil))),+). 270ex(t(tree(tree(nil,s(0),nil),s(s(s(0))),tree(nil,s(s(0)),nil))),+). 271ex(t(tree(tree(nil,s(0),nil),s(s(s(0))),tree(nil,s(s(s(0))),nil))),+). 272ex(t(tree(tree(nil,s(s(0)),nil),0,nil)),+). 273ex(t(tree(tree(nil,s(s(0)),nil),0,tree(nil,0,nil))),+). 274ex(t(tree(tree(nil,s(s(0)),nil),0,tree(nil,s(0),nil))),+). 275ex(t(tree(tree(nil,s(s(0)),nil),0,tree(nil,s(s(0)),nil))),+). 276ex(t(tree(tree(nil,s(s(0)),nil),0,tree(nil,s(s(s(0))),nil))),+). 277ex(t(tree(tree(nil,s(s(0)),nil),s(0),nil)),+). 278ex(t(tree(tree(nil,s(s(0)),nil),s(0),tree(nil,0,nil))),+). 279ex(t(tree(tree(nil,s(s(0)),nil),s(0),tree(nil,s(0),nil))),+). 280ex(t(tree(tree(nil,s(s(0)),nil),s(0),tree(nil,s(s(0)),nil))),+). 281ex(t(tree(tree(nil,s(s(0)),nil),s(0),tree(nil,s(s(s(0))),nil))),+). 282ex(t(tree(tree(nil,s(s(0)),nil),s(s(0)),nil)),+). 283ex(t(tree(tree(nil,s(s(0)),nil),s(s(0)),tree(nil,0,nil))),+). 284ex(t(tree(tree(nil,s(s(0)),nil),s(s(0)),tree(nil,s(0),nil))),+). 285ex(t(tree(tree(nil,s(s(0)),nil),s(s(0)),tree(nil,s(s(0)),nil))),+). 286ex(t(tree(tree(nil,s(s(0)),nil),s(s(0)),tree(nil,s(s(s(0))),nil))),+). 287ex(t(tree(tree(nil,s(s(0)),nil),s(s(s(0))),nil)),+). 288ex(t(tree(tree(nil,s(s(0)),nil),s(s(s(0))),tree(nil,0,nil))),+). 289ex(t(tree(tree(nil,s(s(0)),nil),s(s(s(0))),tree(nil,s(0),nil))),+). 290ex(t(tree(tree(nil,s(s(0)),nil),s(s(s(0))),tree(nil,s(s(0)),nil))),+). 291ex(t(tree(tree(nil,s(s(0)),nil),s(s(s(0))),tree(nil,s(s(s(0))),nil))),+). 292ex(t(tree(tree(nil,s(s(s(0))),nil),0,nil)),+). 293ex(t(tree(tree(nil,s(s(s(0))),nil),0,tree(nil,0,nil))),+). 294ex(t(tree(tree(nil,s(s(s(0))),nil),0,tree(nil,s(0),nil))),+). 295ex(t(tree(tree(nil,s(s(s(0))),nil),0,tree(nil,s(s(0)),nil))),+). 296ex(t(tree(tree(nil,s(s(s(0))),nil),0,tree(nil,s(s(s(0))),nil))),+). 297ex(t(tree(tree(nil,s(s(s(0))),nil),s(0),nil)),+). 298ex(t(tree(tree(nil,s(s(s(0))),nil),s(0),tree(nil,0,nil))),+). 299ex(t(tree(tree(nil,s(s(s(0))),nil),s(0),tree(nil,s(0),nil))),+). 300ex(t(tree(tree(nil,s(s(s(0))),nil),s(0),tree(nil,s(s(0)),nil))),+). 301ex(t(tree(tree(nil,s(s(s(0))),nil),s(0),tree(nil,s(s(s(0))),nil))),+). 302ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(0)),nil)),+). 303ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(0)),tree(nil,0,nil))),+). 304ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(0)),tree(nil,s(0),nil))),+). 305ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(0)),tree(nil,s(s(0)),nil))),+). 306ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(0)),tree(nil,s(s(s(0))),nil))),+). 307ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(s(0))),nil)),+). 308ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(s(0))),tree(nil,0,nil))),+). 309ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(s(0))),tree(nil,s(0),nil))),+). 310ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(s(0))),tree(nil,s(s(0)),nil))),+). 311ex(t(tree(tree(nil,s(s(s(0))),nil),s(s(s(0))),tree(nil,s(s(s(0))),nil))),+)