----- Otter 3.3, August 2003 -----
The process was started by mccune on gyro.thornwood,
Fri Sep 12 16:35:28 2003
The command was "otter".  The process ID is 26076.

include("ortholattice-header").
------- start included file ortholattice-header-------
op(400,infix,^).
op(400,infix,v).

lex([A,B,C,D,0,1,x v x,c(x),x^x,f(x,x)]).
set(anl_eq).
   dependent: set(para_from).
   dependent: set(para_into).
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).
   dependent: set(order_eq).
   dependent: set(back_demod).
   dependent: set(process_input).
   dependent: set(lrpo).
assign(pick_given_ratio,3).
assign(max_weight,25).
clear(detailed_history).
assign(max_seconds,60).
assign(max_mem,100000).
clear(print_new_demod).
clear(print_back_demod).
clear(print_back_sub).
clear(print_kept).
assign(stats_level,1).

list(usable).
0 [] x=x.
end_of_list.
------- end included file ortholattice-header-------

lex([A,B,C,D,0,1,x v x,x^x,c(x),f(x,x)]).
assign(max_weight,19).

list(sos).
0 [] x v (y v z)=y v (x v z).
0 [] x^y=c(c(x) v c(y)).
0 [] x v c(x)=y v c(y).
0 [] (x v c(y))^ (x v y)=x.
0 [] x v c(x)=1.
0 [] c(1)=0.
0 [] A^ (B v C)!= (A^B) v (A^C)|$Ans(DIST1).
end_of_list.

------------> process usable:
** KEPT (pick-wt=3): 1 [] x=x.
  Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] x=x.

------------> process sos:
** KEPT (pick-wt=11): 2 [] x v (y v z)=y v (x v z).
** KEPT (pick-wt=10): 4 [copy,3,flip.1] c(c(x) v c(y))=x^y.
---> New Demodulator: 5 [new_demod,4] c(c(x) v c(y))=x^y.
** KEPT (pick-wt=9): 6 [] x v c(x)=y v c(y).
** KEPT (pick-wt=10): 7 [] (x v c(y))^ (x v y)=x.
---> New Demodulator: 8 [new_demod,7] (x v c(y))^ (x v y)=x.
** KEPT (pick-wt=6): 9 [] x v c(x)=1.
---> New Demodulator: 10 [new_demod,9] x v c(x)=1.
** KEPT (pick-wt=4): 11 [] c(1)=0.
---> New Demodulator: 12 [new_demod,11] c(1)=0.
** KEPT (pick-wt=13): 13 [] A^ (B v C)!= (A^B) v (A^C)|$Ans(DIST1).
  Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x v (y v z)=y v (x v z).
>>>> Starting back demodulation with 5.
  Following clause subsumed by 1 during input processing: 0 [copy,6,flip.1,demod,10,10] 1=1.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 10.
    >> back demodulating 6 with 10.
>>>> Starting back demodulation with 12.

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

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

given clause #1: (wt=11) 2 [] x v (y v z)=y v (x v z).

given clause #2: (wt=4) 11 [] c(1)=0.

given clause #3: (wt=6) 9 [] x v c(x)=1.

given clause #4: (wt=5) 16 [para_into,9,11] 1 v 0=1.

given clause #5: (wt=10) 4 [copy,3,flip.1] c(c(x) v c(y))=x^y.

given clause #6: (wt=6) 30 [para_into,4,9,demod,12,flip.1] x^c(x)=0.

given clause #7: (wt=5) 34 [para_into,30,11] 1^0=0.

given clause #8: (wt=9) 20 [para_from,16,2] x v 1=1 v (x v 0).

given clause #9: (wt=10) 7 [] (x v c(y))^ (x v y)=x.

given clause #10: (wt=7) 44 [para_into,7,9] 1^ (x v x)=x.

given clause #11: (wt=8) 48 [para_into,7,16] (1 v c(0))^1=1.

given clause #12: (wt=9) 21 [copy,20,flip.1] 1 v (x v 0)=x v 1.

given clause #13: (wt=13) 13 [] A^ (B v C)!= (A^B) v (A^C)|$Ans(DIST1).

given clause #14: (wt=9) 22 [para_into,4,11] c(0 v c(x))=1^x.

given clause #15: (wt=8) 62 [para_into,22,11] c(0 v 0)=1^1.

given clause #16: (wt=9) 26 [para_into,4,11] c(c(x) v 0)=x^1.

given clause #17: (wt=15) 14 [para_into,2,2] x v (y v (z v u))=z v (x v (y v u)).

given clause #18: (wt=9) 40 [para_into,7,11] (x v 0)^ (x v 1)=x.

given clause #19: (wt=9) 50 [para_into,7,9] (x v c(c(x)))^1=x.

given clause #20: (wt=9) 74 [para_from,62,30] (0 v 0)^ (1^1)=0.

given clause #21: (wt=15) 15 [copy,14,flip.1] x v (y v (z v u))=y v (z v (x v u)).

given clause #22: (wt=9) 76 [para_from,62,9] (0 v 0) v (1^1)=1.

given clause #23: (wt=10) 18 [para_from,9,2,flip.1] x v (y v c(x))=y v 1.

given clause #24: (wt=10) 68 [para_from,22,30] (0 v c(x))^ (1^x)=0.

given clause #25: (wt=15) 24 [para_into,4,4] c((x^y) v c(z))= (c(x) v c(y))^z.

given clause #26: (wt=9) 147 [para_into,68,62,demod,45] (0 v (1^1))^0=0.

given clause #27: (wt=10) 70 [para_from,22,9] (0 v c(x)) v (1^x)=1.

given clause #28: (wt=9) 174 [para_into,70,62,demod,45] (0 v (1^1)) v 0=1.

given clause #29: (wt=15) 28 [para_into,4,4] c(c(x) v (y^z))=x^ (c(y) v c(z)).

given clause #30: (wt=7) 191 [back_demod,182,demod,185,45,flip.1] 0 v (1^1)=1.

given clause #31: (wt=10) 88 [para_from,26,30] (c(x) v 0)^ (x^1)=0.

given clause #32: (wt=10) 90 [para_from,26,9] (c(x) v 0) v (x^1)=1.

given clause #33: (wt=11) 32 [para_from,4,9] (c(x) v c(y)) v (x^y)=1.

given clause #34: (wt=10) 155 [para_into,68,44] (0 v c(x v x))^x=0.

given clause #35: (wt=10) 178 [para_into,70,44] (0 v c(x v x)) v x=1.

given clause #36: (wt=10) 210 [para_from,191,7] (0 v c(1^1))^1=0.

given clause #37: (wt=11) 36 [para_into,30,4] (c(x) v c(y))^ (x^y)=0.

given clause #38: (wt=11) 46 [para_into,7,20,demod,12] (x v 0)^ (1 v (x v 0))=x.

given clause #39: (wt=11) 212 [para_from,191,2,flip.1] 0 v (x v (1^1))=x v 1.

given clause #40: (wt=9) 286 [para_into,212,90,demod,12,flip.1] (0 v 0) v 1=0 v 1.

given clause #41: (wt=13) 38 [para_from,20,2] x v (1 v (y v 0))=y v (x v 1).

given clause #42: (wt=11) 262 [para_from,210,90,demod,161,63,163] ((1^ (1^1)) v 0) v 0=1.

given clause #43: (wt=9) 311 [para_from,262,46,demod,263,45,flip.1] (1^ (1^1)) v 0=1.

given clause #44: (wt=7) 314 [para_from,311,46,demod,312,45,flip.1] 1^ (1^1)=1.

given clause #45: (wt=13) 39 [copy,38,flip.1] x v (y v 1)=y v (1 v (x v 0)).

given clause #46: (wt=10) 316 [para_from,314,70] (0 v c(1^1)) v 1=1.

given clause #47: (wt=11) 292 [para_into,286,20] 1 v ((0 v 0) v 0)=0 v 1.

given clause #48: (wt=12) 56 [para_from,21,7] (1 v c(x v 0))^ (x v 1)=1.

given clause #49: (wt=15) 42 [para_into,7,4] (x v (y^z))^ (x v (c(y) v c(z)))=x.

given clause #50: (wt=9) 380 [para_into,42,191,demod,12,12] 1^ (0 v (0 v 0))=0.

given clause #51: (wt=11) 358 [para_into,56,62] (1 v (1^1))^ (0 v 1)=1.

given clause #52: (wt=12) 248 [para_into,178,20] 1 v ((0 v c(1 v 1)) v 0)=1.

given clause #53: (wt=14) 52 [para_into,7,2] (x v c(y v z))^ (y v (x v z))=x.

given clause #54: (wt=12) 338 [para_into,316,20] 1 v ((0 v c(1^1)) v 0)=1.

given clause #55: (wt=12) 390 [para_into,42,18] (x v (y^x))^ (c(y) v 1)=x.

given clause #56: (wt=11) 474 [para_into,390,11] (x v (1^x))^ (0 v 1)=x.

given clause #57: (wt=13) 54 [para_into,44,2] 1^ (x v ((x v y) v y))=x v y.

given clause #58: (wt=12) 398 [para_from,380,70] (0 v c(0 v (0 v 0))) v 0=1.

given clause #59: (wt=10) 505 [para_from,398,46,demod,399,45,flip.1] 0 v c(0 v (0 v 0))=1.

given clause #60: (wt=11) 507 [para_from,505,52] 1^ (0 v (0 v (0 v 0)))=0.

given clause #61: (wt=13) 58 [para_from,21,2] x v (y v 1)=1 v (x v (y v 0)).

given clause #62: (wt=11) 509 [para_from,505,18] (0 v (0 v 0)) v 1=0 v 1.

given clause #63: (wt=13) 59 [copy,58,flip.1] 1 v (x v (y v 0))=x v (y v 1).

given clause #64: (wt=13) 72 [para_from,62,7] (x v (1^1))^ (x v (0 v 0))=x.

given clause #65: (wt=14) 64 [para_into,22,4] c(0 v (x^y))=1^ (c(x) v c(y)).

given clause #66: (wt=13) 119 [para_into,15,21] x v (y v 1)=1 v (y v (x v 0)).

given clause #67: (wt=13) 125 [copy,119,flip.1] 1 v (x v (y v 0))=y v (x v 1).

given clause #68: (wt=13) 135 [para_from,76,2,flip.1] (0 v 0) v (x v (1^1))=x v 1.

given clause #69: (wt=14) 66 [para_from,22,7] (x v (1^y))^ (x v (0 v c(y)))=x.

given clause #70: (wt=13) 214 [para_into,88,62] ((1^1) v 0)^ ((0 v 0)^1)=0.

given clause #71: (wt=13) 222 [para_into,90,62] ((1^1) v 0) v ((0 v 0)^1)=1.

given clause #72: (wt=13) 240 [para_into,32,40] (c(x v 0) v c(x v 1)) v x=1.

given clause #73: (wt=14) 84 [para_into,26,4] c((x^y) v 0)= (c(x) v c(y))^1.

given clause #74: (wt=10) 643 [para_from,240,46,demod,63,631,45,63,flip.1] (1^1) v c(0 v 1)=1.

given clause #75: (wt=7) 702 [back_demod,685,demod,688,55,flip.1] 1^1=0 v 1.

given clause #76: (wt=7) 754 [back_demod,314,demod,703] 1^ (0 v 1)=1.

given clause #77: (wt=14) 86 [para_from,26,7] (x v (y^1))^ (x v (c(y) v 0))=x.

given clause #78: (wt=7) 778 [back_demod,191,demod,703] 0 v (0 v 1)=1.

given clause #79: (wt=8) 790 [back_demod,62,demod,703] c(0 v 0)=0 v 1.

given clause #80: (wt=9) 786 [back_demod,76,demod,703] (0 v 0) v (0 v 1)=1.

given clause #81: (wt=17) 92 [para_into,14,21] x v (y v (z v 1))=1 v (x v (y v (z v 0))).

given clause #82: (wt=9) 798 [para_into,754,20] 1^ (1 v (0 v 0))=1.

given clause #83: (wt=9) 806 [para_into,778,20] 0 v (1 v (0 v 0))=1.

given clause #84: (wt=9) 808 [para_into,778,119] 1 v (0 v (0 v 0))=1.

given clause #85: (wt=17) 93 [para_into,14,20] x v (y v (1 v (z v 0)))=z v (x v (y v 1)).

given clause #86: (wt=10) 752 [back_demod,316,demod,703] (0 v c(0 v 1)) v 1=1.

given clause #87: (wt=10) 774 [back_demod,210,demod,703] (0 v c(0 v 1))^1=0.

given clause #88: (wt=11) 772 [back_demod,212,demod,703] 0 v (x v (0 v 1))=x v 1.

given clause #89: (wt=14) 94 [para_into,14,9,flip.1] x v (y v (z v c(x)))=y v (z v 1).

given clause #90: (wt=11) 792 [para_from,702,390,demod,12] (1 v (0 v 1))^ (0 v 1)=1.

given clause #91: (wt=11) 810 [para_from,778,15,flip.1] 0 v (0 v (x v 1))=x v 1.

given clause #92: (wt=11) 816 [para_into,786,20] (0 v 0) v (1 v (0 v 0))=1.

given clause #93: (wt=19) 96 [para_into,14,2] x v (y v (z v (u v v)))=u v (x v (y v (z v v))).

given clause #94: (wt=11) 818 [para_into,786,58] 1 v ((0 v 0) v (0 v 0))=1.

given clause #95: (wt=11) 865 [para_into,792,39,demod,17] (0 v (1 v 1))^ (0 v 1)=1.

given clause #96: (wt=12) 710 [back_demod,683,demod,703] (0 v 1) v c(1 v (0 v 0))=1.

given clause #97: (wt=19) 97 [para_into,14,14] x v (y v (z v (u v v)))=u v (x v (z v (y v v))).

given clause #98: (wt=12) 750 [back_demod,338,demod,703] 1 v ((0 v c(0 v 1)) v 0)=1.

given clause #99: (wt=12) 796 [para_from,702,84,demod,12,12] c((0 v 1) v 0)= (0 v 0)^1.

given clause #100: (wt=12) 832 [para_from,798,70] (0 v c(1 v (0 v 0))) v 1=1.

given clause #101: (wt=15) 98 [para_into,14,2] x v (y v (z v u))=z v (y v (x v u)).

given clause #102: (wt=12) 834 [para_from,798,68] (0 v c(1 v (0 v 0)))^1=0.

given clause #103: (wt=12) 838 [para_from,806,52] (1 v c(0 v (0 v 0)))^1=1.

given clause #104: (wt=13) 276 [para_into,36,40] (c(x v 0) v c(x v 1))^x=0.

given clause #105: (wt=17) 99 [copy,92,flip.1] 1 v (x v (y v (z v 0)))=x v (y v (z v 1)).

given clause #106: (wt=13) 298 [para_from,286,2] x v (0 v 1)= (0 v 0) v (x v 1).

given clause #107: (wt=13) 322 [para_into,39,2] x v (y v 1)=x v (1 v (y v 0)).

given clause #108: (wt=13) 325 [copy,322,flip.1] x v (1 v (y v 0))=x v (y v 1).

given clause #109: (wt=17) 100 [copy,93,flip.1] x v (y v (z v 1))=y v (z v (1 v (x v 0))).

given clause #110: (wt=13) 466 [para_into,390,44,demod,12] ((x v x) v x)^ (0 v 1)=x v x.

given clause #111: (wt=13) 478 [para_into,474,20] (x v (1^x))^ (1 v (0 v 0))=x.

given clause #112: (wt=13) 516 [para_from,505,7] (0 v c(c(0 v (0 v 0))))^1=0.

given clause #113: (wt=19) 101 [copy,96,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (x v v))).

given clause #114: (wt=13) 542 [para_into,509,20] 1 v ((0 v (0 v 0)) v 0)=0 v 1.

given clause #115: (wt=13) 582 [para_into,64,44,demod,12] c(0 v x)=1^ (0 v c(x v x)).

given clause #116: (wt=13) 584 [copy,582,flip.1] 1^ (0 v c(x v x))=c(0 v x).

given clause #117: (wt=19) 102 [copy,97,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (x v v))).

given clause #118: (wt=13) 658 [para_into,84,44,demod,12] c(x v 0)= (0 v c(x v x))^1.

given clause #119: (wt=13) 662 [copy,658,flip.1] (0 v c(x v x))^1=c(x v 0).

given clause #120: (wt=13) 708 [back_demod,462,demod,703,703] ((0 v 1) v 1)^ (0 v 1)=0 v 1.

given clause #121: (wt=19) 103 [para_from,14,44] 1^ (x v ((y v (x v z)) v (y v z)))=y v (x v z).

given clause #122: (wt=13) 716 [back_demod,574,demod,703] 1^ (0 v c(0 v 1))=c(0 v 1).

given clause #123: (wt=13) 732 [back_demod,422,demod,703] (x v (0 v 1))^ (0 v (x v 0))=x.

given clause #124: (wt=13) 768 [back_demod,222,demod,703] ((0 v 1) v 0) v ((0 v 0)^1)=1.

given clause #125: (wt=18) 105 [para_from,14,7] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x.

given clause #126: (wt=13) 770 [back_demod,214,demod,703] ((0 v 1) v 0)^ ((0 v 0)^1)=0.

given clause #127: (wt=13) 780 [back_demod,135,demod,703] (0 v 0) v (x v (0 v 1))=x v 1.

given clause #128: (wt=13) 788 [back_demod,72,demod,703] (x v (0 v 1))^ (x v (0 v 0))=x.

given clause #129: (wt=19) 107 [para_from,14,2] x v (y v (z v (u v v)))=z v (x v (u v (y v v))).

given clause #130: (wt=13) 794 [para_from,702,28,demod,12,12] c(c(x) v (0 v 1))=x^ (0 v 0).

given clause #131: (wt=13) 820 [para_from,786,15,flip.1] (0 v 0) v (0 v (x v 1))=x v 1.

given clause #132: (wt=13) 824 [para_into,92,778,flip.1] 1 v (x v (0 v (0 v 0)))=x v 1.

given clause #133: (wt=19) 108 [copy,107,flip.1] x v (y v (z v (u v v)))=y v (u v (x v (z v v))).

given clause #134: (wt=13) 840 [para_from,806,15,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1.

given clause #135: (wt=13) 849 [para_from,806,2,flip.1] 0 v (x v (1 v (0 v 0)))=x v 1.

given clause #136: (wt=13) 851 [para_from,808,15,flip.1] 1 v (0 v (x v (0 v 0)))=x v 1.

given clause #137: (wt=16) 111 [para_into,50,26] ((c(x) v 0) v c(x^1))^1=c(x) v 0.

given clause #138: (wt=13) 859 [para_into,772,119] 0 v (1 v (0 v (x v 0)))=x v 1.

given clause #139: (wt=13) 860 [para_into,772,39] 0 v (0 v (1 v (x v 0)))=x v 1.

given clause #140: (wt=13) 861 [copy,859,flip.1] x v 1=0 v (1 v (0 v (x v 0))).

given clause #141: (wt=16) 113 [para_into,50,22] ((0 v c(x)) v c(1^x))^1=0 v c(x).

given clause #142: (wt=13) 862 [copy,860,flip.1] x v 1=0 v (0 v (1 v (x v 0))).

given clause #143: (wt=11) 1326 [back_demod,1321,demod,1325] c(1 v (x v 0))=c(x v 1).

given clause #144: (wt=11) 1327 [back_demod,1318,demod,1325] c(x v 1)=c(1 v (x v 0)).

given clause #145: (wt=18) 115 [para_into,50,4] ((c(x) v c(y)) v c(x^y))^1=c(x) v c(y).

given clause #146: (wt=12) 1337 [para_from,1326,30] (1 v (x v 0))^c(x v 1)=0.

given clause #147: (wt=12) 1350 [para_from,1326,9] (1 v (x v 0)) v c(x v 1)=1.

given clause #148: (wt=12) 1366 [para_from,1327,30] (x v 1)^c(1 v (x v 0))=0.

given clause #149: (wt=17) 117 [para_into,15,21] x v (y v (z v 1))=y v (1 v (x v (z v 0))).

given clause #150: (wt=12) 1378 [para_from,1327,9] (x v 1) v c(1 v (x v 0))=1.

given clause #151: (wt=13) 863 [para_into,792,20] (1 v (1 v (0 v 0)))^ (0 v 1)=1.

given clause #152: (wt=13) 877 [para_into,810,92] 1 v (0 v (0 v (x v 0)))=x v 1.

given clause #153: (wt=17) 118 [para_into,15,20] x v (y v (1 v (z v 0)))=y v (z v (x v 1)).

given clause #154: (wt=13) 878 [copy,877,flip.1] x v 1=1 v (0 v (0 v (x v 0))).

given clause #155: (wt=13) 1187 [para_into,732,2] (0 v (x v 1))^ (0 v (x v 0))=x.

given clause #156: (wt=13) 1229 [para_into,788,2] (0 v (x v 1))^ (x v (0 v 0))=x.

given clause #157: (wt=19) 120 [para_into,15,15] x v (y v (z v (u v v)))=u v (y v (x v (z v v))).

given clause #158: (wt=13) 1247 [para_into,794,2] c(0 v (c(x) v 1))=x^ (0 v 0).

given clause #159: (wt=13) 1295 [para_into,840,178,demod,1232,flip.1] ((1 v 1)^1) v 1=0 v (1 v 1).

given clause #160: (wt=13) 1343 [para_from,1326,26,demod,27] (x v 1)^1= (1 v (x v 0))^1.

given clause #161: (wt=19) 121 [para_into,15,14] x v (y v (z v (u v v)))=z v (u v (x v (y v v))).

given clause #162: (wt=13) 1357 [copy,1343,flip.1] (1 v (x v 0))^1= (x v 1)^1.

given clause #163: (wt=13) 1397 [para_from,1350,18] (x v 1) v 1= (1 v (x v 0)) v 1.

given clause #164: (wt=13) 1399 [copy,1397,flip.1] (1 v (x v 0)) v 1= (x v 1) v 1.

given clause #165: (wt=15) 122 [para_into,15,2] x v (y v (z v u))=x v (z v (y v u)).

given clause #166: (wt=14) 137 [para_into,18,26] (c(x) v 0) v (y v (x^1))=y v 1.

given clause #167: (wt=14) 139 [para_into,18,22] (0 v c(x)) v (y v (1^x))=y v 1.

given clause #168: (wt=14) 149 [para_into,68,26] (0 v (x^1))^ (1^ (c(x) v 0))=0.

given clause #169: (wt=17) 123 [copy,117,flip.1] x v (1 v (y v (z v 0)))=y v (x v (z v 1)).

given clause #170: (wt=14) 151 [para_into,68,22] (0 v (1^x))^ (1^ (0 v c(x)))=0.

given clause #171: (wt=14) 176 [para_into,70,26] (0 v (x^1)) v (1^ (c(x) v 0))=1.

given clause #172: (wt=14) 199 [para_into,28,44,demod,12] c(c(x) v y)=x^ (0 v c(y v y)).

given clause #173: (wt=17) 124 [copy,118,flip.1] x v (y v (z v 1))=z v (x v (1 v (y v 0))).

given clause #174: (wt=14) 201 [copy,199,flip.1] x^ (0 v c(y v y))=c(c(x) v y).

given clause #175: (wt=11) 1624 [para_into,201,7,demod,161,791,10,flip.1] c((1^c(x v x)) v x)=0.

given clause #176: (wt=12) 1664 [para_from,1624,30] ((1^c(x v x)) v x)^0=0.

