%------------------------------------------------------------------------------ % File : CARINE---0.734 % Problem : LCL416-1 : TPTP v5.0.0. Released v2.5.0. % Transfm : add_equality % Format : carine % Command : carine %s t=%d xo=off uct=32000 % Computer : art03.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 2018MB % OS : Linux 2.6.26.8-57.fc8 % CPULimit : 300s % DateTime : Sun Nov 28 01:23:46 EST 2010 % Result : Unsatisfiable 4.15s % Output : Refutation 4.15s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % Command entered: % /home/graph/tptp/Systems/CARINE---0.734/carine /tmp/SystemOnTPTP2466/LCL/LCL416-1+noeq.car t=300 xo=off uct=32000 % CARINE version 0.734 (Dec 2003) % Initializing tables ... done. % Parsing ... done. % Calculating time slices ... done. % Building Lookup Tables ... done. % Looking for a proof at depth = 1 ... % t = 0 secs [nr = 3] [nf = 0] [nu = 0] [ut = 2] % Looking for a proof at depth = 2 ... % t = 0 secs [nr = 56] [nf = 0] [nu = 24] [ut = 16] % Looking for a proof at depth = 3 ... % t = 0 secs [nr = 135] [nf = 4] [nu = 66] [ut = 16] % Looking for a proof at depth = 4 ... % +================================================+ % | | % | Congratulations!!! ........ A proof was found. | % | | % +================================================+ % Base Clauses and Unit Clauses used in proof: % ============================================ % Base Clauses: % ------------- % B0: ~is_a_theorem_1(equivalent_2(a_0(),a_0())) % B1: is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) % B2: ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) % Unit Clauses: % -------------- % U1: < d0 v6 dv3 f5 c0 t11 td5 b > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) % U3: < d2 v10 dv5 f9 c0 t19 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) % U4: < d2 v10 dv5 f9 c0 t19 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4))) % U5: < d2 v12 dv6 f11 c0 t23 td10 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0),x4),equivalent_2(x5,x4)),x5))) % U6: < d2 v16 dv8 f15 c0 t31 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),equivalent_2(x7,x6)),x7)) % U7: < d2 v16 dv8 f15 c0 t31 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),x7),equivalent_2(x6,x7))) % U14: < d2 v14 dv7 f13 c0 t27 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(x6,x5)),x6)) % U15: < d2 v14 dv7 f13 c0 t27 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),equivalent_2(x6,x5)),x6)) % U34: < d4 v16 dv8 f17 c2 t35 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),equivalent_2(equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7)),a_0()),a_0()))) % U187: < d4 v12 dv6 f11 c0 t23 td10 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x4),equivalent_2(x5,x4)),x5)),x0)) % U188: < d4 v8 dv4 f7 c0 t15 td7 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3))),x0)) % U253: < d4 v8 dv4 f7 c0 t15 td7 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0))) % U255: < d4 v12 dv6 f11 c0 t23 td7 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))) % U391: < d4 v22 dv11 f21 c0 t43 td10 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5)),equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,x7)),x8))),x9),x10),equivalent_2(x9,x10)))) % U416: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7))) % U418: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7))) % U420: < d4 v14 dv7 f13 c0 t27 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),x6),equivalent_2(x5,x6))) % U424: < d4 v12 dv6 f11 c0 t23 td6 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5)))) % U740: < d4 v18 dv9 f17 c0 t35 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,x7)),x8)),x5))) % U782: < d4 v12 dv6 f11 c0 t23 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),equivalent_2(x5,x4)),x5)) % U786: < d4 v14 dv7 f13 c0 t27 td8 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),x3))) % U831: < d4 v12 dv6 f11 c0 t23 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),x5),equivalent_2(x4,x5))) % U1071: < d4 v14 dv7 f13 c0 t27 td8 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6)),x3)))) % U1161: < d4 v18 dv9 f17 c0 t35 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6)),x3)),x7),equivalent_2(x8,x7)),x8)) % U1506: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7)),x4)),x0)))) % U1751: < d4 v10 dv5 f9 c0 t19 td9 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,x3)),x4)),x1)),x0))) % U2491: < d4 v18 dv9 f17 c0 t35 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),x7),equivalent_2(x8,x7)),x8)) % U2984: < d4 v30 dv15 f31 c2 t63 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,x8)),x9)),x10),equivalent_2(x11,x10)),x11),equivalent_2(equivalent_2(equivalent_2(x12,equivalent_2(equivalent_2(equivalent_2(x12,x13),equivalent_2(x14,x13)),x14)),a_0()),a_0())))) % --------------- Start of Proof --------------- % Derivation of unit clause U1: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... U1 % Derivation of unit clause U3: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4)) ....... R2 [R1:L0, U1:L0] % Derivation of unit clause U4: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4))) ....... R2 [R1:L0, U3:L0] % Derivation of unit clause U5: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4))) ....... U4 % is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0), x4), equivalent_2(x5, x4)), x5))) ....... R2 [R1:L0, U4:L0] % Derivation of unit clause U6: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0),x4),equivalent_2(x5,x4)),x5))) ....... U5 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))), x6), equivalent_2(x7, x6)), x7)) ....... R2 [R1:L0, U5:L0] % Derivation of unit clause U7: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),equivalent_2(x7,x6)),x7)) ....... U6 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))), x6), x7), equivalent_2(x6, x7))) ....... R2 [R1:L0, U6:L0] % Derivation of unit clause U14: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)) ....... R1 [B1:L0, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5), equivalent_2(x6, x5)), x6)) ....... R2 [R1:L0, U3:L0] % Derivation of unit clause U15: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)) ....... R1 [B1:L0, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4))) ....... U4 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5), equivalent_2(x6, x5)), x6)) ....... R2 [R1:L0, U4:L0] % Derivation of unit clause U34: % ~is_a_theorem_1(equivalent_2(a_0(),a_0())) ....... B0 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0, equivalent_2(a_0(), a_0()))) ....... R1 [B0:L0, B2:L2] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(x0, equivalent_2(a_0(), a_0()))) | ~is_a_theorem_1(x1) | ~is_a_theorem_1(equivalent_2(x1, x0)) ....... R2 [R1:L0, B2:L2] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4))) ....... U4 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), a_0()), a_0()))) ....... R3 [R2:L0, U4:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), equivalent_2(equivalent_2(equivalent_2(x5, equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, x6)), x7)), a_0()), a_0()))) ....... R4 [R3:L0, U3:L0] % Derivation of unit clause U187: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... U1 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5)) | is_a_theorem_1(x5) ....... R3 [R2:L0, U1:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4))) ....... U4 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x4), equivalent_2(x5, x4)), x5)), x0)) ....... R4 [R3:L0, U4:L0] % Derivation of unit clause U188: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... U1 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5)) | is_a_theorem_1(x5) ....... R3 [R2:L0, U1:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),x7),equivalent_2(x6,x7))) ....... U7 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3))), x0)) ....... R4 [R3:L0, U7:L0] % Derivation of unit clause U253: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5)) | is_a_theorem_1(x5) ....... R3 [R2:L0, U3:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),x7),equivalent_2(x6,x7))) ....... U7 % is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0))) ....... R4 [R3:L0, U7:L0] % Derivation of unit clause U255: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4)) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5)) | is_a_theorem_1(x5) ....... R3 [R2:L0, U3:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3))),x0)) ....... U188 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))) ....... R4 [R3:L0, U188:L0] % Derivation of unit clause U391: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))),x6),equivalent_2(x7,x6)),x7)) ....... U6 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))), x6), x7), equivalent_2(x6, x7)), x8)) | is_a_theorem_1(x8) ....... R3 [R2:L0, U6:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0))) ....... U253 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5)), equivalent_2(x6, equivalent_2(equivalent_2(equivalent_2(x6, x7), equivalent_2(x8, x7)), x8))), x9), x10), equivalent_2(x9, x10)))) ....... R4 [R3:L0, U253:L0] % Derivation of unit clause U416: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(x6,x5)),x6)) ....... U14 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5), x6), equivalent_2(x5, x6)), x7)) | is_a_theorem_1(x7) ....... R3 [R2:L0, U14:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3))),x0)) ....... U188 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, x6)), x7))) ....... R4 [R3:L0, U188:L0] % Derivation of unit clause U418: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),equivalent_2(x6,x5)),x6)) ....... U15 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5), x6), equivalent_2(x5, x6)), x7)) | is_a_theorem_1(x7) ....... R3 [R2:L0, U15:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3))),x0)) ....... U188 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, x6)), x7))) ....... R4 [R3:L0, U188:L0] % Derivation of unit clause U420: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x4),equivalent_2(x5,x4)),x5)),x0)) ....... U187 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U187:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),equivalent_2(x6,x5)),x6)) ....... U15 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), x4), equivalent_2(x3, x4)), x5), x6), equivalent_2(x5, x6))) ....... R4 [R3:L0, U15:L0] % Derivation of unit clause U424: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x4),equivalent_2(x5,x4)),x5)),x0)) ....... U187 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U187:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0))) ....... U253 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5)))) ....... R4 [R3:L0, U253:L0] % Derivation of unit clause U740: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))) ....... U255 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5), equivalent_2(x6, x5)), x6), x7)) | is_a_theorem_1(x7) ....... R3 [R2:L0, U255:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3))),x0)) ....... U188 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(x4, x3)), x4), x5), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(equivalent_2(x6, x7), equivalent_2(x8, x7)), x8)), x5))) ....... R4 [R3:L0, U188:L0] % Derivation of unit clause U782: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5)),equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,x7)),x8))),x9),x10),equivalent_2(x9,x10)))) ....... U391 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))), x6), x7), equivalent_2(x6, x7)), x8)) | is_a_theorem_1(x8) ....... R3 [R2:L0, U391:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7))) ....... U418 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), x4), equivalent_2(x5, x4)), x5)) ....... R4 [R3:L0, U418:L0] % Derivation of unit clause U786: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5)),equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,x7)),x8))),x9),x10),equivalent_2(x9,x10)))) ....... U391 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, x4)), x5))), x6), x7), equivalent_2(x6, x7)), x8)) | is_a_theorem_1(x8) ....... R3 [R2:L0, U391:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,x7)),x8)),x5))) ....... U740 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6))), x3))) ....... R4 [R3:L0, U740:L0] % Derivation of unit clause U831: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5)))) ....... U424 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U424:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),equivalent_2(x5,x4)),x5)) ....... U782 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), x4), x5), equivalent_2(x4, x5))) ....... R4 [R3:L0, U782:L0] % Derivation of unit clause U1071: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),equivalent_2(x5,x4)),x5)) ....... U782 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), x4), x5), equivalent_2(x4, x5)), x6)) | is_a_theorem_1(x6) ....... R3 [R2:L0, U782:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),equivalent_2(x5,x4)),x5)) ....... U782 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6)), x3)))) ....... R4 [R3:L0, U782:L0] % Derivation of unit clause U1161: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),x3))) ....... U786 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3))), x0), x4)) | is_a_theorem_1(x4) ....... R3 [R2:L0, U786:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),x5),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7))) ....... U416 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6)), x3)), x7), equivalent_2(x8, x7)), x8)) ....... R4 [R3:L0, U416:L0] % Derivation of unit clause U1506: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),equivalent_2(x3,equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6)),x3)))) ....... U1071 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), x4)) | is_a_theorem_1(x4) ....... R3 [R2:L0, U1071:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),x4),x5),equivalent_2(x4,x5))) ....... U831 % is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x5, equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, x6)), x7)), x4)), x0)))) ....... R4 [R3:L0, U831:L0] % Derivation of unit clause U1751: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6)),x3)),x7),equivalent_2(x8,x7)),x8)) ....... U1161 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3), equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6)), x3)), x7), x8), equivalent_2(x7, x8)), x9)) | is_a_theorem_1(x9) ....... R3 [R2:L0, U1161:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),x4),equivalent_2(x3,x4)),x5),x6),equivalent_2(x5,x6))) ....... U420 % is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(equivalent_2(x2, x3), equivalent_2(x4, x3)), x4)), x1)), x0))) ....... R4 [R3:L0, U420:L0] % Derivation of unit clause U2491: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7)),x4)),x0)))) ....... U1506 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6)), x3)), equivalent_2(x7, equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, x8)), x9)))), x10)) | is_a_theorem_1(x10) ....... R3 [R2:L0, U1506:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,x4)),x5))) ....... U255 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6))), x7), equivalent_2(x8, x7)), x8)) ....... R4 [R3:L0, U255:L0] % Derivation of unit clause U2984: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2))) ....... B1 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0,x1)) | is_a_theorem_1(x1) ....... B2 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, x1)), x2)), x3)) | ~is_a_theorem_1(equivalent_2(x3, x4)) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,x3)),x4)),x1)),x0))) ....... U1751 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6))), x7)) | is_a_theorem_1(x7) ....... R3 [R2:L0, U1751:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,x1)),x2)),x3),equivalent_2(x4,x3)),x4),equivalent_2(equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,x6)),x7)),a_0()),a_0()))) ....... U34 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, x2)), x3)), x0)), equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, x5)), x6))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, x8)), x9)), x10), equivalent_2(x11, x10)), x11), equivalent_2(equivalent_2(equivalent_2(x12, equivalent_2(equivalent_2(equivalent_2(x12, x13), equivalent_2(x14, x13)), x14)), a_0()), a_0())))) ....... R4 [R3:L1, U34:L0] % Derivation of the empty clause: % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,x8)),x9)),x10),equivalent_2(x11,x10)),x11),equivalent_2(equivalent_2(equivalent_2(x12,equivalent_2(equivalent_2(equivalent_2(x12,x13),equivalent_2(x14,x13)),x14)),a_0()),a_0())))) ....... U2984 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,x2)),x3)),x0)),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,x5)),x6))),x7),equivalent_2(x8,x7)),x8)) ....... U2491 % [] ....... R1 [U2984:L0, U2491:L0] % --------------- End of Proof --------------- % PROOF FOUND! % --------------------------------------------- % | Statistics | % --------------------------------------------- % Profile 3: Performance Statistics: % ================================== % Total number of generated clauses: 137980 % resolvents: 137972 factors: 8 % Number of unit clauses generated: 137733 % % unit clauses generated to total clauses generated: 99.82 % Number of unit clauses constructed and retained at depth [x]: % ============================================================= % [0] = 2 [2] = 14 [4] = 2969 % Total = 2985 % Number of generated clauses having [x] literals: % ------------------------------------------------ % [1] = 137733 [2] = 236 [3] = 11 % Average size of a generated clause: 2.0 % Number of unit clauses per predicate list: % ========================================== % [0] is_a_theorem_1 (+)583 (-)2402 % ------------------ % Total: (+)583 (-)2402 % Total number of unit clauses retained: 2985 % Number of clauses skipped because of their length: 179 % N base clauses skippped in resolve-with-all-base-clauses % because of the shortest resolvents table: 0 % Number of successful unifications: 138074 % Number of unification failures: 22849 % Number of unit to unit unification failures: 1400226 % N literal unification failure due to lookup root_id table: 26 % N base clause resolution failure due to lookup table: 0 % N UC-BCL resolution dropped due to lookup table: 0 % Max entries in substitution set: 21 % N unit clauses dropped because they exceeded max values: 134505 % N unit clauses dropped because too much nesting: 50121 % N unit clauses not constrcuted because table was full: 0 % N unit clauses dropped because UCFA table was full: 0 % Max number of terms in a unit clause: 63 % Max term depth in a unit clause: 11 % Number of states in UCFA table: 39432 % Total number of terms of all unit clauses in table: 162203 % Max allowed number of states in UCFA: 528000 % Ratio n states used/total allowed states: 0.07 % Ratio n states used/total unit clauses terms: 0.24 % Number of symbols (columns) in UCFA: 37 % Profile 2: Number of calls to: % ============================== % PTUnify() = 160923 % ConstructUnitClause() = 137488 % Profile 1: Time spent in: % ========================= % ConstructUnitClause() : 0.56 secs % -------------------------------------------------------- % | | % Inferences per sec: 34495 % | | % -------------------------------------------------------- % Elapsed time: 4 secs % CPU time: 4.14 secs % %------------------------------------------------------------------------------