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

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-------

list(sos).
0 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
0 [] f(f(x,f(y,y)),f(x,y))=x.
0 [] x v y=f(f(x,x),f(y,y)).
0 [] x^y=f(f(x,y),f(x,y)).
0 [] c(x)=f(x,x).
end_of_list.
assign(max_proofs,5).
assign(max_weight,19).

list(passive).
1 [] A v (B v C)!=B v (A v C)|$Ans(AJ).
2 [] A^B!=c(c(A) v c(B))|$Ans(DM).
3 [] A v c(A)!=B v c(B)|$Ans(ONE).
4 [] c(c(A v c(B)) v c(A v B))!=A|$Ans(CUT_rewritten).
5 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS).
end_of_list.

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

------------> process sos:
** KEPT (pick-wt=19): 7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
** KEPT (pick-wt=11): 8 [] f(f(x,f(y,y)),f(x,y))=x.
---> New Demodulator: 9 [new_demod,8] f(f(x,f(y,y)),f(x,y))=x.
** KEPT (pick-wt=11): 11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
---> New Demodulator: 12 [new_demod,11] f(f(x,x),f(y,y))=x v y.
** KEPT (pick-wt=11): 14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
---> New Demodulator: 15 [new_demod,14] f(f(x,y),f(x,y))=x^y.
** KEPT (pick-wt=6): 17 [copy,16,flip.1] f(x,x)=c(x).
---> New Demodulator: 18 [new_demod,17] f(x,x)=c(x).
** KEPT (pick-wt=13): 19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
>>>> Starting back demodulation with 9.
>>>> Starting back demodulation with 12.
>>>> Starting back demodulation with 15.
    >> back demodulating 7 with 15.
>>>> Starting back demodulation with 18.
    >> back demodulating 14 with 18.
    >> back demodulating 11 with 18.
    >> back demodulating 8 with 18.
** KEPT (pick-wt=11): 26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
>>>> Starting back demodulation with 21.
    >> back demodulating 19 with 21.
>>>> Starting back demodulation with 23.
>>>> Starting back demodulation with 25.
  Following clause subsumed by 26 during input processing: 0 [copy,26,flip.1] f(x,y^z)=f(y,x^z).

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

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

given clause #1: (wt=6) 17 [copy,16,flip.1] f(x,x)=c(x).

given clause #2: (wt=8) 20 [back_demod,14,demod,18] c(f(x,y))=x^y.

given clause #3: (wt=7) 27 [para_into,20,17,flip.1] x^x=c(c(x)).

given clause #4: (wt=9) 22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.

given clause #5: (wt=10) 24 [back_demod,8,demod,18] f(f(x,c(y)),f(x,y))=x.

given clause #6: (wt=7) 32 [para_into,22,17] c(c(x))=x v x.

given clause #7: (wt=7) 35 [back_demod,27,demod,33] x^x=x v x.

given clause #8: (wt=9) 47 [para_into,24,17] f(f(x,c(x)),c(x))=x.

given clause #9: (wt=11) 26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).

given clause #10: (wt=10) 37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).

given clause #11: (wt=10) 51 [para_into,32,32] c(x v x)=c(x) v c(x).

given clause #12: (wt=10) 69 [para_from,47,20,flip.1] f(x,c(x))^c(x)=c(x).

given clause #13: (wt=12) 29 [para_into,22,20] f(x^y,c(z))=f(x,y) v z.

given clause #14: (wt=11) 41 [para_into,24,22] f(x v y,f(c(x),y))=c(x).

given clause #15: (wt=11) 49 [para_from,24,20,flip.1] f(x,c(y))^f(x,y)=c(x).

given clause #16: (wt=11) 57 [para_from,32,22] f(c(x),y v y)=x v c(y).

given clause #17: (wt=12) 31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).

given clause #18: (wt=11) 59 [para_from,32,22] f(x v x,c(y))=c(x) v y.

given clause #19: (wt=11) 61 [back_demod,45,demod,58] f(x v c(y),x v y)=c(x).

given clause #20: (wt=11) 71 [para_into,26,35] f(x,y v y)=f(y,x^y).

given clause #21: (wt=12) 34 [copy,31,flip.1] x v f(y,z)=f(c(x),y^z).

given clause #22: (wt=11) 74 [copy,71,flip.1] f(x,y^x)=f(y,x v x).

given clause #23: (wt=11) 77 [para_from,26,20,demod,21] x^ (y^z)=y^ (x^z).

given clause #24: (wt=11) 176 [para_into,71,61,flip.1] f(x,(x v c(x))^x)=c(x).

given clause #25: (wt=13) 39 [para_into,24,20] f(f(x,y^z),f(x,f(y,z)))=x.

given clause #26: (wt=11) 184 [para_from,71,20,demod,21] x^ (y^x)=y^ (x v x).

given clause #27: (wt=11) 185 [copy,184,flip.1] x^ (y v y)=y^ (x^y).

given clause #28: (wt=11) 200 [para_into,74,37,demod,23,58,33] x v (y v x)=y v (x v x).

given clause #29: (wt=15) 43 [para_into,24,24,demod,21] f(f(f(x,c(y)),x^y),x)=f(x,c(y)).

given clause #30: (wt=11) 203 [copy,200,flip.1] x v (y v y)=y v (x v y).

given clause #31: (wt=12) 53 [para_into,32,20,flip.1] f(x,y) v f(x,y)=c(x^y).

given clause #32: (wt=12) 55 [para_from,32,24] f(f(x,y v y),f(x,c(y)))=x.

given clause #33: (wt=15) 63 [para_into,47,20,demod,21] f(f(f(x,y),x^y),x^y)=f(x,y).

given clause #34: (wt=12) 72 [para_into,26,17,flip.1] f(x,(x^y)^y)=c(x^y).

given clause #35: (wt=12) 78 [para_into,37,32] (x v x)^c(y)=c(c(x) v y).

given clause #36: (wt=12) 81 [para_into,37,32] c(x)^ (y v y)=c(x v c(y)).

given clause #37: (wt=13) 65 [para_from,47,24] f(x,f(f(x,c(x)),x))=f(x,c(x)).

given clause #38: (wt=12) 118 [para_from,41,20,demod,33,flip.1] (x v y)^f(c(x),y)=x v x.

given clause #39: (wt=12) 140 [para_into,49,22,demod,33,58,33] (x v c(y))^ (x v y)=x v x.

given clause #40: (wt=12) 156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).

given clause #41: (wt=15) 67 [para_from,47,24,demod,33] f(f(f(x,c(x)),x v x),x)=f(x,c(x)).

given clause #42: (wt=12) 245 [para_from,176,20,demod,33,flip.1] x^ ((x v c(x))^x)=x v x.

given clause #43: (wt=12) 348 [para_into,55,71] f(f(x,y^x),f(y,c(x)))=y.

given clause #44: (wt=12) 409 [para_into,81,185] x^ (c(y)^x)=c(y v c(x)).

given clause #45: (wt=14) 75 [para_from,26,24] f(f(x,c(y^z)),f(y,x^z))=x.

given clause #46: (wt=13) 80 [para_into,37,20] (x^y)^c(z)=c(f(x,y) v z).

given clause #47: (wt=13) 83 [para_into,37,20] c(x)^ (y^z)=c(x v f(y,z)).

given clause #48: (wt=13) 84 [copy,80,flip.1] c(f(x,y) v z)= (x^y)^c(z).

given clause #49: (wt=13) 85 [copy,83,flip.1] c(x v f(y,z))=c(x)^ (y^z).

given clause #50: (wt=13) 122 [para_into,49,32] f(x,y v y)^f(x,c(y))=c(x).

given clause #51: (wt=13) 126 [para_into,49,47,demod,21] x^f(f(x,c(x)),x)=x^c(x).

given clause #52: (wt=13) 146 [para_into,57,32] f(x v x,y v y)=c(x) v c(y).

given clause #53: (wt=15) 94 [para_into,69,20,demod,21,21] f(f(x,y),x^y)^ (x^y)=x^y.

given clause #54: (wt=13) 150 [para_from,57,41] f(x v (y v y),x v c(y))=c(x).

given clause #55: (wt=13) 249 [para_into,39,176] f(c(x),f(x,f(x v c(x),x)))=x.

given clause #56: (wt=13) 251 [para_into,39,74] f(f(x,y v y),f(y,f(x,y)))=y.

given clause #57: (wt=14) 96 [para_from,69,26] f(x,c(y))=f(f(y,c(y)),x^c(y)).

given clause #58: (wt=13) 253 [para_into,39,26] f(f(x,y^z),f(y,f(x,z)))=y.

given clause #59: (wt=13) 276 [para_into,184,37,demod,38,82,33] c(x v (y v x))=c(y v (x v x)).

given clause #60: (wt=13) 278 [copy,276,flip.1] c(x v (y v y))=c(y v (x v y)).

given clause #61: (wt=14) 97 [copy,96,flip.1] f(f(x,c(x)),y^c(x))=f(y,c(x)).

given clause #62: (wt=13) 330 [para_from,203,41,demod,58] f(x v (y v x),y v c(x))=c(y).

given clause #63: (wt=13) 342 [para_into,53,74,demod,338] c(x^ (y v y))=c(y^ (x^y)).

given clause #64: (wt=13) 343 [para_into,53,71,demod,336] c(x^ (y^x))=c(y^ (x v x)).

given clause #65: (wt=14) 100 [para_into,29,32] f(x^y,z v z)=f(x,y) v c(z).

given clause #66: (wt=13) 344 [para_into,53,26,demod,341] c(x^ (y^z))=c(y^ (x^z)).

given clause #67: (wt=13) 465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).

----> UNIT CONFLICT at   0.09 sec ----> 928 [binary,927,1] $Ans(AJ).

Length of proof is 12.  Level of proof is 6.

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

1 [] A v (B v C)!=B v (A v C)|$Ans(AJ).
7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
10 [] x v y=f(f(x,x),f(y,y)).
11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
13 [] x^y=f(f(x,y),f(x,y)).
14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
16 [] c(x)=f(x,x).
18,17 [copy,16,flip.1] f(x,x)=c(x).
19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
21,20 [back_demod,14,demod,18] c(f(x,y))=x^y.
23,22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.
26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).
37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).
156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).
465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).
927 [para_into,465,22,demod,23] x v (y v z)=y v (x v z).
928 [binary,927,1] $Ans(AJ).

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


given clause #68: (wt=11) 927 [para_into,465,22,demod,23] x v (y v z)=y v (x v z).

given clause #69: (wt=15) 102 [para_into,29,20] f(x^y,z^u)=f(x,y) v f(z,u).

given clause #70: (wt=13) 469 [para_into,156,31] x v f(c(y),z)=y v f(c(x),z).

given clause #71: (wt=13) 486 [para_from,156,20] c(x v f(y,z))=y^ (c(x)^z).

given clause #72: (wt=13) 488 [copy,486,flip.1] x^ (c(y)^z)=c(y v f(x,z)).

given clause #73: (wt=15) 103 [copy,102,flip.1] f(x,y) v f(z,u)=f(x^y,z^u).

given clause #74: (wt=13) 515 [para_from,348,20,flip.1] f(x,y^x)^f(y,c(x))=c(y).

given clause #75: (wt=13) 647 [back_demod,47,demod,641] f(f(x,x v x),c(x^c(x)))=x.

given clause #76: (wt=13) 688 [para_into,251,57] f(x v c(y),f(y,f(c(x),y)))=y.

given clause #77: (wt=17) 104 [para_from,29,69] (f(x,y) v (x^y))^c(x^y)=c(x^y).

given clause #78: (wt=13) 704 [para_into,96,43,demod,23,23,157,161,466,flip.1] x v f(f(x,c(x)),c(y))=x v y.

given clause #79: (wt=13) 1050 [para_into,486,22,demod,38,38] c(x v (y v z))=c(y v (x v z)).

given clause #80: (wt=14) 112 [para_into,41,32,demod,33] f(c(x) v y,f(x v x,y))=x v x.

given clause #81: (wt=16) 106 [para_from,29,47] f(f(x,y) v (x^y),c(x^y))=x^y.

given clause #82: (wt=14) 124 [para_into,49,20] f(x,y^z)^f(x,f(y,z))=c(x).

given clause #83: (wt=14) 152 [para_from,57,49,demod,52,58,33,33] (x v (y v y))^ (x v c(y))=x v x.

given clause #84: (wt=14) 155 [para_into,31,32] f(x v x,y^z)=c(x) v f(y,z).

given clause #85: (wt=15) 108 [para_from,29,24] f(f(x,y) v z,f(x^y,z))=x^y.

given clause #86: (wt=14) 159 [copy,155,flip.1] c(x) v f(y,z)=f(x v x,y^z).

given clause #87: (wt=14) 162 [back_demod,116,demod,157] f(x v f(x v y,y),c(x))=x v y.

given clause #88: (wt=14) 164 [back_demod,114,demod,157] f(x v (y^z),x v f(y,z))=c(x).

given clause #89: (wt=19) 110 [para_into,41,51,demod,52] f((x v x) v y,f(c(x) v c(x),y))=c(x) v c(x).

given clause #90: (wt=14) 201 [para_into,74,31,flip.1] f(x,c(y) v c(y))=y v f(x,c(y)).

given clause #91: (wt=14) 204 [back_demod,182,demod,202] f(x v f(y,c(x)),f(x,y^x))=y.

given clause #92: (wt=14) 214 [para_from,74,24] f(f(x,c(y^x)),f(y,x v x))=x.

given clause #93: (wt=16) 128 [para_into,49,29] (f(x,y) v z)^f(x^y,z)=c(x^y).

given clause #94: (wt=14) 219 [para_into,77,69,flip.1] f(x,c(x))^ (y^c(x))=y^c(x).

given clause #95: (wt=14) 223 [para_into,77,37] x^c(y v z)=c(y)^ (x^c(z)).

given clause #96: (wt=14) 227 [copy,223,flip.1] c(x)^ (y^c(z))=y^c(x v z).

given clause #97: (wt=15) 130 [para_into,49,47,demod,33,21] f(f(x,c(x)),x v x)^x=x^c(x).

given clause #98: (wt=14) 372 [para_into,72,31] x v f(c(x)^y,y)=c(c(x)^y).

given clause #99: (wt=14) 388 [para_from,72,39] f(c(x^y),f(x,f(x^y,y)))=x.

given clause #100: (wt=14) 398 [para_into,78,32] (x v x)^ (y v y)=c(c(x) v c(y)).

given clause #101: (wt=15) 136 [para_into,49,26] f(x,c(y^z))^f(y,x^z)=c(x).

given clause #102: (wt=14) 420 [para_into,118,203,demod,58] (x v (y v x))^ (y v c(x))=y v y.

given clause #103: (wt=14) 456 [para_into,156,32] f(x,(y v y)^z)=c(y) v f(x,z).

given clause #104: (wt=14) 479 [para_from,156,39] f(x v f(y,z),f(y,f(c(x),z)))=y.

given clause #105: (wt=15) 138 [para_into,49,24,demod,21,21] f(f(x,c(y)),x^y)^x=x^c(y).

given clause #106: (wt=14) 519 [para_into,409,32] x^ ((y v y)^x)=c(c(y) v c(x)).

given clause #107: (wt=14) 645 [back_demod,69,demod,639] f(x,x v x)^c(x^c(x))=c(x).

given clause #108: (wt=14) 684 [para_from,249,20,flip.1] c(x)^f(x,f(x v c(x),x))=c(x).

given clause #109: (wt=15) 142 [para_from,49,26] f(x,c(y))=f(f(y,c(z)),x^f(y,z)).

given clause #110: (wt=14) 700 [para_from,251,20,flip.1] f(x,y v y)^f(y,f(x,y))=c(y).

given clause #111: (wt=14) 802 [para_from,253,20,flip.1] f(x,y^z)^f(y,f(x,z))=c(y).

given clause #112: (wt=14) 885 [para_into,100,71] f(x,(y^z)^x)=f(y,z) v c(x).

given clause #113: (wt=15) 143 [copy,142,flip.1] f(f(x,c(y)),z^f(x,y))=f(z,c(x)).

given clause #114: (wt=14) 886 [copy,885,flip.1] f(x,y) v c(z)=f(z,(x^y)^z).

given clause #115: (wt=14) 942 [para_from,465,24] f(x v f(y,c(z)),f(y,x v z))=y.

given clause #116: (wt=14) 945 [para_from,465,20] c(x v f(y,c(z)))=y^c(x v z).

given clause #117: (wt=17) 154 [para_into,31,51] f(c(x) v c(x),y^z)= (x v x) v f(y,z).