given clause #177: (wt=19) 126 [copy,120,flip.1] x v (y v (z v (u v v)))=z v (y v (u v (x v v))).

given clause #178: (wt=12) 1683 [para_from,1624,9] ((1^c(x v x)) v x) v 0=1.

given clause #179: (wt=10) 1705 [para_from,1683,1187,demod,1704,866,flip.1] (1^c(x v x)) v x=1.

given clause #180: (wt=12) 1725 [para_into,1705,20] 1 v ((1^c(1 v 1)) v 0)=1.

given clause #181: (wt=19) 127 [para_from,15,44] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z).

given clause #182: (wt=14) 216 [para_into,88,26] ((x^1) v 0)^ ((c(x) v 0)^1)=0.

given clause #183: (wt=14) 220 [para_into,88,48,demod,161,17,12] (((0 v c(1 v 1))^0) v 0)^1=0.

given clause #184: (wt=14) 224 [para_into,90,26] ((x^1) v 0) v ((c(x) v 0)^1)=1.

given clause #185: (wt=19) 129 [para_from,15,14] x v (y v (z v (u v v)))=y v (x v (u v (z v v))).

given clause #186: (wt=14) 228 [para_into,90,48,demod,161,17,12] (((0 v c(1 v 1))^0) v 0) v 1=1.

given clause #187: (wt=14) 258 [para_from,178,2] x v 1= (0 v c(y v y)) v (x v y).

given clause #188: (wt=14) 261 [copy,258,flip.1] (0 v c(x v x)) v (y v x)=y v 1.

given clause #189: (wt=18) 130 [para_from,15,7] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x.

given clause #190: (wt=14) 353 [para_from,292,7] (1 v c((0 v 0) v 0))^ (0 v 1)=1.

given clause #191: (wt=14) 376 [para_into,42,44,demod,12] (x v y)^ (x v (0 v c(y v y)))=x.

given clause #192: (wt=14) 424 [para_into,52,26] (x v (y^1))^ (c(y) v (x v 0))=x.

given clause #193: (wt=15) 141 [para_into,18,4] (c(x) v c(y)) v (z v (x^y))=z v 1.

given clause #194: (wt=14) 476 [para_into,390,20] (x v (y^x))^ (1 v (c(y) v 0))=x.

given clause #195: (wt=14) 492 [para_into,54,178,demod,179] 1^ ((0 v c(x v x)) v (1 v x))=1.

given clause #196: (wt=14) 520 [para_from,505,2,flip.1] 0 v (x v c(0 v (0 v 0)))=x v 1.

given clause #197: (wt=18) 143 [para_from,18,14,flip.1] x v (y v (z v (u v c(x))))=y v (z v (u v 1)).

given clause #198: (wt=14) 522 [para_from,507,70] (0 v c(0 v (0 v (0 v 0)))) v 0=1.

given clause #199: (wt=12) 1919 [para_from,522,1187,demod,1918,866,flip.1] 0 v c(0 v (0 v (0 v 0)))=1.

given clause #200: (wt=13) 1921 [para_from,1919,130] 1^ (0 v (0 v (0 v (0 v 0))))=0.

given clause #201: (wt=15) 153 [para_into,68,4] (0 v (x^y))^ (1^ (c(x) v c(y)))=0.

given clause #202: (wt=10) 1951 [para_into,153,44] (0 v (x^x))^c(x)=0.

given clause #203: (wt=13) 1924 [para_from,1919,18] (0 v (0 v (0 v 0))) v 1=0 v 1.

given clause #204: (wt=14) 618 [para_into,66,2] (x v (1^y))^ (0 v (x v c(y)))=x.

given clause #205: (wt=17) 160 [para_into,24,40] c(x v c(y))= (c(x v 0) v c(x v 1))^y.

given clause #206: (wt=14) 738 [back_demod,370,demod,703] (x v 1)^ (x v (0 v c(0 v 1)))=x.

given clause #207: (wt=14) 743 [back_demod,346,demod,703] (0 v c(0 v 1)) v (x v 1)=x v 1.

given clause #208: (wt=14) 756 [back_demod,290,demod,703] (0 v c(x v (0 v 1)))^ (x v 1)=0.

given clause #209: (wt=19) 166 [para_into,24,26] c((x^y) v (z^1))= (c(x) v c(y))^ (c(z) v 0).

given clause #210: (wt=14) 760 [back_demod,272,demod,703] (c(x) v (0 v 1))^ (x^ (0 v 0))=0.

given clause #211: (wt=14) 762 [back_demod,268,demod,703] ((0 v 1) v c(x))^ ((0 v 0)^x)=0.

given clause #212: (wt=14) 764 [back_demod,236,demod,703] (c(x) v (0 v 1)) v (x^ (0 v 0))=1.

given clause #213: (wt=19) 168 [para_into,24,22] c((x^y) v (1^z))= (c(x) v c(y))^ (0 v c(z)).

given clause #214: (wt=14) 766 [back_demod,232,demod,703] ((0 v 1) v c(x)) v ((0 v 0)^x)=1.

given clause #215: (wt=14) 784 [back_demod,109,demod,703] ((0 v 0) v c(0 v 1))^1=0 v 0.

given clause #216: (wt=14) 879 [para_from,810,52] (0 v c(0 v (x v 1)))^ (x v 1)=0.

given clause #217: (wt=19) 170 [back_demod,145,demod,161] (x v ((c(y v 0) v c(y v 1))^x))^ (y v 1)=x.

given clause #218: (wt=14) 889 [para_from,816,52] (1 v c((0 v 0) v (0 v 0)))^1=1.

given clause #219: (wt=14) 955 [para_into,796,20] c((1 v (0 v 0)) v 0)= (0 v 0)^1.

given clause #220: (wt=14) 1044 [para_from,516,390,demod,17,161,791,10] 1^ ((1^c(0 v (0 v 0))) v 1)=1.

given clause #221: (wt=18) 180 [para_from,70,14,flip.1] (0 v c(x)) v (y v (z v (1^x)))=y v (z v 1).

given clause #222: (wt=14) 1048 [para_from,516,90,demod,161,791,10] ((1^c(0 v (0 v 0))) v 0) v 0=1.

given clause #223: (wt=12) 2127 [para_from,1048,54,demod,1045,flip.1] (1^c(0 v (0 v 0))) v 0=1.

given clause #224: (wt=10) 2135 [para_from,2127,1187,demod,2132,866,flip.1] 1^c(0 v (0 v 0))=1.

given clause #225: (wt=19) 195 [para_into,28,26] c((x^1) v (y^z))= (c(x) v 0)^ (c(y) v c(z)).

given clause #226: (wt=11) 2137 [para_into,2135,582,demod,1232] 1^ (1^ ((1 v 1)^1))=1.

given clause #227: (wt=13) 2147 [para_from,2135,70] (0 v c(c(0 v (0 v 0)))) v 1=1.

given clause #228: (wt=14) 1092 [back_demod,834,demod,1069] (0 v (1^ (0 v c(1 v 1))))^1=0.

given clause #229: (wt=18) 197 [para_into,28,48,demod,161,17,12,12] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0).

given clause #230: (wt=14) 1094 [back_demod,832,demod,1069] (0 v (1^ (0 v c(1 v 1)))) v 1=1.

given clause #231: (wt=14) 1110 [para_from,582,30] (0 v x)^ (1^ (0 v c(x v x)))=0.

given clause #232: (wt=14) 1122 [para_from,582,9] (0 v x) v (1^ (0 v c(x v x)))=1.

given clause #233: (wt=17) 200 [para_into,28,40] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)).

given clause #234: (wt=14) 1151 [para_from,658,30] (x v 0)^ ((0 v c(x v x))^1)=0.

given clause #235: (wt=14) 1163 [para_from,658,9] (x v 0) v ((0 v c(x v x))^1)=1.

given clause #236: (wt=14) 1213 [para_into,105,816] (1 v c(0 v ((0 v 0) v 0)))^1=1.

given clause #237: (wt=17) 202 [copy,200,flip.1] x^ (c(y v 0) v c(y v 1))=c(c(x) v y).

given clause #238: (wt=14) 1456 [para_from,1247,30] (0 v (c(x) v 1))^ (x^ (0 v 0))=0.

given clause #239: (wt=14) 1470 [para_from,1247,9] (0 v (c(x) v 1)) v (x^ (0 v 0))=1.

given clause #240: (wt=14) 1751 [para_from,1705,54,demod,1706] 1^ ((1^c(x v x)) v (1 v x))=1.

given clause #241: (wt=16) 203 [para_from,28,30] (c(x) v (y^z))^ (x^ (c(y) v c(z)))=0.

given clause #242: (wt=14) 1755 [para_from,1705,2] x v 1= (1^c(y v y)) v (x v y).

given clause #243: (wt=14) 1762 [copy,1755,flip.1] (1^c(x v x)) v (y v x)=y v 1.

given clause #244: (wt=14) 1805 [para_from,258,778] 0 v ((0 v c(x v x)) v (0 v x))=1.

given clause #245: (wt=16) 205 [para_from,28,9] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1.

given clause #246: (wt=10) 2369 [para_into,205,44,demod,12] (0 v (x^x)) v c(x)=1.

given clause #247: (wt=11) 2377 [para_from,2369,18,flip.1] (0 v (x^x)) v 1=x v 1.

given clause #248: (wt=13) 2402 [para_into,2377,20] 1 v ((0 v (x^x)) v 0)=x v 1.

given clause #249: (wt=18) 218 [para_into,88,50,demod,161] (((c(x v 0) v c(x v 1))^c(x)) v 0)^x=0.

given clause #250: (wt=10) 2432 [para_into,218,790,demod,10] ((1^c(0)) v 0)^0=0.

given clause #251: (wt=14) 1807 [para_from,258,754] 1^ ((0 v c(x v x)) v (0 v x))=1.

given clause #252: (wt=14) 1867 [para_into,376,2] (x v y)^ (0 v (x v c(y v y)))=x.

given clause #253: (wt=18) 226 [para_into,90,50,demod,161] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1.

given clause #254: (wt=8) 2463 [para_from,226,1187,demod,791,10,2462,866,791,10,flip.1] (1^c(0)) v 0=1.

given clause #255: (wt=6) 2479 [para_from,2463,1187,demod,2468,866,flip.1] 1^c(0)=1.

given clause #256: (wt=9) 2495 [para_from,2479,70] (0 v c(c(0))) v 1=1.

given clause #257: (wt=18) 230 [para_from,90,14,flip.1] (c(x) v 0) v (y v (z v (x^1)))=y v (z v 1).

given clause #258: (wt=11) 2483 [para_from,2479,390,demod,12] (c(0) v 1)^ (0 v 1)=c(0).

given clause #259: (wt=11) 2501 [para_into,2495,20] 1 v ((0 v c(c(0))) v 0)=1.

given clause #260: (wt=13) 2481 [para_from,2479,476,demod,12] (c(0) v 1)^ (1 v (0 v 0))=c(0).

given clause #261: (wt=15) 234 [para_into,32,26] ((x^1) v c(y)) v ((c(x) v 0)^y)=1.

given clause #262: (wt=13) 2485 [para_from,2479,618] (x v 1)^ (0 v (x v c(c(0))))=x.

given clause #263: (wt=10) 2564 [para_into,2485,2369,demod,2378,2484,flip.1] 0 v (c(0)^c(0))=c(0).

given clause #264: (wt=13) 2487 [para_from,2479,66] (x v 1)^ (x v (0 v c(c(0))))=x.

given clause #265: (wt=15) 238 [para_into,32,26] (c(x) v (y^1)) v (x^ (c(y) v 0))=1.

given clause #266: (wt=13) 2491 [para_from,2479,139] (0 v c(c(0))) v (x v 1)=x v 1.

given clause #267: (wt=13) 2532 [para_into,2483,20] (1 v (c(0) v 0))^ (0 v 1)=c(0).

given clause #268: (wt=13) 2583 [para_from,2564,7] (0 v c(c(0)^c(0)))^c(0)=0.

given clause #269: (wt=19) 242 [para_from,32,14,flip.1] (c(x) v c(y)) v (z v (u v (x^y)))=z v (u v 1).

given clause #270: (wt=14) 1973 [para_into,618,754] (x v 1)^ (0 v (x v c(0 v 1)))=x.

given clause #271: (wt=13) 2637 [para_into,1973,2369,demod,2378,709,flip.1] 0 v ((0 v 1)^ (0 v 1))=0 v 1.

given clause #272: (wt=14) 1995 [para_into,756,794] (0 v (x^ (0 v 0)))^ (c(x) v 1)=0.

given clause #273: (wt=16) 244 [para_into,155,2] (0 v c(x v ((x v y) v y)))^ (x v y)=0.

given clause #274: (wt=14) 2037 [para_into,760,276,demod,287,1441] (c((1 v 1)^1) v (0 v 1))^0=0.

given clause #275: (wt=14) 2055 [para_into,764,276,demod,287,1441] (c((1 v 1)^1) v (0 v 1)) v 0=1.

given clause #276: (wt=12) 2697 [para_from,2055,1187,demod,2258,2696,866,flip.1] c((1 v 1)^1) v (0 v 1)=1.

given clause #277: (wt=16) 246 [para_into,178,2] (0 v c(x v ((x v y) v y))) v (x v y)=1.

given clause #278: (wt=11) 2717 [para_from,2697,794,demod,12,flip.1] ((1 v 1)^1)^ (0 v 0)=0.

given clause #279: (wt=12) 2721 [para_from,2697,780,demod,287,flip.1] c((1 v 1)^1) v 1=0 v 1.

given clause #280: (wt=14) 2161 [para_from,2137,70] (0 v c(1^ ((1 v 1)^1))) v 1=1.

given clause #281: (wt=16) 250 [para_into,178,2] x v ((0 v c((x v y) v (x v y))) v y)=1.

given clause #282: (wt=13) 2803 [para_into,250,1924,demod,1925,1236,2378,287] (0 v (0 v (0 v 0))) v (0 v 1)=1.

given clause #283: (wt=14) 2163 [para_from,2137,68] (0 v c(1^ ((1 v 1)^1)))^1=0.

given clause #284: (wt=14) 2305 [para_from,1755,778] 0 v ((1^c(x v x)) v (0 v x))=1.

given clause #285: (wt=17) 252 [para_from,178,40] ((0 v c(1 v 1)) v 0)^1=0 v c(1 v 1).

given clause #286: (wt=14) 2307 [para_from,1755,754] 1^ ((1^c(x v x)) v (0 v x))=1.

given clause #287: (wt=14) 2341 [para_into,1805,15] (0 v c(x v x)) v (0 v (0 v x))=1.

given clause #288: (wt=14) 2396 [para_from,2369,2,flip.1] (0 v (x^x)) v (y v c(x))=y v 1.

given clause #289: (wt=18) 254 [para_from,178,15] x v (y v 1)=y v ((0 v c(z v z)) v (x v z)).

given clause #290: (wt=14) 2522 [para_from,2495,56] (1 v c((0 v c(c(0))) v 0))^1=1.

given clause #291: (wt=14) 2572 [para_from,2564,141] (c(c(0)) v c(c(0))) v c(0)=0 v 1.

given clause #292: (wt=11) 2868 [para_from,2572,2396,demod,2863,779,flip.1] (c(c(0)) v c(c(0))) v 1=1.

given clause #293: (wt=18) 255 [para_from,178,14] x v (y v 1)= (0 v c(z v z)) v (x v (y v z)).

given clause #294: (wt=13) 2878 [para_into,2868,20] 1 v ((c(c(0)) v c(c(0))) v 0)=1.

given clause #295: (wt=14) 2574 [para_from,2564,42] c(0)^ (0 v (c(c(0)) v c(c(0))))=0.

given clause #296: (wt=14) 2589 [para_from,2564,2,flip.1] 0 v (x v (c(0)^c(0)))=x v c(0).

given clause #297: (wt=18) 256 [para_from,178,7] ((0 v c(x v x)) v c(x))^1=0 v c(x v x).

given clause #298: (wt=14) 2707 [para_into,2697,20] c((1 v 1)^1) v (1 v (0 v 0))=1.

given clause #299: (wt=14) 2711 [para_into,2697,58] 1 v (c((1 v 1)^1) v (0 v 0))=1.

given clause #300: (wt=14) 2781 [para_into,2721,20] 1 v (c((1 v 1)^1) v 0)=0 v 1.

given clause #301: (wt=18) 259 [copy,254,flip.1] x v ((0 v c(y v y)) v (z v y))=z v (x v 1).

given clause #302: (wt=14) 2841 [para_into,2305,15] (1^c(x v x)) v (0 v (0 v x))=1.

given clause #303: (wt=14) 2913 [para_into,2574,2] c(0)^ (c(c(0)) v (0 v c(c(0))))=0.

given clause #304: (wt=15) 270 [para_into,36,26] ((x^1) v c(y))^ ((c(x) v 0)^y)=0.

given clause #305: (wt=18) 260 [copy,255,flip.1] (0 v c(x v x)) v (y v (z v x))=y v (z v 1).

given clause #306: (wt=15) 274 [para_into,36,26] (c(x) v (y^1))^ (x^ (c(y) v 0))=0.

given clause #307: (wt=15) 279 [para_from,46,36] (c(x v 0) v c(1 v (x v 0)))^x=0.

given clause #308: (wt=15) 281 [para_from,46,32] (c(x v 0) v c(1 v (x v 0))) v x=1.

given clause #309: (wt=19) 278 [para_from,46,28] c(c(x) v y)=x^ (c(y v 0) v c(1 v (y v 0))).

given clause #310: (wt=11) 2957 [para_into,281,292,demod,1441] ((1 v 1)^1) v (0 v 0)=1.

given clause #311: (wt=11) 2969 [para_into,2957,2] 0 v (((1 v 1)^1) v 0)=1.

given clause #312: (wt=13) 2971 [para_from,2957,260,demod,791,779,flip.1] ((1 v 1)^1) v (0 v 1)=1 v 1.

given clause #313: (wt=19) 283 [copy,278,flip.1] x^ (c(y v 0) v c(1 v (y v 0)))=c(c(x) v y).

given clause #314: (wt=14) 2984 [para_from,2957,52,demod,85,12] (0 v ((c(1 v 1) v 0)^1))^1=0.

given clause #315: (wt=15) 318 [para_into,39,286] x v (0 v 1)= (0 v 0) v (1 v (x v 0)).

given clause #316: (wt=15) 330 [para_from,39,44] 1^ (x v (1 v ((x v 1) v 0)))=x v 1.

given clause #317: (wt=17) 297 [para_from,286,14] x v (y v (0 v 1))= (0 v 0) v (x v (y v 1)).

given clause #318: (wt=15) 349 [para_from,292,15] x v (0 v 1)=1 v ((0 v 0) v (x v 0)).

given clause #319: (wt=15) 355 [para_from,292,2,flip.1] 1 v (x v ((0 v 0) v 0))=x v (0 v 1).

given clause #320: (wt=15) 364 [para_into,56,178] (1 v c((0 v c(1 v 1)) v 0))^1=1.

given clause #321: (wt=17) 302 [para_from,38,44] 1^ (x v ((1 v (x v 0)) v 1))=1 v (x v 0).

given clause #322: (wt=15) 392 [para_into,42,2] (x v (y^z))^ (c(y) v (x v c(z)))=x.

given clause #323: (wt=15) 485 [para_from,474,36] (c(x v (1^x)) v c(0 v 1))^x=0.

given clause #324: (wt=15) 487 [para_from,474,32] (c(x v (1^x)) v c(0 v 1)) v x=1.

given clause #325: (wt=17) 304 [para_from,38,15] x v (y v (z v 1))=z v (1 v (x v (y v 0))).

given clause #326: (wt=15) 496 [para_into,54,39] 1^ ((x v 1) v (1 v (x v 0)))=x v 1.

given clause #327: (wt=15) 532 [para_from,58,54] 1^ (1 v (x v ((x v 1) v 0)))=x v 1.

given clause #328: (wt=15) 600 [para_from,64,9] (0 v (x^y)) v (1^ (c(x) v c(y)))=1.

given clause #329: (wt=17) 305 [para_from,38,14] x v (y v (z v 1))=1 v (x v (z v (y v 0))).

given clause #330: (wt=14) 3157 [para_into,600,11] (0 v (1^x)) v (1^ (0 v c(x)))=1.

given clause #331: (wt=15) 669 [para_from,84,30] ((x^y) v 0)^ ((c(x) v c(y))^1)=0.

given clause #332: (wt=12) 3179 [para_into,669,50] ((x^c(c(x))) v 0)^c(x)=0.

given clause #333: (wt=16) 306 [para_from,38,7] (x v c(1 v (y v 0)))^ (y v (x v 1))=x.

given clause #334: (wt=14) 3175 [para_into,669,11] ((1^x) v 0)^ ((0 v c(x))^1)=0.

given clause #335: (wt=15) 681 [para_from,84,9] ((x^y) v 0) v ((c(x) v c(y))^1)=1.

given clause #336: (wt=12) 3197 [para_into,681,50] ((x^c(c(x))) v 0) v c(x)=1.

given clause #337: (wt=17) 308 [copy,304,flip.1] x v (1 v (y v (z v 0)))=y v (z v (x v 1)).

given clause #338: (wt=13) 3204 [para_from,3197,2396,demod,2378,flip.1] ((x^c(c(x))) v 0) v 1=x v 1.

given clause #339: (wt=14) 3193 [para_into,681,11] ((1^x) v 0) v ((0 v c(x))^1)=1.

given clause #340: (wt=15) 706 [back_demod,470,demod,703] (x v ((0 v 0)^x))^ ((0 v 1) v 1)=x.

given clause #341: (wt=17) 309 [copy,305,flip.1] 1 v (x v (y v (z v 0)))=x v (z v (y v 1)).

given clause #342: (wt=15) 740 [back_demod,362,demod,703] (1 v c((0 v c(0 v 1)) v 0))^1=1.

given clause #343: (wt=15) 776 [back_demod,208,demod,703] 0 v (x v (y v (0 v 1)))=x v (y v 1).

given clause #344: (wt=15) 822 [para_into,92,786,flip.1] 1 v (x v ((0 v 0) v (0 v 0)))=x v 1.

given clause #345: (wt=16) 319 [para_into,39,178] x v 1= (0 v c(1 v 1)) v (1 v (x v 0)).

given clause #346: (wt=15) 871 [para_from,792,84,demod,17,12,flip.1] (c(1 v (0 v 1)) v c(0 v 1))^1=0.

given clause #347: (wt=15) 875 [para_from,792,32] (c(1 v (0 v 1)) v c(0 v 1)) v 1=1.

given clause #348: (wt=15) 881 [para_from,810,15,flip.1] 0 v (0 v (x v (y v 1)))=x v (y v 1).

given clause #349: (wt=18) 320 [para_into,39,178,flip.1] x v (1 v ((0 v c((x v 1) v (x v 1))) v 0))=1.

given clause #350: (wt=15) 883 [para_from,810,14,flip.1] 0 v (x v (0 v (y v 1)))=x v (y v 1).

given clause #351: (wt=15) 891 [para_from,816,15,flip.1] (0 v 0) v (1 v (x v (0 v 0)))=x v 1.

given clause #352: (wt=15) 900 [para_from,816,2,flip.1] (0 v 0) v (x v (1 v (0 v 0)))=x v 1.

given clause #353: (wt=18) 326 [para_from,39,178] (0 v c(x v (1 v ((x v 1) v 0)))) v (x v 1)=1.

given clause #354: (wt=15) 907 [para_from,818,15,flip.1] 1 v ((0 v 0) v (x v (0 v 0)))=x v 1.

