%------------------------------------------------------------------------------ % File : CARINE---0.734 % Problem : LCL166-1 : TPTP v5.0.0. Released v1.0.0. % Transfm : add_equality % Format : carine % Command : carine %s t=%d xo=off uct=32000 % Computer : art01.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 00:13:39 EST 2010 % Result : Unsatisfiable 34.47s % Output : Refutation 34.47s % 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/SystemOnTPTP13277/LCL/LCL166-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 = 40] [nf = 0] [nu = 17] [ut = 12] % Looking for a proof at depth = 3 ... % t = 0 secs [nr = 94] [nf = 5] [nu = 43] [ut = 12] % 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(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))) % B1: is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) % 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(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) % U3: < d2 v10 dv5 f9 c0 t19 td8 > is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) % U4: < d2 v12 dv6 f11 c0 t23 td7 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2)) % U8: < d2 v14 dv7 f13 c0 t27 td11 > is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))),x2))),x0))) % U9: < d2 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x4)),x0))) % U16: < d4 v12 dv6 f17 c6 t35 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),x3)),x5))) % U59: < d4 v16 dv8 f15 c0 t31 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x1),x2)))),x4),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),equivalent_2(x4,x0))) % U106: < d4 v12 dv6 f17 c6 t35 td8 > ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x5,x3)))) % U159: < d4 v22 dv11 f21 c0 t43 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x1),x2)))),x4),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x7),x5)),equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9)))),x7)),equivalent_2(x4,x0))) % U160: < d4 v24 dv12 f23 c0 t47 td9 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x3),x1)),equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))),x3)),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x0),x7)),equivalent_2(x9,equivalent_2(equivalent_2(x10,x11),equivalent_2(equivalent_2(x11,x9),x10)))))) % U171: < d4 v18 dv9 f17 c0 t35 td11 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))),x3)),x5))) % U179: < d4 v12 dv6 f11 c0 t23 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),x2)) % U181: < d4 v16 dv8 f15 c0 t31 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6))))) % U225: < d4 v24 dv12 f29 c6 t59 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),x11),equivalent_2(x10,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x11,x9))))) % U342: < d4 v12 dv6 f11 c0 t23 td6 > is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))) % U361: < d4 v14 dv7 f13 c0 t27 td7 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),x3),x2),equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))))) % U376: < d4 v18 dv9 f17 c0 t35 td10 > is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),x5),x4),equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))))),x0))) % U420: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3))),x2)) % U422: < d4 v20 dv10 f19 c0 t39 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),x3),x2),equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5))))),equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8))))) % U830: < d4 v22 dv11 f21 c0 t43 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3)),equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9))))),x2)) % U841: < d4 v20 dv10 f19 c0 t39 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x5),x3)),x6),x5),equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8)))))),x2)) % U1172: < d4 v18 dv9 f17 c0 t35 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,x2)),x3))),x5)),x0)),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))) % U1179: < d4 v22 dv11 f21 c0 t43 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,x2)),x3))),x5)),x0)),equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9)))),x6)))) % U1360: < d4 v12 dv6 f17 c6 t35 td7 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),equivalent_2(equivalent_2(equivalent_2(x1,x5),x0),equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))))) % U1492: < d4 v18 dv9 f23 c6 t47 td8 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),equivalent_2(equivalent_2(equivalent_2(x1,x5),x0),equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))) % U1586: < d4 v12 dv6 f11 c0 t23 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) % U1780: < d4 v14 dv7 f19 c6 t39 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x0,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5))))),x2))),equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))) % U1909: < d4 v20 dv10 f19 c0 t39 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x5),x3)),x6),x5)),equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8)))))) % U1958: < d4 v18 dv9 f17 c0 t35 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(x3,x4)),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,equivalent_2(x8,x5)),x6))),x8)),x3))) % U1964: < d4 v22 dv11 f21 c0 t43 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,x6)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,equivalent_2(x10,x7)),x8))),x10)),x5))) % U2099: < d4 v18 dv9 f17 c0 t35 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x4,x1)),x2))),x4)),x5),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))),equivalent_2(x5,x0))) % U3282: < d4 v14 dv7 f19 c6 t39 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x2,x6))) % U6521: < d4 v28 dv14 f27 c0 t55 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,x6)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,equivalent_2(x10,x7)),x8))),x10)),x5)),equivalent_2(x11,equivalent_2(equivalent_2(x12,x13),equivalent_2(equivalent_2(x13,x11),x12))))) % U6971: < d4 v16 dv8 f21 c6 t43 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x2),x6)),equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))) % U9216: < d4 v28 dv14 f27 c0 t55 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3)),equivalent_2(x8,x9))),equivalent_2(equivalent_2(x9,equivalent_2(equivalent_2(x10,equivalent_2(equivalent_2(x11,x12),equivalent_2(equivalent_2(x12,equivalent_2(x13,x10)),x11))),x13)),x8))) % --------------- Start of Proof --------------- % Derivation of unit clause U1: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % Derivation of unit clause U3: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), x0))) ....... R2 [R1:L0, U1:L0] % Derivation of unit clause U4: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4)))), x2)) ....... R2 [R1:L0, U3:L0] % Derivation of unit clause U8: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5)))), x2))), x0))) ....... R2 [R1:L0, U3:L0] % Derivation of unit clause U9: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2)) ....... U4 % is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x4), x2)), equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6)))), x4)), x0))) ....... R2 [R1:L0, U4:L0] % Derivation of unit clause U16: % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_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(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_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(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_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,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2)) ....... U4 % ~is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0())))), x1)), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4)))))) ....... R3 [R2:L0, U4:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))), x3)), x5))) ....... R4 [R3:L1, U3:L0] % Derivation of unit clause U59: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), x0)), x5)) | is_a_theorem_1(x5) ....... R3 [R2:L0, U1:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2)))), x4), equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6)))), equivalent_2(x4, x0))) ....... R4 [R3:L0, U3:L0] % Derivation of unit clause U106: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))) ....... R3 [R2:L1, U1:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),x3)),x5))) ....... U16 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), x5), equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))), equivalent_2(x5, x3)))) ....... R4 [R3:L1, U16:L0] % Derivation of unit clause U159: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x4)),x0))) ....... U9 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | is_a_theorem_1(equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x7), x5)), equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9)))), x7)), x3)) ....... R3 [R2:L1, U9:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2)))), x4), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x7), x5)), equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9)))), x7)), equivalent_2(x4, x0))) ....... R4 [R3:L0, U1:L0] % Derivation of unit clause U160: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x4)),x0))) ....... U9 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | is_a_theorem_1(equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x7), x5)), equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9)))), x7)), x3)) ....... R3 [R2:L1, U9:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x3), x1)), equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5)))), x3)), equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x0), x7)), equivalent_2(x9, equivalent_2(equivalent_2(x10, x11), equivalent_2(equivalent_2(x11, x9), x10)))))) ....... R4 [R3:L0, U3:L0] % Derivation of unit clause U171: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x1),x2)))),x4),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),equivalent_2(x4,x0))) ....... U59 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5)))), x7), equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9)))))) | is_a_theorem_1(equivalent_2(x7, x3)) ....... R3 [R2:L1, U59:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7))))), x3)), x5))) ....... R4 [R3:L0, U3:L0] % Derivation of unit clause U179: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x1),x2)))),x4),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x7),x5)),equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9)))),x7)),equivalent_2(x4,x0))) ....... U159 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5)))), x7), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x10), x8)), equivalent_2(x11, equivalent_2(equivalent_2(x12, x13), equivalent_2(equivalent_2(x13, x11), x12)))), x10)))) | is_a_theorem_1(equivalent_2(x7, x3)) ....... R3 [R2:L1, U159:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))), x0)), x2)) ....... R4 [R3:L0, U1:L0] % Derivation of unit clause U181: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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,x2),equivalent_2(equivalent_2(x2,x3),x1)),equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))),x3)),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x0),x7)),equivalent_2(x9,equivalent_2(equivalent_2(x10,x11),equivalent_2(equivalent_2(x11,x9),x10)))))) ....... U160 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x6), x4)), equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8)))), x6)))) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x10, x11), equivalent_2(equivalent_2(x11, x3), x10)), equivalent_2(x12, equivalent_2(equivalent_2(x13, x14), equivalent_2(equivalent_2(x14, x12), x13))))) ....... R3 [R2:L1, U160:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), x0)), equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6))))) ....... R4 [R3:L0, U1:L0] % Derivation of unit clause U225: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),equivalent_2(x4,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x5,x3)))) ....... U106 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), equivalent_2(x8, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))), equivalent_2(x9, x7))))) ....... R3 [R2:L2, U106:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4)))), x2), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9, x10), x11), equivalent_2(x10, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))), equivalent_2(x11, x9))))) ....... R4 [R3:L0, U3:L0] % Derivation of unit clause U342: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | ~is_a_theorem_1(x3) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))) | is_a_theorem_1(x2) ....... R3 [R2:L0, U3:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),x2)) ....... U179 % is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))) ....... R4 [R3:L0, U179:L0] % Derivation of unit clause U361: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | ~is_a_theorem_1(x3) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))),x3)),x5))) ....... U171 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))), x0))) | is_a_theorem_1(x2) ....... R3 [R2:L0, U171:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))),x3)),x5))) ....... U171 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), x3), x2), equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5)))))) ....... R4 [R3:L0, U171:L0] % Derivation of unit clause U376: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | ~is_a_theorem_1(x3) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))) ....... U342 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R3 [R2:L0, U342:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),x3),x2),equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))))) ....... U361 % is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x4), x2)), x5), x4), equivalent_2(x5, equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7)))))), x0))) ....... R4 [R3:L0, U361:L0] % Derivation of unit clause U420: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | ~is_a_theorem_1(x3) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),x5),x4),equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))))),x0))) ....... U376 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x5), x3)), x6), x5), equivalent_2(x6, equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8))))))) | is_a_theorem_1(x2) ....... R3 [R2:L0, U376:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))),x2))),x0))) ....... U8 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6)))), x3))), x2)) ....... R4 [R3:L0, U8:L0] % Derivation of unit clause U422: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4))) | ~is_a_theorem_1(x3) | is_a_theorem_1(x4) ....... R2 [R1:L1, B2:L1] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),x5),x4),equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))))),x0))) ....... U376 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x5), x3)), x6), x5), equivalent_2(x6, equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8))))))) | is_a_theorem_1(x2) ....... R3 [R2:L0, U376:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),x2)) ....... U179 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), x3), x2), equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5))))), equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8))))) ....... R4 [R3:L0, U179:L0] % Derivation of unit clause U830: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x0) | ~is_a_theorem_1(x1) | ~is_a_theorem_1(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3))), x0))) ....... R2 [R1:L0, B2:L2] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), x3), x2)) | ~is_a_theorem_1(x3) ....... R3 [R2:L2, U1:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6))))) ....... U181 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6)))), x3)), equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9))))), x2)) ....... R4 [R3:L1, U181:L0] % Derivation of unit clause U841: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x0) | ~is_a_theorem_1(x1) | ~is_a_theorem_1(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3))), x0))) ....... R2 [R1:L0, B2:L2] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), x3), x2)) | ~is_a_theorem_1(x3) ....... R3 [R2:L2, U1:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),x3),x2),equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5)))))) ....... U361 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, x2), x0)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x5), x3)), x6), x5), equivalent_2(x6, equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8)))))), x2)) ....... R4 [R3:L1, U361:L0] % Derivation of unit clause U1172: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x0) | ~is_a_theorem_1(x1) | ~is_a_theorem_1(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3))), x0))) ....... R2 [R1:L0, B2:L2] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),x5),x4),equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))))),x0))) ....... U376 % is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, equivalent_2(x4, x1)), x2))), x4))) ....... R3 [R2:L2, U376:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2)) ....... U4 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, x2)), x3))), x5)), x0)), equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7))))) ....... R4 [R3:L1, U4:L0] % Derivation of unit clause U1179: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), 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(x0) | ~is_a_theorem_1(x1) | ~is_a_theorem_1(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3))), x0))) ....... R2 [R1:L0, B2:L2] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,x4),x2)),x5),x4),equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))))),x0))) ....... U376 % is_a_theorem_1(x0) | ~is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, equivalent_2(x4, x1)), x2))), x4))) ....... R3 [R2:L2, U376:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3))),x2)) ....... U420 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, x2)), x3))), x5)), x0)), equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, equivalent_2(x8, equivalent_2(equivalent_2(x9, x10), equivalent_2(equivalent_2(x10, x8), x9)))), x6)))) ....... R4 [R3:L1, U420:L0] % Derivation of unit clause U1360: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0))) ....... U3 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, x0), x2), equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4)))), equivalent_2(x2, x1))) ....... R3 [R2:L1, U3:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4)))),x2),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),x11),equivalent_2(x10,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x11,x9))))) ....... U225 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), equivalent_2(equivalent_2(equivalent_2(x1, x5), x0), equivalent_2(x5, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))))) ....... R4 [R3:L1, U225:L0] % Derivation of unit clause U1492: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),x2)) ....... U179 % ~is_a_theorem_1(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2))))) | is_a_theorem_1(x0) ....... R3 [R2:L1, U179:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),equivalent_2(equivalent_2(equivalent_2(x1,x5),x0),equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))))) ....... U1360 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), equivalent_2(equivalent_2(equivalent_2(x1, x5), x0), equivalent_2(x5, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0())))))), equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7))))) ....... R4 [R3:L1, U1360:L0] % Derivation of unit clause U1586: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3)),equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9))))),x2)) ....... U830 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2)))), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x0), x4)), x6))) | is_a_theorem_1(x6) ....... R3 [R2:L1, U830:L0] % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... U1 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), x2), equivalent_2(x1, equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))), equivalent_2(x2, x0))) ....... R4 [R3:L0, U1:L0] % Derivation of unit clause U1780: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x5),x3)),x6),x5),equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8)))))),x2)) ....... U841 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x3), x1)), x0), x3)) ....... R3 [R2:L1, U841:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),equivalent_2(equivalent_2(equivalent_2(x1,x5),x0),equivalent_2(x5,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))) ....... U1492 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, equivalent_2(x0, equivalent_2(x4, equivalent_2(equivalent_2(x5, x6), equivalent_2(equivalent_2(x6, x4), x5))))), x2))), equivalent_2(x1, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0())))))) ....... R4 [R3:L1, U1492:L0] % Derivation of unit clause U1909: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) ....... U1586 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), x2)) | is_a_theorem_1(equivalent_2(equivalent_2(x2, x0), x1)) ....... R3 [R2:L1, U1586:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,x2),x0)),x3),x2),equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5))))),equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8))))) ....... U422 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x5), x3)), x6), x5)), equivalent_2(x6, equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, x7), x8)))))) ....... R4 [R3:L0, U422:L0] % Derivation of unit clause U1958: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) ....... U1586 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), x2)) | is_a_theorem_1(equivalent_2(equivalent_2(x2, x0), x1)) ....... R3 [R2:L1, U1586:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,x2)),x3))),x5)),x0)),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7))))) ....... U1172 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(x3, x4)), equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, equivalent_2(x8, x5)), x6))), x8)), x3))) ....... R4 [R3:L0, U1172:L0] % Derivation of unit clause U1964: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) ....... U1586 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), x2)) | is_a_theorem_1(equivalent_2(equivalent_2(x2, x0), x1)) ....... R3 [R2:L1, U1586:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,x2)),x3))),x5)),x0)),equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,equivalent_2(x8,equivalent_2(equivalent_2(x9,x10),equivalent_2(equivalent_2(x10,x8),x9)))),x6)))) ....... U1179 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), x0)), equivalent_2(x5, x6)), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, equivalent_2(x10, x7)), x8))), x10)), x5))) ....... R4 [R3:L0, U1179:L0] % Derivation of unit clause U2099: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) ....... U1586 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), x2)) | is_a_theorem_1(equivalent_2(equivalent_2(x2, x0), x1)) ....... R3 [R2:L1, U1586:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(x3,x4)),equivalent_2(equivalent_2(x4,equivalent_2(equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,equivalent_2(x8,x5)),x6))),x8)),x3))) ....... U1958 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, equivalent_2(x4, x1)), x2))), x4)), x5), equivalent_2(x6, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(x8, x6), x7)))), equivalent_2(x5, x0))) ....... R4 [R3:L0, U1958:L0] % Derivation of unit clause U3282: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),equivalent_2(x1,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),equivalent_2(x2,x0))) ....... U1586 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, x1), x2)) | is_a_theorem_1(equivalent_2(equivalent_2(x2, x0), x1)) ....... R3 [R2:L1, U1586:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x0,equivalent_2(x4,equivalent_2(equivalent_2(x5,x6),equivalent_2(equivalent_2(x6,x4),x5))))),x2))),equivalent_2(x1,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))) ....... U1780 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))), x0)), equivalent_2(x6, equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0()))))), equivalent_2(x2, x6))) ....... R4 [R3:L1, U1780:L0] % Derivation of unit clause U6521: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x5),x3)),x6),x5)),equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8)))))) ....... U1909 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2))))) ....... R3 [R2:L1, U1909:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,x6)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,equivalent_2(x10,x7)),x8))),x10)),x5))) ....... U1964 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, x2), x3)))), x0)), equivalent_2(x5, x6)), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x8, x9), equivalent_2(equivalent_2(x9, equivalent_2(x10, x7)), x8))), x10)), x5)), equivalent_2(x11, equivalent_2(equivalent_2(x12, x13), equivalent_2(equivalent_2(x13, x11), x12))))) ....... R4 [R3:L0, U1964:L0] % Derivation of unit clause U6971: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... R2 [R1:L1, B2:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x5),x3)),x6),x5)),equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,x7),x8)))))) ....... U1909 % ~is_a_theorem_1(x0) | is_a_theorem_1(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x2, x3), equivalent_2(equivalent_2(x3, x1), x2))))) ....... R3 [R2:L1, U1909:L0] % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),equivalent_2(x6,equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0()))))),equivalent_2(x2,x6))) ....... U3282 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(x3, equivalent_2(equivalent_2(x4, x5), equivalent_2(equivalent_2(x5, x3), x4))))), x0)), equivalent_2(equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x2), x6)), equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), c_0()), equivalent_2(b_0(), equivalent_2(c_0(), a_0())))))) ....... R4 [R3:L1, U3282:L0] % Derivation of unit clause U9216: % is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1)))) ....... 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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))) ....... R1 [B1:L0, B2:L1] % ~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(x1, x2), equivalent_2(equivalent_2(x2, x0), x1)), x3)) | is_a_theorem_1(x3) ....... 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(x2,x3),equivalent_2(equivalent_2(x3,equivalent_2(x4,x1)),x2))),x4)),x5),equivalent_2(x6,equivalent_2(equivalent_2(x7,x8),equivalent_2(equivalent_2(x8,x6),x7)))),equivalent_2(x5,x0))) ....... U2099 % ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(x1, x2)), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x3, x0), equivalent_2(x1, x2))) ....... R3 [R2:L1, U2099:L0] % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,x2),x3)))),x0)),equivalent_2(x5,x6)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x7,equivalent_2(equivalent_2(x8,x9),equivalent_2(equivalent_2(x9,equivalent_2(x10,x7)),x8))),x10)),x5)),equivalent_2(x11,equivalent_2(equivalent_2(x12,x13),equivalent_2(equivalent_2(x13,x11),x12))))) ....... U6521 % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, x2), equivalent_2(equivalent_2(x2, x0), x1))), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x6, x7), equivalent_2(equivalent_2(x7, x5), x6)))), x3)), equivalent_2(x8, x9))), equivalent_2(equivalent_2(x9, equivalent_2(equivalent_2(x10, equivalent_2(equivalent_2(x11, x12), equivalent_2(equivalent_2(x12, equivalent_2(x13, x10)), x11))), x13)), x8))) ....... R4 [R3:L0, U6521:L0] % Derivation of the empty clause: % is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,x2),equivalent_2(equivalent_2(x2,x0),x1))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x5),x6)))),x3)),equivalent_2(x8,x9))),equivalent_2(equivalent_2(x9,equivalent_2(equivalent_2(x10,equivalent_2(equivalent_2(x11,x12),equivalent_2(equivalent_2(x12,equivalent_2(x13,x10)),x11))),x13)),x8))) ....... U9216 % ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x4,x5),equivalent_2(equivalent_2(x5,x3),x4))))),x0)),equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(equivalent_2(x7,x2),x6)),equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),c_0()),equivalent_2(b_0(),equivalent_2(c_0(),a_0())))))) ....... U6971 % [] ....... R1 [U9216:L0, U6971:L0] % --------------- End of Proof --------------- % PROOF FOUND! % --------------------------------------------- % | Statistics | % --------------------------------------------- % Profile 3: Performance Statistics: % ================================== % Total number of generated clauses: 447087 % resolvents: 447078 factors: 9 % Number of unit clauses generated: 445082 % % unit clauses generated to total clauses generated: 99.55 % Number of unit clauses constructed and retained at depth [x]: % ============================================================= % [0] = 2 [2] = 10 [4] = 9205 % Total = 9217 % Number of generated clauses having [x] literals: % ------------------------------------------------ % [1] = 445082 [2] = 1991 [3] = 14 % Average size of a generated clause: 2.0 % Number of unit clauses per predicate list: % ========================================== % [0] is_a_theorem_1 (+)1587 (-)7630 % ------------------ % Total: (+)1587 (-)7630 % Total number of unit clauses retained: 9217 % Number of clauses skipped because of their length: 1950 % N base clauses skippped in resolve-with-all-base-clauses % because of the shortest resolvents table: 0 % Number of successful unifications: 447215 % Number of unification failures: 548553 % Number of unit to unit unification failures: 12107074 % N literal unification failure due to lookup root_id table: 29 % 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: 26 % N unit clauses dropped because they exceeded max values: 435528 % N unit clauses dropped because too much nesting: 277384 % 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: 204432 % Total number of terms of all unit clauses in table: 494887 % Max allowed number of states in UCFA: 528000 % Ratio n states used/total allowed states: 0.39 % Ratio n states used/total unit clauses terms: 0.41 % Number of symbols (columns) in UCFA: 39 % Profile 2: Number of calls to: % ============================== % PTUnify() = 995768 % ConstructUnitClause() = 444743 % Profile 1: Time spent in: % ========================= % ConstructUnitClause() : 1.46 secs % -------------------------------------------------------- % | | % Inferences per sec: 13150 % | | % -------------------------------------------------------- % Elapsed time: 34 secs % CPU time: 34.45 secs % %------------------------------------------------------------------------------