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

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 v (B^ (A v C))!=A v (C^ (A v B))|$Ans(MOD).
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=15): 14 [copy,13,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD).
  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) 17 [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) 31 [para_into,4,9,demod,12,flip.1] x^c(x)=0.

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

given clause #8: (wt=9) 21 [para_from,17,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) 45 [para_into,7,9] 1^ (x v x)=x.

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

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

given clause #13: (wt=15) 14 [copy,13,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD).

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

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

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

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

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

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

given clause #20: (wt=9) 75 [para_from,63,31] (0 v 0)^ (1^1)=0.

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

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

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

given clause #24: (wt=10) 69 [para_from,23,31] (0 v c(x))^ (1^x)=0.

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

given clause #26: (wt=9) 148 [para_into,69,63,demod,46] (0 v (1^1))^0=0.

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

given clause #28: (wt=9) 175 [para_into,71,63,demod,46] (0 v (1^1)) v 0=1.

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

given clause #30: (wt=7) 192 [back_demod,183,demod,186,46,flip.1] 0 v (1^1)=1.

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

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

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

given clause #34: (wt=10) 156 [para_into,69,45] (0 v c(x v x))^x=0.

given clause #35: (wt=10) 179 [para_into,71,45] (0 v c(x v x)) v x=1.

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

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

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

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

given clause #40: (wt=9) 287 [para_into,213,91,demod,12,flip.1] (0 v 0) v 1=0 v 1.

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

given clause #42: (wt=11) 263 [para_from,211,91,demod,162,64,164] ((1^ (1^1)) v 0) v 0=1.

given clause #43: (wt=9) 312 [para_from,263,47,demod,264,46,flip.1] (1^ (1^1)) v 0=1.

given clause #44: (wt=7) 315 [para_from,312,47,demod,313,46,flip.1] 1^ (1^1)=1.

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

given clause #46: (wt=10) 317 [para_from,315,71] (0 v c(1^1)) v 1=1.

given clause #47: (wt=11) 293 [para_into,287,21] 1 v ((0 v 0) v 0)=0 v 1.

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

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

given clause #50: (wt=9) 381 [para_into,43,192,demod,12,12] 1^ (0 v (0 v 0))=0.

given clause #51: (wt=11) 359 [para_into,57,63] (1 v (1^1))^ (0 v 1)=1.

given clause #52: (wt=12) 249 [para_into,179,21] 1 v ((0 v c(1 v 1)) v 0)=1.

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

given clause #54: (wt=12) 339 [para_into,317,21] 1 v ((0 v c(1^1)) v 0)=1.

given clause #55: (wt=12) 391 [para_into,43,19] (x v (y^x))^ (c(y) v 1)=x.

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

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

given clause #58: (wt=12) 399 [para_from,381,71] (0 v c(0 v (0 v 0))) v 0=1.

given clause #59: (wt=10) 506 [para_from,399,47,demod,400,46,flip.1] 0 v c(0 v (0 v 0))=1.

given clause #60: (wt=11) 508 [para_from,506,53] 1^ (0 v (0 v (0 v 0)))=0.

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

given clause #62: (wt=11) 510 [para_from,506,19] (0 v (0 v 0)) v 1=0 v 1.

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

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

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

given clause #66: (wt=13) 120 [para_into,16,22] x v (y v 1)=1 v (y v (x v 0)).

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

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

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

given clause #70: (wt=13) 215 [para_into,89,63] ((1^1) v 0)^ ((0 v 0)^1)=0.

given clause #71: (wt=13) 223 [para_into,91,63] ((1^1) v 0) v ((0 v 0)^1)=1.

given clause #72: (wt=13) 241 [para_into,33,41] (c(x v 0) v c(x v 1)) v x=1.

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

given clause #74: (wt=10) 644 [para_from,241,47,demod,64,632,46,64,flip.1] (1^1) v c(0 v 1)=1.

given clause #75: (wt=7) 703 [back_demod,686,demod,689,56,flip.1] 1^1=0 v 1.

given clause #76: (wt=7) 755 [back_demod,315,demod,704] 1^ (0 v 1)=1.

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

given clause #78: (wt=7) 779 [back_demod,192,demod,704] 0 v (0 v 1)=1.

given clause #79: (wt=8) 791 [back_demod,63,demod,704] c(0 v 0)=0 v 1.

given clause #80: (wt=9) 787 [back_demod,77,demod,704] (0 v 0) v (0 v 1)=1.

given clause #81: (wt=17) 93 [para_into,15,22] x v (y v (z v 1))=1 v (x v (y v (z v 0))).

given clause #82: (wt=9) 799 [para_into,755,21] 1^ (1 v (0 v 0))=1.

given clause #83: (wt=9) 807 [para_into,779,21] 0 v (1 v (0 v 0))=1.

given clause #84: (wt=9) 809 [para_into,779,120] 1 v (0 v (0 v 0))=1.

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

given clause #86: (wt=10) 753 [back_demod,317,demod,704] (0 v c(0 v 1)) v 1=1.

given clause #87: (wt=10) 775 [back_demod,211,demod,704] (0 v c(0 v 1))^1=0.

given clause #88: (wt=11) 773 [back_demod,213,demod,704] 0 v (x v (0 v 1))=x v 1.

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

given clause #90: (wt=11) 793 [para_from,703,391,demod,12] (1 v (0 v 1))^ (0 v 1)=1.

given clause #91: (wt=11) 811 [para_from,779,16,flip.1] 0 v (0 v (x v 1))=x v 1.

given clause #92: (wt=11) 817 [para_into,787,21] (0 v 0) v (1 v (0 v 0))=1.

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

given clause #94: (wt=11) 819 [para_into,787,59] 1 v ((0 v 0) v (0 v 0))=1.

given clause #95: (wt=11) 866 [para_into,793,40,demod,18] (0 v (1 v 1))^ (0 v 1)=1.

given clause #96: (wt=12) 711 [back_demod,684,demod,704] (0 v 1) v c(1 v (0 v 0))=1.

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

given clause #98: (wt=12) 751 [back_demod,339,demod,704] 1 v ((0 v c(0 v 1)) v 0)=1.

given clause #99: (wt=12) 797 [para_from,703,85,demod,12,12] c((0 v 1) v 0)= (0 v 0)^1.

given clause #100: (wt=12) 833 [para_from,799,71] (0 v c(1 v (0 v 0))) v 1=1.

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

given clause #102: (wt=12) 835 [para_from,799,69] (0 v c(1 v (0 v 0)))^1=0.

given clause #103: (wt=12) 839 [para_from,807,53] (1 v c(0 v (0 v 0)))^1=1.

given clause #104: (wt=13) 277 [para_into,37,41] (c(x v 0) v c(x v 1))^x=0.

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

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

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

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

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

given clause #110: (wt=13) 467 [para_into,391,45,demod,12] ((x v x) v x)^ (0 v 1)=x v x.

given clause #111: (wt=13) 479 [para_into,475,21] (x v (1^x))^ (1 v (0 v 0))=x.

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

given clause #113: (wt=19) 102 [copy,97,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) 543 [para_into,510,21] 1 v ((0 v (0 v 0)) v 0)=0 v 1.

given clause #115: (wt=13) 583 [para_into,65,45,demod,12] c(0 v x)=1^ (0 v c(x v x)).

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

given clause #117: (wt=19) 103 [copy,98,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) 659 [para_into,85,45,demod,12] c(x v 0)= (0 v c(x v x))^1.

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

given clause #120: (wt=13) 709 [back_demod,463,demod,704,704] ((0 v 1) v 1)^ (0 v 1)=0 v 1.

given clause #121: (wt=19) 104 [para_from,15,45] 1^ (x v ((y v (x v z)) v (y v z)))=y v (x v z).

given clause #122: (wt=13) 717 [back_demod,575,demod,704] 1^ (0 v c(0 v 1))=c(0 v 1).

given clause #123: (wt=13) 733 [back_demod,423,demod,704] (x v (0 v 1))^ (0 v (x v 0))=x.

given clause #124: (wt=13) 769 [back_demod,223,demod,704] ((0 v 1) v 0) v ((0 v 0)^1)=1.

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

given clause #126: (wt=13) 771 [back_demod,215,demod,704] ((0 v 1) v 0)^ ((0 v 0)^1)=0.

given clause #127: (wt=13) 781 [back_demod,136,demod,704] (0 v 0) v (x v (0 v 1))=x v 1.

given clause #128: (wt=13) 789 [back_demod,73,demod,704] (x v (0 v 1))^ (x v (0 v 0))=x.

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

given clause #130: (wt=13) 795 [para_from,703,29,demod,12,12] c(c(x) v (0 v 1))=x^ (0 v 0).

given clause #131: (wt=13) 821 [para_from,787,16,flip.1] (0 v 0) v (0 v (x v 1))=x v 1.

given clause #132: (wt=13) 825 [para_into,93,779,flip.1] 1 v (x v (0 v (0 v 0)))=x v 1.

given clause #133: (wt=19) 109 [copy,108,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) 841 [para_from,807,16,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1.

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

given clause #136: (wt=13) 852 [para_from,809,16,flip.1] 1 v (0 v (x v (0 v 0)))=x v 1.

given clause #137: (wt=16) 112 [para_into,51,27] ((c(x) v 0) v c(x^1))^1=c(x) v 0.

given clause #138: (wt=13) 860 [para_into,773,120] 0 v (1 v (0 v (x v 0)))=x v 1.

given clause #139: (wt=13) 861 [para_into,773,40] 0 v (0 v (1 v (x v 0)))=x v 1.

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

given clause #141: (wt=16) 114 [para_into,51,23] ((0 v c(x)) v c(1^x))^1=0 v c(x).

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

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

given clause #144: (wt=11) 1328 [back_demod,1319,demod,1326] c(x v 1)=c(1 v (x v 0)).

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

given clause #146: (wt=12) 1338 [para_from,1327,31] (1 v (x v 0))^c(x v 1)=0.

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

given clause #148: (wt=12) 1367 [para_from,1328,31] (x v 1)^c(1 v (x v 0))=0.

given clause #149: (wt=17) 118 [para_into,16,22] x v (y v (z v 1))=y v (1 v (x v (z v 0))).

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

given clause #151: (wt=13) 864 [para_into,793,21] (1 v (1 v (0 v 0)))^ (0 v 1)=1.

given clause #152: (wt=13) 878 [para_into,811,93] 1 v (0 v (0 v (x v 0)))=x v 1.

given clause #153: (wt=17) 119 [para_into,16,21] x v (y v (1 v (z v 0)))=y v (z v (x v 1)).

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

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

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

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

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

given clause #159: (wt=13) 1296 [para_into,841,179,demod,1233,flip.1] ((1 v 1)^1) v 1=0 v (1 v 1).

given clause #160: (wt=13) 1344 [para_from,1327,27,demod,28] (x v 1)^1= (1 v (x v 0))^1.

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

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

given clause #163: (wt=13) 1398 [para_from,1351,19] (x v 1) v 1= (1 v (x v 0)) v 1.

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

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

given clause #166: (wt=14) 138 [para_into,19,27] (c(x) v 0) v (y v (x^1))=y v 1.

given clause #167: (wt=14) 140 [para_into,19,23] (0 v c(x)) v (y v (1^x))=y v 1.

given clause #168: (wt=14) 150 [para_into,69,27] (0 v (x^1))^ (1^ (c(x) v 0))=0.

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

given clause #170: (wt=14) 152 [para_into,69,23] (0 v (1^x))^ (1^ (0 v c(x)))=0.

given clause #171: (wt=14) 177 [para_into,71,27] (0 v (x^1)) v (1^ (c(x) v 0))=1.

given clause #172: (wt=14) 200 [para_into,29,45,demod,12] c(c(x) v y)=x^ (0 v c(y v y)).

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

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

given clause #175: (wt=11) 1625 [para_into,202,7,demod,162,792,10,flip.1] c((1^c(x v x)) v x)=0.

given clause #176: (wt=12) 1665 [para_from,1625,31] ((1^c(x v x)) v x)^0=0.

given clause #177: (wt=19) 127 [copy,121,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) 1684 [para_from,1625,9] ((1^c(x v x)) v x) v 0=1.

given clause #179: (wt=10) 1706 [para_from,1684,1188,demod,1705,867,flip.1] (1^c(x v x)) v x=1.

given clause #180: (wt=12) 1726 [para_into,1706,21] 1 v ((1^c(1 v 1)) v 0)=1.

given clause #181: (wt=19) 128 [para_from,16,45] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z).

given clause #182: (wt=14) 217 [para_into,89,27] ((x^1) v 0)^ ((c(x) v 0)^1)=0.

given clause #183: (wt=14) 221 [para_into,89,49,demod,162,18,12] (((0 v c(1 v 1))^0) v 0)^1=0.

given clause #184: (wt=14) 225 [para_into,91,27] ((x^1) v 0) v ((c(x) v 0)^1)=1.

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

given clause #186: (wt=14) 229 [para_into,91,49,demod,162,18,12] (((0 v c(1 v 1))^0) v 0) v 1=1.

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

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

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

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

given clause #191: (wt=14) 377 [para_into,43,45,demod,12] (x v y)^ (x v (0 v c(y v y)))=x.

given clause #192: (wt=14) 425 [para_into,53,27] (x v (y^1))^ (c(y) v (x v 0))=x.

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

given clause #194: (wt=14) 477 [para_into,391,21] (x v (y^x))^ (1 v (c(y) v 0))=x.

given clause #195: (wt=14) 493 [para_into,55,179,demod,180] 1^ ((0 v c(x v x)) v (1 v x))=1.

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

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

given clause #198: (wt=14) 523 [para_from,508,71] (0 v c(0 v (0 v (0 v 0)))) v 0=1.

given clause #199: (wt=12) 1920 [para_from,523,1188,demod,1919,867,flip.1] 0 v c(0 v (0 v (0 v 0)))=1.

given clause #200: (wt=13) 1922 [para_from,1920,131] 1^ (0 v (0 v (0 v (0 v 0))))=0.

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

given clause #202: (wt=10) 1952 [para_into,154,45] (0 v (x^x))^c(x)=0.

given clause #203: (wt=13) 1925 [para_from,1920,19] (0 v (0 v (0 v 0))) v 1=0 v 1.

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

given clause #205: (wt=17) 161 [para_into,25,41] c(x v c(y))= (c(x v 0) v c(x v 1))^y.

given clause #206: (wt=14) 739 [back_demod,371,demod,704] (x v 1)^ (x v (0 v c(0 v 1)))=x.

given clause #207: (wt=14) 744 [back_demod,347,demod,704] (0 v c(0 v 1)) v (x v 1)=x v 1.

given clause #208: (wt=14) 757 [back_demod,291,demod,704] (0 v c(x v (0 v 1)))^ (x v 1)=0.

given clause #209: (wt=19) 167 [para_into,25,27] c((x^y) v (z^1))= (c(x) v c(y))^ (c(z) v 0).

given clause #210: (wt=14) 761 [back_demod,273,demod,704] (c(x) v (0 v 1))^ (x^ (0 v 0))=0.

given clause #211: (wt=14) 763 [back_demod,269,demod,704] ((0 v 1) v c(x))^ ((0 v 0)^x)=0.

given clause #212: (wt=14) 765 [back_demod,237,demod,704] (c(x) v (0 v 1)) v (x^ (0 v 0))=1.

given clause #213: (wt=19) 169 [para_into,25,23] c((x^y) v (1^z))= (c(x) v c(y))^ (0 v c(z)).

given clause #214: (wt=14) 767 [back_demod,233,demod,704] ((0 v 1) v c(x)) v ((0 v 0)^x)=1.

given clause #215: (wt=14) 785 [back_demod,110,demod,704] ((0 v 0) v c(0 v 1))^1=0 v 0.

given clause #216: (wt=14) 880 [para_from,811,53] (0 v c(0 v (x v 1)))^ (x v 1)=0.

given clause #217: (wt=19) 171 [back_demod,146,demod,162] (x v ((c(y v 0) v c(y v 1))^x))^ (y v 1)=x.

given clause #218: (wt=14) 890 [para_from,817,53] (1 v c((0 v 0) v (0 v 0)))^1=1.

given clause #219: (wt=14) 956 [para_into,797,21] c((1 v (0 v 0)) v 0)= (0 v 0)^1.

given clause #220: (wt=14) 1045 [para_from,517,391,demod,18,162,792,10] 1^ ((1^c(0 v (0 v 0))) v 1)=1.

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

given clause #222: (wt=14) 1049 [para_from,517,91,demod,162,792,10] ((1^c(0 v (0 v 0))) v 0) v 0=1.

given clause #223: (wt=12) 2128 [para_from,1049,55,demod,1046,flip.1] (1^c(0 v (0 v 0))) v 0=1.

given clause #224: (wt=10) 2136 [para_from,2128,1188,demod,2133,867,flip.1] 1^c(0 v (0 v 0))=1.

given clause #225: (wt=19) 196 [para_into,29,27] c((x^1) v (y^z))= (c(x) v 0)^ (c(y) v c(z)).

given clause #226: (wt=11) 2138 [para_into,2136,583,demod,1233] 1^ (1^ ((1 v 1)^1))=1.

given clause #227: (wt=13) 2148 [para_from,2136,71] (0 v c(c(0 v (0 v 0)))) v 1=1.

given clause #228: (wt=14) 1093 [back_demod,835,demod,1070] (0 v (1^ (0 v c(1 v 1))))^1=0.

given clause #229: (wt=18) 198 [para_into,29,49,demod,162,18,12,12] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0).

given clause #230: (wt=14) 1095 [back_demod,833,demod,1070] (0 v (1^ (0 v c(1 v 1)))) v 1=1.

given clause #231: (wt=14) 1111 [para_from,583,31] (0 v x)^ (1^ (0 v c(x v x)))=0.

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

given clause #233: (wt=17) 201 [para_into,29,41] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)).

given clause #234: (wt=14) 1152 [para_from,659,31] (x v 0)^ ((0 v c(x v x))^1)=0.

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

given clause #236: (wt=14) 1214 [para_into,106,817] (1 v c(0 v ((0 v 0) v 0)))^1=1.

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

given clause #238: (wt=14) 1457 [para_from,1248,31] (0 v (c(x) v 1))^ (x^ (0 v 0))=0.

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

given clause #240: (wt=14) 1752 [para_from,1706,55,demod,1707] 1^ ((1^c(x v x)) v (1 v x))=1.

given clause #241: (wt=16) 204 [para_from,29,31] (c(x) v (y^z))^ (x^ (c(y) v c(z)))=0.

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

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

given clause #244: (wt=14) 1806 [para_from,259,779] 0 v ((0 v c(x v x)) v (0 v x))=1.

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

given clause #246: (wt=10) 2370 [para_into,206,45,demod,12] (0 v (x^x)) v c(x)=1.

given clause #247: (wt=11) 2378 [para_from,2370,19,flip.1] (0 v (x^x)) v 1=x v 1.

given clause #248: (wt=13) 2403 [para_into,2378,21] 1 v ((0 v (x^x)) v 0)=x v 1.

given clause #249: (wt=18) 219 [para_into,89,51,demod,162] (((c(x v 0) v c(x v 1))^c(x)) v 0)^x=0.

given clause #250: (wt=10) 2433 [para_into,219,791,demod,10] ((1^c(0)) v 0)^0=0.

given clause #251: (wt=14) 1808 [para_from,259,755] 1^ ((0 v c(x v x)) v (0 v x))=1.

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

given clause #253: (wt=18) 227 [para_into,91,51,demod,162] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1.

given clause #254: (wt=8) 2464 [para_from,227,1188,demod,792,10,2463,867,792,10,flip.1] (1^c(0)) v 0=1.

given clause #255: (wt=6) 2480 [para_from,2464,1188,demod,2469,867,flip.1] 1^c(0)=1.

given clause #256: (wt=9) 2496 [para_from,2480,71] (0 v c(c(0))) v 1=1.

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

