----- Otter 3.3, August 2003 -----
The process was started by mccune on gyro.thornwood,
Wed Aug  6 14:25:59 2003
The command was "../../bin/otter".  The process ID is 5965.

set(hyper_res).
assign(max_weight,22).
assign(change_limit_after,1000).
assign(new_max_weight,16).
assign(max_proofs,4).
clear(print_kept).
clear(back_sub).
assign(max_mem,24000).
assign(max_distinct_vars,4).
assign(pick_given_ratio,3).
set(order_history).
set(input_sos_first).

weight_list(pick_given).
weight(P(i(n(n(x)),x)),2).
weight(P(i(x,n(n(x)))),2).
weight(P(i(i(x,y),i(i(z,x),i(z,y)))),2).
weight(P(i(i(x,y),i(n(y),n(x)))),2).
weight(P(i(i(i(x,y),i(y,x)),i(y,x))),2).
weight(P(i(x,i(y,x))),2).
weight(P(i(i(x,y),i(i(y,z),i(x,z)))),2).
weight(P(i(i(i(x,y),y),i(i(y,x),x))),2).
weight(P(i(i(n(x),n(y)),i(y,x))),2).
weight(i($(1),$(2)),1).
end_of_list.

list(usable).
1 [] -P(i(x,y))| -P(x)|P(y).
end_of_list.

list(sos).
2 [] P(i(x,i(y,x))).
3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).
4 [] P(i(i(i(x,y),y),i(i(y,x),x))).
5 [] P(i(i(n(x),n(y)),i(y,x))).
end_of_list.

list(passive).
6 [] -P(i(n(n(a)),a))|$ANS(lemma_24).
7 [] -P(i(a,n(n(a))))|$ANS(lemma_29).
8 [] -P(i(i(a,b),i(i(c,a),i(c,b))))|$ANS(lemma_25).
9 [] -P(i(i(a,b),i(n(b),n(a))))|$ANS(lemma_36).
10 [] -P(i(i(i(a,b),i(b,a)),i(b,a)))|$ANS(thm_MV5).
end_of_list.

list(demodulators).
11 [] n(n(n(x)))=junk.
12 [] i(i(x,x),y)=junk.
13 [] i(y,i(x,x))=junk.
14 [] i(n(i(x,x)),y)=junk.
15 [] i(y,n(i(x,x)))=junk.
16 [] i(junk,x)=junk.
17 [] i(x,junk)=junk.
18 [] n(junk)=junk.
19 [] P(junk)=$T.
end_of_list.

======= end of input processing =======

=========== start of search ===========

given clause #1: (wt=-2147483647) 2 [] P(i(x,i(y,x))).

given clause #2: (wt=-2147483647) 3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).

given clause #3: (wt=-2147483647) 4 [] P(i(i(i(x,y),y),i(i(y,x),x))).

given clause #4: (wt=-2147483647) 5 [] P(i(i(n(x),n(y)),i(y,x))).

given clause #5: (wt=23) 20 [hyper,1,2,2] P(i(x,i(y,i(z,y)))).

given clause #6: (wt=17) 23 [hyper,1,3,2] P(i(i(i(x,y),z),i(y,z))).

given clause #7: (wt=12) 33 [hyper,1,23,5] P(i(n(x),i(x,y))).

given clause #8: (wt=17) 28 [hyper,1,4,20] P(i(i(i(x,i(y,x)),z),z)).

given clause #9: (wt=32) 21 [hyper,1,3,3] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).

given clause #10: (wt=5) 39 [hyper,1,23,28] P(i(x,x)).

given clause #11: (wt=17) 34 [hyper,1,23,4] P(i(x,i(i(x,y),y))).

given clause #12: (wt=18) 51 [hyper,1,34,33] P(i(i(i(n(x),i(x,y)),z),z)).

given clause #13: (wt=65) 22 [hyper,1,2,3] P(i(x,i(i(y,z),i(i(z,u),i(y,u))))).

given clause #14: (wt=19) 37 [hyper,1,3,33] P(i(i(i(x,y),z),i(n(x),z))).

given clause #15: (wt=13) 73 [hyper,1,37,5] P(i(n(n(x)),i(y,x))).

given clause #16: (wt=15) 70 [hyper,1,37,28] P(i(n(i(x,i(y,x))),z)).

given clause #17: (wt=32) 24 [hyper,1,3,4] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).

given clause #18: (wt=15) 71 [hyper,1,37,23] P(i(n(i(x,y)),i(y,z))).

given clause #19: (wt=16) 68 [hyper,1,37,51] P(i(n(i(n(x),i(x,y))),z)).

given clause #20: (wt=17) 62 [hyper,1,37,37] P(i(n(i(x,y)),i(n(x),z))).

given clause #21: (wt=47) 25 [hyper,1,2,4] P(i(x,i(i(i(y,z),z),i(i(z,y),y)))).

given clause #22: (wt=19) 75 [hyper,1,34,73] P(i(i(i(n(n(x)),i(y,x)),z),z)).

given clause #23: (wt=17) 105 [hyper,1,37,75] P(i(n(i(n(n(x)),i(y,x))),z)).

given clause #24: (wt=19) 89 [hyper,1,24,37] P(i(i(i(x,y),y),i(n(y),x))).

given clause #25: (wt=29) 26 [hyper,1,3,5] P(i(i(i(x,y),z),i(i(n(y),n(x)),z))).

given clause #26: (wt=13) 116 [hyper,1,23,89] P(i(x,i(n(x),y))).

given clause #27: (wt=17) 114 [hyper,1,37,89] P(i(n(i(x,y)),i(n(y),x))).

given clause #28: (wt=17) 141 [hyper,1,116,116] P(i(n(i(x,i(n(x),y))),z)).

given clause #29: (wt=35) 27 [hyper,1,2,5] P(i(x,i(i(n(y),n(z)),i(z,y)))).

given clause #30: (wt=18) 148 [hyper,1,3,116] P(i(i(i(n(x),y),z),i(x,z))).

given clause #31: (wt=16) 180 [hyper,1,37,148] P(i(n(i(n(x),y)),i(x,z))).

given clause #32: (wt=19) 143 [hyper,1,34,116] P(i(i(i(x,i(n(x),y)),z),z)).

given clause #33: (wt=23) 29 [hyper,1,3,20] P(i(i(i(x,i(y,x)),z),i(u,z))).

given clause #34: (wt=19) 146 [hyper,1,23,116] P(i(x,i(n(i(y,x)),z))).

given clause #35: (wt=19) 153 [hyper,1,116,71] P(i(n(i(n(i(x,y)),i(y,z))),u)).

given clause #36: (wt=19) 154 [hyper,1,116,70] P(i(n(i(n(i(x,i(y,x))),z)),u)).

given clause #37: (wt=47) 30 [hyper,1,2,20] P(i(x,i(y,i(z,i(u,z))))).

given clause #38: (wt=20) 49 [hyper,1,3,34] P(i(i(i(i(x,y),y),z),i(x,z))).

-------- PROOF -------- 242 [binary,241.1,8.1] $ANS(lemma_25).

----> UNIT CONFLICT at   0.02 sec ----> 242 [binary,241.1,8.1] $ANS(lemma_25).

Length of proof is 5.  Level of proof is 4.

---------------- PROOF ----------------

1 [] -P(i(x,y))| -P(x)|P(y).
2 [] P(i(x,i(y,x))).
3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).
4 [] P(i(i(i(x,y),y),i(i(y,x),x))).
8 [] -P(i(i(a,b),i(i(c,a),i(c,b))))|$ANS(lemma_25).
21 [hyper,1,3,3] P(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))).
23 [hyper,1,3,2] P(i(i(i(x,y),z),i(y,z))).
34 [hyper,1,23,4] P(i(x,i(i(x,y),y))).
49 [hyper,1,3,34] P(i(i(i(i(x,y),y),z),i(x,z))).
241 [hyper,1,49,21] P(i(i(x,y),i(i(z,x),i(z,y)))).
242 [binary,241.1,8.1] $ANS(lemma_25).

------------ end of proof -------------


given clause #39: (wt=2) 241 [hyper,1,49,21] P(i(i(x,y),i(i(z,x),i(z,y)))).

given clause #40: (wt=18) 229 [hyper,1,37,49] P(i(n(i(i(x,y),y)),i(x,z))).

given clause #41: (wt=29) 31 [hyper,1,3,23] P(i(i(i(x,y),z),i(i(i(u,x),y),z))).

given clause #42: (wt=20) 138 [hyper,1,26,5] P(i(i(n(n(x)),n(n(y))),i(x,y))).

given clause #43: (wt=20) 142 [hyper,1,37,116] P(i(n(x),i(n(i(x,y)),z))).

given clause #44: (wt=20) 155 [hyper,1,116,68] P(i(n(i(n(i(n(x),i(x,y))),z)),u)).

given clause #45: (wt=35) 32 [hyper,1,2,23] P(i(x,i(i(i(y,z),u),i(z,u)))).

given clause #46: (wt=20) 190 [hyper,1,116,180] P(i(n(i(n(i(n(x),y)),i(x,z))),u)).

given clause #47: (wt=21) 74 [hyper,1,37,4] P(i(n(i(x,y)),i(i(y,x),x))).

given clause #48: (wt=21) 76 [hyper,1,3,73] P(i(i(i(x,y),z),i(n(n(y)),z))).
-------- PROOF -------- 338 [binary,337.1,6.1] $ANS(lemma_24).

----> UNIT CONFLICT at   0.04 sec ----> 338 [binary,337.1,6.1] $ANS(lemma_24).

Length of proof is 11.  Level of proof is 7.

---------------- PROOF ----------------

1 [] -P(i(x,y))| -P(x)|P(y).
2 [] P(i(x,i(y,x))).
3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).
4 [] P(i(i(i(x,y),y),i(i(y,x),x))).
5 [] P(i(i(n(x),n(y)),i(y,x))).
6 [] -P(i(n(n(a)),a))|$ANS(lemma_24).
23 [hyper,1,3,2] P(i(i(i(x,y),z),i(y,z))).
24 [hyper,1,3,4] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
33 [hyper,1,23,5] P(i(n(x),i(x,y))).
34 [hyper,1,23,4] P(i(x,i(i(x,y),y))).
37 [hyper,1,3,33] P(i(i(i(x,y),z),i(n(x),z))).
73 [hyper,1,37,5] P(i(n(n(x)),i(y,x))).
76 [hyper,1,3,73] P(i(i(i(x,y),z),i(n(n(y)),z))).
89 [hyper,1,24,37] P(i(i(i(x,y),y),i(n(y),x))).
116 [hyper,1,23,89] P(i(x,i(n(x),y))).
143 [hyper,1,34,116] P(i(i(i(x,i(n(x),y)),z),z)).
337 [hyper,1,76,143] P(i(n(n(x)),x)).
338 [binary,337.1,6.1] $ANS(lemma_24).

------------ end of proof -------------


given clause #49: (wt=29) 35 [hyper,1,23,3] P(i(x,i(i(x,y),i(z,y)))).

given clause #50: (wt=2) 337 [hyper,1,76,143] P(i(n(n(x)),x)).
-------- PROOF -------- 368 [binary,367.1,7.1] $ANS(lemma_29).

----> UNIT CONFLICT at   0.04 sec ----> 368 [binary,367.1,7.1] $ANS(lemma_29).

Length of proof is 12.  Level of proof is 8.

---------------- PROOF ----------------

1 [] -P(i(x,y))| -P(x)|P(y).
2 [] P(i(x,i(y,x))).
3 [] P(i(i(x,y),i(i(y,z),i(x,z)))).
4 [] P(i(i(i(x,y),y),i(i(y,x),x))).
5 [] P(i(i(n(x),n(y)),i(y,x))).
7 [] -P(i(a,n(n(a))))|$ANS(lemma_29).
23 [hyper,1,3,2] P(i(i(i(x,y),z),i(y,z))).
24 [hyper,1,3,4] P(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))).
33 [hyper,1,23,5] P(i(n(x),i(x,y))).
34 [hyper,1,23,4] P(i(x,i(i(x,y),y))).
37 [hyper,1,3,33] P(i(i(i(x,y),z),i(n(x),z))).
73 [hyper,1,37,5] P(i(n(n(x)),i(y,x))).
76 [hyper,1,3,73] P(i(i(i(x,y),z),i(n(n(y)),z))).
89 [hyper,1,24,37] P(i(i(i(x,y),y),i(n(y),x))).
116 [hyper,1,23,89] P(i(x,i(n(x),y))).
143 [hyper,1,34,116] P(i(i(i(x,i(n(x),y)),z),z)).
337 [hyper,1,76,143] P(i(n(n(x)),x)).
367 [hyper,1,5,337] P(i(x,n(n(x)))).
368 [binary,367.1,7.1] $ANS(lemma_29).

------------ end of proof -------------


given clause #51: (wt=2) 367 [hyper,1,5,337] P(i(x,n(n(x)))).

given clause #52: (wt=7) 418 [hyper,1,367,39] P(n(n(i(x,x)))).

given clause #53: (wt=23) 36 [hyper,1,23,2] P(i(x,i(y,i(z,x)))).

given clause #54: (wt=9) 392 [hyper,1,367,337] P(n(n(i(n(n(x)),x)))).

given clause #55: (wt=11) 364 [hyper,1,116,337] P(i(n(i(n(n(x)),x)),y)).

given clause #56: (wt=11) 370 [hyper,1,367,367] P(n(n(i(x,n(n(x)))))).

given clause #57: (wt=25) 38 [hyper,1,2,33] P(i(x,i(n(y),i(y,z)))).

given clause #58: (wt=13) 366 [hyper,1,34,337] P(i(i(i(n(n(x)),x),y),y)).

given clause #59: (wt=13) 375 [hyper,1,116,367] P(i(n(i(x,n(n(x)))),y)).

given clause #60: (wt=13) 385 [hyper,1,28,367] P(n(n(i(x,i(y,x))))).

given clause #61: (wt=38) 40 [hyper,1,3,28] P(i(i(x,y),i(i(i(z,i(u,z)),x),y))).

given clause #62: (wt=13) 440 [hyper,1,34,418] P(i(i(n(n(i(x,x))),y),y)).

given clause #63: (wt=13) 467 [hyper,1,367,364] P(n(n(i(n(i(n(n(x)),x)),y)))).

given clause #64: (wt=14) 378 [hyper,1,51,367] P(n(n(i(n(x),i(x,y))))).

given clause #65: (wt=35) 41 [hyper,1,2,28] P(i(x,i(i(i(y,i(z,y)),u),u))).

given clause #66: (wt=15) 327 [hyper,1,49,76] P(i(x,i(n(n(y)),y))).

given clause #67: (wt=15) 374 [hyper,1,143,367] P(n(n(i(x,i(n(x),y))))).

given clause #68: (wt=15) 377 [hyper,1,75,367] P(n(n(i(n(n(x)),i(y,x))))).

given clause #69: (wt=62) 42 [hyper,1,28,21] P(i(i(x,y),i(z,i(i(y,u),i(x,u))))).

given clause #70: (wt=15) 382 [hyper,1,34,367] P(i(i(i(x,n(n(x))),y),y)).

given clause #71: (wt=15) 388 [hyper,1,23,367] P(i(x,n(n(i(y,x))))).

given clause #72: (wt=11) 618 [hyper,1,5,388] P(i(n(i(x,n(y))),y)).

given clause #73: (wt=62) 43 [hyper,1,21,21] P(i(i(x,i(y,z)),i(i(u,y),i(x,i(u,z))))).

given clause #74: (wt=13) 665 [hyper,1,367,618] P(n(n(i(n(i(x,n(y))),y)))).

given clause #75: (wt=15) 441 [hyper,1,2,418] P(i(x,n(n(i(y,y))))).

given clause #76: (wt=15) 462 [hyper,1,142,392] P(i(n(i(n(i(n(n(x)),x)),y)),z)).

given clause #77: (wt=26) 44 [hyper,1,21,28] P(i(i(x,y),i(x,i(z,y)))).

given clause #78: (wt=15) 465 [hyper,1,34,392] P(i(i(n(n(i(n(n(x)),x))),y),y)).

given clause #79: (wt=15) 482 [hyper,1,367,366] P(n(n(i(i(i(n(n(x)),x),y),y)))).

given clause #80: (wt=15) 494 [hyper,1,367,375] P(n(n(i(n(i(x,n(n(x)))),y)))).

given clause #81: (wt=50) 45 [hyper,1,21,3] P(i(i(x,y),i(i(i(x,z),u),i(i(y,z),u)))).

given clause #82: (wt=15) 527 [hyper,1,367,440] P(n(n(i(i(n(n(i(x,x))),y),y)))).

given clause #83: (wt=15) 668 [hyper,1,116,618] P(i(n(i(n(i(x,n(y))),y)),z)).

given clause #84: (wt=16) 380 [hyper,1,37,367] P(i(n(x),n(n(i(x,y))))).

given clause #85: (wt=23) 46 [hyper,1,34,34] P(i(i(i(x,i(i(x,y),y)),z),z)).

given clause #86: (wt=9) 831 [hyper,1,5,380] P(i(n(i(x,y)),x)).

given clause #87: (wt=11) 848 [hyper,1,367,831] P(n(n(i(n(i(x,y)),x)))).

given clause #88: (wt=13) 851 [hyper,1,116,831] P(i(n(i(n(i(x,y)),x)),z)).

given clause #89: (wt=23) 47 [hyper,1,23,34] P(i(x,i(i(i(y,x),z),z))).

given clause #90: (wt=15) 853 [hyper,1,44,831] P(i(n(i(x,y)),i(z,x))).

given clause #91: (wt=15) 859 [hyper,1,34,831] P(i(i(i(n(i(x,y)),x),z),z)).

given clause #92: (wt=15) 863 [hyper,1,380,848] P(n(n(i(n(i(n(i(x,y)),x)),z)))).

given clause #93: (wt=44) 48 [hyper,1,21,34] P(i(i(x,y),i(i(i(i(y,z),i(x,z)),u),u))).

given clause #94: (wt=16) 390 [hyper,1,3,367] P(i(i(n(n(x)),y),i(x,y))).

given clause #95: (wt=17) 372 [hyper,1,148,367] P(i(x,n(n(i(n(x),y))))).

given clause #96: (wt=11) 1010 [hyper,1,5,372] P(i(n(i(n(n(x)),y)),x)).

given clause #97: (wt=35) 50 [hyper,1,2,34] P(i(x,i(y,i(i(y,z),z)))).

given clause #98: (wt=13) 1058 [hyper,1,367,1010] P(n(n(i(n(i(n(n(x)),y)),x)))).

given clause #99: (wt=15) 1061 [hyper,1,116,1010] P(i(n(i(n(i(n(n(x)),y)),x)),z)).

given clause #100: (wt=17) 376 [hyper,1,76,367] P(i(n(n(x)),n(n(i(y,x))))).

given clause #101: (wt=23) 52 [hyper,1,34,28] P(i(i(i(i(i(x,i(y,x)),z),z),u),u)).

given clause #102: (wt=11) 1106 [hyper,1,5,376] P(i(n(i(x,y)),n(y))).

given clause #103: (wt=13) 1114 [hyper,1,367,1106] P(n(n(i(n(i(x,y)),n(y))))).

given clause #104: (wt=15) 1117 [hyper,1,116,1106] P(i(n(i(n(i(x,y)),n(y))),z)).

given clause #105: (wt=23) 53 [hyper,1,34,23] P(i(i(i(i(i(x,y),z),i(y,z)),u),u)).

given clause #106: (wt=17) 412 [hyper,1,367,71] P(n(n(i(n(i(x,y)),i(y,z))))).

given clause #107: (wt=17) 413 [hyper,1,367,70] P(n(n(i(n(i(x,i(y,x))),z)))).

given clause #108: (wt=17) 472 [hyper,1,34,364] P(i(i(i(n(i(n(n(x)),x)),y),z),z)).

given clause #109: (wt=29) 54 [hyper,1,34,20] P(i(i(i(x,i(y,i(z,y))),u),u)).

given clause #110: (wt=17) 476 [hyper,1,142,370] P(i(n(i(n(i(x,n(n(x)))),y)),z)).

given clause #111: (wt=17) 479 [hyper,1,34,370] P(i(i(n(n(i(x,n(n(x))))),y),y)).

given clause #112: (wt=17) 485 [hyper,1,116,366] P(i(n(i(i(i(n(n(x)),x),y),y)),z)).

given clause #113: (wt=23) 55 [hyper,1,34,5] P(i(i(i(i(n(x),n(y)),i(y,x)),z),z)).

given clause #114: (wt=17) 530 [hyper,1,116,440] P(i(n(i(i(n(n(i(x,x))),y),y)),z)).

given clause #115: (wt=17) 550 [hyper,1,367,327] P(n(n(i(x,i(n(n(y)),y))))).

given clause #116: (wt=17) 579 [hyper,1,367,382] P(n(n(i(i(i(x,n(n(x))),y),y)))).

given clause #117: (wt=29) 56 [hyper,1,34,4] P(i(i(i(i(i(x,y),y),i(i(y,x),x)),z),z)).

given clause #118: (wt=17) 590 [hyper,1,24,382] P(i(i(i(n(n(x)),x),x),n(n(x)))).

given clause #119: (wt=17) 593 [hyper,1,440,388] P(n(n(i(x,n(n(i(y,y))))))).

given clause #120: (wt=17) 596 [hyper,1,367,388] P(n(n(i(x,n(n(i(y,x))))))).

given clause #121: (wt=38) 57 [hyper,1,34,3] P(i(i(i(i(x,y),i(i(y,z),i(x,z))),u),u)).

given clause #122: (wt=17) 673 [hyper,1,34,618] P(i(i(i(n(i(x,n(y))),y),z),z)).

given clause #123: (wt=17) 723 [hyper,1,367,462] P(n(n(i(n(i(n(i(n(n(x)),x)),y)),z)))).

given clause #124: (wt=17) 739 [hyper,1,44,618] P(i(n(i(x,n(y))),i(z,y))).

given clause #125: (wt=24) 58 [hyper,1,34,51] P(i(i(i(i(i(n(x),i(x,y)),z),z),u),u)).

given clause #126: (wt=17) 759 [hyper,1,367,465] P(n(n(i(i(n(n(i(n(n(x)),x))),y),y)))).

given clause #127: (wt=17) 814 [hyper,1,367,668] P(n(n(i(n(i(n(i(x,n(y))),y)),z)))).

given clause #128: (wt=17) 865 [hyper,1,142,848] P(i(n(i(n(i(n(i(x,y)),x)),z)),u)).

given clause #129: (wt=28) 59 [hyper,1,21,51] P(i(i(x,n(y)),i(x,i(y,z)))).

given clause #130: (wt=17) 868 [hyper,1,34,848] P(i(i(n(n(i(n(i(x,y)),x))),z),z)).

given clause #131: (wt=17) 919 [hyper,1,367,853] P(n(n(i(n(i(x,y)),i(z,x))))).

given clause #132: (wt=17) 928 [hyper,1,367,859] P(n(n(i(i(i(n(i(x,y)),x),z),z)))).

given clause #133: (wt=40) 60 [hyper,1,3,51] P(i(i(x,y),i(i(i(n(z),i(z,u)),x),y))).

given clause #134: (wt=17) 1057 [hyper,1,372,1010] P(n(n(i(n(i(n(i(n(n(x)),y)),x)),z)))).

given clause #135: (wt=17) 1065 [hyper,1,44,1010] P(i(n(i(n(n(x)),y)),i(z,x))).

given clause #136: (wt=17) 1071 [hyper,1,34,1010] P(i(i(i(n(i(n(n(x)),y)),x),z),z)).

given clause #137: (wt=37) 61 [hyper,1,2,51] P(i(x,i(i(i(n(y),i(y,z)),u),u))).

given clause #138: (wt=17) 1113 [hyper,1,372,1106] P(n(n(i(n(i(n(i(x,y)),n(y))),z)))).

given clause #139: (wt=17) 1126 [hyper,1,34,1106] P(i(i(i(n(i(x,y)),n(y)),z),z)).

given clause #140: (wt=18) 362 [hyper,1,241,337] P(i(i(x,n(n(y))),i(x,y))).

given clause #141: (wt=25) 63 [hyper,1,34,37] P(i(i(i(i(i(x,y),z),i(n(x),z)),u),u)).

given clause #142: (wt=17) 1452 [hyper,1,362,440] P(i(i(n(n(i(x,x))),n(n(y))),y)).

given clause #143: (wt=17) 1454 [hyper,1,362,366] P(i(i(i(n(n(x)),x),n(n(y))),y)).

given clause #144: (wt=18) 369 [hyper,1,3,337] P(i(i(x,y),i(n(n(x)),y))).

given clause #145: (wt=24) 64 [hyper,1,28,37] P(i(n(x),i(y,i(x,z)))).

given clause #146: (wt=15) 1547 [hyper,1,369,440] P(i(n(n(i(n(n(i(x,x))),y))),y)).

given clause #147: (wt=15) 1550 [hyper,1,369,366] P(i(n(n(i(i(n(n(x)),x),y))),y)).

given clause #148: (wt=17) 1541 [hyper,1,369,859] P(i(n(n(i(i(n(i(x,y)),x),z))),z)).

given clause #149: (wt=28) 65 [hyper,1,21,37] P(i(i(x,y),i(n(y),i(x,z)))).

given clause #150: (wt=17) 1546 [hyper,1,369,465] P(i(n(n(i(n(n(i(n(n(x)),x))),y))),y)).

given clause #151: (wt=17) 1549 [hyper,1,369,382] P(i(n(n(i(i(x,n(n(x))),y))),y)).

given clause #152: (wt=17) 1595 [hyper,1,367,1547] P(n(n(i(n(n(i(n(n(i(x,x))),y))),y)))).

given clause #153: (wt=30) 66 [hyper,1,3,37] P(i(i(i(n(x),y),z),i(i(i(x,u),y),z))).

given clause #154: (wt=17) 1616 [hyper,1,367,1550] P(n(n(i(n(n(i(i(n(n(x)),x),y))),y)))).

given clause #155: (wt=18) 396 [hyper,1,367,180] P(n(n(i(n(i(n(x),y)),i(x,z))))).

given clause #156: (wt=18) 414 [hyper,1,367,68] P(n(n(i(n(i(n(x),i(x,y))),z)))).

given clause #157: (wt=39) 67 [hyper,1,2,37] P(i(x,i(i(i(y,z),u),i(n(y),u)))).

given clause #158: (wt=18) 820 [hyper,1,367,380] P(n(n(i(n(x),n(n(i(x,y))))))).

given clause #159: (wt=18) 963 [hyper,1,367,390] P(n(n(i(i(n(n(x)),y),i(x,y))))).

