----- Otter 3.3, August 2003 ----- The process was started by mccune on gyro.thornwood, Wed Aug 6 14:26:26 2003 The command was "../../bin/otter". The process ID is 5982. set(hyper_res). assign(max_weight,20). assign(max_proofs,-1). clear(print_kept). clear(back_sub). assign(max_mem,24000). assign(max_given,618). set(order_history). set(input_sos_first). weight_list(pick_and_purge). weight(P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))),2). weight(P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))),2). weight(P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))),2). weight(P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))),2). weight(P(i(i(x,y),i(i(z,x),i(i(y,u),i(z,u))))),2). weight(P(i(i(i(n(x),y),z),i(x,z))),2). weight(P(i(x,i(i(i(n(x),x),x),i(i(y,x),x)))),2). weight(P(i(i(x,i(i(n(y),y),y)),i(i(n(y),y),y))),2). weight(P(i(x,i(i(n(y),y),y))),2). weight(P(i(i(n(x),y),i(z,i(i(y,x),x)))),2). weight(P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))),2). weight(P(i(i(n(x),y),i(i(y,x),x))),2). weight(P(i(x,x)),2). weight(P(i(x,i(i(y,x),x))),2). weight(P(i(x,i(y,x))),2). weight(P(i(i(i(x,y),z),i(y,z))),2). weight(P(i(x,i(i(x,y),y))),2). weight(P(i(i(x,i(y,z)),i(y,i(x,z)))),2). weight(P(i(i(x,y),i(i(z,x),i(z,y)))),2). weight(P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))),2). weight(P(i(i(i(x,y),x),x)),2). weight(P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))),2). weight(P(i(i(i(x,y),z),i(i(z,x),x))),2). weight(P(i(i(i(x,y),y),i(i(y,x),x))),2). weight(P(i(i(i(i(x,y),y),z),i(i(i(y,u),x),z))),2). weight(P(i(i(i(x,y),z),i(i(x,z),z))),2). weight(P(i(i(x,i(x,y)),i(x,y))),2). weight(P(i(i(x,y),i(i(i(x,z),u),i(i(y,u),u)))),2). weight(P(i(i(i(x,y),z),i(i(x,u),i(i(u,z),z)))),2). weight(P(i(i(x,y),i(i(y,i(z,i(x,u))),i(z,i(x,u))))),2). weight(P(i(i(x,i(y,i(z,u))),i(i(z,x),i(y,i(z,u))))),2). weight(P(i(i(x,i(y,z)),i(i(x,y),i(x,z)))),2). weight(P(i(n(x),i(x,y))),2). weight(P(i(i(i(x,y),z),i(n(x),z))),2). weight(P(i(i(x,n(x)),n(x))),2). weight(P(i(n(n(x)),x)),2). weight(P(i(x,n(n(x)))),2). weight(P(i(i(x,y),i(n(n(x)),y))),2). weight(P(i(i(i(n(n(x)),y),z),i(i(x,y),z))),2). weight(P(i(i(x,y),i(i(y,n(x)),n(x)))),2). weight(P(i(i(x,i(y,n(z))),i(i(z,y),i(x,n(z))))),2). weight(P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))),2). weight(P(i(i(x,y),i(n(y),n(x)))),2). weight(P(i(i(x,n(y)),i(y,n(x)))),2). weight(P(i(i(n(x),y),i(n(y),x))),2). weight(P(i(i(n(x),n(y)),i(y,x))),2). weight(P(i(i(i(n(x),y),z),i(i(n(y),x),z))),2). weight(P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))),2). weight(P(i(i(x,i(y,n(z))),i(x,i(z,n(y))))),2). weight(P(i(i(n(x),y),i(i(x,y),y))),2). weight(P(i(i(x,y),i(i(n(x),y),y))),2). weight(P(i(i(x,y),i(i(x,n(y)),n(x)))),2). weight(P(i(i(i(i(x,y),y),z),i(i(n(x),y),z))),2). weight(P(i(i(n(x),y),i(i(x,z),i(i(z,y),y)))),2). weight(P(i(i(i(i(x,y),i(i(y,z),z)),u),i(i(n(x),z),u))),2). weight(P(i(i(n(x),y),i(i(z,y),i(i(x,z),y)))),2). weight(P(i(i(x,i(n(y),z)),i(x,i(i(u,z),i(i(y,u),z))))),2). weight(P(i(i(x,y),i(i(z,y),i(i(n(x),z),y)))),2). weight(P(i(i(n(n(x)),y),i(x,y))),2). weight(P(i(x,i(y,y))),2). weight(P(i(n(i(x,x)),y)),2). weight(P(i(i(n(x),n(i(y,y))),x)),2). weight(P(i(n(i(x,y)),x)),2). weight(P(i(n(i(x,y)),n(y))),2). weight(P(i(n(i(x,n(y))),y)),2). weight(P(i(x,i(n(y),n(i(x,y))))),2). weight(P(i(x,i(y,n(i(x,n(y)))))),2). weight(P(n(i(i(x,x),n(i(y,y))))),2). end_of_list. list(usable). 1 [] -P(i(x,y))| -P(x)|P(y). 2 [] -P(i(p,i(q,p)))| -P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))| -P(i(n(n(p)),p))| -P(i(p,n(n(p))))| -P(i(i(p,q),i(n(q),n(p))))| -P(i(i(p,i(q,r)),i(q,i(p,r))))|$ANSWER(step_allFrege_18_35_39_40_46_21). 3 [] -P(i(p,i(q,p)))| -P(i(i(p,i(q,r)),i(q,i(p,r))))| -P(i(i(q,r),i(i(p,q),i(p,r))))| -P(i(p,i(n(p),q)))| -P(i(i(p,q),i(i(n(p),q),q)))| -P(i(i(p,i(p,q)),i(p,q)))|$ANSWER(step_allHilbert_18_21_22_3_54_30). 4 [] -P(i(p,i(q,p)))| -P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))| -P(i(i(n(p),n(q)),i(q,p)))|$ANSWER(step_allBEH_Church_FL_18_35_49). 5 [] -P(i(i(i(p,q),r),i(q,r)))| -P(i(i(i(p,q),r),i(n(p),r)))| -P(i(i(n(p),r),i(i(q,r),i(i(p,q),r))))|$ANSWER(step_allLuka_x_19_37_59). 6 [] -P(i(i(i(p,q),r),i(q,r)))| -P(i(i(i(p,q),r),i(n(p),r)))| -P(i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r)))))|$ANSWER(step_allWos_x_19_37_60). 7 [] -P(i(i(p,q),i(i(q,r),i(p,r))))| -P(i(i(n(p),p),p))| -P(i(p,i(n(p),q)))|$ANSWER(step_allLuka_1_2_3). 8 [] -P(i(p,p))| -P(i(p,i(q,p)))| -P(i(i(p,i(q,r)),i(q,i(p,r))))| -P(i(i(i(p,q),p),p))| -P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))| -P(i(n(n(p)),p))| -P(i(p,n(n(p))))| -P(i(i(p,q),i(n(q),n(p))))|$ANSWER(step_allScott_orig_16_18_21_24_35_39_40_46). 9 [] -P(i(p,p))| -P(i(p,i(q,p)))| -P(i(i(p,i(q,r)),i(q,i(p,r))))| -P(i(i(i(p,q),p),p))| -P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))| -P(i(n(n(p)),p))| -P(i(p,n(n(p))))| -P(i(i(n(p),n(q)),i(q,p)))|$ANSWER(step_allScott_orig0_16_18_21_24_35_39_40_49). end_of_list. list(sos). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). end_of_list. list(passive). 13 [] -P(i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s)))|$ANS(neg_th_04). 14 [] -P(i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r)))))|$ANS(neg_th_05). 15 [] -P(i(i(p,q),i(i(i(p,r),s),i(i(q,r),s))))|$ANS(neg_th_06). 16 [] -P(i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s)))))|$ANS(neg_th_07). 17 [] -P(i(i(q,r),i(i(p,q),i(i(r,s),i(p,s)))))|$ANS(neg_th_08). 18 [] -P(i(i(i(n(p),q),r),i(p,r)))|$ANS(neg_th_09). 19 [] -P(i(p,i(i(i(n(p),p),p),i(i(q,p),p))))|$ANS(neg_th_10). 20 [] -P(i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p)))|$ANS(neg_th_11). 21 [] -P(i(t,i(i(n(p),p),p)))|$ANS(neg_th_12). 22 [] -P(i(i(n(p),q),i(t,i(i(q,p),p))))|$ANS(neg_th_13). 23 [] -P(i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r)))|$ANS(neg_th_14). 24 [] -P(i(i(n(p),q),i(i(q,p),p)))|$ANS(neg_th_15). 25 [] -P(i(p,p))|$ANS(neg_th_16). 26 [] -P(i(p,i(i(q,p),p)))|$ANS(neg_th_17). 27 [] -P(i(q,i(p,q)))|$ANS(neg_th_18). 28 [] -P(i(i(i(p,q),r),i(q,r)))|$ANS(neg_th_19). 29 [] -P(i(p,i(i(p,q),q)))|$ANS(neg_th_20). 30 [] -P(i(i(p,i(q,r)),i(q,i(p,r))))|$ANS(neg_th_21). 31 [] -P(i(i(q,r),i(i(p,q),i(p,r))))|$ANS(neg_th_22). 32 [] -P(i(i(i(q,i(p,r)),s),i(i(p,i(q,r)),s)))|$ANS(neg_th_23). 33 [] -P(i(i(i(p,q),p),p))|$ANS(neg_th_24). 34 [] -P(i(i(i(p,r),s),i(i(p,q),i(i(q,r),s))))|$ANS(neg_th_25). 35 [] -P(i(i(i(p,q),r),i(i(r,p),p)))|$ANS(neg_th_26). 36 [] -P(i(i(i(p,q),q),i(i(q,p),p)))|$ANS(neg_th_27). 37 [] -P(i(i(i(i(r,p),p),s),i(i(i(p,q),r),s)))|$ANS(neg_th_28). 38 [] -P(i(i(i(p,q),r),i(i(p,r),r)))|$ANS(neg_th_29). 39 [] -P(i(i(p,i(p,q)),i(p,q)))|$ANS(neg_th_30). 40 [] -P(i(i(p,s),i(i(i(p,q),r),i(i(s,r),r))))|$ANS(neg_th_31). 41 [] -P(i(i(i(p,q),r),i(i(p,s),i(i(s,r),r))))|$ANS(neg_th_32). 42 [] -P(i(i(p,s),i(i(s,i(q,i(p,r))),i(q,i(p,r)))))|$ANS(neg_th_33). 43 [] -P(i(i(s,i(q,i(p,r))),i(i(p,s),i(q,i(p,r)))))|$ANS(neg_th_34). 44 [] -P(i(i(p,i(q,r)),i(i(p,q),i(p,r))))|$ANS(neg_th_35). 45 [] -P(i(n(p),i(p,q)))|$ANS(neg_th_36). 46 [] -P(i(i(i(p,q),r),i(n(p),r)))|$ANS(neg_th_37). 47 [] -P(i(i(p,n(p)),n(p)))|$ANS(neg_th_38). 48 [] -P(i(n(n(p)),p))|$ANS(neg_th_39). 49 [] -P(i(p,n(n(p))))|$ANS(neg_th_40). 50 [] -P(i(i(p,q),i(n(n(p)),q)))|$ANS(neg_th_41). 51 [] -P(i(i(i(n(n(p)),q),r),i(i(p,q),r)))|$ANS(neg_th_42). 52 [] -P(i(i(p,q),i(i(q,n(p)),n(p))))|$ANS(neg_th_43). 53 [] -P(i(i(s,i(q,n(p))),i(i(p,q),i(s,n(p)))))|$ANS(neg_th_44). 54 [] -P(i(i(s,i(q,p)),i(i(n(p),q),i(s,p))))|$ANS(neg_th_45). 55 [] -P(i(i(p,q),i(n(q),n(p))))|$ANS(neg_th_46). 56 [] -P(i(i(p,n(q)),i(q,n(p))))|$ANS(neg_th_47). 57 [] -P(i(i(n(p),q),i(n(q),p)))|$ANS(neg_th_48). 58 [] -P(i(i(n(p),n(q)),i(q,p)))|$ANS(neg_th_49). 59 [] -P(i(i(i(n(q),p),r),i(i(n(p),q),r)))|$ANS(neg_th_50). 60 [] -P(i(i(p,i(q,r)),i(p,i(n(r),n(q)))))|$ANS(neg_th_51). 61 [] -P(i(i(p,i(q,n(r))),i(p,i(r,n(q)))))|$ANS(neg_th_52). 62 [] -P(i(i(n(p),q),i(i(p,q),q)))|$ANS(neg_th_53). 63 [] -P(i(i(p,q),i(i(n(p),q),q)))|$ANS(neg_th_54). 64 [] -P(i(i(p,q),i(i(p,n(q)),n(p))))|$ANS(neg_th_55). 65 [] -P(i(i(i(i(p,q),q),r),i(i(n(p),q),r)))|$ANS(neg_th_56). 66 [] -P(i(i(n(p),r),i(i(p,q),i(i(q,r),r))))|$ANS(neg_th_57). 67 [] -P(i(i(i(i(p,q),i(i(q,r),r)),s),i(i(n(p),r),s)))|$ANS(neg_th_58). 68 [] -P(i(i(n(p),r),i(i(q,r),i(i(p,q),r))))|$ANS(neg_th_59). 69 [] -P(i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r)))))|$ANS(neg_th_60). 70 [] -P(i(i(p,r),i(i(q,r),i(i(n(p),q),r))))|$ANS(neg_th_61). 71 [] -P(i(i(n(n(p)),q),i(p,q)))|$ANS(neg_th_62). 72 [] -P(i(q,i(p,p)))|$ANS(neg_th_63). 73 [] -P(i(n(i(p,p)),q))|$ANS(neg_th_64). 74 [] -P(i(i(n(q),n(i(p,p))),q))|$ANS(neg_th_65). 75 [] -P(i(n(i(p,q)),p))|$ANS(neg_th_66). 76 [] -P(i(n(i(p,q)),n(q)))|$ANS(neg_th_67). 77 [] -P(i(n(i(p,n(q))),q))|$ANS(neg_th_68). 78 [] -P(i(p,i(n(q),n(i(p,q)))))|$ANS(neg_th_69). 79 [] -P(i(p,i(q,n(i(p,n(q))))))|$ANS(neg_th_70). 80 [] -P(n(i(i(p,p),n(i(q,q)))))|$ANS(neg_th_71). end_of_list. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=-2147483647) 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). -------- PROOF -------- 82 [binary,81.1,13.1] $ANS(neg_th_04). ----> UNIT CONFLICT at 0.00 sec ----> 82 [binary,81.1,13.1] $ANS(neg_th_04). Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 13 [] -P(i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s)))|$ANS(neg_th_04). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 82 [binary,81.1,13.1] $ANS(neg_th_04). ------------ end of proof ------------- given clause #2: (wt=-2147483647) 11 [] P(i(i(n(x),x),x)). given clause #3: (wt=-2147483647) 12 [] P(i(x,i(n(x),y))). -------- PROOF -------- 84 [hyper,7,10,11,12] $ANSWER(step_allLuka_1_2_3). -----> EMPTY CLAUSE at 0.00 sec ----> 84 [hyper,7,10,11,12] $ANSWER(step_allLuka_1_2_3). Length of proof is 0. Level of proof is 0. ---------------- PROOF ---------------- 7 [] -P(i(i(p,q),i(i(q,r),i(p,r))))| -P(i(i(n(p),p),p))| -P(i(p,i(n(p),q)))|$ANSWER(step_allLuka_1_2_3). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 84 [hyper,7,10,11,12] $ANSWER(step_allLuka_1_2_3). ------------ end of proof ------------- -------- PROOF -------- 87 [binary,86.1,18.1] $ANS(neg_th_09). ----> UNIT CONFLICT at 0.00 sec ----> 87 [binary,86.1,18.1] $ANS(neg_th_09). Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 12 [] P(i(x,i(n(x),y))). 18 [] -P(i(i(i(n(p),q),r),i(p,r)))|$ANS(neg_th_09). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 87 [binary,86.1,18.1] $ANS(neg_th_09). ------------ end of proof ------------- given clause #4: (wt=2) 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). -------- PROOF -------- 91 [binary,90.1,14.1] $ANS(neg_th_05). ----> UNIT CONFLICT at 0.00 sec ----> 91 [binary,90.1,14.1] $ANS(neg_th_05). Length of proof is 2. Level of proof is 2. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 14 [] -P(i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r)))))|$ANS(neg_th_05). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 91 [binary,90.1,14.1] $ANS(neg_th_05). ------------ end of proof ------------- -------- PROOF -------- 96 [binary,95.1,15.1] $ANS(neg_th_06). ----> UNIT CONFLICT at 0.00 sec ----> 96 [binary,95.1,15.1] $ANS(neg_th_06). Length of proof is 2. Level of proof is 2. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 15 [] -P(i(i(p,q),i(i(i(p,r),s),i(i(q,r),s))))|$ANS(neg_th_06). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 96 [binary,95.1,15.1] $ANS(neg_th_06). ------------ end of proof ------------- given clause #5: (wt=2) 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). given clause #6: (wt=2) 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). -------- PROOF -------- 111 [binary,110.1,25.1] $ANS(neg_th_16). ----> UNIT CONFLICT at 0.00 sec ----> 111 [binary,110.1,25.1] $ANS(neg_th_16). Length of proof is 2. Level of proof is 2. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 25 [] -P(i(p,p))|$ANS(neg_th_16). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 110 [hyper,1,86,11] P(i(x,x)). 111 [binary,110.1,25.1] $ANS(neg_th_16). ------------ end of proof ------------- given clause #7: (wt=2) 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). -------- PROOF -------- 116 [binary,115.1,17.1] $ANS(neg_th_08). ----> UNIT CONFLICT at 0.00 sec ----> 116 [binary,115.1,17.1] $ANS(neg_th_08). Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 17 [] -P(i(i(q,r),i(i(p,q),i(i(r,s),i(p,s)))))|$ANS(neg_th_08). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 115 [hyper,1,81,90] P(i(i(x,y),i(i(z,x),i(i(y,u),i(z,u))))). 116 [binary,115.1,17.1] $ANS(neg_th_08). ------------ end of proof ------------- given clause #8: (wt=2) 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). -------- PROOF -------- 123 [binary,122.1,16.1] $ANS(neg_th_07). ----> UNIT CONFLICT at 0.00 sec ----> 123 [binary,122.1,16.1] $ANS(neg_th_07). Length of proof is 4. Level of proof is 3. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 16 [] -P(i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s)))))|$ANS(neg_th_07). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 123 [binary,122.1,16.1] $ANS(neg_th_07). ------------ end of proof ------------- -------- PROOF -------- 125 [binary,124.1,19.1] $ANS(neg_th_10). ----> UNIT CONFLICT at 0.00 sec ----> 125 [binary,124.1,19.1] $ANS(neg_th_10). Length of proof is 4. Level of proof is 3. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 12 [] P(i(x,i(n(x),y))). 19 [] -P(i(p,i(i(i(n(p),p),p),i(i(q,p),p))))|$ANS(neg_th_10). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 124 [hyper,1,86,95] P(i(x,i(i(i(n(x),y),z),i(i(u,y),z)))). 125 [binary,124.1,19.1] $ANS(neg_th_10). ------------ end of proof ------------- given clause #9: (wt=2) 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). given clause #10: (wt=2) 110 [hyper,1,86,11] P(i(x,x)). -------- PROOF -------- 137 [binary,136.1,73.1] $ANS(neg_th_64). ----> UNIT CONFLICT at 0.00 sec ----> 137 [binary,136.1,73.1] $ANS(neg_th_64). Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 73 [] -P(i(n(i(p,p)),q))|$ANS(neg_th_64). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 110 [hyper,1,86,11] P(i(x,x)). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 137 [binary,136.1,73.1] $ANS(neg_th_64). ------------ end of proof ------------- given clause #11: (wt=2) 115 [hyper,1,81,90] P(i(i(x,y),i(i(z,x),i(i(y,u),i(z,u))))). given clause #12: (wt=2) 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). given clause #13: (wt=2) 124 [hyper,1,86,95] P(i(x,i(i(i(n(x),y),z),i(i(u,y),z)))). given clause #14: (wt=2) 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). given clause #15: (wt=2) 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). given clause #16: (wt=2) 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). given clause #17: (wt=2) 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). given clause #18: (wt=2) 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). given clause #19: (wt=2) 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). given clause #20: (wt=10) 85 [hyper,1,12,12] P(i(n(i(x,i(n(x),y))),z)). given clause #21: (wt=10) 88 [hyper,1,12,11] P(i(n(i(i(n(x),x),x)),y)). given clause #22: (wt=10) 109 [hyper,1,86,12] P(i(x,i(n(i(n(x),y)),z))). given clause #23: (wt=10) 175 [hyper,1,12,136] P(i(n(i(n(i(x,x)),y)),z)). given clause #24: (wt=11) 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). given clause #25: (wt=9) 248 [hyper,1,86,105] P(i(x,i(y,i(n(x),z)))). given clause #26: (wt=9) 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). given clause #27: (wt=11) 108 [hyper,1,86,83] P(i(x,i(i(n(n(x)),n(x)),y))). given clause #28: (wt=11) 112 [hyper,1,86,10] P(i(x,i(i(y,z),i(n(x),z)))). given clause #29: (wt=11) 176 [hyper,1,10,136] P(i(i(x,y),i(n(i(z,z)),y))). given clause #30: (wt=12) 180 [hyper,1,86,151] P(i(x,i(i(x,y),i(i(z,x),y)))). given clause #31: (wt=12) 242 [hyper,1,135,105] P(i(i(n(x),x),i(y,i(n(x),z)))). given clause #32: (wt=12) 252 [hyper,1,105,175] P(i(x,i(n(i(n(i(y,y)),z)),u))). given clause #33: (wt=12) 254 [hyper,1,105,88] P(i(x,i(n(i(i(n(y),y),y)),z))). given clause #34: (wt=12) 255 [hyper,1,105,85] P(i(x,i(n(i(y,i(n(y),z))),u))). given clause #35: (wt=12) 267 [hyper,1,86,248] P(i(x,i(y,i(n(i(n(x),z)),u)))). given clause #36: (wt=12) 269 [hyper,1,12,248] P(i(n(i(x,i(y,i(n(x),z)))),u)). given clause #37: (wt=12) 291 [hyper,1,12,253] P(i(n(i(x,i(n(i(y,y)),z))),u)). given clause #38: (wt=13) 102 [hyper,1,83,11] P(i(i(n(i(n(x),x)),i(n(x),x)),x)). given clause #39: (wt=13) 114 [hyper,1,86,90] P(i(x,i(i(y,z),i(n(x),i(y,u))))). given clause #40: (wt=13) 134 [hyper,1,12,101] P(i(n(i(i(n(x),x),i(n(x),y))),z)). given clause #41: (wt=13) 168 [hyper,1,135,12] P(i(i(n(x),x),i(n(i(n(x),y)),z))). given clause #42: (wt=13) 173 [hyper,1,90,136] P(i(i(x,y),i(n(i(z,z)),i(x,u)))). given clause #43: (wt=13) 174 [hyper,1,83,136] P(i(i(n(n(i(x,x))),n(i(x,x))),y)). given clause #44: (wt=13) 208 [hyper,1,12,85] P(i(n(i(n(i(x,i(n(x),y))),z)),u)). given clause #45: (wt=13) 215 [hyper,1,12,88] P(i(n(i(n(i(i(n(x),x),x)),y)),z)). given clause #46: (wt=13) 223 [hyper,1,86,109] P(i(x,i(n(i(n(i(n(x),y)),z)),u))). given clause #47: (wt=13) 225 [hyper,1,12,109] P(i(n(i(x,i(n(i(n(x),y)),z))),u)). given clause #48: (wt=13) 227 [hyper,1,109,136] P(i(n(i(n(i(n(i(x,x)),y)),z)),u)). given clause #49: (wt=13) 266 [hyper,1,90,248] P(i(i(x,y),i(z,i(x,i(n(z),u))))). given clause #50: (wt=13) 270 [hyper,1,10,248] P(i(i(i(x,i(n(y),z)),u),i(y,u))). -------- PROOF -------- 437 [binary,436.1,19.1] $ANS(neg_th_10). ----> UNIT CONFLICT at 0.05 sec ----> 437 [binary,436.1,19.1] $ANS(neg_th_10). Length of proof is 6. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 12 [] P(i(x,i(n(x),y))). 19 [] -P(i(p,i(i(i(n(p),p),p),i(i(q,p),p))))|$ANS(neg_th_10). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 248 [hyper,1,86,105] P(i(x,i(y,i(n(x),z)))). 270 [hyper,1,10,248] P(i(i(i(x,i(n(y),z)),u),i(y,u))). 436 [hyper,1,270,10] P(i(x,i(i(i(n(x),y),z),i(u,z)))). 437 [binary,436.1,19.1] $ANS(neg_th_10). ------------ end of proof ------------- given clause #51: (wt=11) 426 [hyper,1,270,266] P(i(x,i(y,i(z,i(n(y),u))))). given clause #52: (wt=12) 435 [hyper,1,270,12] P(i(x,i(n(i(y,i(n(x),z))),u))). given clause #53: (wt=13) 290 [hyper,1,90,253] P(i(i(x,n(i(y,y))),i(z,i(x,u)))). given clause #54: (wt=13) 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). -------- PROOF -------- 504 [binary,503.1,72.1] $ANS(neg_th_63). ----> UNIT CONFLICT at 0.06 sec ----> 504 [binary,503.1,72.1] $ANS(neg_th_63). Length of proof is 8. Level of proof is 6. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 72 [] -P(i(q,i(p,p)))|$ANS(neg_th_63). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 504 [binary,503.1,72.1] $ANS(neg_th_63). ------------ end of proof ------------- given clause #55: (wt=2) 503 [hyper,1,292,11] P(i(x,i(y,y))). given clause #56: (wt=2) 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). -------- PROOF -------- 527 [binary,526.1,22.1] $ANS(neg_th_13). ----> UNIT CONFLICT at 0.07 sec ----> 527 [binary,526.1,22.1] $ANS(neg_th_13). Length of proof is 16. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 22 [] -P(i(i(n(p),q),i(t,i(i(q,p),p))))|$ANS(neg_th_13). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 527 [binary,526.1,22.1] $ANS(neg_th_13). ------------ end of proof ------------- -------- PROOF -------- 542 [binary,541.1,21.1] $ANS(neg_th_12). ----> UNIT CONFLICT at 0.07 sec ----> 542 [binary,541.1,21.1] $ANS(neg_th_12). Length of proof is 11. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 21 [] -P(i(t,i(i(n(p),p),p)))|$ANS(neg_th_12). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 542 [binary,541.1,21.1] $ANS(neg_th_12). ------------ end of proof ------------- -------- PROOF -------- 543 [binary,541.1,20.1] $ANS(neg_th_11). ----> UNIT CONFLICT at 0.07 sec ----> 543 [binary,541.1,20.1] $ANS(neg_th_11). Length of proof is 11. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 20 [] -P(i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p)))|$ANS(neg_th_11). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 543 [binary,541.1,20.1] $ANS(neg_th_11). ------------ end of proof ------------- given clause #57: (wt=2) 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). -------- PROOF -------- 551 [binary,550.1,19.1] $ANS(neg_th_10). ----> UNIT CONFLICT at 0.07 sec ----> 551 [binary,550.1,19.1] $ANS(neg_th_10). Length of proof is 20. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 19 [] -P(i(p,i(i(i(n(p),p),p),i(i(q,p),p))))|$ANS(neg_th_10). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 550 [hyper,1,86,525] P(i(x,i(y,i(i(z,x),x)))). 551 [binary,550.1,19.1] $ANS(neg_th_10). ------------ end of proof ------------- given clause #58: (wt=2) 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). -------- PROOF -------- 566 [binary,565.1,23.1] $ANS(neg_th_14). ----> UNIT CONFLICT at 0.07 sec ----> 566 [binary,565.1,23.1] $ANS(neg_th_14). Length of proof is 17. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 23 [] -P(i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r)))|$ANS(neg_th_14). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 566 [binary,565.1,23.1] $ANS(neg_th_14). ------------ end of proof ------------- given clause #59: (wt=2) 528 [hyper,1,122,519] P(i(i(x,y),i(i(i(z,z),u),i(i(y,v),u)))). given clause #60: (wt=2) 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). given clause #61: (wt=2) 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). given clause #62: (wt=2) 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). -------- PROOF -------- 627 [binary,626.1,24.1] $ANS(neg_th_15). ----> UNIT CONFLICT at 0.09 sec ----> 627 [binary,626.1,24.1] $ANS(neg_th_15). Length of proof is 18. Level of proof is 10. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 24 [] -P(i(i(n(p),q),i(i(q,p),p)))|$ANS(neg_th_15). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 627 [binary,626.1,24.1] $ANS(neg_th_15). ------------ end of proof ------------- given clause #63: (wt=2) 584 [hyper,1,90,528] P(i(i(x,i(i(y,y),z)),i(i(u,v),i(x,i(i(v,w),z))))). given clause #64: (wt=2) 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). -------- PROOF -------- 650 [binary,649.1,26.1] $ANS(neg_th_17). ----> UNIT CONFLICT at 0.09 sec ----> 650 [binary,649.1,26.1] $ANS(neg_th_17). Length of proof is 22. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 26 [] -P(i(p,i(i(q,p),p)))|$ANS(neg_th_17). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 650 [binary,649.1,26.1] $ANS(neg_th_17). ------------ end of proof ------------- given clause #65: (wt=2) 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). -------- PROOF -------- 666 [binary,665.1,54.1] $ANS(neg_th_45). ----> UNIT CONFLICT at 0.10 sec ----> 666 [binary,665.1,54.1] $ANS(neg_th_45). Length of proof is 19. Level of proof is 11. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 54 [] -P(i(i(s,i(q,p)),i(i(n(p),q),i(s,p))))|$ANS(neg_th_45). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 666 [binary,665.1,54.1] $ANS(neg_th_45). ------------ end of proof ------------- given clause #66: (wt=2) 639 [hyper,1,584,10] P(i(i(x,y),i(i(z,u),i(i(y,v),i(z,u))))). given clause #67: (wt=2) 648 [hyper,1,90,612] P(i(i(x,i(y,z)),i(i(n(z),z),i(x,z)))). given clause #68: (wt=2) 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). given clause #69: (wt=2) 653 [hyper,1,10,612] P(i(i(i(i(x,y),y),z),i(i(n(y),y),z))). given clause #70: (wt=2) 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). -------- PROOF -------- 764 [binary,763.1,58.1] $ANS(neg_th_49). ----> UNIT CONFLICT at 0.11 sec ----> 764 [binary,763.1,58.1] $ANS(neg_th_49). Length of proof is 20. Level of proof is 12. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 58 [] -P(i(i(n(p),n(q)),i(q,p)))|$ANS(neg_th_49). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 764 [binary,763.1,58.1] $ANS(neg_th_49). ------------ end of proof ------------- given clause #71: (wt=2) 669 [hyper,1,10,626] P(i(i(i(i(x,y),y),z),i(i(n(y),x),z))). given clause #72: (wt=2) 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). given clause #73: (wt=2) 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). -------- PROOF -------- 809 [binary,808.1,27.1] $ANS(neg_th_18). ----> UNIT CONFLICT at 0.12 sec ----> 809 [binary,808.1,27.1] $ANS(neg_th_18). Length of proof is 25. Level of proof is 13. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 27 [] -P(i(q,i(p,q)))|$ANS(neg_th_18). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 809 [binary,808.1,27.1] $ANS(neg_th_18). ------------ end of proof ------------- -------- PROOF -------- 810 [binary,808.1,26.1] $ANS(neg_th_17). ----> UNIT CONFLICT at 0.12 sec ----> 810 [binary,808.1,26.1] $ANS(neg_th_17). Length of proof is 25. Level of proof is 13. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 26 [] -P(i(p,i(i(q,p),p)))|$ANS(neg_th_17). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 810 [binary,808.1,26.1] $ANS(neg_th_17). ------------ end of proof ------------- given clause #74: (wt=2) 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). given clause #75: (wt=2) 805 [hyper,1,10,716] P(i(i(i(x,i(y,x)),z),i(i(y,i(u,x)),z))). given clause #76: (wt=2) 807 [hyper,1,716,626] P(i(x,i(i(n(x),y),x))). given clause #77: (wt=2) 808 [hyper,1,716,541] P(i(x,i(y,x))). -------- PROOF -------- 882 [binary,881.1,28.1] $ANS(neg_th_19). ----> UNIT CONFLICT at 0.13 sec ----> 882 [binary,881.1,28.1] $ANS(neg_th_19). Length of proof is 26. Level of proof is 14. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 28 [] -P(i(i(i(p,q),r),i(q,r)))|$ANS(neg_th_19). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 882 [binary,881.1,28.1] $ANS(neg_th_19). ------------ end of proof ------------- given clause #78: (wt=2) 844 [hyper,1,805,90] P(i(i(x,i(y,z)),i(i(u,x),i(z,i(u,z))))). given clause #79: (wt=2) 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). -------- PROOF -------- 937 [binary,936.1,19.1] $ANS(neg_th_10). ----> UNIT CONFLICT at 0.14 sec ----> 937 [binary,936.1,19.1] $ANS(neg_th_10). Length of proof is 27. Level of proof is 15. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 19 [] -P(i(p,i(i(i(n(p),p),p),i(i(q,p),p))))|$ANS(neg_th_10). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 936 [hyper,1,881,808] P(i(x,i(y,i(z,x)))). 937 [binary,936.1,19.1] $ANS(neg_th_10). ------------ end of proof ------------- -------- PROOF -------- 939 [binary,938.1,45.1] $ANS(neg_th_36). ----> UNIT CONFLICT at 0.14 sec ----> 939 [binary,938.1,45.1] $ANS(neg_th_36). Length of proof is 33. Level of proof is 15. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 45 [] -P(i(n(p),i(p,q)))|$ANS(neg_th_36). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 939 [binary,938.1,45.1] $ANS(neg_th_36). ------------ end of proof ------------- -------- PROOF -------- 942 [binary,941.1,29.1] $ANS(neg_th_20). ----> UNIT CONFLICT at 0.14 sec ----> 942 [binary,941.1,29.1] $ANS(neg_th_20). Length of proof is 31. Level of proof is 15. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 29 [] -P(i(p,i(i(p,q),q)))|$ANS(neg_th_20). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 942 [binary,941.1,29.1] $ANS(neg_th_20). ------------ end of proof ------------- given clause #80: (wt=2) 938 [hyper,1,881,763] P(i(n(x),i(x,y))). -------- PROOF -------- 962 [binary,961.1,57.1] $ANS(neg_th_48). ----> UNIT CONFLICT at 0.15 sec ----> 962 [binary,961.1,57.1] $ANS(neg_th_48). Length of proof is 34. Level of proof is 16. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 57 [] -P(i(i(n(p),q),i(n(q),p)))|$ANS(neg_th_48). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 962 [binary,961.1,57.1] $ANS(neg_th_48). ------------ end of proof ------------- -------- PROOF -------- 964 [binary,963.1,33.1] $ANS(neg_th_24). ----> UNIT CONFLICT at 0.15 sec ----> 964 [binary,963.1,33.1] $ANS(neg_th_24). Length of proof is 34. Level of proof is 16. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 33 [] -P(i(i(i(p,q),p),p))|$ANS(neg_th_24). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). 964 [binary,963.1,33.1] $ANS(neg_th_24). ------------ end of proof ------------- -------- PROOF -------- 982 [binary,981.1,46.1] $ANS(neg_th_37). ----> UNIT CONFLICT at 0.15 sec ----> 982 [binary,981.1,46.1] $ANS(neg_th_37). Length of proof is 34. Level of proof is 16. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 46 [] -P(i(i(i(p,q),r),i(n(p),r)))|$ANS(neg_th_37). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 981 [hyper,1,10,938] P(i(i(i(x,y),z),i(n(x),z))). 982 [binary,981.1,46.1] $ANS(neg_th_37). ------------ end of proof ------------- given clause #81: (wt=2) 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). -------- PROOF -------- 1007 [binary,1006.1,30.1] $ANS(neg_th_21). ----> UNIT CONFLICT at 0.15 sec ----> 1007 [binary,1006.1,30.1] $ANS(neg_th_21). Length of proof is 32. Level of proof is 16. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 30 [] -P(i(i(p,i(q,r)),i(q,i(p,r))))|$ANS(neg_th_21). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1007 [binary,1006.1,30.1] $ANS(neg_th_21). ------------ end of proof ------------- given clause #82: (wt=2) 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). -------- PROOF -------- 1076 [binary,1075.1,48.1] $ANS(neg_th_39). ----> UNIT CONFLICT at 0.16 sec ----> 1076 [binary,1075.1,48.1] $ANS(neg_th_39). Length of proof is 36. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 48 [] -P(i(n(n(p)),p))|$ANS(neg_th_39). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1076 [binary,1075.1,48.1] $ANS(neg_th_39). ------------ end of proof ------------- -------- PROOF -------- 1090 [binary,1089.1,59.1] $ANS(neg_th_50). ----> UNIT CONFLICT at 0.16 sec ----> 1090 [binary,1089.1,59.1] $ANS(neg_th_50). Length of proof is 35. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 59 [] -P(i(i(i(n(q),p),r),i(i(n(p),q),r)))|$ANS(neg_th_50). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1090 [binary,1089.1,59.1] $ANS(neg_th_50). ------------ end of proof ------------- -------- PROOF -------- 1093 [binary,1092.1,75.1] $ANS(neg_th_66). ----> UNIT CONFLICT at 0.16 sec ----> 1093 [binary,1092.1,75.1] $ANS(neg_th_66). Length of proof is 35. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 75 [] -P(i(n(i(p,q)),p))|$ANS(neg_th_66). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1092 [hyper,1,961,938] P(i(n(i(x,y)),x)). 1093 [binary,1092.1,75.1] $ANS(neg_th_66). ------------ end of proof ------------- -------- PROOF -------- 1095 [binary,1094.1,77.1] $ANS(neg_th_68). ----> UNIT CONFLICT at 0.16 sec ----> 1095 [binary,1094.1,77.1] $ANS(neg_th_68). Length of proof is 35. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 77 [] -P(i(n(i(p,n(q))),q))|$ANS(neg_th_68). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1094 [hyper,1,961,808] P(i(n(i(x,n(y))),y)). 1095 [binary,1094.1,77.1] $ANS(neg_th_68). ------------ end of proof ------------- given clause #83: (wt=2) 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). -------- PROOF -------- 1120 [binary,1119.1,39.1] $ANS(neg_th_30). ----> UNIT CONFLICT at 0.17 sec ----> 1120 [binary,1119.1,39.1] $ANS(neg_th_30). Length of proof is 35. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 39 [] -P(i(i(p,i(p,q)),i(p,q)))|$ANS(neg_th_30). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). 1119 [hyper,1,81,963] P(i(i(x,i(x,y)),i(x,y))). 1120 [binary,1119.1,39.1] $ANS(neg_th_30). ------------ end of proof ------------- given clause #84: (wt=2) 981 [hyper,1,10,938] P(i(i(i(x,y),z),i(n(x),z))). given clause #85: (wt=2) 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). -------- PROOF -------- 1193 [binary,1192.1,32.1] $ANS(neg_th_23). ----> UNIT CONFLICT at 0.18 sec ----> 1193 [binary,1192.1,32.1] $ANS(neg_th_23). Length of proof is 33. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 32 [] -P(i(i(i(q,i(p,r)),s),i(i(p,i(q,r)),s)))|$ANS(neg_th_23). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1192 [hyper,1,10,1006] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). 1193 [binary,1192.1,32.1] $ANS(neg_th_23). ------------ end of proof ------------- -------- PROOF -------- 1213 [binary,1212.1,34.1] $ANS(neg_th_25). ----> UNIT CONFLICT at 0.18 sec ----> 1213 [binary,1212.1,34.1] $ANS(neg_th_25). Length of proof is 33. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 34 [] -P(i(i(i(p,r),s),i(i(p,q),i(i(q,r),s))))|$ANS(neg_th_25). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1213 [binary,1212.1,34.1] $ANS(neg_th_25). ------------ end of proof ------------- -------- PROOF -------- 1217 [binary,1216.1,31.1] $ANS(neg_th_22). ----> UNIT CONFLICT at 0.18 sec ----> 1217 [binary,1216.1,31.1] $ANS(neg_th_22). Length of proof is 33. Level of proof is 17. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 31 [] -P(i(i(q,r),i(i(p,q),i(p,r))))|$ANS(neg_th_22). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1216 [hyper,1,1006,10] P(i(i(x,y),i(i(z,x),i(z,y)))). 1217 [binary,1216.1,31.1] $ANS(neg_th_22). ------------ end of proof ------------- given clause #86: (wt=2) 1008 [hyper,1,83,941] P(i(i(n(x),x),i(i(x,y),y))). given clause #87: (wt=2) 1075 [hyper,1,671,961] P(i(n(n(x)),x)). -------- PROOF -------- 1237 [binary,1236.1,49.1] $ANS(neg_th_40). ----> UNIT CONFLICT at 0.19 sec ----> 1237 [binary,1236.1,49.1] $ANS(neg_th_40). Length of proof is 37. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 49 [] -P(i(p,n(n(p))))|$ANS(neg_th_40). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1236 [hyper,1,763,1075] P(i(x,n(n(x)))). 1237 [binary,1236.1,49.1] $ANS(neg_th_40). ------------ end of proof ------------- -------- PROOF -------- 1240 [binary,1239.1,47.1] $ANS(neg_th_38). ----> UNIT CONFLICT at 0.19 sec ----> 1240 [binary,1239.1,47.1] $ANS(neg_th_38). Length of proof is 37. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 47 [] -P(i(i(p,n(p)),n(p)))|$ANS(neg_th_38). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1239 [hyper,1,626,1075] P(i(i(x,n(x)),n(x))). 1240 [binary,1239.1,47.1] $ANS(neg_th_38). ------------ end of proof ------------- -------- PROOF -------- 1257 [binary,1256.1,51.1] $ANS(neg_th_42). ----> UNIT CONFLICT at 0.19 sec ----> 1257 [binary,1256.1,51.1] $ANS(neg_th_42). Length of proof is 37. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 51 [] -P(i(i(i(n(n(p)),q),r),i(i(p,q),r)))|$ANS(neg_th_42). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 1257 [binary,1256.1,51.1] $ANS(neg_th_42). ------------ end of proof ------------- -------- PROOF -------- 1262 [binary,1261.1,50.1] $ANS(neg_th_41). ----> UNIT CONFLICT at 0.19 sec ----> 1262 [binary,1261.1,50.1] $ANS(neg_th_41). Length of proof is 37. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 50 [] -P(i(i(p,q),i(n(n(p)),q)))|$ANS(neg_th_41). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1261 [hyper,1,10,1075] P(i(i(x,y),i(n(n(x)),y))). 1262 [binary,1261.1,50.1] $ANS(neg_th_41). ------------ end of proof ------------- given clause #88: (wt=2) 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). -------- PROOF -------- 1278 [binary,1277.1,71.1] $ANS(neg_th_62). ----> UNIT CONFLICT at 0.19 sec ----> 1278 [binary,1277.1,71.1] $ANS(neg_th_62). Length of proof is 36. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 71 [] -P(i(i(n(n(p)),q),i(p,q)))|$ANS(neg_th_62). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1277 [hyper,1,1089,763] P(i(i(n(n(x)),y),i(x,y))). 1278 [binary,1277.1,71.1] $ANS(neg_th_62). ------------ end of proof ------------- -------- PROOF -------- 1281 [binary,1280.1,62.1] $ANS(neg_th_53). ----> UNIT CONFLICT at 0.19 sec ----> 1281 [binary,1280.1,62.1] $ANS(neg_th_53). Length of proof is 36. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 62 [] -P(i(i(n(p),q),i(i(p,q),q)))|$ANS(neg_th_53). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1280 [hyper,1,1089,626] P(i(i(n(x),y),i(i(x,y),y))). 1281 [binary,1280.1,62.1] $ANS(neg_th_53). ------------ end of proof ------------- given clause #89: (wt=2) 1092 [hyper,1,961,938] P(i(n(i(x,y)),x)). given clause #90: (wt=2) 1094 [hyper,1,961,808] P(i(n(i(x,n(y))),y)). given clause #91: (wt=2) 1119 [hyper,1,81,963] P(i(i(x,i(x,y)),i(x,y))). given clause #92: (wt=2) 1183 [hyper,1,188,1006] P(i(i(n(x),x),i(i(y,x),i(i(x,z),z)))). given clause #93: (wt=2) 1184 [hyper,1,182,1006] P(i(i(n(x),y),i(i(y,x),i(i(x,z),z)))). given clause #94: (wt=2) 1192 [hyper,1,10,1006] P(i(i(i(x,i(y,z)),u),i(i(y,i(x,z)),u))). given clause #95: (wt=2) 1201 [hyper,1,1006,626] P(i(i(x,y),i(i(n(y),x),y))). -------- PROOF -------- 1512 [binary,1511.1,74.1] $ANS(neg_th_65). ----> UNIT CONFLICT at 0.22 sec ----> 1512 [binary,1511.1,74.1] $ANS(neg_th_65). Length of proof is 34. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 74 [] -P(i(i(n(q),n(i(p,p))),q))|$ANS(neg_th_65). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1201 [hyper,1,1006,626] P(i(i(x,y),i(i(n(y),x),y))). 1511 [hyper,1,1201,136] P(i(i(n(x),n(i(y,y))),x)). 1512 [binary,1511.1,74.1] $ANS(neg_th_65). ------------ end of proof ------------- given clause #96: (wt=2) 1203 [hyper,1,1006,528] P(i(i(i(x,x),y),i(i(z,u),i(i(u,v),y)))). given clause #97: (wt=2) 1210 [hyper,1,1006,115] P(i(i(x,y),i(i(y,z),i(i(z,u),i(x,u))))). given clause #98: (wt=2) 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). -------- PROOF -------- 1631 [binary,1630.1,36.1] $ANS(neg_th_27). ----> UNIT CONFLICT at 0.23 sec ----> 1631 [binary,1630.1,36.1] $ANS(neg_th_27). Length of proof is 38. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 36 [] -P(i(i(i(p,q),q),i(i(q,p),p)))|$ANS(neg_th_27). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1630 [hyper,1,1212,963] P(i(i(i(x,y),z),i(i(z,x),x))). 1631 [binary,1630.1,36.1] $ANS(neg_th_27). ------------ end of proof ------------- -------- PROOF -------- 1632 [binary,1630.1,35.1] $ANS(neg_th_26). ----> UNIT CONFLICT at 0.23 sec ----> 1632 [binary,1630.1,35.1] $ANS(neg_th_26). Length of proof is 38. Level of proof is 18. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 35 [] -P(i(i(i(p,q),r),i(i(r,p),p)))|$ANS(neg_th_26). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1630 [hyper,1,1212,963] P(i(i(i(x,y),z),i(i(z,x),x))). 1632 [binary,1630.1,35.1] $ANS(neg_th_26). ------------ end of proof ------------- given clause #99: (wt=2) 1216 [hyper,1,1006,10] P(i(i(x,y),i(i(z,x),i(z,y)))). given clause #100: (wt=2) 1230 [hyper,1,90,1008] P(i(i(x,i(y,z)),i(i(n(y),y),i(x,z)))). given clause #101: (wt=2) 1233 [hyper,1,10,1008] P(i(i(i(i(x,y),y),z),i(i(n(x),x),z))). given clause #102: (wt=2) 1236 [hyper,1,763,1075] P(i(x,n(n(x)))). given clause #103: (wt=2) 1239 [hyper,1,626,1075] P(i(i(x,n(x)),n(x))). -------- PROOF -------- 1958 [binary,1957.1,52.1] $ANS(neg_th_43). ----> UNIT CONFLICT at 0.26 sec ----> 1958 [binary,1957.1,52.1] $ANS(neg_th_43). Length of proof is 41. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 52 [] -P(i(i(p,q),i(i(q,n(p)),n(p))))|$ANS(neg_th_43). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1239 [hyper,1,626,1075] P(i(i(x,n(x)),n(x))). 1957 [hyper,1,1212,1239] P(i(i(x,y),i(i(y,n(x)),n(x)))). 1958 [binary,1957.1,52.1] $ANS(neg_th_43). ------------ end of proof ------------- given clause #104: (wt=2) 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). -------- PROOF -------- 2006 [binary,2005.1,55.1] $ANS(neg_th_46). ----> UNIT CONFLICT at 0.26 sec ----> 2006 [binary,2005.1,55.1] $ANS(neg_th_46). Length of proof is 38. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 55 [] -P(i(i(p,q),i(n(q),n(p))))|$ANS(neg_th_46). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 2005 [hyper,1,1256,961] P(i(i(x,y),i(n(y),n(x)))). 2006 [binary,2005.1,55.1] $ANS(neg_th_46). ------------ end of proof ------------- -------- PROOF -------- 2009 [binary,2008.1,56.1] $ANS(neg_th_47). ----> UNIT CONFLICT at 0.27 sec ----> 2009 [binary,2008.1,56.1] $ANS(neg_th_47). Length of proof is 38. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 56 [] -P(i(i(p,n(q)),i(q,n(p))))|$ANS(neg_th_47). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 2008 [hyper,1,1256,763] P(i(i(x,n(y)),i(y,n(x)))). 2009 [binary,2008.1,56.1] $ANS(neg_th_47). ------------ end of proof ------------- given clause #105: (wt=2) 1261 [hyper,1,10,1075] P(i(i(x,y),i(n(n(x)),y))). given clause #106: (wt=2) 1277 [hyper,1,1089,763] P(i(i(n(n(x)),y),i(x,y))). given clause #107: (wt=2) 1280 [hyper,1,1089,626] P(i(i(n(x),y),i(i(x,y),y))). -------- PROOF -------- 2151 [binary,2150.1,63.1] $ANS(neg_th_54). ----> UNIT CONFLICT at 0.27 sec ----> 2151 [binary,2150.1,63.1] $ANS(neg_th_54). Length of proof is 40. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 63 [] -P(i(i(p,q),i(i(n(p),q),q)))|$ANS(neg_th_54). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 1280 [hyper,1,1089,626] P(i(i(n(x),y),i(i(x,y),y))). 2150 [hyper,1,1256,1280] P(i(i(x,y),i(i(n(x),y),y))). 2151 [binary,2150.1,63.1] $ANS(neg_th_54). ------------ end of proof ------------- -------- PROOF -------- 2175 [binary,2174.1,65.1] $ANS(neg_th_56). ----> UNIT CONFLICT at 0.27 sec ----> 2175 [binary,2174.1,65.1] $ANS(neg_th_56). Length of proof is 37. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 65 [] -P(i(i(i(i(p,q),q),r),i(i(n(p),q),r)))|$ANS(neg_th_56). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1280 [hyper,1,1089,626] P(i(i(n(x),y),i(i(x,y),y))). 2174 [hyper,1,10,1280] P(i(i(i(i(x,y),y),z),i(i(n(x),y),z))). 2175 [binary,2174.1,65.1] $ANS(neg_th_56). ------------ end of proof ------------- given clause #108: (wt=2) 1282 [hyper,1,1089,526] P(i(i(n(x),y),i(z,i(i(x,y),y)))). given clause #109: (wt=2) 1288 [hyper,1,1089,151] P(i(i(n(x),y),i(i(y,z),i(i(x,y),z)))). given clause #110: (wt=2) 1358 [hyper,1,81,1119] P(i(i(i(x,y),x),i(i(x,y),y))). given clause #111: (wt=2) 1371 [hyper,1,10,1183] P(i(i(i(i(x,y),i(i(y,z),z)),u),i(i(n(y),y),u))). given clause #112: (wt=2) 1373 [hyper,1,1089,1184] P(i(i(n(x),y),i(i(x,y),i(i(y,z),z)))). given clause #113: (wt=2) 1381 [hyper,1,270,1184] P(i(x,i(i(i(n(x),y),z),i(i(z,u),u)))). given clause #114: (wt=2) 1386 [hyper,1,10,1184] P(i(i(i(i(x,y),i(i(y,z),z)),u),i(i(n(y),x),u))). given clause #115: (wt=2) 1391 [hyper,1,1184,938] P(i(i(i(x,y),x),i(i(x,z),z))). given clause #116: (wt=2) 1394 [hyper,1,1184,503] P(i(i(i(x,x),y),i(i(y,z),z))). given clause #117: (wt=2) 1407 [hyper,1,1184,12] P(i(i(i(n(n(x)),y),x),i(i(x,z),z))). given clause #118: (wt=2) 1430 [hyper,1,1192,665] P(i(i(x,i(y,z)),i(i(n(z),x),i(y,z)))). given clause #119: (wt=2) 1452 [hyper,1,1192,90] P(i(i(x,i(y,z)),i(i(u,x),i(y,i(u,z))))). given clause #120: (wt=2) 1471 [hyper,1,122,1201] P(i(i(n(x),y),i(i(z,x),i(i(y,z),x)))). -------- PROOF -------- 2581 [binary,2580.1,68.1] $ANS(neg_th_59). ----> UNIT CONFLICT at 0.33 sec ----> 2581 [binary,2580.1,68.1] $ANS(neg_th_59). Length of proof is 40. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 68 [] -P(i(i(n(p),r),i(i(q,r),i(i(p,q),r))))|$ANS(neg_th_59). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1201 [hyper,1,1006,626] P(i(i(x,y),i(i(n(y),x),y))). 1471 [hyper,1,122,1201] P(i(i(n(x),y),i(i(z,x),i(i(y,z),x)))). 2580 [hyper,1,1089,1471] P(i(i(n(x),y),i(i(z,y),i(i(x,z),y)))). 2581 [binary,2580.1,68.1] $ANS(neg_th_59). ------------ end of proof ------------- given clause #121: (wt=2) 1482 [hyper,1,1201,1092] P(i(i(n(x),n(i(x,y))),x)). given clause #122: (wt=2) 1511 [hyper,1,1201,136] P(i(i(n(x),n(i(y,y))),x)). given clause #123: (wt=2) 1527 [hyper,1,669,1203] P(i(i(n(x),x),i(i(y,z),i(i(z,u),x)))). given clause #124: (wt=2) 1611 [hyper,1,1210,11] P(i(i(x,y),i(i(y,z),i(i(n(x),x),z)))). given clause #125: (wt=2) 1618 [hyper,1,669,1212] P(i(i(n(x),y),i(i(y,z),i(i(z,x),x)))). -------- PROOF -------- 2731 [binary,2730.1,66.1] $ANS(neg_th_57). ----> UNIT CONFLICT at 0.35 sec ----> 2731 [binary,2730.1,66.1] $ANS(neg_th_57). Length of proof is 41. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 66 [] -P(i(i(n(p),r),i(i(p,q),i(i(q,r),r))))|$ANS(neg_th_57). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 669 [hyper,1,10,626] P(i(i(i(i(x,y),y),z),i(i(n(y),x),z))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1089 [hyper,1,10,961] P(i(i(i(n(x),y),z),i(i(n(y),x),z))). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1618 [hyper,1,669,1212] P(i(i(n(x),y),i(i(y,z),i(i(z,x),x)))). 2730 [hyper,1,1089,1618] P(i(i(n(x),y),i(i(x,z),i(i(z,y),y)))). 2731 [binary,2730.1,66.1] $ANS(neg_th_57). ------------ end of proof ------------- given clause #126: (wt=2) 1625 [hyper,1,1212,1201] P(i(i(x,y),i(i(y,z),i(i(n(z),x),z)))). given clause #127: (wt=2) 1630 [hyper,1,1212,963] P(i(i(i(x,y),z),i(i(z,x),x))). -------- PROOF -------- 2875 [binary,2874.1,37.1] $ANS(neg_th_28). ----> UNIT CONFLICT at 0.36 sec ----> 2875 [binary,2874.1,37.1] $ANS(neg_th_28). Length of proof is 39. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 37 [] -P(i(i(i(i(r,p),p),s),i(i(i(p,q),r),s)))|$ANS(neg_th_28). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 963 [hyper,1,626,938] P(i(i(i(x,y),x),x)). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1630 [hyper,1,1212,963] P(i(i(i(x,y),z),i(i(z,x),x))). 2874 [hyper,1,10,1630] P(i(i(i(i(x,y),y),z),i(i(i(y,u),x),z))). 2875 [binary,2874.1,37.1] $ANS(neg_th_28). ------------ end of proof ------------- given clause #128: (wt=2) 1658 [hyper,1,1212,1216] P(i(i(x,y),i(i(y,z),i(i(u,x),i(u,z))))). given clause #129: (wt=2) 1660 [hyper,1,1192,1216] P(i(i(x,i(y,z)),i(i(u,y),i(u,i(x,z))))). given clause #130: (wt=2) 1665 [hyper,1,805,1216] P(i(i(x,i(y,z)),i(i(u,z),i(u,i(x,z))))). given clause #131: (wt=2) 1673 [hyper,1,122,1216] P(i(i(x,y),i(i(z,u),i(i(y,z),i(x,u))))). given clause #132: (wt=2) 1677 [hyper,1,90,1216] P(i(i(x,i(y,z)),i(i(z,u),i(x,i(y,u))))). given clause #133: (wt=2) 1680 [hyper,1,10,1216] P(i(i(i(i(x,y),i(x,z)),u),i(i(y,z),u))). given clause #134: (wt=2) 1686 [hyper,1,1216,1184] P(i(i(x,i(n(y),z)),i(x,i(i(z,y),i(i(y,u),u))))). given clause #135: (wt=2) 1687 [hyper,1,1216,1183] P(i(i(x,i(n(y),y)),i(x,i(i(z,y),i(i(y,u),u))))). given clause #136: (wt=2) 1730 [hyper,1,1216,177] P(i(i(x,i(n(y),y)),i(x,i(i(y,z),i(i(u,y),z))))). given clause #137: (wt=2) 1734 [hyper,1,1216,151] P(i(i(x,i(n(y),z)),i(x,i(i(y,u),i(i(z,y),u))))). given clause #138: (wt=2) 1805 [hyper,1,1233,1212] P(i(i(n(x),x),i(i(x,y),i(i(y,z),z)))). given clause #139: (wt=2) 1809 [hyper,1,1233,808] P(i(i(n(x),x),i(y,i(i(x,z),z)))). given clause #140: (wt=2) 1822 [hyper,1,1233,10] P(i(i(n(x),x),i(i(y,z),i(i(x,y),z)))). given clause #141: (wt=2) 1957 [hyper,1,1212,1239] P(i(i(x,y),i(i(y,n(x)),n(x)))). -------- PROOF -------- 3494 [binary,3493.1,53.1] $ANS(neg_th_44). ----> UNIT CONFLICT at 0.47 sec ----> 3494 [binary,3493.1,53.1] $ANS(neg_th_44). Length of proof is 42. Level of proof is 20. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 53 [] -P(i(i(s,i(q,n(p))),i(i(p,q),i(s,n(p)))))|$ANS(neg_th_44). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1212 [hyper,1,1006,95] P(i(i(i(x,y),z),i(i(x,u),i(i(u,y),z)))). 1239 [hyper,1,626,1075] P(i(i(x,n(x)),n(x))). 1957 [hyper,1,1212,1239] P(i(i(x,y),i(i(y,n(x)),n(x)))). 3493 [hyper,1,90,1957] P(i(i(x,i(y,n(z))),i(i(z,y),i(x,n(z))))). 3494 [binary,3493.1,53.1] $ANS(neg_th_44). ------------ end of proof ------------- given clause #142: (wt=2) 2005 [hyper,1,1256,961] P(i(i(x,y),i(n(y),n(x)))). -------- PROOF -------- 3557 [binary,3556.1,60.1] $ANS(neg_th_51). ----> UNIT CONFLICT at 0.48 sec ----> 3557 [binary,3556.1,60.1] $ANS(neg_th_51). Length of proof is 42. Level of proof is 20. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 60 [] -P(i(i(p,i(q,r)),i(p,i(n(r),n(q)))))|$ANS(neg_th_51). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 941 [hyper,1,881,626] P(i(x,i(i(x,y),y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1006 [hyper,1,90,941] P(i(i(x,i(y,z)),i(y,i(x,z)))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1216 [hyper,1,1006,10] P(i(i(x,y),i(i(z,x),i(z,y)))). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 2005 [hyper,1,1256,961] P(i(i(x,y),i(n(y),n(x)))). 3556 [hyper,1,1216,2005] P(i(i(x,i(y,z)),i(x,i(n(z),n(y))))). 3557 [binary,3556.1,60.1] $ANS(neg_th_51). ------------ end of proof ------------- -------- PROOF -------- 3637 [binary,3636.1,76.1] $ANS(neg_th_67). ----> UNIT CONFLICT at 0.49 sec ----> 3637 [binary,3636.1,76.1] $ANS(neg_th_67). Length of proof is 39. Level of proof is 20. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 76 [] -P(i(n(i(p,q)),n(q)))|$ANS(neg_th_67). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,i(i(n(y),y),y))). 554 [hyper,1,10,525] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),z),u))). 565 [hyper,1,10,526] P(i(i(i(x,i(i(y,z),z)),u),i(i(n(z),y),u))). 612 [hyper,1,554,11] P(i(i(n(x),x),i(i(y,x),x))). 626 [hyper,1,565,11] P(i(i(n(x),y),i(i(y,x),x))). 649 [hyper,1,86,612] P(i(x,i(i(y,x),x))). 665 [hyper,1,90,626] P(i(i(x,i(y,z)),i(i(n(z),y),i(x,z)))). 671 [hyper,1,626,503] P(i(i(i(x,x),y),y)). 716 [hyper,1,90,649] P(i(i(x,i(y,z)),i(z,i(x,z)))). 763 [hyper,1,665,12] P(i(i(n(x),n(y)),i(y,x))). 808 [hyper,1,716,541] P(i(x,i(y,x))). 881 [hyper,1,10,808] P(i(i(i(x,y),z),i(y,z))). 938 [hyper,1,881,763] P(i(n(x),i(x,y))). 961 [hyper,1,665,938] P(i(i(n(x),y),i(n(y),x))). 1075 [hyper,1,671,961] P(i(n(n(x)),x)). 1256 [hyper,1,95,1075] P(i(i(i(n(n(x)),y),z),i(i(x,y),z))). 2005 [hyper,1,1256,961] P(i(i(x,y),i(n(y),n(x)))). 3636 [hyper,1,2005,808] P(i(n(i(x,y)),n(y))). 3637 [binary,3636.1,76.1] $ANS(neg_th_67). ------------ end of proof ------------- given clause #143: (wt=2) 2008 [hyper,1,1256,763] P(i(i(x,n(y)),i(y,n(x)))). -------- PROOF -------- 3709 [binary,3708.1,61.1] $ANS(neg_th_52). ----> UNIT CONFLICT at 0.49 sec ----> 3709 [binary,3708.1,61.1] $ANS(neg_th_52). Length of proof is 42. Level of proof is 20. ---------------- PROOF ---------------- 1 [] -P(i(x,y))| -P(x)|P(y). 10 [] P(i(i(x,y),i(i(y,z),i(x,z)))). 11 [] P(i(i(n(x),x),x)). 12 [] P(i(x,i(n(x),y))). 61 [] -P(i(i(p,i(q,n(r))),i(p,i(r,n(q)))))|$ANS(neg_th_52). 81 [hyper,1,10,10] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))). 83 [hyper,1,10,11] P(i(i(x,y),i(i(n(x),x),y))). 86 [hyper,1,10,12] P(i(i(i(n(x),y),z),i(x,z))). 90 [hyper,1,81,81] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))). 95 [hyper,1,81,10] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))). 101 [hyper,1,83,12] P(i(i(n(x),x),i(n(x),y))). 105 [hyper,1,81,86] P(i(i(x,n(y)),i(y,i(x,z)))). 110 [hyper,1,86,11] P(i(x,x)). 122 [hyper,1,90,95] P(i(i(x,i(i(y,z),u)),i(i(y,v),i(x,i(i(v,z),u))))). 135 [hyper,1,10,101] P(i(i(i(n(x),y),z),i(i(n(x),x),z))). 136 [hyper,1,12,110] P(i(n(i(x,x)),y)). 151 [hyper,1,122,83] P(i(i(n(x),y),i(i(x,z),i(i(y,x),z)))). 177 [hyper,1,135,151] P(i(i(n(x),x),i(i(x,y),i(i(z,x),y)))). 182 [hyper,1,10,151] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),z),u))). 188 [hyper,1,10,177] P(i(i(i(i(x,y),i(i(z,x),y)),u),i(i(n(x),x),u))). 253 [hyper,1,105,136] P(i(x,i(n(i(y,y)),z))). 292 [hyper,1,10,253] P(i(i(i(n(i(x,x)),y),z),i(u,z))). 503 [hyper,1,292,11] P(i(x,i(y,y))). 519 [hyper,1,10,503] P(i(i(i(x,x),y),i(z,y))). 525 [hyper,1,188,519] P(i(i(n(x),x),i(y,i(i(z,x),x)))). 526 [hyper,1,182,519] P(i(i(n(x),y),i(z,i(i(y,x),x)))). 541 [hyper,1,519,83] P(i(x,