given clause #258: (wt=11) 2484 [para_from,2480,391,demod,12] (c(0) v 1)^ (0 v 1)=c(0).

given clause #259: (wt=11) 2502 [para_into,2496,21] 1 v ((0 v c(c(0))) v 0)=1.

given clause #260: (wt=13) 2482 [para_from,2480,477,demod,12] (c(0) v 1)^ (1 v (0 v 0))=c(0).

given clause #261: (wt=15) 235 [para_into,33,27] ((x^1) v c(y)) v ((c(x) v 0)^y)=1.

given clause #262: (wt=13) 2486 [para_from,2480,619] (x v 1)^ (0 v (x v c(c(0))))=x.

given clause #263: (wt=10) 2565 [para_into,2486,2370,demod,2379,2485,flip.1] 0 v (c(0)^c(0))=c(0).

given clause #264: (wt=13) 2488 [para_from,2480,67] (x v 1)^ (x v (0 v c(c(0))))=x.

given clause #265: (wt=15) 239 [para_into,33,27] (c(x) v (y^1)) v (x^ (c(y) v 0))=1.

given clause #266: (wt=13) 2492 [para_from,2480,140] (0 v c(c(0))) v (x v 1)=x v 1.

given clause #267: (wt=13) 2533 [para_into,2484,21] (1 v (c(0) v 0))^ (0 v 1)=c(0).

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

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

given clause #270: (wt=14) 1974 [para_into,619,755] (x v 1)^ (0 v (x v c(0 v 1)))=x.

given clause #271: (wt=13) 2638 [para_into,1974,2370,demod,2379,710,flip.1] 0 v ((0 v 1)^ (0 v 1))=0 v 1.

given clause #272: (wt=14) 1996 [para_into,757,795] (0 v (x^ (0 v 0)))^ (c(x) v 1)=0.

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

given clause #274: (wt=14) 2038 [para_into,761,277,demod,288,1442] (c((1 v 1)^1) v (0 v 1))^0=0.

given clause #275: (wt=14) 2056 [para_into,765,277,demod,288,1442] (c((1 v 1)^1) v (0 v 1)) v 0=1.

given clause #276: (wt=12) 2698 [para_from,2056,1188,demod,2259,2697,867,flip.1] c((1 v 1)^1) v (0 v 1)=1.

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

given clause #278: (wt=11) 2718 [para_from,2698,795,demod,12,flip.1] ((1 v 1)^1)^ (0 v 0)=0.

given clause #279: (wt=12) 2722 [para_from,2698,781,demod,288,flip.1] c((1 v 1)^1) v 1=0 v 1.

given clause #280: (wt=14) 2162 [para_from,2138,71] (0 v c(1^ ((1 v 1)^1))) v 1=1.

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

given clause #282: (wt=13) 2804 [para_into,251,1925,demod,1926,1237,2379,288] (0 v (0 v (0 v 0))) v (0 v 1)=1.

given clause #283: (wt=14) 2164 [para_from,2138,69] (0 v c(1^ ((1 v 1)^1)))^1=0.

given clause #284: (wt=14) 2306 [para_from,1756,779] 0 v ((1^c(x v x)) v (0 v x))=1.

given clause #285: (wt=17) 253 [para_from,179,41] ((0 v c(1 v 1)) v 0)^1=0 v c(1 v 1).

given clause #286: (wt=14) 2308 [para_from,1756,755] 1^ ((1^c(x v x)) v (0 v x))=1.

given clause #287: (wt=14) 2342 [para_into,1806,16] (0 v c(x v x)) v (0 v (0 v x))=1.

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

given clause #289: (wt=18) 255 [para_from,179,16] x v (y v 1)=y v ((0 v c(z v z)) v (x v z)).

given clause #290: (wt=14) 2523 [para_from,2496,57] (1 v c((0 v c(c(0))) v 0))^1=1.

given clause #291: (wt=14) 2573 [para_from,2565,142] (c(c(0)) v c(c(0))) v c(0)=0 v 1.

given clause #292: (wt=11) 2869 [para_from,2573,2397,demod,2864,780,flip.1] (c(c(0)) v c(c(0))) v 1=1.

given clause #293: (wt=18) 256 [para_from,179,15] x v (y v 1)= (0 v c(z v z)) v (x v (y v z)).

given clause #294: (wt=13) 2879 [para_into,2869,21] 1 v ((c(c(0)) v c(c(0))) v 0)=1.

given clause #295: (wt=14) 2575 [para_from,2565,43] c(0)^ (0 v (c(c(0)) v c(c(0))))=0.

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

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

given clause #298: (wt=14) 2708 [para_into,2698,21] c((1 v 1)^1) v (1 v (0 v 0))=1.

given clause #299: (wt=14) 2712 [para_into,2698,59] 1 v (c((1 v 1)^1) v (0 v 0))=1.

given clause #300: (wt=14) 2782 [para_into,2722,21] 1 v (c((1 v 1)^1) v 0)=0 v 1.

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

given clause #302: (wt=14) 2842 [para_into,2306,16] (1^c(x v x)) v (0 v (0 v x))=1.

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

given clause #304: (wt=15) 271 [para_into,37,27] ((x^1) v c(y))^ ((c(x) v 0)^y)=0.

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

given clause #306: (wt=15) 275 [para_into,37,27] (c(x) v (y^1))^ (x^ (c(y) v 0))=0.

given clause #307: (wt=15) 280 [para_from,47,37] (c(x v 0) v c(1 v (x v 0)))^x=0.

given clause #308: (wt=15) 282 [para_from,47,33] (c(x v 0) v c(1 v (x v 0))) v x=1.

given clause #309: (wt=19) 279 [para_from,47,29] c(c(x) v y)=x^ (c(y v 0) v c(1 v (y v 0))).

given clause #310: (wt=11) 2958 [para_into,282,293,demod,1442] ((1 v 1)^1) v (0 v 0)=1.

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

given clause #312: (wt=13) 2972 [para_from,2958,261,demod,792,780,flip.1] ((1 v 1)^1) v (0 v 1)=1 v 1.

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

given clause #314: (wt=14) 2985 [para_from,2958,53,demod,86,12] (0 v ((c(1 v 1) v 0)^1))^1=0.

given clause #315: (wt=15) 319 [para_into,40,287] x v (0 v 1)= (0 v 0) v (1 v (x v 0)).

given clause #316: (wt=15) 331 [para_from,40,45] 1^ (x v (1 v ((x v 1) v 0)))=x v 1.

given clause #317: (wt=17) 298 [para_from,287,15] x v (y v (0 v 1))= (0 v 0) v (x v (y v 1)).

given clause #318: (wt=15) 350 [para_from,293,16] x v (0 v 1)=1 v ((0 v 0) v (x v 0)).

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

given clause #320: (wt=15) 365 [para_into,57,179] (1 v c((0 v c(1 v 1)) v 0))^1=1.

given clause #321: (wt=17) 303 [para_from,39,45] 1^ (x v ((1 v (x v 0)) v 1))=1 v (x v 0).

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

given clause #323: (wt=15) 486 [para_from,475,37] (c(x v (1^x)) v c(0 v 1))^x=0.

given clause #324: (wt=15) 488 [para_from,475,33] (c(x v (1^x)) v c(0 v 1)) v x=1.

given clause #325: (wt=17) 305 [para_from,39,16] x v (y v (z v 1))=z v (1 v (x v (y v 0))).

given clause #326: (wt=15) 497 [para_into,55,40] 1^ ((x v 1) v (1 v (x v 0)))=x v 1.

given clause #327: (wt=15) 533 [para_from,59,55] 1^ (1 v (x v ((x v 1) v 0)))=x v 1.

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

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

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

given clause #331: (wt=15) 670 [para_from,85,31] ((x^y) v 0)^ ((c(x) v c(y))^1)=0.

given clause #332: (wt=12) 3180 [para_into,670,51] ((x^c(c(x))) v 0)^c(x)=0.

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

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

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

given clause #336: (wt=12) 3198 [para_into,682,51] ((x^c(c(x))) v 0) v c(x)=1.

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

given clause #338: (wt=13) 3205 [para_from,3198,2397,demod,2379,flip.1] ((x^c(c(x))) v 0) v 1=x v 1.

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

given clause #340: (wt=15) 707 [back_demod,471,demod,704] (x v ((0 v 0)^x))^ ((0 v 1) v 1)=x.

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

given clause #342: (wt=15) 741 [back_demod,363,demod,704] (1 v c((0 v c(0 v 1)) v 0))^1=1.

given clause #343: (wt=15) 777 [back_demod,209,demod,704] 0 v (x v (y v (0 v 1)))=x v (y v 1).

given clause #344: (wt=15) 823 [para_into,93,787,flip.1] 1 v (x v ((0 v 0) v (0 v 0)))=x v 1.

given clause #345: (wt=16) 320 [para_into,40,179] x v 1= (0 v c(1 v 1)) v (1 v (x v 0)).

given clause #346: (wt=15) 872 [para_from,793,85,demod,18,12,flip.1] (c(1 v (0 v 1)) v c(0 v 1))^1=0.

given clause #347: (wt=15) 876 [para_from,793,33] (c(1 v (0 v 1)) v c(0 v 1)) v 1=1.

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

given clause #349: (wt=18) 321 [para_into,40,179,flip.1] x v (1 v ((0 v c((x v 1) v (x v 1))) v 0))=1.

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

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

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

given clause #353: (wt=18) 327 [para_from,40,179] (0 v c(x v (1 v ((x v 1) v 0)))) v (x v 1)=1.

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

given clause #355: (wt=15) 918 [para_from,866,85,demod,18,12,flip.1] (c(0 v (1 v 1)) v c(0 v 1))^1=0.

given clause #356: (wt=15) 922 [para_from,866,33] (c(0 v (1 v 1)) v c(0 v 1)) v 1=1.

given clause #357: (wt=18) 329 [para_from,40,156] (0 v c(x v (1 v ((x v 1) v 0))))^ (x v 1)=0.

given clause #358: (wt=15) 1015 [para_into,299,120,flip.1] (0 v 0) v (x v 1)=1 v (0 v (x v 0)).

given clause #359: (wt=15) 1029 [para_into,467,21] (1 v ((1 v 1) v 0))^ (0 v 1)=1 v 1.

given clause #360: (wt=15) 1031 [para_into,467,21] ((x v x) v x)^ (1 v (0 v 0))=x v x.

given clause #361: (wt=17) 333 [para_from,40,16] x v (y v (1 v (z v 0)))=z v (y v (x v 1)).

given clause #362: (wt=15) 1058 [para_into,102,819] x v 1=1 v ((0 v 0) v (0 v (x v 0))).

given clause #363: (wt=15) 1059 [para_into,102,817] x v 1= (0 v 0) v (1 v (0 v (x v 0))).

given clause #364: (wt=15) 1069 [para_into,583,21] c(1 v (0 v 0))=1^ (0 v c(1 v 1)).

given clause #365: (wt=17) 334 [para_from,40,15] x v (y v (1 v (z v 0)))=y v (x v (z v 1)).

given clause #366: (wt=15) 1129 [para_into,103,819] x v 1=1 v (0 v ((0 v 0) v (x v 0))).

given clause #367: (wt=15) 1130 [para_into,103,817] x v 1= (0 v 0) v (0 v (1 v (x v 0))).

given clause #368: (wt=15) 1170 [para_into,709,21] (1 v ((0 v 1) v 0))^ (0 v 1)=0 v 1.

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

given clause #370: (wt=13) 3345 [para_into,335,2370,demod,2404,56,flip.1] 0 v ((x v 1)^ (x v 1))=x v 1.

given clause #371: (wt=15) 1180 [para_into,733,21] (x v (1 v (0 v 0)))^ (0 v (x v 0))=x.

given clause #372: (wt=15) 1182 [para_into,733,120] (1 v (0 v (x v 0)))^ (0 v (x v 0))=x.

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

given clause #374: (wt=15) 1184 [para_into,733,59] (1 v (x v (0 v 0)))^ (0 v (x v 0))=x.

given clause #375: (wt=15) 1186 [para_into,733,40] (0 v (1 v (x v 0)))^ (0 v (x v 0))=x.

given clause #376: (wt=15) 1194 [para_into,769,21] ((1 v (0 v 0)) v 0) v ((0 v 0)^1)=1.

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

given clause #378: (wt=15) 1216 [para_into,771,21] ((1 v (0 v 0)) v 0)^ ((0 v 0)^1)=0.

given clause #379: (wt=15) 1222 [para_into,789,21] (x v (1 v (0 v 0)))^ (x v (0 v 0))=x.

given clause #380: (wt=15) 1224 [para_into,789,120] (1 v (0 v (x v 0)))^ (x v (0 v 0))=x.

given clause #381: (wt=19) 352 [para_from,293,15,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) 1226 [para_into,789,59] (1 v (x v (0 v 0)))^ (x v (0 v 0))=x.

given clause #383: (wt=15) 1228 [para_into,789,40] (0 v (1 v (x v 0)))^ (x v (0 v 0))=x.

given clause #384: (wt=15) 1240 [para_into,795,21] c(c(x) v (1 v (0 v 0)))=x^ (0 v 0).

given clause #385: (wt=19) 367 [para_from,57,37,demod,162,18,12] (((0 v c(1 v 1))^ (x v 0)) v c(x v 1))^1=0.

given clause #386: (wt=15) 1242 [para_into,795,120] c(1 v (0 v (c(x) v 0)))=x^ (0 v 0).

given clause #387: (wt=15) 1244 [para_into,795,59] c(1 v (c(x) v (0 v 0)))=x^ (0 v 0).

given clause #388: (wt=15) 1246 [para_into,795,40] c(0 v (1 v (c(x) v 0)))=x^ (0 v 0).

given clause #389: (wt=19) 369 [para_from,57,33,demod,162,18,12] (((0 v c(1 v 1))^ (x v 0)) v c(x v 1)) v 1=1.

given clause #390: (wt=15) 1323 [para_into,862,21,flip.1] 0 v (1 v (0 v (x v 0)))=1 v (x v 0).

given clause #391: (wt=15) 1325 [para_into,863,21,flip.1] 0 v (0 v (1 v (x v 0)))=1 v (x v 0).

given clause #392: (wt=15) 1431 [para_into,879,21,flip.1] 1 v (0 v (0 v (x v 0)))=1 v (x v 0).

given clause #393: (wt=18) 373 [para_into,43,49,demod,162,18,12,12] (x v 1)^ (x v (((0 v c(1 v 1))^0) v 0))=x.

given clause #394: (wt=15) 1477 [para_into,1296,21] 1 v (((1 v 1)^1) v 0)=0 v (1 v 1).

given clause #395: (wt=15) 1508 [para_into,1398,21] 1 v ((x v 1) v 0)= (1 v (x v 0)) v 1.

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

given clause #397: (wt=19) 375 [para_into,43,47] (x v y)^ (x v (c(y v 0) v c(1 v (y v 0))))=x.

given clause #398: (wt=15) 1535 [para_into,1400,21] 1 v ((1 v (x v 0)) v 0)= (x v 1) v 1.

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

given clause #400: (wt=15) 1607 [para_from,200,31] (c(x) v y)^ (x^ (0 v c(y v y)))=0.

given clause #401: (wt=17) 379 [para_into,43,41] (x v y)^ (x v (c(y v 0) v c(y v 1)))=x.

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

given clause #403: (wt=15) 1744 [para_from,1706,57,demod,86,12] (1 v ((0 v c(c(1 v 1)))^1))^1=1.

given clause #404: (wt=15) 1860 [para_into,377,779,demod,1237] 1^ (0 v (0 v ((0 v 0)^ (0 v 0))))=0.

given clause #405: (wt=19) 385 [para_into,43,27] (x v ((c(y) v 0)^z))^ (x v ((y^1) v c(z)))=x.

given clause #406: (wt=15) 1910 [para_into,521,583,demod,1233] 0 v (x v (1^ ((1 v 1)^1)))=x v 1.

given clause #407: (wt=14) 3519 [para_into,1910,1706,demod,170,12,2341,flip.1] (0 v c((1 v 1)^1)) v 1=0 v 1.

given clause #408: (wt=15) 1912 [para_from,521,95] (0 v (0 v 0)) v (x v 1)=0 v (x v 1).

given clause #409: (wt=19) 389 [para_into,43,27] (x v (y^ (c(z) v 0)))^ (x v (c(y) v (z^1)))=x.

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

given clause #411: (wt=15) 1956 [para_into,1952,791] (0 v ((0 v 0)^ (0 v 0)))^ (0 v 1)=0.

given clause #412: (wt=15) 1960 [para_into,1925,21] 1 v ((0 v (0 v (0 v 0))) v 0)=0 v 1.

given clause #413: (wt=19) 395 [para_from,43,37] (c(x v (y^z)) v c(x v (c(y) v c(z))))^x=0.

given clause #414: (wt=15) 2102 [para_into,171,287,demod,1442,288] (x v (((1 v 1)^1)^x))^ (0 v 1)=x.

given clause #415: (wt=15) 2170 [para_into,2148,21] 1 v ((0 v c(c(0 v (0 v 0)))) v 0)=1.

given clause #416: (wt=15) 2244 [para_into,203,287,demod,1442,flip.1] c(c(x) v (0 v 0))=x^ ((1 v 1)^1).

given clause #417: (wt=19) 397 [para_from,43,33] (c(x v (y^z)) v c(x v (c(y) v c(z)))) v x=1.

given clause #418: (wt=11) 3582 [back_demod,506,demod,3577] 0 v (1^ ((1 v 1)^1))=1.

given clause #419: (wt=12) 3600 [para_from,3582,65,demod,12,12,flip.1] 1^ (0 v c((1 v 1)^1))=0.

given clause #420: (wt=13) 3580 [back_demod,839,demod,3577] (1 v (1^ ((1 v 1)^1)))^1=1.

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

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

given clause #423: (wt=14) 3594 [para_from,3582,619] 1^ (0 v (0 v c((1 v 1)^1)))=0.

given clause #424: (wt=15) 2272 [para_into,204,755,demod,12] (c(x) v 1)^ (x^ (0 v c(0 v 1)))=0.

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

given clause #426: (wt=12) 3642 [para_into,2272,7,demod,162,792,10] ((1^c(0 v 1)) v 1)^0=0.

given clause #427: (wt=14) 3654 [para_into,3642,21] (1 v ((1^c(0 v 1)) v 0))^0=0.

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

given clause #429: (wt=16) 419 [para_into,53,179,demod,12] (x v 0)^ ((0 v c(y v y)) v (x v y))=x.

given clause #430: (wt=12) 3670 [para_into,2276,7,demod,162,792,10] ((1^c(x)) v (1^x))^0=0.

given clause #431: (wt=11) 3688 [para_into,3670,2480] ((1^c(c(0))) v 1)^0=0.

given clause #432: (wt=12) 3694 [para_into,3670,585,demod,162,792,10,46] ((1^x) v c(0 v x))^0=0.

given clause #433: (wt=16) 421 [para_into,53,22] (x v c(y v 1))^ (1 v (x v (y v 0)))=x.

given clause #434: (wt=12) 3712 [para_into,3694,45] (x v c(0 v (x v x)))^0=0.

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

given clause #436: (wt=13) 3700 [para_into,3688,21] (1 v ((1^c(c(0))) v 0))^0=0.

given clause #437: (wt=18) 427 [para_into,53,293] (1 v c(x v ((0 v 0) v 0)))^ (x v (0 v 1))=1.

given clause #438: (wt=14) 3750 [para_into,3712,773] ((0 v 1) v c((0 v 1) v 1))^0=0.

given clause #439: (wt=14) 3756 [para_into,3712,120] (1 v c(1 v (1 v (0 v 0))))^0=0.

given clause #440: (wt=15) 2364 [para_into,206,755,demod,12] (c(x) v 1) v (x^ (0 v c(0 v 1)))=1.

given clause #441: (wt=18) 429 [para_into,53,287] ((0 v 0) v c(x v 1))^ (x v (0 v 1))=0 v 0.