given clause #160: (wt=18) 1548 [hyper,1,369,390] P(i(n(n(i(n(n(x)),y))),i(x,y))).

given clause #161: (wt=24) 69 [hyper,1,37,34] P(i(n(x),i(i(i(x,y),z),z))).

given clause #162: (wt=19) 328 [hyper,1,37,76] P(i(n(i(x,y)),i(n(n(y)),z))).

given clause #163: (wt=19) 340 [hyper,1,76,4] P(i(n(n(x)),i(i(x,y),y))).

given clause #164: (wt=19) 363 [hyper,1,146,337] P(i(n(i(x,i(n(n(y)),y))),z)).

given clause #165: (wt=30) 72 [hyper,1,37,21] P(i(n(i(i(x,y),i(z,y))),i(i(z,x),u))).

given clause #166: (wt=19) 365 [hyper,1,35,337] P(i(i(i(n(n(x)),x),y),i(z,y))).

given clause #167: (wt=19) 391 [hyper,1,2,367] P(i(x,i(y,n(n(y))))).

given clause #168: (wt=19) 404 [hyper,1,367,141] P(n(n(i(n(i(x,i(n(x),y))),z)))).

given clause #169: (wt=27) 77 [hyper,1,2,73] P(i(x,i(n(n(y)),i(z,y)))).

given clause #170: (wt=19) 406 [hyper,1,367,114] P(n(n(i(n(i(x,y)),i(n(y),x))))).

given clause #171: (wt=19) 407 [hyper,1,367,105] P(n(n(i(n(i(n(n(x)),i(y,x))),z)))).

given clause #172: (wt=19) 415 [hyper,1,367,62] P(n(n(i(n(i(x,y)),i(n(x),z))))).

given clause #173: (wt=21) 78 [hyper,1,34,70] P(i(i(i(n(i(x,i(y,x))),z),u),u)).

given clause #174: (wt=19) 421 [hyper,1,367,34] P(n(n(i(x,i(i(x,y),y))))).

given clause #175: (wt=19) 426 [hyper,1,367,28] P(n(n(i(i(i(x,i(y,x)),z),z)))).

given clause #176: (wt=19) 431 [hyper,1,367,23] P(n(n(i(i(i(x,y),z),i(y,z))))).

given clause #177: (wt=34) 79 [hyper,1,3,70] P(i(i(x,y),i(n(i(z,i(u,z))),y))).

given clause #178: (wt=19) 435 [hyper,1,367,5] P(n(n(i(i(n(x),n(y)),i(y,x))))).

given clause #179: (wt=19) 438 [hyper,1,146,418] P(i(n(i(x,n(n(i(y,y))))),z)).

given clause #180: (wt=19) 439 [hyper,1,35,418] P(i(i(n(n(i(x,x))),y),i(z,y))).

given clause #181: (wt=31) 80 [hyper,1,2,70] P(i(x,i(n(i(y,i(z,y))),u))).

given clause #182: (wt=19) 466 [hyper,1,2,392] P(i(x,n(n(i(n(n(y)),y))))).

given clause #183: (wt=19) 488 [hyper,1,34,366] P(i(i(i(i(i(n(n(x)),x),y),y),z),z)).

given clause #184: (wt=19) 491 [hyper,1,24,366] P(i(i(i(x,n(n(x))),n(n(x))),x)).

given clause #185: (wt=30) 81 [hyper,1,37,24] P(i(n(i(i(x,y),y)),i(i(i(y,x),x),z))).

given clause #186: (wt=19) 499 [hyper,1,34,375] P(i(i(i(n(i(x,n(n(x)))),y),z),z)).

given clause #187: (wt=19) 505 [hyper,1,34,385] P(i(i(n(n(i(x,i(y,x)))),z),z)).

given clause #188: (wt=19) 534 [hyper,1,34,440] P(i(i(i(i(n(n(i(x,x))),y),y),z),z)).

given clause #189: (wt=38) 82 [hyper,1,34,24] P(i(i(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z)),u),u)).

given clause #190: (wt=19) 539 [hyper,1,142,467] P(i(n(i(n(i(n(i(n(n(x)),x)),y)),z)),u)).

given clause #191: (wt=19) 542 [hyper,1,34,467] P(i(i(n(n(i(n(i(n(n(x)),x)),y))),z),z)).

given clause #192: (wt=19) 582 [hyper,1,116,382] P(i(n(i(i(i(x,n(n(x))),y),y)),z)).

given clause #193: (wt=41) 83 [hyper,1,28,24] P(i(i(i(x,y),y),i(z,i(i(y,x),x)))).

given clause #194: (wt=19) 601 [hyper,1,138,388] P(i(x,i(y,n(n(x))))).

given clause #195: (wt=19) 602 [hyper,1,116,388] P(i(n(i(x,n(n(i(y,x))))),z)).

given clause #196: (wt=19) 619 [hyper,1,3,388] P(i(i(n(n(i(x,y))),z),i(y,z))).

given clause #197: (wt=41) 84 [hyper,1,24,24] P(i(i(i(x,i(y,x)),i(y,x)),i(i(i(x,y),y),x))).

given clause #198: (wt=19) 712 [hyper,1,142,665] P(i(n(i(n(i(n(i(x,n(y))),y)),z)),u)).

given clause #199: (wt=19) 715 [hyper,1,34,665] P(i(i(n(n(i(n(i(x,n(y))),y))),z),z)).

given clause #200: (wt=19) 762 [hyper,1,116,465] P(i(n(i(i(n(n(i(n(n(x)),x))),y),y)),z)).

given clause #201: (wt=44) 85 [hyper,1,21,24] P(i(i(x,i(y,z)),i(i(i(z,y),y),i(x,z)))).

given clause #202: (wt=19) 834 [hyper,1,380,527] P(n(n(i(n(i(i(n(n(i(x,x))),y),y)),z)))).

given clause #203: (wt=19) 835 [hyper,1,380,494] P(n(n(i(n(i(n(i(x,n(n(x)))),y)),z)))).

given clause #204: (wt=19) 836 [hyper,1,380,482] P(n(n(i(n(i(i(i(n(n(x)),x),y),y)),z)))).

given clause #205: (wt=41) 86 [hyper,1,3,24] P(i(i(i(i(i(x,y),y),z),u),i(i(i(i(y,x),x),z),u))).

given clause #206: (wt=19) 861 [hyper,1,2,831] P(i(x,i(n(i(y,z)),y))).

given clause #207: (wt=19) 872 [hyper,1,34,851] P(i(i(i(n(i(n(i(x,y)),x)),z),u),u)).

given clause #208: (wt=19) 921 [hyper,1,116,853] P(i(n(i(n(i(x,y)),i(z,x))),u)).

given clause #209: (wt=65) 87 [hyper,1,2,24] P(i(x,i(i(i(i(y,z),z),u),i(i(i(z,y),y),u)))).

given clause #210: (wt=19) 930 [hyper,1,116,859] P(i(n(i(i(i(n(i(x,y)),x),z),z)),u)).

given clause #211: (wt=19) 937 [hyper,1,380,863] P(n(n(i(n(i(n(i(n(i(x,y)),x)),z)),u)))).

given clause #212: (wt=19) 986 [hyper,1,367,372] P(n(n(i(x,n(n(i(n(x),y))))))).

given clause #213: (wt=24) 88 [hyper,1,24,51] P(i(i(i(i(x,y),n(x)),n(x)),i(x,y))).

given clause #214: (wt=19) 1079 [hyper,1,142,1058] P(i(n(i(n(i(n(i(n(n(x)),y)),x)),z)),u)).

given clause #215: (wt=19) 1083 [hyper,1,34,1058] P(i(i(n(n(i(n(i(n(n(x)),y)),x))),z),z)).

given clause #216: (wt=19) 1093 [hyper,1,367,376] P(n(n(i(n(n(x)),n(n(i(y,x))))))).

given clause #217: (wt=35) 90 [hyper,1,24,34] P(i(i(i(x,y),y),i(i(i(i(y,x),x),z),z))).

given clause #218: (wt=19) 1121 [hyper,1,44,1106] P(i(n(i(x,y)),i(z,n(y)))).

given clause #219: (wt=19) 1131 [hyper,1,142,1114] P(i(n(i(n(i(n(i(x,y)),n(y))),z)),u)).

given clause #220: (wt=19) 1135 [hyper,1,34,1114] P(i(i(n(n(i(n(i(x,y)),n(y)))),z),z)).

given clause #221: (wt=50) 91 [hyper,1,24,21] P(i(i(i(i(x,y),i(z,y)),i(z,y)),i(i(x,z),i(x,y)))).

given clause #222: (wt=19) 1153 [hyper,1,367,472] P(n(n(i(i(i(n(i(n(n(x)),x)),y),z),z)))).

given clause #223: (wt=19) 1171 [hyper,1,367,479] P(n(n(i(i(n(n(i(x,n(n(x))))),y),y)))).

given clause #224: (wt=19) 1235 [hyper,1,367,590] P(n(n(i(i(i(n(n(x)),x),x),n(n(x)))))).

given clause #225: (wt=47) 92 [hyper,1,24,3] P(i(i(i(x,y),y),i(i(x,z),i(i(y,x),z)))).

given clause #226: (wt=19) 1272 [hyper,1,367,673] P(n(n(i(i(i(n(i(x,n(y))),y),z),z)))).

given clause #227: (wt=19) 1285 [hyper,1,367,739] P(n(n(i(n(i(x,n(y))),i(z,y))))).

given clause #228: (wt=19) 1307 [hyper,1,673,59] P(i(n(i(x,n(n(y)))),i(y,z))).

given clause #229: (wt=21) 93 [hyper,1,34,71] P(i(i(i(n(i(x,y)),i(y,z)),u),u)).

given clause #230: (wt=19) 1338 [hyper,1,367,868] P(n(n(i(i(n(n(i(n(i(x,y)),x))),z),z)))).

given clause #231: (wt=19) 1390 [hyper,1,367,1065] P(n(n(i(n(i(n(n(x)),y)),i(z,x))))).

given clause #232: (wt=19) 1400 [hyper,1,367,1071] P(n(n(i(i(i(n(i(n(n(x)),y)),x),z),z)))).

given clause #233: (wt=25) 94 [hyper,1,3,71] P(i(i(i(x,y),z),i(n(i(u,x)),z))).

given clause #234: (wt=19) 1414 [hyper,1,367,1126] P(n(n(i(i(i(n(i(x,y)),n(y)),z),z)))).

given clause #235: (wt=19) 1447 [hyper,1,362,859] P(i(i(i(n(i(x,y)),x),n(n(z))),z)).

given clause #236: (wt=19) 1451 [hyper,1,362,465] P(i(i(n(n(i(n(n(x)),x))),n(n(y))),y)).

given clause #237: (wt=31) 95 [hyper,1,2,71] P(i(x,i(n(i(y,z)),i(z,u)))).

given clause #238: (wt=19) 1453 [hyper,1,362,382] P(i(i(i(x,n(n(x))),n(n(y))),y)).

given clause #239: (wt=19) 1471 [hyper,1,367,1452] P(n(n(i(i(n(n(i(x,x))),n(n(y))),y)))).

given clause #240: (wt=19) 1491 [hyper,1,367,1454] P(n(n(i(i(i(n(n(x)),x),n(n(y))),y)))).

given clause #241: (wt=22) 96 [hyper,1,34,68] P(i(i(i(n(i(n(x),i(x,y))),z),u),u)).

given clause #242: (wt=19) 1521 [hyper,1,55,369] P(i(n(n(i(n(x),n(y)))),i(y,x))).

given clause #243: (wt=19) 1522 [hyper,1,53,369] P(i(n(n(i(i(x,y),z))),i(y,z))).

given clause #244: (wt=19) 1523 [hyper,1,52,369] P(i(n(n(i(i(x,i(y,x)),z))),z)).

given clause #245: (wt=36) 97 [hyper,1,3,68] P(i(i(x,y),i(n(i(n(z),i(z,u))),y))).

given clause #246: (wt=19) 1536 [hyper,1,369,1454] P(i(n(n(i(i(n(n(x)),x),n(n(y))))),y)).

given clause #247: (wt=19) 1537 [hyper,1,369,1452] P(i(n(n(i(n(n(i(x,x))),n(n(y))))),y)).

given clause #248: (wt=19) 1538 [hyper,1,369,1126] P(i(n(n(i(i(n(i(x,y)),n(y)),z))),z)).

given clause #249: (wt=33) 98 [hyper,1,2,68] P(i(x,i(n(i(n(y),i(y,z))),u))).

given clause #250: (wt=19) 1539 [hyper,1,369,1071] P(i(n(n(i(i(n(i(n(n(x)),y)),x),z))),z)).

given clause #251: (wt=19) 1540 [hyper,1,369,868] P(i(n(n(i(n(n(i(n(i(x,y)),x))),z))),z)).

given clause #252: (wt=19) 1542 [hyper,1,369,673] P(i(n(n(i(i(n(i(x,n(y))),y),z))),z)).

given clause #253: (wt=23) 99 [hyper,1,34,62] P(i(i(i(n(i(x,y)),i(n(x),z)),u),u)).

given clause #254: (wt=19) 1543 [hyper,1,369,590] P(i(n(n(i(i(n(n(x)),x),x))),n(n(x)))).

given clause #255: (wt=19) 1544 [hyper,1,369,479] P(i(n(n(i(n(n(i(x,n(n(x))))),y))),y)).

given clause #256: (wt=19) 1545 [hyper,1,369,472] P(i(n(n(i(i(n(i(n(n(x)),x)),y),z))),z)).

given clause #257: (wt=26) 100 [hyper,1,3,62] P(i(i(i(n(x),y),z),i(n(i(x,u)),z))).

given clause #258: (wt=19) 1598 [hyper,1,116,1547] P(i(n(i(n(n(i(n(n(i(x,x))),y))),y)),z)).

given clause #259: (wt=19) 1619 [hyper,1,116,1550] P(i(n(i(n(n(i(i(n(n(x)),x),y))),y)),z)).

given clause #260: (wt=19) 1637 [hyper,1,367,1541] P(n(n(i(n(n(i(i(n(i(x,y)),x),z))),z)))).

given clause #261: (wt=35) 101 [hyper,1,2,62] P(i(x,i(n(i(y,z)),i(n(y),u)))).

given clause #262: (wt=19) 1690 [hyper,1,65,146] P(i(n(i(n(i(x,y)),z)),i(y,u))).

given clause #263: (wt=19) 1713 [hyper,1,367,1546] P(n(n(i(n(n(i(n(n(i(n(n(x)),x))),y))),y)))).

given clause #264: (wt=19) 1736 [hyper,1,367,1549] P(n(n(i(n(n(i(i(x,n(n(x))),y))),y)))).

given clause #265: (wt=53) 102 [hyper,1,34,25] P(i(i(i(x,i(i(i(y,z),z),i(i(z,y),y))),u),u)).

given clause #266: (wt=19) 1771 [hyper,1,55,66] P(i(i(i(x,y),n(z)),i(z,x))).

given clause #267: (wt=13) 2930 [hyper,1,1771,372] P(i(n(i(n(i(x,y)),z)),x)).

given clause #268: (wt=15) 2929 [hyper,1,1771,388] P(i(n(i(x,i(y,z))),y)).

given clause #269: (wt=35) 103 [hyper,1,3,25] P(i(i(i(i(i(x,y),y),i(i(y,x),x)),z),i(u,z))).

given clause #270: (wt=15) 2934 [hyper,1,367,2930] P(n(n(i(n(i(n(i(x,y)),z)),x)))).

given clause #271: (wt=15) 2935 [hyper,1,362,2930] P(i(n(i(n(i(n(n(x)),y)),z)),x)).

given clause #272: (wt=17) 2937 [hyper,1,116,2930] P(i(n(i(n(i(n(i(x,y)),z)),x)),u)).

given clause #273: (wt=95) 104 [hyper,1,2,25] P(i(x,i(y,i(i(i(z,u),u),i(i(u,z),z))))).

given clause #274: (wt=17) 2948 [hyper,1,367,2929] P(n(n(i(n(i(x,i(y,z))),y)))).

given clause #275: (wt=17) 2973 [hyper,1,367,2935] P(n(n(i(n(i(n(i(n(n(x)),y)),z)),x)))).

given clause #276: (wt=19) 2540 [hyper,1,382,94] P(i(n(i(x,y)),n(n(i(y,z))))).

given clause #277: (wt=25) 106 [hyper,1,34,75] P(i(i(i(i(i(n(n(x)),i(y,x)),z),z),u),u)).

given clause #278: (wt=19) 2933 [hyper,1,372,2930] P(n(n(i(n(i(n(i(n(i(x,y)),z)),x)),u)))).

given clause #279: (wt=19) 2941 [hyper,1,44,2930] P(i(n(i(n(i(x,y)),z)),i(u,x))).

given clause #280: (wt=19) 2942 [hyper,1,34,2930] P(i(i(i(n(i(n(i(x,y)),z)),x),u),u)).

given clause #281: (wt=28) 107 [hyper,1,24,75] P(i(i(i(i(x,y),n(n(y))),n(n(y))),i(x,y))).

given clause #282: (wt=19) 2949 [hyper,1,362,2929] P(i(n(i(x,i(n(n(y)),z))),y)).

given clause #283: (wt=19) 2951 [hyper,1,116,2929] P(i(n(i(n(i(x,i(y,z))),y)),u)).

given clause #284: (wt=19) 2975 [hyper,1,116,2935] P(i(n(i(n(i(n(i(n(n(x)),y)),z)),x)),u)).

given clause #285: (wt=30) 108 [hyper,1,21,75] P(i(i(x,n(n(y))),i(x,i(z,y)))).

given clause #286: (wt=20) 394 [hyper,1,367,229] P(n(n(i(n(i(i(x,y),y)),i(x,z))))).

given clause #287: (wt=20) 400 [hyper,1,367,148] P(n(n(i(i(i(n(x),y),z),i(x,z))))).

given clause #288: (wt=20) 416 [hyper,1,367,51] P(n(n(i(i(i(n(x),i(x,y)),z),z)))).

given clause #289: (wt=42) 109 [hyper,1,3,75] P(i(i(x,y),i(i(i(n(n(z)),i(u,z)),x),y))).

given clause #290: (wt=20) 547 [hyper,1,34,378] P(i(i(n(n(i(n(x),i(x,y)))),z),z)).

given clause #291: (wt=20) 823 [hyper,1,116,380] P(i(n(i(n(x),n(n(i(x,y))))),z)).

given clause #292: (wt=20) 966 [hyper,1,116,390] P(i(n(i(i(n(n(x)),y),i(x,y))),z)).

given clause #293: (wt=39) 110 [hyper,1,2,75] P(i(x,i(i(i(n(n(y)),i(z,y)),u),u))).

given clause #294: (wt=20) 1011 [hyper,1,3,372] P(i(i(n(n(i(n(x),y))),z),i(x,z))).

given clause #295: (wt=20) 1425 [hyper,1,367,362] P(n(n(i(i(x,n(n(y))),i(x,y))))).

given clause #296: (wt=20) 1511 [hyper,1,369,369] P(i(n(n(i(x,y))),i(n(n(x)),y))).

given clause #297: (wt=23) 111 [hyper,1,34,105] P(i(i(i(n(i(n(n(x)),i(y,x))),z),u),u)).

given clause #298: (wt=20) 1512 [hyper,1,367,369] P(n(n(i(i(x,y),i(n(n(x)),y))))).

given clause #299: (wt=20) 1518 [hyper,1,58,369] P(i(n(n(i(i(n(x),i(x,y)),z))),z)).

given clause #300: (wt=20) 1551 [hyper,1,369,362] P(i(n(n(i(x,n(n(y))))),i(x,y))).

given clause #301: (wt=38) 112 [hyper,1,3,105] P(i(i(x,y),i(n(i(n(n(z)),i(u,z))),y))).

given clause #302: (wt=20) 1553 [hyper,1,369,148] P(i(n(n(i(i(n(x),y),z))),i(x,z))).

given clause #303: (wt=20) 1818 [hyper,1,367,1548] P(n(n(i(n(n(i(n(n(x)),y))),i(x,y))))).

given clause #304: (wt=20) 2940 [hyper,1,59,2930] P(i(n(i(n(i(n(x),y)),z)),i(x,u))).

given clause #305: (wt=35) 113 [hyper,1,2,105] P(i(x,i(n(i(n(n(y)),i(z,y))),u))).

given clause #306: (wt=21) 150 [hyper,1,116,105] P(i(n(i(n(i(n(n(x)),i(y,x))),z)),u)).

given clause #307: (wt=21) 156 [hyper,1,116,62] P(i(n(i(n(i(x,y)),i(n(x),z))),u)).

given clause #308: (wt=21) 159 [hyper,1,116,34] P(i(n(i(x,i(i(x,y),y))),z)).

given clause #309: (wt=25) 115 [hyper,1,34,89] P(i(i(i(i(i(x,y),y),i(n(y),x)),z),z)).

given clause #310: (wt=21) 160 [hyper,1,116,28] P(i(n(i(i(i(x,i(y,x)),z),z)),u)).

given clause #311: (wt=21) 164 [hyper,1,116,23] P(i(n(i(i(i(x,y),z),i(y,z))),u)).

given clause #312: (wt=21) 166 [hyper,1,116,5] P(i(n(i(i(n(x),n(y)),i(y,x))),z)).

given clause #313: (wt=30) 117 [hyper,1,3,89] P(i(i(i(n(x),y),z),i(i(i(y,x),x),z))).

given clause #314: (wt=21) 167 [hyper,1,116,114] P(i(n(i(n(i(x,y)),i(n(y),x))),z)).

given clause #315: (wt=21) 171 [hyper,1,116,141] P(i(n(i(n(i(x,i(n(x),y))),z)),u)).

given clause #316: (wt=21) 184 [hyper,1,24,148] P(i(i(i(x,n(y)),n(y)),i(y,x))).

given clause #317: (wt=39) 118 [hyper,1,2,89] P(i(x,i(i(i(y,z),z),i(n(z),y)))).

given clause #318: (wt=21) 188 [hyper,1,148,116] P(i(x,i(n(i(n(x),y)),z))).

given clause #319: (wt=21) 222 [hyper,1,3,146] P(i(i(i(n(i(x,y)),z),u),i(y,u))).

given clause #320: (wt=21) 303 [hyper,1,31,5] P(i(i(i(x,n(y)),n(z)),i(z,y))).

given clause #321: (wt=27) 119 [hyper,1,89,25] P(i(n(i(i(i(x,y),y),i(i(y,x),x))),z)).

given clause #322: (wt=15) 3444 [hyper,1,303,372] P(i(n(i(n(i(x,n(y))),z)),y)).

given clause #323: (wt=17) 3452 [hyper,1,367,3444] P(n(n(i(n(i(n(i(x,n(y))),z)),y)))).

given clause #324: (wt=19) 3443 [hyper,1,303,388] P(i(n(i(x,i(y,n(z)))),z)).

given clause #325: (wt=36) 120 [hyper,1,89,22] P(i(n(i(i(x,y),i(i(y,z),i(x,z)))),u)).

given clause #326: (wt=19) 3454 [hyper,1,116,3444] P(i(n(i(n(i(n(i(x,n(y))),z)),y)),u)).

given clause #327: (wt=21) 325 [hyper,1,143,76] P(i(n(n(x)),i(n(i(y,x)),z))).

given clause #328: (wt=21) 379 [hyper,1,49,367] P(i(x,n(n(i(i(x,y),y))))).

given clause #329: (wt=27) 121 [hyper,1,37,26] P(i(n(i(x,y)),i(i(n(y),n(x)),z))).

given clause #330: (wt=13) 3527 [hyper,1,5,379] P(i(n(i(i(n(x),y),y)),x)).

given clause #331: (wt=15) 3487 [hyper,1,1771,379] P(i(n(i(i(i(x,y),z),z)),x)).

given clause #332: (wt=15) 3747 [hyper,1,367,3527] P(n(n(i(n(i(i(n(x),y),y)),x)))).

given clause #333: (wt=35) 122 [hyper,1,34,26] P(i(i(i(i(i(x,y),z),i(i(n(y),n(x)),z)),u),u)).

given clause #334: (wt=17) 3497 [hyper,1,303,379] P(i(n(i(i(i(x,n(y)),z),z)),y)).

given clause #335: (wt=17) 3751 [hyper,1,116,3527] P(i(n(i(n(i(i(n(x),y),y)),x)),z)).

given clause #336: (wt=17) 3772 [hyper,1,367,3487] P(n(n(i(n(i(i(i(x,y),z),z)),x)))).

given clause #337: (wt=29) 123 [hyper,1,28,26] P(i(i(n(x),n(y)),i(z,i(y,x)))).

given clause #338: (wt=17) 3773 [hyper,1,362,3487] P(i(n(i(i(i(n(n(x)),y),z),z)),x)).

given clause #339: (wt=19) 3746 [hyper,1,372,3527] P(n(n(i(n(i(n(i(i(n(x),y),y)),x)),z)))).

given clause #340: (wt=19) 3759 [hyper,1,44,3527] P(i(n(i(i(n(x),y),y)),i(z,x))).

given clause #341: (wt=35) 124 [hyper,1,26,26] P(i(i(n(x),n(i(y,z))),i(i(n(z),n(y)),x))).

given clause #342: (wt=19) 3765 [hyper,1,34,3527] P(i(i(i(n(i(i(n(x),y),y)),x),z),z)).

given clause #343: (wt=19) 3775 [hyper,1,116,3487] P(i(n(i(n(i(i(i(x,y),z),z)),x)),u)).

given clause #344: (wt=19) 3800 [hyper,1,367,3497] P(n(n(i(n(i(i(i(x,n(y)),z),z)),y)))).

given clause #345: (wt=29) 125 [hyper,1,24,26] P(i(i(i(x,y),y),i(i(n(x),n(y)),x))).

given clause #346: (wt=19) 3849 [hyper,1,367,3773] P(n(n(i(n(i(i(i(n(n(x)),y),z),z)),x)))).

given clause #347: (wt=20) 3755 [hyper,1,59,3527] P(i(n(i(i(n(n(x)),y),y)),i(x,z))).

given clause #348: (wt=21) 381 [hyper,1,35,367] P(i(i(i(x,n(n(x))),y),i(z,y))).

given clause #349: (wt=38) 126 [hyper,1,21,26] P(i(i(x,y),i(i(n(z),n(y)),i(x,z)))).

given clause #350: (wt=21) 383 [hyper,1,31,367] P(i(i(i(x,y),z),n(n(i(y,z))))).

given clause #351: (wt=21) 386 [hyper,1,26,367] P(i(i(n(x),n(y)),n(n(i(y,x))))).