given clause #118: (wt=14) 953 [copy,945,flip.1] x^c(y v z)=c(y v f(x,c(z))).

given clause #119: (wt=14) 1114 [para_into,647,96,demod,30,646] f(f(x,c(x)) v (x^c(x)),c(x))=x.

given clause #120: (wt=14) 1138 [para_from,688,20,flip.1] (x v c(y))^f(y,f(c(x),y))=c(y).

given clause #121: (wt=17) 158 [copy,154,flip.1] (x v x) v f(y,z)=f(c(x) v c(x),y^z).

given clause #122: (wt=14) 1161 [para_into,704,34] f(c(x),f(x,c(x))^c(y))=x v y.

given clause #123: (wt=14) 1166 [para_from,704,486,demod,38,flip.1] f(x,c(x))^c(x v y)=c(x v y).

given clause #124: (wt=14) 1205 [para_into,112,41] f(c(x) v f(c(x),x),c(x))=x v x.

given clause #125: (wt=15) 160 [back_demod,132,demod,157] (x v f(x v y,y))^c(x)=c(x v y).

given clause #126: (wt=14) 1291 [para_into,214,57] f(f(x,c(c(y)^x)),y v c(x))=x.

given clause #127: (wt=14) 1298 [para_into,219,37,demod,38] f(x,c(x))^c(y v x)=c(y v x).

given clause #128: (wt=15) 166 [para_from,31,49,demod,23,33] (x v (y^z))^ (x v f(y,z))=x v x.

given clause #129: (wt=16) 168 [para_from,59,49,demod,52] (c(x) v y)^f(x v x,y)=c(x) v c(x).

given clause #130: (wt=15) 206 [back_demod,180,demod,202] (x v f(y,c(x)))^f(x,y^x)=c(y).

given clause #131: (wt=15) 212 [para_from,74,49] f(x,c(y^x))^f(y,x v x)=c(x).

given clause #132: (wt=15) 218 [para_into,77,77] x^ (y^ (z^u))=z^ (x^ (y^u)).

given clause #133: (wt=16) 170 [para_into,61,51] f(x v (c(y) v c(y)),x v (y v y))=c(x).

given clause #134: (wt=15) 221 [para_into,77,49,flip.1] f(x,c(y))^ (z^f(x,y))=z^c(x).

given clause #135: (wt=15) 224 [para_into,77,35,flip.1] x^ ((x^y)^y)= (x^y) v (x^y).

given clause #136: (wt=15) 226 [copy,218,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)).

given clause #137: (wt=16) 186 [para_into,34,71] x v f(y,z^y)=f(c(x),z^ (y v y)).

given clause #138: (wt=15) 229 [para_from,77,29,demod,30] f(x,y^z) v u=f(y,x^z) v u.

given clause #139: (wt=15) 230 [para_from,77,26] f(x,y^ (z^u))=f(z,x^ (y^u)).

given clause #140: (wt=15) 232 [copy,230,flip.1] f(x,y^ (z^u))=f(y,z^ (x^u)).

given clause #141: (wt=16) 187 [para_into,34,31,demod,157] x v (y v f(z,u))=y v f(c(x),z^u).

given clause #142: (wt=15) 237 [para_into,176,31,demod,33,33] x v f(c(x) v (x v x),c(x))=x v x.

given clause #143: (wt=15) 281 [para_from,184,29,demod,30] f(x,y v y) v z=f(y,x^y) v z.

given clause #144: (wt=15) 282 [para_from,184,77] x^ (y^ (z v z))=z^ (x^ (y^z)).

given clause #145: (wt=17) 188 [para_into,34,29] x v (f(y,z) v u)=f(c(x),(y^z)^c(u)).

given clause #146: (wt=15) 283 [para_from,184,26] f(x,y^ (z v z))=f(z,x^ (y^z)).

given clause #147: (wt=15) 284 [copy,281,flip.1] f(x,y^x) v z=f(y,x v x) v z.

given clause #148: (wt=15) 285 [copy,282,flip.1] x^ (y^ (z^x))=y^ (z^ (x v x)).

given clause #149: (wt=16) 189 [para_into,34,26] x v f(y,z^u)=f(c(x),z^ (y^u)).

given clause #150: (wt=15) 286 [copy,283,flip.1] f(x,y^ (z^x))=f(y,z^ (x v x)).

given clause #151: (wt=15) 293 [para_from,185,77] x^ (y^ (z^y))=z^ (x^ (y v y)).

given clause #152: (wt=15) 294 [para_from,185,26] f(x,y^ (z^y))=f(z,x^ (y v y)).

given clause #153: (wt=16) 190 [copy,186,flip.1] f(c(x),y^ (z v z))=x v f(z,y^z).

given clause #154: (wt=15) 297 [copy,293,flip.1] x^ (y^ (z v z))=y^ (z^ (x^z)).

given clause #155: (wt=15) 298 [copy,294,flip.1] f(x,y^ (z v z))=f(y,z^ (x^z)).

given clause #156: (wt=15) 311 [para_into,43,47,demod,48] f(f(x,f(x,c(x))^x),f(x,c(x)))=x.

given clause #157: (wt=16) 191 [copy,187,flip.1] x v f(c(y),z^u)=y v (x v f(z,u)).

given clause #158: (wt=15) 313 [para_into,43,26] f(f(x,f(x,c(y))^y),x)=f(x,c(y)).

given clause #159: (wt=15) 350 [para_into,55,61] f(c(x),f(x v c(x),c(x)))=x v c(x).

given clause #160: (wt=15) 356 [para_into,63,26] f(f(x,f(x,y)^y),x^y)=f(x,y).

given clause #161: (wt=17) 192 [copy,188,flip.1] f(c(x),(y^z)^c(u))=x v (f(y,z) v u).

given clause #162: (wt=15) 358 [para_into,63,26] f(x,f(f(x,y),x^y)^y)=f(x,y).

given clause #163: (wt=15) 392 [para_from,72,24] f(f(x,c((x^y)^y)),c(x^y))=x.

given clause #164: (wt=12) 2081 [para_into,392,96,demod,30,391] f(f(x,y) v (x^y),c(x))=x.

given clause #165: (wt=16) 193 [copy,189,flip.1] f(c(x),y^ (z^u))=x v f(z,y^u).

given clause #166: (wt=11) 2105 [para_into,2081,176,demod,246] f(c(x) v (x v x),c(x))=x.

given clause #167: (wt=11) 2199 [para_into,2105,927] f(x v (c(x) v x),c(x))=x.

given clause #168: (wt=12) 2228 [para_from,2105,20,flip.1] (c(x) v (x v x))^c(x)=c(x).

given clause #169: (wt=16) 194 [para_from,34,71,demod,21,18] f(x,c(y^z))=f(f(y,z),x^f(y,z)).

given clause #170: (wt=12) 2263 [para_from,2199,20,flip.1] (x v (c(x) v x))^c(x)=c(x).

given clause #171: (wt=13) 2181 [para_from,2081,20,flip.1] (f(x,y) v (x^y))^c(x)=c(x).

given clause #172: (wt=14) 2139 [para_into,2081,24,demod,50,21] f(x v c(x),x^c(y))=f(x,c(y)).

given clause #173: (wt=16) 195 [copy,194,flip.1] f(f(x,y),z^f(x,y))=f(z,c(x^y)).

given clause #174: (wt=14) 2343 [para_into,2181,24,demod,50,21,21] (x v c(x))^ (x^c(y))=x^c(y).

given clause #175: (wt=14) 2384 [para_into,2139,26] f(x,(x v c(x))^c(y))=f(x,c(y)).

given clause #176: (wt=14) 2408 [para_into,2343,77] x^ ((x v c(x))^c(y))=x^c(y).

given clause #177: (wt=16) 198 [para_into,74,49,demod,54,flip.1] f(f(x,c(y)),c(x^y))=f(f(x,y),c(x)).

given clause #178: (wt=15) 400 [para_into,78,20] (x v x)^ (y^z)=c(c(x) v f(y,z)).

given clause #179: (wt=15) 401 [copy,400,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z).

given clause #180: (wt=15) 406 [para_into,81,20] (x^y)^ (z v z)=c(f(x,y) v c(z)).

given clause #181: (wt=16) 216 [para_from,74,34] x v f(y,z v z)=f(c(x),z^ (y^z)).

given clause #182: (wt=15) 411 [copy,406,flip.1] c(f(x,y) v c(z))= (x^y)^ (z v z).

given clause #183: (wt=15) 458 [para_into,156,20] f(x,(y^z)^u)=f(y,z) v f(x,u).

given clause #184: (wt=15) 474 [copy,458,flip.1] f(x,y) v f(z,u)=f(z,(x^y)^u).

given clause #185: (wt=16) 217 [copy,216,flip.1] f(c(x),y^ (z^y))=x v f(z,y v y).

given clause #186: (wt=15) 484 [para_from,156,24] f(f(x,c(c(y)^z)),y v f(x,z))=x.

given clause #187: (wt=15) 521 [para_into,409,20] x^ ((y^z)^x)=c(f(y,z) v c(x)).

given clause #188: (wt=15) 524 [copy,521,flip.1] c(f(x,y) v c(z))=z^ ((x^y)^z).

given clause #189: (wt=19) 228 [para_from,77,74] f(x^y,x^ (z^y))=f(z,(x^y) v (x^y)).

given clause #190: (wt=15) 533 [para_from,409,26,demod,466,33,464] x v f(y,z v z)=x v f(z,y^z).

given clause #191: (wt=15) 535 [copy,533,flip.1] x v f(y,z^y)=x v f(z,y v y).

given clause #192: (wt=15) 591 [para_into,83,184,flip.1] c(x v f(y,c(x)))=y^ (c(x) v c(x)).

given clause #193: (wt=19) 231 [copy,228,flip.1] f(x,(y^z) v (y^z))=f(y^z,y^ (x^z)).

given clause #194: (wt=15) 662 [para_into,94,26] f(x,f(x,y)^y)^ (x^y)=x^y.

given clause #195: (wt=15) 664 [para_into,94,77] x^ (f(f(x,y),x^y)^y)=x^y.

given clause #196: (wt=15) 674 [para_from,249,41] f(x v f(x,f(x v c(x),x)),x)=c(x).

given clause #197: (wt=19) 235 [para_into,176,20,demod,21] f(f(x,y),(f(x,y) v (x^y))^f(x,y))=x^y.

given clause #198: (wt=15) 686 [para_into,251,146] f(c(x) v c(y),f(y,f(x v x,y)))=y.

given clause #199: (wt=15) 690 [para_into,251,65] f(f(f(x,c(x)),x v x),f(x,c(x)))=x.

given clause #200: (wt=15) 718 [para_from,96,24] f(f(f(x,c(x)),y^c(x)),f(y,x))=y.

given clause #201: (wt=17) 247 [para_into,39,77] f(f(x,y^ (z^u)),f(x,f(z,y^u)))=x.

given clause #202: (wt=14) 2625 [para_into,718,17] f(f(f(x,c(x)),x^c(x)),c(x))=x.

given clause #203: (wt=15) 780 [para_into,253,22] f(f(c(x),y^c(z)),f(y,x v z))=y.

given clause #204: (wt=15) 790 [para_into,253,41] f(f(c(x),(x v y)^y),c(x))=x v y.

given clause #205: (wt=16) 255 [para_into,39,17] f(c(x^y),f(x^y,f(x,y)))=x^y.

given clause #206: (wt=15) 865 [para_from,342,22,demod,23] x v (y^ (z^y))=x v (z^ (y v y)).

given clause #207: (wt=15) 868 [para_from,342,22,demod,23] (x^ (y^x)) v z= (y^ (x v x)) v z.

given clause #208: (wt=15) 875 [copy,865,flip.1] x v (y^ (z v z))=x v (z^ (y^z)).

given clause #209: (wt=17) 257 [para_into,39,74] f(f(x,y^ (z^y)),f(x,f(z,y v y)))=x.

given clause #210: (wt=15) 878 [copy,868,flip.1] (x^ (y v y)) v z= (y^ (x^y)) v z.

given clause #211: (wt=15) 921 [para_from,344,22,demod,23] x v (y^ (z^u))=x v (z^ (y^u)).

given clause #212: (wt=15) 924 [para_from,344,22,demod,23] (x^ (y^z)) v u= (y^ (x^z)) v u.

given clause #213: (wt=17) 259 [para_into,39,71] f(f(x,y^ (z v z)),f(x,f(z,y^z)))=x.

given clause #214: (wt=15) 934 [para_from,465,41,demod,23] f(x v c(y v z),y v (x v z))=c(x).

given clause #215: (wt=15) 940 [para_from,465,49] (x v f(y,c(z)))^f(y,x v z)=c(y).

given clause #216: (wt=15) 956 [para_into,927,927] x v (y v (z v u))=z v (x v (y v u)).

given clause #217: (wt=17) 261 [para_into,39,31,demod,157] f(x v f(y,z^u),f(y,x v f(z,u)))=y.

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

given clause #219: (wt=15) 981 [para_from,927,41] f(x v (y v z),f(c(y),x v z))=c(y).

given clause #220: (wt=15) 1009 [para_into,469,32] x v f(y v y,z)=c(y) v f(c(x),z).

given clause #221: (wt=18) 263 [para_into,39,29] f(f(x,(y^z)^c(u)),f(x,f(y,z) v u))=x.

given clause #222: (wt=15) 1010 [para_into,469,465,demod,23,466,23] x v (y v (z v u))=z v (y v (x v u)).

given clause #223: (wt=15) 1017 [copy,1009,flip.1] c(x) v f(c(y),z)=y v f(x v x,z).

given clause #224: (wt=15) 1061 [para_into,488,32] x^ ((y v y)^z)=c(c(y) v f(x,z)).

given clause #225: (wt=19) 265 [para_into,39,39] f(f(f(x,y^z),x^f(y,z)),x)=f(x,y^z).

given clause #226: (wt=15) 1072 [para_into,488,83] c(x v f(c(y),z))=c(y v f(c(x),z)).

given clause #227: (wt=15) 1074 [copy,1061,flip.1] c(c(x) v f(y,z))=y^ ((x v x)^z).

given clause #228: (wt=15) 1085 [para_from,488,26,demod,466,21,464] x v f(y,z^u)=x v f(z,y^u).

given clause #229: (wt=19) 267 [para_from,39,49,demod,21,21] f(f(x,y^z),x^f(y,z))^x=x^ (y^z).

given clause #230: (wt=15) 1146 [para_into,704,32,demod,58] c(x) v f(x v c(x),c(y))=c(x) v y.

given clause #231: (wt=15) 1154 [para_into,704,32] x v f(f(x,c(x)),y v y)=x v c(y).

given clause #232: (wt=15) 1168 [para_from,704,85,flip.1] c(x)^ (f(x,c(x))^c(y))=c(x v y).

given clause #233: (wt=19) 269 [para_into,184,184] (x^y)^ (x^ (y v y))=y^ ((x^y) v (x^y)).

given clause #234: (wt=15) 1196 [para_from,1050,22,demod,23] (x v (y v z)) v u= (y v (x v z)) v u.

given clause #235: (wt=15) 1223 [para_into,124,156] (x v f(y,z))^f(y,f(c(x),z))=c(y).

given clause #236: (wt=15) 1227 [para_into,124,72] c(x^y)^f(x,f(x^y,y))=c(x).

given clause #237: (wt=19) 271 [para_into,184,77] (x^y)^ (x^ (z^y))=z^ ((x^y) v (x^y)).

given clause #238: (wt=15) 1283 [para_into,204,34] f(f(c(x),y^c(x)),f(x,y^x))=y.

given clause #239: (wt=15) 1394 [para_into,456,118,flip.1] c(x) v f(y,f(c(x),x))=f(y,x v x).

given clause #240: (wt=15) 1429 [para_into,138,26] f(x,f(x,c(y))^y)^x=x^c(y).

given clause #241: (wt=16) 272 [para_into,184,69,demod,36,flip.1] f(x,c(x))^ (c(x) v c(x))=c(x) v c(x).

given clause #242: (wt=15) 1658 [para_from,1291,20,flip.1] f(x,c(c(y)^x))^ (y v c(x))=c(x).

given clause #243: (wt=15) 1708 [para_into,218,77] x^ (y^ (z^u))=z^ (y^ (x^u)).

given clause #244: (wt=15) 1753 [para_into,226,184] x^ (y^ (z v z))=z^ (y^ (x^z)).

given clause #245: (wt=16) 274 [para_into,184,49,demod,54,flip.1] f(x,c(y))^c(x^y)=f(x,y)^c(x).

given clause #246: (wt=15) 1756 [para_into,226,77] x^ (y^ (z^u))=x^ (z^ (y^u)).