given clause #355: (wt=15) 917 [para_from,865,84,demod,17,12,flip.1] (c(0 v (1 v 1)) v c(0 v 1))^1=0.

given clause #356: (wt=15) 921 [para_from,865,32] (c(0 v (1 v 1)) v c(0 v 1)) v 1=1.

given clause #357: (wt=18) 328 [para_from,39,155] (0 v c(x v (1 v ((x v 1) v 0))))^ (x v 1)=0.

given clause #358: (wt=15) 1014 [para_into,298,119,flip.1] (0 v 0) v (x v 1)=1 v (0 v (x v 0)).

given clause #359: (wt=15) 1028 [para_into,466,20] (1 v ((1 v 1) v 0))^ (0 v 1)=1 v 1.

given clause #360: (wt=15) 1030 [para_into,466,20] ((x v x) v x)^ (1 v (0 v 0))=x v x.

given clause #361: (wt=17) 332 [para_from,39,15] x v (y v (1 v (z v 0)))=z v (y v (x v 1)).

given clause #362: (wt=15) 1057 [para_into,101,818] x v 1=1 v ((0 v 0) v (0 v (x v 0))).

given clause #363: (wt=15) 1058 [para_into,101,816] x v 1= (0 v 0) v (1 v (0 v (x v 0))).

given clause #364: (wt=15) 1068 [para_into,582,20] c(1 v (0 v 0))=1^ (0 v c(1 v 1)).

given clause #365: (wt=17) 333 [para_from,39,14] x v (y v (1 v (z v 0)))=y v (x v (z v 1)).

given clause #366: (wt=15) 1128 [para_into,102,818] x v 1=1 v (0 v ((0 v 0) v (x v 0))).

given clause #367: (wt=15) 1129 [para_into,102,816] x v 1= (0 v 0) v (0 v (1 v (x v 0))).

given clause #368: (wt=15) 1169 [para_into,708,20] (1 v ((0 v 1) v 0))^ (0 v 1)=0 v 1.

given clause #369: (wt=16) 334 [para_from,39,7] (x v c(y v 1))^ (y v (1 v (x v 0)))=x.

given clause #370: (wt=13) 3344 [para_into,334,2369,demod,2403,55,flip.1] 0 v ((x v 1)^ (x v 1))=x v 1.

given clause #371: (wt=15) 1179 [para_into,732,20] (x v (1 v (0 v 0)))^ (0 v (x v 0))=x.

given clause #372: (wt=15) 1181 [para_into,732,119] (1 v (0 v (x v 0)))^ (0 v (x v 0))=x.

given clause #373: (wt=17) 336 [copy,332,flip.1] x v (y v (z v 1))=z v (y v (1 v (x v 0))).

given clause #374: (wt=15) 1183 [para_into,732,58] (1 v (x v (0 v 0)))^ (0 v (x v 0))=x.

given clause #375: (wt=15) 1185 [para_into,732,39] (0 v (1 v (x v 0)))^ (0 v (x v 0))=x.

given clause #376: (wt=15) 1193 [para_into,768,20] ((1 v (0 v 0)) v 0) v ((0 v 0)^1)=1.

given clause #377: (wt=17) 337 [copy,333,flip.1] x v (y v (z v 1))=y v (x v (1 v (z v 0))).

given clause #378: (wt=15) 1215 [para_into,770,20] ((1 v (0 v 0)) v 0)^ ((0 v 0)^1)=0.

given clause #379: (wt=15) 1221 [para_into,788,20] (x v (1 v (0 v 0)))^ (x v (0 v 0))=x.

given clause #380: (wt=15) 1223 [para_into,788,119] (1 v (0 v (x v 0)))^ (x v (0 v 0))=x.

given clause #381: (wt=19) 351 [para_from,292,14,flip.1] 1 v (x v (y v ((0 v 0) v 0)))=x v (y v (0 v 1)).

given clause #382: (wt=15) 1225 [para_into,788,58] (1 v (x v (0 v 0)))^ (x v (0 v 0))=x.

given clause #383: (wt=15) 1227 [para_into,788,39] (0 v (1 v (x v 0)))^ (x v (0 v 0))=x.

given clause #384: (wt=15) 1239 [para_into,794,20] c(c(x) v (1 v (0 v 0)))=x^ (0 v 0).

given clause #385: (wt=19) 366 [para_from,56,36,demod,161,17,12] (((0 v c(1 v 1))^ (x v 0)) v c(x v 1))^1=0.

given clause #386: (wt=15) 1241 [para_into,794,119] c(1 v (0 v (c(x) v 0)))=x^ (0 v 0).

given clause #387: (wt=15) 1243 [para_into,794,58] c(1 v (c(x) v (0 v 0)))=x^ (0 v 0).

given clause #388: (wt=15) 1245 [para_into,794,39] c(0 v (1 v (c(x) v 0)))=x^ (0 v 0).

given clause #389: (wt=19) 368 [para_from,56,32,demod,161,17,12] (((0 v c(1 v 1))^ (x v 0)) v c(x v 1)) v 1=1.

given clause #390: (wt=15) 1322 [para_into,861,20,flip.1] 0 v (1 v (0 v (x v 0)))=1 v (x v 0).

given clause #391: (wt=15) 1324 [para_into,862,20,flip.1] 0 v (0 v (1 v (x v 0)))=1 v (x v 0).

given clause #392: (wt=15) 1430 [para_into,878,20,flip.1] 1 v (0 v (0 v (x v 0)))=1 v (x v 0).

given clause #393: (wt=18) 372 [para_into,42,48,demod,161,17,12,12] (x v 1)^ (x v (((0 v c(1 v 1))^0) v 0))=x.

given clause #394: (wt=15) 1476 [para_into,1295,20] 1 v (((1 v 1)^1) v 0)=0 v (1 v 1).

given clause #395: (wt=15) 1507 [para_into,1397,20] 1 v ((x v 1) v 0)= (1 v (x v 0)) v 1.

given clause #396: (wt=15) 1509 [copy,1507,flip.1] (1 v (x v 0)) v 1=1 v ((x v 1) v 0).

given clause #397: (wt=19) 374 [para_into,42,46] (x v y)^ (x v (c(y v 0) v c(1 v (y v 0))))=x.

given clause #398: (wt=15) 1534 [para_into,1399,20] 1 v ((1 v (x v 0)) v 0)= (x v 1) v 1.

given clause #399: (wt=15) 1535 [copy,1534,flip.1] (x v 1) v 1=1 v ((1 v (x v 0)) v 0).

given clause #400: (wt=15) 1606 [para_from,199,30] (c(x) v y)^ (x^ (0 v c(y v y)))=0.

given clause #401: (wt=17) 378 [para_into,42,40] (x v y)^ (x v (c(y v 0) v c(y v 1)))=x.

given clause #402: (wt=15) 1618 [para_from,199,9] (c(x) v y) v (x^ (0 v c(y v y)))=1.

given clause #403: (wt=15) 1743 [para_from,1705,56,demod,85,12] (1 v ((0 v c(c(1 v 1)))^1))^1=1.

given clause #404: (wt=15) 1859 [para_into,376,778,demod,1236] 1^ (0 v (0 v ((0 v 0)^ (0 v 0))))=0.

given clause #405: (wt=19) 384 [para_into,42,26] (x v ((c(y) v 0)^z))^ (x v ((y^1) v c(z)))=x.

given clause #406: (wt=15) 1909 [para_into,520,582,demod,1232] 0 v (x v (1^ ((1 v 1)^1)))=x v 1.

given clause #407: (wt=14) 3518 [para_into,1909,1705,demod,169,12,2340,flip.1] (0 v c((1 v 1)^1)) v 1=0 v 1.

given clause #408: (wt=15) 1911 [para_from,520,94] (0 v (0 v 0)) v (x v 1)=0 v (x v 1).

given clause #409: (wt=19) 388 [para_into,42,26] (x v (y^ (c(z) v 0)))^ (x v (c(y) v (z^1)))=x.

given clause #410: (wt=15) 1928 [para_from,1919,7] (0 v c(c(0 v (0 v (0 v 0)))))^1=0.

given clause #411: (wt=15) 1955 [para_into,1951,790] (0 v ((0 v 0)^ (0 v 0)))^ (0 v 1)=0.

given clause #412: (wt=15) 1959 [para_into,1924,20] 1 v ((0 v (0 v (0 v 0))) v 0)=0 v 1.

given clause #413: (wt=19) 394 [para_from,42,36] (c(x v (y^z)) v c(x v (c(y) v c(z))))^x=0.

given clause #414: (wt=15) 2101 [para_into,170,286,demod,1441,287] (x v (((1 v 1)^1)^x))^ (0 v 1)=x.

given clause #415: (wt=15) 2169 [para_into,2147,20] 1 v ((0 v c(c(0 v (0 v 0)))) v 0)=1.

given clause #416: (wt=15) 2243 [para_into,202,286,demod,1441,flip.1] c(c(x) v (0 v 0))=x^ ((1 v 1)^1).

given clause #417: (wt=19) 396 [para_from,42,32] (c(x v (y^z)) v c(x v (c(y) v c(z)))) v x=1.

given clause #418: (wt=11) 3581 [back_demod,505,demod,3576] 0 v (1^ ((1 v 1)^1))=1.

given clause #419: (wt=12) 3599 [para_from,3581,64,demod,12,12,flip.1] 1^ (0 v c((1 v 1)^1))=0.

given clause #420: (wt=13) 3579 [back_demod,838,demod,3576] (1 v (1^ ((1 v 1)^1)))^1=1.

given clause #421: (wt=16) 412 [para_from,248,15] x v 1=1 v ((0 v c(1 v 1)) v (x v 0)).

given clause #422: (wt=14) 3575 [para_into,2243,11] c(0 v (0 v 0))=1^ ((1 v 1)^1).

given clause #423: (wt=14) 3593 [para_from,3581,618] 1^ (0 v (0 v c((1 v 1)^1)))=0.

given clause #424: (wt=15) 2271 [para_into,203,754,demod,12] (c(x) v 1)^ (x^ (0 v c(0 v 1)))=0.

given clause #425: (wt=16) 413 [para_from,248,2,flip.1] 1 v (x v ((0 v c(1 v 1)) v 0))=x v 1.

given clause #426: (wt=12) 3641 [para_into,2271,7,demod,161,791,10] ((1^c(0 v 1)) v 1)^0=0.

given clause #427: (wt=14) 3653 [para_into,3641,20] (1 v ((1^c(0 v 1)) v 0))^0=0.

given clause #428: (wt=15) 2275 [para_into,203,11] (c(x) v (1^y))^ (x^ (0 v c(y)))=0.

given clause #429: (wt=16) 418 [para_into,52,178,demod,12] (x v 0)^ ((0 v c(y v y)) v (x v y))=x.

given clause #430: (wt=12) 3669 [para_into,2275,7,demod,161,791,10] ((1^c(x)) v (1^x))^0=0.

given clause #431: (wt=11) 3687 [para_into,3669,2479] ((1^c(c(0))) v 1)^0=0.

given clause #432: (wt=12) 3693 [para_into,3669,584,demod,161,791,10,45] ((1^x) v c(0 v x))^0=0.

given clause #433: (wt=16) 420 [para_into,52,21] (x v c(y v 1))^ (1 v (x v (y v 0)))=x.

given clause #434: (wt=12) 3711 [para_into,3693,44] (x v c(0 v (x v x)))^0=0.

given clause #435: (wt=12) 3769 [para_into,3711,2] (x v c(x v (0 v x)))^0=0.

given clause #436: (wt=13) 3699 [para_into,3687,20] (1 v ((1^c(c(0))) v 0))^0=0.

given clause #437: (wt=18) 426 [para_into,52,292] (1 v c(x v ((0 v 0) v 0)))^ (x v (0 v 1))=1.

given clause #438: (wt=14) 3749 [para_into,3711,772] ((0 v 1) v c((0 v 1) v 1))^0=0.

given clause #439: (wt=14) 3755 [para_into,3711,119] (1 v c(1 v (1 v (0 v 0))))^0=0.

given clause #440: (wt=15) 2363 [para_into,205,754,demod,12] (c(x) v 1) v (x^ (0 v c(0 v 1)))=1.

given clause #441: (wt=18) 428 [para_into,52,286] ((0 v 0) v c(x v 1))^ (x v (0 v 1))=0 v 0.

given clause #442: (wt=12) 3805 [para_into,2363,7,demod,161,791,10] ((1^c(0 v 1)) v 1) v 0=1.

given clause #443: (wt=10) 3838 [para_from,3805,1187,demod,3828,866,flip.1] (1^c(0 v 1)) v 1=1.

given clause #444: (wt=12) 3850 [para_into,3838,20] 1 v ((1^c(0 v 1)) v 0)=1.

given clause #445: (wt=19) 430 [para_into,52,248] (1 v c(x v ((0 v c(1 v 1)) v 0)))^ (x v 1)=1.

given clause #446: (wt=14) 3844 [para_into,3838,20,demod,1069] (1^ (1^ (0 v c(1 v 1)))) v 1=1.

given clause #447: (wt=14) 3852 [para_from,3838,259,demod,179,flip.1] (1^c(0 v 1)) v (x v 1)=x v 1.

given clause #448: (wt=15) 2367 [para_into,205,11] (c(x) v (1^y)) v (x^ (0 v c(y)))=1.

given clause #449: (wt=16) 436 [para_into,52,21] (1 v c(x v (y v 0)))^ (x v (y v 1))=1.

given clause #450: (wt=12) 3895 [para_into,2367,7,demod,161,791,10] ((1^c(x)) v (1^x)) v 0=1.

given clause #451: (wt=10) 3928 [para_from,3895,1187,demod,3924,866,flip.1] (1^c(x)) v (1^x)=1.

given clause #452: (wt=10) 3964 [para_into,3928,584,demod,161,791,10,45] (1^x) v c(0 v x)=1.

given clause #453: (wt=17) 438 [para_into,52,18] (x v c(y v (z v c(x))))^ (y v (z v 1))=x.

given clause #454: (wt=10) 4033 [para_into,3964,44] x v c(0 v (x v x))=1.

given clause #455: (wt=10) 4204 [para_into,4033,2] x v c(x v (0 v x))=1.

given clause #456: (wt=11) 4111 [para_from,3964,2396,demod,2378,flip.1] (1^x) v 1= (0 v x) v 1.

given clause #457: (wt=19) 440 [para_into,52,178] (x v c((0 v c((x v y) v (x v y))) v y))^1=x.

given clause #458: (wt=11) 4217 [para_from,4033,130] 1^ (0 v (x v (x v x)))=x.

given clause #459: (wt=11) 4219 [para_from,4033,105] 1^ (x v (x v (0 v x)))=x.

given clause #460: (wt=11) 4228 [para_from,4033,2396,demod,2378] (0 v (x v x)) v 1=x v 1.

given clause #461: (wt=16) 442 [para_into,52,39] (x v c(y v 1))^ (x v (1 v (y v 0)))=x.

given clause #462: (wt=7) 4589 [back_demod,3541,demod,4567,4300,flip.1] 1 v 1=0 v 1.

given clause #463: (wt=7) 5017 [para_from,4589,1014,demod,1015,809,17,flip.1] 1 v (0 v 1)=1.

given clause #464: (wt=9) 4607 [back_demod,1295,demod,4590,4590,779] ((0 v 1)^1) v 1=1.

given clause #465: (wt=16) 444 [para_into,52,38] (1 v c(x v (y v 0)))^ (y v (x v 1))=1.

given clause #466: (wt=9) 5078 [para_into,5017,20] 1 v (1 v (0 v 0))=1.

given clause #467: (wt=10) 5039 [para_from,4589,440,demod,4590,1236,2378,287] (1 v c(0 v 1))^1=1.

given clause #468: (wt=11) 4249 [para_from,4033,7] 1^ (x v (0 v (x v x)))=x.

given clause #469: (wt=18) 446 [para_into,52,15] (x v c(y v (z v u)))^ (x v (z v (y v u)))=x.

given clause #470: (wt=11) 4299 [para_from,4204,2396,demod,2378] (x v (0 v x)) v 1=x v 1.

given clause #471: (wt=11) 4554 [para_into,4228,18] (c(0) v 1) v 1=c(0) v 1.

given clause #472: (wt=4) 5475 [back_demod,5357,demod,5424] c(0)=1.

given clause #473: (wt=18) 448 [para_into,52,14] (x v c(y v (z v u)))^ (z v (y v (x v u)))=x.

given clause #474: (wt=5) 5423 [back_demod,4878,demod,5406,5358,3353] 0 v 1=1.

given clause #475: (wt=5) 5651 [back_demod,4589,demod,5424] 1 v 1=1.

given clause #476: (wt=5) 5861 [back_demod,702,demod,5424] 1^1=1.

given clause #477: (wt=16) 468 [para_into,390,40] ((x v 1) v x)^ (c(x v 0) v 1)=x v 1.

given clause #478: (wt=5) 5912 [back_demod,5448,demod,5466,5440,flip.1] 0^1=0.

given clause #479: (wt=6) 5841 [back_demod,790,demod,5424] c(0 v 0)=1.

given clause #480: (wt=7) 5439 [back_demod,2583,demod,5358,5424,5358,5424,703,5424,12,5358,5424] (0 v 0)^1=0.

given clause #481: (wt=16) 472 [para_into,390,26] (x v ((c(y) v 0)^x))^ ((y^1) v 1)=x.

given clause #482: (wt=7) 5455 [back_demod,4474,demod,5424,4590,5424,925,5424,4590,5424,703,5424,flip.1] 1 v (0 v 0)=1.

given clause #483: (wt=7) 5465 [back_demod,5405,demod,5424,12,5424,12] 0^ (0 v 0)=0.

given clause #484: (wt=7) 5881 [back_demod,286,demod,5424] (0 v 0) v 1=1.

given clause #485: (wt=17) 494 [para_into,54,21] 1^ (1 v ((x v 1) v (x v 0)))=1 v (x v 0).

given clause #486: (wt=8) 5631 [back_demod,4692,demod,5424,703,5424,703,5424] c(0 v (0 v 0))=1.

given clause #487: (wt=9) 5435 [back_demod,2589,demod,5358,5424,5358,5424,703,5424,5358,5424] 0 v (x v 1)=x v 1.

given clause #488: (wt=9) 5443 [copy,5369,flip.1,demod,5424,4590,5424,5424,4590,5424] 1 v (x v 1)=x v 1.

given clause #489: (wt=19) 498 [para_into,54,15] 1^ ((x v (y v z)) v (y v (x v z)))=x v (y v z).

given clause #490: (wt=9) 5453 [back_demod,3424,demod,5424,17,5424,4590,5424,12,flip.1] (0 v 0)^ (0 v 0)=0.

given clause #491: (wt=9) 5553 [back_demod,4918,demod,5424,703,5424,5424] (x v (1^x))^1=x.

given clause #492: (wt=9) 5647 [back_demod,4666,demod,5424,703,5424,703,5424] (0 v (0 v 0))^1=0.

given clause #493: (wt=19) 500 [para_into,54,14] 1^ (x v (y v ((y v (x v z)) v z)))=y v (x v z).

given clause #494: (wt=9) 5879 [back_demod,292,demod,5424] 1 v ((0 v 0) v 0)=1.

given clause #495: (wt=9) 5966 [para_from,5475,390,demod,5652] (x v (0^x))^1=x.

given clause #496: (wt=9) 5986 [para_from,5475,7] (x v 1)^ (x v 0)=x.

given clause #497: (wt=18) 530 [para_into,58,178,flip.1] 1 v ((0 v c((x v 1) v (x v 1))) v (x v 0))=1.

given clause #498: (wt=9) 6006 [para_from,5475,3197,demod,5476,12] ((0^0) v 0) v 1=1.

given clause #499: (wt=9) 6008 [para_from,5475,3179,demod,5476,12] ((0^0) v 0)^1=0.

given clause #500: (wt=10) 5531 [back_demod,4948,demod,5424,12,5424,703,5424] c((0 v 0) v 0) v 0=1.

given clause #501: (wt=16) 534 [para_from,58,52] (x v c(y v 1))^ (1 v (y v (x v 0)))=x.

given clause #502: (wt=5) 6382 [para_from,5531,278,demod,12,5842,5456,12,17,5874,flip.1] 0 v 0=0.

given clause #503: (wt=5) 6446 [back_demod,5465,demod,6383] 0^0=0.

given clause #504: (wt=9) 6390 [back_demod,5948,demod,6383] c(c(x) v 1)=x^0.

given clause #505: (wt=18) 536 [para_from,58,178] (0 v c(1 v ((x v 1) v (x v 0)))) v (x v 1)=1.

given clause #506: (wt=9) 6498 [para_from,6382,2,flip.1] 0 v (x v 0)=x v 0.

given clause #507: (wt=10) 6002 [para_from,5475,36] (c(x) v 1)^ (x^0)=0.

given clause #508: (wt=10) 6004 [para_from,5475,32] (c(x) v 1) v (x^0)=1.

given clause #509: (wt=18) 538 [para_from,58,155] (0 v c(1 v ((x v 1) v (x v 0))))^ (x v 1)=0.

given clause #510: (wt=10) 6046 [para_from,5475,36] (1 v c(x))^ (0^x)=0.

given clause #511: (wt=10) 6048 [para_from,5475,32] (1 v c(x)) v (0^x)=1.

given clause #512: (wt=11) 5445 [copy,5375,flip.1,demod,5424,5424] x v 1=1 v (1 v (x v 0)).

given clause #513: (wt=17) 540 [para_from,58,14] x v (1 v (y v (z v 0)))=z v (x v (y v 1)).

given clause #514: (wt=11) 5873 [back_demod,466,demod,5424] ((x v x) v x)^1=x v x.

given clause #515: (wt=11) 6282 [para_into,5986,20] (1 v (x v 0))^ (x v 0)=x.

given clause #516: (wt=11) 6436 [back_demod,5535,demod,6383] c(1 v (c(x) v 0))=x^0.

given clause #517: (wt=17) 541 [copy,540,flip.1] x v (y v (z v 1))=y v (1 v (z v (x v 0))).

given clause #518: (wt=12) 5431 [back_demod,4085,demod,5358,5424] (1^ (x v 1)) v c(x v 1)=1.

given clause #519: (wt=9) 6844 [para_from,5431,534,demod,4372,5436,55,flip.1] 1^ (x v 1)=x v 1.

given clause #520: (wt=11) 6886 [para_into,6844,20] 1^ (1 v (x v 0))=x v 1.

given clause #521: (wt=17) 562 [para_from,59,54] 1^ ((1 v (x v 0)) v (x v 1))=1 v (x v 0).

given clause #522: (wt=12) 5437 [back_demod,2585,demod,5358,5424,5358,5424,703,5424,5358,5424] (0 v c(x v 1))^ (x v 1)=0.

given clause #523: (wt=12) 5463 [back_demod,5414,demod,5424,17,5424] (1 v c(x v 1))^ (x v 1)=1.

given clause #524: (wt=12) 5499 [back_demod,4982,demod,5424] (0 v c(x v x)) v (1 v x)=1.

given clause #525: (wt=16) 564 [para_from,59,52] (x v c(1 v (y v 0)))^ (x v (y v 1))=x.

given clause #526: (wt=12) 5501 [back_demod,4980,demod,5424] (1^c(x v x)) v (1 v x)=1.

given clause #527: (wt=12) 5575 [back_demod,4844,demod,5424,703,5424,12,5424] (1^c(x v x)) v (0 v x)=1.