given clause #442: (wt=12) 3806 [para_into,2364,7,demod,162,792,10] ((1^c(0 v 1)) v 1) v 0=1.

given clause #443: (wt=10) 3839 [para_from,3806,1188,demod,3829,867,flip.1] (1^c(0 v 1)) v 1=1.

given clause #444: (wt=12) 3851 [para_into,3839,21] 1 v ((1^c(0 v 1)) v 0)=1.

given clause #445: (wt=19) 431 [para_into,53,249] (1 v c(x v ((0 v c(1 v 1)) v 0)))^ (x v 1)=1.

given clause #446: (wt=14) 3845 [para_into,3839,21,demod,1070] (1^ (1^ (0 v c(1 v 1)))) v 1=1.

given clause #447: (wt=14) 3853 [para_from,3839,260,demod,180,flip.1] (1^c(0 v 1)) v (x v 1)=x v 1.

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

given clause #449: (wt=16) 437 [para_into,53,22] (1 v c(x v (y v 0)))^ (x v (y v 1))=1.

given clause #450: (wt=12) 3896 [para_into,2368,7,demod,162,792,10] ((1^c(x)) v (1^x)) v 0=1.

given clause #451: (wt=10) 3929 [para_from,3896,1188,demod,3925,867,flip.1] (1^c(x)) v (1^x)=1.

given clause #452: (wt=10) 3965 [para_into,3929,585,demod,162,792,10,46] (1^x) v c(0 v x)=1.

given clause #453: (wt=17) 439 [para_into,53,19] (x v c(y v (z v c(x))))^ (y v (z v 1))=x.

given clause #454: (wt=10) 4034 [para_into,3965,45] x v c(0 v (x v x))=1.

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

given clause #456: (wt=11) 4112 [para_from,3965,2397,demod,2379,flip.1] (1^x) v 1= (0 v x) v 1.

given clause #457: (wt=19) 441 [para_into,53,179] (x v c((0 v c((x v y) v (x v y))) v y))^1=x.

given clause #458: (wt=11) 4218 [para_from,4034,131] 1^ (0 v (x v (x v x)))=x.

given clause #459: (wt=11) 4220 [para_from,4034,106] 1^ (x v (x v (0 v x)))=x.

given clause #460: (wt=11) 4229 [para_from,4034,2397,demod,2379] (0 v (x v x)) v 1=x v 1.

given clause #461: (wt=16) 443 [para_into,53,40] (x v c(y v 1))^ (x v (1 v (y v 0)))=x.

given clause #462: (wt=7) 4590 [back_demod,3542,demod,4568,4301,flip.1] 1 v 1=0 v 1.

given clause #463: (wt=7) 5018 [para_from,4590,1015,demod,1016,810,18,flip.1] 1 v (0 v 1)=1.

given clause #464: (wt=9) 4608 [back_demod,1296,demod,4591,4591,780] ((0 v 1)^1) v 1=1.

given clause #465: (wt=16) 445 [para_into,53,39] (1 v c(x v (y v 0)))^ (y v (x v 1))=1.

given clause #466: (wt=9) 5079 [para_into,5018,21] 1 v (1 v (0 v 0))=1.

given clause #467: (wt=10) 5040 [para_from,4590,441,demod,4591,1237,2379,288] (1 v c(0 v 1))^1=1.

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

given clause #469: (wt=18) 447 [para_into,53,16] (x v c(y v (z v u)))^ (x v (z v (y v u)))=x.

given clause #470: (wt=11) 4300 [para_from,4205,2397,demod,2379] (x v (0 v x)) v 1=x v 1.

given clause #471: (wt=11) 4555 [para_into,4229,19] (c(0) v 1) v 1=c(0) v 1.

given clause #472: (wt=4) 5476 [back_demod,5358,demod,5425] c(0)=1.

given clause #473: (wt=18) 449 [para_into,53,15] (x v c(y v (z v u)))^ (z v (y v (x v u)))=x.

given clause #474: (wt=5) 5424 [back_demod,4879,demod,5407,5359,3354] 0 v 1=1.

given clause #475: (wt=5) 5652 [back_demod,4590,demod,5425] 1 v 1=1.

given clause #476: (wt=5) 5862 [back_demod,703,demod,5425] 1^1=1.

given clause #477: (wt=16) 469 [para_into,391,41] ((x v 1) v x)^ (c(x v 0) v 1)=x v 1.

given clause #478: (wt=5) 5913 [back_demod,5449,demod,5467,5441,flip.1] 0^1=0.

given clause #479: (wt=6) 5842 [back_demod,791,demod,5425] c(0 v 0)=1.

given clause #480: (wt=7) 5440 [back_demod,2584,demod,5359,5425,5359,5425,704,5425,12,5359,5425] (0 v 0)^1=0.

given clause #481: (wt=16) 473 [para_into,391,27] (x v ((c(y) v 0)^x))^ ((y^1) v 1)=x.

given clause #482: (wt=7) 5456 [back_demod,4475,demod,5425,4591,5425,926,5425,4591,5425,704,5425,flip.1] 1 v (0 v 0)=1.

given clause #483: (wt=7) 5466 [back_demod,5406,demod,5425,12,5425,12] 0^ (0 v 0)=0.

given clause #484: (wt=7) 5882 [back_demod,287,demod,5425] (0 v 0) v 1=1.

given clause #485: (wt=17) 495 [para_into,55,22] 1^ (1 v ((x v 1) v (x v 0)))=1 v (x v 0).

given clause #486: (wt=8) 5632 [back_demod,4693,demod,5425,704,5425,704,5425] c(0 v (0 v 0))=1.

given clause #487: (wt=9) 5436 [back_demod,2590,demod,5359,5425,5359,5425,704,5425,5359,5425] 0 v (x v 1)=x v 1.

given clause #488: (wt=9) 5444 [copy,5370,flip.1,demod,5425,4591,5425,5425,4591,5425] 1 v (x v 1)=x v 1.

given clause #489: (wt=19) 499 [para_into,55,16] 1^ ((x v (y v z)) v (y v (x v z)))=x v (y v z).

given clause #490: (wt=9) 5454 [back_demod,3425,demod,5425,18,5425,4591,5425,12,flip.1] (0 v 0)^ (0 v 0)=0.

given clause #491: (wt=9) 5554 [back_demod,4919,demod,5425,704,5425,5425] (x v (1^x))^1=x.

given clause #492: (wt=9) 5648 [back_demod,4667,demod,5425,704,5425,704,5425] (0 v (0 v 0))^1=0.

given clause #493: (wt=19) 501 [para_into,55,15] 1^ (x v (y v ((y v (x v z)) v z)))=y v (x v z).

given clause #494: (wt=9) 5880 [back_demod,293,demod,5425] 1 v ((0 v 0) v 0)=1.

given clause #495: (wt=9) 5967 [para_from,5476,391,demod,5653] (x v (0^x))^1=x.

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

given clause #497: (wt=18) 531 [para_into,59,179,flip.1] 1 v ((0 v c((x v 1) v (x v 1))) v (x v 0))=1.

given clause #498: (wt=9) 6007 [para_from,5476,3198,demod,5477,12] ((0^0) v 0) v 1=1.

given clause #499: (wt=9) 6009 [para_from,5476,3180,demod,5477,12] ((0^0) v 0)^1=0.

given clause #500: (wt=10) 5532 [back_demod,4949,demod,5425,12,5425,704,5425] c((0 v 0) v 0) v 0=1.

given clause #501: (wt=16) 535 [para_from,59,53] (x v c(y v 1))^ (1 v (y v (x v 0)))=x.

given clause #502: (wt=5) 6383 [para_from,5532,279,demod,12,5843,5457,12,18,5875,flip.1] 0 v 0=0.

given clause #503: (wt=5) 6447 [back_demod,5466,demod,6384] 0^0=0.

given clause #504: (wt=9) 6391 [back_demod,5949,demod,6384] c(c(x) v 1)=x^0.

given clause #505: (wt=18) 537 [para_from,59,179] (0 v c(1 v ((x v 1) v (x v 0)))) v (x v 1)=1.

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

given clause #507: (wt=10) 6003 [para_from,5476,37] (c(x) v 1)^ (x^0)=0.

given clause #508: (wt=10) 6005 [para_from,5476,33] (c(x) v 1) v (x^0)=1.

given clause #509: (wt=18) 539 [para_from,59,156] (0 v c(1 v ((x v 1) v (x v 0))))^ (x v 1)=0.

given clause #510: (wt=10) 6047 [para_from,5476,37] (1 v c(x))^ (0^x)=0.

given clause #511: (wt=10) 6049 [para_from,5476,33] (1 v c(x)) v (0^x)=1.

given clause #512: (wt=11) 5446 [copy,5376,flip.1,demod,5425,5425] x v 1=1 v (1 v (x v 0)).

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

given clause #514: (wt=11) 5874 [back_demod,467,demod,5425] ((x v x) v x)^1=x v x.

given clause #515: (wt=11) 6283 [para_into,5987,21] (1 v (x v 0))^ (x v 0)=x.

given clause #516: (wt=11) 6437 [back_demod,5536,demod,6384] c(1 v (c(x) v 0))=x^0.

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

given clause #518: (wt=12) 5432 [back_demod,4086,demod,5359,5425] (1^ (x v 1)) v c(x v 1)=1.

given clause #519: (wt=9) 6845 [para_from,5432,535,demod,4373,5437,56,flip.1] 1^ (x v 1)=x v 1.

given clause #520: (wt=11) 6887 [para_into,6845,21] 1^ (1 v (x v 0))=x v 1.

given clause #521: (wt=17) 563 [para_from,60,55] 1^ ((1 v (x v 0)) v (x v 1))=1 v (x v 0).

given clause #522: (wt=12) 5438 [back_demod,2586,demod,5359,5425,5359,5425,704,5425,5359,5425] (0 v c(x v 1))^ (x v 1)=0.

given clause #523: (wt=12) 5464 [back_demod,5415,demod,5425,18,5425] (1 v c(x v 1))^ (x v 1)=1.

given clause #524: (wt=12) 5500 [back_demod,4983,demod,5425] (0 v c(x v x)) v (1 v x)=1.

given clause #525: (wt=16) 565 [para_from,60,53] (x v c(1 v (y v 0)))^ (x v (y v 1))=x.

given clause #526: (wt=12) 5502 [back_demod,4981,demod,5425] (1^c(x v x)) v (1 v x)=1.

given clause #527: (wt=12) 5576 [back_demod,4845,demod,5425,704,5425,12,5425] (1^c(x v x)) v (0 v x)=1.

given clause #528: (wt=12) 5578 [back_demod,4843,demod,5425,704,5425,12,5425] (0 v c(x v x)) v (0 v x)=1.

given clause #529: (wt=17) 567 [para_from,60,16] x v (y v (z v 1))=1 v (y v (x v (z v 0))).

given clause #530: (wt=12) 5626 [back_demod,4701,demod,5425,704,5425,5425,12] (c(x v (1^x)) v 0)^x=0.

given clause #531: (wt=12) 5628 [back_demod,4699,demod,5425,704,5425,5425,12] (c(x v (1^x)) v 0) v x=1.

given clause #532: (wt=12) 6246 [para_from,5967,91] (c(x v (0^x)) v 0) v x=1.

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

given clause #534: (wt=12) 6248 [para_from,5967,89] (c(x v (0^x)) v 0)^x=0.

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

given clause #536: (wt=12) 6387 [back_demod,6291,demod,6384] ((x^0) v (x^1))^c(x)=0.

given clause #537: (wt=19) 577 [para_into,65,55,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) 6411 [back_demod,5694,demod,6384] (1 v (c(x) v 0))^ (x^0)=0.

given clause #539: (wt=12) 6413 [back_demod,5688,demod,6384] (1 v (c(x) v 0)) v (x^0)=1.

given clause #540: (wt=12) 6433 [back_demod,5540,demod,6384] ((x^1) v (x^0)) v c(x)=1.

given clause #541: (wt=18) 581 [para_into,65,47,flip.1] 1^ (c(x v 0) v c(1 v (x v 0)))=c(0 v x).

given clause #542: (wt=12) 6435 [back_demod,5538,demod,6384] ((x^1) v (x^0))^c(x)=0.

given clause #543: (wt=12) 6474 [para_from,6383,425] (0 v (x^1))^ (c(x) v 0)=0.

given clause #544: (wt=12) 6495 [para_from,6383,53] (0 v c(x v 0))^ (x v 0)=0.

given clause #545: (wt=16) 584 [para_into,65,41] c(0 v x)=1^ (c(x v 0) v c(x v 1)).

given clause #546: (wt=12) 6639 [para_from,6499,3965] (1^ (x v 0)) v c(x v 0)=1.

given clause #547: (wt=12) 6785 [para_from,6437,445,demod,5653] (1 v (x^0))^ (c(x) v 1)=1.

given clause #548: (wt=12) 6871 [back_demod,6415,demod,6846] (1^ (x^0)) v (c(x) v 1)=1.

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

given clause #550: (wt=12) 6873 [back_demod,5995,demod,6846] (0 v (x^0)) v (c(x) v 1)=1.

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

given clause #552: (wt=12) 6891 [back_demod,1345,demod,6888] (0 v c(x v 1)) v (x v 1)=1.

given clause #553: (wt=19) 587 [para_from,65,53] (x v (1^ (c(y) v c(z))))^ (0 v (x v (y^z)))=x.

given clause #554: (wt=12) 7346 [para_into,6639,279,demod,6384,5477,6384,18,12,18] (1^ (c(x) v 0)) v (x^1)=1.

given clause #555: (wt=8) 7680 [para_into,7346,5967,demod,6258] c(0 v x) v x=1.

given clause #556: (wt=7) 7808 [para_from,7680,1868,demod,162,6384,5477,5425,12,18,46,5425,162,6384,5477,5425,12,18,46] (x v x)^1=x.

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

given clause #558: (wt=8) 7744 [para_into,7680,161,demod,6384,5477,5425,12,18] (1^x) v c(x)=1.

given clause #559: (wt=8) 8289 [para_into,7744,45] x v c(x v x)=1.

given clause #560: (wt=9) 7949 [para_from,7680,2397,demod,2379,162,6384,5477,5425,12,18,4113,flip.1] (0 v x) v 1=x v 1.

given clause #561: (wt=19) 591 [para_from,65,91] ((1^ (c(x) v c(y))) v 0) v ((0 v (x^y))^1)=1.

given clause #562: (wt=9) 8137 [back_demod,4229,demod,7950] (x v x) v 1=x v 1.

given clause #563: (wt=9) 8141 [back_demod,4112,demod,7950] (1^x) v 1=x v 1.

given clause #564: (wt=9) 8153 [back_demod,2378,demod,7950] (x^x) v 1=x v 1.

given clause #565: (wt=19) 593 [para_from,65,89] ((1^ (c(x) v c(y))) v 0)^ ((0 v (x^y))^1)=0.

given clause #566: (wt=9) 8360 [para_from,8289,53] 1^ (x v (x v x))=x.

given clause #567: (wt=9) 8780 [back_demod,8350,demod,8728] x^ (c(x) v c(x))=0.

given clause #568: (wt=10) 7694 [para_into,7680,6499] c(x v 0) v (x v 0)=1.

given clause #569: (wt=19) 595 [para_from,65,71] (0 v (1^ (c(x) v c(y)))) v (1^ (0 v (x^y)))=1.

given clause #570: (wt=10) 7696 [para_into,7680,5436] c(x v 1) v (x v 1)=1.

given clause #571: (wt=10) 7919 [para_from,7680,126,demod,5653,6500,flip.1] x v (c(x v 0) v 1)=1.

given clause #572: (wt=10) 7921 [para_from,7680,60,demod,5653,6500,flip.1] c(x v 0) v (x v 1)=1.

given clause #573: (wt=19) 597 [para_from,65,69] (0 v (1^ (c(x) v c(y))))^ (1^ (0 v (x^y)))=0.

given clause #574: (wt=8) 9090 [para_into,7921,8153,demod,86,7809] c(x) v (x v 1)=1.

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

given clause #576: (wt=9) 9226 [para_from,9090,307,demod,6438] (x v (x^0))^1=x.

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

given clause #578: (wt=9) 9380 [para_from,9222,1763,demod,8566,6392,8142] (x^0) v 1=x v 1.

given clause #579: (wt=9) 9408 [back_demod,9040,demod,9381] (x v 0) v 1=x v 1.

given clause #580: (wt=10) 7985 [para_from,7680,251,demod,7681,5653,12,6384] c(0 v x) v (0 v x)=1.

given clause #581: (wt=18) 607 [para_from,120,179] (0 v c(1 v (x v ((x v 1) v 0)))) v (x v 1)=1.

given clause #582: (wt=10) 8007 [para_from,7680,601,demod,5863,7950] ((0 v c(x))^x) v 1=1.

given clause #583: (wt=8) 9980 [para_from,8007,41,demod,8004,flip.1] (0 v c(x))^x=0.

given clause #584: (wt=10) 8185 [para_from,7808,682] ((x^x) v 0) v c(x)=1.

given clause #585: (wt=18) 609 [para_from,120,156] (0 v c(1 v (x v ((x v 1) v 0))))^ (x v 1)=0.

given clause #586: (wt=10) 8187 [para_from,7808,670] ((x^x) v 0)^c(x)=0.

given clause #587: (wt=10) 8233 [para_from,7808,91] (c(x v x) v 0) v x=1.

given clause #588: (wt=10) 8235 [para_from,7808,89] (c(x v x) v 0)^x=0.

given clause #589: (wt=17) 611 [para_from,120,16] x v (1 v (y v (z v 0)))=z v (y v (x v 1)).

given clause #590: (wt=10) 8749 [para_from,8153,57,demod,86,7809] (1 v c(x))^ (x v 1)=1.

given clause #591: (wt=10) 8822 [para_from,8360,7744] x v c(x v (x v x))=1.

given clause #592: (wt=10) 8872 [para_from,8780,206] (c(x) v (x^x)) v 0=1.

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

given clause #594: (wt=8) 10213 [para_from,8872,6283,demod,8873,5653,5863,flip.1] c(x) v (x^x)=1.

given clause #595: (wt=10) 8878 [para_into,7694,279,demod,6384,5477,6384,18,12,18] (x^1) v (c(x) v 0)=1.

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

given clause #597: (wt=17) 615 [para_from,126,16] x v (y v (z v 1))=1 v (z v (x v (y v 0))).

given clause #598: (wt=10) 8977 [para_into,7696,6391] (x^0) v (c(x) v 1)=1.

given clause #599: (wt=10) 9028 [para_into,7919,279,demod,6384,5477,6384,18,12,18] c(x) v ((x^1) v 1)=1.

given clause #600: (wt=10) 9086 [para_into,7921,279,demod,6384,5477,6384,18,12,18] (x^1) v (c(x) v 1)=1.

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

given clause #602: (wt=9) 10606 [para_from,9086,1763,demod,8566,9519,9617,8142,9381,flip.1] (x^1) v 1=x v 1.

given clause #603: (wt=9) 10631 [back_demod,10320,demod,10607] c(c(x)) v 1=x v 1.

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

given clause #605: (wt=18) 617 [para_into,67,27] (x v (1^ (c(y) v 0)))^ (x v (0 v (y^1)))=x.

given clause #606: (wt=9) 10980 [back_demod,9518,demod,10855] c(x v 1)=c(x)^0.

given clause #607: (wt=9) 11050 [para_into,10796,10631,demod,10797,flip.1] c(c(x))^0=x^0.

given clause #608: (wt=9) 11052 [para_into,10796,10606,demod,10797,flip.1] (x^1)^0=x^0.

given clause #609: (wt=18) 621 [para_from,67,37] (c(x v (1^y)) v c(x v (0 v c(y))))^x=0.

given clause #610: (wt=9) 11054 [para_into,10796,9408,demod,10797,flip.1] (x v 0)^0=x^0.