given clause #352: (wt=19) 4202 [hyper,1,100,386] P(i(n(i(x,y)),n(n(i(z,x))))).

given clause #353: (wt=35) 127 [hyper,1,3,26] P(i(i(i(i(n(x),n(y)),z),u),i(i(i(y,x),z),u))).

given clause #354: (wt=21) 398 [hyper,1,367,154] P(n(n(i(n(i(n(i(x,i(y,x))),z)),u)))).

given clause #355: (wt=21) 399 [hyper,1,367,153] P(n(n(i(n(i(n(i(x,y)),i(y,z))),u)))).

given clause #356: (wt=21) 401 [hyper,1,367,146] P(n(n(i(x,i(n(i(y,x)),z))))).

given clause #357: (wt=59) 128 [hyper,1,2,26] P(i(x,i(i(i(y,z),u),i(i(n(z),n(y)),u)))).

given clause #358: (wt=21) 402 [hyper,1,367,143] P(n(n(i(i(i(x,i(n(x),y)),z),z)))).

given clause #359: (wt=21) 408 [hyper,1,367,89] P(n(n(i(i(i(x,y),y),i(n(y),x))))).

given clause #360: (wt=21) 410 [hyper,1,367,75] P(n(n(i(i(i(n(n(x)),i(y,x)),z),z)))).

given clause #361: (wt=25) 129 [hyper,1,26,89] P(i(i(n(x),n(i(y,x))),i(n(x),y))).

given clause #362: (wt=21) 419 [hyper,1,367,37] P(n(n(i(i(i(x,y),z),i(n(x),z))))).

given clause #363: (wt=21) 464 [hyper,1,35,392] P(i(i(n(n(i(n(n(x)),x))),y),i(z,y))).

given clause #364: (wt=21) 489 [hyper,1,31,366] P(i(i(i(x,i(n(n(y)),y)),z),z)).

given clause #365: (wt=33) 130 [hyper,1,26,75] P(i(i(n(x),n(i(n(n(y)),i(z,y)))),x)).

given clause #366: (wt=21) 490 [hyper,1,26,366] P(i(i(n(x),n(i(n(n(y)),y))),x)).

given clause #367: (wt=21) 507 [hyper,1,366,40] P(i(i(i(x,i(y,x)),n(n(z))),z)).

given clause #368: (wt=21) 517 [hyper,1,40,367] P(i(i(i(x,i(y,x)),z),n(n(z)))).

given clause #369: (wt=31) 131 [hyper,1,26,51] P(i(i(n(x),n(i(n(y),i(y,z)))),x)).

given clause #370: (wt=21) 535 [hyper,1,31,440] P(i(i(i(x,n(n(i(y,y)))),z),z)).

given clause #371: (wt=21) 557 [hyper,1,34,374] P(i(i(n(n(i(x,i(n(x),y)))),z),z)).

given clause #372: (wt=21) 562 [hyper,1,34,377] P(i(i(n(n(i(n(n(x)),i(y,x)))),z),z)).

given clause #373: (wt=25) 132 [hyper,1,26,37] P(i(i(n(x),n(i(y,z))),i(n(y),x))).

given clause #374: (wt=21) 587 [hyper,1,34,382] P(i(i(i(i(i(x,n(n(x))),y),y),z),z)).

given clause #375: (wt=21) 595 [hyper,1,382,388] P(n(n(i(x,i(y,n(n(y))))))).

given clause #376: (wt=21) 611 [hyper,1,34,388] P(i(i(i(x,n(n(i(y,x)))),z),z)).

given clause #377: (wt=29) 133 [hyper,1,26,34] P(i(i(n(x),n(y)),i(i(i(y,x),z),z))).

given clause #378: (wt=21) 623 [hyper,1,388,392] P(n(n(i(x,n(n(i(n(n(y)),y))))))).

given clause #379: (wt=21) 725 [hyper,1,34,462] P(i(i(i(n(i(n(i(n(n(x)),x)),y)),z),u),u)).

given clause #380: (wt=21) 768 [hyper,1,34,465] P(i(i(i(i(n(n(i(n(n(x)),x))),y),y),z),z)).

given clause #381: (wt=29) 134 [hyper,1,26,28] P(i(i(n(x),n(i(y,i(z,y)))),x)).

given clause #382: (wt=21) 774 [hyper,1,142,482] P(i(n(i(n(i(i(i(n(n(x)),x),y),y)),z)),u)).

given clause #383: (wt=21) 777 [hyper,1,34,482] P(i(i(n(n(i(i(i(n(n(x)),x),y),y))),z),z)).

given clause #384: (wt=21) 781 [hyper,1,142,494] P(i(n(i(n(i(n(i(x,n(n(x)))),y)),z)),u)).

given clause #385: (wt=41) 135 [hyper,1,26,24] P(i(i(n(x),n(i(i(y,z),z))),i(i(i(z,y),y),x))).

given clause #386: (wt=21) 784 [hyper,1,34,494] P(i(i(n(n(i(n(i(x,n(n(x)))),y))),z),z)).

given clause #387: (wt=21) 808 [hyper,1,142,527] P(i(n(i(n(i(i(n(n(i(x,x))),y),y)),z)),u)).

given clause #388: (wt=21) 811 [hyper,1,34,527] P(i(i(n(n(i(i(n(n(i(x,x))),y),y))),z),z)).

given clause #389: (wt=23) 136 [hyper,1,26,23] P(i(i(n(x),n(i(y,z))),i(z,x))).

given clause #390: (wt=21) 816 [hyper,1,34,668] P(i(i(i(n(i(n(i(x,n(y))),y)),z),u),u)).

given clause #391: (wt=21) 832 [hyper,1,3,380] P(i(i(n(n(i(x,y))),z),i(n(x),z))).

given clause #392: (wt=21) 847 [hyper,1,388,831] P(n(n(i(x,i(n(i(y,z)),y))))).

given clause #393: (wt=47) 137 [hyper,1,26,21] P(i(i(n(x),n(i(i(y,z),i(u,z)))),i(i(u,y),x))).

given clause #394: (wt=21) 858 [hyper,1,35,831] P(i(i(i(n(i(x,y)),x),z),i(u,z))).

given clause #395: (wt=21) 924 [hyper,1,34,853] P(i(i(i(n(i(x,y)),i(z,x)),u),u)).

given clause #396: (wt=21) 931 [hyper,1,34,859] P(i(i(i(i(i(n(i(x,y)),x),z),z),u),u)).

given clause #397: (wt=29) 139 [hyper,1,26,4] P(i(i(n(x),n(i(y,x))),i(i(x,y),y))).

given clause #398: (wt=21) 938 [hyper,1,34,863] P(i(i(n(n(i(n(i(n(i(x,y)),x)),z))),u),u)).

given clause #399: (wt=21) 969 [hyper,1,46,390] P(i(x,i(i(n(n(x)),y),y))).

given clause #400: (wt=21) 977 [hyper,1,31,390] P(i(i(i(x,n(n(y))),z),i(y,z))).

given clause #401: (wt=35) 140 [hyper,1,26,3] P(i(i(n(x),n(y)),i(i(x,z),i(y,z)))).

given clause #402: (wt=21) 990 [hyper,1,116,372] P(i(n(i(x,n(n(i(n(x),y))))),z)).

given clause #403: (wt=21) 1013 [hyper,1,372,859] P(n(n(i(n(i(i(i(n(i(x,y)),x),z),z)),u)))).

given clause #404: (wt=21) 1014 [hyper,1,372,853] P(n(n(i(n(i(n(i(x,y)),i(z,x))),u)))).

given clause #405: (wt=25) 144 [hyper,1,26,116] P(i(i(n(x),n(y)),i(n(i(y,x)),z))).

given clause #406: (wt=21) 1015 [hyper,1,372,668] P(n(n(i(n(i(n(i(n(i(x,n(y))),y)),z)),u)))).

given clause #407: (wt=21) 1016 [hyper,1,372,465] P(n(n(i(n(i(i(n(n(i(n(n(x)),x))),y),y)),z)))).

given clause #408: (wt=21) 1017 [hyper,1,372,462] P(n(n(i(n(i(n(i(n(i(n(n(x)),x)),y)),z)),u)))).

given clause #409: (wt=31) 145 [hyper,1,24,116] P(i(i(i(x,y),y),i(n(i(i(y,x),x)),z))).

given clause #410: (wt=21) 1018 [hyper,1,372,441] P(n(n(i(n(i(x,n(n(i(y,y))))),z)))).

given clause #411: (wt=21) 1020 [hyper,1,372,388] P(n(n(i(n(i(x,n(n(i(y,x))))),z)))).

given clause #412: (wt=21) 1021 [hyper,1,372,382] P(n(n(i(n(i(i(i(x,n(n(x))),y),y)),z)))).

given clause #413: (wt=40) 147 [hyper,1,21,116] P(i(i(x,y),i(n(i(i(y,z),i(x,z))),u))).

given clause #414: (wt=21) 1023 [hyper,1,372,327] P(n(n(i(n(i(x,i(n(n(y)),y))),z)))).

given clause #415: (wt=21) 1086 [hyper,1,372,1061] P(n(n(i(n(i(n(i(n(i(n(n(x)),y)),x)),z)),u)))).

given clause #416: (wt=21) 1088 [hyper,1,34,1061] P(i(i(i(n(i(n(i(n(n(x)),y)),x)),z),u),u)).

given clause #417: (wt=27) 149 [hyper,1,2,116] P(i(x,i(y,i(n(y),z)))).

given clause #418: (wt=21) 1096 [hyper,1,116,376] P(i(n(i(n(n(x)),n(n(i(y,x))))),z)).

given clause #419: (wt=21) 1138 [hyper,1,372,1117] P(n(n(i(n(i(n(i(n(i(x,y)),n(y))),z)),u)))).

given clause #420: (wt=21) 1140 [hyper,1,34,1117] P(i(i(i(n(i(n(i(x,y)),n(y))),z),u),u)).

given clause #421: (wt=23) 151 [hyper,1,116,89] P(i(n(i(i(i(x,y),y),i(n(y),x))),z)).

given clause #422: (wt=21) 1155 [hyper,1,116,472] P(i(n(i(i(i(n(i(n(n(x)),x)),y),z),z)),u)).

given clause #423: (wt=21) 1174 [hyper,1,116,479] P(i(n(i(i(n(n(i(x,n(n(x))))),y),y)),z)).

given clause #424: (wt=21) 1238 [hyper,1,116,590] P(i(n(i(i(i(n(n(x)),x),x),n(n(x)))),y)).

given clause #425: (wt=23) 152 [hyper,1,116,75] P(i(n(i(i(i(n(n(x)),i(y,x)),z),z)),u)).

given clause #426: (wt=21) 1274 [hyper,1,116,673] P(i(n(i(i(i(n(i(x,n(y))),y),z),z)),u)).

given clause #427: (wt=21) 1287 [hyper,1,116,739] P(i(n(i(n(i(x,n(y))),i(z,y))),u)).

given clause #428: (wt=21) 1324 [hyper,1,59,590] P(i(i(i(n(n(x)),x),x),i(n(x),y))).

given clause #429: (wt=22) 157 [hyper,1,116,51] P(i(n(i(i(i(n(x),i(x,y)),z),z)),u)).

given clause #430: (wt=21) 1328 [hyper,1,59,440] P(i(i(n(n(i(x,x))),n(y)),i(y,z))).

given clause #431: (wt=21) 1330 [hyper,1,59,366] P(i(i(i(n(n(x)),x),n(y)),i(y,z))).

given clause #432: (wt=21) 1340 [hyper,1,116,868] P(i(n(i(i(n(n(i(n(i(x,y)),x))),z),z)),u)).

given clause #433: (wt=23) 158 [hyper,1,116,37] P(i(n(i(i(i(x,y),z),i(n(x),z))),u)).

given clause #434: (wt=21) 1392 [hyper,1,116,1065] P(i(n(i(n(i(n(n(x)),y)),i(z,x))),u)).

given clause #435: (wt=21) 1402 [hyper,1,116,1071] P(i(n(i(i(i(n(i(n(n(x)),y)),x),z),z)),u)).

given clause #436: (wt=21) 1416 [hyper,1,116,1126] P(i(n(i(i(i(n(i(x,y)),n(y)),z),z)),u)).

given clause #437: (wt=33) 161 [hyper,1,116,26] P(i(n(i(i(i(x,y),z),i(i(n(y),n(x)),z))),u)).

given clause #438: (wt=21) 1440 [hyper,1,31,362] P(i(i(i(x,y),n(n(z))),i(y,z))).

given clause #439: (wt=21) 1444 [hyper,1,362,1126] P(i(i(i(n(i(x,y)),n(y)),n(n(z))),z)).

given clause #440: (wt=21) 1445 [hyper,1,362,1071] P(i(i(i(n(i(n(n(x)),y)),x),n(n(z))),z)).

given clause #441: (wt=51) 162 [hyper,1,116,25] P(i(n(i(x,i(i(i(y,z),z),i(i(z,y),y)))),u)).

given clause #442: (wt=21) 1446 [hyper,1,362,868] P(i(i(n(n(i(n(i(x,y)),x))),n(n(z))),z)).

given clause #443: (wt=21) 1448 [hyper,1,362,673] P(i(i(i(n(i(x,n(y))),y),n(n(z))),z)).

given clause #444: (wt=21) 1449 [hyper,1,362,479] P(i(i(n(n(i(x,n(n(x))))),n(n(y))),y)).

given clause #445: (wt=36) 163 [hyper,1,116,24] P(i(n(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))),u)).

given clause #446: (wt=21) 1450 [hyper,1,362,472] P(i(i(i(n(i(n(n(x)),x)),y),n(n(z))),z)).

given clause #447: (wt=21) 1474 [hyper,1,116,1452] P(i(n(i(i(n(n(i(x,x))),n(n(y))),y)),z)).

given clause #448: (wt=21) 1494 [hyper,1,116,1454] P(i(n(i(i(i(n(n(x)),x),n(n(y))),y)),z)).

given clause #449: (wt=27) 165 [hyper,1,116,20] P(i(n(i(x,i(y,i(z,y)))),u)).

given clause #450: (wt=21) 1516 [hyper,1,63,369] P(i(n(n(i(i(x,y),z))),i(n(x),z))).

given clause #451: (wt=21) 1524 [hyper,1,49,369] P(i(x,i(n(n(i(x,y))),y))).

given clause #452: (wt=20) 5560 [hyper,1,65,1524] P(i(n(i(n(n(i(x,y))),y)),i(x,z))).

given clause #453: (wt=23) 168 [hyper,1,34,114] P(i(i(i(n(i(x,y)),i(n(y),x)),z),z)).

given clause #454: (wt=21) 1534 [hyper,1,26,369] P(i(i(n(x),n(y)),i(n(n(y)),x))).

given clause #455: (wt=21) 1554 [hyper,1,369,143] P(i(n(n(i(i(x,i(n(x),y)),z))),z)).

given clause #456: (wt=21) 1556 [hyper,1,369,89] P(i(n(n(i(i(x,y),y))),i(n(y),x))).

given clause #457: (wt=26) 169 [hyper,1,3,114] P(i(i(i(n(x),y),z),i(n(i(y,x)),z))).

given clause #458: (wt=20) 6004 [hyper,1,169,386] P(i(n(i(n(x),y)),n(n(i(x,y))))).

given clause #459: (wt=21) 1558 [hyper,1,369,75] P(i(n(n(i(i(n(n(x)),i(y,x)),z))),z)).

given clause #460: (wt=21) 1594 [hyper,1,372,1547] P(n(n(i(n(i(n(n(i(n(n(i(x,x))),y))),y)),z)))).

given clause #461: (wt=35) 170 [hyper,1,2,114] P(i(x,i(n(i(y,z)),i(n(z),y)))).

given clause #462: (wt=21) 1604 [hyper,1,44,1547] P(i(n(n(i(n(n(i(x,x))),y))),i(z,y))).

given clause #463: (wt=21) 1610 [hyper,1,34,1547] P(i(i(i(n(n(i(n(n(i(x,x))),y))),y),z),z)).

given clause #464: (wt=21) 1615 [hyper,1,372,1550] P(n(n(i(n(i(n(n(i(i(n(n(x)),x),y))),y)),z)))).

given clause #465: (wt=23) 172 [hyper,1,34,141] P(i(i(i(n(i(x,i(n(x),y))),z),u),u)).

given clause #466: (wt=21) 1625 [hyper,1,44,1550] P(i(n(n(i(i(n(n(x)),x),y))),i(z,y))).

given clause #467: (wt=21) 1631 [hyper,1,34,1550] P(i(i(i(n(n(i(i(n(n(x)),x),y))),y),z),z)).

given clause #468: (wt=21) 1638 [hyper,1,362,1541] P(i(n(n(i(i(n(i(x,y)),x),n(n(z))))),z)).

given clause #469: (wt=38) 173 [hyper,1,3,141] P(i(i(x,y),i(n(i(z,i(n(z),u))),y))).

given clause #470: (wt=21) 1640 [hyper,1,116,1541] P(i(n(i(n(n(i(i(n(i(x,y)),x),z))),z)),u)).

given clause #471: (wt=21) 1692 [hyper,1,65,142] P(i(n(i(n(i(x,y)),z)),i(n(x),u))).

given clause #472: (wt=21) 1704 [hyper,1,65,47] P(i(n(i(i(i(x,y),z),z)),i(y,u))).

given clause #473: (wt=35) 174 [hyper,1,2,141] P(i(x,i(n(i(y,i(n(y),z))),u))).

given clause #474: (wt=21) 1707 [hyper,1,65,36] P(i(n(i(x,i(y,z))),i(z,u))).

given clause #475: (wt=21) 1714 [hyper,1,362,1546] P(i(n(n(i(n(n(i(n(n(x)),x))),n(n(y))))),y)).

given clause #476: (wt=21) 1717 [hyper,1,116,1546] P(i(n(i(n(n(i(n(n(i(n(n(x)),x))),y))),y)),z)).

given clause #477: (wt=39) 175 [hyper,1,116,27] P(i(n(i(x,i(i(n(y),n(z)),i(z,y)))),u)).

given clause #478: (wt=21) 1737 [hyper,1,362,1549] P(i(n(n(i(i(x,n(n(x))),n(n(y))))),y)).

given clause #479: (wt=21) 1740 [hyper,1,116,1549] P(i(n(i(n(n(i(i(x,n(n(x))),y))),y)),z)).

given clause #480: (wt=21) 1858 [hyper,1,367,328] P(n(n(i(n(i(x,y)),i(n(n(y)),z))))).

given clause #481: (wt=41) 176 [hyper,1,34,27] P(i(i(i(x,i(i(n(y),n(z)),i(z,y))),u),u)).

given clause #482: (wt=21) 1869 [hyper,1,367,340] P(n(n(i(n(n(x)),i(i(x,y),y))))).

given clause #483: (wt=21) 1893 [hyper,1,367,365] P(n(n(i(i(i(n(n(x)),x),y),i(z,y))))).

given clause #484: (wt=21) 1970 [hyper,1,367,439] P(n(n(i(i(n(n(i(x,x))),y),i(z,y))))).

given clause #485: (wt=29) 177 [hyper,1,3,27] P(i(i(i(i(n(x),n(y)),i(y,x)),z),i(u,z))).

given clause #486: (wt=21) 1987 [hyper,1,369,488] P(i(n(n(i(i(i(i(n(n(x)),x),y),y),z))),z)).

given clause #487: (wt=21) 1988 [hyper,1,367,488] P(n(n(i(i(i(i(i(n(n(x)),x),y),y),z),z)))).

given clause #488: (wt=21) 2000 [hyper,1,367,491] P(n(n(i(i(i(x,n(n(x))),n(n(x))),x)))).

given clause #489: (wt=71) 178 [hyper,1,2,27] P(i(x,i(y,i(i(n(z),n(u)),i(u,z))))).

given clause #490: (wt=21) 2030 [hyper,1,369,499] P(i(n(n(i(i(n(i(x,n(n(x)))),y),z))),z)).

given clause #491: (wt=21) 2031 [hyper,1,367,499] P(n(n(i(i(i(n(i(x,n(n(x)))),y),z),z)))).

given clause #492: (wt=21) 2044 [hyper,1,369,505] P(i(n(n(i(n(n(i(x,i(y,x)))),z))),z)).

given clause #493: (wt=22) 179 [hyper,1,116,148] P(i(n(i(i(i(n(x),y),z),i(x,z))),u)).

given clause #494: (wt=21) 2045 [hyper,1,367,505] P(n(n(i(i(n(n(i(x,i(y,x)))),z),z)))).

given clause #495: (wt=21) 2056 [hyper,1,369,534] P(i(n(n(i(i(i(n(n(i(x,x))),y),y),z))),z)).

given clause #496: (wt=21) 2057 [hyper,1,367,534] P(n(n(i(i(i(i(n(n(i(x,x))),y),y),z),z)))).

given clause #497: (wt=24) 181 [hyper,1,34,148] P(i(i(i(i(i(n(x),y),z),i(x,z)),u),u)).

given clause #498: (wt=21) 2073 [hyper,1,369,542] P(i(n(n(i(n(n(i(n(i(n(n(x)),x)),y))),z))),z)).

given clause #499: (wt=21) 2074 [hyper,1,367,542] P(n(n(i(i(n(n(i(n(i(n(n(x)),x)),y))),z),z)))).

given clause #500: (wt=21) 2099 [hyper,1,367,601] P(n(n(i(x,i(y,n(n(x))))))).

given clause #501: (wt=27) 182 [hyper,1,28,148] P(i(x,i(y,i(n(x),z)))).

given clause #502: (wt=21) 2197 [hyper,1,369,619] P(i(n(n(i(n(n(i(x,y))),z))),i(y,z))).

given clause #503: (wt=21) 2198 [hyper,1,367,619] P(n(n(i(i(n(n(i(x,y))),z),i(y,z))))).

given clause #504: (wt=21) 2233 [hyper,1,369,715] P(i(n(n(i(n(n(i(n(i(x,n(y))),y))),z))),z)).

given clause #505: (wt=25) 183 [hyper,1,26,148] P(i(i(n(x),n(i(n(y),z))),i(y,x))).

given clause #506: (wt=21) 2234 [hyper,1,367,715] P(n(n(i(i(n(n(i(n(i(x,n(y))),y))),z),z)))).

given clause #507: (wt=21) 2365 [hyper,1,369,872] P(i(n(n(i(i(n(i(n(i(x,y)),x)),z),u))),u)).

given clause #508: (wt=21) 2366 [hyper,1,367,872] P(n(n(i(i(i(n(i(n(i(x,y)),x)),z),u),u)))).

given clause #509: (wt=28) 185 [hyper,1,21,148] P(i(i(x,n(y)),i(y,i(x,z)))).

given clause #510: (wt=21) 2406 [hyper,1,369,1083] P(i(n(n(i(n(n(i(n(i(n(n(x)),y)),x))),z))),z)).

given clause #511: (wt=21) 2407 [hyper,1,367,1083] P(n(n(i(i(n(n(i(n(i(n(n(x)),y)),x))),z),z)))).

given clause #512: (wt=21) 2446 [hyper,1,367,1121] P(n(n(i(n(i(x,y)),i(z,n(y)))))).

given clause #513: (wt=31) 186 [hyper,1,3,148] P(i(i(i(x,y),z),i(i(i(n(x),u),y),z))).

given clause #514: (wt=21) 2458 [hyper,1,369,1135] P(i(n(n(i(n(n(i(n(i(x,y)),n(y)))),z))),z)).

given clause #515: (wt=21) 2459 [hyper,1,367,1135] P(n(n(i(i(n(n(i(n(i(x,y)),n(y)))),z),z)))).

given clause #516: (wt=21) 2519 [hyper,1,367,1307] P(n(n(i(n(i(x,n(n(y)))),i(y,z))))).

given clause #517: (wt=37) 187 [hyper,1,2,148] P(i(x,i(i(i(n(y),z),u),i(y,u)))).

given clause #518: (wt=21) 2568 [hyper,1,367,1447] P(n(n(i(i(i(n(i(x,y)),x),n(n(z))),z)))).

given clause #519: (wt=21) 2582 [hyper,1,367,1451] P(n(n(i(i(n(n(i(n(n(x)),x))),n(n(y))),y)))).

given clause #520: (wt=21) 2606 [hyper,1,367,1453] P(n(n(i(i(i(x,n(n(x))),n(n(y))),y)))).

given clause #521: (wt=25) 189 [hyper,1,148,34] P(i(x,i(i(i(n(x),y),z),z))).

given clause #522: (wt=21) 2652 [hyper,1,367,1521] P(n(n(i(n(n(i(n(x),n(y)))),i(y,x))))).

given clause #523: (wt=21) 2674 [hyper,1,367,1522] P(n(n(i(n(n(i(i(x,y),z))),i(y,z))))).

given clause #524: (wt=21) 2687 [hyper,1,367,1523] P(n(n(i(n(n(i(i(x,i(y,x)),z))),z)))).

given clause #525: (wt=22) 191 [hyper,1,34,180] P(i(i(i(n(i(n(x),y)),i(x,z)),u),u)).

given clause #526: (wt=21) 2701 [hyper,1,367,1536] P(n(n(i(n(n(i(i(n(n(x)),x),n(n(y))))),y)))).

given clause #527: (wt=21) 2723 [hyper,1,367,1537] P(n(n(i(n(n(i(n(n(i(x,x))),n(n(y))))),y)))).

given clause #528: (wt=21) 2745 [hyper,1,367,1538] P(n(n(i(n(n(i(i(n(i(x,y)),n(y)),z))),z)))).

given clause #529: (wt=27) 192 [hyper,1,3,180] P(i(i(i(x,y),z),i(n(i(n(x),u)),z))).

given clause #530: (wt=20) 6927 [hyper,1,382,192] P(i(n(i(n(x),y)),n(n(i(x,z))))).

given clause #531: (wt=21) 2761 [hyper,1,367,1539] P(n(n(i(n(n(i(i(n(i(n(n(x)),y)),x),z))),z)))).

given clause #532: (wt=21) 2775 [hyper,1,367,1540] P(n(n(i(n(n(i(n(n(i(n(i(x,y)),x))),z))),z)))).

given clause #533: (wt=33) 193 [hyper,1,2,180] P(i(x,i(n(i(n(y),z)),i(y,u)))).

given clause #534: (wt=21) 2789 [hyper,1,367,1542] P(n(n(i(n(n(i(i(n(i(x,n(y))),y),z))),z)))).

given clause #535: (wt=21) 2809 [hyper,1,367,1543] P(n(n(i(n(n(i(i(n(n(x)),x),x))),n(n(x)))))).

given clause #536: (wt=21) 2830 [hyper,1,367,1544] P(n(n(i(n(n(i(n(n(i(x,n(n(x))))),y))),y)))).