given clause #247: (wt=15) 1765 [copy,1753,flip.1] x^ (y^ (z^x))=z^ (y^ (x v x)).

given clause #248: (wt=15) 1811 [para_into,230,26] f(x,y^ (z^u))=f(z,y^ (x^u)).

given clause #249: (wt=19) 277 [copy,271,flip.1] x^ ((y^z) v (y^z))= (y^z)^ (y^ (x^z)).

given clause #250: (wt=15) 1838 [para_into,232,184] f(x,y^ (z v z))=f(z,y^ (x^z)).

given clause #251: (wt=15) 1843 [para_into,232,26] f(x,y^ (z^u))=f(x,z^ (y^u)).

given clause #252: (wt=15) 1850 [copy,1838,flip.1] f(x,y^ (z^x))=f(z,y^ (x v x)).

given clause #253: (wt=19) 279 [para_from,184,74] f(x^y,x^ (y v y))=f(y,(x^y) v (x^y)).

given clause #254: (wt=15) 1904 [para_into,285,77] x^ (y^ (z^y))=x^ (z^ (y v y)).

given clause #255: (wt=15) 1907 [copy,1904,flip.1] x^ (y^ (z v z))=x^ (z^ (y^z)).

given clause #256: (wt=15) 1923 [para_into,286,26] f(x,y^ (z^y))=f(x,z^ (y v y)).

given clause #257: (wt=16) 287 [para_into,185,34,demod,21,18,flip.1] f(x,y)^ (z^f(x,y))=z^c(x^y).

given clause #258: (wt=15) 1925 [copy,1923,flip.1] f(x,y^ (z v z))=f(x,z^ (y^z)).

given clause #259: (wt=15) 2015 [para_into,356,24,demod,50,25] f(f(f(x,c(y)),x^f(x,y)),c(x))=x.

given clause #260: (wt=15) 2021 [para_into,356,26] f(x,f(x,f(x,y)^y)^y)=f(x,y).

given clause #261: (wt=17) 301 [para_into,200,34,demod,54] f(x,y) v f(c(z),x^y)=z v c(x^y).

given clause #262: (wt=15) 2075 [para_into,358,24,demod,50,25] f(f(x,c(y)),f(x,c(x))^f(x,y))=x.

given clause #263: (wt=15) 2083 [para_into,2081,1161,demod,1169,33] f((x v y) v c(x v y),x v x)=c(x).

given clause #264: (wt=15) 2131 [para_into,2081,41,demod,119,466] x v f(c(x) v (x v x),c(y))=x v y.

given clause #265: (wt=18) 307 [para_into,43,32,demod,33] f(f(f(x,y v y),x^c(y)),x)=f(x,y v y).

given clause #266: (wt=15) 2151 [para_into,2081,409,demod,157,18] f((x v c(y)) v c(x v c(y)),c(y))=y.

given clause #267: (wt=15) 2579 [para_into,662,77] x^ (f(x,f(x,y)^y)^y)=x^y.

given clause #268: (wt=15) 2631 [para_from,2625,20,flip.1] f(f(x,c(x)),x^c(x))^c(x)=c(x).

given clause #269: (wt=16) 318 [para_into,203,34,demod,21,18,flip.1] f(x,y) v (z v f(x,y))=z v c(x^y).

given clause #270: (wt=15) 2749 [para_into,957,927] x v (y v (z v u))=x v (z v (y v u)).

given clause #271: (wt=15) 2817 [para_into,1154,71] x v f(y,f(x,c(x))^y)=x v c(y).

given clause #272: (wt=15) 2951 [para_into,2083,71] f(x,((x v y) v c(x v y))^x)=c(x).

given clause #273: (wt=16) 328 [para_from,203,61,demod,52] f(x v (c(y) v c(y)),y v (x v y))=c(x).

given clause #274: (wt=15) 2957 [para_into,2131,927] x v f(x v (c(x) v x),c(y))=x v y.

given clause #275: (wt=16) 390 [para_from,72,49] f(x,c((x^y)^y))^c(x^y)=c(x).

given clause #276: (wt=16) 402 [para_from,78,77] x^c(c(y) v z)= (y v y)^ (x^c(z)).

given clause #277: (wt=18) 335 [para_into,53,74] f(x,y v y) v f(y,x^y)=c(y^ (x^y)).

given clause #278: (wt=16) 404 [copy,402,flip.1] (x v x)^ (y^c(z))=y^c(c(x) v z).

given clause #279: (wt=16) 412 [para_from,81,77] x^c(y v c(z))=c(y)^ (x^ (z v z)).

given clause #280: (wt=16) 414 [copy,412,flip.1] c(x)^ (y^ (z v z))=y^c(x v c(z)).

given clause #281: (wt=18) 337 [para_into,53,71] f(x,y^x) v f(y,x v x)=c(y^ (x v x)).

given clause #282: (wt=16) 418 [para_from,65,49,demod,21] f(x,f(x,c(x))^x)^f(x,c(x))=c(x).

given clause #283: (wt=16) 438 [para_from,118,77,flip.1] (x v y)^ (z^f(c(x),y))=z^ (x v x).

given clause #284: (wt=16) 440 [para_from,118,26] f(x,y v y)=f(y v z,x^f(c(y),z)).

given clause #285: (wt=18) 340 [para_into,53,26] f(x,y^z) v f(y,x^z)=c(y^ (x^z)).

given clause #286: (wt=16) 450 [para_from,140,77] x^ (y v y)= (y v c(z))^ (x^ (y v z)).

given clause #287: (wt=16) 451 [para_from,140,26] f(x,y v y)=f(y v c(z),x^ (y v z)).

given clause #288: (wt=16) 463 [para_into,156,77] f(x,y^ (c(z)^u))=z v f(x,y^u).

given clause #289: (wt=18) 354 [para_from,55,49,demod,21,21] f(f(x,y v y),x^c(y))^x=x^ (y v y).

given clause #290: (wt=16) 477 [para_from,156,41] f(x v (c(y)^z),y v f(c(x),z))=c(x).

given clause #291: (wt=16) 482 [para_from,156,49] f(x,c(c(y)^z))^ (y v f(x,z))=c(x).

given clause #292: (wt=16) 491 [para_from,245,77,flip.1] x^ (y^ ((x v c(x))^x))=y^ (x v x).

given clause #293: (wt=18) 360 [para_into,72,185] f(x,(y^ (x^y))^ (y v y))=c(x^ (y v y)).

given clause #294: (wt=16) 493 [para_from,245,26] f(x,y v y)=f(y,x^ ((y v c(y))^y)).

given clause #295: (wt=16) 528 [para_from,409,77,flip.1] x^ (y^ (c(z)^x))=y^c(z v c(x)).

given clause #296: (wt=16) 530 [para_from,409,39,demod,466,33,157,18] f(x v f(y,z v z),f(y,x v c(z)))=y.

given clause #297: (wt=18) 362 [para_into,72,184] f(x,(y^ (x v x))^ (y^x))=c(x^ (y^x)).

given clause #298: (wt=16) 572 [para_into,80,20] (x^y)^ (z^u)=c(f(x,y) v f(z,u)).

given clause #299: (wt=16) 577 [copy,572,flip.1] c(f(x,y) v f(z,u))= (x^y)^ (z^u).

given clause #300: (wt=16) 601 [para_from,83,29,demod,23] (x v f(y,z)) v u=f(c(x),y^z) v u.

given clause #301: (wt=18) 364 [para_into,72,77] f(x,(y^ (x^z))^ (y^z))=c(x^ (y^z)).

given clause #302: (wt=16) 604 [copy,601,flip.1] f(c(x),y^z) v u= (x v f(y,z)) v u.

given clause #303: (wt=16) 636 [para_into,122,61] c(x)^f(x v c(x),c(x))=c(x v c(x)).

given clause #304: (wt=16) 672 [para_from,249,118] (x v f(x,f(x v c(x),x)))^x=x v x.

given clause #305: (wt=18) 368 [para_into,72,185] f(x,y^ ((x^ (y v y))^y))=c(x^ (y v y)).

given clause #306: (wt=16) 676 [para_from,249,39] f(f(c(x),x^f(x v c(x),x)),x)=c(x).

given clause #307: (wt=16) 716 [para_from,96,49] f(f(x,c(x)),y^c(x))^f(y,x)=c(y).

given clause #308: (wt=16) 778 [para_into,253,24] f(f(f(x,c(y)),z^f(x,y)),f(z,x))=z.

given clause #309: (wt=18) 370 [para_into,72,77] f(x,y^ ((x^ (y^z))^z))=c(x^ (y^z)).

given clause #310: (wt=16) 845 [para_into,330,32] f(c(x) v (y v c(x)),y v (x v x))=c(y).

given clause #311: (wt=16) 887 [para_from,100,251] f(f(x,y) v c(z),f(z,f(x^y,z)))=z.

given clause #312: (wt=16) 899 [para_into,344,37] c(x^c(y v z))=c(c(y)^ (x^c(z))).

given clause #313: (wt=19) 374 [back_demod,345,demod,367] c((x^y)^c(z))=f(x,y) v ((f(x,y) v z) v z).

given clause #314: (wt=16) 908 [copy,899,flip.1] c(c(x)^ (y^c(z)))=c(y^c(x v z)).

given clause #315: (wt=16) 932 [para_from,465,118,demod,23] (x v c(y v z))^ (y v (x v z))=x v x.

given clause #316: (wt=16) 979 [para_from,927,118] (x v (y v z))^f(c(y),x v z)=y v y.

given clause #317: (wt=19) 375 [back_demod,339,demod,367] f(x,y) v ((f(x,y) v z) v z)=c((x^y)^c(z)).

given clause #318: (wt=16) 992 [para_into,102,156] x v f(y^z,u)=f(y,z) v f(c(x),u).

given clause #319: (wt=16) 1001 [copy,992,flip.1] f(x,y) v f(c(z),u)=z v f(x^y,u).

given clause #320: (wt=16) 1041 [para_into,486,71,demod,82] c(x v f(y,z^y))=z^c(x v c(y)).

given clause #321: (wt=19) 381 [back_demod,295,demod,367] x^ (y v ((y v y) v y))= (y v y)^ (y^ (x^y)).

given clause #322: (wt=16) 1055 [copy,1041,flip.1] x^c(y v c(z))=c(y v f(z,x^z)).

given clause #323: (wt=16) 1062 [para_into,488,20] x^ ((y^z)^u)=c(f(y,z) v f(x,u)).

given clause #324: (wt=16) 1065 [para_into,488,185,demod,410] x^c(y v c(z))=c(y v f(x,z v z)).

given clause #325: (wt=19) 383 [back_demod,291,demod,367] (x v x)^ (x^ (y^x))=y^ (x v ((x v x) v x)).

given clause #326: (wt=16) 1075 [copy,1062,flip.1] c(f(x,y) v f(z,u))=z^ ((x^y)^u).

given clause #327: (wt=16) 1078 [copy,1065,flip.1] c(x v f(y,z v z))=y^c(x v c(z)).

given clause #328: (wt=16) 1156 [para_into,704,20] x v f(f(x,c(x)),y^z)=x v f(y,z).

given clause #329: (wt=17) 386 [para_from,72,41] f(x v ((c(x)^y)^y),c(c(x)^y))=c(x).

given clause #330: (wt=16) 1163 [copy,1156,flip.1] x v f(y,z)=x v f(f(x,c(x)),y^z).

given clause #331: (wt=16) 1174 [para_from,704,61,demod,21] f(x v (f(x,c(x))^c(y)),x v y)=c(x).

given clause #332: (wt=16) 1253 [para_from,155,253] f(c(x) v f(y,z),f(y,f(x v x,z)))=y.

given clause #333: (wt=17) 416 [para_from,65,41,demod,33,58,33,58] f(x v f(x v c(x),c(x)),x v c(x))=c(x).

given clause #334: (wt=16) 1259 [para_into,159,704,demod,33,58,flip.1] f(x v x,(x v c(x))^c(y))=c(x) v y.

given clause #335: (wt=16) 1287 [para_into,214,146] f(f(x,c((y v y)^x)),c(y) v c(x))=x.

given clause #336: (wt=16) 1348 [para_into,388,29] f(c(x^c(y)),f(x,f(x,c(y)) v y))=x.

given clause #337: (wt=17) 424 [para_into,118,53,demod,21,54] c(x^y)^f(x^y,f(x,y))=c(x^y).

given clause #338: (wt=16) 1417 [para_into,479,71,demod,58] f(x v f(y,z^y),f(z,x v c(y)))=z.

given clause #339: (wt=16) 1477 [para_into,700,146] (c(x) v c(y))^f(y,f(x v x,y))=c(y).

given clause #340: (wt=16) 1481 [para_into,700,65] f(f(x,c(x)),x v x)^f(x,c(x))=c(x).

given clause #341: (wt=18) 428 [para_into,118,72] (x v ((c(x)^y)^y))^c(c(x)^y)=x v x.

given clause #342: (wt=16) 1529 [para_into,802,22] f(c(x),y^c(z))^f(y,x v z)=c(y).

given clause #343: (wt=16) 1541 [para_into,802,41] f(c(x),(x v y)^y)^c(x)=c(x v y).

given clause #344: (wt=16) 1622 [para_into,1161,32] f(c(x),f(x,c(x))^ (y v y))=x v c(y).

given clause #345: (wt=18) 430 [para_into,118,65,demod,33,58,33,58] (x v f(x v c(x),c(x)))^ (x v c(x))=x v x.

given clause #346: (wt=16) 1630 [para_into,1166,32,demod,58] (x v c(x))^c(c(x) v y)=c(c(x) v y).

given clause #347: (wt=16) 1650 [para_from,1205,20,demod,52,flip.1] (c(x) v f(c(x),x))^c(x)=c(x) v c(x).

given clause #348: (wt=16) 1660 [para_into,1298,32,demod,58] (x v c(x))^c(y v c(x))=c(y v c(x)).

given clause #349: (wt=18) 432 [para_from,118,184,demod,54] f(c(x),y)^ (x v x)= (x v y)^c(c(x)^y).

given clause #350: (wt=16) 1682 [para_into,206,34] f(c(x),y^c(x))^f(x,y^x)=c(y).

given clause #351: (wt=16) 1748 [para_into,226,409] x^c(y v c(z))=z^ (c(y)^ (x^z)).

given clause #352: (wt=16) 1761 [copy,1748,flip.1] x^ (c(y)^ (z^x))=z^c(y v c(x)).

given clause #353: (wt=18) 434 [para_from,118,74,demod,54] f(f(c(x),y),x v x)=f(x v y,c(c(x)^y)).

given clause #354: (wt=16) 1854 [para_into,187,927] x v (y v f(z,u))=x v f(c(y),z^u).

given clause #355: (wt=16) 1855 [copy,1854,flip.1] x v f(c(y),z^u)=x v (y v f(z,u)).

given clause #356: (wt=16) 1898 [para_into,285,488,demod,82] x^c(y v f(z,x))=z^c(y v c(x)).

given clause #357: (wt=17) 442 [para_into,140,51] (x v (c(y) v c(y)))^ (x v (y v y))=x v x.

given clause #358: (wt=16) 1905 [copy,1898,flip.1] x^c(y v c(z))=z^c(y v f(x,z)).

given clause #359: (wt=16) 1954 [para_into,297,81] x^c(y v c(z))=c(y)^ (z^ (x^z)).

given clause #360: (wt=16) 1957 [copy,1954,flip.1] c(x)^ (y^ (z^y))=z^c(x v c(y)).

given clause #361: (wt=17) 444 [para_into,140,203,demod,52] (x v (c(y) v c(y)))^ (y v (x v y))=x v x.

given clause #362: (wt=16) 2047 [para_into,358,311,demod,419,36,54,312] f(f(x,f(x,c(x))^x),c(x^c(x)))=x.

given clause #363: (wt=16) 2089 [para_into,2081,479,demod,1224,466,21] x v f(y v c(y),y^z)=x v f(y,z).

given clause #364: (wt=16) 2100 [para_into,2081,253,demod,803,21] f(x v c(x),y^ (x^z))=f(y,x^z).

given clause #365: (wt=18) 461 [para_into,156,184] f(x,y^ (c(z) v c(z)))=z v f(x,y^c(z)).

given clause #366: (wt=12) 3168 [para_into,2100,662,demod,357] f(x v c(x),x^y)=f(x,y).

given clause #367: (wt=12) 3200 [para_into,3168,26] f(x,(x v c(x))^y)=f(x,y).

given clause #368: (wt=12) 3228 [para_from,3168,20,demod,21,flip.1] (x v c(x))^ (x^y)=x^y.