given clause #611: (wt=9) 11056 [para_into,10796,9380,demod,10797,flip.1] (x^0)^0=x^0.

given clause #612: (wt=9) 11058 [para_into,10796,8153,demod,10797,flip.1] (x^x)^0=x^0.

given clause #613: (wt=18) 623 [para_from,67,33] (c(x v (1^y)) v c(x v (0 v c(y)))) v x=1.

given clause #614: (wt=9) 11060 [para_into,10796,8141,demod,10797,flip.1] (1^x)^0=x^0.

given clause #615: (wt=9) 11062 [para_into,10796,8137,demod,10797,flip.1] (x v x)^0=x^0.

given clause #616: (wt=9) 11064 [para_into,10796,7949,demod,10797,flip.1] (0 v x)^0=x^0.

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

given clause #618: (wt=9) 11108 [para_from,10796,9380,demod,9381,flip.1] (x v 1) v 1=x v 1.

given clause #619: (wt=10) 9194 [para_into,9090,8153] c(x^x) v (x v 1)=1.

given clause #620: (wt=10) 9196 [para_into,9090,8141] c(1^x) v (x v 1)=1.

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

given clause #622: (wt=10) 9198 [para_into,9090,8137] c(x v x) v (x v 1)=1.

given clause #623: (wt=10) 9200 [para_into,9090,7949] c(0 v x) v (x v 1)=1.

given clause #624: (wt=5) 12035 [para_into,9200,2,demod,12016] x v 1=1.

given clause #625: (wt=19) 666 [para_from,85,53] (x v ((c(y) v c(z))^1))^ ((y^z) v (x v 0))=x.

given clause #626: (wt=5) 12067 [back_demod,8852,demod,12036,46] x^0=0.

given clause #627: (wt=5) 12531 [back_demod,6035,demod,12052,12060] 0^x=0.

given clause #628: (wt=6) 12747 [back_demod,6052,demod,12532,flip.1] c(1 v x)=0.

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

given clause #630: (wt=5) 12908 [para_from,12747,51,demod,5477,12036,5863,flip.1] 1 v x=1.

given clause #631: (wt=7) 12059 [back_demod,9398,demod,12036,12036,12036,12,12036,12036] (x v 0)^1=x.

given clause #632: (wt=7) 12073 [back_demod,7392,demod,12036,12036,5914,12068,6384] 1^ (x v 0)=x.

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

given clause #634: (wt=7) 12630 [back_demod,7284,demod,12068,12074] x^1=1^x.

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

given clause #636: (wt=8) 12523 [back_demod,19,demod,12036] x v (y v c(x))=1.

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

given clause #638: (wt=8) 12543 [back_demod,7678,demod,12074,12060] (x^1) v c(x)=1.

given clause #639: (wt=8) 12599 [back_demod,10942,demod,12068,12074] c(x v 0) v x=1.

given clause #640: (wt=8) 12681 [back_demod,8208,demod,12074] c(x v x) v x=1.

given clause #641: (wt=19) 907 [copy,905,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) 12685 [back_demod,7346,demod,12074] c(x) v (x^1)=1.

given clause #643: (wt=8) 12968 [para_from,12073,7744] x v c(x v 0)=1.

given clause #644: (wt=8) 13138 [back_demod,12595,demod,13123] (c(x) v 0)^x=0.

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

given clause #646: (wt=8) 13580 [para_into,12685,12630] c(x) v (1^x)=1.

given clause #647: (wt=8) 13644 [para_from,12968,670,demod,5863,12060] x^ (c(x) v 0)=0.

given clause #648: (wt=9) 12099 [back_demod,391,demod,12036] (x v (y^x))^1=x.

given clause #649: (wt=19) 951 [para_into,98,16] x v (y v (z v (u v v)))=u v (z v (y v (x v v))).

given clause #650: (wt=9) 12525 [back_demod,8261,demod,12060] c(x v x)=c(x v 0).

given clause #651: (wt=9) 12526 [back_demod,8251,demod,12060] c(x v 0)=c(x v x).

given clause #652: (wt=9) 12585 [back_demod,11086,demod,12068] 1^ (x v (x v 0))=x.

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

given clause #654: (wt=9) 12608 [back_demod,9496,demod,12068,12074] c(x v 0)=c(0 v x).

given clause #655: (wt=5) 14142 [back_demod,13192,demod,14120] x^1=x.

given clause #656: (wt=5) 14148 [back_demod,8360,demod,14120] 1^x=x.

given clause #657: (wt=19) 1064 [copy,1060,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) 14152 [back_demod,4218,demod,14120,14149] 0 v x=x.

given clause #659: (wt=5) 14182 [back_demod,13960,demod,14153,14143] c(c(x))=x.

given clause #660: (wt=5) 14200 [back_demod,13860,demod,14143,14153,14143] x^x=x.

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

given clause #662: (wt=5) 14228 [back_demod,13708,demod,14143,14143] x v x=x.

given clause #663: (wt=5) 14258 [back_demod,13484,demod,14143,14143,14229,13645,14143] x v 0=x.

given clause #664: (wt=6) 14274 [back_demod,13300,demod,14259,14259,14143,14229,14183] c(x) v x=1.

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

given clause #666: (wt=6) 14278 [back_demod,13270,demod,14153,14149,14153,14143,14153,14149] c(x)^x=0.

given clause #667: (wt=7) 14146 [back_demod,12057,demod,14120,14143] x v (y^x)=x.

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

given clause #669: (wt=12) 12513 [back_demod,144,demod,12036,12036,12036] x v (y v (z v (u v c(x))))=1.

given clause #670: (wt=7) 14601 [para_into,14566,14146,flip.1] (x^y) v y=y.

given clause #671: (wt=8) 14296 [back_demod,12519,demod,14259,14143] c(x) v (y v x)=1.

given clause #672: (wt=8) 14310 [back_demod,12289,demod,14259,14259,14293,14183,14143] x v (x^c(y))=x.

given clause #673: (wt=13) 12515 [back_demod,142,demod,12036] (c(x) v c(y)) v (z v (x^y))=1.

given clause #674: (wt=7) 14869 [para_into,14310,14182] x v (x^y)=x.

given clause #675: (wt=7) 14881 [para_into,14869,14566] (x^y) v x=x.

given clause #676: (wt=8) 14318 [back_demod,12165,demod,14143,14259] c(x) v (x v y)=1.

given clause #677: (wt=10) 12521 [back_demod,95,demod,12036,12036] x v (y v (z v c(x)))=1.

given clause #678: (wt=8) 14320 [back_demod,12163,demod,14143,14259] x v (c(x) v y)=1.

given clause #679: (wt=8) 14603 [para_into,14566,12523,flip.1] (x v c(y)) v y=1.

given clause #680: (wt=8) 14865 [para_into,14296,14566] (x v y) v c(y)=1.

given clause #681: (wt=17) 13040 [para_into,905,33,demod,12036,12036,12036,flip.1] (c(x) v c(y)) v (z v (u v (v v (x^y))))=1.

given clause #682: (wt=8) 14959 [para_into,14318,14566] (x v y) v c(x)=1.

given clause #683: (wt=8) 14967 [para_into,14320,14566] (c(x) v y) v x=1.

given clause #684: (wt=9) 14222 [back_demod,13738,demod,14143] (x v y) v x=x v y.

given clause #685: (wt=14) 13280 [para_from,12523,905,demod,12036,12036,12036,flip.1] x v (y v (z v (u v (v v c(x)))))=1.

given clause #686: (wt=9) 14440 [back_demod,13278,demod,14183,14183,14229,14293,14153] x^ (c(y)^c(x))=0.

given clause #687: (wt=8) 15173 [para_into,14440,14182] x^ (y^c(x))=0.

given clause #688: (wt=8) 15177 [para_into,15173,14182] c(x)^ (y^x)=0.

given clause #689: (wt=13) 14224 [back_demod,13734,demod,14143] (x v (y v z)) v y=x v (y v z).

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

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

given clause #692: (wt=9) 15017 [para_from,14603,7,demod,14183,14149,14183] (x v y) v y=x v y.

given clause #693: (wt=17) 14226 [back_demod,13720,demod,14143] (x v (y v (z v u))) v z=x v (y v (z v u)).

given clause #694: (wt=9) 15183 [para_into,15177,7,demod,14293] (c(x)^c(y))^x=0.

given clause #695: (wt=8) 15261 [para_into,15183,14182] (c(x)^y)^x=0.

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

given clause #697: (wt=10) 14244 [back_demod,13610,demod,14143] c(x) v (y v (z v x))=1.

given clause #698: (wt=8) 15269 [para_into,15263,7,demod,14293,14183] x^ (c(x)^y)=0.

given clause #699: (wt=8) 15281 [para_into,15269,14182] c(x)^ (x^y)=0.

given clause #700: (wt=10) 14260 [back_demod,13480,demod,14229,14143] x v ((x v c(y))^y)=x.

given clause #701: (wt=12) 14246 [back_demod,13602,demod,14143] c(x) v (y v (z v (u v x)))=1.

given clause #702: (wt=10) 14280 [back_demod,13254,demod,14143,14153] (x v y)^ (x v c(y))=x.

given clause #703: (wt=10) 14292 [back_demod,12959,demod,14259,14259,14259,14143,flip.1] c(x v y)=c(x)^c(y).

given clause #704: (wt=9) 15366 [para_into,14292,14865,demod,12,14293,14183,flip.1] (c(x)^c(y))^y=0.

given clause #705: (wt=11) 14250 [back_demod,13578,demod,14229,14153,14143] (x^c(y)) v (c(x) v y)=1.

given clause #706: (wt=8) 15447 [para_into,15366,14182] (x^c(y))^y=0.

given clause #707: (wt=8) 15541 [para_into,15447,14182] (x^y)^c(y)=0.

given clause #708: (wt=10) 14294 [back_demod,12567,demod,14143,14259] (x v c(y))^ (y v x)=x.

given clause #709: (wt=11) 14272 [back_demod,13306,demod,14143,14229,14153] (c(x) v y) v (x^c(y))=1.

given clause #710: (wt=10) 14314 [back_demod,12169,demod,14143,14259] x v (y v (c(x) v z))=1.

given clause #711: (wt=10) 14316 [back_demod,12167,demod,14143,14259] c(x) v (y v (x v z))=1.

given clause #712: (wt=10) 14354 [back_demod,425,demod,14143,14259] (x v y)^ (c(y) v x)=x.

given clause #713: (wt=11) 14282 [back_demod,13250,demod,14143,14153] (c(x) v y)^ (x^c(y))=0.

given clause #714: (wt=10) 14366 [back_demod,85,demod,14259,14143] c(x^y)=c(x) v c(y).

given clause #715: (wt=10) 14432 [back_demod,13051,demod,14229,14293,14153,14293,14367,14183,14183,14149] x v ((x v y)^c(y))=x.

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

given clause #717: (wt=11) 14284 [back_demod,13238,demod,14153,14143] (x^y)^ (c(x) v c(y))=0.

given clause #718: (wt=10) 14961 [para_into,12521,14566] x v ((y v c(x)) v z)=1.

given clause #719: (wt=10) 14963 [para_into,12521,14566] (x v (y v c(z))) v z=1.

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

given clause #721: (wt=11) 14286 [back_demod,13236,demod,14153,14143] (x^y) v (c(x) v c(y))=1.

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

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

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

given clause #725: (wt=15) 14288 [back_demod,13234,demod,14143,14153] (x v (c(y) v c(z)))^ (x v (y^z))=x.

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

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

given clause #728: (wt=10) 15179 [para_into,15177,393,demod,14293,14183,14293,14183] (x^ (c(y)^z))^y=0.

given clause #729: (wt=13) 14298 [back_demod,12501,demod,14259,14143] (x^y) v (z v (c(x) v c(y)))=1.

given clause #730: (wt=10) 15271 [para_into,14244,14566] c(x) v ((y v x) v z)=1.

given clause #731: (wt=10) 15277 [para_into,14244,14566] (x v (y v z)) v c(z)=1.

given clause #732: (wt=10) 15283 [para_into,14260,14566] x v ((c(y) v x)^y)=x.

given clause #733: (wt=11) 14300 [back_demod,12491,demod,14293,14293,14183,14143] x v (c(y)^ (c(z)^x))=x.

given clause #734: (wt=10) 15285 [para_into,14260,14566] ((x v c(y))^y) v x=x.

given clause #735: (wt=10) 15334 [para_into,14280,14566] (x v y)^ (y v c(x))=y.

given clause #736: (wt=10) 15545 [para_into,15541,393,demod,14293,14183,14293,14183] x^ (y^ (c(x)^z))=0.

given clause #737: (wt=13) 14302 [back_demod,12479,demod,14143,14259] (x v c(y)) v (z v (c(x)^y))=1.

given clause #738: (wt=10) 15555 [para_into,14294,14566] (c(x) v y)^ (x v y)=y.

given clause #739: (wt=10) 15597 [para_into,14314,14566] x v ((c(x) v y) v z)=1.

given clause #740: (wt=10) 15611 [para_into,14316,14566] c(x) v ((x v y) v z)=1.

given clause #741: (wt=13) 14304 [back_demod,12477,demod,14143,14259] (c(x) v y) v (z v (x^c(y)))=1.

given clause #742: (wt=10) 15623 [para_into,14354,14566] (x v y)^ (c(x) v y)=y.

given clause #743: (wt=10) 15741 [para_into,14432,14566] x v ((y v x)^c(y))=x.

given clause #744: (wt=10) 15747 [para_into,14432,14566] ((x v y)^c(y)) v x=x.

given clause #745: (wt=17) 14330 [back_demod,8167,demod,14143] (x v (y v z)) v (y v (x v z))=x v (y v z).

given clause #746: (wt=10) 15818 [para_into,14961,14566] ((x v c(y)) v z) v y=1.

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

given clause #748: (wt=10) 15960 [para_into,15045,14566] (x v y) v (c(y) v z)=1.

given clause #749: (wt=11) 14338 [back_demod,3892,demod,14143,14149,14259,14153] (x v y) v (c(x)^c(y))=1.

given clause #750: (wt=10) 15974 [para_into,15073,14566] ((x v y) v z) v c(x)=1.

given clause #751: (wt=10) 16000 [para_into,15087,14566] (x v y) v (c(x) v z)=1.

given clause #752: (wt=10) 16032 [para_into,15099,14566] ((c(x) v y) v z) v x=1.

given clause #753: (wt=11) 14340 [back_demod,3666,demod,14143,14149,14259,14153] (x v y)^ (c(x)^c(y))=0.

given clause #754: (wt=10) 16076 [para_into,15143,14566] (c(x) v y) v (x v z)=1.

given clause #755: (wt=10) 16094 [para_into,15179,14182] (x^ (y^z))^c(y)=0.

given clause #756: (wt=10) 16122 [para_into,15271,14566] ((x v y) v z) v c(y)=1.

given clause #757: (wt=11) 14342 [back_demod,3192,demod,14259,14259,14143,14143] (c(x)^y) v (x v c(y))=1.

given clause #758: (wt=10) 16158 [para_into,15283,14566] ((c(x) v y)^x) v y=y.

given clause #759: (wt=10) 16203 [para_into,14300,14182] x v (y^ (c(z)^x))=x.

given clause #760: (wt=9) 16853 [para_into,16203,14182] x v (y^ (z^x))=x.

given clause #761: (wt=11) 14344 [back_demod,3178,demod,14259,14259,14143,14143] (x^c(y))^ (c(x) v y)=0.

given clause #762: (wt=9) 16857 [para_into,16853,14566] (x^ (y^z)) v z=z.

given clause #763: (wt=10) 16266 [para_into,15545,14182] c(x)^ (y^ (x^z))=0.

given clause #764: (wt=10) 16432 [para_into,15741,14566] ((x v y)^c(x)) v y=y.

given clause #765: (wt=11) 14346 [back_demod,3174,demod,14259,14259,14143,14143] (c(x)^y)^ (x v c(y))=0.

given clause #766: (wt=10) 16736 [para_into,16094,15555,demod,14293,14183] (x^y)^ (z^c(y))=0.

given clause #767: (wt=10) 16740 [para_into,16094,14294,demod,14293,14183] (x^y)^ (c(y)^z)=0.

given clause #768: (wt=10) 16949 [para_into,16266,15555,demod,14293,14183] (x^c(y))^ (z^y)=0.

given clause #769: (wt=15) 14348 [back_demod,3126,demod,14259,14143] (x v (y^c(z)))^ (c(y) v (x v z))=x.

given clause #770: (wt=10) 16953 [para_into,16266,14294,demod,14293,14183] (c(x)^y)^ (z^x)=0.

given clause #771: (wt=10) 16998 [para_into,16736,15623,demod,14293,14183] x^ (y^ (z^c(x)))=0.

given clause #772: (wt=10) 17006 [para_into,16740,15623,demod,14293,14183] x^ ((y^c(x))^z)=0.

given clause #773: (wt=15) 14350 [back_demod,3124,demod,14259,14143] (x v (c(y)^z))^ (y v (x v c(z)))=x.

given clause #774: (wt=10) 17008 [para_into,16740,15334,demod,14293,14183] x^ ((c(x)^y)^z)=0.

given clause #775: (wt=10) 17016 [para_into,16740,14182] (x^c(y))^ (y^z)=0.

given clause #776: (wt=10) 17022 [para_into,16949,15623,demod,14293,14183] (x^ (y^c(z)))^z=0.

given clause #777: (wt=15) 14352 [back_demod,666,demod,14143,14259] (x v (c(y) v c(z)))^ ((y^z) v x)=x.

given clause #778: (wt=10) 17068 [para_into,14348,14320,demod,14293,14183,12036,14143] x v (y^ (x^c(z)))=x.

given clause #779: (wt=9) 17204 [para_into,17068,14182] x v (y^ (x^z))=x.

given clause #780: (wt=9) 17208 [para_into,17204,14566] (x^ (y^z)) v y=y.

given clause #781: (wt=15) 14356 [back_demod,389,demod,14259,14143] (x v (y^c(z)))^ (x v (c(y) v z))=x.

given clause #782: (wt=10) 17104 [para_into,16953,14182] (x^y)^ (z^c(x))=0.

given clause #783: (wt=10) 17106 [para_into,16953,15623,demod,14293,14183] ((x^c(y))^z)^y=0.

given clause #784: (wt=10) 17108 [para_into,16953,15334,demod,14293,14183] ((c(x)^y)^z)^x=0.

given clause #785: (wt=15) 14358 [back_demod,385,demod,14259,14143] (x v (c(y)^z))^ (x v (y v c(z)))=x.

given clause #786: (wt=10) 17118 [para_into,16998,14182] c(x)^ (y^ (z^x))=0.

given clause #787: (wt=10) 17124 [para_into,17006,14182] c(x)^ ((y^x)^z)=0.

given clause #788: (wt=10) 17136 [para_into,14350,16076,demod,14293,14183,14143] x v ((x^c(y))^z)=x.

given clause #789: (wt=11) 14360 [back_demod,271,demod,14143,14259] (x v c(y))^ (c(x)^y)=0.

given clause #790: (wt=9) 17370 [para_into,17136,14182] x v ((x^y)^z)=x.

given clause #791: (wt=9) 17390 [para_into,17370,14566] ((x^y)^z) v x=x.

given clause #792: (wt=10) 17142 [para_into,14350,15836,demod,14293,14183,14143] x v ((c(y)^x)^z)=x.

given clause #793: (wt=11) 14362 [back_demod,235,demod,14143,14259] (x v c(y)) v (c(x)^y)=1.

given clause #794: (wt=9) 17472 [para_into,17142,14182] x v ((y^x)^z)=x.

given clause #795: (wt=9) 17514 [para_into,17472,14566] ((x^y)^z) v y=y.

given clause #796: (wt=10) 17172 [para_into,17008,14182] c(x)^ ((x^y)^z)=0.

given clause #797: (wt=11) 14370 [back_demod,13762,demod,14259,14293,14153] x v ((c(x)^c(y)) v y)=1.