given clause #537: (wt=23) 194 [hyper,1,116,143] P(i(n(i(i(i(x,i(n(x),y)),z),z)),u)).

given clause #538: (wt=21) 2855 [hyper,1,367,1545] P(n(n(i(n(n(i(i(n(i(n(n(x)),x)),y),z))),z)))).

given clause #539: (wt=21) 2866 [hyper,1,382,100] P(i(n(i(x,y)),n(n(i(n(x),z))))).

given clause #540: (wt=21) 2887 [hyper,1,367,1690] P(n(n(i(n(i(n(i(x,y)),z)),i(y,u))))).

given clause #541: (wt=25) 195 [hyper,1,34,143] P(i(i(i(i(i(x,i(n(x),y)),z),z),u),u)).

given clause #542: (wt=21) 2914 [hyper,1,369,1771] P(i(n(n(i(i(x,y),n(z)))),i(z,x))).

given clause #543: (wt=21) 2915 [hyper,1,367,1771] P(n(n(i(i(i(x,y),n(z)),i(z,x))))).

given clause #544: (wt=21) 2918 [hyper,1,94,1771] P(i(n(i(x,i(y,z))),i(u,y))).

given clause #545: (wt=33) 196 [hyper,1,26,143] P(i(i(n(x),n(i(y,i(n(y),z)))),x)).

given clause #546: (wt=21) 2947 [hyper,1,372,2929] P(n(n(i(n(i(n(i(x,i(y,z))),y)),u)))).

given clause #547: (wt=21) 2953 [hyper,1,34,2929] P(i(i(i(n(i(x,i(y,z))),y),u),u)).

given clause #548: (wt=21) 2969 [hyper,1,34,2934] P(i(i(n(n(i(n(i(n(i(x,y)),z)),x))),u),u)).

given clause #549: (wt=23) 197 [hyper,1,24,143] P(i(i(i(i(n(x),y),x),x),i(n(x),y))).

given clause #550: (wt=21) 2972 [hyper,1,372,2935] P(n(n(i(n(i(n(i(n(i(n(n(x)),y)),z)),x)),u)))).

given clause #551: (wt=21) 2978 [hyper,1,44,2935] P(i(n(i(n(i(n(n(x)),y)),z)),i(u,x))).

given clause #552: (wt=21) 2979 [hyper,1,34,2935] P(i(i(i(n(i(n(i(n(n(x)),y)),z)),x),u),u)).

given clause #553: (wt=30) 198 [hyper,1,21,143] P(i(i(x,y),i(x,i(n(y),z)))).

given clause #554: (wt=21) 2989 [hyper,1,367,2540] P(n(n(i(n(i(x,y)),n(n(i(y,z))))))).

given clause #555: (wt=21) 2999 [hyper,1,367,2941] P(n(n(i(n(i(n(i(x,y)),z)),i(u,x))))).

given clause #556: (wt=21) 3000 [hyper,1,369,2942] P(i(n(n(i(i(n(i(n(i(x,y)),z)),x),u))),u)).

given clause #557: (wt=42) 199 [hyper,1,3,143] P(i(i(x,y),i(i(i(z,i(n(z),u)),x),y))).

given clause #558: (wt=21) 3001 [hyper,1,367,2942] P(n(n(i(i(i(n(i(n(i(x,y)),z)),x),u),u)))).

given clause #559: (wt=21) 3028 [hyper,1,367,2949] P(n(n(i(n(i(x,i(n(n(y)),z))),y)))).

given clause #560: (wt=21) 3346 [hyper,1,117,362] P(i(i(i(n(n(x)),y),y),i(n(y),x))).

given clause #561: (wt=39) 200 [hyper,1,2,143] P(i(x,i(i(i(y,i(n(y),z)),u),u))).

given clause #562: (wt=21) 3451 [hyper,1,372,3444] P(n(n(i(n(i(n(i(n(i(x,n(y))),z)),y)),u)))).

given clause #563: (wt=21) 3457 [hyper,1,44,3444] P(i(n(i(n(i(x,n(y))),z)),i(u,y))).

given clause #564: (wt=21) 3458 [hyper,1,34,3444] P(i(i(i(n(i(n(i(x,n(y))),z)),y),u),u)).

given clause #565: (wt=35) 201 [hyper,1,26,29] P(i(i(n(x),n(i(y,i(z,y)))),i(u,x))).

given clause #566: (wt=21) 3466 [hyper,1,367,3443] P(n(n(i(n(i(x,i(y,n(z)))),z)))).

given clause #567: (wt=21) 3745 [hyper,1,379,3527] P(n(n(i(i(i(n(i(i(n(x),y),y)),x),z),z)))).

given clause #568: (wt=21) 3749 [hyper,1,188,3527] P(i(n(i(n(i(n(i(i(n(x),y),y)),x)),z)),u)).

given clause #569: (wt=32) 202 [hyper,1,24,29] P(i(i(i(i(x,y),y),y),i(z,i(x,y)))).

given clause #570: (wt=21) 3771 [hyper,1,372,3487] P(n(n(i(n(i(n(i(i(i(x,y),z),z)),x)),u)))).

given clause #571: (wt=21) 3780 [hyper,1,44,3487] P(i(n(i(i(i(x,y),z),z)),i(u,x))).

given clause #572: (wt=21) 3781 [hyper,1,34,3487] P(i(i(i(n(i(i(i(x,y),z),z)),x),u),u)).

given clause #573: (wt=50) 203 [hyper,1,21,29] P(i(i(x,y),i(z,i(x,i(u,y))))).

given clause #574: (wt=21) 3792 [hyper,1,34,3747] P(i(i(n(n(i(n(i(i(n(x),y),y)),x))),z),z)).

given clause #575: (wt=21) 3802 [hyper,1,116,3497] P(i(n(i(n(i(i(i(x,n(y)),z),z)),y)),u)).

given clause #576: (wt=21) 3851 [hyper,1,116,3773] P(i(n(i(n(i(i(i(n(n(x)),y),z),z)),x)),u)).

given clause #577: (wt=55) 204 [hyper,1,29,148] P(i(x,i(y,i(z,i(n(y),u))))).

given clause #578: (wt=21) 3864 [hyper,1,367,3759] P(n(n(i(n(i(i(n(x),y),y)),i(z,x))))).

given clause #579: (wt=21) 3915 [hyper,1,369,3765] P(i(n(n(i(i(n(i(i(n(x),y),y)),x),z))),z)).

given clause #580: (wt=21) 4203 [hyper,1,94,386] P(i(n(i(x,n(y))),n(n(i(z,y))))).

given clause #581: (wt=55) 205 [hyper,1,29,143] P(i(x,i(y,i(z,i(n(z),u))))).

given clause #582: (wt=21) 4240 [hyper,1,367,4202] P(n(n(i(n(i(x,y)),n(n(i(z,x))))))).

given clause #583: (wt=21) 4888 [hyper,1,100,139] P(i(n(i(x,y)),i(i(x,z),z))).

given clause #584: (wt=21) 6740 [hyper,1,55,186] P(i(i(i(n(n(x)),y),n(z)),i(z,x))).

given clause #585: (wt=55) 206 [hyper,1,29,75] P(i(x,i(y,i(n(n(z)),i(u,z))))).

given clause #586: (wt=21) 6749 [hyper,1,186,590] P(i(i(i(n(i(n(n(x)),x)),y),x),n(n(x)))).

given clause #587: (wt=21) 6938 [hyper,1,192,386] P(i(n(i(n(n(x)),y)),n(n(i(z,x))))).

given clause #588: (wt=21) 7113 [hyper,1,534,198] P(i(i(n(n(i(x,x))),y),i(n(y),z))).

given clause #589: (wt=51) 207 [hyper,1,29,51] P(i(x,i(y,i(n(z),i(z,u))))).

given clause #590: (wt=21) 7114 [hyper,1,488,198] P(i(i(i(n(n(x)),x),y),i(n(y),z))).

given clause #591: (wt=22) 281 [hyper,1,116,229] P(i(n(i(n(i(i(x,y),y)),i(x,z))),u)).

given clause #592: (wt=22) 371 [hyper,1,241,367] P(i(i(x,y),i(x,n(n(y))))).

given clause #593: (wt=49) 208 [hyper,1,29,37] P(i(x,i(n(y),i(z,i(y,u))))).

given clause #594: (wt=13) 7678 [hyper,1,859,371] P(i(n(i(x,y)),n(n(x)))).

given clause #595: (wt=15) 7926 [hyper,1,367,7678] P(n(n(i(n(i(x,y)),n(n(x)))))).

given clause #596: (wt=17) 7669 [hyper,1,3765,371] P(i(n(i(i(n(x),y),y)),n(n(x)))).

given clause #597: (wt=59) 209 [hyper,1,29,26] P(i(x,i(i(n(y),n(z)),i(u,i(z,y))))).

given clause #598: (wt=17) 7672 [hyper,1,2942,371] P(i(n(i(n(i(x,y)),z)),n(n(x)))).

given clause #599: (wt=17) 7683 [hyper,1,534,371] P(i(i(n(n(i(x,x))),y),n(n(y)))).

given clause #600: (wt=17) 7684 [hyper,1,488,371] P(i(i(i(n(n(x)),x),y),n(n(y)))).

given clause #601: (wt=83) 210 [hyper,1,29,24] P(i(x,i(i(i(y,z),z),i(u,i(i(z,y),y))))).

given clause #602: (wt=17) 7935 [hyper,1,116,7678] P(i(n(i(n(i(x,y)),n(n(x)))),z)).

given clause #603: (wt=19) 7668 [hyper,1,3781,371] P(i(n(i(i(i(x,y),z),z)),n(n(x)))).

given clause #604: (wt=19) 7670 [hyper,1,3458,371] P(i(n(i(n(i(x,n(y))),z)),n(n(y)))).

given clause #605: (wt=47) 211 [hyper,1,29,23] P(i(x,i(y,i(z,i(u,y))))).

given clause #606: (wt=19) 7671 [hyper,1,2953,371] P(i(n(i(x,i(y,z))),n(n(y)))).

given clause #607: (wt=19) 7673 [hyper,1,1631,371] P(i(n(n(i(i(n(n(x)),x),y))),n(n(y)))).

given clause #608: (wt=19) 7674 [hyper,1,1610,371] P(i(n(n(i(n(n(i(x,x))),y))),n(n(y)))).

given clause #609: (wt=35) 212 [hyper,1,148,146] P(i(x,i(n(i(y,i(n(x),z))),u))).

given clause #610: (wt=19) 7677 [hyper,1,931,371] P(i(i(i(n(i(x,y)),x),z),n(n(z)))).

given clause #611: (wt=19) 7680 [hyper,1,768,371] P(i(i(n(n(i(n(n(x)),x))),y),n(n(y)))).

given clause #612: (wt=19) 7682 [hyper,1,587,371] P(i(i(i(x,n(n(x))),y),n(n(y)))).

given clause #613: (wt=31) 213 [hyper,1,143,146] P(i(n(i(x,i(y,i(n(y),z)))),u)).

given clause #614: (wt=19) 7925 [hyper,1,372,7678] P(n(n(i(n(i(n(i(x,y)),n(n(x)))),z)))).

given clause #615: (wt=19) 7946 [hyper,1,34,7678] P(i(i(i(n(i(x,y)),n(n(x))),z),z)).

given clause #616: (wt=19) 7961 [hyper,1,367,7669] P(n(n(i(n(i(i(n(x),y),y)),n(n(x)))))).

given clause #617: (wt=23) 214 [hyper,1,116,146] P(i(n(i(x,i(n(i(y,x)),z))),u)).

given clause #618: (wt=19) 7991 [hyper,1,367,7672] P(n(n(i(n(i(n(i(x,y)),z)),n(n(x)))))).

given clause #619: (wt=19) 8004 [hyper,1,367,7683] P(n(n(i(i(n(n(i(x,x))),y),n(n(y)))))).

given clause #620: (wt=19) 8033 [hyper,1,367,7684] P(n(n(i(i(i(n(n(x)),x),y),n(n(y)))))).

given clause #621: (wt=31) 215 [hyper,1,75,146] P(i(n(i(x,i(n(n(y)),i(z,y)))),u)).

given clause #622: (wt=20) 7835 [hyper,1,371,390] P(i(i(n(n(x)),y),n(n(i(x,y))))).

given clause #623: (wt=21) 7738 [hyper,1,371,3497] P(i(n(i(i(i(x,n(y)),z),z)),n(n(y)))).

given clause #624: (wt=21) 7774 [hyper,1,371,1549] P(i(n(n(i(i(x,n(n(x))),y))),n(n(y)))).

given clause #625: (wt=29) 216 [hyper,1,51,146] P(i(n(i(x,i(n(y),i(y,z)))),u)).

given clause #626: (wt=21) 7776 [hyper,1,371,1546] P(i(n(n(i(n(n(i(n(n(x)),x))),y))),n(n(y)))).

given clause #627: (wt=21) 7780 [hyper,1,371,1541] P(i(n(n(i(i(n(i(x,y)),x),z))),n(n(z)))).

given clause #628: (wt=21) 7795 [hyper,1,371,1126] P(i(i(i(n(i(x,y)),n(y)),z),n(n(z)))).

given clause #629: (wt=32) 217 [hyper,1,37,146] P(i(n(x),i(n(i(y,i(x,z))),u))).

given clause #630: (wt=21) 7799 [hyper,1,371,1071] P(i(i(i(n(i(n(n(x)),y)),x),z),n(n(z)))).

given clause #631: (wt=21) 7806 [hyper,1,371,868] P(i(i(n(n(i(n(i(x,y)),x))),z),n(n(z)))).

given clause #632: (wt=21) 7816 [hyper,1,371,673] P(i(i(i(n(i(x,n(y))),y),z),n(n(z)))).

given clause #633: (wt=25) 218 [hyper,1,34,146] P(i(i(i(x,i(n(i(y,x)),z)),u),u)).

given clause #634: (wt=21) 7831 [hyper,1,371,479] P(i(i(n(n(i(x,n(n(x))))),y),n(n(y)))).

given clause #635: (wt=21) 7832 [hyper,1,371,472] P(i(i(i(n(i(n(n(x)),x)),y),z),n(n(z)))).

given clause #636: (wt=21) 7920 [hyper,1,1524,7678] P(i(n(n(i(i(n(i(x,y)),n(n(x))),z))),z)).

given clause #637: (wt=37) 219 [hyper,1,26,146] P(i(i(n(x),n(y)),i(n(i(z,i(y,x))),u))).

given clause #638: (wt=21) 7921 [hyper,1,969,7678] P(i(i(n(n(i(n(i(x,y)),n(n(x))))),z),z)).

given clause #639: (wt=21) 7924 [hyper,1,379,7678] P(n(n(i(i(i(n(i(x,y)),n(n(x))),z),z)))).

given clause #640: (wt=21) 7931 [hyper,1,188,7678] P(i(n(i(n(i(n(i(x,y)),n(n(x)))),z)),u)).

given clause #641: (wt=49) 220 [hyper,1,24,146] P(i(i(i(x,y),y),i(n(i(z,i(i(y,x),x))),u))).

given clause #642: (wt=21) 7970 [hyper,1,116,7669] P(i(n(i(n(i(i(n(x),y),y)),n(n(x)))),z)).

given clause #643: (wt=21) 7993 [hyper,1,116,7672] P(i(n(i(n(i(n(i(x,y)),z)),n(n(x)))),u)).

given clause #644: (wt=21) 8013 [hyper,1,116,7683] P(i(n(i(i(n(n(i(x,x))),y),n(n(y)))),z)).

given clause #645: (wt=31) 221 [hyper,1,23,146] P(i(x,i(n(i(y,i(z,x))),u))).

given clause #646: (wt=21) 8042 [hyper,1,116,7684] P(i(n(i(i(i(n(n(x)),x),y),n(n(y)))),z)).

given clause #647: (wt=21) 8078 [hyper,1,367,7668] P(n(n(i(n(i(i(i(x,y),z),z)),n(n(x)))))).

given clause #648: (wt=21) 8091 [hyper,1,367,7670] P(n(n(i(n(i(n(i(x,n(y))),z)),n(n(y)))))).

given clause #649: (wt=39) 223 [hyper,1,2,146] P(i(x,i(y,i(n(i(z,y)),u)))).

given clause #650: (wt=21) 8107 [hyper,1,367,7671] P(n(n(i(n(i(x,i(y,z))),n(n(y)))))).

given clause #651: (wt=21) 8121 [hyper,1,367,7673] P(n(n(i(n(n(i(i(n(n(x)),x),y))),n(n(y)))))).

given clause #652: (wt=21) 8156 [hyper,1,367,7674] P(n(n(i(n(n(i(n(n(i(x,x))),y))),n(n(y)))))).

given clause #653: (wt=39) 224 [hyper,1,146,114] P(i(n(i(x,i(n(i(y,z)),i(n(z),y)))),u)).

given clause #654: (wt=21) 8196 [hyper,1,367,7677] P(n(n(i(i(i(n(i(x,y)),x),z),n(n(z)))))).

given clause #655: (wt=21) 8226 [hyper,1,367,7680] P(n(n(i(i(n(n(i(n(n(x)),x))),y),n(n(y)))))).

given clause #656: (wt=21) 8257 [hyper,1,367,7682] P(n(n(i(i(i(x,n(n(x))),y),n(n(y)))))).

given clause #657: (wt=43) 225 [hyper,1,146,89] P(i(n(i(x,i(i(i(y,z),z),i(n(z),y)))),u)).

given clause #658: (wt=22) 395 [hyper,1,367,190] P(n(n(i(n(i(n(i(n(x),y)),i(x,z))),u)))).

given clause #659: (wt=22) 397 [hyper,1,367,155] P(n(n(i(n(i(n(i(n(x),i(x,y))),z)),u)))).

given clause #660: (wt=22) 403 [hyper,1,367,142] P(n(n(i(n(x),i(n(i(x,y)),z))))).

given clause #661: (wt=39) 226 [hyper,1,146,34] P(i(n(i(x,i(y,i(i(y,z),z)))),u)).

given clause #662: (wt=22) 405 [hyper,1,367,138] P(n(n(i(i(n(n(x)),n(n(y))),i(x,y))))).

given clause #663: (wt=22) 417 [hyper,1,367,49] P(n(n(i(i(i(i(x,y),y),z),i(x,z))))).

given clause #664: (wt=22) 830 [hyper,1,34,380] P(i(i(i(n(x),n(n(i(x,y)))),z),z)).

given clause #665: (wt=25) 227 [hyper,1,143,49] P(i(x,i(n(i(i(x,y),y)),z))).

given clause #666: (wt=22) 849 [hyper,1,241,831] P(i(i(x,n(i(y,z))),i(x,y))).

given clause #667: (wt=17) 8976 [hyper,1,3765,849] P(i(n(i(i(n(n(i(x,y))),z),z)),x)).

given clause #668: (wt=17) 8979 [hyper,1,2942,849] P(i(n(i(n(i(n(i(x,y)),z)),u)),x)).

given clause #669: (wt=24) 228 [hyper,1,116,49] P(i(n(i(i(i(i(x,y),y),z),i(x,z))),u)).

given clause #670: (wt=19) 8975 [hyper,1,3781,849] P(i(n(i(i(i(n(i(x,y)),z),u),u)),x)).

given clause #671: (wt=19) 8986 [hyper,1,673,849] P(i(n(i(x,n(n(i(y,z))))),y)).

given clause #672: (wt=19) 9089 [hyper,1,367,8976] P(n(n(i(n(i(i(n(n(i(x,y))),z),z)),x)))).

given clause #673: (wt=26) 230 [hyper,1,34,49] P(i(i(i(i(i(i(x,y),y),z),i(x,z)),u),u)).

given clause #674: (wt=19) 9090 [hyper,1,362,8976] P(i(n(i(i(n(n(i(n(n(x)),y))),z),z)),x)).

given clause #675: (wt=19) 9112 [hyper,1,367,8979] P(n(n(i(n(i(n(i(n(i(x,y)),z)),u)),x)))).

given clause #676: (wt=19) 9113 [hyper,1,362,8979] P(i(n(i(n(i(n(i(n(n(x)),y)),z)),u)),x)).

given clause #677: (wt=71) 231 [hyper,1,29,49] P(i(x,i(y,i(z,i(i(y,u),u))))).

given clause #678: (wt=21) 8974 [hyper,1,7816,849] P(n(n(i(n(i(x,n(n(i(y,z))))),y)))).

given clause #679: (wt=21) 8989 [hyper,1,534,849] P(i(i(n(n(i(x,x))),n(i(y,z))),y)).

given clause #680: (wt=21) 8990 [hyper,1,488,849] P(i(i(i(n(n(x)),x),n(i(y,z))),y)).

given clause #681: (wt=35) 232 [hyper,1,28,49] P(i(x,i(y,i(i(x,z),z)))).

given clause #682: (wt=21) 9010 [hyper,1,26,849] P(i(i(n(n(i(x,y))),n(z)),i(z,x))).

given clause #683: (wt=21) 9082 [hyper,1,849,8976] P(i(n(i(i(n(n(i(n(i(x,y)),z))),u),u)),x)).

given clause #684: (wt=21) 9088 [hyper,1,371,8976] P(i(n(i(i(n(n(i(x,y))),z),z)),n(n(x)))).

given clause #685: (wt=29) 233 [hyper,1,26,49] P(i(i(n(x),n(i(i(y,z),z))),i(y,x))).

given clause #686: (wt=21) 9102 [hyper,1,116,8976] P(i(n(i(n(i(i(n(n(i(x,y))),z),z)),x)),u)).

given clause #687: (wt=21) 9111 [hyper,1,371,8979] P(i(n(i(n(i(n(i(x,y)),z)),u)),n(n(x)))).

given clause #688: (wt=21) 9116 [hyper,1,367,8975] P(n(n(i(n(i(i(i(n(i(x,y)),z),u),u)),x)))).

given clause #689: (wt=32) 234 [hyper,1,21,49] P(i(i(x,i(y,z)),i(y,i(x,z)))).

given clause #690: (wt=21) 9117 [hyper,1,362,8975] P(i(n(i(i(i(n(i(n(n(x)),y)),z),u),u)),x)).

given clause #691: (wt=21) 9154 [hyper,1,367,9090] P(n(n(i(n(i(i(n(n(i(n(n(x)),y))),z),z)),x)))).

given clause #692: (wt=21) 9161 [hyper,1,367,9113] P(n(n(i(n(i(n(i(n(i(n(n(x)),y)),z)),u)),x)))).

given clause #693: (wt=35) 235 [hyper,1,3,49] P(i(i(i(x,y),z),i(i(i(i(x,u),u),y),z))).

given clause #694: (wt=22) 860 [hyper,1,3,831] P(i(i(x,y),i(n(i(x,z)),y))).

given clause #695: (wt=15) 9695 [hyper,1,1126,860] P(i(n(i(n(i(x,y)),z)),n(y))).

given clause #696: (wt=17) 9687 [hyper,1,7795,860] P(n(n(i(n(i(n(i(x,y)),z)),n(y))))).

given clause #697: (wt=41) 236 [hyper,1,2,49] P(i(x,i(i(i(i(y,z),z),u),i(y,u)))).

given clause #698: (wt=17) 9689 [hyper,1,3765,860] P(i(n(i(n(i(i(n(x),y),y)),z)),x)).

given clause #699: (wt=17) 9702 [hyper,1,534,860] P(i(n(i(i(n(n(i(x,x))),y),z)),y)).

given clause #700: (wt=17) 9703 [hyper,1,488,860] P(i(n(i(i(i(n(n(x)),x),y),z)),y)).

given clause #701: (wt=43) 237 [hyper,1,49,146] P(i(x,i(n(i(y,i(i(x,z),z))),u))).

given clause #702: (wt=19) 9688 [hyper,1,3781,860] P(i(n(i(n(i(i(i(x,y),z),z)),u)),x)).

given clause #703: (wt=19) 9690 [hyper,1,3458,860] P(i(n(i(n(i(n(i(x,n(y))),z)),u)),y)).

given clause #704: (wt=19) 9691 [hyper,1,2953,860] P(i(n(i(n(i(x,i(y,z))),u)),y)).

given clause #705: (wt=29) 238 [hyper,1,49,34] P(i(x,i(i(i(i(x,y),y),z),z))).

given clause #706: (wt=19) 9692 [hyper,1,1631,860] P(i(n(i(n(n(i(i(n(n(x)),x),y))),z)),y)).

given clause #707: (wt=19) 9693 [hyper,1,1610,860] P(i(n(i(n(n(i(n(n(i(x,x))),y))),z)),y)).

given clause #708: (wt=19) 9697 [hyper,1,931,860] P(i(n(i(i(i(n(i(x,y)),x),z),u)),z)).

given clause #709: (wt=23) 239 [hyper,1,49,26] P(i(x,i(i(n(y),n(x)),y))).

given clause #710: (wt=19) 9699 [hyper,1,768,860] P(i(n(i(i(n(n(i(n(n(x)),x))),y),z)),y)).

given clause #711: (wt=19) 9701 [hyper,1,587,860] P(i(n(i(i(i(x,n(n(x))),y),z)),y)).

given clause #712: (wt=19) 9925 [hyper,1,860,9695] P(i(n(i(n(i(n(i(x,y)),z)),u)),n(y))).

given clause #713: (wt=26) 240 [hyper,1,49,24] P(i(i(x,y),i(i(i(y,x),x),y))).

given clause #714: (wt=19) 9932 [hyper,1,116,9695] P(i(n(i(n(i(n(i(x,y)),z)),n(y))),u)).

given clause #715: (wt=19) 9946 [hyper,1,367,9689] P(n(n(i(n(i(n(i(i(n(x),y),y)),z)),x)))).

given clause #716: (wt=19) 9972 [hyper,1,367,9702] P(n(n(i(n(i(i(n(n(i(x,x))),y),z)),y)))).

given clause #717: (wt=41) 243 [hyper,1,49,3] P(i(x,i(i(y,z),i(i(x,y),z)))).

given clause #718: (wt=19) 10005 [hyper,1,367,9703] P(n(n(i(n(i(i(i(n(n(x)),x),y),z)),y)))).

given clause #719: (wt=20) 9872 [hyper,1,860,390] P(i(n(i(i(n(n(x)),y),z)),i(x,y))).

given clause #720: (wt=21) 9726 [hyper,1,55,860] P(i(n(i(i(n(x),n(y)),z)),i(y,x))).

given clause #721: (wt=68) 244 [hyper,1,241,241] P(i(i(x,i(y,z)),i(x,i(i(u,y),i(u,z))))).

given clause #722: (wt=21) 9727 [hyper,1,53,860] P(i(n(i(i(i(x,y),z),u)),i(y,z))).