given clause #369: (wt=17) 467 [para_into,156,63,demod,157,flip.1] x v f(x v f(f(c(x),y),y),y)=f(c(x),y).

given clause #370: (wt=12) 3264 [para_from,3200,20,demod,21,flip.1] x^ ((x v c(x))^y)=x^y.

given clause #371: (wt=13) 3236 [para_into,3200,1138,flip.1] f(x,f(x,f(c(x),x)))=f(x,c(x)).

given clause #372: (wt=13) 3308 [para_into,3264,1138,flip.1] x^f(x,f(c(x),x))=x^c(x).

given clause #373: (wt=18) 470 [back_demod,315,demod,457] f(x,(c(x) v f(c(x) v y,y))^x)=c(x) v y.

given clause #374: (wt=14) 3216 [para_from,3168,253] f(f(x,y),f(x,f(x v c(x),y)))=x.

given clause #375: (wt=14) 3298 [para_from,467,1166,demod,21,468,21] f(x,c(x))^ (c(x)^y)=c(x)^y.

given clause #376: (wt=14) 3389 [para_into,3298,488] c(x v f(f(x,c(x)),y))=c(x)^y.

given clause #377: (wt=18) 472 [back_demod,309,demod,457] f(c(x) v f(c(x) v y,y),x v x)=c(x) v y.

given clause #378: (wt=13) 3430 [para_from,3389,2105,demod,3390,367,3406,3112,54,157,2198,flip.1] x v f(f(x,c(x)),y)=f(c(x),y).

given clause #379: (wt=14) 3395 [para_into,3298,77] c(x)^ (f(x,c(x))^y)=c(x)^y.

given clause #380: (wt=14) 3445 [para_into,3430,17,demod,21,flip.1] f(c(x),f(x,c(x)))=x v (x^c(x)).

given clause #381: (wt=17) 475 [para_from,156,118] (x v (c(y)^z))^ (y v f(c(x),z))=x v x.

given clause #382: (wt=14) 3455 [para_into,3430,34] f(c(x),f(x,c(x))^y)=f(c(x),y).

given clause #383: (wt=15) 3180 [para_into,3168,32,demod,157] x v f(c(x) v (x v x),y)=f(c(x),y).

given clause #384: (wt=15) 3210 [para_from,3168,75] f(f(x,c((x v c(x))^y)),f(x,y))=x.

given clause #385: (wt=19) 481 [para_from,156,53,demod,157,367] x v ((x v f(y,z)) v f(y,z))=c(y^ (c(x)^z)).

given clause #386: (wt=15) 3212 [para_from,3168,802] f(x,y)^f(x,f(x v c(x),y))=c(x).

given clause #387: (wt=15) 3234 [para_into,3200,1477,demod,33,58,60,flip.1] f(c(x),f(c(x),c(x) v x))=x v c(x).

given clause #388: (wt=15) 3330 [para_from,3236,253] f(f(x,x^f(c(x),x)),f(x,c(x)))=x.

given clause #389: (wt=19) 487 [copy,481,flip.1] c(x^ (c(y)^z))=y v ((y v f(x,z)) v f(x,z)).

given clause #390: (wt=15) 3354 [para_from,470,2081,demod,1432] f((c(x) v y) v c(c(x) v y),c(x))=x.

given clause #391: (wt=15) 3391 [para_into,3298,409,demod,21,flip.1] c(x)^f(x,c(x))=c(x v (x^c(x))).

given clause #392: (wt=15) 3432 [para_into,3430,32,demod,58,33] c(x) v f(x v c(x),y)=f(x v x,y).

given clause #393: (wt=18) 495 [para_into,348,185,demod,52,202] f(f(x v x,x^ (y^x)),x v f(y,c(x)))=y.

given clause #394: (wt=15) 3488 [para_into,3180,927] x v f(x v (c(x) v x),y)=f(c(x),y).

given clause #395: (wt=15) 3538 [para_into,3432,688,flip.1] f(x v x,f(x,f(c(x),x)))=c(x) v x.

given clause #396: (wt=14) 3578 [para_from,3538,778,demod,457,25,1395] f(f(x,x v x),c(x) v x)=x v x.

given clause #397: (wt=18) 497 [para_into,348,77] f(f(x^y,x^ (z^y)),f(z,c(x^y)))=z.

given clause #398: (wt=16) 2119 [para_into,2081,74] f(f(x,y v y) v (y^ (x^y)),c(y))=y.

given clause #399: (wt=16) 2123 [para_into,2081,71] f(f(x,y^x) v (y^ (x v x)),c(y))=y.

given clause #400: (wt=16) 2137 [para_into,2081,26] f(f(x,y^z) v (y^ (x^z)),c(y))=y.

given clause #401: (wt=17) 505 [para_into,348,20] f(f(f(x,y),z^f(x,y)),f(z,x^y))=z.

given clause #402: (wt=16) 2155 [para_into,2081,185] f(f(x,y v y) v (y^ (x^y)),c(x))=x.

given clause #403: (wt=16) 2157 [para_into,2081,184] f(f(x,y^x) v (y^ (x v x)),c(x))=x.

given clause #404: (wt=16) 2159 [para_into,2081,77] f(f(x,y^z) v (y^ (x^z)),c(x))=x.

given clause #405: (wt=17) 507 [para_into,348,29] f(f(x,(y^z)^x),f(y,z) v x)=y^z.

given clause #406: (wt=16) 2161 [para_into,2081,32] f(f(c(x),y) v (c(x)^y),x v x)=c(x).

given clause #407: (wt=16) 2193 [para_into,2105,32,demod,33] f((x v x) v (c(x) v c(x)),x v x)=c(x).

given clause #408: (wt=16) 2195 [para_into,2105,20,demod,54,21] f((x^y) v c(x^y),x^y)=f(x,y).

given clause #409: (wt=18) 509 [para_from,348,39] f(f(f(x,y^x),y^c(x)),y)=f(x,y^x).

given clause #410: (wt=16) 2207 [para_from,2105,945,flip.1] (c(x) v (x v x))^c(y v x)=c(y v x).

given clause #411: (wt=16) 2234 [para_into,2199,32,demod,33] f(c(x) v ((x v x) v c(x)),x v x)=c(x).

given clause #412: (wt=16) 2242 [para_from,2199,945,flip.1] (x v (c(x) v x))^c(y v x)=c(y v x).

given clause #413: (wt=18) 513 [para_from,348,49,demod,21,21] f(f(x,y^x),y^c(x))^y=x^ (y^x).

given clause #414: (wt=16) 2271 [para_into,2228,20,demod,54,21,21] ((x^y) v c(x^y))^ (x^y)=x^y.

given clause #415: (wt=16) 2273 [para_from,2228,356,demod,2106,2106] f(f(c(x) v (x v x),x^c(x)),c(x))=x.

given clause #416: (wt=16) 2279 [para_from,2228,77,flip.1] (c(x) v (x v x))^ (y^c(x))=y^c(x).

given clause #417: (wt=18) 522 [para_into,409,77] (x^y)^ (x^ (c(z)^y))=c(z v c(x^y)).

given clause #418: (wt=16) 2283 [para_from,2228,26] f(x,c(y))=f(c(y) v (y v y),x^c(y)).

given clause #419: (wt=16) 2284 [copy,2283,flip.1] f(c(x) v (x v x),y^c(x))=f(y,c(x)).

given clause #420: (wt=16) 2299 [para_from,2263,356,demod,2200,2200] f(f(x v (c(x) v x),x^c(x)),c(x))=x.

given clause #421: (wt=19) 526 [para_from,409,348,demod,466,33,101] f(x v (f(c(x),y) v c(y)),f(y,c(c(x)^y)))=y.

given clause #422: (wt=16) 2303 [para_from,2263,77,flip.1] (x v (c(x) v x))^ (y^c(x))=y^c(x).

given clause #423: (wt=16) 2307 [para_from,2263,26] f(x,c(y))=f(y v (c(y) v y),x^c(y)).

given clause #424: (wt=16) 2308 [copy,2307,flip.1] f(x v (c(x) v x),y^c(x))=f(y,c(x)).

given clause #425: (wt=18) 538 [para_into,75,185] f(f(x,c(y^ (z^y))),f(z,x^ (y v y)))=x.

given clause #426: (wt=16) 2309 [para_into,2181,1161,demod,1169,33,33] ((x v y) v c(x v y))^ (x v x)=x v x.

given clause #427: (wt=16) 2317 [para_into,2181,253,demod,803,21,21] (x v c(x))^ (y^ (x^z))=y^ (x^z).

given clause #428: (wt=16) 2337 [para_into,2181,41,demod,119] (c(x) v (x v x))^c(x v y)=c(x v y).

given clause #429: (wt=18) 540 [para_into,75,184] f(f(x,c(y^ (z v z))),f(z,x^ (y^z)))=x.

given clause #430: (wt=16) 2353 [para_into,2181,409,demod,157,18] ((x v c(y)) v c(x v c(y)))^c(y)=c(y).

given clause #431: (wt=16) 2575 [para_into,662,24,demod,50,50] f(f(x,c(y)),x^f(x,y))^c(x)=c(x).

given clause #432: (wt=16) 2621 [para_from,690,358,demod,1482,36,54,691] f(f(f(x,c(x)),x v x),c(x^c(x)))=x.

given clause #433: (wt=18) 546 [para_into,75,77] f(f(x,c(y^ (z^u))),f(z,x^ (y^u)))=x.

given clause #434: (wt=16) 2758 [para_into,981,201,demod,23] f(c(x) v (y v c(x)),x v (y v x))=c(y).

given clause #435: (wt=16) 3009 [para_into,2951,51] f(x,((x v x) v (c(x) v c(x)))^x)=c(x).

given clause #436: (wt=16) 3013 [para_from,2951,20,demod,33,flip.1] x^ (((x v y) v c(x v y))^x)=x v x.

given clause #437: (wt=17) 548 [para_into,75,69,demod,33] f(f(x,y v y),f(f(y,c(y)),x^c(y)))=x.

given clause #438: (wt=14) 3650 [para_into,548,3200,demod,21,3593,641,648,21] f(c(x),x)=f(x,c(x)) v (x^c(x)).

given clause #439: (wt=10) 3683 [para_from,3650,434,demod,3593,60,flip.1] c(x) v (c(x)^x)=c(x).

given clause #440: (wt=12) 3664 [back_demod,3312,demod,3663] f(x,(c(x) v x)^y)=f(x,y).

given clause #441: (wt=18) 550 [para_into,75,49,demod,33] f(f(x,y v y),f(f(y,c(z)),x^f(y,z)))=x.

given clause #442: (wt=11) 3787 [para_into,3664,74,demod,18] f(c(x) v x,x v x)=c(x).

given clause #443: (wt=12) 3666 [back_demod,3304,demod,3663] x^ ((c(x) v x)^y)=x^y.

given clause #444: (wt=12) 3668 [back_demod,3290,demod,3663] f(c(x) v x,x^y)=f(x,y).

given clause #445: (wt=19) 552 [para_into,75,37,demod,33,367] f(f(x,y v ((y v z) v z)),f(c(y),x^c(z)))=x.

given clause #446: (wt=11) 3975 [para_into,3668,684,demod,33,250] f((x v x) v c(x),c(x))=x.

given clause #447: (wt=12) 3670 [back_demod,3274,demod,3663] (c(x) v x)^ (x^y)=x^y.

given clause #448: (wt=12) 3869 [para_from,3787,354,demod,3812,flip.1] (c(x) v x)^ (x v x)=x v x.

given clause #449: (wt=19) 554 [para_into,75,29] f(f(x,y) v (z^u),f(z,(x^y)^u))=x^y.

given clause #450: (wt=12) 3955 [para_into,3668,3212,demod,21,3217] f((x^y) v f(x,y),c(x))=x.

given clause #451: (wt=12) 4048 [para_from,3975,20,flip.1] ((x v x) v c(x))^c(x)=c(x).

given clause #452: (wt=13) 3692 [para_into,3683,32,demod,33,79,33] (x v x) v c(c(x) v x)=x v x.

given clause #453: (wt=19) 556 [para_into,75,409,demod,466,33] f(f(x,c(y^ (c(z)^x))),z v f(y,x v x))=x.

given clause #454: (wt=10) 4401 [back_demod,4195,demod,4274] c(x)^x=c(x v c(x)).

----> UNIT CONFLICT at   3.31 sec ----> 4834 [binary,4832,2] $Ans(DM).

Length of proof is 145.  Level of proof is 22.

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