given clause #798: (wt=10) 17182 [para_into,17022,14182] (x^ (y^z))^c(z)=0.

given clause #799: (wt=10) 17308 [para_into,17106,14182] ((x^y)^z)^c(y)=0.

given clause #800: (wt=10) 17314 [para_into,17108,14182] ((x^y)^z)^c(x)=0.

given clause #801: (wt=18) 14372 [back_demod,13754,demod,14259,14293,14293] x v (y v ((c(y)^ (c(x)^c(z))) v (u v z)))=1.

given clause #802: (wt=10) 17358 [para_into,17124,15334,demod,14293,14183] (c(x)^y)^ (x^z)=0.

given clause #803: (wt=10) 17634 [para_into,17308,15334,demod,14293,14183] (x^y)^ (c(x)^z)=0.

given clause #804: (wt=11) 14374 [back_demod,13752,demod,14259,14259,14259] c(x)^ (c(y) v c(x))=c(x).

given clause #805: (wt=18) 14376 [back_demod,13572,demod,14259,14293,14293] x v (y v ((c(x)^ (c(y)^c(z))) v (u v z)))=1.

given clause #806: (wt=8) 17696 [para_into,14374,14182,demod,14183,14183] x^ (c(y) v x)=x.

given clause #807: (wt=7) 17734 [para_into,17696,14182] x^ (y v x)=x.

given clause #808: (wt=7) 17774 [para_into,17734,14566] x^ (x v y)=x.

given clause #809: (wt=13) 14378 [back_demod,13450,demod,14259,14293] x v (y v ((c(x)^c(z)) v z))=1.

given clause #810: (wt=9) 17772 [para_into,17734,14869] (x^y)^x=x^y.

given clause #811: (wt=9) 17784 [para_into,17734,14224] x^ (y v (x v z))=x.

given clause #812: (wt=9) 17786 [para_into,17734,14146] (x^y)^y=x^y.

given clause #813: (wt=13) 14380 [back_demod,13448,demod,14259,14293] (c(x)^c(y)) v (x v (z v y))=1.

given clause #814: (wt=9) 17860 [para_into,17784,14566] x^ (y v (z v x))=x.

given clause #815: (wt=9) 17864 [para_into,17784,14566] x^ ((x v y) v z)=x.

given clause #816: (wt=9) 17944 [para_into,17860,14566] x^ ((y v x) v z)=x.

given clause #817: (wt=13) 14382 [back_demod,13446,demod,14259,14293] x v ((c(x)^c(y)) v (z v y))=1.

given clause #818: (wt=11) 14430 [back_demod,13210,demod,14153,14293,14149,14153] (c(x)^c(y)) v (x v y)=1.

given clause #819: (wt=11) 14450 [back_demod,6476,demod,14259,14293,14153,14259] (c(x)^c(y))^ (y v x)=0.

given clause #820: (wt=11) 14562 [para_from,14258,123,demod,14259] x v (y v z)=x v (z v y).

given clause #821: (wt=15) 14384 [back_demod,13412,demod,14259,14293] x v (y v (z v ((c(x)^c(u)) v u)))=1.

given clause #822: (wt=11) 14563 [para_from,14258,99,demod,14259] x v (y v z)=z v (y v x).

given clause #823: (wt=10) 18570 [back_demod,17610,demod,18418,14882,flip.1] (x^c(y)) v y=y v x.

given clause #824: (wt=10) 18928 [back_demod,17490,demod,18571] c(x) v ((y v x)^x)=1.

given clause #825: (wt=15) 14386 [back_demod,13410,demod,14259,14293] (c(x)^c(y)) v (x v (z v (u v y)))=1.

given clause #826: (wt=7) 19087 [para_from,18928,14354,demod,14602,14143,flip.1] (x v y)^y=y.

given clause #827: (wt=7) 19113 [para_into,19087,18570] (x v y)^x=x.

given clause #828: (wt=9) 19123 [para_into,19087,14869] x^ (x^y)=x^y.

given clause #829: (wt=15) 14388 [back_demod,13408,demod,14259,14293] (c(x)^c(y)) v (z v (x v (u v y)))=1.

given clause #830: (wt=9) 19133 [para_into,19087,14146] x^ (y^x)=y^x.

given clause #831: (wt=9) 19151 [para_into,19113,14563] (x v (y v z))^z=z.

given clause #832: (wt=9) 19163 [para_into,19113,2] (x v (y v z))^y=y.

given clause #833: (wt=15) 14390 [back_demod,13406,demod,14259,14293] x v ((c(x)^c(y)) v (z v (u v y)))=1.

given clause #834: (wt=10) 18989 [para_into,18570,17786,demod,18571,flip.1] x v (y^c(x))=x v y.

given clause #835: (wt=10) 19021 [para_from,18570,15334,demod,14183,14147,14183] x^ (c(x) v y)=y^x.

given clause #836: (wt=10) 19037 [para_from,18570,14294,demod,14183,14147,14183] (c(x) v y)^x=y^x.

given clause #837: (wt=15) 14392 [back_demod,13404,demod,14259,14293] x v (y v ((c(x)^c(z)) v (u v z)))=1.

given clause #838: (wt=10) 19047 [copy,19021,flip.1] x^y=y^ (c(y) v x).

given clause #839: (wt=10) 19299 [para_into,19021,14566] x^ (y v c(x))=y^x.

given clause #840: (wt=10) 19324 [copy,19299,flip.1] x^y=y^ (x v c(y)).

given clause #841: (wt=18) 14394 [back_demod,13402,demod,14259,14293,14293] x v (y v ((c(z)^ (c(x)^c(u))) v (z v u)))=1.

given clause #842: (wt=10) 19355 [back_demod,15285,demod,19303] (x^ (y v c(x))) v y=y.

given clause #843: (wt=10) 19357 [back_demod,14260,demod,19303] x v (y^ (x v c(y)))=x.

given clause #844: (wt=10) 19540 [para_from,19047,15747,demod,14183,14529] (c(x)^ (y v x)) v y=y.

given clause #845: (wt=18) 14396 [back_demod,13400,demod,14259,14293,14293] x v (y v (z v ((c(z)^ (c(x)^c(u))) v u)))=1.

given clause #846: (wt=10) 19542 [para_from,19047,14432,demod,14183,14529] x v (c(y)^ (x v y))=x.

given clause #847: (wt=10) 19636 [para_from,19047,14881] (x^ (c(x) v y)) v y=y.

given clause #848: (wt=10) 19638 [para_from,19047,14869] x v (y^ (c(y) v x))=x.

given clause #849: (wt=18) 14398 [back_demod,13398,demod,14259,14293,14293] (c(x)^ (c(y)^c(z))) v (x v (y v (u v z)))=1.

given clause #850: (wt=10) 19860 [para_into,19540,14566] (c(x)^ (x v y)) v y=y.

given clause #851: (wt=10) 19931 [para_into,19542,14566] x v (c(y)^ (y v x))=x.

given clause #852: (wt=11) 14564 [para_from,14258,16,demod,14259] x v (y v z)=y v (z v x).

given clause #853: (wt=18) 14400 [back_demod,13396,demod,14259,14293,14293] (c(x)^ (c(y)^c(z))) v (y v (x v (u v z)))=1.

given clause #854: (wt=11) 14565 [para_from,14258,15,demod,14259] x v (y v z)=z v (x v y).

given clause #855: (wt=11) 14599 [para_from,14146,2,flip.1] x v (y v (z^x))=y v x.

given clause #856: (wt=11) 14743 [para_from,14566,37] (c(x) v c(y))^ (y^x)=0.

given clause #857: (wt=18) 14404 [back_demod,13392,demod,14259,14293,14293] (c(x)^ (c(y)^c(z))) v (y v (u v (x v z)))=1.

given clause #858: (wt=11) 14861 [para_from,14601,2,flip.1] (x^y) v (z v y)=z v y.

given clause #859: (wt=11) 14909 [para_from,14869,2,flip.1] x v (y v (x^z))=y v x.

given clause #860: (wt=11) 14949 [para_from,14881,2,flip.1] (x^y) v (z v x)=z v x.

given clause #861: (wt=18) 14406 [back_demod,13390,demod,14259,14293,14293] x v ((c(y)^ (c(x)^c(z))) v (u v (y v z)))=1.

given clause #862: (wt=11) 15302 [para_from,14260,14865,demod,14367,14293,14183] x v ((c(x)^y) v c(y))=1.

given clause #863: (wt=10) 20674 [para_from,15302,19037,demod,14149,14183,flip.1] ((x^y) v c(y))^x=x.

given clause #864: (wt=9) 20720 [back_demod,18945,demod,20713] x^c(y)=c(y)^x.

given clause #865: (wt=18) 14408 [back_demod,13388,demod,14259,14293,14293] x v (y v (z v ((c(x)^ (c(y)^c(u))) v u)))=1.

given clause #866: (wt=7) 20740 [para_into,20720,14182,demod,14183] x^y=y^x.

given clause #867: (wt=10) 20706 [para_into,20674,14280,demod,14293,14183,20391] x v (c(x)^y)=x v y.

given clause #868: (wt=10) 20718 [back_demod,19592,demod,20713] (c(x)^y) v x=x v y.

given clause #869: (wt=18) 14410 [back_demod,13386,demod,14259,14293,14293] x v ((c(x)^ (c(y)^c(z))) v (y v (u v z)))=1.

given clause #870: (wt=10) 20728 [para_from,20674,17772,demod,20675] x^ ((x^y) v c(y))=x.

given clause #871: (wt=10) 20767 [para_into,20740,19324] x^ (y v c(x))=x^y.

given clause #872: (wt=10) 20769 [para_into,20740,19047] x^ (c(x) v y)=x^y.

given clause #873: (wt=18) 14412 [back_demod,13384,demod,14259,14293,14293] (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) 14414 [back_demod,13382,demod,14259,14293,14293] x v (y v (z v ((c(y)^ (c(x)^c(u))) v u)))=1.

given clause #878: (wt=11) 15425 [para_from,14292,14278] (c(x)^c(y))^ (x v y)=0.

given clause #879: (wt=11) 15459 [para_into,14250,14566] (x^c(y)) v (y v c(x))=1.

given clause #880: (wt=11) 15667 [para_into,14282,14566] (x v c(y))^ (y^c(x))=0.

given clause #881: (wt=18) 14416 [back_demod,13380,demod,14259,14293,14293] x v ((c(y)^ (c(x)^c(z))) v (y v (u v z)))=1.

given clause #882: (wt=11) 15808 [para_into,14284,14566] (x^y)^ (c(y) v c(x))=0.

given clause #883: (wt=11) 15922 [para_into,14286,14566] (x^y) v (c(y) v c(x))=1.

given clause #884: (wt=11) 15924 [para_into,14286,2] c(x) v ((x^y) v c(y))=1.

given clause #885: (wt=16) 14418 [back_demod,13354,demod,14259,14293,14293] x v ((c(y)^ (c(x)^c(z))) v (y v z))=1.

given clause #886: (wt=11) 16716 [para_into,14340,14566] (x v y)^ (c(y)^c(x))=0.

given clause #887: (wt=11) 16792 [para_into,14342,14566] (c(x)^y) v (c(y) v x)=1.

given clause #888: (wt=11) 16904 [para_into,14344,14566] (x^c(y))^ (y v c(x))=0.

given clause #889: (wt=16) 14422 [back_demod,13350,demod,14259,14293,14293] x v (y v ((c(y)^ (c(x)^c(z))) v z))=1.

given clause #890: (wt=11) 16912 [para_into,16857,14739] (x^y) v (y v z)=y v z.

given clause #891: (wt=11) 16992 [para_into,14346,14566] (c(x)^y)^ (c(y) v x)=0.

given clause #892: (wt=11) 17190 [para_into,14352,16076,demod,14183,14149,14183] (x^y) v (x v z)=x v z.

given clause #893: (wt=16) 14424 [back_demod,13348,demod,14259,14293,14293] (c(x)^ (c(y)^c(z))) v (y v (x v z))=1.

given clause #894: (wt=11) 17380 [para_into,14360,14566] (c(x) v y)^ (c(y)^x)=0.

given clause #895: (wt=11) 17616 [para_from,14370,14344,demod,14183,14293,14367,14183,14143] x^ ((c(x) v y)^c(y))=0.

given clause #896: (wt=11) 17620 [para_from,14370,14340,demod,14293,14367,14183,14183,14149] c(x)^ ((x v y)^c(y))=0.

given clause #897: (wt=13) 14442 [back_demod,12241,demod,14153,14293,14153] (c(x)^c(y)) v (z v (x v y))=1.

given clause #898: (wt=11) 17782 [para_into,17734,14226] x^ (y v (z v (x v u)))=x.

given clause #899: (wt=11) 17856 [para_into,17784,14881] (x^y)^ (z v x)=x^y.

given clause #900: (wt=11) 17858 [para_into,17784,14601] (x^y)^ (z v y)=x^y.

given clause #901: (wt=16) 14444 [back_demod,9988,demod,14153] (x^ (c(y) v c(z)))^ (c(x) v (y^z))=0.

given clause #902: (wt=11) 17984 [para_into,17864,14881] (x^y)^ (x v z)=x^y.

given clause #903: (wt=11) 17986 [para_into,17864,14601] (x^y)^ (y v z)=x^y.

given clause #904: (wt=11) 18108 [para_into,14430,14566] (c(x)^c(y)) v (y v x)=1.

given clause #905: (wt=16) 14448 [back_demod,9846,demod,14153,14293,14293,14153] (c(x)^ (c(y)^c(z))) v (x v (y v z))=1.

given clause #906: (wt=11) 18128 [para_into,14450,14370,demod,14293,14367,14183,14183,14143] ((x v y)^c(y))^c(x)=0.

given clause #907: (wt=11) 18417 [para_into,14563,14566] (x v y) v z=y v (x v z).

given clause #908: (wt=11) 18940 [back_demod,15342,demod,18571] (x v y)^c(x)=y^c(x).

given clause #909: (wt=16) 14452 [back_demod,2202,demod,14153,14153,14293,14293] (x v (y v z))^ (c(y)^ (c(x)^c(z)))=0.

given clause #910: (wt=11) 18983 [para_from,14563,17784] x^ (y v (z v (u v x)))=x.

given clause #911: (wt=11) 19159 [para_into,19113,99] (x v (y v (z v u)))^z=z.

given clause #912: (wt=11) 19201 [para_into,19151,14869] (x v y)^ (y^z)=y^z.

given clause #913: (wt=16) 14454 [back_demod,2200,demod,14153,14153,14293,14293] (x v (y v z))^ (c(x)^ (c(y)^c(z)))=0.

given clause #914: (wt=11) 19211 [para_into,19151,14146] (x v y)^ (z^y)=z^y.

given clause #915: (wt=11) 19219 [para_into,19163,14563] (x v (y v (z v u)))^u=u.

given clause #916: (wt=11) 19257 [para_into,18989,14182] c(x) v (y^x)=c(x) v y.

given clause #917: (wt=17) 14456 [back_demod,1568,demod,14153,14293,14293,14153,14293,14293] c(x)^ (c(y)^c(z))=c(y)^ (c(x)^c(z)).

given clause #918: (wt=10) 22207 [para_into,19257,20769,demod,14293,14183,14293,14183,14882] (x^c(y)) v (x^y)=x.

given clause #919: (wt=10) 22209 [para_into,19257,20767,demod,14293,14183,14293,14183,14602] (c(x)^y) v (y^x)=y.

given clause #920: (wt=10) 22238 [para_into,22207,14182] (x^y) v (x^c(y))=x.

given clause #921: (wt=15) 14461 [back_demod,14264,demod,14293,14293,14293,14367,14183,14367,14183,14183,14293] 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,14182] (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) 14465 [back_demod,14256,demod,14293,14293,14367,14183,14183,14293] x v ((x v y)^ (c(z)^c(y)))=x.

given clause #926: (wt=10) 22271 [para_into,22209,14566] (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) 19415 [para_into,19037,14562,demod,19038] (x v y)^z= (y v x)^z.

given clause #929: (wt=15) 14469 [back_demod,53,demod,14293] (x v (c(y)^c(z)))^ (y v (x v z))=x.

given clause #930: (wt=11) 20373 [para_into,14599,17514,demod,14147,flip.1] ((x^ (y^z))^u) v z=z.

given clause #931: (wt=11) 20375 [para_into,14599,17390,demod,14147,flip.1] (((x^y)^z)^u) v y=y.

given clause #932: (wt=11) 20377 [para_into,14599,17208,demod,14147,flip.1] (x^ ((y^z)^u)) v z=z.

given clause #933: (wt=16) 14473 [para_from,14182,204] (c(x) v (y^c(z)))^ (x^ (c(y) v z))=0.

given clause #934: (wt=11) 20379 [para_into,14599,16857,demod,14147,flip.1] (x^ (y^ (z^u))) v u=u.

given clause #935: (wt=11) 20494 [para_into,14861,17370,demod,17371] (x^ ((y^z)^u)) v y=y.

given clause #936: (wt=11) 20496 [para_into,14861,17204,demod,17205] (x^ (y^ (z^u))) v z=z.

given clause #937: (wt=16) 14477 [para_from,14182,204] (c(x) v (c(y)^z))^ (x^ (y v c(z)))=0.

given clause #938: (wt=11) 20531 [para_into,14909,17514,demod,14870,flip.1] ((x^ (y^z))^u) v y=y.

given clause #939: (wt=11) 20533 [para_into,14909,17390,demod,14870,flip.1] (((x^y)^z)^u) v x=x.

given clause #940: (wt=11) 20694 [para_into,20674,15623,demod,14293,14183,18990] (x v y)^ (y v x)=y v x.

given clause #941: (wt=16) 14481 [para_from,14182,204] (x v (y^z))^ (c(x)^ (c(y) v c(z)))=0.

given clause #942: (wt=11) 20712 [back_demod,15551,demod,20707] c(x)^ (x v y)=c(x)^y.

given clause #943: (wt=11) 20741 [para_into,20720,19324,demod,14183] 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) 14515 [para_from,14228,97,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,19326,demod,20770] (x v y)^z=z^ (y v x).

given clause #947: (wt=11) 20788 [back_demod,19301,demod,20770] x^ (y v z)= (z v y)^x.

given clause #948: (wt=11) 20814 [para_into,20706,14182] c(x) v (x^y)=c(x) v y.

given clause #949: (wt=13) 14526 [para_from,14228,15,flip.1] x v (y v (z v x))=y v (z v x).

given clause #950: (wt=11) 20994 [para_into,20769,14563,demod,20993] x^ (y v z)=x^ (z v y).

given clause #951: (wt=11) 21072 [para_into,20775,14743,demod,14293,14183,14183,14153] (x^y)^ (y^x)=y^x.

given clause #952: (wt=11) 21464 [para_into,16912,2] x v ((y^x) v z)=x v z.

given clause #953: (wt=15) 14544 [para_from,14258,1131,demod,14259] 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,16912,19113] (x v y)^ (z^x)=z^x.

given clause #956: (wt=11) 21587 [para_into,17190,2] x v ((x^y) v z)=x v z.

given clause #957: (wt=15) 14545 [para_from,14258,1064,demod,14259] 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,17190,19113] (x v y)^ (x^z)=x^z.

given clause #960: (wt=11) 21974 [para_into,18940,14566] (x v y)^c(y)=x^c(y).

given clause #961: (wt=15) 14546 [para_from,14258,1060,demod,14259] x v (y v (z v u))=x v (z v (u v y)).

given clause #962: (wt=11) 22660 [para_into,20373,14566] x v ((y^ (z^x))^u)=x.

given clause #963: (wt=11) 22707 [para_into,20375,14566] x v (((y^x)^z)^u)=x.

given clause #964: (wt=11) 22752 [para_into,20377,14566] x v (y^ ((z^x)^u))=x.

given clause #965: (wt=15) 14547 [para_from,14258,951,demod,14259] x v (y v (z v u))=u v (z v (y v x)).