given clause #723: (wt=21) 9728 [hyper,1,52,860] P(i(n(i(i(i(x,i(y,x)),z),u)),z)).

given clause #724: (wt=21) 9736 [hyper,1,860,8976] P(i(n(i(n(i(i(n(n(i(x,y))),z),z)),u)),x)).

given clause #725: (wt=33) 245 [hyper,1,148,241] P(i(x,i(i(y,n(x)),i(y,z)))).

given clause #726: (wt=21) 9751 [hyper,1,860,7684] P(i(n(i(i(i(n(n(x)),x),y),z)),n(n(y)))).

given clause #727: (wt=21) 9752 [hyper,1,860,7683] P(i(n(i(i(n(n(i(x,x))),y),z)),n(n(y)))).

given clause #728: (wt=21) 9760 [hyper,1,860,7669] P(i(n(i(n(i(i(n(x),y),y)),z)),n(n(x)))).

given clause #729: (wt=36) 246 [hyper,1,116,241] P(i(n(i(i(x,y),i(i(z,x),i(z,y)))),u)).

given clause #730: (wt=21) 9769 [hyper,1,860,3773] P(i(n(i(n(i(i(i(n(n(x)),y),z),z)),u)),x)).

given clause #731: (wt=21) 9773 [hyper,1,860,3497] P(i(n(i(n(i(i(i(x,n(y)),z),z)),u)),y)).

given clause #732: (wt=21) 9800 [hyper,1,860,1549] P(i(n(i(n(n(i(i(x,n(n(x))),y))),z)),y)).

given clause #733: (wt=41) 247 [hyper,1,49,241] P(i(x,i(i(y,i(x,z)),i(y,z)))).

given clause #734: (wt=21) 9802 [hyper,1,860,1546] P(i(n(i(n(n(i(n(n(i(n(n(x)),x))),y))),z)),y)).

given clause #735: (wt=21) 9806 [hyper,1,860,1541] P(i(n(i(n(n(i(i(n(i(x,y)),x),z))),u)),z)).

given clause #736: (wt=21) 9820 [hyper,1,860,1454] P(i(n(i(i(i(n(n(x)),x),n(n(y))),z)),y)).

given clause #737: (wt=30) 248 [hyper,1,37,241] P(i(n(x),i(i(y,x),i(y,z)))).

given clause #738: (wt=21) 9822 [hyper,1,860,1452] P(i(n(i(i(n(n(i(x,x))),n(n(y))),z)),y)).

given clause #739: (wt=21) 9835 [hyper,1,860,1126] P(i(n(i(i(i(n(i(x,y)),n(y)),z),u)),z)).

given clause #740: (wt=21) 9838 [hyper,1,860,1071] P(i(n(i(i(i(n(i(n(n(x)),y)),x),z),u)),z)).

given clause #741: (wt=38) 249 [hyper,1,34,241] P(i(i(i(i(x,y),i(i(z,x),i(z,y))),u),u)).

given clause #742: (wt=21) 9842 [hyper,1,860,868] P(i(n(i(i(n(n(i(n(i(x,y)),x))),z),u)),z)).

given clause #743: (wt=21) 9851 [hyper,1,860,673] P(i(n(i(i(i(n(i(x,n(y))),y),z),u)),z)).

given clause #744: (wt=21) 9868 [hyper,1,860,479] P(i(n(i(i(n(n(i(x,n(n(x))))),y),z)),y)).

given clause #745: (wt=53) 250 [hyper,1,29,241] P(i(x,i(i(y,z),i(y,i(u,z))))).

given clause #746: (wt=21) 9869 [hyper,1,860,472] P(i(n(i(i(i(n(i(n(n(x)),x)),y),z),u)),z)).

given clause #747: (wt=21) 9929 [hyper,1,372,9695] P(n(n(i(n(i(n(i(n(i(x,y)),z)),n(y))),u)))).

given clause #748: (wt=21) 9933 [hyper,1,34,9695] P(i(i(i(n(i(n(i(x,y)),z)),n(y)),u),u)).

given clause #749: (wt=35) 251 [hyper,1,26,241] P(i(i(n(x),n(y)),i(i(z,y),i(z,x)))).

given clause #750: (wt=21) 9941 [hyper,1,860,9689] P(i(n(i(n(i(n(i(i(n(x),y),y)),z)),u)),x)).

given clause #751: (wt=21) 9958 [hyper,1,116,9689] P(i(n(i(n(i(n(i(i(n(x),y),y)),z)),x)),u)).

given clause #752: (wt=21) 9965 [hyper,1,860,9702] P(i(n(i(n(i(i(n(n(i(x,x))),y),z)),u)),y)).

given clause #753: (wt=47) 252 [hyper,1,24,241] P(i(i(i(x,y),y),i(i(z,i(y,x)),i(z,x)))).

given clause #754: (wt=21) 9989 [hyper,1,116,9702] P(i(n(i(n(i(i(n(n(i(x,x))),y),z)),y)),u)).

given clause #755: (wt=21) 9998 [hyper,1,860,9703] P(i(n(i(n(i(i(i(n(n(x)),x),y),z)),u)),y)).

given clause #756: (wt=21) 10022 [hyper,1,116,9703] P(i(n(i(n(i(i(i(n(n(x)),x),y),z)),y)),u)).

given clause #757: (wt=68) 253 [hyper,1,21,241] P(i(i(x,y),i(i(z,i(y,u)),i(z,i(x,u))))).

given clause #758: (wt=21) 10039 [hyper,1,367,9688] P(n(n(i(n(i(n(i(i(i(x,y),z),z)),u)),x)))).

given clause #759: (wt=21) 10041 [hyper,1,367,9690] P(n(n(i(n(i(n(i(n(i(x,n(y))),z)),u)),y)))).

given clause #760: (wt=21) 10042 [hyper,1,367,9691] P(n(n(i(n(i(n(i(x,i(y,z))),u)),y)))).

given clause #761: (wt=32) 254 [hyper,1,3,241] P(i(i(i(i(x,y),i(x,z)),u),i(i(y,z),u))).

given clause #762: (wt=21) 10170 [hyper,1,367,9692] P(n(n(i(n(i(n(n(i(i(n(n(x)),x),y))),z)),y)))).

given clause #763: (wt=21) 10206 [hyper,1,367,9693] P(n(n(i(n(i(n(n(i(n(n(i(x,x))),y))),z)),y)))).

given clause #764: (wt=21) 10234 [hyper,1,367,9697] P(n(n(i(n(i(i(i(n(i(x,y)),x),z),u)),z)))).

given clause #765: (wt=65) 255 [hyper,1,2,241] P(i(x,i(i(y,z),i(i(u,y),i(u,z))))).

given clause #766: (wt=21) 10283 [hyper,1,65,239] P(i(n(i(i(n(x),n(y)),x)),i(y,z))).

given clause #767: (wt=21) 10564 [hyper,1,367,9699] P(n(n(i(n(i(i(n(n(i(n(n(x)),x))),y),z)),y)))).

given clause #768: (wt=21) 10601 [hyper,1,367,9701] P(n(n(i(n(i(i(i(x,n(n(x))),y),z)),y)))).

given clause #769: (wt=36) 256 [hyper,1,241,180] P(i(i(x,n(i(n(y),z))),i(x,i(y,u)))).

given clause #770: (wt=21) 10630 [hyper,1,367,9925] P(n(n(i(n(i(n(i(n(i(x,y)),z)),u)),n(y))))).

given clause #771: (wt=22) 941 [hyper,1,382,48] P(i(i(i(i(n(n(x)),y),i(x,y)),z),z)).

given clause #772: (wt=22) 1019 [hyper,1,372,390] P(n(n(i(n(i(i(n(n(x)),y),i(x,y))),z)))).

given clause #773: (wt=40) 257 [hyper,1,241,148] P(i(i(x,i(i(n(y),z),u)),i(x,i(y,u)))).

given clause #774: (wt=22) 1022 [hyper,1,372,380] P(n(n(i(n(i(n(x),n(n(i(x,y))))),z)))).

given clause #775: (wt=22) 1354 [hyper,1,382,60] P(i(i(i(n(x),i(x,y)),z),n(n(z)))).

given clause #776: (wt=22) 1356 [hyper,1,366,60] P(i(i(i(n(x),i(x,y)),n(n(z))),z)).

given clause #777: (wt=42) 258 [hyper,1,241,146] P(i(i(x,y),i(x,i(n(i(z,y)),u)))).

given clause #778: (wt=22) 1428 [hyper,1,116,362] P(i(n(i(i(x,n(n(y))),i(x,y))),z)).

given clause #779: (wt=22) 1515 [hyper,1,116,369] P(i(n(i(i(x,y),i(n(n(x)),y))),z)).

given clause #780: (wt=22) 1555 [hyper,1,369,138] P(i(n(n(i(n(n(x)),n(n(y))))),i(x,y))).

given clause #781: (wt=42) 259 [hyper,1,241,143] P(i(i(x,i(i(y,i(n(y),z)),u)),i(x,u))).

given clause #782: (wt=22) 1569 [hyper,1,369,49] P(i(n(n(i(i(i(x,y),y),z))),i(x,z))).

given clause #783: (wt=22) 1779 [hyper,1,66,138] P(i(i(i(n(x),y),n(n(z))),i(x,z))).

given clause #784: (wt=22) 1821 [hyper,1,116,1548] P(i(n(i(n(n(i(n(n(x)),y))),i(x,y))),z)).

given clause #785: (wt=38) 260 [hyper,1,241,141] P(i(i(x,n(i(y,i(n(y),z)))),i(x,u))).

given clause #786: (wt=22) 1873 [hyper,1,65,340] P(i(n(i(i(x,y),y)),i(n(n(x)),z))).

given clause #787: (wt=22) 3143 [hyper,1,369,547] P(i(n(n(i(n(n(i(n(x),i(x,y)))),z))),z)).

given clause #788: (wt=22) 3144 [hyper,1,367,547] P(n(n(i(i(n(n(i(n(x),i(x,y)))),z),z)))).

given clause #789: (wt=38) 261 [hyper,1,241,114] P(i(i(x,n(i(y,z))),i(x,i(n(z),y)))).

given clause #790: (wt=22) 3166 [hyper,1,369,1011] P(i(n(n(i(n(n(i(n(x),y))),z))),i(x,z))).

given clause #791: (wt=22) 3167 [hyper,1,367,1011] P(n(n(i(i(n(n(i(n(x),y))),z),i(x,z))))).

given clause #792: (wt=22) 3172 [hyper,1,66,1011] P(i(i(i(n(i(n(x),y)),z),u),i(x,u))).

given clause #793: (wt=38) 262 [hyper,1,241,105] P(i(i(x,n(i(n(n(y)),i(z,y)))),i(x,u))).

given clause #794: (wt=22) 3199 [hyper,1,367,1511] P(n(n(i(n(n(i(x,y))),i(n(n(x)),y))))).

given clause #795: (wt=22) 3236 [hyper,1,367,1518] P(n(n(i(n(n(i(i(n(x),i(x,y)),z))),z)))).

given clause #796: (wt=22) 3252 [hyper,1,367,1551] P(n(n(i(n(n(i(x,n(n(y))))),i(x,y))))).

given clause #797: (wt=42) 263 [hyper,1,241,89] P(i(i(x,i(i(y,z),z)),i(x,i(n(z),y)))).

given clause #798: (wt=21) 12406 [hyper,1,941,263] P(i(i(n(n(i(x,y))),y),i(n(y),x))).

given clause #799: (wt=22) 3275 [hyper,1,367,1553] P(n(n(i(n(n(i(i(n(x),y),z))),i(x,z))))).

given clause #800: (wt=22) 3294 [hyper,1,367,2940] P(n(n(i(n(i(n(i(n(x),y)),z)),i(x,u))))).

given clause #801: (wt=42) 264 [hyper,1,241,75] P(i(i(x,i(i(n(n(y)),i(z,y)),u)),i(x,u))).

given clause #802: (wt=22) 3528 [hyper,1,3,379] P(i(i(n(n(i(i(x,y),y))),z),i(x,z))).

given clause #803: (wt=22) 3779 [hyper,1,59,3487] P(i(n(i(i(i(n(x),y),z),z)),i(x,u))).

given clause #804: (wt=22) 3967 [hyper,1,367,3755] P(n(n(i(n(i(i(n(n(x)),y),y)),i(x,z))))).

given clause #805: (wt=34) 265 [hyper,1,241,71] P(i(i(x,n(i(y,z))),i(x,i(z,u)))).

given clause #806: (wt=22) 4199 [hyper,1,117,386] P(i(i(i(n(x),y),y),n(n(i(x,y))))).

given clause #807: (wt=22) 4946 [hyper,1,3,969] P(i(i(i(i(n(n(x)),y),y),z),i(x,z))).

given clause #808: (wt=22) 5579 [hyper,1,3,1524] P(i(i(i(n(n(i(x,y))),y),z),i(x,z))).

given clause #809: (wt=34) 266 [hyper,1,241,70] P(i(i(x,n(i(y,i(z,y)))),i(x,u))).

given clause #810: (wt=22) 5849 [hyper,1,367,5560] P(n(n(i(n(i(n(n(i(x,y))),y)),i(x,z))))).

given clause #811: (wt=22) 6027 [hyper,1,367,6004] P(n(n(i(n(i(n(x),y)),n(n(i(x,y))))))).

given clause #812: (wt=22) 6728 [hyper,1,382,186] P(i(i(i(n(x),y),z),n(n(i(x,z))))).

given clause #813: (wt=36) 267 [hyper,1,241,68] P(i(i(x,n(i(n(y),i(y,z)))),i(x,u))).

given clause #814: (wt=22) 6952 [hyper,1,192,49] P(i(n(i(n(i(i(x,y),y)),z)),i(x,u))).

given clause #815: (wt=22) 6959 [hyper,1,367,6927] P(n(n(i(n(i(n(x),y)),n(n(i(x,z))))))).

given clause #816: (wt=22) 7775 [hyper,1,371,1548] P(i(n(n(i(n(n(x)),y))),n(n(i(x,y))))).

given clause #817: (wt=38) 268 [hyper,1,241,62] P(i(i(x,n(i(y,z))),i(x,i(n(y),u)))).

given clause #818: (wt=21) 13056 [hyper,1,5,7775] P(i(n(i(x,y)),n(i(n(n(x)),y)))).

given clause #819: (wt=22) 7837 [hyper,1,371,369] P(i(i(x,y),n(n(i(n(n(x)),y))))).

given clause #820: (wt=22) 7839 [hyper,1,371,362] P(i(i(x,n(n(y))),n(n(i(x,y))))).

given clause #821: (wt=40) 269 [hyper,1,241,51] P(i(i(x,i(i(n(y),i(y,z)),u)),i(x,u))).

given clause #822: (wt=22) 7842 [hyper,1,371,229] P(i(n(i(i(x,y),y)),n(n(i(x,z))))).

given clause #823: (wt=22) 8349 [hyper,1,367,7835] P(n(n(i(i(n(n(x)),y),n(n(i(x,y))))))).

given clause #824: (wt=22) 9710 [hyper,1,181,860] P(i(n(i(i(i(n(x),y),z),u)),i(x,z))).

given clause #825: (wt=44) 270 [hyper,1,241,49] P(i(i(x,i(i(i(y,z),z),u)),i(x,i(y,u)))).

given clause #826: (wt=22) 9723 [hyper,1,58,860] P(i(n(i(i(i(n(x),i(x,y)),z),u)),z)).

given clause #827: (wt=22) 9801 [hyper,1,860,1548] P(i(n(i(n(n(i(n(n(x)),y))),z)),i(x,y))).

given clause #828: (wt=22) 9877 [hyper,1,860,369] P(i(n(i(i(x,y),z)),i(n(n(x)),y))).

given clause #829: (wt=42) 271 [hyper,1,241,37] P(i(i(x,i(i(y,z),u)),i(x,i(n(y),u)))).

given clause #830: (wt=22) 9879 [hyper,1,860,362] P(i(n(i(i(x,n(n(y))),z)),i(x,y))).

given clause #831: (wt=22) 10885 [hyper,1,367,9872] P(n(n(i(n(i(i(n(n(x)),y),z)),i(x,y))))).

given clause #832: (wt=23) 302 [hyper,1,31,23] P(i(i(i(x,i(y,z)),u),i(z,u))).

given clause #833: (wt=38) 272 [hyper,1,241,34] P(i(i(x,y),i(x,i(i(y,z),z)))).

given clause #834: (wt=23) 316 [hyper,1,3,142] P(i(i(i(n(i(x,y)),z),u),i(n(x),u))).

given clause #835: (wt=23) 373 [hyper,1,146,367] P(i(n(i(x,i(y,n(n(y))))),z)).

given clause #836: (wt=23) 409 [hyper,1,367,76] P(n(n(i(i(i(x,y),z),i(n(n(y)),z))))).

given clause #837: (wt=38) 273 [hyper,1,241,28] P(i(i(x,i(i(y,i(z,y)),u)),i(x,u))).

given clause #838: (wt=23) 411 [hyper,1,367,74] P(n(n(i(n(i(x,y)),i(i(y,x),x))))).

given clause #839: (wt=23) 461 [hyper,1,146,392] P(i(n(i(x,n(n(i(n(n(y)),y))))),z)).

given clause #840: (wt=23) 471 [hyper,1,35,364] P(i(i(i(n(i(n(n(x)),x)),y),z),i(u,z))).

given clause #841: (wt=62) 274 [hyper,1,241,26] P(i(i(x,i(i(y,z),u)),i(x,i(i(n(z),n(y)),u)))).

given clause #842: (wt=23) 474 [hyper,1,2,364] P(i(x,i(n(i(n(n(y)),y)),z))).

given clause #843: (wt=23) 478 [hyper,1,35,370] P(i(i(n(n(i(x,n(n(x))))),y),i(z,y))).

given clause #844: (wt=23) 480 [hyper,1,2,370] P(i(x,n(n(i(y,n(n(y))))))).

given clause #845: (wt=68) 275 [hyper,1,241,24] P(i(i(x,i(i(i(y,z),z),u)),i(x,i(i(i(z,y),y),u)))).

given clause #846: (wt=23) 672 [hyper,1,35,618] P(i(i(i(n(i(x,n(y))),y),z),i(u,z))).

given clause #847: (wt=23) 675 [hyper,1,2,618] P(i(x,i(n(i(y,n(z))),z))).

given clause #848: (wt=23) 850 [hyper,1,146,831] P(i(n(i(x,i(n(i(y,z)),y))),u)).

given clause #849: (wt=38) 276 [hyper,1,241,23] P(i(i(x,i(i(y,z),u)),i(x,i(z,u)))).

given clause #850: (wt=23) 867 [hyper,1,35,848] P(i(i(n(n(i(n(i(x,y)),x))),z),i(u,z))).

given clause #851: (wt=23) 869 [hyper,1,2,848] P(i(x,n(n(i(n(i(y,z)),y))))).

given clause #852: (wt=23) 889 [hyper,1,3,47] P(i(i(i(i(i(x,y),z),z),u),i(y,u))).

given clause #853: (wt=38) 277 [hyper,1,241,5] P(i(i(x,i(n(y),n(z))),i(x,i(z,y)))).

given clause #854: (wt=17) 14575 [hyper,1,277,371] P(i(i(n(x),y),i(n(y),x))).

given clause #855: (wt=14) 14687 [hyper,1,14575,340] P(i(n(i(i(x,y),y)),n(x))).

given clause #856: (wt=15) 14680 [hyper,1,14575,1524] P(i(n(i(n(n(i(n(x),y))),y)),x)).

given clause #857: (wt=50) 278 [hyper,1,241,4] P(i(i(x,i(i(y,z),z)),i(x,i(i(z,y),y)))).

given clause #858: (wt=16) 14704 [hyper,1,367,14687] P(n(n(i(n(i(i(x,y),y)),n(x))))).

given clause #859: (wt=17) 14692 [hyper,1,14575,239] P(i(n(i(i(n(x),n(n(y))),x)),y)).

given clause #860: (wt=17) 14747 [hyper,1,367,14680] P(n(n(i(n(i(n(n(i(n(x),y))),y)),x)))).

given clause #861: (wt=68) 279 [hyper,1,241,3] P(i(i(x,i(y,z)),i(x,i(i(z,u),i(y,u))))).

given clause #862: (wt=18) 14688 [hyper,1,14575,248] P(i(n(i(i(x,y),i(x,z))),y)).

given clause #863: (wt=18) 14699 [hyper,1,860,14687] P(i(n(i(n(i(i(x,y),y)),z)),n(x))).

given clause #864: (wt=18) 14725 [hyper,1,116,14687] P(i(n(i(n(i(i(x,y),y)),n(x))),z)).

given clause #865: (wt=40) 280 [hyper,1,241,229] P(i(i(x,n(i(i(y,z),z))),i(x,i(y,u)))).

given clause #866: (wt=19) 14603 [hyper,1,369,14575] P(i(n(n(i(n(x),y))),i(n(y),x))).

given clause #867: (wt=19) 14604 [hyper,1,367,14575] P(n(n(i(i(n(x),y),i(n(y),x))))).

given clause #868: (wt=19) 14633 [hyper,1,66,14575] P(i(i(i(x,y),z),i(n(z),x))).

given clause #869: (wt=24) 282 [hyper,1,34,229] P(i(i(i(n(i(i(x,y),y)),i(x,z)),u),u)).

given clause #870: (wt=15) 15382 [hyper,1,14633,240] P(i(n(i(i(i(x,y),y),x)),y)).

given clause #871: (wt=17) 15377 [hyper,1,14633,1524] P(i(n(i(n(n(i(i(x,y),z))),z)),x)).

given clause #872: (wt=17) 15389 [hyper,1,14633,133] P(i(n(i(i(i(x,y),z),z)),n(y))).

given clause #873: (wt=31) 283 [hyper,1,3,229] P(i(i(i(x,y),z),i(n(i(i(x,u),u)),z))).

given clause #874: (wt=17) 15390 [hyper,1,14633,123] P(i(n(i(x,i(y,z))),n(z))).

given clause #875: (wt=17) 15411 [hyper,1,367,15382] P(n(n(i(n(i(i(i(x,y),y),x)),y)))).

given clause #876: (wt=19) 14686 [hyper,1,14575,1511] P(i(n(i(n(n(x)),y)),n(i(x,y)))).

given clause #877: (wt=37) 284 [hyper,1,2,229] P(i(x,i(n(i(i(y,z),z)),i(y,u)))).

given clause #878: (wt=19) 14693 [hyper,1,14575,238] P(i(n(i(i(i(i(n(x),y),y),z),z)),x)).

given clause #879: (wt=19) 14696 [hyper,1,14575,35] P(i(n(i(i(n(x),y),i(z,y))),x)).

given clause #880: (wt=19) 14740 [hyper,1,860,14680] P(i(n(i(n(i(n(n(i(n(x),y))),y)),z)),x)).

given clause #881: (wt=25) 285 [hyper,1,143,31] P(i(i(i(x,y),z),i(n(i(y,z)),u))).

given clause #882: (wt=19) 14741 [hyper,1,849,14680] P(i(n(i(n(n(i(n(n(i(x,y))),z))),z)),x)).

given clause #883: (wt=19) 14746 [hyper,1,371,14680] P(i(n(i(n(n(i(n(x),y))),y)),n(n(x)))).

given clause #884: (wt=19) 14796 [hyper,1,116,14680] P(i(n(i(n(i(n(n(i(n(x),y))),y)),x)),z)).

given clause #885: (wt=27) 286 [hyper,1,37,31] P(i(n(i(x,y)),i(i(i(z,x),y),u))).

given clause #886: (wt=19) 15035 [hyper,1,367,14692] P(n(n(i(n(i(i(n(x),n(n(y))),x)),y)))).

given clause #887: (wt=19) 15404 [hyper,1,860,15382] P(i(n(i(n(i(i(i(x,y),y),x)),z)),y)).

given clause #888: (wt=19) 15410 [hyper,1,371,15382] P(i(n(i(i(i(x,y),y),x)),n(n(y)))).

given clause #889: (wt=29) 287 [hyper,1,28,31] P(i(i(i(x,y),z),i(u,i(y,z)))).

given clause #890: (wt=19) 15456 [hyper,1,116,15382] P(i(n(i(n(i(i(i(x,y),y),x)),y)),z)).

given clause #891: (wt=19) 15485 [hyper,1,367,15377] P(n(n(i(n(i(n(n(i(i(x,y),z))),z)),x)))).

given clause #892: (wt=19) 15486 [hyper,1,362,15377] P(i(n(i(n(n(i(i(n(n(x)),y),z))),z)),x)).

given clause #893: (wt=35) 288 [hyper,1,26,31] P(i(i(n(x),n(i(y,z))),i(i(i(u,y),z),x))).

given clause #894: (wt=19) 15519 [hyper,1,367,15389] P(n(n(i(n(i(i(i(x,y),z),z)),n(y))))).

given clause #895: (wt=19) 15558 [hyper,1,367,15390] P(n(n(i(n(i(x,i(y,z))),n(z))))).

given clause #896: (wt=20) 14576 [hyper,1,277,369] P(i(i(x,n(y)),i(y,n(x)))).

given clause #897: (wt=29) 289 [hyper,1,24,31] P(i(i(i(x,y),y),i(i(i(z,y),x),x))).

given clause #898: (wt=20) 14617 [hyper,1,234,14575] P(i(n(x),i(i(n(y),x),y))).

given clause #899: (wt=13) 16171 [hyper,1,14575,14617] P(i(n(i(i(n(x),y),x)),y)).

given clause #900: (wt=15) 16228 [hyper,1,367,16171] P(n(n(i(n(i(i(n(x),y),x)),y)))).

given clause #901: (wt=38) 290 [hyper,1,21,31] P(i(i(x,y),i(i(i(z,y),u),i(x,u)))).

given clause #902: (wt=17) 16222 [hyper,1,860,16171] P(i(n(i(n(i(i(n(x),y),x)),z)),y)).

given clause #903: (wt=17) 16227 [hyper,1,371,16171] P(i(n(i(i(n(x),y),x)),n(n(y)))).

given clause #904: (wt=17) 16265 [hyper,1,116,16171] P(i(n(i(n(i(i(n(x),y),x)),y)),z)).

given clause #905: (wt=35) 291 [hyper,1,31,241] P(i(i(i(x,y),z),i(i(u,y),i(u,z)))).

given clause #906: (wt=19) 16226 [hyper,1,372,16171] P(n(n(i(n(i(n(i(i(n(x),y),x)),y)),z)))).

given clause #907: (wt=19) 16272 [hyper,1,44,16171] P(i(n(i(i(n(x),y),x)),i(z,y))).