2 [] A^B!=c(c(A) v c(B))|$Ans(DM).
7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
8 [] f(f(x,f(y,y)),f(x,y))=x.
10 [] x v y=f(f(x,x),f(y,y)).
11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
13 [] x^y=f(f(x,y),f(x,y)).
14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
16 [] c(x)=f(x,x).
18,17 [copy,16,flip.1] f(x,x)=c(x).
19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
21,20 [back_demod,14,demod,18] c(f(x,y))=x^y.
23,22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.
24 [back_demod,8,demod,18] f(f(x,c(y)),f(x,y))=x.
26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
27 [para_into,20,17,flip.1] x^x=c(c(x)).
30,29 [para_into,22,20] f(x^y,c(z))=f(x,y) v z.
31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).
33,32 [para_into,22,17] c(c(x))=x v x.
36,35 [back_demod,27,demod,33] x^x=x v x.
38,37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).
39 [para_into,24,20] f(f(x,y^z),f(x,f(y,z)))=x.
41 [para_into,24,22] f(x v y,f(c(x),y))=c(x).
43 [para_into,24,24,demod,21] f(f(f(x,c(y)),x^y),x)=f(x,c(y)).
45 [para_into,24,22,demod,33] f(f(c(x),y v y),x v y)=c(x).
47 [para_into,24,17] f(f(x,c(x)),c(x))=x.
49 [para_from,24,20,flip.1] f(x,c(y))^f(x,y)=c(x).
52,51 [para_into,32,32] c(x v x)=c(x) v c(x).
54,53 [para_into,32,20,flip.1] f(x,y) v f(x,y)=c(x^y).
55 [para_from,32,24] f(f(x,y v y),f(x,c(y)))=x.
58,57 [para_from,32,22] f(c(x),y v y)=x v c(y).
60,59 [para_from,32,22] f(x v x,c(y))=c(x) v y.
62,61 [back_demod,45,demod,58] f(x v c(y),x v y)=c(x).
63 [para_into,47,20,demod,21] f(f(f(x,y),x^y),x^y)=f(x,y).
69 [para_from,47,20,flip.1] f(x,c(x))^c(x)=c(x).
71 [para_into,26,35] f(x,y v y)=f(y,x^y).
72 [para_into,26,17,flip.1] f(x,(x^y)^y)=c(x^y).
74 [copy,71,flip.1] f(x,y^x)=f(y,x v x).
75 [para_from,26,24] f(f(x,c(y^z)),f(y,x^z))=x.
77 [para_from,26,20,demod,21] x^ (y^z)=y^ (x^z).
79,78 [para_into,37,32] (x v x)^c(y)=c(c(x) v y).
82,81 [para_into,37,32] c(x)^ (y v y)=c(x v c(y)).
94 [para_into,69,20,demod,21,21] f(f(x,y),x^y)^ (x^y)=x^y.
96 [para_from,69,26] f(x,c(y))=f(f(y,c(y)),x^c(y)).
118 [para_from,41,20,demod,33,flip.1] (x v y)^f(c(x),y)=x v x.
122 [para_into,49,32] f(x,y v y)^f(x,c(y))=c(x).
132 [para_into,49,41,demod,21] f(x v y,c(x)^y)^c(x)=c(x v y).
141,140 [para_into,49,22,demod,33,58,33] (x v c(y))^ (x v y)=x v x.
147,146 [para_into,57,32] f(x v x,y v y)=c(x) v c(y).
155 [para_into,31,32] f(x v x,y^z)=c(x) v f(y,z).
157,156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).
161,160 [back_demod,132,demod,157] (x v f(x v y,y))^c(x)=c(x v y).
176 [para_into,71,61,flip.1] f(x,(x v c(x))^x)=c(x).
184 [para_from,71,20,demod,21] x^ (y^x)=y^ (x v x).
185 [copy,184,flip.1] x^ (y v y)=y^ (x^y).
200 [para_into,74,37,demod,23,58,33] x v (y v x)=y v (x v x).
203 [copy,200,flip.1] x v (y v y)=y v (x v y).
214 [para_from,74,24] f(f(x,c(y^x)),f(y,x v x))=x.
218 [para_into,77,77] x^ (y^ (z^u))=z^ (x^ (y^u)).
226 [copy,218,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)).
246,245 [para_from,176,20,demod,33,flip.1] x^ ((x v c(x))^x)=x v x.
250,249 [para_into,39,176] f(c(x),f(x,f(x v c(x),x)))=x.
251 [para_into,39,74] f(f(x,y v y),f(y,f(x,y)))=y.
253 [para_into,39,26] f(f(x,y^z),f(y,f(x,z)))=y.
331,330 [para_from,203,41,demod,58] f(x v (y v x),y v c(x))=c(y).
348 [para_into,55,71] f(f(x,y^x),f(y,c(x)))=y.
357,356 [para_into,63,26] f(f(x,f(x,y)^y),x^y)=f(x,y).
367,366 [para_into,72,37,demod,38,23,38,33,flip.1] (x v y) v (x v y)=x v ((x v y) v y).
373,372 [para_into,72,31] x v f(c(x)^y,y)=c(c(x)^y).
391,390 [para_from,72,49] f(x,c((x^y)^y))^c(x^y)=c(x).
392 [para_from,72,24] f(f(x,c((x^y)^y)),c(x^y))=x.
400 [para_into,78,20] (x v x)^ (y^z)=c(c(x) v f(y,z)).
401 [copy,400,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z).
409 [para_into,81,185] x^ (c(y)^x)=c(y v c(x)).
434 [para_from,118,74,demod,54] f(f(c(x),y),x v x)=f(x v y,c(c(x)^y)).
466,465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).
468,467 [para_into,156,63,demod,157,flip.1] x v f(x v f(f(c(x),y),y),y)=f(c(x),y).
469 [para_into,156,31] x v f(c(y),z)=y v f(c(x),z).
479 [para_from,156,39] f(x v f(y,z),f(y,f(c(x),z)))=y.
486 [para_from,156,20] c(x v f(y,z))=y^ (c(x)^z).
488 [copy,486,flip.1] x^ (c(y)^z)=c(y v f(x,z)).
515 [para_from,348,20,flip.1] f(x,y^x)^f(y,c(x))=c(y).
548 [para_into,75,69,demod,33] f(f(x,y v y),f(f(y,c(y)),x^c(y)))=x.
641,640 [para_from,122,74,demod,54] f(f(x,c(y)),c(x))=f(f(x,y v y),c(x^c(y))).
648,647 [back_demod,47,demod,641] f(f(x,x v x),c(x^c(x)))=x.
662 [para_into,94,26] f(x,f(x,y)^y)^ (x^y)=x^y.
684 [para_from,249,20,flip.1] c(x)^f(x,f(x v c(x),x))=c(x).
688 [para_into,251,57] f(x v c(y),f(y,f(c(x),y)))=y.
700 [para_from,251,20,flip.1] f(x,y v y)^f(y,f(x,y))=c(y).
704 [para_into,96,43,demod,23,23,157,161,466,flip.1] x v f(f(x,c(x)),c(y))=x v y.
803,802 [para_from,253,20,flip.1] f(x,y^z)^f(y,f(x,z))=c(y).
1154 [para_into,704,32] x v f(f(x,c(x)),y v y)=x v c(y).
1156 [para_into,704,20] x v f(f(x,c(x)),y^z)=x v f(y,z).
1163 [copy,1156,flip.1] x v f(y,z)=x v f(f(x,c(x)),y^z).
1166 [para_from,704,486,demod,38,flip.1] f(x,c(x))^c(x v y)=c(x v y).
1241,1240 [para_into,155,74,demod,367] f(x,y v ((y v y) v y))=c(y) v f(x,y v y).
1291 [para_into,214,57] f(f(x,c(c(y)^x)),y v c(x))=x.
1456,1455 [para_from,684,77,flip.1] c(x)^ (y^f(x,f(x v c(x),x)))=y^c(x).
1477 [para_into,700,146] (c(x) v c(y))^f(y,f(x v x,y))=c(y).
2081 [para_into,392,96,demod,30,391] f(f(x,y) v (x^y),c(x))=x.
2100 [para_into,2081,253,demod,803,21] f(x v c(x),y^ (x^z))=f(y,x^z).
2105 [para_into,2081,176,demod,246] f(c(x) v (x v x),c(x))=x.
2119 [para_into,2081,74] f(f(x,y v y) v (y^ (x^y)),c(y))=y.
2137 [para_into,2081,26] f(f(x,y^z) v (y^ (x^z)),c(y))=y.
2198,2197 [para_into,2105,469,demod,21,21,373,21,157] x v f((c(x)^y) v c(c(x)^y),y)=f(c(x),y).
2817 [para_into,1154,71] x v f(y,f(x,c(x))^y)=x v c(y).
2981 [para_from,2817,401,demod,33,58,flip.1] (x v x)^ (y^ ((x v c(x))^y))=c(c(x) v c(y)).
3112,3111 [para_into,1163,469,demod,157,flip.1] x v (y v f(f(x,c(x)),z))=y v f(c(x),z).
3169,3168 [para_into,2100,662,demod,357] f(x v c(x),x^y)=f(x,y).
3201,3200 [para_into,3168,26] f(x,(x v c(x))^y)=f(x,y).
3228 [para_from,3168,20,demod,21,flip.1] (x v c(x))^ (x^y)=x^y.
3264 [para_from,3200,20,demod,21,flip.1] x^ ((x v c(x))^y)=x^y.
3283,3282 [para_into,3228,226] x^ (y^ ((x v c(x))^z))=x^ (y^z).
3290 [para_from,3228,3168,demod,3169] f((x v c(x)) v c(x v c(x)),x^y)=f(x,y).
3298 [para_from,467,1166,demod,21,468,21] f(x,c(x))^ (c(x)^y)=c(x)^y.
3306 [para_into,3264,1477,demod,33,82,60,flip.1] c(x)^f(c(x),c(x) v x)=c(x v c(x)).
3312 [para_from,3264,3200,demod,3201,flip.1] f(x,((x v c(x)) v c(x v c(x)))^y)=f(x,y).
3390,3389 [para_into,3298,488] c(x v f(f(x,c(x)),y))=c(x)^y.
3406,3405 [para_from,3298,29,demod,30,157,flip.1] (x v f(f(x,c(x)),y)) v z=f(c(x),y) v z.
3430 [para_from,3389,2105,demod,3390,367,3406,3112,54,157,2198,flip.1] x v f(f(x,c(x)),y)=f(c(x),y).
3432 [para_into,3430,32,demod,58,33] c(x) v f(x v c(x),y)=f(x v x,y).
3538 [para_into,3432,688,flip.1] f(x v x,f(x,f(c(x),x)))=c(x) v x.
3580 [para_from,3538,479,demod,33,60,62,33,33] f(x v (x v x),(x v x) v c(x))=c(x) v c(x).
3593,3592 [para_into,2137,684,demod,1456,33] f(f(x,c(y)) v (x^c(y)),y v y)=c(y).
3650 [para_into,548,3200,demod,21,3593,641,648,21] f(c(x),x)=f(x,c(x)) v (x^c(x)).
3663,3662 [para_into,3650,32,demod,60,33,58,33,82,flip.1] (x v c(x)) v c(x v c(x))=c(x) v x.
3664 [back_demod,3312,demod,3663] f(x,(c(x) v x)^y)=f(x,y).
3668 [back_demod,3290,demod,3663] f(c(x) v x,x^y)=f(x,y).
3683 [para_from,3650,434,demod,3593,60,flip.1] c(x) v (c(x)^x)=c(x).
3692 [para_into,3683,32,demod,33,79,33] (x v x) v c(c(x) v x)=x v x.
3748,3747 [para_into,3664,32] f(c(x),((x v x) v c(x))^y)=f(c(x),y).
3788,3787 [para_into,3664,74,demod,18] f(c(x) v x,x v x)=c(x).
3809 [para_from,3664,515,demod,18] c(x)^f(c(x) v x,c(x))=c(c(x) v x).
3871 [para_from,3787,251] f(c(x),f(x,f(c(x) v x,x)))=x.
3976,3975 [para_into,3668,684,demod,33,250] f((x v x) v c(x),c(x))=x.
4022 [para_from,3975,55] f(f((x v x) v c(x),x v x),x)= (x v x) v c(x).
4029,4028 [para_from,3975,24] f(x,f((x v x) v c(x),x))= (x v x) v c(x).
4192,4191 [para_from,3692,1291,demod,52,141,52,33,33,367,1241,3788,147,33,flip.1] c(x) v x= (x v x) v c(x).
4196,4195 [back_demod,3809,demod,4192,3976,4192] c(x)^x=c((x v x) v c(x)).
4214,4213 [back_demod,3871,demod,4192,4029] f(c(x),(x v x) v c(x))=x.
4236,4235 [back_demod,3787,demod,4192] f((x v x) v c(x),x v x)=c(x).
4252,4251 [back_demod,3662,demod,4192] (x v c(x)) v c(x v c(x))= (x v x) v c(x).
4274,4273 [back_demod,3306,demod,4192,4214,4196] c((x v x) v c(x))=c(x v c(x)).
4300,4299 [back_demod,4022,demod,4236] f(c(x),x)= (x v x) v c(x).
4401 [back_demod,4195,demod,4274] c(x)^x=c(x v c(x)).
4446,4445 [para_from,4401,409] x^c(x v c(x))=c(x v c(x)).
4501,4500 [para_from,4401,356,demod,4300,3748,4300,466,33,4236,4300,flip.1] (x v x) v c(x)=x v c(x).
4503,4502 [para_from,4401,2119,demod,58,4446,4252,4501] f(x v c(x),c(x))=x.
4512 [para_from,4401,43,demod,18,33,466,33,18,52,18,33] f(x v (c(x) v c(x)),c(x))=x v x.
4610,4609 [back_demod,3580,demod,4501,331,flip.1] c(x) v c(x)=c(x).
4647,4646 [back_demod,4512,demod,4610,4503,flip.1] x v x=x.
4832 [back_demod,2981,demod,4647,3283,36,4647] x^y=c(c(x) v c(y)).
4834 [binary,4832,2] $Ans(DM).

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


----> UNIT CONFLICT at   3.31 sec ----> 4846 [binary,4844,5] $Ans(DEF_SS).

Length of proof is 150.  Level of proof is 23.

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