given clause #966: (wt=11) 22809 [para_into,20379,14566] x v (y^ (z^ (u^x)))=x.

given clause #967: (wt=11) 22840 [para_into,20494,14566] x v (y^ ((x^z)^u))=x.

given clause #968: (wt=11) 22871 [para_into,20496,14566] x v (y^ (z^ (x^u)))=x.

given clause #969: (wt=15) 14548 [para_from,14258,949,demod,14259] x v (y v (z v u))=x v (y v (u v z)).

given clause #970: (wt=11) 22904 [para_into,20531,14566] x v ((y^ (x^z))^u)=x.

given clause #971: (wt=11) 22927 [para_into,20533,14566] x v (((x^y)^z)^u)=x.

given clause #972: (wt=11) 23039 [para_from,20783,19415,demod,20784] (x^y)^z= (y^x)^z.

given clause #973: (wt=15) 14549 [para_from,14258,907,demod,14259] x v (y v (z v u))=z v (u v (y v x)).

given clause #974: (wt=11) 23048 [para_from,20783,14564,demod,23045] x v (y^z)= (z^y) v x.

given clause #975: (wt=11) 23049 [para_from,20783,14562,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) 14550 [para_from,14258,906,demod,14259] 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) 14551 [para_from,14258,905,demod,14259] 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) 14805 [para_into,12513,14566] x v (y v (z v (c(x) v u)))=1.

given clause #984: (wt=12) 14957 [para_into,14318,99] c(x) v (y v (z v (x v u)))=1.

given clause #985: (wt=15) 14552 [para_from,14258,130,demod,14259] x v (y v (z v u))=y v (x v (u v z)).

given clause #986: (wt=12) 17000 [para_into,16736,393,demod,14293,14183,14293,14183] x^ (y^ (z^ (c(x)^u)))=0.

given clause #987: (wt=12) 17010 [para_into,16740,393,demod,14293,14183,14293,14183] x^ ((y^ (c(x)^z))^u)=0.

given clause #988: (wt=12) 17024 [para_into,16949,393,demod,14293,14183,14293,14183] (x^ (y^ (c(z)^u)))^z=0.

given clause #989: (wt=15) 14553 [para_from,14258,127,demod,14259] x v (y v (z v u))=z v (y v (u v x)).

given clause #990: (wt=12) 17112 [para_into,16953,393,demod,14293,14183,14293,14183] ((x^ (c(y)^z))^u)^y=0.

given clause #991: (wt=12) 17352 [para_into,17118,393,demod,14293,14183,14293,14183] (x^ (c(y)^z))^ (u^y)=0.

given clause #992: (wt=12) 17364 [para_into,17124,393,demod,14293,14183,14293,14183] (x^ (c(y)^z))^ (y^u)=0.

given clause #993: (wt=15) 14554 [para_from,14258,122,demod,14259] x v (y v (z v u))=z v (u v (x v y)).

given clause #994: (wt=12) 17628 [para_into,17182,393,demod,14293,14183,14293,14183] (x^y)^ (z^ (c(y)^u))=0.

given clause #995: (wt=12) 17640 [para_into,17308,393,demod,14293,14183,14293,14183] (x^y)^ (z^ (c(x)^u))=0.

given clause #996: (wt=12) 19380 [para_from,19021,17124,demod,14293,14183] (x^c(y))^ ((y^x)^z)=0.

given clause #997: (wt=15) 14555 [para_from,14258,121,demod,14259] x v (y v (z v u))=u v (y v (x v z)).

given clause #998: (wt=12) 19400 [para_from,19021,17308,demod,14293,14183] ((x^y)^z)^ (y^c(x))=0.

given clause #999: (wt=12) 19660 [para_from,19299,17124,demod,14293,14183] (c(x)^y)^ ((x^y)^z)=0.

given clause #1000: (wt=12) 19672 [para_from,19299,17308,demod,14293,14183] ((x^y)^z)^ (c(x)^y)=0.

given clause #1001: (wt=15) 14556 [para_from,14258,109,demod,14259] 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,17118,demod,14293,14183] (c(x)^y)^ (z^ (y^x))=0.

given clause #1005: (wt=15) 14557 [para_from,14258,108,demod,14259] x v (y v (z v u))=z v (x v (u v y)).

given clause #1006: (wt=12) 20965 [para_from,20767,17124,demod,14293,14183] (c(x)^y)^ ((y^x)^z)=0.

given clause #1007: (wt=12) 20969 [para_from,20767,17182,demod,14293,14183] (x^ (y^z))^ (c(z)^y)=0.

given clause #1008: (wt=12) 20979 [para_from,20767,17308,demod,14293,14183] ((x^y)^z)^ (c(y)^x)=0.

given clause #1009: (wt=15) 14558 [para_from,14258,103,demod,14259] x v (y v (z v u))=y v (u v (z v x)).

given clause #1010: (wt=12) 20987 [para_into,20769,14909,demod,20768,flip.1] x^ (y v (c(x)^z))=x^y.

given clause #1011: (wt=12) 20989 [para_into,20769,14599,demod,20768,flip.1] x^ (y v (z^c(x)))=x^y.

given clause #1012: (wt=12) 21032 [para_from,20769,17118,demod,14293,14183] (x^c(y))^ (z^ (x^y))=0.

given clause #1013: (wt=15) 14559 [para_from,14258,102,demod,14259] x v (y v (z v u))=y v (z v (u v x)).

given clause #1014: (wt=12) 21034 [para_from,20769,17124,demod,14293,14183] (x^c(y))^ ((x^y)^z)=0.

given clause #1015: (wt=12) 21036 [para_from,20769,17182,demod,14293,14183] (x^ (y^z))^ (y^c(z))=0.

given clause #1016: (wt=12) 21044 [para_from,20769,17308,demod,14293,14183] ((x^y)^z)^ (x^c(y))=0.

given clause #1017: (wt=15) 14560 [para_from,14258,98,demod,14259] x v (y v (z v u))=u v (x v (z v y)).

given clause #1018: (wt=12) 22462 [para_into,14465,14182] x v ((x v y)^ (z^c(y)))=x.

given clause #1019: (wt=12) 22676 [para_from,20373,20767,demod,32,flip.1] x^ ((y^ (z^c(x)))^u)=0.

given clause #1020: (wt=12) 22721 [para_from,20375,20767,demod,32,flip.1] x^ (((y^c(x))^z)^u)=0.

given clause #1021: (wt=15) 14561 [para_from,14258,97,demod,14259] 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,32,flip.1] x^ (y^ ((z^c(x))^u))=0.

given clause #1023: (wt=12) 22825 [para_from,20379,20767,demod,32,flip.1] x^ (y^ (z^ (u^c(x))))=0.

given clause #1024: (wt=12) 22852 [para_from,20494,20767,demod,32,flip.1] x^ (y^ ((c(x)^z)^u))=0.

given clause #1025: (wt=19) 14588 [para_from,14146,97,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,32,flip.1] x^ (((c(x)^y)^z)^u)=0.

given clause #1027: (wt=12) 22989 [para_into,20741,20533,demod,14279,flip.1] c(x)^ (((x^y)^z)^u)=0.

given clause #1028: (wt=12) 22991 [para_into,20741,20531,demod,14279,flip.1] c(x)^ ((y^ (x^z))^u)=0.

given clause #1029: (wt=15) 14597 [para_from,14146,15,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,14279,flip.1] c(x)^ (y^ (z^ (x^u)))=0.

given clause #1031: (wt=12) 22995 [para_into,20741,20494,demod,14279,flip.1] c(x)^ (y^ ((x^z)^u))=0.

given clause #1032: (wt=12) 22997 [para_into,20741,20379,demod,14279,flip.1] c(x)^ (y^ (z^ (u^x)))=0.

given clause #1033: (wt=15) 14657 [para_from,14566,393] (x v (y^z))^ (c(y) v (c(z) v x))=x.

given clause #1034: (wt=12) 22999 [para_into,20741,20377,demod,14279,flip.1] c(x)^ (y^ ((z^x)^u))=0.

given clause #1035: (wt=12) 23001 [para_into,20741,20375,demod,14279,flip.1] c(x)^ (((y^x)^z)^u)=0.

given clause #1036: (wt=12) 23003 [para_into,20741,20373,demod,14279,flip.1] c(x)^ ((y^ (z^x))^u)=0.

given clause #1037: (wt=19) 14699 [para_from,14566,1131] 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,19037,demod,19038,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) 14700 [para_from,14566,1064] 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,19037,demod,19038,flip.1] ((c(x)^y) v z)^x=z^x.

given clause #1043: (wt=12) 23537 [para_into,21974,20533,demod,32,flip.1] (((x^y)^z)^u)^c(x)=0.

given clause #1044: (wt=12) 23539 [para_into,21974,20531,demod,32,flip.1] ((x^ (y^z))^u)^c(y)=0.

given clause #1045: (wt=19) 14701 [para_from,14566,1060] 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,32,flip.1] (x^ (y^ (z^u)))^c(z)=0.

given clause #1047: (wt=12) 23543 [para_into,21974,20494,demod,32,flip.1] (x^ ((y^z)^u))^c(y)=0.

given clause #1048: (wt=12) 23545 [para_into,21974,20379,demod,32,flip.1] (x^ (y^ (z^u)))^c(u)=0.

given clause #1049: (wt=19) 14702 [para_from,14566,951] 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,32,flip.1] (x^ ((y^z)^u))^c(z)=0.

given clause #1051: (wt=12) 23549 [para_into,21974,20375,demod,32,flip.1] (((x^y)^z)^u)^c(y)=0.

given clause #1052: (wt=12) 23551 [para_into,21974,20373,demod,32,flip.1] ((x^ (y^z))^u)^c(z)=0.

given clause #1053: (wt=19) 14703 [para_from,14566,949] 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,19037,demod,14279,flip.1] ((x^ (y^c(z)))^u)^z=0.

given clause #1055: (wt=12) 23590 [para_from,22707,19037,demod,14279,flip.1] (((x^c(y))^z)^u)^y=0.

given clause #1056: (wt=12) 23599 [para_from,22752,19037,demod,14279,flip.1] (x^ ((y^c(z))^u))^z=0.

given clause #1057: (wt=19) 14704 [para_from,14566,907] 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,19037,demod,14279,flip.1] (x^ (y^ (z^c(u))))^u=0.

given clause #1059: (wt=12) 23643 [para_from,22840,19037,demod,14279,flip.1] (x^ ((c(y)^z)^u))^y=0.

given clause #1060: (wt=12) 23688 [para_from,22927,19037,demod,14279,flip.1] (((c(x)^y)^z)^u)^x=0.

given clause #1061: (wt=19) 14705 [para_from,14566,906] x v (y v (z v (u v v)))=v v (y v (z v (x v u))).

given clause #1062: (wt=12) 24495 [para_into,17352,14182] (x^ (y^z))^ (u^c(y))=0.

given clause #1063: (wt=12) 24501 [para_into,17352,20740] (x^ (y^c(z)))^ (u^z)=0.

given clause #1064: (wt=12) 24503 [para_into,17352,23096] ((x^c(y))^z)^ (u^y)=0.

given clause #1065: (wt=19) 14706 [para_from,14566,905] x v (y v (z v (u v v)))=v v (z v (x v (y v u))).

given clause #1066: (wt=12) 24507 [para_into,17352,20959] ((c(x)^y)^z)^ (u^x)=0.

given clause #1067: (wt=12) 24543 [para_into,17352,23064] (x^y)^ ((c(y)^z)^u)=0.

given clause #1068: (wt=12) 24549 [para_into,17364,14182] (x^ (y^z))^ (c(y)^u)=0.

given clause #1069: (wt=19) 14707 [para_from,14566,130] x v (y v (z v (u v v)))=y v (x v (v v (z v u))).

given clause #1070: (wt=12) 24555 [para_into,17364,20740] (x^ (y^c(z)))^ (z^u)=0.

given clause #1071: (wt=12) 24557 [para_into,17364,23096] ((x^c(y))^z)^ (y^u)=0.

given clause #1072: (wt=12) 24561 [para_into,17364,20959] ((c(x)^y)^z)^ (x^u)=0.

given clause #1073: (wt=19) 14708 [para_from,14566,127] x v (y v (z v (u v v)))=z v (y v (v v (x v u))).

given clause #1074: (wt=12) 24565 [para_into,17364,23064] (x^y)^ ((c(x)^z)^u)=0.

given clause #1075: (wt=12) 24593 [para_into,17628,21974,demod,14183] (x^c(y))^ (z^ (y^u))=0.

given clause #1076: (wt=12) 24633 [para_into,17628,20740] (x^y)^ (z^ (u^c(y)))=0.

given clause #1077: (wt=19) 14709 [para_from,14566,122] x v (y v (z v (u v v)))=z v (v v (x v (y v u))).

given clause #1078: (wt=12) 24635 [para_into,17628,23096] (x^y)^ ((z^c(y))^u)=0.

given clause #1079: (wt=12) 24637 [para_into,17640,20741,demod,14183] (c(x)^y)^ (z^ (x^u))=0.

given clause #1080: (wt=12) 24649 [para_into,17640,20740] (x^y)^ (z^ (u^c(x)))=0.

given clause #1081: (wt=19) 14710 [para_from,14566,121] x v (y v (z v (u v v)))=v v (y v (x v (z v u))).

given clause #1082: (wt=12) 24651 [para_into,17640,23096] (x^y)^ ((z^c(x))^u)=0.

given clause #1083: (wt=12) 24842 [para_into,20777,18570,demod,23439,14367,14183,flip.1] x^ (y^ (x v c(z)))=y^x.

given clause #1084: (wt=11) 26809 [para_into,24842,14182] x^ (y^ (x v z))=y^x.

given clause #1085: (wt=19) 14711 [para_from,14566,109] x v (y v (z v (u v v)))=y v (v v (x v (z v u))).

given clause #1086: (wt=11) 26852 [para_into,26809,14909] x^ (y^ (z v x))=y^x.

given clause #1087: (wt=11) 26870 [para_into,26809,20959,demod,14293,20778] x^ ((x v y)^z)=x^z.

given clause #1088: (wt=11) 26873 [para_into,26809,17786,demod,26810,flip.1] (x^ (y v z))^y=x^y.

given clause #1089: (wt=19) 14712 [para_from,14566,108] x v (y v (z v (u v v)))=z v (x v (v v (y v u))).

given clause #1090: (wt=11) 27027 [para_into,26852,20959,demod,14293,20780] x^ ((y v x)^z)=x^z.

given clause #1091: (wt=11) 27342 [para_into,26873,22271,demod,27179] (x^y)^z=x^ (y^z).

given clause #1092: (wt=11) 27346 [para_into,26873,23064,demod,27343,27343,23404,27343] x^ (y^z)=y^ (x^z).

given clause #1093: (wt=19) 14713 [para_from,14566,103] x v (y v (z v (u v v)))=y v (v v (z v (x v u))).

given clause #1094: (wt=11) 27351 [back_demod,24290,demod,27343,27343,27343,27343,19122,19124,19120] x^ (y^z)=z^ (y^x).

given clause #1095: (wt=11) 27449 [back_demod,26886,demod,27343,19122] x^ (y^z)=z^ (x^y).

given clause #1096: (wt=11) 27453 [back_demod,26841,demod,27343,19122] x^ (y^z)=y^ (z^x).

given clause #1097: (wt=19) 14714 [para_from,14566,102] x v (y v (z v (u v v)))=y v (z v (v v (x v u))).

given clause #1098: (wt=12) 25351 [para_into,22462,14566] x v ((y v x)^ (z^c(y)))=x.

given clause #1099: (wt=12) 25371 [para_into,22462,14182] x v ((x v c(y))^ (z^y))=x.

given clause #1100: (wt=12) 26939 [para_from,26809,20718,demod,18571,flip.1] x v (y^ (c(x) v z))=x v y.

given clause #1101: (wt=19) 14715 [para_from,14566,98] x v (y v (z v (u v v)))=v v (x v (z v (y v u))).

given clause #1102: (wt=12) 27033 [para_into,26852,14657,demod,19088,flip.1] (x v (y^z))^ (c(z) v x)=x.

given clause #1103: (wt=12) 27041 [para_into,26852,14348,demod,19114,flip.1] (x v (y^c(z)))^ (x v z)=x.

given clause #1104: (wt=12) 27043 [para_into,26852,393,demod,19114,flip.1] (x v (y^z))^ (x v c(z))=x.

given clause #1105: (wt=19) 14716 [para_from,14566,97] x v (y v (z v (u v v)))=v v (x v (y v (z v u))).

given clause #1106: (wt=12) 27097 [para_from,26852,20718,demod,18571,flip.1] x v (y^ (z v c(x)))=x v y.

given clause #1107: (wt=12) 27265 [para_from,26870,20718,demod,20719,flip.1] x v ((c(x) v y)^z)=x v z.

given clause #1108: (wt=12) 28006 [para_from,27027,20718,demod,20719,flip.1] x v ((y v c(x))^z)=x v z.

given clause #1109: (wt=15) 14719 [para_from,14566,393] ((x^y) v z)^ (c(x) v (z v c(y)))=z.

given clause #1110: (wt=12) 28594 [para_into,26939,23048] ((c(x) v y)^z) v x=x v z.

given clause #1111: (wt=12) 28596 [para_into,26939,14566] (x^ (c(y) v z)) v y=y v x.

given clause #1112: (wt=12) 28626 [para_into,27033,27033,demod,14293,14183] (x v y)^ ((z^c(y)) v x)=x.

given clause #1113: (wt=15) 14721 [para_from,14566,43] ((x^y) v z)^ (z v (c(x) v c(y)))=z.

given clause #1114: (wt=12) 28642 [para_into,27033,21974,demod,14183] (x v (y^c(z)))^ (z v x)=x.

given clause #1115: (wt=12) 28650 [para_into,27033,20959] (x v (y^z))^ (c(y) v x)=x.

given clause #1116: (wt=12) 28668 [para_into,27033,15334,demod,14293,14183] (x v y)^ ((c(y)^z) v x)=x.

given clause #1117: (wt=15) 14727 [para_from,14566,43] (x v (y^z))^ (x v (c(z) v c(y)))=x.

given clause #1118: (wt=12) 28682 [para_into,27033,23048] ((x^y) v z)^ (c(x) v z)=z.

given clause #1119: (wt=12) 28686 [para_into,27033,14566] ((x^y) v z)^ (c(y) v z)=z.

given clause #1120: (wt=12) 28708 [para_into,27033,20788] (x v c(y))^ (x v (z^y))=x.

given clause #1121: (wt=15) 14737 [para_from,14566,14] (C^ (A v B)) v A!=A v (B^ (A v C))|$Ans(MOD).

given clause #1122: (wt=12) 28710 [para_into,27033,20786] (c(x) v y)^ ((z^x) v y)=y.

given clause #1123: (wt=12) 28712 [para_into,27033,20740] (c(x) v y)^ (y v (z^x))=y.

given clause #1124: (wt=12) 28731 [para_into,27041,20959] (x v (c(y)^z))^ (x v y)=x.

given clause #1125: (wt=15) 14738 [para_from,14566,14] A v (C^ (B v A))!=A v (B^ (A v C))|$Ans(MOD).

given clause #1126: (wt=12) 28737 [para_into,27041,23048] ((c(x)^y) v z)^ (z v x)=z.

given clause #1127: (wt=12) 28741 [para_into,27041,14566] ((x^c(y)) v z)^ (z v y)=z.

given clause #1128: (wt=12) 28787 [para_into,27041,20788] (x v y)^ (y v (z^c(x)))=y.

given clause #1129: (wt=19) 14783 [copy,14699,flip.1] x v (y v (z v (u v v)))=x v (u v (z v (v v y))).

given clause #1130: (wt=12) 28789 [para_into,27041,20740] (x v y)^ (x v (z^c(y)))=x.

given clause #1131: (wt=12) 28812 [para_into,27043,27043,demod,14293,14183] (x v y)^ (x v (c(y)^z))=x.