given clause #528: (wt=12) 5577 [back_demod,4842,demod,5424,703,5424,12,5424] (0 v c(x v x)) v (0 v x)=1.

given clause #529: (wt=17) 566 [para_from,59,15] x v (y v (z v 1))=1 v (y v (x v (z v 0))).

given clause #530: (wt=12) 5625 [back_demod,4700,demod,5424,703,5424,5424,12] (c(x v (1^x)) v 0)^x=0.

given clause #531: (wt=12) 5627 [back_demod,4698,demod,5424,703,5424,5424,12] (c(x v (1^x)) v 0) v x=1.

given clause #532: (wt=12) 6245 [para_from,5966,90] (c(x v (0^x)) v 0) v x=1.

given clause #533: (wt=17) 567 [copy,566,flip.1] 1 v (x v (y v (z v 0)))=y v (x v (z v 1)).

given clause #534: (wt=12) 6247 [para_from,5966,88] (c(x v (0^x)) v 0)^x=0.

given clause #535: (wt=12) 6384 [back_demod,6292,demod,6383] ((x^0) v (x^1)) v c(x)=1.

given clause #536: (wt=12) 6386 [back_demod,6290,demod,6383] ((x^0) v (x^1))^c(x)=0.

given clause #537: (wt=19) 576 [para_into,64,54,demod,12,flip.1] 1^ (0 v c(x v ((x v y) v y)))=c(0 v (x v y)).

given clause #538: (wt=12) 6410 [back_demod,5693,demod,6383] (1 v (c(x) v 0))^ (x^0)=0.

given clause #539: (wt=12) 6412 [back_demod,5687,demod,6383] (1 v (c(x) v 0)) v (x^0)=1.

given clause #540: (wt=12) 6432 [back_demod,5539,demod,6383] ((x^1) v (x^0)) v c(x)=1.

given clause #541: (wt=18) 580 [para_into,64,46,flip.1] 1^ (c(x v 0) v c(1 v (x v 0)))=c(0 v x).

given clause #542: (wt=12) 6434 [back_demod,5537,demod,6383] ((x^1) v (x^0))^c(x)=0.

given clause #543: (wt=12) 6473 [para_from,6382,424] (0 v (x^1))^ (c(x) v 0)=0.

given clause #544: (wt=12) 6494 [para_from,6382,52] (0 v c(x v 0))^ (x v 0)=0.

given clause #545: (wt=16) 583 [para_into,64,40] c(0 v x)=1^ (c(x v 0) v c(x v 1)).

given clause #546: (wt=12) 6638 [para_from,6498,3964] (1^ (x v 0)) v c(x v 0)=1.

given clause #547: (wt=12) 6784 [para_from,6436,444,demod,5652] (1 v (x^0))^ (c(x) v 1)=1.

given clause #548: (wt=12) 6870 [back_demod,6414,demod,6845] (1^ (x^0)) v (c(x) v 1)=1.

given clause #549: (wt=16) 585 [copy,583,flip.1] 1^ (c(x v 0) v c(x v 1))=c(0 v x).

given clause #550: (wt=12) 6872 [back_demod,5994,demod,6845] (0 v (x^0)) v (c(x) v 1)=1.

given clause #551: (wt=12) 6888 [back_demod,3932,demod,6887] (1^c(x v 1)) v (x v 1)=1.

given clause #552: (wt=12) 6890 [back_demod,1344,demod,6887] (0 v c(x v 1)) v (x v 1)=1.

given clause #553: (wt=19) 586 [para_from,64,52] (x v (1^ (c(y) v c(z))))^ (0 v (x v (y^z)))=x.

given clause #554: (wt=12) 7345 [para_into,6638,278,demod,6383,5476,6383,17,12,17] (1^ (c(x) v 0)) v (x^1)=1.

given clause #555: (wt=8) 7679 [para_into,7345,5966,demod,6257] c(0 v x) v x=1.

given clause #556: (wt=7) 7807 [para_from,7679,1867,demod,161,6383,5476,5424,12,17,45,5424,161,6383,5476,5424,12,17,45] (x v x)^1=x.

given clause #557: (wt=19) 588 [para_from,64,7] (x v (1^ (c(y) v c(z))))^ (x v (0 v (y^z)))=x.

given clause #558: (wt=8) 7743 [para_into,7679,160,demod,6383,5476,5424,12,17] (1^x) v c(x)=1.

given clause #559: (wt=8) 8288 [para_into,7743,44] x v c(x v x)=1.

given clause #560: (wt=9) 7948 [para_from,7679,2396,demod,2378,161,6383,5476,5424,12,17,4112,flip.1] (0 v x) v 1=x v 1.

given clause #561: (wt=19) 590 [para_from,64,90] ((1^ (c(x) v c(y))) v 0) v ((0 v (x^y))^1)=1.

given clause #562: (wt=9) 8136 [back_demod,4228,demod,7949] (x v x) v 1=x v 1.

given clause #563: (wt=9) 8140 [back_demod,4111,demod,7949] (1^x) v 1=x v 1.

given clause #564: (wt=9) 8152 [back_demod,2377,demod,7949] (x^x) v 1=x v 1.

given clause #565: (wt=19) 592 [para_from,64,88] ((1^ (c(x) v c(y))) v 0)^ ((0 v (x^y))^1)=0.

given clause #566: (wt=9) 8359 [para_from,8288,52] 1^ (x v (x v x))=x.

given clause #567: (wt=9) 8779 [back_demod,8349,demod,8727] x^ (c(x) v c(x))=0.

given clause #568: (wt=10) 7693 [para_into,7679,6498] c(x v 0) v (x v 0)=1.

given clause #569: (wt=19) 594 [para_from,64,70] (0 v (1^ (c(x) v c(y)))) v (1^ (0 v (x^y)))=1.

given clause #570: (wt=10) 7695 [para_into,7679,5435] c(x v 1) v (x v 1)=1.

given clause #571: (wt=10) 7918 [para_from,7679,125,demod,5652,6499,flip.1] x v (c(x v 0) v 1)=1.

given clause #572: (wt=10) 7920 [para_from,7679,59,demod,5652,6499,flip.1] c(x v 0) v (x v 1)=1.

given clause #573: (wt=19) 596 [para_from,64,68] (0 v (1^ (c(x) v c(y))))^ (1^ (0 v (x^y)))=0.

given clause #574: (wt=8) 9089 [para_into,7920,8152,demod,85,7808] c(x) v (x v 1)=1.

given clause #575: (wt=8) 9221 [para_into,9089,2] x v (c(x) v 1)=1.

given clause #576: (wt=9) 9225 [para_from,9089,306,demod,6437] (x v (x^0))^1=x.

given clause #577: (wt=19) 598 [para_from,64,18] (0 v (x^y)) v (z v (1^ (c(x) v c(y))))=z v 1.

given clause #578: (wt=9) 9379 [para_from,9221,1762,demod,8565,6391,8141] (x^0) v 1=x v 1.

given clause #579: (wt=9) 9407 [back_demod,9039,demod,9380] (x v 0) v 1=x v 1.

given clause #580: (wt=10) 7984 [para_from,7679,250,demod,7680,5652,12,6383] c(0 v x) v (0 v x)=1.

given clause #581: (wt=18) 606 [para_from,119,178] (0 v c(1 v (x v ((x v 1) v 0)))) v (x v 1)=1.

given clause #582: (wt=10) 8006 [para_from,7679,600,demod,5862,7949] ((0 v c(x))^x) v 1=1.

given clause #583: (wt=8) 9979 [para_from,8006,40,demod,8003,flip.1] (0 v c(x))^x=0.

given clause #584: (wt=10) 8184 [para_from,7807,681] ((x^x) v 0) v c(x)=1.

given clause #585: (wt=18) 608 [para_from,119,155] (0 v c(1 v (x v ((x v 1) v 0))))^ (x v 1)=0.

given clause #586: (wt=10) 8186 [para_from,7807,669] ((x^x) v 0)^c(x)=0.

given clause #587: (wt=10) 8232 [para_from,7807,90] (c(x v x) v 0) v x=1.

given clause #588: (wt=10) 8234 [para_from,7807,88] (c(x v x) v 0)^x=0.

given clause #589: (wt=17) 610 [para_from,119,15] x v (1 v (y v (z v 0)))=z v (y v (x v 1)).

given clause #590: (wt=10) 8748 [para_from,8152,56,demod,85,7808] (1 v c(x))^ (x v 1)=1.

given clause #591: (wt=10) 8821 [para_from,8359,7743] x v c(x v (x v x))=1.

given clause #592: (wt=10) 8871 [para_from,8779,205] (c(x) v (x^x)) v 0=1.

given clause #593: (wt=17) 611 [copy,610,flip.1] x v (y v (z v 1))=z v (1 v (y v (x v 0))).

given clause #594: (wt=8) 10212 [para_from,8871,6282,demod,8872,5652,5862,flip.1] c(x) v (x^x)=1.

given clause #595: (wt=10) 8877 [para_into,7693,278,demod,6383,5476,6383,17,12,17] (x^1) v (c(x) v 0)=1.

given clause #596: (wt=10) 8881 [para_into,7693,2] x v (c(x v 0) v 0)=1.

given clause #597: (wt=17) 614 [para_from,125,15] x v (y v (z v 1))=1 v (z v (x v (y v 0))).

given clause #598: (wt=10) 8976 [para_into,7695,6390] (x^0) v (c(x) v 1)=1.

given clause #599: (wt=10) 9027 [para_into,7918,278,demod,6383,5476,6383,17,12,17] c(x) v ((x^1) v 1)=1.

given clause #600: (wt=10) 9085 [para_into,7920,278,demod,6383,5476,6383,17,12,17] (x^1) v (c(x) v 1)=1.

given clause #601: (wt=17) 615 [copy,614,flip.1] 1 v (x v (y v (z v 0)))=y v (z v (x v 1)).

given clause #602: (wt=9) 10605 [para_from,9085,1762,demod,8565,9518,9616,8141,9380,flip.1] (x^1) v 1=x v 1.

given clause #603: (wt=9) 10630 [back_demod,10319,demod,10606] c(c(x)) v 1=x v 1.

given clause #604: (wt=9) 10795 [back_demod,9615,demod,10794] (x v 1)^0=x^0.

given clause #605: (wt=18) 616 [para_into,66,26] (x v (1^ (c(y) v 0)))^ (x v (0 v (y^1)))=x.

given clause #606: (wt=9) 10979 [back_demod,9517,demod,10854] c(x v 1)=c(x)^0.

given clause #607: (wt=9) 11049 [para_into,10795,10630,demod,10796,flip.1] c(c(x))^0=x^0.

given clause #608: (wt=9) 11051 [para_into,10795,10605,demod,10796,flip.1] (x^1)^0=x^0.

given clause #609: (wt=18) 620 [para_from,66,36] (c(x v (1^y)) v c(x v (0 v c(y))))^x=0.

given clause #610: (wt=9) 11053 [para_into,10795,9407,demod,10796,flip.1] (x v 0)^0=x^0.

given clause #611: (wt=9) 11055 [para_into,10795,9379,demod,10796,flip.1] (x^0)^0=x^0.

given clause #612: (wt=9) 11057 [para_into,10795,8152,demod,10796,flip.1] (x^x)^0=x^0.

given clause #613: (wt=18) 622 [para_from,66,32] (c(x v (1^y)) v c(x v (0 v c(y)))) v x=1.

given clause #614: (wt=9) 11059 [para_into,10795,8140,demod,10796,flip.1] (1^x)^0=x^0.

given clause #615: (wt=9) 11061 [para_into,10795,8136,demod,10796,flip.1] (x v x)^0=x^0.

given clause #616: (wt=9) 11063 [para_into,10795,7948,demod,10796,flip.1] (0 v x)^0=x^0.

given clause #617: (wt=19) 655 [para_into,84,54,demod,12] c((x v y) v 0)= (0 v c(x v ((x v y) v y)))^1.

given clause #618: (wt=9) 11107 [para_from,10795,9379,demod,9380,flip.1] (x v 1) v 1=x v 1.

given clause #619: (wt=10) 9193 [para_into,9089,8152] c(x^x) v (x v 1)=1.

given clause #620: (wt=10) 9195 [para_into,9089,8140] c(1^x) v (x v 1)=1.

given clause #621: (wt=19) 661 [copy,655,flip.1] (0 v c(x v ((x v y) v y)))^1=c((x v y) v 0).

given clause #622: (wt=10) 9197 [para_into,9089,8136] c(x v x) v (x v 1)=1.

given clause #623: (wt=10) 9199 [para_into,9089,7948] c(0 v x) v (x v 1)=1.

given clause #624: (wt=5) 12034 [para_into,9199,2,demod,12015] x v 1=1.

given clause #625: (wt=19) 665 [para_from,84,52] (x v ((c(y) v c(z))^1))^ ((y^z) v (x v 0))=x.

given clause #626: (wt=5) 12066 [back_demod,8851,demod,12035,45] x^0=0.

given clause #627: (wt=5) 12530 [back_demod,6034,demod,12051,12059] 0^x=0.

given clause #628: (wt=6) 12746 [back_demod,6051,demod,12531,flip.1] c(1 v x)=0.

given clause #629: (wt=19) 667 [para_from,84,7] (x v ((c(y) v c(z))^1))^ (x v ((y^z) v 0))=x.

given clause #630: (wt=5) 12907 [para_from,12746,50,demod,5476,12035,5862,flip.1] 1 v x=1.

given clause #631: (wt=7) 12058 [back_demod,9397,demod,12035,12035,12035,12,12035,12035] (x v 0)^1=x.

given clause #632: (wt=7) 12072 [back_demod,7391,demod,12035,12035,5913,12067,6383] 1^ (x v 0)=x.

given clause #633: (wt=19) 904 [para_into,96,15] x v (y v (z v (u v v)))=u v (z v (x v (y v v))).

given clause #634: (wt=7) 12629 [back_demod,7283,demod,12067,12073] x^1=1^x.

given clause #635: (wt=7) 12761 [copy,12629,flip.1] 1^x=x^1.

given clause #636: (wt=8) 12522 [back_demod,18,demod,12035] x v (y v c(x))=1.

given clause #637: (wt=19) 905 [para_into,96,14] x v (y v (z v (u v v)))=u v (y v (z v (x v v))).

given clause #638: (wt=8) 12542 [back_demod,7677,demod,12073,12059] (x^1) v c(x)=1.

given clause #639: (wt=8) 12598 [back_demod,10941,demod,12067,12073] c(x v 0) v x=1.

given clause #640: (wt=8) 12680 [back_demod,8207,demod,12073] c(x v x) v x=1.

given clause #641: (wt=19) 906 [copy,904,flip.1] x v (y v (z v (u v v)))=z v (u v (y v (x v v))).

given clause #642: (wt=8) 12684 [back_demod,7345,demod,12073] c(x) v (x^1)=1.

given clause #643: (wt=8) 12967 [para_from,12072,7743] x v c(x v 0)=1.

given clause #644: (wt=8) 13137 [back_demod,12594,demod,13122] (c(x) v 0)^x=0.

given clause #645: (wt=19) 948 [para_into,97,96] x v (y v (z v (u v v)))=x v (y v (u v (z v v))).

given clause #646: (wt=8) 13579 [para_into,12684,12629] c(x) v (1^x)=1.

given clause #647: (wt=8) 13643 [para_from,12967,669,demod,5862,12059] x^ (c(x) v 0)=0.

given clause #648: (wt=9) 12098 [back_demod,390,demod,12035] (x v (y^x))^1=x.

given clause #649: (wt=19) 950 [para_into,97,15] x v (y v (z v (u v v)))=u v (z v (y v (x v v))).

given clause #650: (wt=9) 12524 [back_demod,8260,demod,12059] c(x v x)=c(x v 0).

given clause #651: (wt=9) 12525 [back_demod,8250,demod,12059] c(x v 0)=c(x v x).

given clause #652: (wt=9) 12584 [back_demod,11085,demod,12067] 1^ (x v (x v 0))=x.

given clause #653: (wt=19) 1059 [para_into,101,2] x v (y v (z v (u v v)))=x v (z v (u v (y v v))).

given clause #654: (wt=9) 12607 [back_demod,9495,demod,12067,12073] c(x v 0)=c(0 v x).

given clause #655: (wt=5) 14141 [back_demod,13191,demod,14119] x^1=x.

given clause #656: (wt=5) 14147 [back_demod,8359,demod,14119] 1^x=x.

given clause #657: (wt=19) 1063 [copy,1059,flip.1] x v (y v (z v (u v v)))=x v (u v (y v (z v v))).

given clause #658: (wt=5) 14151 [back_demod,4217,demod,14119,14148] 0 v x=x.

given clause #659: (wt=5) 14181 [back_demod,13959,demod,14152,14142] c(c(x))=x.

given clause #660: (wt=5) 14199 [back_demod,13859,demod,14142,14152,14142] x^x=x.

given clause #661: (wt=19) 1130 [para_into,102,2] x v (y v (z v (u v v)))=x v (u v (z v (y v v))).

given clause #662: (wt=5) 14227 [back_demod,13707,demod,14142,14142] x v x=x.

given clause #663: (wt=5) 14257 [back_demod,13483,demod,14142,14142,14228,13644,14142] x v 0=x.

given clause #664: (wt=6) 14273 [back_demod,13299,demod,14258,14258,14142,14228,14182] c(x) v x=1.

given clause #665: (wt=15) 12506 [back_demod,242,demod,12035,12035] (c(x) v c(y)) v (z v (u v (x^y)))=1.

given clause #666: (wt=6) 14277 [back_demod,13269,demod,14152,14148,14152,14142,14152,14148] c(x)^x=0.

given clause #667: (wt=7) 14145 [back_demod,12056,demod,14119,14142] x v (y^x)=x.

given clause #668: (wt=7) 14565 [para_from,14257,2,demod,14258] x v y=y v x.

given clause #669: (wt=12) 12512 [back_demod,143,demod,12035,12035,12035] x v (y v (z v (u v c(x))))=1.

given clause #670: (wt=7) 14600 [para_into,14565,14145,flip.1] (x^y) v y=y.

given clause #671: (wt=8) 14295 [back_demod,12518,demod,14258,14142] c(x) v (y v x)=1.

given clause #672: (wt=8) 14309 [back_demod,12288,demod,14258,14258,14292,14182,14142] x v (x^c(y))=x.

given clause #673: (wt=13) 12514 [back_demod,141,demod,12035] (c(x) v c(y)) v (z v (x^y))=1.

given clause #674: (wt=7) 14867 [para_into,14309,14181] x v (x^y)=x.

given clause #675: (wt=7) 14879 [para_into,14867,14565] (x^y) v x=x.

given clause #676: (wt=8) 14317 [back_demod,12164,demod,14142,14258] c(x) v (x v y)=1.

given clause #677: (wt=10) 12520 [back_demod,94,demod,12035,12035] x v (y v (z v c(x)))=1.

given clause #678: (wt=8) 14319 [back_demod,12162,demod,14142,14258] x v (c(x) v y)=1.

given clause #679: (wt=8) 14602 [para_into,14565,12522,flip.1] (x v c(y)) v y=1.

given clause #680: (wt=8) 14863 [para_into,14295,14565] (x v y) v c(y)=1.

given clause #681: (wt=17) 13039 [para_into,904,32,demod,12035,12035,12035,flip.1] (c(x) v c(y)) v (z v (u v (v v (x^y))))=1.

given clause #682: (wt=8) 14957 [para_into,14317,14565] (x v y) v c(x)=1.

given clause #683: (wt=8) 14965 [para_into,14319,14565] (c(x) v y) v x=1.

given clause #684: (wt=9) 14221 [back_demod,13737,demod,14142] (x v y) v x=x v y.

given clause #685: (wt=14) 13279 [para_from,12522,904,demod,12035,12035,12035,flip.1] x v (y v (z v (u v (v v c(x)))))=1.

given clause #686: (wt=9) 14439 [back_demod,13277,demod,14182,14182,14228,14292,14152] x^ (c(y)^c(x))=0.

given clause #687: (wt=8) 15171 [para_into,14439,14181] x^ (y^c(x))=0.

given clause #688: (wt=8) 15175 [para_into,15171,14181] c(x)^ (y^x)=0.

given clause #689: (wt=13) 14223 [back_demod,13733,demod,14142] (x v (y v z)) v y=x v (y v z).

given clause #690: (wt=9) 14527 [para_from,14227,2,flip.1] x v (y v x)=y v x.

given clause #691: (wt=9) 14819 [para_into,14600,7] x v (x v y)=x v y.

given clause #692: (wt=9) 15015 [para_from,14602,7,demod,14182,14148,14182] (x v y) v y=x v y.

given clause #693: (wt=17) 14225 [back_demod,13719,demod,14142] (x v (y v (z v u))) v z=x v (y v (z v u)).

given clause #694: (wt=9) 15181 [para_into,15175,7,demod,14292] (c(x)^c(y))^x=0.

given clause #695: (wt=8) 15259 [para_into,15181,14181] (c(x)^y)^x=0.

given clause #696: (wt=8) 15261 [para_into,15259,14181] (x^y)^c(x)=0.

given clause #697: (wt=10) 14243 [back_demod,13609,demod,14142] c(x) v (y v (z v x))=1.

given clause #698: (wt=8) 15267 [para_into,15261,7,demod,14292,14182] x^ (c(x)^y)=0.

given clause #699: (wt=8) 15279 [para_into,15267,14181] c(x)^ (x^y)=0.

given clause #700: (wt=10) 14259 [back_demod,13479,demod,14228,14142] x v ((x v c(y))^y)=x.

given clause #701: (wt=12) 14245 [back_demod,13601,demod,14142] c(x) v (y v (z v (u v x)))=1.

given clause #702: (wt=10) 14279 [back_demod,13253,demod,14142,14152] (x v y)^ (x v c(y))=x.

given clause #703: (wt=10) 14291 [back_demod,12958,demod,14258,14258,14258,14142,flip.1] c(x v y)=c(x)^c(y).

given clause #704: (wt=9) 15364 [para_into,14291,14863,demod,12,14292,14182,flip.1] (c(x)^c(y))^y=0.

given clause #705: (wt=11) 14249 [back_demod,13577,demod,14228,14152,14142] (x^c(y)) v (c(x) v y)=1.

given clause #706: (wt=8) 15445 [para_into,15364,14181] (x^c(y))^y=0.

given clause #707: (wt=8) 15539 [para_into,15445,14181] (x^y)^c(y)=0.

given clause #708: (wt=10) 14293 [back_demod,12566,demod,14142,14258] (x v c(y))^ (y v x)=x.

given clause #709: (wt=11) 14271 [back_demod,13305,demod,14142,14228,14152] (c(x) v y) v (x^c(y))=1.

given clause #710: (wt=10) 14313 [back_demod,12168,demod,14142,14258] x v (y v (c(x) v z))=1.

given clause #711: (wt=10) 14315 [back_demod,12166,demod,14142,14258] c(x) v (y v (x v z))=1.

given clause #712: (wt=10) 14353 [back_demod,424,demod,14142,14258] (x v y)^ (c(y) v x)=x.

given clause #713: (wt=11) 14281 [back_demod,13249,demod,14142,14152] (c(x) v y)^ (x^c(y))=0.

given clause #714: (wt=10) 14365 [back_demod,84,demod,14258,14142] c(x^y)=c(x) v c(y).

given clause #715: (wt=10) 14431 [back_demod,13050,demod,14228,14292,14152,14292,14366,14182,14182,14148] x v ((x v y)^c(y))=x.