5 [] f(A,B)!=c(A) v c(B)|$Ans(DEF_SS).
7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
8 [] f(f(x,f(y,y)),f(x,y))=x.
10 [] x v y=f(f(x,x),f(y,y)).
11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
13 [] x^y=f(f(x,y),f(x,y)).
14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
16 [] c(x)=f(x,x).
18,17 [copy,16,flip.1] f(x,x)=c(x).
19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
21,20 [back_demod,14,demod,18] c(f(x,y))=x^y.
23,22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.
24 [back_demod,8,demod,18] f(f(x,c(y)),f(x,y))=x.
26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
27 [para_into,20,17,flip.1] x^x=c(c(x)).
30,29 [para_into,22,20] f(x^y,c(z))=f(x,y) v z.
31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).
33,32 [para_into,22,17] c(c(x))=x v x.
36,35 [back_demod,27,demod,33] x^x=x v x.
38,37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).
39 [para_into,24,20] f(f(x,y^z),f(x,f(y,z)))=x.
41 [para_into,24,22] f(x v y,f(c(x),y))=c(x).
43 [para_into,24,24,demod,21] f(f(f(x,c(y)),x^y),x)=f(x,c(y)).
45 [para_into,24,22,demod,33] f(f(c(x),y v y),x v y)=c(x).
47 [para_into,24,17] f(f(x,c(x)),c(x))=x.
49 [para_from,24,20,flip.1] f(x,c(y))^f(x,y)=c(x).
52,51 [para_into,32,32] c(x v x)=c(x) v c(x).
54,53 [para_into,32,20,flip.1] f(x,y) v f(x,y)=c(x^y).
55 [para_from,32,24] f(f(x,y v y),f(x,c(y)))=x.
58,57 [para_from,32,22] f(c(x),y v y)=x v c(y).
60,59 [para_from,32,22] f(x v x,c(y))=c(x) v y.
62,61 [back_demod,45,demod,58] f(x v c(y),x v y)=c(x).
63 [para_into,47,20,demod,21] f(f(f(x,y),x^y),x^y)=f(x,y).
69 [para_from,47,20,flip.1] f(x,c(x))^c(x)=c(x).
71 [para_into,26,35] f(x,y v y)=f(y,x^y).
72 [para_into,26,17,flip.1] f(x,(x^y)^y)=c(x^y).
74 [copy,71,flip.1] f(x,y^x)=f(y,x v x).
75 [para_from,26,24] f(f(x,c(y^z)),f(y,x^z))=x.
77 [para_from,26,20,demod,21] x^ (y^z)=y^ (x^z).
79,78 [para_into,37,32] (x v x)^c(y)=c(c(x) v y).
82,81 [para_into,37,32] c(x)^ (y v y)=c(x v c(y)).
94 [para_into,69,20,demod,21,21] f(f(x,y),x^y)^ (x^y)=x^y.
96 [para_from,69,26] f(x,c(y))=f(f(y,c(y)),x^c(y)).
102 [para_into,29,20] f(x^y,z^u)=f(x,y) v f(z,u).
118 [para_from,41,20,demod,33,flip.1] (x v y)^f(c(x),y)=x v x.
122 [para_into,49,32] f(x,y v y)^f(x,c(y))=c(x).
132 [para_into,49,41,demod,21] f(x v y,c(x)^y)^c(x)=c(x v y).
141,140 [para_into,49,22,demod,33,58,33] (x v c(y))^ (x v y)=x v x.
147,146 [para_into,57,32] f(x v x,y v y)=c(x) v c(y).
155 [para_into,31,32] f(x v x,y^z)=c(x) v f(y,z).
157,156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).
161,160 [back_demod,132,demod,157] (x v f(x v y,y))^c(x)=c(x v y).
176 [para_into,71,61,flip.1] f(x,(x v c(x))^x)=c(x).
184 [para_from,71,20,demod,21] x^ (y^x)=y^ (x v x).
185 [copy,184,flip.1] x^ (y v y)=y^ (x^y).
200 [para_into,74,37,demod,23,58,33] x v (y v x)=y v (x v x).
203 [copy,200,flip.1] x v (y v y)=y v (x v y).
214 [para_from,74,24] f(f(x,c(y^x)),f(y,x v x))=x.
218 [para_into,77,77] x^ (y^ (z^u))=z^ (x^ (y^u)).
226 [copy,218,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)).
246,245 [para_from,176,20,demod,33,flip.1] x^ ((x v c(x))^x)=x v x.
250,249 [para_into,39,176] f(c(x),f(x,f(x v c(x),x)))=x.
251 [para_into,39,74] f(f(x,y v y),f(y,f(x,y)))=y.
253 [para_into,39,26] f(f(x,y^z),f(y,f(x,z)))=y.
279 [para_from,184,74] f(x^y,x^ (y v y))=f(y,(x^y) v (x^y)).
331,330 [para_from,203,41,demod,58] f(x v (y v x),y v c(x))=c(y).
348 [para_into,55,71] f(f(x,y^x),f(y,c(x)))=y.
357,356 [para_into,63,26] f(f(x,f(x,y)^y),x^y)=f(x,y).
367,366 [para_into,72,37,demod,38,23,38,33,flip.1] (x v y) v (x v y)=x v ((x v y) v y).
373,372 [para_into,72,31] x v f(c(x)^y,y)=c(c(x)^y).
391,390 [para_from,72,49] f(x,c((x^y)^y))^c(x^y)=c(x).
392 [para_from,72,24] f(f(x,c((x^y)^y)),c(x^y))=x.
400 [para_into,78,20] (x v x)^ (y^z)=c(c(x) v f(y,z)).
401 [copy,400,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z).
409 [para_into,81,185] x^ (c(y)^x)=c(y v c(x)).
434 [para_from,118,74,demod,54] f(f(c(x),y),x v x)=f(x v y,c(c(x)^y)).
466,465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).
468,467 [para_into,156,63,demod,157,flip.1] x v f(x v f(f(c(x),y),y),y)=f(c(x),y).
469 [para_into,156,31] x v f(c(y),z)=y v f(c(x),z).
479 [para_from,156,39] f(x v f(y,z),f(y,f(c(x),z)))=y.
486 [para_from,156,20] c(x v f(y,z))=y^ (c(x)^z).
488 [copy,486,flip.1] x^ (c(y)^z)=c(y v f(x,z)).
515 [para_from,348,20,flip.1] f(x,y^x)^f(y,c(x))=c(y).
548 [para_into,75,69,demod,33] f(f(x,y v y),f(f(y,c(y)),x^c(y)))=x.
641,640 [para_from,122,74,demod,54] f(f(x,c(y)),c(x))=f(f(x,y v y),c(x^c(y))).
648,647 [back_demod,47,demod,641] f(f(x,x v x),c(x^c(x)))=x.
662 [para_into,94,26] f(x,f(x,y)^y)^ (x^y)=x^y.
684 [para_from,249,20,flip.1] c(x)^f(x,f(x v c(x),x))=c(x).
688 [para_into,251,57] f(x v c(y),f(y,f(c(x),y)))=y.
700 [para_from,251,20,flip.1] f(x,y v y)^f(y,f(x,y))=c(y).
704 [para_into,96,43,demod,23,23,157,161,466,flip.1] x v f(f(x,c(x)),c(y))=x v y.
803,802 [para_from,253,20,flip.1] f(x,y^z)^f(y,f(x,z))=c(y).
1154 [para_into,704,32] x v f(f(x,c(x)),y v y)=x v c(y).
1156 [para_into,704,20] x v f(f(x,c(x)),y^z)=x v f(y,z).
1163 [copy,1156,flip.1] x v f(y,z)=x v f(f(x,c(x)),y^z).
1166 [para_from,704,486,demod,38,flip.1] f(x,c(x))^c(x v y)=c(x v y).
1241,1240 [para_into,155,74,demod,367] f(x,y v ((y v y) v y))=c(y) v f(x,y v y).
1291 [para_into,214,57] f(f(x,c(c(y)^x)),y v c(x))=x.
1456,1455 [para_from,684,77,flip.1] c(x)^ (y^f(x,f(x v c(x),x)))=y^c(x).
1477 [para_into,700,146] (c(x) v c(y))^f(y,f(x v x,y))=c(y).
2081 [para_into,392,96,demod,30,391] f(f(x,y) v (x^y),c(x))=x.
2100 [para_into,2081,253,demod,803,21] f(x v c(x),y^ (x^z))=f(y,x^z).
2105 [para_into,2081,176,demod,246] f(c(x) v (x v x),c(x))=x.
2119 [para_into,2081,74] f(f(x,y v y) v (y^ (x^y)),c(y))=y.
2137 [para_into,2081,26] f(f(x,y^z) v (y^ (x^z)),c(y))=y.
2198,2197 [para_into,2105,469,demod,21,21,373,21,157] x v f((c(x)^y) v c(c(x)^y),y)=f(c(x),y).
2817 [para_into,1154,71] x v f(y,f(x,c(x))^y)=x v c(y).
2935 [para_into,279,102] f(x,y) v f(x,y v y)=f(y,(x^y) v (x^y)).
2936 [copy,2935,flip.1] f(x,(y^x) v (y^x))=f(y,x) v f(y,x v x).
2981 [para_from,2817,401,demod,33,58,flip.1] (x v x)^ (y^ ((x v c(x))^y))=c(c(x) v c(y)).
3112,3111 [para_into,1163,469,demod,157,flip.1] x v (y v f(f(x,c(x)),z))=y v f(c(x),z).
3169,3168 [para_into,2100,662,demod,357] f(x v c(x),x^y)=f(x,y).
3201,3200 [para_into,3168,26] f(x,(x v c(x))^y)=f(x,y).
3228 [para_from,3168,20,demod,21,flip.1] (x v c(x))^ (x^y)=x^y.
3264 [para_from,3200,20,demod,21,flip.1] x^ ((x v c(x))^y)=x^y.
3283,3282 [para_into,3228,226] x^ (y^ ((x v c(x))^z))=x^ (y^z).
3290 [para_from,3228,3168,demod,3169] f((x v c(x)) v c(x v c(x)),x^y)=f(x,y).
3298 [para_from,467,1166,demod,21,468,21] f(x,c(x))^ (c(x)^y)=c(x)^y.
3306 [para_into,3264,1477,demod,33,82,60,flip.1] c(x)^f(c(x),c(x) v x)=c(x v c(x)).
3312 [para_from,3264,3200,demod,3201,flip.1] f(x,((x v c(x)) v c(x v c(x)))^y)=f(x,y).
3390,3389 [para_into,3298,488] c(x v f(f(x,c(x)),y))=c(x)^y.
3406,3405 [para_from,3298,29,demod,30,157,flip.1] (x v f(f(x,c(x)),y)) v z=f(c(x),y) v z.
3430 [para_from,3389,2105,demod,3390,367,3406,3112,54,157,2198,flip.1] x v f(f(x,c(x)),y)=f(c(x),y).
3432 [para_into,3430,32,demod,58,33] c(x) v f(x v c(x),y)=f(x v x,y).
3538 [para_into,3432,688,flip.1] f(x v x,f(x,f(c(x),x)))=c(x) v x.
3580 [para_from,3538,479,demod,33,60,62,33,33] f(x v (x v x),(x v x) v c(x))=c(x) v c(x).
3593,3592 [para_into,2137,684,demod,1456,33] f(f(x,c(y)) v (x^c(y)),y v y)=c(y).
3650 [para_into,548,3200,demod,21,3593,641,648,21] f(c(x),x)=f(x,c(x)) v (x^c(x)).
3663,3662 [para_into,3650,32,demod,60,33,58,33,82,flip.1] (x v c(x)) v c(x v c(x))=c(x) v x.
3664 [back_demod,3312,demod,3663] f(x,(c(x) v x)^y)=f(x,y).
3668 [back_demod,3290,demod,3663] f(c(x) v x,x^y)=f(x,y).
3683 [para_from,3650,434,demod,3593,60,flip.1] c(x) v (c(x)^x)=c(x).
3692 [para_into,3683,32,demod,33,79,33] (x v x) v c(c(x) v x)=x v x.
3748,3747 [para_into,3664,32] f(c(x),((x v x) v c(x))^y)=f(c(x),y).
3788,3787 [para_into,3664,74,demod,18] f(c(x) v x,x v x)=c(x).
3809 [para_from,3664,515,demod,18] c(x)^f(c(x) v x,c(x))=c(c(x) v x).
3871 [para_from,3787,251] f(c(x),f(x,f(c(x) v x,x)))=x.
3976,3975 [para_into,3668,684,demod,33,250] f((x v x) v c(x),c(x))=x.
4022 [para_from,3975,55] f(f((x v x) v c(x),x v x),x)= (x v x) v c(x).
4029,4028 [para_from,3975,24] f(x,f((x v x) v c(x),x))= (x v x) v c(x).
4192,4191 [para_from,3692,1291,demod,52,141,52,33,33,367,1241,3788,147,33,flip.1] c(x) v x= (x v x) v c(x).
4196,4195 [back_demod,3809,demod,4192,3976,4192] c(x)^x=c((x v x) v c(x)).
4214,4213 [back_demod,3871,demod,4192,4029] f(c(x),(x v x) v c(x))=x.
4236,4235 [back_demod,3787,demod,4192] f((x v x) v c(x),x v x)=c(x).
4252,4251 [back_demod,3662,demod,4192] (x v c(x)) v c(x v c(x))= (x v x) v c(x).
4274,4273 [back_demod,3306,demod,4192,4214,4196] c((x v x) v c(x))=c(x v c(x)).
4300,4299 [back_demod,4022,demod,4236] f(c(x),x)= (x v x) v c(x).
4401 [back_demod,4195,demod,4274] c(x)^x=c(x v c(x)).
4446,4445 [para_from,4401,409] x^c(x v c(x))=c(x v c(x)).
4501,4500 [para_from,4401,356,demod,4300,3748,4300,466,33,4236,4300,flip.1] (x v x) v c(x)=x v c(x).
4503,4502 [para_from,4401,2119,demod,58,4446,4252,4501] f(x v c(x),c(x))=x.
4512 [para_from,4401,43,demod,18,33,466,33,18,52,18,33] f(x v (c(x) v c(x)),c(x))=x v x.
4610,4609 [back_demod,3580,demod,4501,331,flip.1] c(x) v c(x)=c(x).
4647,4646 [back_demod,4512,demod,4610,4503,flip.1] x v x=x.
4833,4832 [back_demod,2981,demod,4647,3283,36,4647] x^y=c(c(x) v c(y)).
4844 [back_demod,2936,demod,4833,4833,4647,466,33,4647,18,4647,4647,flip.1] f(x,y)=c(x) v c(y).
4846 [binary,4844,5] $Ans(DEF_SS).

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


----> UNIT CONFLICT at   3.35 sec ----> 4907 [binary,4905,4] $Ans(CUT_rewritten).

Length of proof is 154.  Level of proof is 23.

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

4 [] c(c(A v c(B)) v c(A v B))!=A|$Ans(CUT_rewritten).
7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
8 [] f(f(x,f(y,y)),f(x,y))=x.
10 [] x v y=f(f(x,x),f(y,y)).
11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
13 [] x^y=f(f(x,y),f(x,y)).
14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
16 [] c(x)=f(x,x).
18,17 [copy,16,flip.1] f(x,x)=c(x).
19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
21,20 [back_demod,14,demod,18] c(f(x,y))=x^y.
23,22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.
24 [back_demod,8,demod,18] f(f(x,c(y)),f(x,y))=x.
26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
27 [para_into,20,17,flip.1] x^x=c(c(x)).
30,29 [para_into,22,20] f(x^y,c(z))=f(x,y) v z.
31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).
33,32 [para_into,22,17] c(c(x))=x v x.
36,35 [back_demod,27,demod,33] x^x=x v x.
38,37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).
39 [para_into,24,20] f(f(x,y^z),f(x,f(y,z)))=x.
41 [para_into,24,22] f(x v y,f(c(x),y))=c(x).
43 [para_into,24,24,demod,21] f(f(f(x,c(y)),x^y),x)=f(x,c(y)).
45 [para_into,24,22,demod,33] f(f(c(x),y v y),x v y)=c(x).
47 [para_into,24,17] f(f(x,c(x)),c(x))=x.
49 [para_from,24,20,flip.1] f(x,c(y))^f(x,y)=c(x).
52,51 [para_into,32,32] c(x v x)=c(x) v c(x).
54,53 [para_into,32,20,flip.1] f(x,y) v f(x,y)=c(x^y).
55 [para_from,32,24] f(f(x,y v y),f(x,c(y)))=x.
58,57 [para_from,32,22] f(c(x),y v y)=x v c(y).
60,59 [para_from,32,22] f(x v x,c(y))=c(x) v y.
62,61 [back_demod,45,demod,58] f(x v c(y),x v y)=c(x).
63 [para_into,47,20,demod,21] f(f(f(x,y),x^y),x^y)=f(x,y).
69 [para_from,47,20,flip.1] f(x,c(x))^c(x)=c(x).
71 [para_into,26,35] f(x,y v y)=f(y,x^y).
72 [para_into,26,17,flip.1] f(x,(x^y)^y)=c(x^y).
74 [copy,71,flip.1] f(x,y^x)=f(y,x v x).
75 [para_from,26,24] f(f(x,c(y^z)),f(y,x^z))=x.
77 [para_from,26,20,demod,21] x^ (y^z)=y^ (x^z).
79,78 [para_into,37,32] (x v x)^c(y)=c(c(x) v y).
82,81 [para_into,37,32] c(x)^ (y v y)=c(x v c(y)).
94 [para_into,69,20,demod,21,21] f(f(x,y),x^y)^ (x^y)=x^y.
96 [para_from,69,26] f(x,c(y))=f(f(y,c(y)),x^c(y)).
118 [para_from,41,20,demod,33,flip.1] (x v y)^f(c(x),y)=x v x.
122 [para_into,49,32] f(x,y v y)^f(x,c(y))=c(x).
132 [para_into,49,41,demod,21] f(x v y,c(x)^y)^c(x)=c(x v y).
141,140 [para_into,49,22,demod,33,58,33] (x v c(y))^ (x v y)=x v x.
147,146 [para_into,57,32] f(x v x,y v y)=c(x) v c(y).
155 [para_into,31,32] f(x v x,y^z)=c(x) v f(y,z).
157,156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).
161,160 [back_demod,132,demod,157] (x v f(x v y,y))^c(x)=c(x v y).
176 [para_into,71,61,flip.1] f(x,(x v c(x))^x)=c(x).
184 [para_from,71,20,demod,21] x^ (y^x)=y^ (x v x).
185 [copy,184,flip.1] x^ (y v y)=y^ (x^y).
200 [para_into,74,37,demod,23,58,33] x v (y v x)=y v (x v x).
203 [copy,200,flip.1] x v (y v y)=y v (x v y).
214 [para_from,74,24] f(f(x,c(y^x)),f(y,x v x))=x.
218 [para_into,77,77] x^ (y^ (z^u))=z^ (x^ (y^u)).
226 [copy,218,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)).
246,245 [para_from,176,20,demod,33,flip.1] x^ ((x v c(x))^x)=x v x.
250,249 [para_into,39,176] f(c(x),f(x,f(x v c(x),x)))=x.
251 [para_into,39,74] f(f(x,y v y),f(y,f(x,y)))=y.
253 [para_into,39,26] f(f(x,y^z),f(y,f(x,z)))=y.
331,330 [para_from,203,41,demod,58] f(x v (y v x),y v c(x))=c(y).
338,337 [para_into,53,71] f(x,y^x) v f(y,x v x)=c(y^ (x v x)).
342 [para_into,53,74,demod,338] c(x^ (y v y))=c(y^ (x^y)).
348 [para_into,55,71] f(f(x,y^x),f(y,c(x)))=y.
357,356 [para_into,63,26] f(f(x,f(x,y)^y),x^y)=f(x,y).
367,366 [para_into,72,37,demod,38,23,38,33,flip.1] (x v y) v (x v y)=x v ((x v y) v y).
373,372 [para_into,72,31] x v f(c(x)^y,y)=c(c(x)^y).
391,390 [para_from,72,49] f(x,c((x^y)^y))^c(x^y)=c(x).
392 [para_from,72,24] f(f(x,c((x^y)^y)),c(x^y))=x.
400 [para_into,78,20] (x v x)^ (y^z)=c(c(x) v f(y,z)).
401 [copy,400,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z).
409 [para_into,81,185] x^ (c(y)^x)=c(y v c(x)).
420 [para_into,118,203,demod,58] (x v (y v x))^ (y v c(x))=y v y.
434 [para_from,118,74,demod,54] f(f(c(x),y),x v x)=f(x v y,c(c(x)^y)).
466,465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).
468,467 [para_into,156,63,demod,157,flip.1] x v f(x v f(f(c(x),y),y),y)=f(c(x),y).
469 [para_into,156,31] x v f(c(y),z)=y v f(c(x),z).
479 [para_from,156,39] f(x v f(y,z),f(y,f(c(x),z)))=y.
486 [para_from,156,20] c(x v f(y,z))=y^ (c(x)^z).
488 [copy,486,flip.1] x^ (c(y)^z)=c(y v f(x,z)).
515 [para_from,348,20,flip.1] f(x,y^x)^f(y,c(x))=c(y).
548 [para_into,75,69,demod,33] f(f(x,y v y),f(f(y,c(y)),x^c(y)))=x.
641,640 [para_from,122,74,demod,54] f(f(x,c(y)),c(x))=f(f(x,y v y),c(x^c(y))).
648,647 [back_demod,47,demod,641] f(f(x,x v x),c(x^c(x)))=x.
662 [para_into,94,26] f(x,f(x,y)^y)^ (x^y)=x^y.
684 [para_from,249,20,flip.1] c(x)^f(x,f(x v c(x),x))=c(x).
688 [para_into,251,57] f(x v c(y),f(y,f(c(x),y)))=y.
700 [para_from,251,20,flip.1] f(x,y v y)^f(y,f(x,y))=c(y).
704 [para_into,96,43,demod,23,23,157,161,466,flip.1] x v f(f(x,c(x)),c(y))=x v y.
803,802 [para_from,253,20,flip.1] f(x,y^z)^f(y,f(x,z))=c(y).
868 [para_from,342,22,demod,23] (x^ (y^x)) v z= (y^ (x v x)) v z.
1154 [para_into,704,32] x v f(f(x,c(x)),y v y)=x v c(y).
1156 [para_into,704,20] x v f(f(x,c(x)),y^z)=x v f(y,z).
1163 [copy,1156,flip.1] x v f(y,z)=x v f(f(x,c(x)),y^z).
1166 [para_from,704,486,demod,38,flip.1] f(x,c(x))^c(x v y)=c(x v y).
1241,1240 [para_into,155,74,demod,367] f(x,y v ((y v y) v y))=c(y) v f(x,y v y).
1291 [para_into,214,57] f(f(x,c(c(y)^x)),y v c(x))=x.
1384 [para_into,420,32] (c(x) v (y v c(x)))^ (y v (x v x))=y v y.
1456,1455 [para_from,684,77,flip.1] c(x)^ (y^f(x,f(x v c(x),x)))=y^c(x).
1477 [para_into,700,146] (c(x) v c(y))^f(y,f(x v x,y))=c(y).
2081 [para_into,392,96,demod,30,391] f(f(x,y) v (x^y),c(x))=x.
2100 [para_into,2081,253,demod,803,21] f(x v c(x),y^ (x^z))=f(y,x^z).
2105 [para_into,2081,176,demod,246] f(c(x) v (x v x),c(x))=x.
2119 [para_into,2081,74] f(f(x,y v y) v (y^ (x^y)),c(y))=y.
2137 [para_into,2081,26] f(f(x,y^z) v (y^ (x^z)),c(y))=y.
2198,2197 [para_into,2105,469,demod,21,21,373,21,157] x v f((c(x)^y) v c(c(x)^y),y)=f(c(x),y).
2648 [para_into,868,37,demod,38,82,33] c(x v (y v x)) v z=c(y v (x v x)) v z.
2652 [copy,2648,flip.1] c(x v (y v y)) v z=c(y v (x v y)) v z.
2817 [para_into,1154,71] x v f(y,f(x,c(x))^y)=x v c(y).
2981 [para_from,2817,401,demod,33,58,flip.1] (x v x)^ (y^ ((x v c(x))^y))=c(c(x) v c(y)).
3112,3111 [para_into,1163,469,demod,157,flip.1] x v (y v f(f(x,c(x)),z))=y v f(c(x),z).
3169,3168 [para_into,2100,662,demod,357] f(x v c(x),x^y)=f(x,y).
3201,3200 [para_into,3168,26] f(x,(x v c(x))^y)=f(x,y).
3228 [para_from,3168,20,demod,21,flip.1] (x v c(x))^ (x^y)=x^y.
3264 [para_from,3200,20,demod,21,flip.1] x^ ((x v c(x))^y)=x^y.
3283,3282 [para_into,3228,226] x^ (y^ ((x v c(x))^z))=x^ (y^z).
3290 [para_from,3228,3168,demod,3169] f((x v c(x)) v c(x v c(x)),x^y)=f(x,y).
3298 [para_from,467,1166,demod,21,468,21] f(x,c(x))^ (c(x)^y)=c(x)^y.
3306 [para_into,3264,1477,demod,33,82,60,flip.1] c(x)^f(c(x),c(x) v x)=c(x v c(x)).
3312 [para_from,3264,3200,demod,3201,flip.1] f(x,((x v c(x)) v c(x v c(x)))^y)=f(x,y).
3390,3389 [para_into,3298,488] c(x v f(f(x,c(x)),y))=c(x)^y.
3406,3405 [para_from,3298,29,demod,30,157,flip.1] (x v f(f(x,c(x)),y)) v z=f(c(x),y) v z.
3430 [para_from,3389,2105,demod,3390,367,3406,3112,54,157,2198,flip.1] x v f(f(x,c(x)),y)=f(c(x),y).
3432 [para_into,3430,32,demod,58,33] c(x) v f(x v c(x),y)=f(x v x,y).
3538 [para_into,3432,688,flip.1] f(x v x,f(x,f(c(x),x)))=c(x) v x.
3580 [para_from,3538,479,demod,33,60,62,33,33] f(x v (x v x),(x v x) v c(x))=c(x) v c(x).
3593,3592 [para_into,2137,684,demod,1456,33] f(f(x,c(y)) v (x^c(y)),y v y)=c(y).
3650 [para_into,548,3200,demod,21,3593,641,648,21] f(c(x),x)=f(x,c(x)) v (x^c(x)).
3663,3662 [para_into,3650,32,demod,60,33,58,33,82,flip.1] (x v c(x)) v c(x v c(x))=c(x) v x.
3664 [back_demod,3312,demod,3663] f(x,(c(x) v x)^y)=f(x,y).
3668 [back_demod,3290,demod,3663] f(c(x) v x,x^y)=f(x,y).
3683 [para_from,3650,434,demod,3593,60,flip.1] c(x) v (c(x)^x)=c(x).
3692 [para_into,3683,32,demod,33,79,33] (x v x) v c(c(x) v x)=x v x.
3748,3747 [para_into,3664,32] f(c(x),((x v x) v c(x))^y)=f(c(x),y).
3788,3787 [para_into,3664,74,demod,18] f(c(x) v x,x v x)=c(x).
3809 [para_from,3664,515,demod,18] c(x)^f(c(x) v x,c(x))=c(c(x) v x).
3871 [para_from,3787,251] f(c(x),f(x,f(c(x) v x,x)))=x.
3976,3975 [para_into,3668,684,demod,33,250] f((x v x) v c(x),c(x))=x.
4022 [para_from,3975,55] f(f((x v x) v c(x),x v x),x)= (x v x) v c(x).
4029,4028 [para_from,3975,24] f(x,f((x v x) v c(x),x))= (x v x) v c(x).
4192,4191 [para_from,3692,1291,demod,52,141,52,33,33,367,1241,3788,147,33,flip.1] c(x) v x= (x v x) v c(x).
4196,4195 [back_demod,3809,demod,4192,3976,4192] c(x)^x=c((x v x) v c(x)).
4214,4213 [back_demod,3871,demod,4192,4029] f(c(x),(x v x) v c(x))=x.
4236,4235 [back_demod,3787,demod,4192] f((x v x) v c(x),x v x)=c(x).
4252,4251 [back_demod,3662,demod,4192] (x v c(x)) v c(x v c(x))= (x v x) v c(x).
4274,4273 [back_demod,3306,demod,4192,4214,4196] c((x v x) v c(x))=c(x v c(x)).
4300,4299 [back_demod,4022,demod,4236] f(c(x),x)= (x v x) v c(x).
4401 [back_demod,4195,demod,4274] c(x)^x=c(x v c(x)).
4446,4445 [para_from,4401,409] x^c(x v c(x))=c(x v c(x)).
4501,4500 [para_from,4401,356,demod,4300,3748,4300,466,33,4236,4300,flip.1] (x v x) v c(x)=x v c(x).
4503,4502 [para_from,4401,2119,demod,58,4446,4252,4501] f(x v c(x),c(x))=x.
4512 [para_from,4401,43,demod,18,33,466,33,18,52,18,33] f(x v (c(x) v c(x)),c(x))=x v x.
4610,4609 [back_demod,3580,demod,4501,331,flip.1] c(x) v c(x)=c(x).
4647,4646 [back_demod,4512,demod,4610,4503,flip.1] x v x=x.
4833,4832 [back_demod,2981,demod,4647,3283,36,4647] x^y=c(c(x) v c(y)).
4850,4849 [back_demod,2652,demod,4647,flip.1] c(x v (y v x)) v z=c(y v x) v z.
4905 [back_demod,1384,demod,4647,4833,4850,4647] c(c(x v c(y)) v c(x v y))=x.
4907 [binary,4905,4] $Ans(CUT_rewritten).

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