given clause #1132: (wt=12) 28834 [para_into,27043,20959] (x v (y^z))^ (x v c(y))=x.

given clause #1133: (wt=19) 14784 [copy,14700,flip.1] x v (y v (z v (u v v)))=x v (z v (u v (v v y))).

given clause #1134: (wt=12) 28860 [para_into,27043,23048] ((x^y) v z)^ (z v c(x))=z.

given clause #1135: (wt=12) 28862 [para_into,27043,14566] ((x^y) v z)^ (z v c(y))=z.

given clause #1136: (wt=12) 28868 [para_into,27043,20786] (x v c(y))^ ((z^y) v x)=x.

given clause #1137: (wt=19) 14785 [copy,14701,flip.1] x v (y v (z v (u v v)))=x v (u v (y v (v v z))).

given clause #1138: (wt=12) 28889 [para_into,27097,23048] ((x v c(y))^z) v y=y v z.

given clause #1139: (wt=12) 28891 [para_into,27097,14566] (x^ (y v c(z))) v z=z v x.

given clause #1140: (wt=12) 29117 [para_into,28626,14566] (x v y)^ ((z^c(x)) v y)=y.

given clause #1141: (wt=19) 14786 [copy,14702,flip.1] x v (y v (z v (u v v)))=u v (z v (y v (v v x))).

given clause #1142: (wt=12) 29151 [para_into,28626,20786] ((x^c(y)) v z)^ (y v z)=z.

given clause #1143: (wt=12) 29172 [para_into,28642,20959] (x v (c(y)^z))^ (y v x)=x.

given clause #1144: (wt=12) 29176 [para_into,28642,23048] ((c(x)^y) v z)^ (x v z)=z.

given clause #1145: (wt=19) 14787 [copy,14703,flip.1] x v (y v (z v (u v v)))=x v (y v (u v (v v z))).

given clause #1146: (wt=12) 29247 [para_into,28650,20788] (x v c(y))^ (x v (y^z))=x.

given clause #1147: (wt=12) 29249 [para_into,28650,20786] (c(x) v y)^ ((x^z) v y)=y.

given clause #1148: (wt=12) 29251 [para_into,28650,20740] (c(x) v y)^ (y v (x^z))=y.

given clause #1149: (wt=19) 14788 [copy,14704,flip.1] x v (y v (z v (u v v)))=u v (z v (x v (v v y))).

given clause #1150: (wt=12) 29306 [para_into,28668,14909,demod,14293,14367,27343,29034] (x v y)^ (y v (c(x)^z))=y.

given clause #1151: (wt=12) 29310 [para_into,28668,14566] (x v y)^ ((c(x)^z) v y)=y.

given clause #1152: (wt=12) 29328 [para_into,28668,14182] (x v c(y))^ ((y^z) v x)=x.

given clause #1153: (wt=19) 14789 [copy,14705,flip.1] x v (y v (z v (u v v)))=u v (y v (z v (v v x))).

given clause #1154: (wt=13) 14831 [para_into,14601,2] x v ((y^ (x v z)) v z)=x v z.

given clause #1155: (wt=13) 14919 [para_into,14881,2] x v (((x v y)^z) v y)=x v y.

given clause #1156: (wt=13) 15021 [back_demod,14521,demod,15018] x v (y v (x v z))=y v (x v z).

given clause #1157: (wt=19) 14790 [copy,14706,flip.1] x v (y v (z v (u v v)))=z v (u v (y v (v v x))).

given clause #1158: (wt=13) 15417 [para_from,14292,15173] (x v y)^ (z^ (c(x)^c(y)))=0.

given clause #1159: (wt=13) 15537 [para_from,14250,2,demod,12036,flip.1] (x^c(y)) v (z v (c(x) v y))=1.

given clause #1160: (wt=13) 15707 [para_from,14366,15177] (c(x) v c(y))^ (z^ (x^y))=0.

given clause #1161: (wt=19) 14791 [copy,14707,flip.1] x v (y v (z v (u v v)))=y v (x v (u v (v v z))).

given clause #1162: (wt=13) 16100 [para_into,14298,14182] (c(x)^y) v (z v (x v c(y)))=1.

given clause #1163: (wt=13) 16106 [para_into,14298,14566] (x^y) v (z v (c(y) v c(x)))=1.

given clause #1164: (wt=13) 16894 [para_from,16853,2,flip.1] x v (y v (z^ (u^x)))=y v x.

given clause #1165: (wt=19) 14792 [copy,14708,flip.1] x v (y v (z v (u v v)))=u v (y v (x v (v v z))).

given clause #1166: (wt=13) 16937 [para_from,16857,14330,demod,14529,16858] (x^ (y^z)) v (u v z)=u v z.

given clause #1167: (wt=13) 17243 [para_from,17204,2,flip.1] x v (y v (z^ (x^u)))=y v x.

given clause #1168: (wt=13) 17266 [para_from,17208,14330,demod,14529,17209] (x^ (y^z)) v (u v y)=u v y.

given clause #1169: (wt=19) 14793 [copy,14709,flip.1] x v (y v (z v (u v v)))=z v (u v (x v (v v y))).

given clause #1170: (wt=13) 17796 [para_into,17734,2] (x v y)^ (x v (z v y))=x v y.

given clause #1171: (wt=13) 17806 [para_into,17774,951] x^ (y v (z v (u v (x v v))))=x.

given clause #1172: (wt=13) 18171 [para_into,14562,14881,flip.1] ((x v y)^z) v (y v x)=x v y.

given clause #1173: (wt=19) 14794 [copy,14710,flip.1] x v (y v (z v (u v v)))=z v (y v (u v (v v x))).

given clause #1174: (wt=13) 18175 [para_into,14562,14601,flip.1] (x^ (y v z)) v (z v y)=y v z.

given clause #1175: (wt=13) 18194 [para_from,14562,17734] (x v y)^ (z v (y v x))=x v y.

given clause #1176: (wt=13) 18207 [para_from,14562,14296,demod,14293] (c(x)^c(y)) v (z v (y v x))=1.

given clause #1177: (wt=19) 14795 [copy,14711,flip.1] x v (y v (z v (u v v)))=z v (x v (u v (v v y))).

given clause #1178: (wt=13) 18411 [para_into,14563,14881,flip.1] x v (y v ((y v x)^z))=y v x.

given clause #1179: (wt=13) 18415 [para_into,14563,14601,flip.1] x v (y v (z^ (y v x)))=y v x.

given clause #1180: (wt=13) 18433 [para_into,14563,14298,demod,18418,flip.1] c(x) v (c(y) v (z v (y^x)))=1.

given clause #1181: (wt=19) 14796 [copy,14712,flip.1] x v (y v (z v (u v v)))=y v (u v (x v (v v z))).

given clause #1182: (wt=13) 18850 [back_demod,14873,demod,18418] c(x) v (c(y) v (z v (x^y)))=1.

given clause #1183: (wt=13) 18950 [para_from,14563,17734] (x v y)^ (y v (x v z))=x v y.

given clause #1184: (wt=13) 19053 [back_demod,18524,demod,19038] x v (y v ((x v y)^z))=y v x.

given clause #1185: (wt=19) 14797 [copy,14713,flip.1] x v (y v (z v (u v v)))=u v (x v (z v (v v y))).

given clause #1186: (wt=13) 19119 [para_into,19087,17204] x^ (y^ (x^z))=y^ (x^z).

given clause #1187: (wt=13) 19121 [para_into,19087,16853] x^ (y^ (z^x))=y^ (z^x).

given clause #1188: (wt=13) 19125 [para_into,19087,14563] (x v (y v z))^ (y v x)=y v x.

given clause #1189: (wt=19) 14798 [copy,14714,flip.1] x v (y v (z v (u v v)))=u v (x v (y v (v v z))).

given clause #1190: (wt=13) 19127 [para_into,19087,14562] (x v (y v z))^ (z v y)=z v y.

given clause #1191: (wt=13) 19143 [para_into,19087,2] (x v (y v z))^ (x v z)=x v z.

given clause #1192: (wt=13) 19153 [para_into,19113,951] (x v (y v (z v (u v v))))^u=u.

given clause #1193: (wt=19) 14799 [copy,14715,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (v v x))).

given clause #1194: (wt=13) 19316 [para_into,19021,13280,demod,14143,14183,flip.1] (x v (y v (z v (u v v))))^v=v.

given clause #1195: (wt=13) 20150 [para_into,14564,14601,flip.1] x v (y v (z^ (x v y)))=x v y.

given clause #1196: (wt=13) 20180 [para_from,14564,17734] (x v y)^ (x v (y v z))=x v y.

given clause #1197: (wt=19) 14800 [copy,14716,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (v v x))).

given clause #1198: (wt=13) 20207 [para_from,14564,19087] (x v (y v z))^ (x v y)=x v y.

given clause #1199: (wt=13) 20226 [back_demod,18724,demod,20193] x v (((y v x)^z) v y)=x v y.

given clause #1200: (wt=13) 20280 [para_into,14565,14601,flip.1] x v ((y^ (z v x)) v z)=z v x.

given clause #1201: (wt=16) 14813 [para_from,12513,907,demod,12036,12036,flip.1] x v (y v (z v (u v (v v (w v c(x))))))=1.

given clause #1202: (wt=13) 20308 [para_from,14565,17734] (x v y)^ (y v (z v x))=x v y.

given clause #1203: (wt=13) 20343 [para_from,14565,19087] (x v (y v z))^ (z v x)=z v x.

given clause #1204: (wt=13) 20523 [para_from,14861,19163] (x v (y v z))^ (u^z)=u^z.

given clause #1205: (wt=18) 14815 [para_from,12513,951,demod,12036,12036,12036,flip.1] x v (y v (z v (u v (v v (w v (v6 v c(x)))))))=1.

given clause #1206: (wt=13) 20629 [para_from,14949,19163] (x v (y v z))^ (z^u)=z^u.

given clause #1207: (wt=13) 21015 [para_into,20769,13280,demod,14143,14183,flip.1] x^ (y v (z v (u v (v v x))))=x.

given clause #1208: (wt=13) 21194 [para_from,15459,2,demod,12036,flip.1] (x^c(y)) v (z v (y v c(x)))=1.

given clause #1209: (wt=19) 14823 [para_into,14601,123] (x^ (y v (z v u))) v (z v (y v u))=y v (z v u).

given clause #1210: (wt=13) 21268 [para_from,15922,14348,demod,14293,14183,14183,12036,14143] (x^y) v (z^ (y^x))=x^y.

given clause #1211: (wt=13) 21412 [para_from,16792,2,demod,12036,flip.1] (c(x)^y) v (z v (c(y) v x))=1.

given clause #1212: (wt=13) 21440 [para_into,16912,16912,demod,16913] (x^ (y^z)) v (z v u)=z v u.

given clause #1213: (wt=19) 14825 [para_into,14601,99] x v (y v ((z^ (y v (x v u))) v u))=y v (x v u).

given clause #1214: (wt=13) 21517 [para_from,16912,19163] (x v (y v z))^ (u^y)=u^y.

given clause #1215: (wt=13) 21642 [para_from,17190,16912,demod,17191] (x^ (y^z)) v (y v u)=y v u.

given clause #1216: (wt=13) 21644 [para_from,17190,19163] (x v (y v z))^ (y^u)=y^u.

given clause #1217: (wt=19) 14827 [para_into,14601,16] x v (y v ((z^ (x v (y v u))) v u))=x v (y v u).

given clause #1218: (wt=13) 21942 [para_into,18417,17208,flip.1] x v ((y^ (x^z)) v u)=x v u.

given clause #1219: (wt=13) 21944 [para_into,18417,16857,flip.1] x v ((y^ (z^x)) v u)=x v u.

given clause #1220: (wt=13) 21985 [back_demod,21972,demod,21975] (x v (y^z))^c(z)=x^c(z).

given clause #1221: (wt=19) 14829 [para_into,14601,15] x v ((y^ (z v (x v u))) v (z v u))=z v (x v u).

given clause #1222: (wt=13) 21987 [back_demod,21970,demod,21975] (x v (y^z))^c(y)=x^c(y).

given clause #1223: (wt=13) 22821 [para_from,20379,14909,demod,14870,flip.1] (x^ (y^ (z^ (u^v)))) v u=u.

given clause #1224: (wt=13) 22823 [para_from,20379,14599,demod,14147,flip.1] (x^ (y^ (z^ (u^v)))) v v=v.

given clause #1225: (wt=19) 14846 [para_from,14601,97,flip.1] (x^y) v (z v (u v (v v y)))=z v (u v (v v y)).

given clause #1226: (wt=13) 22972 [para_into,20712,14909,demod,20742,flip.1] c(x)^ (y v (x^z))=c(x)^y.

given clause #1227: (wt=13) 22974 [para_into,20712,14599,demod,20742,flip.1] c(x)^ (y v (z^x))=c(x)^y.

given clause #1228: (wt=13) 23031 [para_from,20783,14861,demod,20784] (x^ (y^z)) v (z^y)=z^y.

given clause #1229: (wt=17) 14848 [para_from,14601,99] x v (y v z)=y v ((u^ (y v z)) v (x v z)).

given clause #1230: (wt=13) 23050 [para_from,20783,19151] (x v (y^z))^ (z^y)=z^y.

given clause #1231: (wt=13) 23253 [para_from,21072,16266,demod,14367] (c(x) v c(y))^ (z^ (y^x))=0.

given clause #1232: (wt=13) 23331 [para_from,21464,20712,demod,20713,flip.1] c(x)^ ((y^x) v z)=c(x)^z.

given clause #1233: (wt=15) 14855 [para_from,14601,15,flip.1] (x^y) v (z v (u v y))=z v (u v y).

given clause #1234: (wt=13) 23339 [para_from,21464,18940,demod,18941,flip.1] ((x^y) v z)^c(y)=z^c(y).

given clause #1235: (wt=13) 23452 [para_from,21587,20712,demod,20713,flip.1] c(x)^ ((x^y) v z)=c(x)^z.

given clause #1236: (wt=13) 23460 [para_from,21587,18940,demod,18941,flip.1] ((x^y) v z)^c(x)=z^c(x).

given clause #1237: (wt=14) 14867 [para_from,14296,951,demod,12036,12036,12036,flip.1] c(x) v (y v (z v (u v (v v x))))=1.

given clause #1238: (wt=13) 23535 [para_into,21638,21072,demod,21073] ((x^y) v z)^ (y^x)=y^x.

given clause #1239: (wt=13) 23628 [para_from,22809,21464,demod,14147,flip.1] x v (y^ (z^ (u^ (v^x))))=x.

given clause #1240: (wt=13) 23630 [para_from,22809,21587,demod,14870,flip.1] x v (y^ (z^ (u^ (x^v))))=x.

given clause #1241: (wt=19) 14898 [para_from,14869,97,flip.1] x v (y v (z v (u v (x^v))))=y v (z v (u v x)).

given clause #1242: (wt=13) 26861 [para_into,26809,14597] x^ (y^ (z v (u v x)))=y^x.

given clause #1243: (wt=13) 26865 [para_into,26809,14565] x^ (y^ (z v (x v u)))=y^x.

given clause #1244: (wt=13) 26983 [para_from,26809,21468,demod,21594,flip.1] (x^ (y v z)) v c(y)=x v c(y).

given clause #1245: (wt=15) 14907 [para_from,14869,15,flip.1] x v (y v (z v (x^u)))=y v (z v x).

given clause #1246: (wt=13) 26985 [para_from,26809,20814,demod,19258,flip.1] c(x) v (y^ (x v z))=c(x) v y.

given clause #1247: (wt=13) 27141 [para_from,26852,21468,demod,21594,flip.1] (x^ (y v z)) v c(z)=x v c(z).

given clause #1248: (wt=13) 27143 [para_from,26852,20814,demod,19258,flip.1] c(x) v (y^ (z v x))=c(x) v y.

given clause #1249: (wt=19) 14911 [para_into,14881,123] ((x v (y v z))^u) v (y v (x v z))=x v (y v z).

given clause #1250: (wt=13) 27214 [para_into,26870,14597] x^ ((y v (z v x))^u)=x^u.

given clause #1251: (wt=13) 27218 [para_into,26870,14565] x^ ((y v (x v z))^u)=x^u.

given clause #1252: (wt=13) 27309 [para_from,26870,21468,demod,21469,flip.1] ((x v y)^z) v c(x)=z v c(x).

given clause #1253: (wt=19) 14913 [para_into,14881,99] x v (y v (((y v (x v z))^u) v z))=y v (x v z).

given clause #1254: (wt=13) 27311 [para_from,26870,20814,demod,20815,flip.1] c(x) v ((x v y)^z)=c(x) v z.

given clause #1255: (wt=13) 27777 [back_demod,23273,demod,27343] (x^y) v (y^ (x^z))=x^y.

given clause #1256: (wt=13) 27783 [back_demod,23265,demod,27343] x^ (y^ ((y^x) v z))=x^y.

given clause #1257: (wt=19) 14915 [para_into,14881,16] x v (y v (((x v (y v z))^u) v z))=x v (y v z).

given clause #1258: (wt=13) 27813 [back_demod,23025,demod,27343] (x^ (y^z)) v (y^x)=y^x.

given clause #1259: (wt=13) 27958 [back_demod,25323,demod,27575] (x^y) v (x^ (z^y))=x^y.

given clause #1260: (wt=13) 27960 [back_demod,25321,demod,27575] (x^y) v (y^ (z^x))=x^y.

given clause #1261: (wt=19) 14917 [para_into,14881,15] x v (((y v (x v z))^u) v (y v z))=y v (x v z).

given clause #1262: (wt=13) 28022 [para_from,27027,21468,demod,21469,flip.1] ((x v y)^z) v c(y)=z v c(y).

given clause #1263: (wt=13) 28024 [para_from,27027,20814,demod,20815,flip.1] c(x) v ((y v x)^z)=c(x) v z.

given clause #1264: (wt=13) 28128 [para_into,27342,17774,flip.1] x^ (y^ ((x^y) v z))=x^y.

given clause #1265: (wt=19) 14934 [para_from,14881,97,flip.1] (x^y) v (z v (u v (v v x)))=z v (u v (v v x)).

given clause #1266: (wt=13) 28200 [para_from,27342,14881] (x^ (y^z)) v (x^y)=x^y.

given clause #1267: (wt=13) 28202 [para_from,27342,14869] (x^y) v (x^ (y^z))=x^y.

given clause #1268: (wt=13) 28349 [para_from,27346,14601] (x^ (y^z)) v (x^z)=x^z.

given clause #1269: (wt=17) 14936 [para_from,14881,99] x v (y v z)=y v (((y v z)^u) v (x v z)).

given clause #1270: (wt=13) 28469 [para_from,27449,14601] (x^ (y^z)) v (z^x)=z^x.

given clause #1271: (wt=13) 30648 [para_from,14831,14294,demod,18418,26984,23304,flip.1] (x^ (y v z)) v z= (x^y) v z.

----> UNIT CONFLICT at  21.11 sec ----> 33670 [binary,33669,23056] $Ans(MOD).

Length of proof is 453.  Level of proof is 77.