given clause #908: (wt=19) 16278 [hyper,1,34,16171] P(i(i(i(n(i(i(n(x),y),x)),y),z),z)).

given clause #909: (wt=25) 292 [hyper,1,31,148] P(i(i(i(x,i(n(y),z)),u),i(y,u))).

given clause #910: (wt=19) 16388 [hyper,1,367,16222] P(n(n(i(n(i(n(i(i(n(x),y),x)),z)),y)))).

given clause #911: (wt=19) 16425 [hyper,1,367,16227] P(n(n(i(n(i(i(n(x),y),x)),n(n(y)))))).

given clause #912: (wt=20) 14703 [hyper,1,372,14687] P(n(n(i(n(i(n(i(i(x,y),y)),n(x))),z)))).

given clause #913: (wt=33) 293 [hyper,1,31,143] P(i(i(i(x,i(y,i(n(y),z))),u),u)).

given clause #914: (wt=20) 14735 [hyper,1,34,14687] P(i(i(i(n(i(i(x,y),y)),n(x)),z),z)).

given clause #915: (wt=20) 15215 [hyper,1,367,14688] P(n(n(i(n(i(i(x,y),i(x,z))),y)))).

given clause #916: (wt=20) 15240 [hyper,1,367,14699] P(n(n(i(n(i(n(i(i(x,y),y)),z)),n(x))))).

given clause #917: (wt=25) 294 [hyper,1,31,89] P(i(i(i(x,i(y,z)),z),i(n(z),y))).

given clause #918: (wt=20) 15284 [hyper,1,14575,14603] P(i(n(i(n(x),y)),n(i(n(y),x)))).

given clause #919: (wt=20) 15379 [hyper,1,14633,251] P(i(n(i(i(x,y),i(x,z))),n(z))).

given clause #920: (wt=20) 15388 [hyper,1,14633,140] P(i(n(i(i(x,y),i(z,y))),n(x))).

given clause #921: (wt=33) 295 [hyper,1,31,75] P(i(i(i(x,i(n(n(y)),i(z,y))),u),u)).

given clause #922: (wt=21) 14493 [hyper,1,277,5560] P(i(n(i(n(n(i(n(x),y))),y)),i(z,x))).

given clause #923: (wt=21) 14593 [hyper,1,7837,14575] P(n(n(i(n(n(i(n(x),y))),i(n(y),x))))).

given clause #924: (wt=21) 14597 [hyper,1,860,14575] P(i(n(i(i(n(x),y),z)),i(n(y),x))).

given clause #925: (wt=31) 296 [hyper,1,31,51] P(i(i(i(x,i(n(y),i(y,z))),u),u)).

given clause #926: (wt=21) 14602 [hyper,1,371,14575] P(i(i(n(x),y),n(n(i(n(y),x))))).

given clause #927: (wt=21) 14625 [hyper,1,186,14575] P(i(i(i(n(n(x)),y),z),i(n(z),x))).

given clause #928: (wt=21) 14630 [hyper,1,116,14575] P(i(n(i(i(n(x),y),i(n(y),x))),z)).

given clause #929: (wt=29) 297 [hyper,1,31,49] P(i(i(i(x,i(i(y,z),z)),u),i(y,u))).

given clause #930: (wt=21) 14646 [hyper,1,31,14575] P(i(i(i(x,n(y)),z),i(n(z),y))).

given clause #931: (wt=19) 16992 [hyper,1,14646,1524] P(i(n(i(n(n(i(i(x,n(y)),z))),z)),y)).

given clause #932: (wt=19) 16993 [hyper,1,14646,969] P(i(n(i(i(n(n(i(x,n(y)))),z),z)),y)).

given clause #933: (wt=25) 298 [hyper,1,31,37] P(i(i(i(x,i(y,z)),u),i(n(y),u))).

given clause #934: (wt=21) 14745 [hyper,1,372,14680] P(n(n(i(n(i(n(i(n(n(i(n(x),y))),y)),x)),z)))).

given clause #935: (wt=21) 14809 [hyper,1,34,14680] P(i(i(i(n(i(n(n(i(n(x),y))),y)),x),z),z)).

given clause #936: (wt=21) 15029 [hyper,1,860,14692] P(i(n(i(n(i(i(n(x),n(n(y))),x)),z)),y)).

given clause #937: (wt=29) 299 [hyper,1,31,34] P(i(i(i(x,y),z),i(i(i(y,z),u),u))).

given clause #938: (wt=21) 15034 [hyper,1,371,14692] P(i(n(i(i(n(x),n(n(y))),x)),n(n(y)))).

given clause #939: (wt=21) 15069 [hyper,1,116,14692] P(i(n(i(n(i(i(n(x),n(n(y))),x)),y)),z)).

given clause #940: (wt=21) 15354 [hyper,1,369,14633] P(i(n(n(i(i(x,y),z))),i(n(z),x))).

given clause #941: (wt=35) 300 [hyper,1,31,26] P(i(i(i(x,i(y,z)),u),i(i(n(z),n(y)),u))).

given clause #942: (wt=21) 15355 [hyper,1,367,14633] P(n(n(i(i(i(x,y),z),i(n(z),x))))).

given clause #943: (wt=21) 15383 [hyper,1,14633,239] P(i(n(i(i(n(x),n(i(y,z))),x)),y)).

given clause #944: (wt=21) 15384 [hyper,1,14633,238] P(i(n(i(i(i(i(i(x,y),z),z),u),u)),x)).

given clause #945: (wt=41) 301 [hyper,1,31,24] P(i(i(i(x,i(i(y,z),z)),u),i(i(i(z,y),y),u))).

given clause #946: (wt=21) 15387 [hyper,1,14633,219] P(i(n(i(n(i(x,i(y,z))),u)),n(z))).

given clause #947: (wt=21) 15392 [hyper,1,14633,47] P(i(n(i(i(i(x,i(y,z)),u),u)),y)).

given clause #948: (wt=21) 15396 [hyper,1,14633,35] P(i(n(i(i(i(x,y),z),i(u,z))),x)).

given clause #949: (wt=29) 304 [hyper,1,31,4] P(i(i(i(x,i(y,z)),z),i(i(z,y),y))).

given clause #950: (wt=21) 15409 [hyper,1,372,15382] P(n(n(i(n(i(n(i(i(i(x,y),y),x)),y)),z)))).

given clause #951: (wt=21) 15466 [hyper,1,44,15382] P(i(n(i(i(i(x,y),y),x)),i(z,y))).

given clause #952: (wt=21) 15472 [hyper,1,34,15382] P(i(i(i(n(i(i(i(x,y),y),x)),y),z),z)).

given clause #953: (wt=35) 305 [hyper,1,31,3] P(i(i(i(x,y),z),i(i(z,u),i(y,u)))).

given clause #954: (wt=21) 15475 [hyper,1,7839,15377] P(n(n(i(n(i(n(n(i(i(n(n(x)),y),z))),z)),x)))).

given clause #955: (wt=21) 15478 [hyper,1,860,15377] P(i(n(i(n(i(n(n(i(i(x,y),z))),z)),u)),x)).

given clause #956: (wt=21) 15479 [hyper,1,849,15377] P(i(n(i(n(n(i(i(n(i(x,y)),z),u))),u)),x)).

given clause #957: (wt=44) 306 [hyper,1,241,138] P(i(i(x,i(n(n(y)),n(n(z)))),i(x,i(y,z)))).

given clause #958: (wt=21) 15484 [hyper,1,371,15377] P(i(n(i(n(n(i(i(x,y),z))),z)),n(n(x)))).

given clause #959: (wt=21) 15504 [hyper,1,116,15377] P(i(n(i(n(i(n(n(i(i(x,y),z))),z)),x)),u)).

given clause #960: (wt=21) 15514 [hyper,1,860,15389] P(i(n(i(n(i(i(i(x,y),z),z)),u)),n(y))).

given clause #961: (wt=45) 307 [hyper,1,146,138] P(i(n(i(x,i(i(n(n(y)),n(n(z))),i(y,z)))),u)).

given clause #962: (wt=21) 15525 [hyper,1,116,15389] P(i(n(i(n(i(i(i(x,y),z),z)),n(y))),u)).

given clause #963: (wt=21) 15564 [hyper,1,116,15390] P(i(n(i(n(i(x,i(y,z))),n(z))),u)).

given clause #964: (wt=21) 15588 [hyper,1,367,14686] P(n(n(i(n(i(n(n(x)),y)),n(i(x,y)))))).

given clause #965: (wt=24) 308 [hyper,1,116,138] P(i(n(i(i(n(n(x)),n(n(y))),i(x,y))),z)).

given clause #966: (wt=21) 15631 [hyper,1,367,14693] P(n(n(i(n(i(i(i(i(n(x),y),y),z),z)),x)))).

given clause #967: (wt=21) 15661 [hyper,1,367,14696] P(n(n(i(n(i(i(n(x),y),i(z,y))),x)))).

given clause #968: (wt=21) 15695 [hyper,1,367,14740] P(n(n(i(n(i(n(i(n(n(i(n(x),y))),y)),z)),x)))).

given clause #969: (wt=26) 309 [hyper,1,34,138] P(i(i(i(i(n(n(x)),n(n(y))),i(x,y)),z),z)).

given clause #970: (wt=21) 15746 [hyper,1,367,14741] P(n(n(i(n(i(n(n(i(n(n(i(x,y))),z))),z)),x)))).

given clause #971: (wt=21) 15747 [hyper,1,362,14741] P(i(n(i(n(n(i(n(n(i(n(n(x)),y))),z))),z)),x)).

given clause #972: (wt=21) 15778 [hyper,1,367,14746] P(n(n(i(n(i(n(n(i(n(x),y))),y)),n(n(x)))))).

given clause #973: (wt=25) 310 [hyper,1,31,138] P(i(i(i(x,n(n(y))),n(n(z))),i(y,z))).

given clause #974: (wt=21) 15845 [hyper,1,367,15404] P(n(n(i(n(i(n(i(i(i(x,y),y),x)),z)),y)))).

given clause #975: (wt=21) 15877 [hyper,1,367,15410] P(n(n(i(n(i(i(i(x,y),y),x)),n(n(y)))))).

given clause #976: (wt=21) 16206 [hyper,1,65,14617] P(i(n(i(i(n(x),y),x)),i(n(y),z))).

given clause #977: (wt=35) 311 [hyper,1,3,138] P(i(i(i(x,y),z),i(i(n(n(x)),n(n(y))),z))).

given clause #978: (wt=21) 16220 [hyper,1,1524,16171] P(i(n(n(i(i(n(i(i(n(x),y),x)),y),z))),z)).

given clause #979: (wt=21) 16221 [hyper,1,969,16171] P(i(i(n(n(i(n(i(i(n(x),y),x)),y))),z),z)).

given clause #980: (wt=21) 16225 [hyper,1,379,16171] P(n(n(i(i(i(n(i(i(n(x),y),x)),y),z),z)))).

given clause #981: (wt=41) 312 [hyper,1,2,138] P(i(x,i(i(n(n(y)),n(n(z))),i(y,z)))).

given clause #982: (wt=21) 16260 [hyper,1,188,16171] P(i(n(i(n(i(n(i(i(n(x),y),x)),y)),z)),u)).

given clause #983: (wt=21) 16380 [hyper,1,860,16222] P(i(n(i(n(i(n(i(i(n(x),y),x)),z)),u)),y)).

given clause #984: (wt=21) 16387 [hyper,1,371,16222] P(i(n(i(n(i(i(n(x),y),x)),z)),n(n(y)))).

given clause #985: (wt=44) 313 [hyper,1,241,142] P(i(i(x,n(y)),i(x,i(n(i(y,z)),u)))).

given clause #986: (wt=21) 16411 [hyper,1,116,16222] P(i(n(i(n(i(n(i(i(n(x),y),x)),z)),y)),u)).

given clause #987: (wt=21) 16445 [hyper,1,116,16227] P(i(n(i(n(i(i(n(x),y),x)),n(n(y)))),z)).

given clause #988: (wt=21) 16499 [hyper,1,367,16272] P(n(n(i(n(i(i(n(x),y),x)),i(z,y))))).

given clause #989: (wt=24) 314 [hyper,1,116,142] P(i(n(i(n(x),i(n(i(x,y)),z))),u)).

given clause #990: (wt=21) 17005 [hyper,1,14646,189] P(i(n(i(i(i(n(i(x,n(y))),z),u),u)),y)).

given clause #991: (wt=21) 17022 [hyper,1,367,16992] P(n(n(i(n(i(n(n(i(i(x,n(y)),z))),z)),y)))).

given clause #992: (wt=21) 17067 [hyper,1,367,16993] P(n(n(i(n(i(i(n(n(i(x,n(y)))),z),z)),y)))).

given clause #993: (wt=26) 315 [hyper,1,34,142] P(i(i(i(n(x),i(n(i(x,y)),z)),u),u)).

given clause #994: (wt=22) 14511 [hyper,1,277,1873] P(i(n(i(i(x,y),y)),i(z,n(x)))).

given clause #995: (wt=22) 14533 [hyper,1,277,1511] P(i(n(n(i(x,n(y)))),i(y,n(x)))).

given clause #996: (wt=22) 14690 [hyper,1,14575,245] P(i(n(i(i(x,n(n(y))),i(x,z))),y)).

given clause #997: (wt=41) 317 [hyper,1,2,142] P(i(x,i(n(y),i(n(i(y,z)),u)))).

given clause #998: (wt=22) 14697 [hyper,1,1524,14687] P(i(n(n(i(i(n(i(i(x,y),y)),n(x)),z))),z)).

given clause #999: (wt=22) 14698 [hyper,1,969,14687] P(i(i(n(n(i(n(i(i(x,y),y)),n(x)))),z),z)).

given clause #1000: (wt=22) 14702 [hyper,1,379,14687] P(n(n(i(i(i(n(i(i(x,y),y)),n(x)),z),z)))).

reducing weight limit to 16.

given clause #1001: (wt=46) 318 [hyper,1,241,74] P(i(i(x,n(i(y,z))),i(x,i(i(z,y),y)))).

given clause #1002: (wt=22) 14720 [hyper,1,188,14687] P(i(n(i(n(i(n(i(i(x,y),y)),n(x))),z)),u)).

given clause #1003: (wt=22) 14800 [hyper,1,59,14680] P(i(n(i(n(n(i(n(n(x)),y))),y)),i(x,z))).

given clause #1004: (wt=22) 15208 [hyper,1,860,14688] P(i(n(i(n(i(i(x,y),i(x,z))),u)),y)).

given clause #1005: (wt=47) 319 [hyper,1,146,74] P(i(n(i(x,i(n(i(y,z)),i(i(z,y),y)))),u)).

given clause #1006: (wt=22) 15214 [hyper,1,371,14688] P(i(n(i(i(x,y),i(x,z))),n(n(y)))).

given clause #1007: (wt=22) 15226 [hyper,1,116,14688] P(i(n(i(n(i(i(x,y),i(x,z))),y)),u)).

given clause #1008: (wt=22) 15235 [hyper,1,860,14699] P(i(n(i(n(i(n(i(i(x,y),y)),z)),u)),n(x))).

given clause #1009: (wt=25) 320 [hyper,1,116,74] P(i(n(i(n(i(x,y)),i(i(y,x),x))),z)).

given clause #1010: (wt=22) 15245 [hyper,1,116,14699] P(i(n(i(n(i(n(i(i(x,y),y)),z)),n(x))),u)).

given clause #1011: (wt=22) 15983 [hyper,1,367,14576] P(n(n(i(i(x,n(y)),i(y,n(x)))))).

given clause #1012: (wt=22) 16180 [hyper,1,367,14617] P(n(n(i(n(x),i(i(n(y),x),y))))).

given clause #1013: (wt=27) 321 [hyper,1,34,74] P(i(i(i(n(i(x,y)),i(i(y,x),x)),z),z)).

given clause #1014: (wt=22) 16639 [hyper,1,367,15284] P(n(n(i(n(i(n(x),y)),n(i(n(y),x)))))).

given clause #1015: (wt=22) 16681 [hyper,1,367,15388] P(n(n(i(n(i(i(x,y),i(z,y))),n(x))))).

given clause #1016: (wt=23) 979 [hyper,1,390,388] P(i(x,n(n(i(y,n(n(x))))))).

given clause #1017: (wt=28) 322 [hyper,1,3,74] P(i(i(i(i(x,y),y),z),i(n(i(y,x)),z))).

given clause #1018: (wt=23) 985 [hyper,1,372,372] P(n(n(i(n(i(x,n(n(i(n(x),y))))),z)))).

given clause #1019: (wt=23) 995 [hyper,1,46,372] P(n(n(i(n(i(x,i(i(x,y),y))),z)))).

given clause #1020: (wt=23) 1003 [hyper,1,34,372] P(i(i(i(x,n(n(i(n(x),y)))),z),z)).

given clause #1021: (wt=43) 323 [hyper,1,2,74] P(i(x,i(n(i(y,z)),i(i(z,y),y)))).

given clause #1022: (wt=23) 1008 [hyper,1,23,372] P(i(x,n(n(i(n(i(y,x)),z))))).

given clause #1023: (wt=23) 1030 [hyper,1,372,141] P(n(n(i(n(i(n(i(x,i(n(x),y))),z)),u)))).

given clause #1024: (wt=23) 1032 [hyper,1,372,105] P(n(n(i(n(i(n(i(n(n(x)),i(y,x))),z)),u)))).

given clause #1025: (wt=46) 324 [hyper,1,241,76] P(i(i(x,i(i(y,z),u)),i(x,i(n(n(z)),u)))).

given clause #1026: (wt=23) 1036 [hyper,1,372,62] P(n(n(i(n(i(n(i(x,y)),i(n(x),z))),u)))).

given clause #1027: (wt=23) 1046 [hyper,1,372,28] P(n(n(i(n(i(i(i(x,i(y,x)),z),z)),u)))).

given clause #1028: (wt=23) 1051 [hyper,1,372,23] P(n(n(i(n(i(i(i(x,y),z),i(y,z))),u)))).

given clause #1029: (wt=25) 326 [hyper,1,116,76] P(i(n(i(i(i(x,y),z),i(n(n(y)),z))),u)).

given clause #1030: (wt=23) 1053 [hyper,1,372,5] P(n(n(i(n(i(i(n(x),n(y)),i(y,x))),z)))).

given clause #1031: (wt=23) 1070 [hyper,1,35,1010] P(i(i(i(n(i(n(n(x)),y)),x),z),i(u,z))).

given clause #1032: (wt=23) 1073 [hyper,1,2,1010] P(i(x,i(n(i(n(n(y)),z)),y))).

given clause #1033: (wt=27) 329 [hyper,1,34,76] P(i(i(i(i(i(x,y),z),i(n(n(y)),z)),u),u)).

given clause #1034: (wt=23) 1092 [hyper,1,372,376] P(n(n(i(n(i(n(n(x)),n(n(i(y,x))))),z)))).

given clause #1035: (wt=23) 1105 [hyper,1,34,376] P(i(i(i(n(n(x)),n(n(i(y,x)))),z),z)).

given clause #1036: (wt=23) 1107 [hyper,1,3,376] P(i(i(n(n(i(x,y))),z),i(n(n(y)),z))).

given clause #1037: (wt=27) 330 [hyper,1,31,76] P(i(i(i(x,i(y,z)),u),i(n(n(z)),u))).

given clause #1038: (wt=23) 1125 [hyper,1,35,1106] P(i(i(i(n(i(x,y)),n(y)),z),i(u,z))).

given clause #1039: (wt=23) 1127 [hyper,1,3,1106] P(i(i(n(x),y),i(n(i(z,x)),y))).

given clause #1040: (wt=23) 1128 [hyper,1,2,1106] P(i(x,i(n(i(y,z)),n(z)))).

given clause #1041: (wt=51) 331 [hyper,1,29,76] P(i(x,i(n(n(y)),i(z,i(u,y))))).

given clause #1042: (wt=23) 1147 [hyper,1,34,412] P(i(i(n(n(i(n(i(x,y)),i(y,z)))),u),u)).

given clause #1043: (wt=23) 1150 [hyper,1,34,413] P(i(i(n(n(i(n(i(x,i(y,x))),z))),u),u)).

given clause #1044: (wt=23) 1152 [hyper,1,372,472] P(n(n(i(n(i(i(i(n(i(n(n(x)),x)),y),z),z)),u)))).

given clause #1045: (wt=25) 332 [hyper,1,28,76] P(i(n(n(x)),i(y,i(z,x)))).

given clause #1046: (wt=23) 1156 [hyper,1,34,472] P(i(i(i(i(i(n(i(n(n(x)),x)),y),z),z),u),u)).

given clause #1047: (wt=23) 1164 [hyper,1,372,476] P(n(n(i(n(i(n(i(n(i(x,n(n(x)))),y)),z)),u)))).

given clause #1048: (wt=23) 1166 [hyper,1,34,476] P(i(i(i(n(i(n(i(x,n(n(x)))),y)),z),u),u)).

given clause #1049: (wt=27) 333 [hyper,1,26,76] P(i(i(n(x),n(i(y,z))),i(n(n(z)),x))).

given clause #1050: (wt=23) 1170 [hyper,1,372,479] P(n(n(i(n(i(i(n(n(i(x,n(n(x))))),y),y)),z)))).

given clause #1051: (wt=23) 1183 [hyper,1,34,479] P(i(i(i(i(n(n(i(x,n(n(x))))),y),y),z),z)).

given clause #1052: (wt=23) 1187 [hyper,1,372,485] P(n(n(i(n(i(n(i(i(i(n(n(x)),x),y),y)),z)),u)))).

given clause #1053: (wt=31) 334 [hyper,1,3,76] P(i(i(i(n(n(x)),y),z),i(i(i(u,x),y),z))).

given clause #1054: (wt=23) 1189 [hyper,1,34,485] P(i(i(i(n(i(i(i(n(n(x)),x),y),y)),z),u),u)).

given clause #1055: (wt=23) 1203 [hyper,1,372,530] P(n(n(i(n(i(n(i(i(n(n(i(x,x))),y),y)),z)),u)))).

given clause #1056: (wt=23) 1205 [hyper,1,34,530] P(i(i(i(n(i(i(n(n(i(x,x))),y),y)),z),u),u)).

given clause #1057: (wt=43) 335 [hyper,1,2,76] P(i(x,i(i(i(y,z),u),i(n(n(z)),u)))).

given clause #1058: (wt=23) 1210 [hyper,1,142,550] P(i(n(i(n(i(x,i(n(n(y)),y))),z)),u)).

given clause #1059: (wt=23) 1214 [hyper,1,34,550] P(i(i(n(n(i(x,i(n(n(y)),y)))),z),z)).

given clause #1060: (wt=23) 1218 [hyper,1,142,579] P(i(n(i(n(i(i(i(x,n(n(x))),y),y)),z)),u)).

given clause #1061: (wt=33) 336 [hyper,1,76,146] P(i(n(n(x)),i(n(i(y,i(z,x))),u))).

given clause #1062: (wt=23) 1222 [hyper,1,34,579] P(i(i(n(n(i(i(i(x,n(n(x))),y),y))),z),z)).

given clause #1063: (wt=23) 1234 [hyper,1,372,590] P(n(n(i(n(i(i(i(n(n(x)),x),x),n(n(x)))),y)))).

given clause #1064: (wt=23) 1247 [hyper,1,34,590] P(i(i(i(i(i(n(n(x)),x),x),n(n(x))),y),y)).

given clause #1065: (wt=25) 339 [hyper,1,76,34] P(i(n(n(x)),i(i(i(y,x),z),z))).

given clause #1066: (wt=23) 1254 [hyper,1,142,593] P(i(n(i(n(i(x,n(n(i(y,y))))),z)),u)).

given clause #1067: (wt=23) 1258 [hyper,1,34,593] P(i(i(n(n(i(x,n(n(i(y,y)))))),z),z)).

given clause #1068: (wt=23) 1262 [hyper,1,142,596] P(i(n(i(n(i(x,n(n(i(y,x))))),z)),u)).

given clause #1069: (wt=31) 341 [hyper,1,76,3] P(i(n(n(x)),i(i(x,y),i(z,y)))).

given clause #1070: (wt=23) 1266 [hyper,1,34,596] P(i(i(n(n(i(x,n(n(i(y,x)))))),z),z)).

given clause #1071: (wt=23) 1271 [hyper,1,372,673] P(n(n(i(n(i(i(i(n(i(x,n(y))),y),z),z)),u)))).

given clause #1072: (wt=23) 1275 [hyper,1,34,673] P(i(i(i(i(i(n(i(x,n(y))),y),z),z),u),u)).

given clause #1073: (wt=62) 342 [hyper,1,241,35] P(i(i(x,y),i(x,i(i(y,z),i(u,z))))).

given clause #1074: (wt=23) 1281 [hyper,1,34,723] P(i(i(n(n(i(n(i(n(i(n(n(x)),x)),y)),z))),u),u)).

given clause #1075: (wt=23) 1284 [hyper,1,372,739] P(n(n(i(n(i(n(i(x,n(y))),i(z,y))),u)))).

given clause #1076: (wt=23) 1290 [hyper,1,34,739] P(i(i(i(n(i(x,n(y))),i(z,y)),u),u)).

given clause #1077: (wt=37) 343 [hyper,1,148,35] P(i(x,i(i(i(n(x),y),z),i(u,z)))).

given clause #1078: (wt=23) 1298 [hyper,1,142,759] P(i(n(i(n(i(i(n(n(i(n(n(x)),x))),y),y)),z)),u)).

given clause #1079: (wt=23) 1302 [hyper,1,34,759] P(i(i(n(n(i(i(n(n(i(n(n(x)),x))),y),y))),z),z)).

given clause #1080: (wt=23) 1305 [hyper,1,34,814] P(i(i(n(n(i(n(i(n(i(x,n(y))),y)),z))),u),u)).

given clause #1081: (wt=25) 344 [hyper,1,143,35] P(i(i(i(x,i(n(x),y)),z),i(u,z))).

given clause #1082: (wt=23) 1322 [hyper,1,59,859] P(i(i(i(n(i(x,y)),x),n(z)),i(z,u))).

given clause #1083: (wt=23) 1327 [hyper,1,59,465] P(i(i(n(n(i(n(n(x)),x))),n(y)),i(y,z))).

given clause #1084: (wt=23) 1329 [hyper,1,59,382] P(i(i(i(x,n(n(x))),n(y)),i(y,z))).

given clause #1085: (wt=33) 345 [hyper,1,116,35] P(i(n(i(x,i(i(x,y),i(z,y)))),u)).

given clause #1086: (wt=23) 1337 [hyper,1,372,868] P(n(n(i(n(i(i(n(n(i(n(i(x,y)),x))),z),z)),u)))).