given clause #716: (wt=10) 14737 [para_from,14565,7] (c(x) v y)^ (y v x)=y.

given clause #717: (wt=11) 14283 [back_demod,13237,demod,14152,14142] (x^y)^ (c(x) v c(y))=0.

given clause #718: (wt=10) 14959 [para_into,12520,14565] x v ((y v c(x)) v z)=1.

given clause #719: (wt=10) 14961 [para_into,12520,14565] (x v (y v c(z))) v z=1.

given clause #720: (wt=10) 15017 [para_from,14602,2,demod,12035,flip.1] (x v c(y)) v (z v y)=1.

given clause #721: (wt=11) 14285 [back_demod,13235,demod,14152,14142] (x^y) v (c(x) v c(y))=1.

given clause #722: (wt=10) 15043 [para_from,14863,2,demod,12035,flip.1] (x v y) v (z v c(y))=1.

given clause #723: (wt=10) 15071 [para_into,14957,2] (x v (y v z)) v c(y)=1.

given clause #724: (wt=10) 15085 [para_from,14957,2,demod,12035,flip.1] (x v y) v (z v c(x))=1.

given clause #725: (wt=15) 14287 [back_demod,13233,demod,14142,14152] (x v (c(y) v c(z)))^ (x v (y^z))=x.

given clause #726: (wt=10) 15097 [para_into,14965,2] (x v (c(y) v z)) v y=1.

given clause #727: (wt=10) 15141 [para_from,14965,2,demod,12035,flip.1] (c(x) v y) v (z v x)=1.

given clause #728: (wt=10) 15177 [para_into,15175,392,demod,14292,14182,14292,14182] (x^ (c(y)^z))^y=0.

given clause #729: (wt=13) 14297 [back_demod,12500,demod,14258,14142] (x^y) v (z v (c(x) v c(y)))=1.

given clause #730: (wt=10) 15269 [para_into,14243,14565] c(x) v ((y v x) v z)=1.

given clause #731: (wt=10) 15275 [para_into,14243,14565] (x v (y v z)) v c(z)=1.

given clause #732: (wt=10) 15281 [para_into,14259,14565] x v ((c(y) v x)^y)=x.

given clause #733: (wt=11) 14299 [back_demod,12490,demod,14292,14292,14182,14142] x v (c(y)^ (c(z)^x))=x.

given clause #734: (wt=10) 15283 [para_into,14259,14565] ((x v c(y))^y) v x=x.

given clause #735: (wt=10) 15332 [para_into,14279,14565] (x v y)^ (y v c(x))=y.

given clause #736: (wt=10) 15543 [para_into,15539,392,demod,14292,14182,14292,14182] x^ (y^ (c(x)^z))=0.

given clause #737: (wt=13) 14301 [back_demod,12478,demod,14142,14258] (x v c(y)) v (z v (c(x)^y))=1.

given clause #738: (wt=10) 15553 [para_into,14293,14565] (c(x) v y)^ (x v y)=y.

given clause #739: (wt=10) 15595 [para_into,14313,14565] x v ((c(x) v y) v z)=1.

given clause #740: (wt=10) 15609 [para_into,14315,14565] c(x) v ((x v y) v z)=1.

given clause #741: (wt=13) 14303 [back_demod,12476,demod,14142,14258] (c(x) v y) v (z v (x^c(y)))=1.

given clause #742: (wt=10) 15621 [para_into,14353,14565] (x v y)^ (c(x) v y)=y.

given clause #743: (wt=10) 15739 [para_into,14431,14565] x v ((y v x)^c(y))=x.

given clause #744: (wt=10) 15745 [para_into,14431,14565] ((x v y)^c(y)) v x=x.

given clause #745: (wt=17) 14329 [back_demod,8166,demod,14142] (x v (y v z)) v (y v (x v z))=x v (y v z).

given clause #746: (wt=10) 15816 [para_into,14959,14565] ((x v c(y)) v z) v y=1.

given clause #747: (wt=10) 15834 [para_into,14959,2] (x v c(y)) v (y v z)=1.

given clause #748: (wt=10) 15958 [para_into,15043,14565] (x v y) v (c(y) v z)=1.

given clause #749: (wt=11) 14337 [back_demod,3891,demod,14142,14148,14258,14152] (x v y) v (c(x)^c(y))=1.

given clause #750: (wt=10) 15972 [para_into,15071,14565] ((x v y) v z) v c(x)=1.

given clause #751: (wt=10) 15998 [para_into,15085,14565] (x v y) v (c(x) v z)=1.

given clause #752: (wt=10) 16030 [para_into,15097,14565] ((c(x) v y) v z) v x=1.

given clause #753: (wt=11) 14339 [back_demod,3665,demod,14142,14148,14258,14152] (x v y)^ (c(x)^c(y))=0.

given clause #754: (wt=10) 16074 [para_into,15141,14565] (c(x) v y) v (x v z)=1.

given clause #755: (wt=10) 16092 [para_into,15177,14181] (x^ (y^z))^c(y)=0.

given clause #756: (wt=10) 16120 [para_into,15269,14565] ((x v y) v z) v c(y)=1.

given clause #757: (wt=11) 14341 [back_demod,3191,demod,14258,14258,14142,14142] (c(x)^y) v (x v c(y))=1.

given clause #758: (wt=10) 16156 [para_into,15281,14565] ((c(x) v y)^x) v y=y.

given clause #759: (wt=10) 16201 [para_into,14299,14181] x v (y^ (c(z)^x))=x.

given clause #760: (wt=9) 16851 [para_into,16201,14181] x v (y^ (z^x))=x.

given clause #761: (wt=11) 14343 [back_demod,3177,demod,14258,14258,14142,14142] (x^c(y))^ (c(x) v y)=0.

given clause #762: (wt=9) 16855 [para_into,16851,14565] (x^ (y^z)) v z=z.

given clause #763: (wt=10) 16264 [para_into,15543,14181] c(x)^ (y^ (x^z))=0.

given clause #764: (wt=10) 16430 [para_into,15739,14565] ((x v y)^c(x)) v y=y.

given clause #765: (wt=11) 14345 [back_demod,3173,demod,14258,14258,14142,14142] (c(x)^y)^ (x v c(y))=0.

given clause #766: (wt=10) 16734 [para_into,16092,15553,demod,14292,14182] (x^y)^ (z^c(y))=0.

given clause #767: (wt=10) 16738 [para_into,16092,14293,demod,14292,14182] (x^y)^ (c(y)^z)=0.

given clause #768: (wt=10) 16947 [para_into,16264,15553,demod,14292,14182] (x^c(y))^ (z^y)=0.

given clause #769: (wt=15) 14347 [back_demod,3125,demod,14258,14142] (x v (y^c(z)))^ (c(y) v (x v z))=x.

given clause #770: (wt=10) 16951 [para_into,16264,14293,demod,14292,14182] (c(x)^y)^ (z^x)=0.

given clause #771: (wt=10) 16996 [para_into,16734,15621,demod,14292,14182] x^ (y^ (z^c(x)))=0.

given clause #772: (wt=10) 17004 [para_into,16738,15621,demod,14292,14182] x^ ((y^c(x))^z)=0.

given clause #773: (wt=15) 14349 [back_demod,3123,demod,14258,14142] (x v (c(y)^z))^ (y v (x v c(z)))=x.

given clause #774: (wt=10) 17006 [para_into,16738,15332,demod,14292,14182] x^ ((c(x)^y)^z)=0.

given clause #775: (wt=10) 17014 [para_into,16738,14181] (x^c(y))^ (y^z)=0.

given clause #776: (wt=10) 17020 [para_into,16947,15621,demod,14292,14182] (x^ (y^c(z)))^z=0.

given clause #777: (wt=15) 14351 [back_demod,665,demod,14142,14258] (x v (c(y) v c(z)))^ ((y^z) v x)=x.

given clause #778: (wt=10) 17066 [para_into,14347,14319,demod,14292,14182,12035,14142] x v (y^ (x^c(z)))=x.

given clause #779: (wt=9) 17202 [para_into,17066,14181] x v (y^ (x^z))=x.

given clause #780: (wt=9) 17206 [para_into,17202,14565] (x^ (y^z)) v y=y.

given clause #781: (wt=15) 14355 [back_demod,388,demod,14258,14142] (x v (y^c(z)))^ (x v (c(y) v z))=x.

given clause #782: (wt=10) 17102 [para_into,16951,14181] (x^y)^ (z^c(x))=0.

given clause #783: (wt=10) 17104 [para_into,16951,15621,demod,14292,14182] ((x^c(y))^z)^y=0.

given clause #784: (wt=10) 17106 [para_into,16951,15332,demod,14292,14182] ((c(x)^y)^z)^x=0.

given clause #785: (wt=15) 14357 [back_demod,384,demod,14258,14142] (x v (c(y)^z))^ (x v (y v c(z)))=x.

given clause #786: (wt=10) 17116 [para_into,16996,14181] c(x)^ (y^ (z^x))=0.

given clause #787: (wt=10) 17122 [para_into,17004,14181] c(x)^ ((y^x)^z)=0.

given clause #788: (wt=10) 17134 [para_into,14349,16074,demod,14292,14182,14142] x v ((x^c(y))^z)=x.

given clause #789: (wt=11) 14359 [back_demod,270,demod,14142,14258] (x v c(y))^ (c(x)^y)=0.

given clause #790: (wt=9) 17368 [para_into,17134,14181] x v ((x^y)^z)=x.

given clause #791: (wt=9) 17388 [para_into,17368,14565] ((x^y)^z) v x=x.

given clause #792: (wt=10) 17140 [para_into,14349,15834,demod,14292,14182,14142] x v ((c(y)^x)^z)=x.

given clause #793: (wt=11) 14361 [back_demod,234,demod,14142,14258] (x v c(y)) v (c(x)^y)=1.

given clause #794: (wt=9) 17470 [para_into,17140,14181] x v ((y^x)^z)=x.

given clause #795: (wt=9) 17512 [para_into,17470,14565] ((x^y)^z) v y=y.

given clause #796: (wt=10) 17170 [para_into,17006,14181] c(x)^ ((x^y)^z)=0.

given clause #797: (wt=11) 14369 [back_demod,13761,demod,14258,14292,14152] x v ((c(x)^c(y)) v y)=1.

given clause #798: (wt=10) 17180 [para_into,17020,14181] (x^ (y^z))^c(z)=0.

given clause #799: (wt=10) 17306 [para_into,17104,14181] ((x^y)^z)^c(y)=0.

given clause #800: (wt=10) 17312 [para_into,17106,14181] ((x^y)^z)^c(x)=0.

given clause #801: (wt=18) 14371 [back_demod,13753,demod,14258,14292,14292] x v (y v ((c(y)^ (c(x)^c(z))) v (u v z)))=1.

given clause #802: (wt=10) 17356 [para_into,17122,15332,demod,14292,14182] (c(x)^y)^ (x^z)=0.

given clause #803: (wt=10) 17632 [para_into,17306,15332,demod,14292,14182] (x^y)^ (c(x)^z)=0.

given clause #804: (wt=11) 14373 [back_demod,13751,demod,14258,14258,14258] c(x)^ (c(y) v c(x))=c(x).

given clause #805: (wt=18) 14375 [back_demod,13571,demod,14258,14292,14292] x v (y v ((c(x)^ (c(y)^c(z))) v (u v z)))=1.

given clause #806: (wt=8) 17694 [para_into,14373,14181,demod,14182,14182] x^ (c(y) v x)=x.

given clause #807: (wt=7) 17732 [para_into,17694,14181] x^ (y v x)=x.

given clause #808: (wt=7) 17772 [para_into,17732,14565] x^ (x v y)=x.

given clause #809: (wt=13) 14377 [back_demod,13449,demod,14258,14292] x v (y v ((c(x)^c(z)) v z))=1.

given clause #810: (wt=9) 17770 [para_into,17732,14867] (x^y)^x=x^y.

given clause #811: (wt=9) 17782 [para_into,17732,14223] x^ (y v (x v z))=x.

given clause #812: (wt=9) 17784 [para_into,17732,14145] (x^y)^y=x^y.

given clause #813: (wt=13) 14379 [back_demod,13447,demod,14258,14292] (c(x)^c(y)) v (x v (z v y))=1.

given clause #814: (wt=9) 17858 [para_into,17782,14565] x^ (y v (z v x))=x.

given clause #815: (wt=9) 17862 [para_into,17782,14565] x^ ((x v y) v z)=x.

given clause #816: (wt=9) 17942 [para_into,17858,14565] x^ ((y v x) v z)=x.

given clause #817: (wt=13) 14381 [back_demod,13445,demod,14258,14292] x v ((c(x)^c(y)) v (z v y))=1.

given clause #818: (wt=11) 14429 [back_demod,13209,demod,14152,14292,14148,14152] (c(x)^c(y)) v (x v y)=1.

given clause #819: (wt=11) 14449 [back_demod,6475,demod,14258,14292,14152,14258] (c(x)^c(y))^ (y v x)=0.

given clause #820: (wt=11) 14561 [para_from,14257,122,demod,14258] x v (y v z)=x v (z v y).

given clause #821: (wt=15) 14383 [back_demod,13411,demod,14258,14292] x v (y v (z v ((c(x)^c(u)) v u)))=1.

given clause #822: (wt=11) 14562 [para_from,14257,98,demod,14258] x v (y v z)=z v (y v x).

given clause #823: (wt=10) 18568 [back_demod,17608,demod,18416,14880,flip.1] (x^c(y)) v y=y v x.

given clause #824: (wt=10) 18926 [back_demod,17488,demod,18569] c(x) v ((y v x)^x)=1.

given clause #825: (wt=15) 14385 [back_demod,13409,demod,14258,14292] (c(x)^c(y)) v (x v (z v (u v y)))=1.

given clause #826: (wt=7) 19085 [para_from,18926,14353,demod,14601,14142,flip.1] (x v y)^y=y.

given clause #827: (wt=7) 19111 [para_into,19085,18568] (x v y)^x=x.

given clause #828: (wt=9) 19121 [para_into,19085,14867] x^ (x^y)=x^y.

given clause #829: (wt=15) 14387 [back_demod,13407,demod,14258,14292] (c(x)^c(y)) v (z v (x v (u v y)))=1.

given clause #830: (wt=9) 19131 [para_into,19085,14145] x^ (y^x)=y^x.

given clause #831: (wt=9) 19149 [para_into,19111,14562] (x v (y v z))^z=z.

given clause #832: (wt=9) 19161 [para_into,19111,2] (x v (y v z))^y=y.

given clause #833: (wt=15) 14389 [back_demod,13405,demod,14258,14292] x v ((c(x)^c(y)) v (z v (u v y)))=1.

given clause #834: (wt=10) 18987 [para_into,18568,17784,demod,18569,flip.1] x v (y^c(x))=x v y.

given clause #835: (wt=10) 19019 [para_from,18568,15332,demod,14182,14146,14182] x^ (c(x) v y)=y^x.

given clause #836: (wt=10) 19035 [para_from,18568,14293,demod,14182,14146,14182] (c(x) v y)^x=y^x.

given clause #837: (wt=15) 14391 [back_demod,13403,demod,14258,14292] x v (y v ((c(x)^c(z)) v (u v z)))=1.

given clause #838: (wt=10) 19045 [copy,19019,flip.1] x^y=y^ (c(y) v x).

given clause #839: (wt=10) 19297 [para_into,19019,14565] x^ (y v c(x))=y^x.

given clause #840: (wt=10) 19322 [copy,19297,flip.1] x^y=y^ (x v c(y)).

given clause #841: (wt=18) 14393 [back_demod,13401,demod,14258,14292,14292] x v (y v ((c(z)^ (c(x)^c(u))) v (z v u)))=1.

given clause #842: (wt=10) 19353 [back_demod,15283,demod,19301] (x^ (y v c(x))) v y=y.

given clause #843: (wt=10) 19355 [back_demod,14259,demod,19301] x v (y^ (x v c(y)))=x.

given clause #844: (wt=10) 19538 [para_from,19045,15745,demod,14182,14528] (c(x)^ (y v x)) v y=y.

given clause #845: (wt=18) 14395 [back_demod,13399,demod,14258,14292,14292] x v (y v (z v ((c(z)^ (c(x)^c(u))) v u)))=1.

given clause #846: (wt=10) 19540 [para_from,19045,14431,demod,14182,14528] x v (c(y)^ (x v y))=x.

given clause #847: (wt=10) 19634 [para_from,19045,14879] (x^ (c(x) v y)) v y=y.

given clause #848: (wt=10) 19636 [para_from,19045,14867] x v (y^ (c(y) v x))=x.

given clause #849: (wt=18) 14397 [back_demod,13397,demod,14258,14292,14292] (c(x)^ (c(y)^c(z))) v (x v (y v (u v z)))=1.

given clause #850: (wt=10) 19860 [para_into,19538,14565] (c(x)^ (x v y)) v y=y.

given clause #851: (wt=10) 19931 [para_into,19540,14565] x v (c(y)^ (y v x))=x.

given clause #852: (wt=11) 14563 [para_from,14257,15,demod,14258] x v (y v z)=y v (z v x).

given clause #853: (wt=18) 14399 [back_demod,13395,demod,14258,14292,14292] (c(x)^ (c(y)^c(z))) v (y v (x v (u v z)))=1.

given clause #854: (wt=11) 14564 [para_from,14257,14,demod,14258] x v (y v z)=z v (x v y).

given clause #855: (wt=11) 14598 [para_from,14145,2,flip.1] x v (y v (z^x))=y v x.

given clause #856: (wt=11) 14741 [para_from,14565,36] (c(x) v c(y))^ (y^x)=0.

given clause #857: (wt=18) 14403 [back_demod,13391,demod,14258,14292,14292] (c(x)^ (c(y)^c(z))) v (y v (u v (x v z)))=1.

given clause #858: (wt=11) 14859 [para_from,14600,2,flip.1] (x^y) v (z v y)=z v y.

given clause #859: (wt=11) 14907 [para_from,14867,2,flip.1] x v (y v (x^z))=y v x.

given clause #860: (wt=11) 14947 [para_from,14879,2,flip.1] (x^y) v (z v x)=z v x.

given clause #861: (wt=18) 14405 [back_demod,13389,demod,14258,14292,14292] x v ((c(y)^ (c(x)^c(z))) v (u v (y v z)))=1.

given clause #862: (wt=11) 15300 [para_from,14259,14863,demod,14366,14292,14182] x v ((c(x)^y) v c(y))=1.

given clause #863: (wt=10) 20674 [para_from,15300,19035,demod,14148,14182,flip.1] ((x^y) v c(y))^x=x.

given clause #864: (wt=9) 20720 [back_demod,18943,demod,20713] x^c(y)=c(y)^x.

given clause #865: (wt=18) 14407 [back_demod,13387,demod,14258,14292,14292] x v (y v (z v ((c(x)^ (c(y)^c(u))) v u)))=1.

given clause #866: (wt=7) 20740 [para_into,20720,14181,demod,14182] x^y=y^x.

given clause #867: (wt=10) 20706 [para_into,20674,14279,demod,14292,14182,20391] x v (c(x)^y)=x v y.

given clause #868: (wt=10) 20718 [back_demod,19590,demod,20713] (c(x)^y) v x=x v y.

given clause #869: (wt=18) 14409 [back_demod,13385,demod,14258,14292,14292] x v ((c(x)^ (c(y)^c(z))) v (y v (u v z)))=1.

given clause #870: (wt=10) 20728 [para_from,20674,17770,demod,20675] x^ ((x^y) v c(y))=x.

given clause #871: (wt=10) 20767 [para_into,20740,19322] x^ (y v c(x))=x^y.

given clause #872: (wt=10) 20769 [para_into,20740,19045] x^ (c(x) v y)=x^y.

given clause #873: (wt=18) 14411 [back_demod,13383,demod,14258,14292,14292] (c(x)^ (c(y)^c(z))) v (u v (y v (x v z)))=1.

given clause #874: (wt=10) 20775 [back_demod,20678,demod,20768] ((x^y) v c(x))^y=y.

given clause #875: (wt=10) 20905 [para_into,20728,20740] x^ ((y^x) v c(y))=x.

given clause #876: (wt=10) 20959 [para_into,20767,20740] (x v c(y))^y=y^x.

given clause #877: (wt=18) 14413 [back_demod,13381,demod,14258,14292,14292] x v (y v (z v ((c(y)^ (c(x)^c(u))) v u)))=1.

given clause #878: (wt=11) 15423 [para_from,14291,14277] (c(x)^c(y))^ (x v y)=0.

given clause #879: (wt=11) 15457 [para_into,14249,14565] (x^c(y)) v (y v c(x))=1.

given clause #880: (wt=11) 15665 [para_into,14281,14565] (x v c(y))^ (y^c(x))=0.

given clause #881: (wt=18) 14415 [back_demod,13379,demod,14258,14292,14292] x v ((c(y)^ (c(x)^c(z))) v (y v (u v z)))=1.

given clause #882: (wt=11) 15806 [para_into,14283,14565] (x^y)^ (c(y) v c(x))=0.

given clause #883: (wt=11) 15920 [para_into,14285,14565] (x^y) v (c(y) v c(x))=1.

given clause #884: (wt=11) 15922 [para_into,14285,2] c(x) v ((x^y) v c(y))=1.

given clause #885: (wt=16) 14417 [back_demod,13353,demod,14258,14292,14292] x v ((c(y)^ (c(x)^c(z))) v (y v z))=1.

given clause #886: (wt=11) 16714 [para_into,14339,14565] (x v y)^ (c(y)^c(x))=0.

given clause #887: (wt=11) 16790 [para_into,14341,14565] (c(x)^y) v (c(y) v x)=1.

given clause #888: (wt=11) 16902 [para_into,14343,14565] (x^c(y))^ (y v c(x))=0.

given clause #889: (wt=16) 14421 [back_demod,13349,demod,14258,14292,14292] x v (y v ((c(y)^ (c(x)^c(z))) v z))=1.

given clause #890: (wt=11) 16910 [para_into,16855,14737] (x^y) v (y v z)=y v z.

given clause #891: (wt=11) 16990 [para_into,14345,14565] (c(x)^y)^ (c(y) v x)=0.

given clause #892: (wt=11) 17188 [para_into,14351,16074,demod,14182,14148,14182] (x^y) v (x v z)=x v z.

given clause #893: (wt=16) 14423 [back_demod,13347,demod,14258,14292,14292] (c(x)^ (c(y)^c(z))) v (y v (x v z))=1.

given clause #894: (wt=11) 17378 [para_into,14359,14565] (c(x) v y)^ (c(y)^x)=0.

given clause #895: (wt=11) 17614 [para_from,14369,14343,demod,14182,14292,14366,14182,14142] x^ ((c(x) v y)^c(y))=0.

given clause #896: (wt=11) 17618 [para_from,14369,14339,demod,14292,14366,14182,14182,14148] c(x)^ ((x v y)^c(y))=0.

given clause #897: (wt=13) 14441 [back_demod,12240,demod,14152,14292,14152] (c(x)^c(y)) v (z v (x v y))=1.

given clause #898: (wt=11) 17780 [para_into,17732,14225] x^ (y v (z v (x v u)))=x.

given clause #899: (wt=11) 17854 [para_into,17782,14879] (x^y)^ (z v x)=x^y.

given clause #900: (wt=11) 17856 [para_into,17782,14600] (x^y)^ (z v y)=x^y.

given clause #901: (wt=16) 14443 [back_demod,9987,demod,14152] (x^ (c(y) v c(z)))^ (c(x) v (y^z))=0.