---------------- 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 v (B^ (A v C))!=A v (C^ (A v B))|$Ans(MOD).
14 [copy,13,flip.1] A v (C^ (A v B))!=A v (B^ (A v C))|$Ans(MOD).
15 [para_into,2,2] x v (y v (z v u))=z v (x v (y v u)).
16 [copy,15,flip.1] x v (y v (z v u))=y v (z v (x v u)).
18,17 [para_into,9,11] 1 v 0=1.
19 [para_from,9,2,flip.1] x v (y v c(x))=y v 1.
21 [para_from,17,2] x v 1=1 v (x v 0).
22 [copy,21,flip.1] 1 v (x v 0)=x v 1.
23 [para_into,4,11] c(0 v c(x))=1^x.
25 [para_into,4,4] c((x^y) v c(z))= (c(x) v c(y))^z.
28,27 [para_into,4,11] c(c(x) v 0)=x^1.
30,29 [para_into,4,4] c(c(x) v (y^z))=x^ (c(y) v c(z)).
31 [para_into,4,9,demod,12,flip.1] x^c(x)=0.
33 [para_from,4,9] (c(x) v c(y)) v (x^y)=1.
35 [para_into,31,11] 1^0=0.
37 [para_into,31,4] (c(x) v c(y))^ (x^y)=0.
39 [para_from,21,2] x v (1 v (y v 0))=y v (x v 1).
40 [copy,39,flip.1] x v (y v 1)=y v (1 v (x v 0)).
42,41 [para_into,7,11] (x v 0)^ (x v 1)=x.
43 [para_into,7,4] (x v (y^z))^ (x v (c(y) v c(z)))=x.
46,45 [para_into,7,9] 1^ (x v x)=x.
47 [para_into,7,21,demod,12] (x v 0)^ (1 v (x v 0))=x.
49 [para_into,7,17] (1 v c(0))^1=1.
51 [para_into,7,9] (x v c(c(x)))^1=x.
53 [para_into,7,2] (x v c(y v z))^ (y v (x v z))=x.
56,55 [para_into,45,2] 1^ (x v ((x v y) v y))=x v y.
59 [para_from,22,2] x v (y v 1)=1 v (x v (y v 0)).
60 [copy,59,flip.1] 1 v (x v (y v 0))=x v (y v 1).
64,63 [para_into,23,11] c(0 v 0)=1^1.
65 [para_into,23,4] c(0 v (x^y))=1^ (c(x) v c(y)).
67 [para_from,23,7] (x v (1^y))^ (x v (0 v c(y)))=x.
71 [para_from,23,9] (0 v c(x)) v (1^x)=1.
73 [para_from,63,7] (x v (1^1))^ (x v (0 v 0))=x.
86,85 [para_into,27,4] c((x^y) v 0)= (c(x) v c(y))^1.
91 [para_from,27,9] (c(x) v 0) v (x^1)=1.
95 [para_into,15,9,flip.1] x v (y v (z v c(x)))=y v (z v 1).
99 [para_into,15,2] x v (y v (z v u))=z v (y v (x v u)).
106 [para_from,15,7] (x v c(y v (z v u)))^ (z v (x v (y v u)))=x.
128 [para_from,16,45] 1^ (x v (y v ((x v (y v z)) v z)))=x v (y v z).
131 [para_from,16,7] (x v c(y v (z v u)))^ (y v (z v (x v u)))=x.
138 [para_into,19,27] (c(x) v 0) v (y v (x^1))=y v 1.
142 [para_into,19,4] (c(x) v c(y)) v (z v (x^y))=z v 1.
162,161 [para_into,25,41] c(x v c(y))= (c(x v 0) v c(x v 1))^y.
164,163 [para_into,25,35,demod,162,64,12,10] ((1^1) v c(0 v 1))^x=1^x.
175 [para_into,71,63,demod,46] (0 v (1^1)) v 0=1.
179 [para_into,71,45] (0 v c(x v x)) v x=1.
183 [para_from,175,41] 1^ ((0 v (1^1)) v 1)=0 v (1^1).
186,185 [para_from,175,22,flip.1] (0 v (1^1)) v 1=1 v 1.
192 [back_demod,183,demod,186,46,flip.1] 0 v (1^1)=1.
197,196 [para_into,29,27] c((x^1) v (y^z))= (c(x) v 0)^ (c(y) v c(z)).
198 [para_into,29,49,demod,162,18,12,12] c(c(x) v 1)=x^ (((0 v c(1 v 1))^0) v 0).
200 [para_into,29,45,demod,12] c(c(x) v y)=x^ (0 v c(y v y)).
201 [para_into,29,41] c(c(x) v y)=x^ (c(y v 0) v c(y v 1)).
202 [copy,200,flip.1] x^ (0 v c(y v y))=c(c(x) v y).
203 [copy,201,flip.1] x^ (c(y v 0) v c(y v 1))=c(c(x) v y).
206 [para_from,29,9] (c(x) v (y^z)) v (x^ (c(y) v c(z)))=1.
211 [para_from,192,7] (0 v c(1^1))^1=0.
213 [para_from,192,2,flip.1] 0 v (x v (1^1))=x v 1.
227 [para_into,91,51,demod,162] (((c(x v 0) v c(x v 1))^c(x)) v 0) v x=1.
235 [para_into,33,27] ((x^1) v c(y)) v ((c(x) v 0)^y)=1.
241 [para_into,33,41] (c(x v 0) v c(x v 1)) v x=1.
251 [para_into,179,2] x v ((0 v c((x v y) v (x v y))) v y)=1.
256 [para_from,179,15] x v (y v 1)= (0 v c(z v z)) v (x v (y v z)).
259 [para_from,179,2] x v 1= (0 v c(y v y)) v (x v y).
261 [copy,256,flip.1] (0 v c(x v x)) v (y v (z v x))=y v (z v 1).
264,263 [para_from,211,91,demod,162,64,164] ((1^ (1^1)) v 0) v 0=1.
279 [para_from,47,29] c(c(x) v y)=x^ (c(y v 0) v c(1 v (y v 0))).
288,287 [para_into,213,91,demod,12,flip.1] (0 v 0) v 1=0 v 1.
307 [para_from,39,7] (x v c(1 v (y v 0)))^ (y v (x v 1))=x.
313,312 [para_from,263,47,demod,264,46,flip.1] (1^ (1^1)) v 0=1.
315 [para_from,312,47,demod,313,46,flip.1] 1^ (1^1)=1.
323 [para_into,40,2] x v (y v 1)=x v (1 v (y v 0)).
326 [copy,323,flip.1] x v (1 v (y v 0))=x v (y v 1).
335 [para_from,40,7] (x v c(y v 1))^ (y v (1 v (x v 0)))=x.
377 [para_into,43,45,demod,12] (x v y)^ (x v (0 v c(y v y)))=x.
381 [para_into,43,192,demod,12,12] 1^ (0 v (0 v 0))=0.
389 [para_into,43,27] (x v (y^ (c(z) v 0)))^ (x v (c(y) v (z^1)))=x.
391 [para_into,43,19] (x v (y^x))^ (c(y) v 1)=x.
393 [para_into,43,2] (x v (y^z))^ (c(y) v (x v c(z)))=x.
400,399 [para_from,381,71] (0 v c(0 v (0 v 0))) v 0=1.
423 [para_into,53,63] (x v (1^1))^ (0 v (x v 0))=x.
425 [para_into,53,27] (x v (y^1))^ (c(y) v (x v 0))=x.
441 [para_into,53,179] (x v c((0 v c((x v y) v (x v y))) v y))^1=x.
445 [para_into,53,39] (1 v c(x v (y v 0)))^ (y v (x v 1))=1.
449 [para_into,53,15] (x v c(y v (z v u)))^ (z v (y v (x v u)))=x.
467 [para_into,391,45,demod,12] ((x v x) v x)^ (0 v 1)=x v x.
501 [para_into,55,15] 1^ (x v (y v ((y v (x v z)) v z)))=y v (x v z).
506 [para_from,399,47,demod,400,46,flip.1] 0 v c(0 v (0 v 0))=1.
521 [para_from,506,2,flip.1] 0 v (x v c(0 v (0 v 0)))=x v 1.
562,561 [para_into,60,179,flip.1] (0 v c((x v 0) v (x v 0))) v (x v 1)=1 v 1.
581 [para_into,65,47,flip.1] 1^ (c(x v 0) v c(1 v (x v 0)))=c(0 v x).
583 [para_into,65,45,demod,12] c(0 v x)=1^ (0 v c(x v x)).
585 [copy,583,flip.1] 1^ (0 v c(x v x))=c(0 v x).
619 [para_into,67,2] (x v (1^y))^ (0 v (x v c(y)))=x.
632,631 [para_into,241,63] ((1^1) v c(0 v 1)) v 0=1.
644 [para_from,241,47,demod,64,632,46,64,flip.1] (1^1) v c(0 v 1)=1.
659 [para_into,85,45,demod,12] c(x v 0)= (0 v c(x v x))^1.
663 [copy,659,flip.1] (0 v c(x v x))^1=c(x v 0).
666 [para_from,85,53] (x v ((c(y) v c(z))^1))^ ((y^z) v (x v 0))=x.
670 [para_from,85,31] ((x^y) v 0)^ ((c(x) v c(y))^1)=0.
684 [para_into,644,21] (1^1) v c(1 v (0 v 0))=1.
686 [para_from,644,53] 1^ (0 v ((1^1) v 1))=1^1.
689,688 [para_from,644,19,flip.1] (1^1) v 1= (0 v 1) v 1.
704,703 [back_demod,686,demod,689,56,flip.1] 1^1=0 v 1.
711 [back_demod,684,demod,704] (0 v 1) v c(1 v (0 v 0))=1.
733 [back_demod,423,demod,704] (x v (0 v 1))^ (0 v (x v 0))=x.
756,755 [back_demod,315,demod,704] 1^ (0 v 1)=1.
773 [back_demod,213,demod,704] 0 v (x v (0 v 1))=x v 1.
779 [back_demod,192,demod,704] 0 v (0 v 1)=1.
789 [back_demod,73,demod,704] (x v (0 v 1))^ (x v (0 v 0))=x.
792,791 [back_demod,63,demod,704] c(0 v 0)=0 v 1.
793 [para_from,703,391,demod,12] (1 v (0 v 1))^ (0 v 1)=1.
795 [para_from,703,29,demod,12,12] c(c(x) v (0 v 1))=x^ (0 v 0).
807 [para_into,779,21] 0 v (1 v (0 v 0))=1.
812,811 [para_from,779,16,flip.1] 0 v (0 v (x v 1))=x v 1.
815 [para_from,791,29] c((0 v 1) v (x^y))= (0 v 0)^ (c(x) v c(y)).
841 [para_from,807,16,flip.1] 0 v (1 v (x v (0 v 0)))=x v 1.
861 [para_into,773,40] 0 v (0 v (1 v (x v 0)))=x v 1.
863 [copy,861,flip.1] x v 1=0 v (0 v (1 v (x v 0))).
867,866 [para_into,793,40,demod,18] (0 v (1 v 1))^ (0 v 1)=1.
926,925 [para_from,711,19] (1 v (0 v 0)) v 1= (0 v 1) v 1.
1074,1073 [para_into,583,2,flip.1] 1^ (0 v c((x v y) v (x v y)))=c(x v (0 v y)).
1188 [para_into,733,2] (0 v (x v 1))^ (0 v (x v 0))=x.
1212 [para_into,106,19] (x v c(y v (z v c(x))))^ (z v (y v 1))=x.
1230 [para_into,789,2] (0 v (x v 1))^ (x v (0 v 0))=x.
1233,1232 [para_into,789,179,demod,562,flip.1] 0 v c((0 v 0) v (0 v 0))= (1 v 1)^1.
1295,1294 [para_into,841,241,demod,288,flip.1] (c((0 v 0) v 0) v c(0 v 1)) v 1=0 v (1 v 1).
1297,1296 [para_into,841,179,demod,1233,flip.1] ((1 v 1)^1) v 1=0 v (1 v 1).
1319 [para_from,861,583,demod,1074] c(x v 1)=c(0 v (0 v (1 v (x v 0)))).
1326,1325 [para_into,863,21,flip.1] 0 v (0 v (1 v (x v 0)))=1 v (x v 0).
1328 [back_demod,1319,demod,1326] c(x v 1)=c(1 v (x v 0)).
1441 [para_into,1230,241,demod,288,1295,812,288,flip.1] c((0 v 0) v 0) v c(0 v 1)= (1 v 1)^1.
1590,1589 [para_into,200,21] c(1 v (c(x) v 0))=x^ (0 v c(1 v 1)).
1625 [para_into,202,7,demod,162,792,10,flip.1] c((1^c(x v x)) v x)=0.
1684 [para_from,1625,9] ((1^c(x v x)) v x) v 0=1.
1705,1704 [para_from,1684,326,flip.1] x v (((1^c(y v y)) v y) v 1)=x v (1 v 1).
1706 [para_from,1684,1188,demod,1705,867,flip.1] (1^c(x v x)) v x=1.
1756 [para_from,1706,2] x v 1= (1^c(y v y)) v (x v y).
1763 [copy,1756,flip.1] (1^c(x v x)) v (y v x)=y v 1.
1868 [para_into,377,2] (x v y)^ (0 v (x v c(y v y)))=x.
1878 [para_into,425,27] (x v ((c(y) v 0)^1))^ ((y^1) v (x v 0))=x.
1912 [para_from,521,95] (0 v (0 v 0)) v (x v 1)=0 v (x v 1).
2368 [para_into,206,11] (c(x) v (1^y)) v (x^ (0 v c(y)))=1.
2370 [para_into,206,45,demod,12] (0 v (x^x)) v c(x)=1.
2379,2378 [para_from,2370,19,flip.1] (0 v (x^x)) v 1=x v 1.
2397 [para_from,2370,2,flip.1] (0 v (x^x)) v (y v c(x))=y v 1.
2404,2403 [para_into,2378,21] 1 v ((0 v (x^x)) v 0)=x v 1.
2463,2462 [para_from,227,326,demod,792,10,flip.1] x v (((1^c(0)) v 0) v 1)=x v (1 v 1).
2464 [para_from,227,1188,demod,792,10,2463,867,792,10,flip.1] (1^c(0)) v 0=1.
2469,2468 [para_from,2464,1763,demod,792,756,flip.1] (1^c(0)) v 1=1 v 1.
2480 [para_from,2464,1188,demod,2469,867,flip.1] 1^c(0)=1.
2485,2484 [para_from,2480,391,demod,12] (c(0) v 1)^ (0 v 1)=c(0).
2486 [para_from,2480,619] (x v 1)^ (0 v (x v c(c(0))))=x.
2533 [para_into,2484,21] (1 v (c(0) v 0))^ (0 v 1)=c(0).
2565 [para_into,2486,2370,demod,2379,2485,flip.1] 0 v (c(0)^c(0))=c(0).
2584 [para_from,2565,7] (0 v c(c(0)^c(0)))^c(0)=0.
2606 [para_from,2533,85,demod,28,1590,flip.1] ((0^ (0 v c(1 v 1))) v c(0 v 1))^1=0^1.
2614 [para_from,2533,33,demod,1590] ((0^ (0 v c(1 v 1))) v c(0 v 1)) v c(0)=1.
3124 [para_into,393,27] (x v ((c(y) v 0)^z))^ ((y^1) v (x v c(z)))=x.
3345 [para_into,335,2370,demod,2404,56,flip.1] 0 v ((x v 1)^ (x v 1))=x v 1.
3354,3353 [para_from,3345,142] (c(x v 1) v c(x v 1)) v (x v 1)=0 v 1.
3542 [para_into,1912,1296,demod,1297,812] (0 v (0 v 0)) v (0 v (1 v 1))=1 v 1.
3896 [para_into,2368,7,demod,162,792,10] ((1^c(x)) v (1^x)) v 0=1.
3925,3924 [para_from,3896,1763,demod,792,756,flip.1] ((1^c(x)) v (1^x)) v 1=1 v 1.
3929 [para_from,3896,1188,demod,3925,867,flip.1] (1^c(x)) v (1^x)=1.
3965 [para_into,3929,585,demod,162,792,10,46] (1^x) v c(0 v x)=1.
4034 [para_into,3965,45] x v c(0 v (x v x))=1.
4113,4112 [para_from,3965,2397,demod,2379,flip.1] (1^x) v 1= (0 v x) v 1.
4205 [para_into,4034,2] x v c(x v (0 v x))=1.
4219,4218 [para_from,4034,131] 1^ (0 v (x v (x v x)))=x.
4220 [para_from,4034,106] 1^ (x v (x v (0 v x)))=x.
4229 [para_from,4034,2397,demod,2379] (0 v (x v x)) v 1=x v 1.
4301,4300 [para_from,4205,2397,demod,2379] (x v (0 v x)) v 1=x v 1.
4438,4437 [para_into,4218,95] 1^ (c(0) v (c(0) v 1))=c(0).
4475 [para_into,4220,807,demod,926] 1^ ((1 v (0 v 0)) v ((0 v 1) v 1))=1 v (0 v 0).
4555 [para_into,4229,19] (c(0) v 1) v 1=c(0) v 1.
4568,4567 [para_from,4229,128,demod,4219,flip.1] 0 v (1 v 1)=1.
4591,4590 [back_demod,3542,demod,4568,4301,flip.1] 1 v 1=0 v 1.
4879 [back_demod,2614,demod,4591] ((0^ (0 v c(0 v 1))) v c(0 v 1)) v c(0)=1.
4885 [back_demod,2606,demod,4591] ((0^ (0 v c(0 v 1))) v c(0 v 1))^1=0^1.
4946,4945 [back_demod,1589,demod,4591] c(1 v (c(x) v 0))=x^ (0 v c(0 v 1)).
4949 [back_demod,1441,demod,4591] c((0 v 0) v 0) v c(0 v 1)= (0 v 1)^1.
4977 [back_demod,198,demod,4591] c(c(x) v 1)=x^ (((0 v c(0 v 1))^0) v 0).
4983 [para_into,4590,259] (0 v c(x v x)) v (1 v x)=0 v 1.
5311,5310 [para_from,4555,55,demod,4438,flip.1] c(0) v 1=c(0).
5348 [para_from,4555,1328,demod,5311,5311,4946] c(c(0))=0^ (0 v c(0 v 1)).
5359,5358 [para_from,4555,811,demod,5311,10,5311,5311,flip.1] c(0)=0 v 1.
5407,5406 [back_demod,5348,demod,5359,flip.1] 0^ (0 v c(0 v 1))=c(0 v 1).
5425,5424 [back_demod,4879,demod,5407,5359,3354] 0 v 1=1.
5441,5440 [back_demod,2584,demod,5359,5425,5359,5425,704,5425,12,5359,5425] (0 v 0)^1=0.
5449 [back_demod,4885,demod,5425,12,5425,12] ((0^ (0 v 0)) v 0)^1=0^1.
5457,5456 [back_demod,4475,demod,5425,4591,5425,926,5425,4591,5425,704,5425,flip.1] 1 v (0 v 0)=1.
5467,5466 [back_demod,5406,demod,5425,12,5425,12] 0^ (0 v 0)=0.
5477,5476 [back_demod,5358,demod,5425] c(0)=1.
5500 [back_demod,4983,demod,5425] (0 v c(x v x)) v (1 v x)=1.
5505,5504 [back_demod,4977,demod,5425,12] c(c(x) v 1)=x^ (((0 v 0)^0) v 0).
5532 [back_demod,4949,demod,5425,12,5425,704,5425] c((0 v 0) v 0) v 0=1.
5536 [back_demod,4945,demod,5425,12] c(1 v (c(x) v 0))=x^ (0 v 0).
5653,5652 [back_demod,4590,demod,5425] 1 v 1=1.
5839,5838 [back_demod,815,demod,5425] c(1 v (x^y))= (0 v 0)^ (c(x) v c(y)).
5841,5840 [back_demod,795,demod,5425,5505] x^ (((0 v 0)^0) v 0)=x^ (0 v 0).
5843,5842 [back_demod,791,demod,5425] c(0 v 0)=1.
5863,5862 [back_demod,703,demod,5425] 1^1=1.
5875,5874 [back_demod,467,demod,5425] ((x v x) v x)^1=x v x.
5914,5913 [back_demod,5449,demod,5467,5441,flip.1] 0^1=0.
5949 [back_demod,5504,demod,5841] c(c(x) v 1)=x^ (0 v 0).
5967 [para_from,5476,391,demod,5653] (x v (0^x))^1=x.
6032,6031 [para_from,5476,29,demod,5839] (0 v 0)^ (c(x) v c(y))=0^ (c(x) v c(y)).
6054,6053 [back_demod,5838,demod,6032] c(1 v (x^y))