given clause #1087: (wt=23) 1342 [hyper,1,34,868] P(i(i(i(i(n(n(i(n(i(x,y)),x))),z),z),u),u)).

given clause #1088: (wt=23) 1346 [hyper,1,34,919] P(i(i(n(n(i(n(i(x,y)),i(z,x)))),u),u)).

given clause #1089: (wt=37) 346 [hyper,1,76,35] P(i(n(n(x)),i(i(i(y,x),z),i(u,z)))).

given clause #1090: (wt=23) 1349 [hyper,1,34,928] P(i(i(n(n(i(i(i(n(i(x,y)),x),z),z))),u),u)).

given clause #1091: (wt=23) 1386 [hyper,1,34,1057] P(i(i(n(n(i(n(i(n(i(n(n(x)),y)),x)),z))),u),u)).

given clause #1092: (wt=23) 1389 [hyper,1,372,1065] P(n(n(i(n(i(n(i(n(n(x)),y)),i(z,x))),u)))).

given clause #1093: (wt=25) 347 [hyper,1,75,35] P(i(i(i(n(n(x)),i(y,x)),z),i(u,z))).

given clause #1094: (wt=23) 1395 [hyper,1,34,1065] P(i(i(i(n(i(n(n(x)),y)),i(z,x)),u),u)).

given clause #1095: (wt=23) 1399 [hyper,1,372,1071] P(n(n(i(n(i(i(i(n(i(n(n(x)),y)),x),z),z)),u)))).

given clause #1096: (wt=23) 1404 [hyper,1,34,1071] P(i(i(i(i(i(n(i(n(n(x)),y)),x),z),z),u),u)).

given clause #1097: (wt=24) 348 [hyper,1,51,35] P(i(i(i(n(x),i(x,y)),z),i(u,z))).

given clause #1098: (wt=23) 1410 [hyper,1,34,1113] P(i(i(n(n(i(n(i(n(i(x,y)),n(y))),z))),u),u)).

given clause #1099: (wt=23) 1413 [hyper,1,372,1126] P(n(n(i(n(i(i(i(n(i(x,y)),n(y)),z),z)),u)))).

given clause #1100: (wt=23) 1418 [hyper,1,34,1126] P(i(i(i(i(i(n(i(x,y)),n(y)),z),z),u),u)).

given clause #1101: (wt=41) 349 [hyper,1,49,35] P(i(x,i(i(i(i(x,y),y),z),i(u,z)))).

given clause #1102: (wt=23) 1455 [hyper,1,362,143] P(i(i(i(x,i(n(x),y)),n(n(z))),z)).

given clause #1103: (wt=23) 1456 [hyper,1,362,75] P(i(i(i(n(n(x)),i(y,x)),n(n(z))),z)).

given clause #1104: (wt=23) 1470 [hyper,1,372,1452] P(n(n(i(n(i(i(n(n(i(x,x))),n(n(y))),y)),z)))).

given clause #1105: (wt=36) 350 [hyper,1,37,35] P(i(n(x),i(i(i(x,y),z),i(u,z)))).

given clause #1106: (wt=23) 1479 [hyper,1,44,1452] P(i(i(n(n(i(x,x))),n(n(y))),i(z,y))).

given clause #1107: (wt=23) 1485 [hyper,1,34,1452] P(i(i(i(i(n(n(i(x,x))),n(n(y))),y),z),z)).

given clause #1108: (wt=23) 1490 [hyper,1,372,1454] P(n(n(i(n(i(i(i(n(n(x)),x),n(n(y))),y)),z)))).

given clause #1109: (wt=35) 351 [hyper,1,34,35] P(i(i(i(x,i(i(x,y),i(z,y))),u),u)).

given clause #1110: (wt=23) 1499 [hyper,1,44,1454] P(i(i(i(n(n(x)),x),n(n(y))),i(z,y))).

given clause #1111: (wt=23) 1505 [hyper,1,34,1454] P(i(i(i(i(i(n(n(x)),x),n(n(y))),y),z),z)).

given clause #1112: (wt=23) 1557 [hyper,1,369,76] P(i(n(n(i(i(x,y),z))),i(n(n(y)),z))).

given clause #1113: (wt=41) 352 [hyper,1,26,35] P(i(i(n(x),n(y)),i(i(i(y,x),z),i(u,z)))).

given clause #1114: (wt=23) 1600 [hyper,1,59,1547] P(i(n(n(i(n(n(i(x,x))),n(y)))),i(y,z))).

given clause #1115: (wt=23) 1621 [hyper,1,59,1550] P(i(n(n(i(i(n(n(x)),x),n(y)))),i(y,z))).

given clause #1116: (wt=23) 1636 [hyper,1,372,1541] P(n(n(i(n(i(n(n(i(i(n(i(x,y)),x),z))),z)),u)))).

given clause #1117: (wt=47) 353 [hyper,1,24,35] P(i(i(i(x,y),y),i(i(i(i(y,x),x),z),i(u,z)))).

given clause #1118: (wt=23) 1642 [hyper,1,44,1541] P(i(n(n(i(i(n(i(x,y)),x),z))),i(u,z))).

given clause #1119: (wt=23) 1643 [hyper,1,34,1541] P(i(i(i(n(n(i(i(n(i(x,y)),x),z))),z),u),u)).

given clause #1120: (wt=23) 1674 [hyper,1,65,853] P(i(n(i(x,y)),i(n(i(y,z)),u))).

given clause #1121: (wt=35) 354 [hyper,1,23,35] P(i(x,i(i(i(y,x),z),i(u,z)))).

given clause #1122: (wt=23) 1683 [hyper,1,65,369] P(i(n(i(n(n(x)),y)),i(i(x,y),z))).

given clause #1123: (wt=23) 1697 [hyper,1,65,71] P(i(n(i(x,y)),i(n(i(z,x)),u))).

given clause #1124: (wt=23) 1698 [hyper,1,65,64] P(i(n(i(x,i(y,z))),i(n(y),u))).

given clause #1125: (wt=26) 355 [hyper,1,3,35] P(i(i(i(i(x,y),i(z,y)),u),i(x,u))).

given clause #1126: (wt=23) 1712 [hyper,1,372,1546] P(n(n(i(n(i(n(n(i(n(n(i(n(n(x)),x))),y))),y)),z)))).

given clause #1127: (wt=23) 1724 [hyper,1,44,1546] P(i(n(n(i(n(n(i(n(n(x)),x))),y))),i(z,y))).

given clause #1128: (wt=23) 1730 [hyper,1,34,1546] P(i(i(i(n(n(i(n(n(i(n(n(x)),x))),y))),y),z),z)).

given clause #1129: (wt=59) 356 [hyper,1,2,35] P(i(x,i(y,i(i(y,z),i(u,z))))).

given clause #1130: (wt=23) 1735 [hyper,1,372,1549] P(n(n(i(n(i(n(n(i(i(x,n(n(x))),y))),y)),z)))).

given clause #1131: (wt=23) 1747 [hyper,1,44,1549] P(i(n(n(i(i(x,n(n(x))),y))),i(z,y))).

given clause #1132: (wt=23) 1753 [hyper,1,34,1549] P(i(i(i(n(n(i(i(x,n(n(x))),y))),y),z),z)).

given clause #1133: (wt=32) 357 [hyper,1,35,138] P(i(i(i(i(n(n(x)),n(n(y))),i(x,y)),z),i(u,z))).

given clause #1134: (wt=23) 1759 [hyper,1,142,1595] P(i(n(i(n(i(n(n(i(n(n(i(x,x))),y))),y)),z)),u)).

given clause #1135: (wt=23) 1764 [hyper,1,34,1595] P(i(i(n(n(i(n(n(i(n(n(i(x,x))),y))),y))),z),z)).

given clause #1136: (wt=23) 1766 [hyper,1,382,66] P(i(i(i(x,y),z),n(n(i(n(x),z))))).

given clause #1137: (wt=29) 358 [hyper,1,35,114] P(i(i(i(n(i(x,y)),i(n(y),x)),z),i(u,z))).

given clause #1138: (wt=23) 1777 [hyper,1,66,362] P(i(i(i(x,y),n(n(z))),i(n(x),z))).

given clause #1139: (wt=23) 1785 [hyper,1,142,1616] P(i(n(i(n(i(n(n(i(i(n(n(x)),x),y))),y)),z)),u)).

given clause #1140: (wt=23) 1790 [hyper,1,34,1616] P(i(i(n(n(i(n(n(i(i(n(n(x)),x),y))),y))),z),z)).

given clause #1141: (wt=31) 359 [hyper,1,35,89] P(i(i(i(i(i(x,y),y),i(n(y),x)),z),i(u,z))).

given clause #1142: (wt=23) 1841 [hyper,1,65,69] P(i(n(i(i(i(x,y),z),z)),i(n(x),u))).

given clause #1143: (wt=23) 1860 [hyper,1,116,328] P(i(n(i(n(i(x,y)),i(n(n(y)),z))),u)).

given clause #1144: (wt=23) 1872 [hyper,1,116,340] P(i(n(i(n(n(x)),i(i(x,y),y))),z)).

given clause #1145: (wt=33) 360 [hyper,1,35,74] P(i(i(i(n(i(x,y)),i(i(y,x),x)),z),i(u,z))).

given clause #1146: (wt=23) 1895 [hyper,1,116,365] P(i(n(i(i(i(n(n(x)),x),y),i(z,y))),u)).

given clause #1147: (wt=23) 1934 [hyper,1,369,78] P(i(n(n(i(i(n(i(x,i(y,x))),z),u))),u)).

given clause #1148: (wt=23) 1935 [hyper,1,367,78] P(n(n(i(i(i(n(i(x,i(y,x))),z),u),u)))).

given clause #1149: (wt=29) 361 [hyper,1,35,34] P(i(i(i(x,i(i(x,y),y)),z),i(u,z))).

given clause #1150: (wt=23) 1972 [hyper,1,116,439] P(i(n(i(i(n(n(i(x,x))),y),i(z,y))),u)).

given clause #1151: (wt=23) 1989 [hyper,1,362,488] P(i(i(i(i(i(n(n(x)),x),y),y),n(n(z))),z)).

given clause #1152: (wt=23) 1991 [hyper,1,116,488] P(i(n(i(i(i(i(i(n(n(x)),x),y),y),z),z)),u)).

given clause #1153: (wt=27) 384 [hyper,1,29,367] P(i(x,n(n(i(y,i(z,y)))))).

given clause #1154: (wt=23) 2003 [hyper,1,116,491] P(i(n(i(i(i(x,n(n(x))),n(n(x))),x)),y)).

given clause #1155: (wt=23) 2032 [hyper,1,362,499] P(i(i(i(n(i(x,n(n(x)))),y),n(n(z))),z)).

given clause #1156: (wt=23) 2034 [hyper,1,116,499] P(i(n(i(i(i(n(i(x,n(n(x)))),y),z),z)),u)).

given clause #1157: (wt=27) 387 [hyper,1,24,367] P(i(i(i(x,y),y),n(n(i(i(y,x),x))))).

given clause #1158: (wt=23) 2046 [hyper,1,362,505] P(i(i(n(n(i(x,i(y,x)))),n(n(z))),z)).

given clause #1159: (wt=23) 2048 [hyper,1,116,505] P(i(n(i(i(n(n(i(x,i(y,x)))),z),z)),u)).

given clause #1160: (wt=23) 2058 [hyper,1,362,534] P(i(i(i(i(n(n(i(x,x))),y),y),n(n(z))),z)).

given clause #1161: (wt=36) 389 [hyper,1,21,367] P(i(i(x,y),n(n(i(i(y,z),i(x,z)))))).

given clause #1162: (wt=23) 2060 [hyper,1,116,534] P(i(n(i(i(i(i(n(n(i(x,x))),y),y),z),z)),u)).

given clause #1163: (wt=23) 2075 [hyper,1,362,542] P(i(i(n(n(i(n(i(n(n(x)),x)),y))),n(n(z))),z)).

given clause #1164: (wt=23) 2077 [hyper,1,116,542] P(i(n(i(i(n(n(i(n(i(n(n(x)),x)),y))),z),z)),u)).

given clause #1165: (wt=34) 393 [hyper,1,367,241] P(n(n(i(i(x,y),i(i(z,x),i(z,y)))))).

given clause #1166: (wt=23) 2102 [hyper,1,116,601] P(i(n(i(x,i(y,n(n(x))))),z)).

given clause #1167: (wt=23) 2200 [hyper,1,116,619] P(i(n(i(i(n(n(i(x,y))),z),i(y,z))),u)).

given clause #1168: (wt=23) 2235 [hyper,1,362,715] P(i(i(n(n(i(n(i(x,n(y))),y))),n(n(z))),z)).

given clause #1169: (wt=31) 420 [hyper,1,367,35] P(n(n(i(x,i(i(x,y),i(z,y)))))).

given clause #1170: (wt=23) 2237 [hyper,1,116,715] P(i(n(i(i(n(n(i(n(i(x,n(y))),y))),z),z)),u)).

given clause #1171: (wt=23) 2367 [hyper,1,362,872] P(i(i(i(n(i(n(i(x,y)),x)),z),n(n(u))),u)).

given clause #1172: (wt=23) 2408 [hyper,1,362,1083] P(i(i(n(n(i(n(i(n(n(x)),y)),x))),n(n(z))),z)).

given clause #1173: (wt=37) 422 [hyper,1,367,32] P(n(n(i(x,i(i(i(y,z),u),i(z,u)))))).

given clause #1174: (wt=23) 2410 [hyper,1,116,1083] P(i(n(i(i(n(n(i(n(i(n(n(x)),y)),x))),z),z)),u)).

given clause #1175: (wt=23) 2448 [hyper,1,116,1121] P(i(n(i(n(i(x,y)),i(z,n(y)))),u)).

given clause #1176: (wt=23) 2460 [hyper,1,362,1135] P(i(i(n(n(i(n(i(x,y)),n(y)))),n(n(z))),z)).

given clause #1177: (wt=31) 423 [hyper,1,367,31] P(n(n(i(i(i(x,y),z),i(i(i(u,x),y),z))))).

given clause #1178: (wt=23) 2462 [hyper,1,116,1135] P(i(n(i(i(n(n(i(n(i(x,y)),n(y)))),z),z)),u)).

given clause #1179: (wt=23) 2521 [hyper,1,116,1307] P(i(n(i(n(i(x,n(n(y)))),i(y,z))),u)).

given clause #1180: (wt=23) 2529 [hyper,1,369,93] P(i(n(n(i(i(n(i(x,y)),i(y,z)),u))),u)).

given clause #1181: (wt=49) 424 [hyper,1,367,30] P(n(n(i(x,i(y,i(z,i(u,z))))))).

given clause #1182: (wt=23) 2530 [hyper,1,367,93] P(n(n(i(i(i(n(i(x,y)),i(y,z)),u),u)))).

given clause #1183: (wt=23) 2553 [hyper,1,94,148] P(i(n(i(x,i(n(y),z))),i(y,u))).

given clause #1184: (wt=23) 2557 [hyper,1,94,89] P(i(n(i(x,i(y,z))),i(n(z),y))).

given clause #1185: (wt=25) 425 [hyper,1,367,29] P(n(n(i(i(i(x,i(y,x)),z),i(u,z))))).

given clause #1186: (wt=23) 2570 [hyper,1,116,1447] P(i(n(i(i(i(n(i(x,y)),x),n(n(z))),z)),u)).

given clause #1187: (wt=23) 2585 [hyper,1,116,1451] P(i(n(i(i(n(n(i(n(n(x)),x))),n(n(y))),y)),z)).

given clause #1188: (wt=23) 2609 [hyper,1,116,1453] P(i(n(i(i(i(x,n(n(x))),n(n(y))),y)),z)).

given clause #1189: (wt=37) 427 [hyper,1,367,27] P(n(n(i(x,i(i(n(y),n(z)),i(z,y)))))).

given clause #1190: (wt=23) 2655 [hyper,1,116,1521] P(i(n(i(n(n(i(n(x),n(y)))),i(y,x))),z)).

given clause #1191: (wt=23) 2676 [hyper,1,116,1522] P(i(n(i(n(n(i(i(x,y),z))),i(y,z))),u)).

given clause #1192: (wt=23) 2688 [hyper,1,362,1523] P(i(n(n(i(i(x,i(y,x)),n(n(z))))),z)).

given clause #1193: (wt=31) 428 [hyper,1,367,26] P(n(n(i(i(i(x,y),z),i(i(n(y),n(x)),z))))).

given clause #1194: (wt=23) 2690 [hyper,1,116,1523] P(i(n(i(n(n(i(i(x,i(y,x)),z))),z)),u)).

given clause #1195: (wt=23) 2704 [hyper,1,116,1536] P(i(n(i(n(n(i(i(n(n(x)),x),n(n(y))))),y)),z)).

given clause #1196: (wt=23) 2726 [hyper,1,116,1537] P(i(n(i(n(n(i(n(n(i(x,x))),n(n(y))))),y)),z)).

given clause #1197: (wt=49) 429 [hyper,1,367,25] P(n(n(i(x,i(i(i(y,z),z),i(i(z,y),y)))))).

given clause #1198: (wt=23) 2746 [hyper,1,362,1538] P(i(n(n(i(i(n(i(x,y)),n(y)),n(n(z))))),z)).

given clause #1199: (wt=23) 2748 [hyper,1,116,1538] P(i(n(i(n(n(i(i(n(i(x,y)),n(y)),z))),z)),u)).

given clause #1200: (wt=23) 2762 [hyper,1,362,1539] P(i(n(n(i(i(n(i(n(n(x)),y)),x),n(n(z))))),z)).

given clause #1201: (wt=34) 430 [hyper,1,367,24] P(n(n(i(i(i(i(x,y),y),z),i(i(i(y,x),x),z))))).

given clause #1202: (wt=23) 2764 [hyper,1,116,1539] P(i(n(i(n(n(i(i(n(i(n(n(x)),y)),x),z))),z)),u)).

given clause #1203: (wt=23) 2776 [hyper,1,362,1540] P(i(n(n(i(n(n(i(n(i(x,y)),x))),n(n(z))))),z)).

given clause #1204: (wt=23) 2778 [hyper,1,116,1540] P(i(n(i(n(n(i(n(n(i(n(i(x,y)),x))),z))),z)),u)).

given clause #1205: (wt=67) 432 [hyper,1,367,22] P(n(n(i(x,i(i(y,z),i(i(z,u),i(y,u))))))).

given clause #1206: (wt=23) 2790 [hyper,1,362,1542] P(i(n(n(i(i(n(i(x,n(y))),y),n(n(z))))),z)).

given clause #1207: (wt=23) 2792 [hyper,1,116,1542] P(i(n(i(n(n(i(i(n(i(x,n(y))),y),z))),z)),u)).

given clause #1208: (wt=23) 2812 [hyper,1,116,1543] P(i(n(i(n(n(i(i(n(n(x)),x),x))),n(n(x)))),y)).

given clause #1209: (wt=34) 433 [hyper,1,367,21] P(n(n(i(i(i(i(x,y),i(z,y)),u),i(i(z,x),u))))).

given clause #1210: (wt=23) 2814 [hyper,1,59,1543] P(i(n(n(i(i(n(n(x)),x),x))),i(n(x),y))).

given clause #1211: (wt=23) 2831 [hyper,1,362,1544] P(i(n(n(i(n(n(i(x,n(n(x))))),n(n(y))))),y)).

given clause #1212: (wt=23) 2834 [hyper,1,116,1544] P(i(n(i(n(n(i(n(n(i(x,n(n(x))))),y))),y)),z)).

given clause #1213: (wt=25) 434 [hyper,1,367,20] P(n(n(i(x,i(y,i(z,y)))))).

given clause #1214: (wt=23) 2856 [hyper,1,362,1545] P(i(n(n(i(i(n(i(n(n(x)),x)),y),n(n(z))))),z)).

given clause #1215: (wt=23) 2858 [hyper,1,116,1545] P(i(n(i(n(n(i(i(n(i(n(n(x)),x)),y),z))),z)),u)).

given clause #1216: (wt=23) 2917 [hyper,1,116,1771] P(i(n(i(i(i(x,y),n(z)),i(z,x))),u)).

given clause #1217: (wt=25) 436 [hyper,1,367,4] P(n(n(i(i(i(x,y),y),i(i(y,x),x))))).

given clause #1218: (wt=23) 2983 [hyper,1,34,2948] P(i(i(n(n(i(n(i(x,i(y,z))),y))),u),u)).

given clause #1219: (wt=23) 2985 [hyper,1,34,2973] P(i(i(n(n(i(n(i(n(i(n(n(x)),y)),z)),x))),u),u)).

given clause #1220: (wt=23) 2991 [hyper,1,116,2540] P(i(n(i(n(i(x,y)),n(n(i(y,z))))),u)).

given clause #1221: (wt=34) 437 [hyper,1,367,3] P(n(n(i(i(x,y),i(i(y,z),i(x,z)))))).

given clause #1222: (wt=23) 3002 [hyper,1,362,2942] P(i(i(i(n(i(n(i(x,y)),z)),x),n(n(u))),u)).

given clause #1223: (wt=23) 3030 [hyper,1,116,2949] P(i(n(i(n(i(x,i(n(n(y)),z))),y)),u)).

given clause #1224: (wt=23) 3097 [hyper,1,382,109] P(i(i(i(n(n(x)),i(y,x)),z),n(n(z)))).

given clause #1225: (wt=25) 442 [hyper,1,367,36] P(n(n(i(x,i(y,i(z,x)))))).

given clause #1226: (wt=23) 3322 [hyper,1,382,117] P(i(i(i(x,y),y),n(n(i(n(y),x))))).

given clause #1227: (wt=23) 3349 [hyper,1,117,138] P(i(i(i(n(n(x)),n(y)),n(y)),i(y,x))).

given clause #1228: (wt=23) 3386 [hyper,1,367,188] P(n(n(i(x,i(n(i(n(x),y)),z))))).

given clause #1229: (wt=50) 443 [hyper,1,241,36] P(i(i(x,y),i(x,i(z,i(u,y))))).

given clause #1230: (wt=23) 3417 [hyper,1,369,222] P(i(n(n(i(i(n(i(x,y)),z),u))),i(y,u))).

given clause #1231: (wt=23) 3418 [hyper,1,367,222] P(n(n(i(i(i(n(i(x,y)),z),u),i(y,u))))).

given clause #1232: (wt=23) 3428 [hyper,1,369,303] P(i(n(n(i(i(x,n(y)),n(z)))),i(z,y))).

given clause #1233: (wt=55) 444 [hyper,1,148,36] P(i(x,i(y,i(z,i(n(x),u))))).

given clause #1234: (wt=23) 3429 [hyper,1,367,303] P(n(n(i(i(i(x,n(y)),n(z)),i(z,y))))).

given clause #1235: (wt=23) 3433 [hyper,1,86,303] P(i(i(i(i(n(x),y),y),n(z)),i(z,x))).

given clause #1236: (wt=17) 18887 [hyper,1,3433,7839] P(i(n(i(i(n(x),n(n(y))),y)),x)).

given clause #1237: (wt=27) 445 [hyper,1,116,36] P(i(n(i(x,i(y,i(z,x)))),u)).

given clause #1238: (wt=19) 18898 [hyper,1,367,18887] P(n(n(i(n(i(i(n(x),n(n(y))),y)),x)))).

given clause #1239: (wt=21) 18891 [hyper,1,860,18887] P(i(n(i(n(i(i(n(x),n(n(y))),y)),z)),x)).

given clause #1240: (wt=21) 18892 [hyper,1,849,18887] P(i(n(i(i(n(n(i(x,y))),n(n(z))),z)),x)).

given clause #1241: (wt=49) 446 [hyper,1,76,36] P(i(n(n(x)),i(y,i(z,i(u,x))))).

given clause #1242: (wt=21) 18897 [hyper,1,371,18887] P(i(n(i(i(n(x),n(n(y))),y)),n(n(x)))).

given clause #1243: (wt=21) 18913 [hyper,1,116,18887] P(i(n(i(n(i(i(n(x),n(n(y))),y)),x)),z)).

given clause #1244: (wt=23) 3456 [hyper,1,59,3444] P(i(n(i(n(i(x,n(n(y)))),z)),i(y,u))).

given clause #1245: (wt=71) 447 [hyper,1,49,36] P(i(x,i(y,i(z,i(i(x,u),u))))).

given clause #1246: (wt=23) 3462 [hyper,1,34,3452] P(i(i(n(n(i(n(i(n(i(x,n(y))),z)),y))),u),u)).

given clause #1247: (wt=23) 3468 [hyper,1,116,3443] P(i(n(i(n(i(x,i(y,n(z)))),z)),u)).

given clause #1248: (wt=23) 3477 [hyper,1,367,325] P(n(n(i(n(n(x)),i(n(i(y,x)),z))))).

given clause #1249: (wt=48) 448 [hyper,1,37,36] P(i(n(x),i(y,i(z,i(x,u))))).

given clause #1250: (wt=23) 3481 [hyper,1,65,325] P(i(n(i(n(i(x,y)),z)),i(n(n(y)),u))).

given clause #1251: (wt=23) 3495 [hyper,1,369,379] P(i(n(n(x)),n(n(i(i(x,y),y))))).

given clause #1252: (wt=23) 3496 [hyper,1,367,379] P(n(n(i(x,n(n(i(i(x,y),y))))))).

given clause #1253: (wt=29) 449 [hyper,1,34,36] P(i(i(i(x,i(y,i(z,x))),u),u)).

given clause #1254: (wt=23) 3531 [hyper,1,379,3444] P(n(n(i(i(i(n(i(n(i(x,n(y))),z)),y),u),u)))).

given clause #1255: (wt=23) 3536 [hyper,1,379,2935] P(n(n(i(i(i(n(i(n(i(n(n(x)),y)),z)),x),u),u)))).

given clause #1256: (wt=23) 3537 [hyper,1,379,2934] P(n(n(i(i(n(n(i(n(i(n(i(x,y)),z)),x))),u),u)))).

given clause #1257: (wt=53) 450 [hyper,1,26,36] P(i(i(n(x),n(y)),i(z,i(u,i(y,x))))).

given clause #1258: (wt=23) 3538 [hyper,1,379,2929] P(n(n(i(i(i(n(i(x,i(y,z))),y),u),u)))).

given clause #1259: (wt=23) 3551 [hyper,1,379,1550] P(n(n(i(i(i(n(n(i(i(n(n(x)),x),y))),y),z),z)))).

given clause #1260: (wt=23) 3554 [hyper,1,379,1547] P(n(n(i(i(i(n(n(i(n(n(i(x,x))),y))),y),z),z)))).

given clause #1261: (wt=77) 451 [hyper,1,24,36] P(i(i(i(x,y),y),i(z,i(u,i(i(y,x),x))))).