given clause #455: (wt=5) 4646 [back_demod,4512,demod,4610,4503,flip.1] x v x=x.

given clause #456: (wt=5) 4930 [back_demod,32,demod,4647] c(c(x))=x.

given clause #457: (wt=17) 1178 [para_into,1050,927] c(x v (y v (z v u)))=c(z v (x v (y v u))).

given clause #458: (wt=9) 4555 [back_demod,4191,demod,4501] c(x) v x=x v c(x).

given clause #459: (wt=9) 4678 [back_demod,4311,demod,4644,4554,4644,flip.1] x v c(x v c(x))=x.

given clause #460: (wt=9) 4844 [back_demod,2936,demod,4833,4833,4647,466,33,4647,18,4647,4647,flip.1] f(x,y)=c(x) v c(y).

given clause #461: (wt=17) 1181 [copy,1178,flip.1] c(x v (y v (z v u)))=c(y v (z v (x v u))).

given clause #462: (wt=9) 4891 [back_demod,2105,demod,4647,4556,4845,33,4647] c(x v c(x)) v x=x.

given clause #463: (wt=9) 4922 [back_demod,640,demod,4845,33,4647,4845,33,4647,4647,4845,4833,33,4647,33,4647,4845,4919,33,4647] c(c(x) v y) v x=x.

given clause #464: (wt=9) 5074 [para_from,4646,927,flip.1] x v (y v x)=y v x.

given clause #465: (wt=17) 1189 [para_from,1050,37,demod,38] c(x v (y v (z v u)))=c(x v (z v (y v u))).

given clause #466: (wt=9) 5151 [para_from,5074,4922] c(x v c(y)) v y=y.

given clause #467: (wt=10) 4832 [back_demod,2981,demod,4647,3283,36,4647] x^y=c(c(x) v c(y)).

given clause #468: (wt=10) 5116 [para_into,4922,4930] c(x v y) v c(x)=c(x).

given clause #469: (wt=17) 1195 [para_from,1050,37,demod,38] c((x v (y v z)) v u)=c((y v (x v z)) v u).

given clause #470: (wt=9) 5181 [para_into,5116,5116,demod,4931,4931,4931] x v (x v y)=x v y.

given clause #471: (wt=10) 5156 [para_into,5151,4930] c(x v y) v c(y)=c(y).

given clause #472: (wt=11) 4271 [back_demod,3324,demod,4192,4214,3475] c(x) v c(x v c(x))=c(x).

given clause #473: (wt=19) 2722 [para_into,956,927] x v (y v (z v (u v v)))=u v (x v (y v (z v v))).

given clause #474: (wt=11) 5059 [para_into,4646,927] x v ((x v y) v y)=x v y.

given clause #475: (wt=11) 5122 [para_into,4922,927] c(x v (c(y) v z)) v y=y.

given clause #476: (wt=11) 5160 [back_demod,5019,demod,5157] c(x v c(y)) v x=x v y.

given clause #477: (wt=19) 2723 [para_into,956,956] x v (y v (z v (u v v)))=u v (x v (z v (y v v))).

given clause #478: (wt=11) 5237 [para_into,5122,5074] c(x v (y v c(z))) v z=z.

given clause #479: (wt=11) 5256 [para_into,5160,4930] c(x v y) v x=x v c(y).

given clause #480: (wt=9) 5301 [para_into,5256,5237,flip.1] x v c(y v c(x))=x.

given clause #481: (wt=19) 2724 [copy,2722,flip.1] x v (y v (z v (u v v)))=y v (z v (u v (x v v))).

given clause #482: (wt=9) 5303 [para_into,5256,5122,flip.1] x v c(c(x) v y)=x.

given clause #483: (wt=9) 5366 [para_into,5303,5156,demod,4931] (x v y) v y=x v y.

given clause #484: (wt=9) 5370 [para_into,5303,5116,demod,4931] (x v y) v x=x v y.

given clause #485: (wt=19) 2725 [copy,2723,flip.1] x v (y v (z v (u v v)))=y v (u v (z v (x v v))).

given clause #486: (wt=10) 5329 [para_into,5301,4930] c(x) v c(y v x)=c(x).

given clause #487: (wt=10) 5360 [para_into,5303,4930] c(x) v c(x v y)=c(x).

given clause #488: (wt=11) 5263 [para_into,5160,5116,demod,4931,5257] x v c(x v y)=x v c(y).

given clause #489: (wt=17) 2726 [para_from,956,1050] c(x v (y v (z v u)))=c(z v (y v (x v u))).

given clause #490: (wt=9) 5556 [back_demod,5431,demod,5549,5553] c(x v c(x)) v y=y.

given clause #491: (wt=9) 5572 [para_from,5556,5370,demod,5557] x v c(y v c(y))=x.

----> UNIT CONFLICT at   3.65 sec ----> 5596 [binary,5595,3] $Ans(ONE).

Length of proof is 202.  Level of proof is 37.

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