given clause #902: (wt=11) 17982 [para_into,17862,14879] (x^y)^ (x v z)=x^y.

given clause #903: (wt=11) 17984 [para_into,17862,14600] (x^y)^ (y v z)=x^y.

given clause #904: (wt=11) 18106 [para_into,14429,14565] (c(x)^c(y)) v (y v x)=1.

given clause #905: (wt=16) 14447 [back_demod,9845,demod,14152,14292,14292,14152] (c(x)^ (c(y)^c(z))) v (x v (y v z))=1.

given clause #906: (wt=11) 18126 [para_into,14449,14369,demod,14292,14366,14182,14182,14142] ((x v y)^c(y))^c(x)=0.

given clause #907: (wt=11) 18415 [para_into,14562,14565] (x v y) v z=y v (x v z).

given clause #908: (wt=11) 18938 [back_demod,15340,demod,18569] (x v y)^c(x)=y^c(x).

given clause #909: (wt=16) 14451 [back_demod,2201,demod,14152,14152,14292,14292] (x v (y v z))^ (c(y)^ (c(x)^c(z)))=0.

given clause #910: (wt=11) 18981 [para_from,14562,17782] x^ (y v (z v (u v x)))=x.

given clause #911: (wt=11) 19157 [para_into,19111,98] (x v (y v (z v u)))^z=z.

given clause #912: (wt=11) 19199 [para_into,19149,14867] (x v y)^ (y^z)=y^z.

given clause #913: (wt=16) 14453 [back_demod,2199,demod,14152,14152,14292,14292] (x v (y v z))^ (c(x)^ (c(y)^c(z)))=0.

given clause #914: (wt=11) 19209 [para_into,19149,14145] (x v y)^ (z^y)=z^y.

given clause #915: (wt=11) 19217 [para_into,19161,14562] (x v (y v (z v u)))^u=u.

given clause #916: (wt=11) 19255 [para_into,18987,14181] c(x) v (y^x)=c(x) v y.

given clause #917: (wt=17) 14455 [back_demod,1567,demod,14152,14292,14292,14152,14292,14292] c(x)^ (c(y)^c(z))=c(y)^ (c(x)^c(z)).

given clause #918: (wt=10) 22207 [para_into,19255,20769,demod,14292,14182,14292,14182,14880] (x^c(y)) v (x^y)=x.

given clause #919: (wt=10) 22209 [para_into,19255,20767,demod,14292,14182,14292,14182,14601] (c(x)^y) v (y^x)=y.

given clause #920: (wt=10) 22238 [para_into,22207,14181] (x^y) v (x^c(y))=x.

given clause #921: (wt=15) 14460 [back_demod,14263,demod,14292,14292,14292,14366,14182,14366,14182,14182,14292] x v ((y v (x v z))^ (c(y)^c(z)))=x.

given clause #922: (wt=10) 22240 [para_into,22207,20740] (x^c(y)) v (y^x)=x.

given clause #923: (wt=10) 22267 [para_into,22209,14181] (x^y) v (y^c(x))=y.

given clause #924: (wt=10) 22269 [para_into,22209,20740] (c(x)^y) v (x^y)=y.

given clause #925: (wt=13) 14464 [back_demod,14255,demod,14292,14292,14366,14182,14182,14292] x v ((x v y)^ (c(z)^c(y)))=x.

given clause #926: (wt=10) 22271 [para_into,22209,14565] (x^y) v (c(y)^x)=x.

given clause #927: (wt=10) 22394 [para_into,22267,20740] (x^y) v (c(x)^y)=y.

given clause #928: (wt=11) 19413 [para_into,19035,14561,demod,19036] (x v y)^z= (y v x)^z.

given clause #929: (wt=15) 14468 [back_demod,52,demod,14292] (x v (c(y)^c(z)))^ (y v (x v z))=x.

given clause #930: (wt=11) 20373 [para_into,14598,17512,demod,14146,flip.1] ((x^ (y^z))^u) v z=z.

given clause #931: (wt=11) 20375 [para_into,14598,17388,demod,14146,flip.1] (((x^y)^z)^u) v y=y.

given clause #932: (wt=11) 20377 [para_into,14598,17206,demod,14146,flip.1] (x^ ((y^z)^u)) v z=z.

given clause #933: (wt=16) 14472 [para_from,14181,203] (c(x) v (y^c(z)))^ (x^ (c(y) v z))=0.

given clause #934: (wt=11) 20379 [para_into,14598,16855,demod,14146,flip.1] (x^ (y^ (z^u))) v u=u.

given clause #935: (wt=11) 20494 [para_into,14859,17368,demod,17369] (x^ ((y^z)^u)) v y=y.

given clause #936: (wt=11) 20496 [para_into,14859,17202,demod,17203] (x^ (y^ (z^u))) v z=z.

given clause #937: (wt=16) 14476 [para_from,14181,203] (c(x) v (c(y)^z))^ (x^ (y v c(z)))=0.

given clause #938: (wt=11) 20531 [para_into,14907,17512,demod,14868,flip.1] ((x^ (y^z))^u) v y=y.

given clause #939: (wt=11) 20533 [para_into,14907,17388,demod,14868,flip.1] (((x^y)^z)^u) v x=x.

given clause #940: (wt=11) 20694 [para_into,20674,15621,demod,14292,14182,18988] (x v y)^ (y v x)=y v x.

given clause #941: (wt=16) 14480 [para_from,14181,203] (x v (y^z))^ (c(x)^ (c(y) v c(z)))=0.

given clause #942: (wt=11) 20712 [back_demod,15549,demod,20707] c(x)^ (x v y)=c(x)^y.

given clause #943: (wt=11) 20741 [para_into,20720,19322,demod,14182] c(x)^ (y v x)=c(x)^y.

given clause #944: (wt=11) 20783 [back_demod,19852,demod,20770] (x^y) v (y^x)=x^y.

given clause #945: (wt=17) 14514 [para_from,14227,96,flip.1] x v (y v (z v (u v x)))=y v (z v (u v x)).

given clause #946: (wt=11) 20786 [back_demod,19324,demod,20770] (x v y)^z=z^ (y v x).

given clause #947: (wt=11) 20788 [back_demod,19299,demod,20770] x^ (y v z)= (z v y)^x.

given clause #948: (wt=11) 20814 [para_into,20706,14181] c(x) v (x^y)=c(x) v y.

given clause #949: (wt=13) 14525 [para_from,14227,14,flip.1] x v (y v (z v x))=y v (z v x).

given clause #950: (wt=11) 20994 [para_into,20769,14562,demod,20993] x^ (y v z)=x^ (z v y).

given clause #951: (wt=11) 21072 [para_into,20775,14741,demod,14292,14182,14182,14152] (x^y)^ (y^x)=y^x.

given clause #952: (wt=11) 21464 [para_into,16910,2] x v ((y^x) v z)=x v z.

given clause #953: (wt=15) 14543 [para_from,14257,1130,demod,14258] x v (y v (z v u))=x v (u v (z v y)).

given clause #954: (wt=11) 21468 [back_demod,21087,demod,21465,flip.1] (x^y) v c(x)=y v c(x).

given clause #955: (wt=11) 21513 [para_from,16910,19111] (x v y)^ (z^x)=z^x.

given clause #956: (wt=11) 21587 [para_into,17188,2] x v ((x^y) v z)=x v z.

given clause #957: (wt=15) 14544 [para_from,14257,1063,demod,14258] x v (y v (z v u))=x v (u v (y v z)).

given clause #958: (wt=11) 21593 [back_demod,20672,demod,21588,flip.1] (x^y) v c(y)=x v c(y).

given clause #959: (wt=11) 21638 [para_from,17188,19111] (x v y)^ (x^z)=x^z.

given clause #960: (wt=11) 21974 [para_into,18938,14565] (x v y)^c(y)=x^c(y).

given clause #961: (wt=15) 14545 [para_from,14257,1059,demod,14258] x v (y v (z v u))=x v (z v (u v y)).

given clause #962: (wt=11) 22660 [para_into,20373,14565] x v ((y^ (z^x))^u)=x.

given clause #963: (wt=11) 22707 [para_into,20375,14565] x v (((y^x)^z)^u)=x.

given clause #964: (wt=11) 22752 [para_into,20377,14565] x v (y^ ((z^x)^u))=x.

given clause #965: (wt=15) 14546 [para_from,14257,950,demod,14258] x v (y v (z v u))=u v (z v (y v x)).

given clause #966: (wt=11) 22809 [para_into,20379,14565] x v (y^ (z^ (u^x)))=x.

given clause #967: (wt=11) 22840 [para_into,20494,14565] x v (y^ ((x^z)^u))=x.

given clause #968: (wt=11) 22871 [para_into,20496,14565] x v (y^ (z^ (x^u)))=x.

given clause #969: (wt=15) 14547 [para_from,14257,948,demod,14258] x v (y v (z v u))=x v (y v (u v z)).

given clause #970: (wt=11) 22904 [para_into,20531,14565] x v ((y^ (x^z))^u)=x.

given clause #971: (wt=11) 22927 [para_into,20533,14565] x v (((x^y)^z)^u)=x.

given clause #972: (wt=11) 23039 [para_from,20783,19413,demod,20784] (x^y)^z= (y^x)^z.

given clause #973: (wt=15) 14548 [para_from,14257,906,demod,14258] x v (y v (z v u))=z v (u v (y v x)).

given clause #974: (wt=11) 23048 [para_from,20783,14563,demod,23045] x v (y^z)= (z^y) v x.

given clause #975: (wt=11) 23049 [para_from,20783,14561,demod,20784] x v (y^z)=x v (z^y).

given clause #976: (wt=11) 23056 [copy,23048,flip.1] (x^y) v z=z v (y^x).

given clause #977: (wt=15) 14549 [para_from,14257,905,demod,14258] x v (y v (z v u))=u v (y v (z v x)).

given clause #978: (wt=11) 23064 [para_into,20786,20783,demod,20784] (x^y)^z=z^ (y^x).

given clause #979: (wt=11) 23096 [copy,23064,flip.1] x^ (y^z)= (z^y)^x.

given clause #980: (wt=11) 23227 [para_into,20994,20783,demod,20784] x^ (y^z)=x^ (z^y).

given clause #981: (wt=15) 14550 [para_from,14257,904,demod,14258] x v (y v (z v u))=u v (z v (x v y)).

given clause #982: (wt=11) 23407 [para_into,21587,21072,demod,23045] (x^y) v z= (y^x) v z.

given clause #983: (wt=12) 14803 [para_into,12512,14565] x v (y v (z v (c(x) v u)))=1.

given clause #984: (wt=12) 14955 [para_into,14317,98] c(x) v (y v (z v (x v u)))=1.

given clause #985: (wt=15) 14551 [para_from,14257,129,demod,14258] x v (y v (z v u))=y v (x v (u v z)).

given clause #986: (wt=12) 16998 [para_into,16734,392,demod,14292,14182,14292,14182] x^ (y^ (z^ (c(x)^u)))=0.

given clause #987: (wt=12) 17008 [para_into,16738,392,demod,14292,14182,14292,14182] x^ ((y^ (c(x)^z))^u)=0.

given clause #988: (wt=12) 17022 [para_into,16947,392,demod,14292,14182,14292,14182] (x^ (y^ (c(z)^u)))^z=0.

given clause #989: (wt=15) 14552 [para_from,14257,126,demod,14258] x v (y v (z v u))=z v (y v (u v x)).

given clause #990: (wt=12) 17110 [para_into,16951,392,demod,14292,14182,14292,14182] ((x^ (c(y)^z))^u)^y=0.

given clause #991: (wt=12) 17350 [para_into,17116,392,demod,14292,14182,14292,14182] (x^ (c(y)^z))^ (u^y)=0.

given clause #992: (wt=12) 17362 [para_into,17122,392,demod,14292,14182,14292,14182] (x^ (c(y)^z))^ (y^u)=0.

given clause #993: (wt=15) 14553 [para_from,14257,121,demod,14258] x v (y v (z v u))=z v (u v (x v y)).

given clause #994: (wt=12) 17626 [para_into,17180,392,demod,14292,14182,14292,14182] (x^y)^ (z^ (c(y)^u))=0.

given clause #995: (wt=12) 17638 [para_into,17306,392,demod,14292,14182,14292,14182] (x^y)^ (z^ (c(x)^u))=0.

given clause #996: (wt=12) 19378 [para_from,19019,17122,demod,14292,14182] (x^c(y))^ ((y^x)^z)=0.

given clause #997: (wt=15) 14554 [para_from,14257,120,demod,14258] x v (y v (z v u))=u v (y v (x v z)).

given clause #998: (wt=12) 19398 [para_from,19019,17306,demod,14292,14182] ((x^y)^z)^ (y^c(x))=0.

given clause #999: (wt=12) 19659 [para_from,19297,17122,demod,14292,14182] (c(x)^y)^ ((x^y)^z)=0.

given clause #1000: (wt=12) 19671 [para_from,19297,17306,demod,14292,14182] ((x^y)^z)^ (c(x)^y)=0.

given clause #1001: (wt=15) 14555 [para_from,14257,108,demod,14258] x v (y v (z v u))=y v (u v (x v z)).

given clause #1002: (wt=12) 20777 [back_demod,20556,demod,20768] (x v (c(y)^z))^y=y^x.

given clause #1003: (wt=12) 20779 [back_demod,20402,demod,20768] (x v (y^c(z)))^z=z^x.

given clause #1004: (wt=12) 20963 [para_from,20767,17116,demod,14292,14182] (c(x)^y)^ (z^ (y^x))=0.

given clause #1005: (wt=15) 14556 [para_from,14257,107,demod,14258] x v (y v (z v u))=z v (x v (u v y)).

given clause #1006: (wt=12) 20965 [para_from,20767,17122,demod,14292,14182] (c(x)^y)^ ((y^x)^z)=0.

given clause #1007: (wt=12) 20969 [para_from,20767,17180,demod,14292,14182] (x^ (y^z))^ (c(z)^y)=0.

given clause #1008: (wt=12) 20979 [para_from,20767,17306,demod,14292,14182] ((x^y)^z)^ (c(y)^x)=0.

given clause #1009: (wt=15) 14557 [para_from,14257,102,demod,14258] x v (y v (z v u))=y v (u v (z v x)).

given clause #1010: (wt=12) 20987 [para_into,20769,14907,demod,20768,flip.1] x^ (y v (c(x)^z))=x^y.

given clause #1011: (wt=12) 20989 [para_into,20769,14598,demod,20768,flip.1] x^ (y v (z^c(x)))=x^y.

given clause #1012: (wt=12) 21032 [para_from,20769,17116,demod,14292,14182] (x^c(y))^ (z^ (x^y))=0.

given clause #1013: (wt=15) 14558 [para_from,14257,101,demod,14258] x v (y v (z v u))=y v (z v (u v x)).

given clause #1014: (wt=12) 21034 [para_from,20769,17122,demod,14292,14182] (x^c(y))^ ((x^y)^z)=0.

given clause #1015: (wt=12) 21036 [para_from,20769,17180,demod,14292,14182] (x^ (y^z))^ (y^c(z))=0.

given clause #1016: (wt=12) 21044 [para_from,20769,17306,demod,14292,14182] ((x^y)^z)^ (x^c(y))=0.

given clause #1017: (wt=15) 14559 [para_from,14257,97,demod,14258] x v (y v (z v u))=u v (x v (z v y)).

given clause #1018: (wt=12) 22462 [para_into,14464,14181] x v ((x v y)^ (z^c(y)))=x.

given clause #1019: (wt=12) 22676 [para_from,20373,20767,demod,31,flip.1] x^ ((y^ (z^c(x)))^u)=0.

given clause #1020: (wt=12) 22721 [para_from,20375,20767,demod,31,flip.1] x^ (((y^c(x))^z)^u)=0.

given clause #1021: (wt=15) 14560 [para_from,14257,96,demod,14258] x v (y v (z v u))=u v (x v (y v z)).

given clause #1022: (wt=12) 22766 [para_from,20377,20767,demod,31,flip.1] x^ (y^ ((z^c(x))^u))=0.

given clause #1023: (wt=12) 22825 [para_from,20379,20767,demod,31,flip.1] x^ (y^ (z^ (u^c(x))))=0.

given clause #1024: (wt=12) 22852 [para_from,20494,20767,demod,31,flip.1] x^ (y^ ((c(x)^z)^u))=0.

given clause #1025: (wt=19) 14587 [para_from,14145,96,flip.1] x v (y v (z v (u v (v^x))))=y v (z v (u v x)).

given clause #1026: (wt=12) 22939 [para_from,20533,20767,demod,31,flip.1] x^ (((c(x)^y)^z)^u)=0.

given clause #1027: (wt=12) 22989 [para_into,20741,20533,demod,14278,flip.1] c(x)^ (((x^y)^z)^u)=0.

given clause #1028: (wt=12) 22991 [para_into,20741,20531,demod,14278,flip.1] c(x)^ ((y^ (x^z))^u)=0.

given clause #1029: (wt=15) 14596 [para_from,14145,14,flip.1] x v (y v (z v (u^x)))=y v (z v x).

given clause #1030: (wt=12) 22993 [para_into,20741,20496,demod,14278,flip.1] c(x)^ (y^ (z^ (x^u)))=0.

given clause #1031: (wt=12) 22995 [para_into,20741,20494,demod,14278,flip.1] c(x)^ (y^ ((x^z)^u))=0.

given clause #1032: (wt=12) 22997 [para_into,20741,20379,demod,14278,flip.1] c(x)^ (y^ (z^ (u^x)))=0.

given clause #1033: (wt=15) 14656 [para_from,14565,392] (x v (y^z))^ (c(y) v (c(z) v x))=x.

given clause #1034: (wt=12) 22999 [para_into,20741,20377,demod,14278,flip.1] c(x)^ (y^ ((z^x)^u))=0.

given clause #1035: (wt=12) 23001 [para_into,20741,20375,demod,14278,flip.1] c(x)^ (((y^x)^z)^u)=0.

given clause #1036: (wt=12) 23003 [para_into,20741,20373,demod,14278,flip.1] c(x)^ ((y^ (z^x))^u)=0.

given clause #1037: (wt=19) 14698 [para_from,14565,1130] x v (y v (z v (u v v)))=x v (v v (z v (y v u))).

given clause #1038: (wt=12) 23315 [para_from,21464,20769,demod,20770,flip.1] x^ ((y^c(x)) v z)=x^z.

given clause #1039: (wt=12) 23317 [para_from,21464,19035,demod,19036,flip.1] ((x^c(y)) v z)^y=z^y.

given clause #1040: (wt=12) 23436 [para_from,21587,20769,demod,20770,flip.1] x^ ((c(x)^y) v z)=x^z.

given clause #1041: (wt=19) 14699 [para_from,14565,1063] x v (y v (z v (u v v)))=x v (v v (y v (z v u))).

given clause #1042: (wt=12) 23438 [para_from,21587,19035,demod,19036,flip.1] ((c(x)^y) v z)^x=z^x.

given clause #1043: (wt=12) 23537 [para_into,21974,20533,demod,31,flip.1] (((x^y)^z)^u)^c(x)=0.

given clause #1044: (wt=12) 23539 [para_into,21974,20531,demod,31,flip.1] ((x^ (y^z))^u)^c(y)=0.

given clause #1045: (wt=19) 14700 [para_from,14565,1059] x v (y v (z v (u v v)))=x v (z v (v v (y v u))).

given clause #1046: (wt=12) 23541 [para_into,21974,20496,demod,31,flip.1] (x^ (y^ (z^u)))^c(z)=0.

given clause #1047: (wt=12) 23543 [para_into,21974,20494,demod,31,flip.1] (x^ ((y^z)^u))^c(y)=0.

given clause #1048: (wt=12) 23545 [para_into,21974,20379,demod,31,flip.1] (x^ (y^ (z^u)))^c(u)=0.

given clause #1049: (wt=19) 14701 [para_from,14565,950] x v (y v (z v (u v v)))=v v (z v (y v (x v u))).

given clause #1050: (wt=12) 23547 [para_into,21974,20377,demod,31,flip.1] (x^ ((y^z)^u))^c(z)=0.

given clause #1051: (wt=12) 23549 [para_into,21974,20375,demod,31,flip.1] (((x^y)^z)^u)^c(y)=0.

given clause #1052: (wt=12) 23551 [para_into,21974,20373,demod,31,flip.1] ((x^ (y^z))^u)^c(z)=0.

given clause #1053: (wt=19) 14702 [para_from,14565,948] x v (y v (z v (u v v)))=x v (y v (v v (z v u))).

given clause #1054: (wt=12) 23581 [para_from,22660,19035,demod,14278,flip.1] ((x^ (y^c(z)))^u)^z=0.

given clause #1055: (wt=12) 23590 [para_from,22707,19035,demod,14278,flip.1] (((x^c(y))^z)^u)^y=0.

given clause #1056: (wt=12) 23599 [para_from,22752,19035,demod,14278,flip.1] (x^ ((y^c(z))^u))^z=0.

given clause #1057: (wt=19) 14703 [para_from,14565,906] x v (y v (z v (u v v)))=z v (v v (y v (x v u))).

given clause #1058: (wt=12) 23632 [para_from,22809,19035,demod,14278,flip.1] (x^ (y^ (z^c(u))))^u=0.

given clause #1059: (wt=12) 23643 [para_from,22840,19035,demod,14278,flip.1] (x^ ((c(y)^z)^u))^y=0.

given clause #1060: (wt=12) 23688 [para_from,22927,19035,demod,14278,flip.1] (((c(x)^y)^z)^u)^x=0.

given clause #1061: (wt=19) 14704 [para_from,14565,905] x v (y v (z v (u v v)))=v v (y v (z v (x v u))).

given clause #1062: (wt=12) 24494 [para_into,17350,14181] (x^ (y^z))^ (u^c(y))=0.

given clause #1063: (wt=12) 24500 [para_into,17350,20740] (x^ (y^c(z)))^ (u^z)=0.

given clause #1064: (wt=12) 24502 [para_into,17350,23096] ((x^c(y))^z)^ (u^y)=0.

given clause #1065: (wt=19) 14705 [para_from,14565,904] x v (y v (z v (u v v)))=v v (z v (x v (y v u))).

given clause #1066: (wt=12) 24506 [para_into,17350,20959] ((c(x)^y)^z)^ (u^x)=0.

given clause #1067: (wt=12) 24542 [para_into,17350,23064] (x^y)^ ((c(y)^z)^u)=0.

given clause #1068: (wt=12) 24548 [para_into,17362,14181] (x^ (y^z))^ (c(y)^u)=0.

given clause #1069: (wt=19) 14706 [para_from,14565,129] x v (y v (z v (u v v)))=y v (x v (v v (z v u))).

given clause #1070: (wt=12) 24554 [para_into,17362,20740] (x^ (y^c(z)))^ (z^u)=0.

given clause #1071: (wt=12) 24556 [para_into,17362,23096] ((x^c(y))^z)^ (y^u)=0.

given clause #1072: (wt=12) 24560 [para_into,17362,20959] ((c(x)^y)^z)^ (x^u)=0.

given clause #1073: (wt=19) 14707 [para_from,14565,126] x v (y v (z v (u v v)))=z v (y v (v v (x v u))).

given clause #1074: (wt=12) 24564 [para_into,17362,23064] (x^y)^ ((c(x)^z)^u)=0.

given clause #1075: (wt=12) 24592 [para_into,17626,21974,demod,14182] (x^c(y))^ (z^ (y^u))=0.