given clause #1262: (wt=23) 3593 [hyper,1,379,1117] P(n(n(i(i(i(n(i(n(i(x,y)),n(y))),z),u),u)))).

given clause #1263: (wt=23) 3599 [hyper,1,379,1061] P(n(n(i(i(i(n(i(n(i(n(n(x)),y)),x)),z),u),u)))).

given clause #1264: (wt=23) 3608 [hyper,1,379,863] P(n(n(i(i(n(n(i(n(i(n(i(x,y)),x)),z))),u),u)))).

given clause #1265: (wt=47) 452 [hyper,1,23,36] P(i(x,i(y,i(z,i(u,x))))).

given clause #1266: (wt=23) 3610 [hyper,1,379,859] P(n(n(i(i(i(i(i(n(i(x,y)),x),z),z),u),u)))).

given clause #1267: (wt=23) 3611 [hyper,1,379,853] P(n(n(i(i(i(n(i(x,y)),i(z,x)),u),u)))).

given clause #1268: (wt=23) 3624 [hyper,1,379,668] P(n(n(i(i(i(n(i(n(i(x,n(y))),y)),z),u),u)))).

given clause #1269: (wt=31) 453 [hyper,1,36,418] P(i(x,i(y,n(n(i(z,z)))))).

given clause #1270: (wt=23) 3638 [hyper,1,379,527] P(n(n(i(i(n(n(i(i(n(n(i(x,x))),y),y))),z),z)))).

given clause #1271: (wt=23) 3641 [hyper,1,379,494] P(n(n(i(i(n(n(i(n(i(x,n(n(x)))),y))),z),z)))).

given clause #1272: (wt=23) 3644 [hyper,1,379,482] P(n(n(i(i(n(n(i(i(i(n(n(x)),x),y),y))),z),z)))).

given clause #1273: (wt=39) 454 [hyper,1,36,367] P(i(x,i(y,i(z,n(n(z)))))).

given clause #1274: (wt=23) 3649 [hyper,1,379,465] P(n(n(i(i(i(i(n(n(i(n(n(x)),x))),y),y),z),z)))).

given clause #1275: (wt=23) 3650 [hyper,1,379,462] P(n(n(i(i(i(n(i(n(i(n(n(x)),x)),y)),z),u),u)))).

given clause #1276: (wt=23) 3651 [hyper,1,379,441] P(n(n(i(i(i(x,n(n(i(y,y)))),z),z)))).

given clause #1277: (wt=31) 455 [hyper,1,36,337] P(i(x,i(y,i(n(n(z)),z)))).

given clause #1278: (wt=23) 3670 [hyper,1,379,388] P(n(n(i(i(i(x,n(n(i(y,x)))),z),z)))).

given clause #1279: (wt=23) 3671 [hyper,1,379,382] P(n(n(i(i(i(i(i(x,n(n(x))),y),y),z),z)))).

given clause #1280: (wt=23) 3673 [hyper,1,379,377] P(n(n(i(i(n(n(i(n(n(x)),i(y,x)))),z),z)))).

given clause #1281: (wt=83) 456 [hyper,1,36,138] P(i(x,i(y,i(i(n(n(z)),n(n(u))),i(z,u))))).

given clause #1282: (wt=23) 3675 [hyper,1,379,374] P(n(n(i(i(n(n(i(x,i(n(x),y)))),z),z)))).

given clause #1283: (wt=23) 3683 [hyper,1,379,327] P(n(n(i(i(i(x,i(n(n(y)),y)),z),z)))).

given clause #1284: (wt=23) 3770 [hyper,1,379,3487] P(n(n(i(i(i(n(i(i(i(x,y),z),z)),x),u),u)))).

given clause #1285: (wt=71) 457 [hyper,1,36,114] P(i(x,i(y,i(n(i(z,u)),i(n(u),z))))).

given clause #1286: (wt=23) 3776 [hyper,1,108,3487] P(i(n(i(i(i(n(n(x)),y),z),z)),i(u,x))).

given clause #1287: (wt=23) 3785 [hyper,1,379,3747] P(n(n(i(i(n(n(i(n(i(i(n(x),y),y)),x))),z),z)))).

given clause #1288: (wt=23) 3787 [hyper,1,69,3747] P(i(i(i(n(i(n(i(i(n(x),y),y)),x)),z),u),u)).

given clause #1289: (wt=79) 458 [hyper,1,36,89] P(i(x,i(y,i(i(i(z,u),u),i(n(u),z))))).

given clause #1290: (wt=23) 3799 [hyper,1,372,3497] P(n(n(i(n(i(n(i(i(i(x,n(y)),z),z)),y)),u)))).

given clause #1291: (wt=23) 3806 [hyper,1,44,3497] P(i(n(i(i(i(x,n(y)),z),z)),i(u,y))).

given clause #1292: (wt=23) 3807 [hyper,1,34,3497] P(i(i(i(n(i(i(i(x,n(y)),z),z)),y),u),u)).

given clause #1293: (wt=87) 459 [hyper,1,36,74] P(i(x,i(y,i(n(i(z,u)),i(i(u,z),z))))).

given clause #1294: (wt=23) 3813 [hyper,1,372,3751] P(n(n(i(n(i(n(i(n(i(i(n(x),y),y)),x)),z)),u)))).

given clause #1295: (wt=23) 3817 [hyper,1,34,3772] P(i(i(n(n(i(n(i(i(i(x,y),z),z)),x))),u),u)).

given clause #1296: (wt=23) 3848 [hyper,1,372,3773] P(n(n(i(n(i(n(i(i(i(n(n(x)),y),z),z)),x)),u)))).

given clause #1297: (wt=71) 460 [hyper,1,36,34] P(i(x,i(y,i(z,i(i(z,u),u))))).

given clause #1298: (wt=23) 3854 [hyper,1,34,3773] P(i(i(i(n(i(i(i(n(n(x)),y),z),z)),x),u),u)).

given clause #1299: (wt=23) 3866 [hyper,1,116,3759] P(i(n(i(n(i(i(n(x),y),y)),i(z,x))),u)).

given clause #1300: (wt=23) 3916 [hyper,1,362,3765] P(i(i(i(n(i(i(n(x),y),y)),x),n(n(z))),z)).

given clause #1301: (wt=39) 463 [hyper,1,36,392] P(i(x,i(y,n(n(i(n(n(z)),z)))))).

given clause #1302: (wt=23) 3918 [hyper,1,116,3765] P(i(n(i(i(i(n(i(i(n(x),y),y)),x),z),z)),u)).

given clause #1303: (wt=23) 3981 [hyper,1,367,381] P(n(n(i(i(i(x,n(n(x))),y),i(z,y))))).

given clause #1304: (wt=23) 4158 [hyper,1,369,383] P(i(n(n(i(i(x,y),z))),n(n(i(y,z))))).

given clause #1305: (wt=26) 468 [hyper,1,241,364] P(i(i(x,n(i(n(n(y)),y))),i(x,z))).

given clause #1306: (wt=23) 4159 [hyper,1,367,383] P(n(n(i(i(i(x,y),z),n(n(i(y,z))))))).

given clause #1307: (wt=23) 4189 [hyper,1,3765,386] P(n(n(i(x,i(i(n(n(x)),y),y))))).

given clause #1308: (wt=23) 4194 [hyper,1,369,386] P(i(n(n(i(n(x),n(y)))),n(n(i(y,x))))).

given clause #1309: (wt=27) 469 [hyper,1,146,364] P(i(n(i(x,i(n(i(n(n(y)),y)),z))),u)).

given clause #1310: (wt=23) 4195 [hyper,1,367,386] P(n(n(i(i(n(x),n(y)),n(n(i(y,x))))))).

given clause #1311: (wt=23) 4204 [hyper,1,66,386] P(i(i(i(x,y),n(z)),n(n(i(z,x))))).

given clause #1312: (wt=23) 4242 [hyper,1,116,4202] P(i(n(i(n(i(x,y)),n(n(i(z,x))))),u)).

given clause #1313: (wt=47) 470 [hyper,1,36,364] P(i(x,i(y,i(n(i(n(n(z)),z)),u)))).

given clause #1314: (wt=23) 4259 [hyper,1,127,1771] P(i(i(i(x,y),n(z)),i(z,n(y)))).

given clause #1315: (wt=21) 19064 [hyper,1,4259,979] P(i(n(i(x,n(n(i(y,z))))),n(z))).

given clause #1316: (wt=23) 4304 [hyper,1,117,129] P(i(i(i(n(i(x,y)),y),y),i(n(y),x))).

given clause #1317: (wt=26) 473 [hyper,1,3,364] P(i(i(x,y),i(n(i(n(n(z)),z)),y))).

given clause #1318: (wt=23) 4331 [hyper,1,367,464] P(n(n(i(i(n(n(i(n(n(x)),x))),y),i(z,y))))).

given clause #1319: (wt=23) 4344 [hyper,1,369,489] P(i(n(n(i(i(x,i(n(n(y)),y)),z))),z)).

given clause #1320: (wt=23) 4390 [hyper,1,369,490] P(i(n(n(i(n(x),n(i(n(n(y)),y))))),x)).

given clause #1321: (wt=27) 475 [hyper,1,146,370] P(i(n(i(x,n(n(i(y,n(n(y))))))),z)).

given clause #1322: (wt=23) 4391 [hyper,1,367,490] P(n(n(i(i(n(x),n(i(n(n(y)),y))),x)))).

given clause #1323: (wt=23) 4399 [hyper,1,66,490] P(i(i(i(x,y),n(i(n(n(z)),z))),x)).

given clause #1324: (wt=23) 4415 [hyper,1,490,1550] P(n(i(i(n(n(x)),x),n(i(n(n(y)),y))))).

given clause #1325: (wt=47) 477 [hyper,1,36,370] P(i(x,i(y,n(n(i(z,n(n(z)))))))).

given clause #1326: (wt=23) 4417 [hyper,1,490,1547] P(n(i(n(n(i(x,x))),n(i(n(n(y)),y))))).

given clause #1327: (wt=23) 4432 [hyper,1,367,507] P(n(n(i(i(i(x,i(y,x)),n(n(z))),z)))).

given clause #1328: (wt=23) 4443 [hyper,1,369,517] P(i(n(n(i(i(x,i(y,x)),z))),n(n(z)))).

given clause #1329: (wt=27) 481 [hyper,1,367,38] P(n(n(i(x,i(n(y),i(y,z)))))).

given clause #1330: (wt=23) 4444 [hyper,1,367,517] P(n(n(i(i(i(x,i(y,x)),z),n(n(z)))))).

given clause #1331: (wt=23) 4498 [hyper,1,369,535] P(i(n(n(i(i(x,n(n(i(y,y)))),z))),z)).

given clause #1332: (wt=23) 4513 [hyper,1,369,557] P(i(n(n(i(n(n(i(x,i(n(x),y)))),z))),z)).

given clause #1333: (wt=30) 483 [hyper,1,241,366] P(i(i(x,i(i(n(n(y)),y),z)),i(x,z))).

given clause #1334: (wt=21) 19144 [hyper,1,3765,483] P(i(n(i(i(n(i(i(n(n(x)),x),y)),z),z)),y)).

given clause #1335: (wt=22) 19157 [hyper,1,483,14576] P(i(i(x,n(i(n(n(y)),y))),n(x))).

given clause #1336: (wt=23) 4530 [hyper,1,369,562] P(i(n(n(i(n(n(i(n(n(x)),i(y,x)))),z))),z)).

given clause #1337: (wt=31) 484 [hyper,1,146,366] P(i(n(i(x,i(i(i(n(n(y)),y),z),z))),u)).

given clause #1338: (wt=23) 4582 [hyper,1,369,587] P(i(n(n(i(i(i(i(x,n(n(x))),y),y),z))),z)).

given clause #1339: (wt=23) 4607 [hyper,1,369,611] P(i(n(n(i(i(x,n(n(i(y,x)))),z))),z)).

given clause #1340: (wt=23) 4670 [hyper,1,369,725] P(i(n(n(i(i(n(i(n(i(n(n(x)),x)),y)),z),u))),u)).

given clause #1341: (wt=55) 486 [hyper,1,36,366] P(i(x,i(y,i(i(i(n(n(z)),z),u),u)))).

given clause #1342: (wt=23) 4677 [hyper,1,369,768] P(i(n(n(i(i(i(n(n(i(n(n(x)),x))),y),y),z))),z)).

given clause #1343: (wt=23) 4723 [hyper,1,369,777] P(i(n(n(i(n(n(i(i(i(n(n(x)),x),y),y))),z))),z)).

given clause #1344: (wt=23) 4769 [hyper,1,369,784] P(i(n(n(i(n(n(i(n(i(x,n(n(x)))),y))),z))),z)).

given clause #1345: (wt=25) 487 [hyper,1,35,366] P(i(i(i(i(i(n(n(x)),x),y),y),z),i(u,z))).

given clause #1346: (wt=23) 4784 [hyper,1,369,811] P(i(n(n(i(n(n(i(i(n(n(i(x,x))),y),y))),z))),z)).

given clause #1347: (wt=23) 4810 [hyper,1,26,136] P(i(i(n(n(i(x,y))),n(n(z))),i(y,z))).

given clause #1348: (wt=23) 4825 [hyper,1,369,816] P(i(n(n(i(i(n(i(n(i(x,n(y))),y)),z),u))),u)).

given clause #1349: (wt=30) 492 [hyper,1,3,366] P(i(i(x,y),i(i(i(n(n(z)),z),x),y))).

given clause #1350: (wt=23) 4834 [hyper,1,369,832] P(i(n(n(i(n(n(i(x,y))),z))),i(n(x),z))).

given clause #1351: (wt=23) 4835 [hyper,1,367,832] P(n(n(i(i(n(n(i(x,y))),z),i(n(x),z))))).

given clause #1352: (wt=23) 4861 [hyper,1,367,858] P(n(n(i(i(i(n(i(x,y)),x),z),i(u,z))))).

given clause #1353: (wt=27) 493 [hyper,1,2,366] P(i(x,i(i(i(n(n(y)),y),z),z))).

given clause #1354: (wt=23) 4867 [hyper,1,369,924] P(i(n(n(i(i(n(i(x,y)),i(z,x)),u))),u)).

given clause #1355: (wt=23) 4871 [hyper,1,369,931] P(i(n(n(i(i(i(i(n(i(x,y)),x),z),z),u))),u)).

given clause #1356: (wt=23) 4889 [hyper,1,94,139] P(i(n(i(x,n(y))),i(i(y,z),z))).

given clause #1357: (wt=30) 495 [hyper,1,241,375] P(i(i(x,n(i(y,n(n(y))))),i(x,z))).

given clause #1358: (wt=23) 4905 [hyper,1,369,938] P(i(n(n(i(n(n(i(n(i(n(i(x,y)),x)),z))),u))),u)).

given clause #1359: (wt=23) 5078 [hyper,1,369,977] P(i(n(n(i(i(x,n(n(y))),z))),i(y,z))).

given clause #1360: (wt=23) 5079 [hyper,1,367,977] P(n(n(i(i(i(x,n(n(y))),z),i(y,z))))).

given clause #1361: (wt=31) 496 [hyper,1,146,375] P(i(n(i(x,i(n(i(y,n(n(y)))),z))),u)).

given clause #1362: (wt=23) 5269 [hyper,1,369,1088] P(i(n(n(i(i(n(i(n(i(n(n(x)),y)),x)),z),u))),u)).

given clause #1363: (wt=23) 5286 [hyper,1,369,1140] P(i(n(n(i(i(n(i(n(i(x,y)),n(y))),z),u))),u)).

given clause #1364: (wt=23) 5321 [hyper,1,367,1324] P(n(n(i(i(i(n(n(x)),x),x),i(n(x),y))))).

given clause #1365: (wt=55) 497 [hyper,1,36,375] P(i(x,i(y,i(n(i(z,n(n(z)))),u)))).

given clause #1366: (wt=23) 5351 [hyper,1,367,1328] P(n(n(i(i(n(n(i(x,x))),n(y)),i(y,z))))).

given clause #1367: (wt=23) 5367 [hyper,1,367,1330] P(n(n(i(i(i(n(n(x)),x),n(y)),i(y,z))))).

given clause #1368: (wt=23) 5383 [hyper,1,369,1440] P(i(n(n(i(i(x,y),n(n(z))))),i(y,z))).

given clause #1369: (wt=25) 498 [hyper,1,35,375] P(i(i(i(n(i(x,n(n(x)))),y),z),i(u,z))).

given clause #1370: (wt=23) 5384 [hyper,1,367,1440] P(n(n(i(i(i(x,y),n(n(z))),i(y,z))))).

given clause #1371: (wt=23) 5402 [hyper,1,367,1444] P(n(n(i(i(i(n(i(x,y)),n(y)),n(n(z))),z)))).

given clause #1372: (wt=23) 5418 [hyper,1,367,1445] P(n(n(i(i(i(n(i(n(n(x)),y)),x),n(n(z))),z)))).

given clause #1373: (wt=30) 500 [hyper,1,3,375] P(i(i(x,y),i(n(i(z,n(n(z)))),y))).

given clause #1374: (wt=23) 5432 [hyper,1,367,1446] P(n(n(i(i(n(n(i(n(i(x,y)),x))),n(n(z))),z)))).

given clause #1375: (wt=23) 5447 [hyper,1,367,1448] P(n(n(i(i(i(n(i(x,n(y))),y),n(n(z))),z)))).

given clause #1376: (wt=23) 5463 [hyper,1,367,1449] P(n(n(i(i(n(n(i(x,n(n(x))))),n(n(y))),y)))).

given clause #1377: (wt=27) 501 [hyper,1,2,375] P(i(x,i(n(i(y,n(n(y)))),z))).

given clause #1378: (wt=23) 5492 [hyper,1,367,1450] P(n(n(i(i(i(n(i(n(n(x)),x)),y),n(n(z))),z)))).

given clause #1379: (wt=23) 5518 [hyper,1,367,1516] P(n(n(i(n(n(i(i(x,y),z))),i(n(x),z))))).

given clause #1380: (wt=23) 5541 [hyper,1,369,1524] P(i(n(n(x)),i(n(n(i(x,y))),y))).

given clause #1381: (wt=31) 502 [hyper,1,146,385] P(i(n(i(x,n(n(i(y,i(z,y)))))),u)).

given clause #1382: (wt=16) 19291 [hyper,1,14575,5541] P(i(n(i(n(n(i(x,y))),y)),n(x))).

given clause #1383: (wt=18) 19290 [hyper,1,14602,5541] P(n(n(i(n(i(n(n(i(x,y))),y)),n(x))))).

given clause #1384: (wt=20) 19315 [hyper,1,860,19291] P(i(n(i(n(i(n(n(i(x,y))),y)),z)),n(x))).

given clause #1385: (wt=55) 503 [hyper,1,36,385] P(i(x,i(y,n(n(i(z,i(u,z))))))).

given clause #1386: (wt=20) 19322 [hyper,1,116,19291] P(i(n(i(n(i(n(n(i(x,y))),y)),n(x))),z)).

given clause #1387: (wt=22) 19325 [hyper,1,34,19291] P(i(i(i(n(i(n(n(i(x,y))),y)),n(x)),z),z)).

given clause #1388: (wt=23) 5542 [hyper,1,367,1524] P(n(n(i(x,i(n(n(i(x,y))),y))))).

given clause #1389: (wt=25) 504 [hyper,1,35,385] P(i(i(n(n(i(x,i(y,x)))),z),i(u,z))).

given clause #1390: (wt=23) 5590 [hyper,1,1524,3747] P(i(n(n(i(n(n(i(n(i(i(n(x),y),y)),x))),z))),z)).

given clause #1391: (wt=23) 5593 [hyper,1,1524,3487] P(i(n(n(i(i(n(i(i(i(x,y),z),z)),x),u))),u)).

given clause #1392: (wt=23) 5595 [hyper,1,1524,3444] P(i(n(n(i(i(n(i(n(i(x,n(y))),z)),y),u))),u)).

given clause #1393: (wt=40) 506 [hyper,1,367,40] P(n(n(i(i(x,y),i(i(i(z,i(u,z)),x),y))))).

given clause #1394: (wt=23) 5600 [hyper,1,1524,2935] P(i(n(n(i(i(n(i(n(i(n(n(x)),y)),z)),x),u))),u)).

given clause #1395: (wt=23) 5601 [hyper,1,1524,2934] P(i(n(n(i(n(n(i(n(i(n(i(x,y)),z)),x))),u))),u)).

given clause #1396: (wt=23) 5602 [hyper,1,1524,2929] P(i(n(n(i(i(n(i(x,i(y,z))),y),u))),u)).

given clause #1397: (wt=39) 508 [hyper,1,148,40] P(i(x,i(i(i(y,i(z,y)),n(x)),u))).

given clause #1398: (wt=23) 5615 [hyper,1,1524,1550] P(i(n(n(i(i(n(n(i(i(n(n(x)),x),y))),y),z))),z)).

given clause #1399: (wt=23) 5618 [hyper,1,1524,1547] P(i(n(n(i(i(n(n(i(n(n(i(x,x))),y))),y),z))),z)).

given clause #1400: (wt=23) 5882 [hyper,1,369,1534] P(i(n(n(i(n(x),n(y)))),i(n(n(y)),x))).

given clause #1401: (wt=25) 509 [hyper,1,143,40] P(i(i(i(x,i(y,x)),z),i(n(z),u))).

given clause #1402: (wt=23) 5883 [hyper,1,367,1534] P(n(n(i(i(n(x),n(y)),i(n(n(y)),x))))).

given clause #1403: (wt=23) 5892 [hyper,1,66,1534] P(i(i(i(x,y),n(z)),i(n(n(z)),x))).

given clause #1404: (wt=23) 5929 [hyper,1,367,1554] P(n(n(i(n(n(i(i(x,i(n(x),y)),z))),z)))).

given clause #1405: (wt=27) 510 [hyper,1,75,40] P(i(i(i(x,i(y,x)),n(n(z))),i(u,z))).

given clause #1406: (wt=23) 5960 [hyper,1,367,1556] P(n(n(i(n(n(i(i(x,y),y))),i(n(y),x))))).

given clause #1407: (wt=23) 6055 [hyper,1,367,1558] P(n(n(i(n(n(i(i(n(n(x)),i(y,x)),z))),z)))).

given clause #1408: (wt=23) 6096 [hyper,1,367,1604] P(n(n(i(n(n(i(n(n(i(x,x))),y))),i(z,y))))).

given clause #1409: (wt=25) 511 [hyper,1,51,40] P(i(i(i(x,i(y,x)),n(z)),i(z,u))).

given clause #1410: (wt=23) 6132 [hyper,1,367,1625] P(n(n(i(n(n(i(i(n(n(x)),x),y))),i(z,y))))).

given clause #1411: (wt=23) 6165 [hyper,1,367,1638] P(n(n(i(n(n(i(i(n(i(x,y)),x),n(n(z))))),z)))).

given clause #1412: (wt=23) 6173 [hyper,1,367,1692] P(n(n(i(n(i(n(i(x,y)),z)),i(n(x),u))))).

given clause #1413: (wt=47) 512 [hyper,1,49,40] P(i(x,i(i(i(y,i(z,y)),i(x,u)),u))).

given clause #1414: (wt=23) 6175 [hyper,1,367,1704] P(n(n(i(n(i(i(i(x,y),z),z)),i(y,u))))).

given clause #1415: (wt=23) 6178 [hyper,1,367,1707] P(n(n(i(n(i(x,i(y,z))),i(z,u))))).

given clause #1416: (wt=23) 6186 [hyper,1,367,1714] P(n(n(i(n(n(i(n(n(i(n(n(x)),x))),n(n(y))))),y)))).

given clause #1417: (wt=36) 513 [hyper,1,37,40] P(i(n(x),i(i(i(y,i(z,y)),x),u))).

given clause #1418: (wt=23) 6211 [hyper,1,367,1737] P(n(n(i(n(n(i(i(x,n(n(x))),n(n(y))))),y)))).

given clause #1419: (wt=23) 6274 [hyper,1,367,1987] P(n(n(i(n(n(i(i(i(i(n(n(x)),x),y),y),z))),z)))).

given clause #1420: (wt=23) 6318 [hyper,1,367,2030] P(n(n(i(n(n(i(i(n(i(x,n(n(x)))),y),z))),z)))).

given clause #1421: (wt=41) 514 [hyper,1,26,40] P(i(i(n(x),n(y)),i(i(i(z,i(u,z)),y),x))).

given clause #1422: (wt=23) 6353 [hyper,1,367,2044] P(n(n(i(n(n(i(n(n(i(x,i(y,x)))),z))),z)))).

given clause #1423: (wt=23) 6390 [hyper,1,367,2056] P(n(n(i(n(n(i(i(i(n(n(i(x,x))),y),y),z))),z)))).

given clause #1424: (wt=23) 6425 [hyper,1,367,2073] P(n(n(i(n(n(i(n(n(i(n(i(n(n(x)),x)),y))),z))),z)))).

given clause #1425: (wt=53) 515 [hyper,1,24,40] P(i(i(i(x,y),y),i(i(i(z,i(u,z)),i(y,x)),x))).

given clause #1426: (wt=23) 6504 [hyper,1,367,2197] P(n(n(i(n(n(i(n(n(i(x,y))),z))),i(y,z))))).

given clause #1427: (wt=23) 6527 [hyper,1,367,2233] P(n(n(i(n(n(i(n(n(i(n(i(x,n(y))),y))),z))),z)))).

given clause #1428: (wt=23) 6598 [hyper,1,367,2365] P(n(n(i(n(n(i(i(n(i(n(i(x,y)),x)),z),u))),u)))).

given clause #1429: (wt=33) 516 [hyper,1,40,375] P(i(i(i(x,i(y,x)),n(i(z,n(n(z))))),u)).

given clause #1430: (wt=23) 6699 [hyper,1,367,2406] P(n(n(i(n(n(i(n(n(i(n(i(n(n(x)),y)),x))),z))),z)))).

given clause #1431: (wt=23) 6735 [hyper,1,115,186] P(i(i(i(n(i(x,y)),z),y),i(n(y),x))).

given clause #1432: (wt=23) 6742 [hyper,1,186,1771] P(i(i(i(n(i(x,y)),z),n(u)),i(u,x))).

given clause #1433: (wt=33) 518 [hyper,1,40,366] P(i(i(i(x,i(y,x)),i(i(n(n(z)),z),u)),u)).

given clause #1434: (wt=23) 6799 [hyper,1,367,2458] P(n(n(i(n(n(i(n(n(i(n(i(x,y)),n(y)))),z))),z)))).

given clause #1435: (wt=23) 6939 [hyper,1,192,383]