3 [] A v c(A)!=B v c(B)|$Ans(ONE).
7 [] f(x,f(f(y,z),f(y,z)))=f(y,f(f(x,z),f(x,z))).
8 [] f(f(x,f(y,y)),f(x,y))=x.
10 [] x v y=f(f(x,x),f(y,y)).
11 [copy,10,flip.1] f(f(x,x),f(y,y))=x v y.
13 [] x^y=f(f(x,y),f(x,y)).
14 [copy,13,flip.1] f(f(x,y),f(x,y))=x^y.
16 [] c(x)=f(x,x).
18,17 [copy,16,flip.1] f(x,x)=c(x).
19 [copy,7,flip.1,demod,18,18] f(x,c(f(y,z)))=f(y,c(f(x,z))).
21,20 [back_demod,14,demod,18] c(f(x,y))=x^y.
23,22 [back_demod,11,demod,18,18] f(c(x),c(y))=x v y.
24 [back_demod,8,demod,18] f(f(x,c(y)),f(x,y))=x.
26 [copy,19,flip.1,demod,21,21] f(x,y^z)=f(y,x^z).
27 [para_into,20,17,flip.1] x^x=c(c(x)).
30,29 [para_into,22,20] f(x^y,c(z))=f(x,y) v z.
31 [para_into,22,20] f(c(x),y^z)=x v f(y,z).
33,32 [para_into,22,17] c(c(x))=x v x.
36,35 [back_demod,27,demod,33] x^x=x v x.
38,37 [para_from,22,20,flip.1] c(x)^c(y)=c(x v y).
39 [para_into,24,20] f(f(x,y^z),f(x,f(y,z)))=x.
41 [para_into,24,22] f(x v y,f(c(x),y))=c(x).
43 [para_into,24,24,demod,21] f(f(f(x,c(y)),x^y),x)=f(x,c(y)).
45 [para_into,24,22,demod,33] f(f(c(x),y v y),x v y)=c(x).
47 [para_into,24,17] f(f(x,c(x)),c(x))=x.
49 [para_from,24,20,flip.1] f(x,c(y))^f(x,y)=c(x).
52,51 [para_into,32,32] c(x v x)=c(x) v c(x).
54,53 [para_into,32,20,flip.1] f(x,y) v f(x,y)=c(x^y).
55 [para_from,32,24] f(f(x,y v y),f(x,c(y)))=x.
58,57 [para_from,32,22] f(c(x),y v y)=x v c(y).
60,59 [para_from,32,22] f(x v x,c(y))=c(x) v y.
62,61 [back_demod,45,demod,58] f(x v c(y),x v y)=c(x).
63 [para_into,47,20,demod,21] f(f(f(x,y),x^y),x^y)=f(x,y).
69 [para_from,47,20,flip.1] f(x,c(x))^c(x)=c(x).
71 [para_into,26,35] f(x,y v y)=f(y,x^y).
72 [para_into,26,17,flip.1] f(x,(x^y)^y)=c(x^y).
74 [copy,71,flip.1] f(x,y^x)=f(y,x v x).
75 [para_from,26,24] f(f(x,c(y^z)),f(y,x^z))=x.
77 [para_from,26,20,demod,21] x^ (y^z)=y^ (x^z).
79,78 [para_into,37,32] (x v x)^c(y)=c(c(x) v y).
82,81 [para_into,37,32] c(x)^ (y v y)=c(x v c(y)).
94 [para_into,69,20,demod,21,21] f(f(x,y),x^y)^ (x^y)=x^y.
96 [para_from,69,26] f(x,c(y))=f(f(y,c(y)),x^c(y)).
102 [para_into,29,20] f(x^y,z^u)=f(x,y) v f(z,u).
118 [para_from,41,20,demod,33,flip.1] (x v y)^f(c(x),y)=x v x.
122 [para_into,49,32] f(x,y v y)^f(x,c(y))=c(x).
132 [para_into,49,41,demod,21] f(x v y,c(x)^y)^c(x)=c(x v y).
141,140 [para_into,49,22,demod,33,58,33] (x v c(y))^ (x v y)=x v x.
147,146 [para_into,57,32] f(x v x,y v y)=c(x) v c(y).
155 [para_into,31,32] f(x v x,y^z)=c(x) v f(y,z).
157,156 [para_into,31,26] f(x,c(y)^z)=y v f(x,z).
161,160 [back_demod,132,demod,157] (x v f(x v y,y))^c(x)=c(x v y).
176 [para_into,71,61,flip.1] f(x,(x v c(x))^x)=c(x).
184 [para_from,71,20,demod,21] x^ (y^x)=y^ (x v x).
185 [copy,184,flip.1] x^ (y v y)=y^ (x^y).
200 [para_into,74,37,demod,23,58,33] x v (y v x)=y v (x v x).
203 [copy,200,flip.1] x v (y v y)=y v (x v y).
214 [para_from,74,24] f(f(x,c(y^x)),f(y,x v x))=x.
218 [para_into,77,77] x^ (y^ (z^u))=z^ (x^ (y^u)).
223 [para_into,77,37] x^c(y v z)=c(y)^ (x^c(z)).
226 [copy,218,flip.1] x^ (y^ (z^u))=y^ (z^ (x^u)).
246,245 [para_from,176,20,demod,33,flip.1] x^ ((x v c(x))^x)=x v x.
250,249 [para_into,39,176] f(c(x),f(x,f(x v c(x),x)))=x.
251 [para_into,39,74] f(f(x,y v y),f(y,f(x,y)))=y.
253 [para_into,39,26] f(f(x,y^z),f(y,f(x,z)))=y.
279 [para_from,184,74] f(x^y,x^ (y v y))=f(y,(x^y) v (x^y)).
331,330 [para_from,203,41,demod,58] f(x v (y v x),y v c(x))=c(y).
338,337 [para_into,53,71] f(x,y^x) v f(y,x v x)=c(y^ (x v x)).
342 [para_into,53,74,demod,338] c(x^ (y v y))=c(y^ (x^y)).
348 [para_into,55,71] f(f(x,y^x),f(y,c(x)))=y.
357,356 [para_into,63,26] f(f(x,f(x,y)^y),x^y)=f(x,y).
367,366 [para_into,72,37,demod,38,23,38,33,flip.1] (x v y) v (x v y)=x v ((x v y) v y).
373,372 [para_into,72,31] x v f(c(x)^y,y)=c(c(x)^y).
391,390 [para_from,72,49] f(x,c((x^y)^y))^c(x^y)=c(x).
392 [para_from,72,24] f(f(x,c((x^y)^y)),c(x^y))=x.
400 [para_into,78,20] (x v x)^ (y^z)=c(c(x) v f(y,z)).
401 [copy,400,flip.1] c(c(x) v f(y,z))= (x v x)^ (y^z).
409 [para_into,81,185] x^ (c(y)^x)=c(y v c(x)).
434 [para_from,118,74,demod,54] f(f(c(x),y),x v x)=f(x v y,c(c(x)^y)).
466,465 [para_into,156,37] f(x,c(y v z))=y v f(x,c(z)).
468,467 [para_into,156,63,demod,157,flip.1] x v f(x v f(f(c(x),y),y),y)=f(c(x),y).
469 [para_into,156,31] x v f(c(y),z)=y v f(c(x),z).
479 [para_from,156,39] f(x v f(y,z),f(y,f(c(x),z)))=y.
486 [para_from,156,20] c(x v f(y,z))=y^ (c(x)^z).
488 [copy,486,flip.1] x^ (c(y)^z)=c(y v f(x,z)).
515 [para_from,348,20,flip.1] f(x,y^x)^f(y,c(x))=c(y).
548 [para_into,75,69,demod,33] f(f(x,y v y),f(f(y,c(y)),x^c(y)))=x.
641,640 [para_from,122,74,demod,54] f(f(x,c(y)),c(x))=f(f(x,y v y),c(x^c(y))).
648,647 [back_demod,47,demod,641] f(f(x,x v x),c(x^c(x)))=x.
662 [para_into,94,26] f(x,f(x,y)^y)^ (x^y)=x^y.
684 [para_from,249,20,flip.1] c(x)^f(x,f(x v c(x),x))=c(x).
688 [para_into,251,57] f(x v c(y),f(y,f(c(x),y)))=y.
700 [para_from,251,20,flip.1] f(x,y v y)^f(y,f(x,y))=c(y).
704 [para_into,96,43,demod,23,23,157,161,466,flip.1] x v f(f(x,c(x)),c(y))=x v y.
790 [para_into,253,41] f(f(c(x),(x v y)^y),c(x))=x v y.
803,802 [para_from,253,20,flip.1] f(x,y^z)^f(y,f(x,z))=c(y).
845 [para_into,330,32] f(c(x) v (y v c(x)),y v (x v x))=c(y).
868 [para_from,342,22,demod,23] (x^ (y^x)) v z= (y^ (x v x)) v z.
927 [para_into,465,22,demod,23] x v (y v z)=y v (x v z).
1154 [para_into,704,32] x v f(f(x,c(x)),y v y)=x v c(y).
1156 [para_into,704,20] x v f(f(x,c(x)),y^z)=x v f(y,z).
1163 [copy,1156,flip.1] x v f(y,z)=x v f(f(x,c(x)),y^z).
1166 [para_from,704,486,demod,38,flip.1] f(x,c(x))^c(x v y)=c(x v y).
1241,1240 [para_into,155,74,demod,367] f(x,y v ((y v y) v y))=c(y) v f(x,y v y).
1291 [para_into,214,57] f(f(x,c(c(y)^x)),y v c(x))=x.
1456,1455 [para_from,684,77,flip.1] c(x)^ (y^f(x,f(x v c(x),x)))=y^c(x).
1477 [para_into,700,146] (c(x) v c(y))^f(y,f(x v x,y))=c(y).
2081 [para_into,392,96,demod,30,391] f(f(x,y) v (x^y),c(x))=x.
2100 [para_into,2081,253,demod,803,21] f(x v c(x),y^ (x^z))=f(y,x^z).
2105 [para_into,2081,176,demod,246] f(c(x) v (x v x),c(x))=x.
2119 [para_into,2081,74] f(f(x,y v y) v (y^ (x^y)),c(y))=y.
2137 [para_into,2081,26] f(f(x,y^z) v (y^ (x^z)),c(y))=y.
2198,2197 [para_into,2105,469,demod,21,21,373,21,157] x v f((c(x)^y) v c(c(x)^y),y)=f(c(x),y).
2648 [para_into,868,37,demod,38,82,33] c(x v (y v x)) v z=c(y v (x v x)) v z.
2652 [copy,2648,flip.1] c(x v (y v y)) v z=c(y v (x v y)) v z.
2817 [para_into,1154,71] x v f(y,f(x,c(x))^y)=x v c(y).
2935 [para_into,279,102] f(x,y) v f(x,y v y)=f(y,(x^y) v (x^y)).
2936 [copy,2935,flip.1] f(x,(y^x) v (y^x))=f(y,x) v f(y,x v x).
2981 [para_from,2817,401,demod,33,58,flip.1] (x v x)^ (y^ ((x v c(x))^y))=c(c(x) v c(y)).
3112,3111 [para_into,1163,469,demod,157,flip.1] x v (y v f(f(x,c(x)),z))=y v f(c(x),z).
3169,3168 [para_into,2100,662,demod,357] f(x v c(x),x^y)=f(x,y).
3201,3200 [para_into,3168,26] f(x,(x v c(x))^y)=f(x,y).
3212 [para_from,3168,802] f(x,y)^f(x,f(x v c(x),y))=c(x).
3217,3216 [para_from,3168,253] f(f(x,y),f(x,f(x v c(x),y)))=x.
3228 [para_from,3168,20,demod,21,flip.1] (x v c(x))^ (x^y)=x^y.
3264 [para_from,3200,20,demod,21,flip.1] x^ ((x v c(x))^y)=x^y.
3283,3282 [para_into,3228,226] x^ (y^ ((x v c(x))^z))=x^ (y^z).
3290 [para_from,3228,3168,demod,3169] f((x v c(x)) v c(x v c(x)),x^y)=f(x,y).
3298 [para_from,467,1166,demod,21,468,21] f(x,c(x))^ (c(x)^y)=c(x)^y.
3306 [para_into,3264,1477,demod,33,82,60,flip.1] c(x)^f(c(x),c(x) v x)=c(x v c(x)).
3312 [para_from,3264,3200,demod,3201,flip.1] f(x,((x v c(x)) v c(x v c(x)))^y)=f(x,y).
3390,3389 [para_into,3298,488] c(x v f(f(x,c(x)),y))=c(x)^y.
3406,3405 [para_from,3298,29,demod,30,157,flip.1] (x v f(f(x,c(x)),y)) v z=f(c(x),y) v z.
3430 [para_from,3389,2105,demod,3390,367,3406,3112,54,157,2198,flip.1] x v f(f(x,c(x)),y)=f(c(x),y).
3432 [para_into,3430,32,demod,58,33] c(x) v f(x v c(x),y)=f(x v x,y).
3538 [para_into,3432,688,flip.1] f(x v x,f(x,f(c(x),x)))=c(x) v x.
3580 [para_from,3538,479,demod,33,60,62,33,33] f(x v (x v x),(x v x) v c(x))=c(x) v c(x).
3593,3592 [para_into,2137,684,demod,1456,33] f(f(x,c(y)) v (x^c(y)),y v y)=c(y).
3650 [para_into,548,3200,demod,21,3593,641,648,21] f(c(x),x)=f(x,c(x)) v (x^c(x)).
3663,3662 [para_into,3650,32,demod,60,33,58,33,82,flip.1] (x v c(x)) v c(x v c(x))=c(x) v x.
3664 [back_demod,3312,demod,3663] f(x,(c(x) v x)^y)=f(x,y).
3668 [back_demod,3290,demod,3663] f(c(x) v x,x^y)=f(x,y).
3683 [para_from,3650,434,demod,3593,60,flip.1] c(x) v (c(x)^x)=c(x).
3692 [para_into,3683,32,demod,33,79,33] (x v x) v c(c(x) v x)=x v x.
3748,3747 [para_into,3664,32] f(c(x),((x v x) v c(x))^y)=f(c(x),y).
3788,3787 [para_into,3664,74,demod,18] f(c(x) v x,x v x)=c(x).
3809 [para_from,3664,515,demod,18] c(x)^f(c(x) v x,c(x))=c(c(x) v x).
3871 [para_from,3787,251] f(c(x),f(x,f(c(x) v x,x)))=x.
3955 [para_into,3668,3212,demod,21,3217] f((x^y) v f(x,y),c(x))=x.
3976,3975 [para_into,3668,684,demod,33,250] f((x v x) v c(x),c(x))=x.
4022 [para_from,3975,55] f(f((x v x) v c(x),x v x),x)= (x v x) v c(x).
4029,4028 [para_from,3975,24] f(x,f((x v x) v c(x),x))= (x v x) v c(x).
4115 [para_into,3955,223,demod,466] f((c(x)^ (y^c(z))) v (x v f(y,c(z))),c(y))=y.
4192,4191 [para_from,3692,1291,demod,52,141,52,33,33,367,1241,3788,147,33,flip.1] c(x) v x= (x v x) v c(x).
4196,4195 [back_demod,3809,demod,4192,3976,4192] c(x)^x=c((x v x) v c(x)).
4214,4213 [back_demod,3871,demod,4192,4029] f(c(x),(x v x) v c(x))=x.
4236,4235 [back_demod,3787,demod,4192] f((x v x) v c(x),x v x)=c(x).
4252,4251 [back_demod,3662,demod,4192] (x v c(x)) v c(x v c(x))= (x v x) v c(x).
4274,4273 [back_demod,3306,demod,4192,4214,4196] c((x v x) v c(x))=c(x v c(x)).
4300,4299 [back_demod,4022,demod,4236] f(c(x),x)= (x v x) v c(x).
4401 [back_demod,4195,demod,4274] c(x)^x=c(x v c(x)).
4446,4445 [para_from,4401,409] x^c(x v c(x))=c(x v c(x)).
4501,4500 [para_from,4401,356,demod,4300,3748,4300,466,33,4236,4300,flip.1] (x v x) v c(x)=x v c(x).
4503,4502 [para_from,4401,2119,demod,58,4446,4252,4501] f(x v c(x),c(x))=x.
4512 [para_from,4401,43,demod,18,33,466,33,18,52,18,33] f(x v (c(x) v c(x)),c(x))=x v x.
4556,4555 [back_demod,4191,demod,4501] c(x) v x=x v c(x).
4610,4609 [back_demod,3580,demod,4501,331,flip.1] c(x) v c(x)=c(x).
4647,4646 [back_demod,4512,demod,4610,4503,flip.1] x v x=x.
4833,4832 [back_demod,2981,demod,4647,3283,36,4647] x^y=c(c(x) v c(y)).
4845,4844 [back_demod,2936,demod,4833,4833,4647,466,33,4647,18,4647,4647,flip.1] f(x,y)=c(x) v c(y).
4850,4849 [back_demod,2652,demod,4647,flip.1] c(x v (y v x)) v z=c(y v x) v z.
4919,4918 [back_demod,845,demod,4647,4845,4850] c(x v c(y)) v c(x v y)=c(x).
4922 [back_demod,640,demod,4845,33,4647,4845,33,4647,4647,4845,4833,33,4647,33,4647,4845,4919,33,4647] c(c(x) v y) v x=x.
4931,4930 [back_demod,32,demod,4647] c(c(x))=x.
4981 [back_demod,4115,demod,4833,4931,4833,4931,4931,4845,4931,4556,4845,4931] c((x v (c(y) v z)) v c(x v (c(y) v z))) v y=y.
5019 [back_demod,790,demod,4833,4845,4931,4931,4845,4931] c(x v (c(x v y) v c(y))) v x=x v y.
5074 [para_from,4646,927,flip.1] x v (y v x)=y v x.
5078 [para_into,4555,927] x v (c(x v y) v y)= (x v y) v c(x v y).
5088 [para_from,4555,927] x v (y v c(y))=c(y) v (x v y).
5095 [copy,5088,flip.1] c(x) v (y v x)=y v (x v c(x)).
5116 [para_into,4922,4930] c(x v y) v c(x)=c(x).
5122 [para_into,4922,927] c(x v (c(y) v z)) v y=y.
5151 [para_from,5074,4922] c(x v c(y)) v y=y.
5157,5156 [para_into,5151,4930] c(x v y) v c(y)=c(y).
5160 [back_demod,5019,demod,5157] c(x v c(y)) v x=x v y.
5237 [para_into,5122,5074] c(x v (y v c(z))) v z=z.
5257,5256 [para_into,5160,4930] c(x v y) v x=x v c(y).
5260,5259 [para_into,5160,5156,demod,4931,flip.1] c(x v y) v y=y v c(x v y).
5263 [para_into,5160,5116,demod,4931,5257] x v c(x v y)=x v c(y).
5268,5267 [back_demod,5078,demod,5260,flip.1] (x v y) v c(x v y)=x v (y v c(x v y)).
5271 [back_demod,4981,demod,5268] c(x v ((c(y) v z) v c(x v (c(y) v z)))) v y=y.
5301 [para_into,5256,5237,flip.1] x v c(y v c(x))=x.
5303 [para_into,5256,5122,flip.1] x v c(c(x) v y)=x.
5329 [para_into,5301,4930] c(x) v c(y v x)=c(x).
5349,5348 [para_from,5301,5256,demod,4556,4931,flip.1] x v (y v c(x))=x v c(x).
5366 [para_into,5303,5156,demod,4931] (x v y) v y=x v y.
5370 [para_into,5303,5116,demod,4931] (x v y) v x=x v y.
5417,5416 [para_from,5366,5256,demod,4556,5268] x v (y v c(x v y))= (x v y) v c(y).
5431 [back_demod,5271,demod,5417] c((x v (c(y) v z)) v c(c(y) v z)) v y=y.
5435 [back_demod,5267,demod,5417] (x v y) v c(x v y)= (x v y) v c(y).
5499,5498 [para_from,5329,5256,demod,4931,4931,flip.1] c(x) v (y v x)=x v c(x).
5506,5505 [back_demod,5095,demod,5499,flip.1] x v (y v c(y))=y v c(y).
5547,5546 [para_from,5263,927,flip.1] x v (y v c(x v z))=y v (x v c(z)).
5549,5548 [back_demod,5416,demod,5547,5349,flip.1] (x v y) v c(y)=y v c(y).
5553,5552 [back_demod,5435,demod,5549] (x v y) v c(x v y)=y v c(y).
5557,5556 [back_demod,5431,demod,5549,5553] c(x v c(x)) v y=y.
5572 [para_from,5556,5370,demod,5557] x v c(y v c(y))=x.
5595 [para_from,5572,5263,demod,4931,5506] x v c(x)=y v c(y).
5596 [binary,5595,3] $Ans(ONE).

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


Search stopped by max_proofs option.

============ end of search ============

-------------- statistics -------------
clauses given                491
clauses generated          98092
clauses kept                3492
clauses forward subsumed   33972
clauses back subsumed        116
Kbytes malloced             3608

----------- times (seconds) -----------
user CPU time          3.65          (0 hr, 0 min, 3 sec)
system CPU time        0.97          (0 hr, 0 min, 0 sec)
wall-clock time        5             (0 hr, 0 min, 5 sec)
para_into time         0.29
para_from time         0.27
for_sub time           0.16
back_sub time          0.02
conflict time          0.01
demod time             1.29

That finishes the proof of the theorem.

Process 26031 finished Fri Sep 12 16:35:17 2003