given clause #1076: (wt=12) 24632 [para_into,17626,20740] (x^y)^ (z^ (u^c(y)))=0.

given clause #1077: (wt=19) 14708 [para_from,14565,121] x v (y v (z v (u v v)))=z v (v v (x v (y v u))).

given clause #1078: (wt=12) 24634 [para_into,17626,23096] (x^y)^ ((z^c(y))^u)=0.

given clause #1079: (wt=12) 24636 [para_into,17638,20741,demod,14182] (c(x)^y)^ (z^ (x^u))=0.

given clause #1080: (wt=12) 24648 [para_into,17638,20740] (x^y)^ (z^ (u^c(x)))=0.

given clause #1081: (wt=19) 14709 [para_from,14565,120] x v (y v (z v (u v v)))=v v (y v (x v (z v u))).

given clause #1082: (wt=12) 24650 [para_into,17638,23096] (x^y)^ ((z^c(x))^u)=0.

given clause #1083: (wt=12) 24841 [para_into,20777,18568,demod,23439,14366,14182,flip.1] x^ (y^ (x v c(z)))=y^x.

given clause #1084: (wt=11) 26808 [para_into,24841,14181] x^ (y^ (x v z))=y^x.

given clause #1085: (wt=19) 14710 [para_from,14565,108] x v (y v (z v (u v v)))=y v (v v (x v (z v u))).

given clause #1086: (wt=11) 26851 [para_into,26808,14907] x^ (y^ (z v x))=y^x.

given clause #1087: (wt=11) 26869 [para_into,26808,20959,demod,14292,20778] x^ ((x v y)^z)=x^z.

given clause #1088: (wt=11) 26872 [para_into,26808,17784,demod,26809,flip.1] (x^ (y v z))^y=x^y.

given clause #1089: (wt=19) 14711 [para_from,14565,107] x v (y v (z v (u v v)))=z v (x v (v v (y v u))).

given clause #1090: (wt=11) 27026 [para_into,26851,20959,demod,14292,20780] x^ ((y v x)^z)=x^z.

given clause #1091: (wt=11) 27341 [para_into,26872,22271,demod,27178] (x^y)^z=x^ (y^z).

given clause #1092: (wt=11) 27345 [para_into,26872,23064,demod,27342,27342,23404,27342] x^ (y^z)=y^ (x^z).

given clause #1093: (wt=19) 14712 [para_from,14565,102] x v (y v (z v (u v v)))=y v (v v (z v (x v u))).

given clause #1094: (wt=11) 27350 [back_demod,24289,demod,27342,27342,27342,27342,19120,19122,19118] x^ (y^z)=z^ (y^x).

given clause #1095: (wt=11) 27448 [back_demod,26885,demod,27342,19120] x^ (y^z)=z^ (x^y).

given clause #1096: (wt=11) 27452 [back_demod,26840,demod,27342,19120] x^ (y^z)=y^ (z^x).

given clause #1097: (wt=19) 14713 [para_from,14565,101] x v (y v (z v (u v v)))=y v (z v (v v (x v u))).

given clause #1098: (wt=12) 25350 [para_into,22462,14565] x v ((y v x)^ (z^c(y)))=x.

given clause #1099: (wt=12) 25370 [para_into,22462,14181] x v ((x v c(y))^ (z^y))=x.

given clause #1100: (wt=12) 26938 [para_from,26808,20718,demod,18569,flip.1] x v (y^ (c(x) v z))=x v y.

given clause #1101: (wt=19) 14714 [para_from,14565,97] x v (y v (z v (u v v)))=v v (x v (z v (y v u))).

given clause #1102: (wt=12) 27032 [para_into,26851,14656,demod,19086,flip.1] (x v (y^z))^ (c(z) v x)=x.

given clause #1103: (wt=12) 27040 [para_into,26851,14347,demod,19112,flip.1] (x v (y^c(z)))^ (x v z)=x.

given clause #1104: (wt=12) 27042 [para_into,26851,392,demod,19112,flip.1] (x v (y^z))^ (x v c(z))=x.

given clause #1105: (wt=19) 14715 [para_from,14565,96] x v (y v (z v (u v v)))=v v (x v (y v (z v u))).

given clause #1106: (wt=12) 27096 [para_from,26851,20718,demod,18569,flip.1] x v (y^ (z v c(x)))=x v y.

given clause #1107: (wt=12) 27264 [para_from,26869,20718,demod,20719,flip.1] x v ((c(x) v y)^z)=x v z.

given clause #1108: (wt=12) 28005 [para_from,27026,20718,demod,20719,flip.1] x v ((y v c(x))^z)=x v z.

given clause #1109: (wt=15) 14718 [para_from,14565,392] ((x^y) v z)^ (c(x) v (z v c(y)))=z.

given clause #1110: (wt=12) 28593 [para_into,26938,23048] ((c(x) v y)^z) v x=x v z.

given clause #1111: (wt=12) 28595 [para_into,26938,14565] (x^ (c(y) v z)) v y=y v x.

given clause #1112: (wt=12) 28625 [para_into,27032,27032,demod,14292,14182] (x v y)^ ((z^c(y)) v x)=x.

given clause #1113: (wt=15) 14720 [para_from,14565,42] ((x^y) v z)^ (z v (c(x) v c(y)))=z.

given clause #1114: (wt=12) 28641 [para_into,27032,21974,demod,14182] (x v (y^c(z)))^ (z v x)=x.

given clause #1115: (wt=12) 28649 [para_into,27032,20959] (x v (y^z))^ (c(y) v x)=x.

given clause #1116: (wt=12) 28667 [para_into,27032,15332,demod,14292,14182] (x v y)^ ((c(y)^z) v x)=x.

given clause #1117: (wt=15) 14726 [para_from,14565,42] (x v (y^z))^ (x v (c(z) v c(y)))=x.

given clause #1118: (wt=12) 28681 [para_into,27032,23048] ((x^y) v z)^ (c(x) v z)=z.

given clause #1119: (wt=12) 28685 [para_into,27032,14565] ((x^y) v z)^ (c(y) v z)=z.

given clause #1120: (wt=12) 28707 [para_into,27032,20788] (x v c(y))^ (x v (z^y))=x.

given clause #1121: (wt=13) 14736 [para_from,14565,13] A^ (C v B)!= (A^B) v (A^C)|$Ans(DIST1).

given clause #1122: (wt=12) 28709 [para_into,27032,20786] (c(x) v y)^ ((z^x) v y)=y.

given clause #1123: (wt=12) 28711 [para_into,27032,20740] (c(x) v y)^ (y v (z^x))=y.

given clause #1124: (wt=12) 28730 [para_into,27040,20959] (x v (c(y)^z))^ (x v y)=x.

given clause #1125: (wt=19) 14781 [copy,14698,flip.1] x v (y v (z v (u v v)))=x v (u v (z v (v v y))).

given clause #1126: (wt=12) 28736 [para_into,27040,23048] ((c(x)^y) v z)^ (z v x)=z.

given clause #1127: (wt=12) 28740 [para_into,27040,14565] ((x^c(y)) v z)^ (z v y)=z.

given clause #1128: (wt=12) 28786 [para_into,27040,20788] (x v y)^ (y v (z^c(x)))=y.

given clause #1129: (wt=19) 14782 [copy,14699,flip.1] x v (y v (z v (u v v)))=x v (z v (u v (v v y))).

given clause #1130: (wt=12) 28788 [para_into,27040,20740] (x v y)^ (x v (z^c(y)))=x.

given clause #1131: (wt=12) 28811 [para_into,27042,27042,demod,14292,14182] (x v y)^ (x v (c(y)^z))=x.

given clause #1132: (wt=12) 28833 [para_into,27042,20959] (x v (y^z))^ (x v c(y))=x.

given clause #1133: (wt=19) 14783 [copy,14700,flip.1] x v (y v (z v (u v v)))=x v (u v (y v (v v z))).

given clause #1134: (wt=12) 28859 [para_into,27042,23048] ((x^y) v z)^ (z v c(x))=z.

given clause #1135: (wt=12) 28861 [para_into,27042,14565] ((x^y) v z)^ (z v c(y))=z.

given clause #1136: (wt=12) 28867 [para_into,27042,20786] (x v c(y))^ ((z^y) v x)=x.

given clause #1137: (wt=19) 14784 [copy,14701,flip.1] x v (y v (z v (u v v)))=u v (z v (y v (v v x))).

given clause #1138: (wt=12) 28888 [para_into,27096,23048] ((x v c(y))^z) v y=y v z.

given clause #1139: (wt=12) 28890 [para_into,27096,14565] (x^ (y v c(z))) v z=z v x.

given clause #1140: (wt=12) 29116 [para_into,28625,14565] (x v y)^ ((z^c(x)) v y)=y.

given clause #1141: (wt=19) 14785 [copy,14702,flip.1] x v (y v (z v (u v v)))=x v (y v (u v (v v z))).

given clause #1142: (wt=12) 29150 [para_into,28625,20786] ((x^c(y)) v z)^ (y v z)=z.

given clause #1143: (wt=12) 29171 [para_into,28641,20959] (x v (c(y)^z))^ (y v x)=x.

given clause #1144: (wt=12) 29175 [para_into,28641,23048] ((c(x)^y) v z)^ (x v z)=z.

given clause #1145: (wt=19) 14786 [copy,14703,flip.1] x v (y v (z v (u v v)))=u v (z v (x v (v v y))).

given clause #1146: (wt=12) 29246 [para_into,28649,20788] (x v c(y))^ (x v (y^z))=x.

given clause #1147: (wt=12) 29248 [para_into,28649,20786] (c(x) v y)^ ((x^z) v y)=y.

given clause #1148: (wt=12) 29250 [para_into,28649,20740] (c(x) v y)^ (y v (x^z))=y.

given clause #1149: (wt=19) 14787 [copy,14704,flip.1] x v (y v (z v (u v v)))=u v (y v (z v (v v x))).

given clause #1150: (wt=12) 29305 [para_into,28667,14907,demod,14292,14366,27342,29033] (x v y)^ (y v (c(x)^z))=y.

given clause #1151: (wt=12) 29309 [para_into,28667,14565] (x v y)^ ((c(x)^z) v y)=y.

given clause #1152: (wt=12) 29327 [para_into,28667,14181] (x v c(y))^ ((y^z) v x)=x.

given clause #1153: (wt=19) 14788 [copy,14705,flip.1] x v (y v (z v (u v v)))=z v (u v (y v (v v x))).

given clause #1154: (wt=13) 14829 [para_into,14600,2] x v ((y^ (x v z)) v z)=x v z.

given clause #1155: (wt=13) 14917 [para_into,14879,2] x v (((x v y)^z) v y)=x v y.

given clause #1156: (wt=13) 15019 [back_demod,14520,demod,15016] x v (y v (x v z))=y v (x v z).

given clause #1157: (wt=19) 14789 [copy,14706,flip.1] x v (y v (z v (u v v)))=y v (x v (u v (v v z))).

given clause #1158: (wt=13) 15415 [para_from,14291,15171] (x v y)^ (z^ (c(x)^c(y)))=0.

given clause #1159: (wt=13) 15535 [para_from,14249,2,demod,12035,flip.1] (x^c(y)) v (z v (c(x) v y))=1.

given clause #1160: (wt=13) 15705 [para_from,14365,15175] (c(x) v c(y))^ (z^ (x^y))=0.

given clause #1161: (wt=19) 14790 [copy,14707,flip.1] x v (y v (z v (u v v)))=u v (y v (x v (v v z))).

given clause #1162: (wt=13) 16098 [para_into,14297,14181] (c(x)^y) v (z v (x v c(y)))=1.

given clause #1163: (wt=13) 16104 [para_into,14297,14565] (x^y) v (z v (c(y) v c(x)))=1.

given clause #1164: (wt=13) 16892 [para_from,16851,2,flip.1] x v (y v (z^ (u^x)))=y v x.

given clause #1165: (wt=19) 14791 [copy,14708,flip.1] x v (y v (z v (u v v)))=z v (u v (x v (v v y))).

given clause #1166: (wt=13) 16935 [para_from,16855,14329,demod,14528,16856] (x^ (y^z)) v (u v z)=u v z.

given clause #1167: (wt=13) 17241 [para_from,17202,2,flip.1] x v (y v (z^ (x^u)))=y v x.

given clause #1168: (wt=13) 17264 [para_from,17206,14329,demod,14528,17207] (x^ (y^z)) v (u v y)=u v y.

given clause #1169: (wt=19) 14792 [copy,14709,flip.1] x v (y v (z v (u v v)))=z v (y v (u v (v v x))).

given clause #1170: (wt=13) 17794 [para_into,17732,2] (x v y)^ (x v (z v y))=x v y.

given clause #1171: (wt=13) 17804 [para_into,17772,950] x^ (y v (z v (u v (x v v))))=x.

given clause #1172: (wt=13) 18169 [para_into,14561,14879,flip.1] ((x v y)^z) v (y v x)=x v y.

given clause #1173: (wt=19) 14793 [copy,14710,flip.1] x v (y v (z v (u v v)))=z v (x v (u v (v v y))).

given clause #1174: (wt=13) 18173 [para_into,14561,14600,flip.1] (x^ (y v z)) v (z v y)=y v z.

given clause #1175: (wt=13) 18192 [para_from,14561,17732] (x v y)^ (z v (y v x))=x v y.

given clause #1176: (wt=13) 18205 [para_from,14561,14295,demod,14292] (c(x)^c(y)) v (z v (y v x))=1.

given clause #1177: (wt=19) 14794 [copy,14711,flip.1] x v (y v (z v (u v v)))=y v (u v (x v (v v z))).

given clause #1178: (wt=13) 18409 [para_into,14562,14879,flip.1] x v (y v ((y v x)^z))=y v x.

given clause #1179: (wt=13) 18413 [para_into,14562,14600,flip.1] x v (y v (z^ (y v x)))=y v x.

given clause #1180: (wt=13) 18431 [para_into,14562,14297,demod,18416,flip.1] c(x) v (c(y) v (z v (y^x)))=1.

given clause #1181: (wt=19) 14795 [copy,14712,flip.1] x v (y v (z v (u v v)))=u v (x v (z v (v v y))).

given clause #1182: (wt=13) 18848 [back_demod,14871,demod,18416] c(x) v (c(y) v (z v (x^y)))=1.

given clause #1183: (wt=13) 18948 [para_from,14562,17732] (x v y)^ (y v (x v z))=x v y.

given clause #1184: (wt=13) 19051 [back_demod,18522,demod,19036] x v (y v ((x v y)^z))=y v x.

given clause #1185: (wt=19) 14796 [copy,14713,flip.1] x v (y v (z v (u v v)))=u v (x v (y v (v v z))).

given clause #1186: (wt=13) 19117 [para_into,19085,17202] x^ (y^ (x^z))=y^ (x^z).

given clause #1187: (wt=13) 19119 [para_into,19085,16851] x^ (y^ (z^x))=y^ (z^x).

given clause #1188: (wt=13) 19123 [para_into,19085,14562] (x v (y v z))^ (y v x)=y v x.

given clause #1189: (wt=19) 14797 [copy,14714,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (v v x))).

given clause #1190: (wt=13) 19125 [para_into,19085,14561] (x v (y v z))^ (z v y)=z v y.

given clause #1191: (wt=13) 19141 [para_into,19085,2] (x v (y v z))^ (x v z)=x v z.

given clause #1192: (wt=13) 19151 [para_into,19111,950] (x v (y v (z v (u v v))))^u=u.

given clause #1193: (wt=19) 14798 [copy,14715,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (v v x))).

given clause #1194: (wt=13) 19314 [para_into,19019,13279,demod,14142,14182,flip.1] (x v (y v (z v (u v v))))^v=v.

given clause #1195: (wt=13) 20150 [para_into,14563,14600,flip.1] x v (y v (z^ (x v y)))=x v y.

given clause #1196: (wt=13) 20180 [para_from,14563,17732] (x v y)^ (x v (y v z))=x v y.

given clause #1197: (wt=16) 14811 [para_from,12512,906,demod,12035,12035,flip.1] x v (y v (z v (u v (v v (w v c(x))))))=1.

given clause #1198: (wt=13) 20207 [para_from,14563,19085] (x v (y v z))^ (x v y)=x v y.

given clause #1199: (wt=13) 20226 [back_demod,18722,demod,20193] x v (((y v x)^z) v y)=x v y.

given clause #1200: (wt=13) 20280 [para_into,14564,14600,flip.1] x v ((y^ (z v x)) v z)=z v x.

given clause #1201: (wt=18) 14813 [para_from,12512,950,demod,12035,12035,12035,flip.1] x v (y v (z v (u v (v v (w v (v6 v c(x)))))))=1.

given clause #1202: (wt=13) 20308 [para_from,14564,17732] (x v y)^ (y v (z v x))=x v y.

given clause #1203: (wt=13) 20343 [para_from,14564,19085] (x v (y v z))^ (z v x)=z v x.

given clause #1204: (wt=13) 20523 [para_from,14859,19161] (x v (y v z))^ (u^z)=u^z.

given clause #1205: (wt=19) 14821 [para_into,14600,122] (x^ (y v (z v u))) v (z v (y v u))=y v (z v u).

given clause #1206: (wt=13) 20629 [para_from,14947,19161] (x v (y v z))^ (z^u)=z^u.

given clause #1207: (wt=13) 20809 [para_from,20740,13] (B v C)^A!= (A^B) v (A^C)|$Ans(DIST1).

given clause #1208: (wt=13) 21015 [para_into,20769,13279,demod,14142,14182,flip.1] x^ (y v (z v (u v (v v x))))=x.

given clause #1209: (wt=19) 14823 [para_into,14600,98] x v (y v ((z^ (y v (x v u))) v u))=y v (x v u).

given clause #1210: (wt=13) 21194 [para_from,15457,2,demod,12035,flip.1] (x^c(y)) v (z v (y v c(x)))=1.

given clause #1211: (wt=13) 21268 [para_from,15920,14347,demod,14292,14182,14182,12035,14142] (x^y) v (z^ (y^x))=x^y.

given clause #1212: (wt=13) 21412 [para_from,16790,2,demod,12035,flip.1] (c(x)^y) v (z v (c(y) v x))=1.

given clause #1213: (wt=19) 14825 [para_into,14600,15] x v (y v ((z^ (x v (y v u))) v u))=x v (y v u).

given clause #1214: (wt=13) 21440 [para_into,16910,16910,demod,16911] (x^ (y^z)) v (z v u)=z v u.

given clause #1215: (wt=13) 21517 [para_from,16910,19161] (x v (y v z))^ (u^y)=u^y.

given clause #1216: (wt=13) 21642 [para_from,17188,16910,demod,17189] (x^ (y^z)) v (y v u)=y v u.

given clause #1217: (wt=19) 14827 [para_into,14600,14] x v ((y^ (z v (x v u))) v (z v u))=z v (x v u).

given clause #1218: (wt=13) 21644 [para_from,17188,19161] (x v (y v z))^ (y^u)=y^u.

given clause #1219: (wt=13) 21942 [para_into,18415,17206,flip.1] x v ((y^ (x^z)) v u)=x v u.

given clause #1220: (wt=13) 21944 [para_into,18415,16855,flip.1] x v ((y^ (z^x)) v u)=x v u.

given clause #1221: (wt=19) 14844 [para_from,14600,96,flip.1] (x^y) v (z v (u v (v v y)))=z v (u v (v v y)).

given clause #1222: (wt=13) 21985 [back_demod,21972,demod,21975] (x v (y^z))^c(z)=x^c(z).

given clause #1223: (wt=13) 21987 [back_demod,21970,demod,21975] (x v (y^z))^c(y)=x^c(y).

given clause #1224: (wt=13) 22821 [para_from,20379,14907,demod,14868,flip.1] (x^ (y^ (z^ (u^v)))) v u=u.

given clause #1225: (wt=17) 14846 [para_from,14600,98] x v (y v z)=y v ((u^ (y v z)) v (x v z)).

given clause #1226: (wt=13) 22823 [para_from,20379,14598,demod,14146,flip.1] (x^ (y^ (z^ (u^v)))) v v=v.

given clause #1227: (wt=13) 22972 [para_into,20712,14907,demod,20742,flip.1] c(x)^ (y v (x^z))=c(x)^y.

given clause #1228: (wt=13) 22974 [para_into,20712,14598,demod,20742,flip.1] c(x)^ (y v (z^x))=c(x)^y.

given clause #1229: (wt=15) 14853 [para_from,14600,14,flip.1] (x^y) v (z v (u v y))=z v (u v y).

given clause #1230: (wt=13) 23031 [para_from,20783,14859,demod,20784] (x^ (y^z)) v (z^y)=z^y.

given clause #1231: (wt=13) 23050 [para_from,20783,19149] (x v (y^z))^ (z^y)=z^y.

given clause #1232: (wt=13) 23196 [para_from,20788,13] (C v B)^A!= (A^B) v (A^C)|$Ans(DIST1).

given clause #1233: (wt=14) 14865 [para_from,14295,950,demod,12035,12035,12035,flip.1] c(x) v (y v (z v (u v (v v x))))=1.

given clause #1234: (wt=13) 23253 [para_from,21072,16264,demod,14366] (c(x) v c(y))^ (z^ (y^x))=0.

given clause #1235: (wt=13) 23331 [para_from,21464,20712,demod,20713,flip.1] c(x)^ ((y^x) v z)=c(x)^z.

given clause #1236: (wt=13) 23339 [para_from,21464,18938,demod,18939,flip.1] ((x^y) v z)^c(y)=z^c(y).

given clause #1237: (wt=19) 14896 [para_from,14867,96,flip.1] x v (y v (z v (u v (x^v))))=y v (z v (u v x)).

given clause #1238: (wt=13) 23452 [para_from,21587,20712,demod,20713,flip.1] c(x)^ ((x^y) v z)=c(x)^z.

given clause #1239: (wt=13) 23460 [para_from,21587,18938,demod,18939,flip.1] ((x^y) v z)^c(x)=z^c(x).

given clause #1240: (wt=13) 23535 [para_into,21638,21072,demod,21073] ((x^y) v z)^ (y^x)=y^x.

given clause #1241: (wt=15) 14905 [para_from,14867,14,flip.1] x v (y v (z v (x^u)))=y v (z v x).

given clause #1242: (wt=13) 23628 [para_from,22809,21464,demod,14146,flip.1] x v (y^ (z^ (u^ (v^x))))=x.

given clause #1243: (wt=13) 23630 [para_from,22809,21587,demod,14868,flip.1] x v (y^ (z^ (u^ (x^v))))=x.

given clause #1244: (wt=13) 26860 [para_into,26808,14596] x^ (y^ (z v (u v x)))=y^x.

given clause #1245: (wt=19) 14909 [para_into,14879,122] ((x v (y v z))^u) v (y v (x v z))=x v (y v z).

given clause #1246: (wt=13) 26864 [para_into,26808,14564] x^ (y^ (z v (x v u)))=y^x.

given clause #1247: (wt=13) 26982 [para_from,26808,21468,demod,21594,flip.1] (x^ (y v z)) v c(y)=x v c(y).

given clause #1248: (wt=13) 26984 [para_from,26808,20814,demod,19256,flip.1] c(x) v (y^ (x v z))=c(x) v y.

given clause #1249: (wt=19) 14911 [para_into,14879,98] x v (y v (((y v (x v z))^u) v z))=y v (x v z).

given clause #1250: (wt=13) 27140 [para_from,26851,21468,demod,21594,flip.1] (x^ (y v z)) v c(z)=x v c(z).

given clause #1251: (wt=13) 27142 [para_from,26851,20814,demod,19256,flip.1] c(x) v (y^ (z v x))=c(x) v y.

given clause #1252: (wt=13) 27213 [para_into,26869,14596] x^ ((y v (z v x))^u)=x^u.

given clause #1253: (wt=19) 14913 [para_into,14879,15] x v (y v (((x v (y v z))^u) v z))=x v (y v z).

given clause #1254: (wt=13) 27217 [para_into,26869,14564] x^ ((y v (x v z))^u)=x^u.

given clause #1255: (wt=13) 27308 [para_from,26869,21468,demod,21469,flip.1] ((x v y)^z) v c(x)=z v c(x).

given clause #1256: (wt=13) 27310 [para_from,26869,20814,demod,20815,flip.1] c(x) v ((x v y)^z)=c(x) v z.

given clause #1257: (wt=19) 14915 [para_into,14879,14] x v (((y v (x v z))^u) v (y v z))=y v (x v z).

given clause #1258: (wt=13) 27776 [back_demod,23273,demod,27342] (x^y) v (y^ (x^z))=x^y.

given clause #1259: (wt=13) 27782 [back_demod,23265,demod,27342] x^ (y^ ((y^x) v z))=x^y.

given clause #1260: (wt=13) 27812 [back_demod,23025,demod,27342] (x^ (y^z)) v (y^x)=y^x.

given clause #1261: (wt=19) 14932 [para_from,14879,96,flip.1] (x^y) v (z v (u v (v v x)))=z v (u v (v v x)).

given clause #1262: (wt=13) 27957 [back_demod,25322,demod,27574] (x^y) v (x^ (z^y))=x^y.

given clause #1263: (wt=13) 27959 [back_demod,25320,demod,27574] (x^y) v (y^ (z^x))=x^y.

given clause #1264: (wt=13) 28021 [para_from,27026,21468,demod,21469,flip.1] ((x v y)^z) v c(y)=z v c(y).

given clause #1265: (wt=17) 14934 [para_from,14879,98] x v (y v z)=y v (((y v z)^u) v (x v z)).

given clause #1266: (wt=13) 28023 [para_from,27026,20814,demod,20815,flip.1] c(x) v ((y v x)^z)=c(x) v z.

given clause #1267: (wt=13) 28127 [para_into,27341,17772,flip.1] x^ (y^ ((x^y) v z))=x^y.

given clause #1268: (wt=13) 28199 [para_from,27341,14879] (x^ (y^z)) v (x^y)=x^y.

given clause #1269: (wt=17) 14935 [para_from,14879,15] x v (y v z)= ((y v z)^u) v (y v (x v z)).

given clause #1270: (wt=13) 28201 [para_from,27341,14867] (x^y) v (x^ (y^z))=x^y.

given clause #1271: (wt=13) 28348 [para_from,27345,14600] (x^ (y^z)) v (x^z)=x^z.

given clause #1272: (wt=13) 28468 [para_from,27448,14600] (x^ (y^z)) v (z^x)=z^x.

given clause #1273: (wt=15) 14941 [para_from,14879,14,flip.1] (x^y) v (z v (u v x))=z v (u v x).

given clause #1274: (wt=13) 30647 [para_from,14829,14293,demod,18416,26983,23304,flip.1] (x^ (y v z)) v z= (x^y) v z.

----> UNIT CONFLICT at  20.66 sec ----> 33674 [binary,33672,13] $Ans(DIST1).

Length of proof is 449.  Level of proof is 76.

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

2 [] x v (y v z)=y v (x v z).
3 [] x^y=c(c(x) v c(y)).
4 [copy,3,flip.1] c(c(x) v c(y))=x^y.
7 [] (x v c(y))^ (x v y)=x.
10,9 [] x v c(x)=1.
12,11 [] c(1)=0.
13 [] A^ (B v C)!= (A^B) v (A^C)|$Ans(DIST1).
14 [para_into,2,2] x v (y v (z v u))=z v (x v (y v u)).
15 [copy,14,flip.1] x v (y v (z v u))=y v (z v (x v u)).
17,16 [para_into,9,11] 1 v 0=1.
18 [para_from,9,2,flip.1] x v (y v c(x))=y v 1.
20 [para_from,16,2] x v 1=1 v (x v 0).
21 [copy,20,flip.1] 1 v (x v 0)=x v 1.
22 [para_into,4,11] c(0 v c(x))=1^x.
24 [para_into,4,4] c((x^y) v c(z))= (c(x) v c(y))^z.
27,26 [para_into,4,11] c(c(x) v 0)=x^1.
29,28 [para_into,4,4] c(c(x) v (y^z))=x^ (c(y) v c(z)).
30 [para_into,4,9,demod,12,flip.1] x^c(x)=0.
32 [para_from,4,9] (c(x) v c(y)) v (x^y)=1.
34 [para_into,30,11] 1^0=0.
36 [para_into,30,4] (c(x) v c(y))^ (x^y)=0.
38 [para_from,20,2] x v (1 v (y v 0))=y v (x v 1).
39 [copy,38,flip.1] x v (y v 1)=y v (1 v (x v 0)).
41,40 [para_into,7,11] (x v 0)^ (x v 1)=x.
42 [para_into,7,4] (x v (y^z))^ (x v (c(y) v c(z)))=x.
45,44 [para_into,7,9] 1^ (x v x)=x.
46 [para_into,7,20,demod,12] (x v 0)^ (1 v (x v 0))=x.
48 [para_into,7,16] (1 v c(0))^1=1.
50 [para_into,7,9] (x v c(c(x)))^1=x.
52 [para_into,7,2] (x v c(y v z))^ (y v (x v z))=x.
55,54 [para_into,44,2] 1^ (x v ((x v y) v y))=x v y.
58 [para_from,21,2] x v (y v 1)=1 v (x v (y v 0)).
59 [copy,58,flip.1] 1 v (x v (y v 0))=x v (y v 1).
63,62 [para_into,22,11] c(0 v 0)=1^1.
64 [para_into,22,4] c(0 v (x^y))=1^ (c(x) v c(y)).
66 [para_from,22,7] (x v (1^y))^ (x v (0 v c(y)))=x.
70 [para_from,22,9] (0 v c(x)) v (1^x)=1.
72 [para_from,62,7] (x v (1^1))^ (x v (0 v 0))=x.
85,84 [para_into,26,4] c((x^y) v 0)= (c(x) v c(y))^1.
90 [para_from,26,9] (c(x) v 0) v (x^1)=1.
94 [para_into,14,9,flip.1] x v (y v (z v c(x)))=y v (z v 1).
98 [para_into,14,2] x v (y v (z v u))=z v (y v (x v u)).
105 [para_from,14,7] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x.
127 [para_from,15,44] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z).
130 [para_from,15,7] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x.
137 [para_into,18,26] (c(x) v 0) v (y v (x^1))=y v 1.
141 [para_into,18,4] (c(x) v c(y)) v (z v (x^y))=z v 1.
161,160 [para_into,24,40] c(x v c(y))= (c(x v 0) v c(x v 1))^y.
163,162 [para_into,24,34,demod,161,63,12,10] ((1^1) v c(0 v 1))^x=1^x.
174 [para_into,70,62,demod,45] (0 v (1^1)) v 0=1.
178 [para_into,70,44] (0 v c(x v x)) v x=1.
182 [para_from,174,40] 1^ ((0 v (1^1)) v 1)=0 v (1^1).
185,184 [para_from,174,21,flip.1] (0 v (1^1)) v 1=1 v 1.
191 [back_demod,182,demod,185,45,flip.1] 0 v (1^1)=1.
196,195 [para_into,28,26] c((x^1) v (y^z))= (c(x) v 0)^ (c(y) v c(z)).
197 [para_into,28,48,demod,161,17,12,12] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0).
199 [para_into,28,44,demod,12] c(c(x) v y)=x^ (0 v c(y v y)).
200 [para_into,28,40] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)).
201 [copy,199,flip.1] x^ (0 v c(y v y))=c(c(x) v y).
202 [copy,200,flip.1] x^ (c(y v 0) v c(y v 1))=c(c(x) v y).
205 [para_from,28,9] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1.
210 [para_from,191,7] (0 v c(1^1))^1=0.
212 [para_from,191,2,flip.1] 0 v (x v (1^1))=x v 1.
226 [para_into,90,50,demod,161] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1.
234 [para_into,32,26] ((x^1) v c(y)) v ((c(x) v 0)^y)=1.
240 [para_into,32,40] (c(x v 0) v c(x v 1)) v x=1.
250 [para_into,178,2] x v ((0 v c((x v y) v (x v y))) v y)=1.
255 [para_from,178,14] x v (y v 1)= (0 v c(z v z)) v (x v (y v z)).
258 [para_from,178,2] x v 1= (0 v c(y v y)) v (x v y).
260 [copy,255,flip.1] (0 v c(x v x)) v (y v (z v x))=y v (z v 1).
263,262 [para_from,210,90,demod,161,63,163] ((1^ (1^1)) v 0) v 0=1.
278 [para_from,46,28] c(c(x) v y)=x^ (c(y v 0) v c(1 v (y v 0))).
287,286 [para_into,212,90,demod,12,flip.1] (0 v 0) v 1=0 v 1.
306 [para_from,38,7] (x v c(1 v (y v 0)))^ (y v (x v 1))=x.
312,311 [para_from,262,46,demod,263,45,flip.1] (1^ (1^1)) v 0=1.
314 [para_from,311,46,demod,312,45,flip.1] 1^ (1^1)=1.
322 [para_into,39,2] x v (y v 1)=x v (1 v (y v 0)).
325 [copy,322,flip.1] x v (1 v (y v 0))=x v (y v 1).
334 [para_from,39,7] (x v c(y v 1))^ (y v (1 v (x v 0)))=x.
376 [para_into,42,44,demod,12] (x v y)^ (x v (0 v c(y v y)))=x.
380 [para_into,42,191,demod,12,12] 1^ (0 v (0 v 0))=0.
388 [para_into,42,26] (x v (y^ (c(z) v 0)))^ (x v (c(y) v (z^1)))=x.
390 [para_into,42,18] (x v (y^x))^ (c(y) v 1)=x.
392 [para_into,42,2] (x v (y^z))^ (c(y) v (x v c(z)))=x.
399,398 [para_from,380,70] (0 v c(0 v (0 v 0))) v 0=1.
422 [para_into,52,62] (x v (1^1))^ (0 v (x v 0))=x.
424 [para_into,52,26] (x v (y^1))^ (c(y) v (x v 0))=x.
440 [para_into,52,178] (x v c((0 v c((x v y) v (x v y))) v y))^1=x.
444 [para_into,52,38] (1 v c(x v (y v 0)))^ (y v (x v 1))=1.
448 [para_into,52,14] (x v c(y v (z v u)))^ (z v (y v (x v u)))=x.
466 [para_into,390,44,demod,12] ((x v x) v x)^ (0 v 1)=x v x.
500 [para_into,54,14] 1^ (x v (y v ((y v (x v z)) v z)))=y v (x v z).
505 [para_from,398,46,demod,399,45,flip.1] 0 v c(0 v (0 v 0))=1.
520 [para_from,505,2,flip.1] 0 v (x v c(0 v (0 v 0)))=x v 1.
561,560 [para_into,59,178,flip.1] (0 v c((x v 0) v (x v 0))) v (x v 1)=1 v 1.
580 [para_into,64,46,flip.1] 1^ (c(x v 0) v c(1 v (x v 0)))=c(0 v x).
582 [para_into,64,44,demod,12] c(0 v x)=1^ (0 v c(x v x)).
584 [copy,582,flip.1] 1^ (0 v c(x v x))=c(0 v x).
618 [para_into,66,2] (x v (1^y))^ (0 v (x v c(y)))=x.
631,630 [para_into,240,62] ((1^1) v c(0 v 1)) v 0=1.
643 [para_from,240,46,demod,63,631,45,63,flip.1] (1^1) v c(0 v 1)=1.
658 [para_into,84,44,demod,12] c(x v 0)= (0 v c(x v x))^1.
662 [copy,658,flip.1] (0 v c(x v x))^1=c(x v 0).
665 [para_from,84,52] (x v ((c(y) v c(z))^1))^ ((y^z) v (x v 0))=x.
669 [para_from,84,30] ((x^y) v 0)^ ((c(x) v c(y))^1)=0.
683 [para_into,643,20] (1^1) v c(1 v (0 v 0))=1.
685 [para_from,643,52] 1^ (0 v ((1^1) v 1))=1^1.
688,687 [para_from,643,18,flip.1] (1^1) v 1= (0 v 1) v 1.
703,702 [back_demod,685,demod,688,55,flip.1] 1^1=0 v 1.
710 [back_demod,683,demod,703] (0 v 1) v c(1 v (0 v 0))=1.
732 [back_demod,422,demod,703] (x v (0 v 1))^ (0 v (x v 0))=x.
755,754 [back_demod,314,demod,703] 1^ (0 v 1)=1.
772 [back_demod,212,demod,703] 0 v (x v (0 v 1))=x v 1.
778 [back_demod,191,demod,703] 0 v (0 v 1)=1.
788 [back_demod,72,demod,703] (x v (0 v 1))^ (x v (0 v 0))=x.
791,790 [back_demod,62,demod,703] c(0 v 0)=0 v 1.
792 [para_from,702,390,demod,12] (1 v (0 v 1))^ (0 v 1)=1.
794 [para_from,702,28,demod,12,12] c(c(x) v (0 v 1))=x^ (0 v 0).
806 [para_into,778,20] 0 v (1 v (0 v 0))=1.
811,810 [para_from,778,15,flip.1] 0 v (0 v (x v 1))=x v 1.
814 [para_from,790,28] c((0 v 1) v (x^y))= (0 v 0)^ (c(x) v c(y)).
840 [para_from,806,15,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1.
860 [para_into,772,39] 0 v (0 v (1 v (x v 0)))=x v 1.
862 [copy,860,flip.1] x v 1=0 v (0 v (1 v (x v 0))).
866,865 [para_into,792,39,demod,17] (0 v (1 v 1))^ (0 v 1)=1.
925,924 [para_from,710,18] (1 v (0 v 0)) v 1= (0 v 1) v 1.
1073,1072 [para_into,582,2,flip.1] 1^ (0 v c((x v y) v (x v y)))=c(x v (0 v y)).
1187 [para_into,732,2] (0 v (x v 1))^ (0 v (x v 0))=x.
1211 [para_into,105,18] (x v c(y v (z v c(x))))^ (z v (y v 1))=x.
1229 [para_into,788,2] (0 v (x v 1))^ (x v (0 v 0))=x.
1232,1231 [para_into,788,178,demod,561,flip.1] 0 v c((0 v 0) v (0 v 0))= (1 v 1)^1.
1294,1293 [para_into,840,240,demod,287,flip.1] (c((0 v 0) v 0) v c(0 v 1)) v 1=0 v (1 v 1).
1296,1295 [para_into,840,178,demod,1232,flip.1] ((1 v 1)^1) v 1=0 v (1 v 1).
1318 [para_from,860,582,demod,1073] c(x v 1)=c(0 v (0 v (1 v (x v 0)))).
1325,1324 [para_into,862,20,flip.1] 0 v (0 v (1 v (x v 0)))=1 v (x v 0).
1327 [back_demod,1318,demod,1325] c(x v 1)=c(1 v (x v 0)).
1440 [para_into,1229,240,demod,287,1294,811,287,flip.1] c((0 v 0) v 0) v c(0 v 1)= (1 v 1)^1.
1589,1588 [para_into,199,20] c(1 v (c(x) v 0))=x^ (0 v c(1 v 1)).
1624 [para_into,201,7,demod,161,791,10,flip.1] c((1^c(x v x)) v x)=0.
1683 [para_from,1624,9] ((1^c(x v x)) v x) v 0=1.
1704,1703 [para_from,1683,325,flip.1] x v (((1^c(y v y)) v y) v 1)=x v (1 v 1).
1705 [para_from,1683,1187,demod,1704,866,flip.1] (1^c(x v x)) v x=1.
1755 [para_from,1705,2] x v 1= (1^c(y v y)) v (x v y).
1762 [copy,1755,flip.1] (1^c(x v x)) v (y v x)=y v 1.
1867 [para_into,376,2] (x v y)^ (0 v (x v c(y v y)))=x.
1877 [para_into,424,26] (x v ((c(y) v 0)^1))^ ((y^1) v (x v 0))=x.
1911 [para_from,520,94] (0 v (0 v 0)) v (x v 1)=0 v (x v 1).
2367 [para_into,205,11] (c(x) v (1^y)) v (x^ (0 v c(y)))=1.
2369 [para_into,205,44,demod,12] (0 v (x^x)) v c(x)=1.
2378,2377 [para_from,2369,18,flip.1] (0 v (x^x)) v 1=x v 1.
2396 [para_from,2369,2,flip.1] (0 v (x^x)) v (y v c(x))=y v 1.
2403,2402 [para_into,2377,20] 1 v ((0 v (x^x)) v 0)=x v 1.
2462,2461 [para_from,226,325,demod,791,10,flip.1] x v (((1^c(0)) v 0) v 1)=x v (1 v 1).
2463 [para_from,226,1187,demod,791,10,2462,866,791,10,flip.1] (1^c(0)) v 0=1.
2468,2467 [para_from,2463,1762,demod,791,755,flip.1] (1^c(0)) v 1=1 v 1.
2479 [para_from,2463,1187,demod,2468,866,flip.1] 1^c(0)=1.
2484,2483 [para_from,2479,390,demod,12] (c(0) v 1)^ (0 v 1)=c(0).
2485 [para_from,2479,618] (x v 1)^ (0 v (x v c(c(0))))=x.
2532 [para_into,2483,20] (1 v (c(0) v 0))^ (0 v 1)=c(0).
2564 [para_into,2485,2369,demod,2378,2484,flip.1] 0 v (c(0)^c(0))=c(0).
2583 [para_from,2564,7] (0 v c(c(0)^c(0)))^c(0)=0.
2605 [para_from,2532,84,demod,27,1589,flip.1] ((0^ (0 v c(1 v 1))) v c(0 v 1))^1=0^1.
2613 [para_from,2532,32,demod,1589] ((0^ (0 v c(1 v 1))) v c(0 v 1)) v c(0)=1.
3123 [para_into,392,26] (x v ((c(y) v 0)^z))^ ((y^1) v (x v c(z)))=x.
3344 [para_into,334,2369,demod,2403,55,flip.1] 0 v ((x v 1)^ (x v 1))=x v 1.
3353,3352 [para_from,3344,141] (c(x v 1) v c(x v 1)) v (x v 1)=0 v 1.
3541 [para_into,1911,1295,demod,1296,811] (0 v (0 v 0)) v (0 v (1 v 1))=1 v 1.
3895 [para_into,2367,7,demod,161,791,10] ((1^c(x)) v (1^x)) v 0=1.
3924,3923 [para_from,3895,1762,demod,791,755,flip.1] ((1^c(x)) v (1^x)) v 1=1 v 1.
3928 [para_from,3895,1187,demod,3924,866,flip.1] (1^c(x)) v (1^x)=1.
3964 [para_into,3928,584,demod,161,791,10,45] (1^x) v c(0 v x)=1.
4033 [para_into,3964,44] x v c(0 v (x v x))=1.
4112,4111 [para_from,3964,2396,demod,2378,flip.1] (1^x) v 1= (0 v x) v 1.
4204 [para_into,4033,2] x v c(x v (0 v x))=1.
4218,4217 [para_from,4033,130] 1^ (0 v (x v (x v x)))=x.
4219 [para_from,4033,105] 1^ (x v (x v (0 v x)))=x.
4228 [para_from,4033,2396,demod,2378] (0 v (x v x)) v 1=x v 1.
4300,4299 [para_from,4204,2396,demod,2378] (x v (0 v x)) v 1=x v 1.
4437,4436 [para_into,4217,94] 1^ (c(0) v (c(0) v 1))=c(0).
4474 [para_into,4219,806,demod,925] 1^ ((1 v (0 v 0)) v ((0 v 1) v 1))=1 v (0 v 0).
4554 [para_into,4228,18] (c(0) v 1) v 1=c(0) v 1.
4567,4566 [para_from,4228,127,demod,4218,flip.1] 0 v (1 v 1)=1.
4590,4589 [back_demod,3541,demod,4567,4300,flip.1] 1 v 1=0 v 1.
4878 [back_demod,2613,demod,4590] ((0^ (0 v c(0 v 1))) v c(0 v 1)) v c(0)=1.
4884 [back_demod,2605,demod,4590] ((0^ (0 v c(0 v 1))) v c(0 v 1))^1=0^1.
4945,4944 [back_demod,1588,demod,4590] c(1 v (c(x) v 0))=x^ (0 v c(0 v 1)).
4948 [back_demod,1440,demod,4590] c((0 v 0) v 0) v c(0 v 1)= (0 v 1)^1.
4976 [back_demod,197,demod,4590] c(c(x) v 1)=x^ (((0 v c(0 v 1))^0) v 0).
4982 [para_into,4589,258] (0 v c(x v x)) v (1 v x)=0 v 1.
5310,5309 [para_from,4554,54,demod,4437,flip.1] c(0) v 1=c(0).
5347 [para_from,4554,1327,demod,5310,5310,4945] c(c(0))=0^ (0 v c(0 v 1)).
5358,5357 [para_from,4554,810,demod,5310,10,5310,5310,flip.1] c(0)=0 v 1.
5406,5405 [back_demod,5347,demod,5358,flip.1] 0^ (0 v c(0 v 1))=c(0 v 1).
5424,5423 [back_demod,4878,demod,5406,5358,3353] 0 v 1=1.
5440,5439 [back_demod,2583,demod,5358,5424,5358,5424,703,5424,12,5358,5424] (0 v 0)^1=0.
5448 [back_demod,4884,demod,5424,12,5424,12] ((0^ (0 v 0)) v 0)^1=0^1.
5456,5455 [back_demod,4474,demod,5424,4590,5424,925,5424,4590,5424,703,5424,flip.1] 1 v (0 v 0)=1.
5466,5465 [back_demod,5405,demod,5424,12,5424,12] 0^ (0 v 0)=0.
5476,5475 [back_demod,5357,demod,5424] c(0)=1.
5499 [back_demod,4982,demod,5424] (0 v c(x v x)) v (1 v x)=1.
5504,5503 [back_demod,4976,demod,5424,12] c(c(x) v 1)=x^ (((0 v 0)^0) v 0).
5531 [back_demod,4948,demod,5424,12,5424,703,5424] c((0 v 0) v 0) v 0=1.
5535 [back_demod,4944,demod,5424,12] c(1 v (c(x) v 0))=x^ (0 v 0).
5652,5651 [back_demod,4589,demod,5424] 1 v 1=1.
5838,5837 [back_demod,814,demod,5424] c(1 v (x^y))= (0 v 0)^ (c(x) v c(y)).
5840,5839 [back_demod,794,demod,5424,5504] x^ (((0 v 0)^0) v 0)=x^ (0 v 0).
5842,5841 [back_demod,790,demod,5424] c(0 v 0)=1.
5862,5861 [back_demod,702,demod,5424] 1^1=1.
5874,5873 [back_demod,466,demod,5424] ((x v x) v x)^1=x v x.
5913,5912 [back_demod,5448,demod,5466,5440,flip.1] 0^1=0.
5948 [back_demod,5503,demod,5840] c(c(x) v 1)=x^ (0 v 0).
5966 [para_from,5475,390,demo