CARINE---0.734.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : CARINE---0.734
% Problem  : LCL016-1 : TPTP v5.0.0. Released v1.0.0.
% Transfm  : add_equality
% Format   : carine
% Command  : carine %s t=%d xo=off uct=32000

% Computer : art06.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 : Sat Nov 27 23:17:30 EST 2010

% Result   : Unsatisfiable 15.43s
% Output   : Refutation 15.43s
% 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/SystemOnTPTP19011/LCL/LCL016-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 = 49] [nf = 0] [nu = 20] [ut = 16]
% Looking for a proof at depth = 3 ...
% 	t = 0 secs [nr = 118] [nf = 5] [nu = 55] [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(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))))
% B1: is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))))
% 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(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))))
% U3: < d2 v8 dv4 f7 c0 t15 td7 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))))
% U4: < d2 v12 dv6 f11 c0 t23 td7 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4)))
% U8: < d2 v10 dv5 f9 c0 t19 td9 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x2,x3),x4))),equivalent_2(x4,x3))),x1)))
% U9: < d2 v14 dv7 f13 c0 t27 td8 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1))))))
% U10: < d2 v12 dv6 f11 c0 t23 td11 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))),x2)),x1)))
% U11: < d2 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,x3)),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x3),x2))))),x1)))
% U40: < d4 v6 dv3 f11 c6 t23 td7 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),x1),x0),x2),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))))
% U113: < d4 v14 dv7 f13 c0 t27 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5)))
% U115: < d4 v20 dv10 f19 c0 t39 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(x4,x5)),equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,x7),x6))),equivalent_2(x9,equivalent_2(equivalent_2(x9,x5),x4)))))
% U200: < d4 v18 dv9 f17 c0 t35 td7 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,x4)),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(x8,equivalent_2(equivalent_2(x8,x4),x3)))))
% U203: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6))),x4))))
% U221: < d4 v12 dv6 f17 c6 t35 td8 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),x4),x3),x5),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))))))
% U302: < d4 v16 dv8 f15 c0 t31 td9 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6))))))
% U354: < d4 v22 dv11 f21 c0 t43 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),x4),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(equivalent_2(x4,equivalent_2(x8,equivalent_2(equivalent_2(x8,x9),x10))),equivalent_2(x10,x9)))))
% U449: < d4 v20 dv10 f19 c0 t39 td9 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,equivalent_2(equivalent_2(x3,x2),x1))),equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6)))),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,equivalent_2(equivalent_2(x9,x8),x7))),equivalent_2(x6,x5)))))
% U450: < d4 v18 dv9 f17 c0 t35 td11 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7))),x5)))))
% U594: < d4 v20 dv10 f25 c6 t51 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5)),equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x5,x4)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),x8),x7),x9),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))))))))
% U607: < d4 v22 dv11 f21 c0 t43 td11 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,x5)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(x9,x8))),equivalent_2(x10,equivalent_2(equivalent_2(x10,x5),x4)))))))
% U682: < d4 v26 dv13 f25 c0 t51 td9 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4)),x6),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,equivalent_2(equivalent_2(x9,x8),x7))),equivalent_2(equivalent_2(x6,equivalent_2(x10,equivalent_2(equivalent_2(x10,x11),x12))),equivalent_2(x12,x11)))))
% U683: < d4 v20 dv10 f19 c0 t39 td8 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(x3,equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(x9,x8)))))
% U738: < d4 v22 dv11 f21 c0 t43 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x7,equivalent_2(x8,equivalent_2(equivalent_2(x8,x9),x10))),equivalent_2(x10,x9))),x7))))
% U828: < d4 v16 dv8 f15 c0 t31 td10 > is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x2),x1))))))
% U904: < d4 v26 dv13 f25 c0 t51 td10 > is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7)),equivalent_2(equivalent_2(x9,equivalent_2(x10,equivalent_2(equivalent_2(x10,x11),x12))),equivalent_2(x12,x11))),x9)))
% U1340: < d4 v10 dv5 f15 c6 t31 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),x4),x3),x4))))
% U1710: < d4 v16 dv8 f21 c6 t43 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),x7)),x3),x7)))
% U2201: < d4 v26 dv13 f31 c6 t63 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(equivalent_2(equivalent_2(x10,x11),equivalent_2(x12,equivalent_2(equivalent_2(x12,x11),x10))),equivalent_2(x9,x8))))))
% U2628: < d4 v14 dv7 f19 c6 t39 td8 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x4),x3))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x5)))
% U3031: < d4 v22 dv11 f27 c6 t55 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5)),equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x5,x4)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),equivalent_2(x10,equivalent_2(equivalent_2(x10,x8),x7))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x9))))))
% U3441: < d4 v18 dv9 f23 c6 t47 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5,x6),x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,x6),x5))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x7))),x4)))
% U3865: < d4 v12 dv6 f17 c6 t35 td8 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()))))
% U4386: < d4 v14 dv7 f19 c6 t39 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))))))
% U5042: < d4 v24 dv12 f29 c6 t59 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x2,x3),x4))),equivalent_2(x4,x3))),x1)),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),equivalent_2(x8,equivalent_2(equivalent_2(x8,equivalent_2(x9,equivalent_2(equivalent_2(x9,x10),x11))),equivalent_2(x11,x10)))))))
% U5840: < d4 v16 dv8 f21 c6 t43 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,equivalent_2(x5,x6)),equivalent_2(x3,equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))))))))
% U6816: < d4 v24 dv12 f29 c6 t59 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,equivalent_2(x9,x10)),equivalent_2(x7,equivalent_2(x11,equivalent_2(equivalent_2(x11,x10),x9)))))))))
% U7757: < d4 v14 dv7 f19 c6 t39 td10 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x3),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),x6),x4)),equivalent_2(x6,x5))))
% U8673: < d4 v22 dv11 f27 c6 t55 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x7),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),x10),x8)),equivalent_2(x10,x9)))))
% U9594: < d4 v16 dv8 f21 c6 t43 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,x5)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x6),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x6,x7),x5),x4),x7))))))
% U10539: < d4 v22 dv11 f27 c6 t55 td11 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),x6),equivalent_2(x7,x8)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x9),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),x8),x7),x10))),x6)))
% U11503: < d4 v26 dv13 f31 c6 t63 td9 > ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),equivalent_2(x11,equivalent_2(equivalent_2(x11,x10),x9))),equivalent_2(a_0(),x12)),equivalent_2(x12,equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()))))))
% --------------- Start of Proof ---------------
% Derivation of unit clause U1:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
% Derivation of unit clause U3:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0]
%  is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%   is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2)))) ....... R2 [R1:L0, U1:L0]
% Derivation of unit clause U4:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(x3) ....... R1 [B1:L0, B2:L0]
%  is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2)))) ....... U3
%   is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), x5))), equivalent_2(x5, x4))) ....... R2 [R1:L0, U3:L0]
% Derivation of unit clause U8:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(x0, x1)) | is_a_theorem_1(equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))) ....... R1 [B1:L0, B2:L1]
%  is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2)))) ....... U3
%   is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x2, x3), x4))), equivalent_2(x4, x3))), x1))) ....... R2 [R1:L0, U3:L0]
% Derivation of unit clause U9:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(x0, x1)) | is_a_theorem_1(equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))) ....... R1 [B1:L0, B2:L1]
%  is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%   is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, x2)), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), equivalent_2(x6, equivalent_2(equivalent_2(x6, x2), x1)))))) ....... R2 [R1:L0, U4:L0]
% Derivation of unit clause U10:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(x0, x1)) | is_a_theorem_1(equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))) ....... R1 [B1:L0, B2:L1]
%  is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x2,x3),x4))),equivalent_2(x4,x3))),x1))) ....... U8
%   is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x2, equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), x5))), equivalent_2(x5, x4))), x2)), x1))) ....... R2 [R1:L0, U8:L0]
% Derivation of unit clause U11:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(x0, x1)) | is_a_theorem_1(equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))) ....... R1 [B1:L0, B2:L1]
%  is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%   is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(x2, x3)), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(x7, equivalent_2(equivalent_2(x7, x3), x2))))), x1))) ....... R2 [R1:L0, U9:L0]
% Derivation of unit clause U40:
% ~is_a_theorem_1(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),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(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), 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(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), 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(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%    ~is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))))) | ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, equivalent_2(equivalent_2(x3, x2), x1))), equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5)), x0)) ....... R3 [R2:L1, U4:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), x2), x1), x0), x2), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))))) ....... R4 [R3:L1, U4:L0]
% Derivation of unit clause U113:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%    ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), x4)) | is_a_theorem_1(x4) ....... R3 [R2:L0, U1:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2)))) ....... U3
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5))) ....... R4 [R3:L0, U3:L0]
% Derivation of unit clause U115:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%    ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), x4)) | is_a_theorem_1(x4) ....... R3 [R2:L0, U1:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), equivalent_2(x4, x5)), equivalent_2(equivalent_2(equivalent_2(x6, x7), equivalent_2(x8, equivalent_2(equivalent_2(x8, x7), x6))), equivalent_2(x9, equivalent_2(equivalent_2(x9, x5), x4))))) ....... R4 [R3:L0, U9:L0]
% Derivation of unit clause U200:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U4:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, x4)), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(x8, equivalent_2(equivalent_2(x8, x4), x3))))) ....... R4 [R3:L0, U9:L0]
% Derivation of unit clause U203:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U4:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,x4)),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(x8,equivalent_2(equivalent_2(x8,x4),x3))))) ....... U200
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x5, x6), x7))), equivalent_2(x7, x6))), x4)))) ....... R4 [R3:L0, U200:L0]
% Derivation of unit clause U221:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(x3) ....... R3 [R2:L0, U4:L0]
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),x2),x1),x0),x2),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))))) ....... U40
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), x5), x4), x3), x5), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))))) ....... R4 [R3:L1, U40:L0]
% Derivation of unit clause U302:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x2,x3),x4))),equivalent_2(x4,x3))),x1))) ....... U8
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5))), x3), x7)) | is_a_theorem_1(x7) ....... R3 [R2:L0, U8:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(equivalent_2(x2, x3), equivalent_2(x4, equivalent_2(equivalent_2(x4, x3), x2))), equivalent_2(equivalent_2(x1, equivalent_2(x5, equivalent_2(equivalent_2(x5, x6), x7))), equivalent_2(x7, x6)))))) ....... R4 [R3:L0, U1:L0]
% Derivation of unit clause U354:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))) ....... U113
%    ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), x4)) | is_a_theorem_1(x4) ....... R3 [R2:L0, U113:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6)))))) ....... U302
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), x4), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(equivalent_2(x4, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))))) ....... R4 [R3:L0, U302:L0]
% Derivation of unit clause U449:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, x4))) | is_a_theorem_1(equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))) ....... R3 [R2:L1, U1:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(equivalent_2(x1, x2), equivalent_2(x3, equivalent_2(equivalent_2(x3, x2), x1))), equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6)))), equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), equivalent_2(x6, x5))))) ....... R4 [R3:L0, U9:L0]
% Derivation of unit clause U450:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, x4))) | is_a_theorem_1(equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))) ....... R3 [R2:L1, U1:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x2,equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))),x2)),x1))) ....... U10
%     is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, x1), equivalent_2(equivalent_2(equivalent_2(x2, x3), equivalent_2(x4, equivalent_2(equivalent_2(x4, x3), x2))), equivalent_2(equivalent_2(x1, equivalent_2(equivalent_2(x5, equivalent_2(x6, equivalent_2(equivalent_2(x6, x7), x8))), equivalent_2(x8, x7))), x5))))) ....... R4 [R3:L0, U10:L0]
% Derivation of unit clause U594:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,x3)),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x3),x2))))),x1))) ....... U11
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(x5, x6)), equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), equivalent_2(x10, equivalent_2(equivalent_2(x10, x6), x5))))), x4)) ....... R3 [R2:L1, U11:L0]
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),x4),x3),x5),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))))) ....... U221
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), x5)), equivalent_2(x6, equivalent_2(equivalent_2(x6, equivalent_2(x5, x4)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), x8), x7), x9), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))))))))) ....... R4 [R3:L1, U221:L0]
% Derivation of unit clause U607:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(x4,x5)),equivalent_2(equivalent_2(equivalent_2(x6,x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,x7),x6))),equivalent_2(x9,equivalent_2(equivalent_2(x9,x5),x4))))) ....... U115
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5))), equivalent_2(x7, x8)))) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x9, x10), equivalent_2(x11, equivalent_2(equivalent_2(x11, x10), x9))), equivalent_2(x12, equivalent_2(equivalent_2(x12, x8), x7)))) ....... R3 [R2:L1, U115:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, x5)), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(x6, equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), x9))), equivalent_2(x9, x8))), equivalent_2(x10, equivalent_2(equivalent_2(x10, x5), x4))))))) ....... R4 [R3:L0, U1:L0]
% Derivation of unit clause U682:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6)))))) ....... U302
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(equivalent_2(x4, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))))) ....... R3 [R2:L1, U302:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2)))) ....... U3
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), x5))), equivalent_2(x5, x4)), x6), equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), equivalent_2(equivalent_2(x6, equivalent_2(x10, equivalent_2(equivalent_2(x10, x11), x12))), equivalent_2(x12, x11))))) ....... R4 [R3:L0, U3:L0]
% Derivation of unit clause U683:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6)))))) ....... U302
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(equivalent_2(x4, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))))) ....... R3 [R2:L1, U302:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x3, equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), x9))), equivalent_2(x9, x8))))) ....... R4 [R3:L0, U4:L0]
% Derivation of unit clause U738:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,x1),equivalent_2(equivalent_2(equivalent_2(x2,x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,x3),x2))),equivalent_2(equivalent_2(x1,equivalent_2(equivalent_2(x5,equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7))),x5))))) ....... U450
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | is_a_theorem_1(equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x8, equivalent_2(x9, equivalent_2(equivalent_2(x9, x10), x11))), equivalent_2(x11, x10))), x8)))) ....... R3 [R2:L1, U450:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x7, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))), x7)))) ....... R4 [R3:L0, U4:L0]
% Derivation of unit clause U828:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,x5)),equivalent_2(equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(x9,x8))),equivalent_2(x10,equivalent_2(equivalent_2(x10,x5),x4))))))) ....... U607
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))))) | is_a_theorem_1(equivalent_2(x6, equivalent_2(equivalent_2(x6, equivalent_2(x7, x8)), equivalent_2(equivalent_2(x9, equivalent_2(equivalent_2(x9, equivalent_2(x10, equivalent_2(equivalent_2(x10, x11), x12))), equivalent_2(x12, x11))), equivalent_2(x13, equivalent_2(equivalent_2(x13, x8), x7)))))) ....... R3 [R2:L1, U607:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4))) ....... U4
%     is_a_theorem_1(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, x2)), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5))), equivalent_2(x7, equivalent_2(equivalent_2(x7, x2), x1)))))) ....... R4 [R3:L0, U4:L0]
% Derivation of unit clause U904:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x7,equivalent_2(x8,equivalent_2(equivalent_2(x8,x9),x10))),equivalent_2(x10,x9))),x7)))) ....... U738
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), x6))) | is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), equivalent_2(equivalent_2(x6, equivalent_2(equivalent_2(x10, equivalent_2(x11, equivalent_2(equivalent_2(x11, x12), x13))), equivalent_2(x13, x12))), x10))) ....... R3 [R2:L1, U738:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), equivalent_2(x6, equivalent_2(equivalent_2(x6, x7), x8))), equivalent_2(x8, x7)), equivalent_2(equivalent_2(x9, equivalent_2(x10, equivalent_2(equivalent_2(x10, x11), x12))), equivalent_2(x12, x11))), x9))) ....... R4 [R3:L0, U1:L0]
% Derivation of unit clause U1340:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5)),equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x5,x4)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),x8),x7),x9),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))))))))) ....... U594
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), x9)), equivalent_2(x10, equivalent_2(equivalent_2(x10, equivalent_2(x9, x8)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x11, x12), x13), x12), x11), x13), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))))))))) ....... R3 [R2:L2, U594:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), x4), x3), x4)))) ....... R4 [R3:L1, U9:L0]
% Derivation of unit clause U1710:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),x4),x3),x4)))) ....... U1340
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(x7, equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), x8), x7), x8))))) ....... R3 [R2:L2, U1340:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), x3), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), x7)), x3), x7))) ....... R4 [R3:L1, U1:L0]
% Derivation of unit clause U2201:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),x7)),x3),x7))) ....... U1710
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), x7), equivalent_2(equivalent_2(equivalent_2(x8, x9), equivalent_2(x10, equivalent_2(equivalent_2(x10, x9), x8))), x11)), x7), x11)))) ....... R3 [R2:L2, U1710:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),x4),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(equivalent_2(x4,equivalent_2(x8,equivalent_2(equivalent_2(x8,x9),x10))),equivalent_2(x10,x9))))) ....... U354
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), x9))), equivalent_2(equivalent_2(equivalent_2(x10, x11), equivalent_2(x12, equivalent_2(equivalent_2(x12, x11), x10))), equivalent_2(x9, x8)))))) ....... R4 [R3:L1, U354:L0]
% Derivation of unit clause U2628:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0()))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(equivalent_2(equivalent_2(x10,x11),equivalent_2(x12,equivalent_2(equivalent_2(x12,x11),x10))),equivalent_2(x9,x8)))))) ....... U2201
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x7, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0()))), equivalent_2(x11, equivalent_2(equivalent_2(x11, x12), x13))), equivalent_2(equivalent_2(equivalent_2(x14, x15), equivalent_2(x16, equivalent_2(equivalent_2(x16, x15), x14))), equivalent_2(x13, x12))))))) ....... R3 [R2:L2, U2201:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x2),x1)))))) ....... U828
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x4), x3))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x5))) ....... R4 [R3:L1, U828:L0]
% Derivation of unit clause U3031:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x4),x3))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x5))) ....... U2628
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), equivalent_2(x10, equivalent_2(equivalent_2(x10, x8), x7))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x9)))) ....... R3 [R2:L2, U2628:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,x3)),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x3),x2))))),x1))) ....... U11
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), x5)), equivalent_2(x6, equivalent_2(equivalent_2(x6, equivalent_2(x5, x4)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), equivalent_2(x10, equivalent_2(equivalent_2(x10, x8), x7))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x9)))))) ....... R4 [R3:L1, U11:L0]
% Derivation of unit clause U3441:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5)),equivalent_2(x6,equivalent_2(equivalent_2(x6,equivalent_2(x5,x4)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),equivalent_2(x10,equivalent_2(equivalent_2(x10,x8),x7))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x9)))))) ....... U3031
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), x9)), equivalent_2(x10, equivalent_2(equivalent_2(x10, equivalent_2(x9, x8)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x11, x12), x13), equivalent_2(x14, equivalent_2(equivalent_2(x14, x12), x11))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x13))))))) ....... R3 [R2:L2, U3031:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5))),equivalent_2(x7,equivalent_2(equivalent_2(x7,x2),x1)))))) ....... U828
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(x3, equivalent_2(equivalent_2(x3, x4), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5, x6), x7), equivalent_2(x8, equivalent_2(equivalent_2(x8, x6), x5))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x7))), x4))) ....... R4 [R3:L1, U828:L0]
% Derivation of unit clause U3865:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x5,x6),x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,x6),x5))),equivalent_2(equivalent_2(a_0(),b_0()),equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())))),x7))),x4))) ....... U3441
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(x7, equivalent_2(equivalent_2(x7, x8), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9, x10), x11), equivalent_2(x12, equivalent_2(equivalent_2(x12, x10), x9))), equivalent_2(equivalent_2(a_0(), b_0()), equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())))), x11))), x8)))) ....... R3 [R2:L2, U3441:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),x3),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(x3,equivalent_2(x7,equivalent_2(equivalent_2(x7,x8),x9))),equivalent_2(x9,x8))))) ....... U683
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0())))) ....... R4 [R3:L1, U683:L0]
% Derivation of unit clause U4386:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0())))) ....... U3865
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()))))) ....... R3 [R2:L2, U3865:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, equivalent_2(equivalent_2(x4, x5), x6))), equivalent_2(x6, x5)))))) ....... R4 [R3:L1, U1:L0]
% Derivation of unit clause U5042:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6))),equivalent_2(x6,x5)))))) ....... U4386
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), equivalent_2(x7, equivalent_2(equivalent_2(x7, equivalent_2(x8, equivalent_2(equivalent_2(x8, x9), x10))), equivalent_2(x10, x9))))))) ....... R3 [R2:L2, U4386:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(equivalent_2(x4,equivalent_2(x5,equivalent_2(equivalent_2(x5,x6),x7))),equivalent_2(x7,x6))),x4)))) ....... U203
%     ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x1, equivalent_2(x2, equivalent_2(equivalent_2(x2, x3), x4))), equivalent_2(x4, x3))), x1)), equivalent_2(equivalent_2(equivalent_2(x5, x6), equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), equivalent_2(x8, equivalent_2(equivalent_2(x8, equivalent_2(x9, equivalent_2(equivalent_2(x9, x10), x11))), equivalent_2(x11, x10))))))) ....... R4 [R3:L0, U203:L0]
% Derivation of unit clause U5840:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(equivalent_2(x1,equivalent_2(x2,equivalent_2(equivalent_2(x2,x3),x4))),equivalent_2(x4,x3))),x1)),equivalent_2(equivalent_2(equivalent_2(x5,x6),equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),equivalent_2(x8,equivalent_2(equivalent_2(x8,equivalent_2(x9,equivalent_2(equivalent_2(x9,x10),x11))),equivalent_2(x11,x10))))))) ....... U5042
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x5, equivalent_2(x6, equivalent_2(equivalent_2(x6, x7), x8))), equivalent_2(x8, x7))), x5)), equivalent_2(equivalent_2(equivalent_2(x9, x10), equivalent_2(x11, equivalent_2(equivalent_2(x11, x10), x9))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), equivalent_2(x12, equivalent_2(equivalent_2(x12, equivalent_2(x13, equivalent_2(equivalent_2(x13, x14), x15))), equivalent_2(x15, x14)))))))) ....... R3 [R2:L2, U5042:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x3), equivalent_2(x4, equivalent_2(equivalent_2(x4, equivalent_2(x5, x6)), equivalent_2(x3, equivalent_2(x7, equivalent_2(equivalent_2(x7, x6), x5)))))))) ....... R4 [R3:L1, U9:L0]
% Derivation of unit clause U6816:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x3),equivalent_2(x4,equivalent_2(equivalent_2(x4,equivalent_2(x5,x6)),equivalent_2(x3,equivalent_2(x7,equivalent_2(equivalent_2(x7,x6),x5)))))))) ....... U5840
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x7), equivalent_2(x8, equivalent_2(equivalent_2(x8, equivalent_2(x9, x10)), equivalent_2(x7, equivalent_2(x11, equivalent_2(equivalent_2(x11, x10), x9))))))))) ....... R3 [R2:L2, U5840:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x7), equivalent_2(x8, equivalent_2(equivalent_2(x8, equivalent_2(x9, x10)), equivalent_2(x7, equivalent_2(x11, equivalent_2(equivalent_2(x11, x10), x9))))))))) ....... R4 [R3:L0, U1:L0]
% Derivation of unit clause U7757:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x7),equivalent_2(x8,equivalent_2(equivalent_2(x8,equivalent_2(x9,x10)),equivalent_2(x7,equivalent_2(x11,equivalent_2(equivalent_2(x11,x10),x9))))))))) ....... U6816
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x5, x6), x7))), equivalent_2(x7, x6))), equivalent_2(equivalent_2(equivalent_2(x8, x9), equivalent_2(x10, equivalent_2(equivalent_2(x10, x9), x8))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x11), equivalent_2(x12, equivalent_2(equivalent_2(x12, equivalent_2(x13, x14)), equivalent_2(x11, equivalent_2(x15, equivalent_2(equivalent_2(x15, x14), x13)))))))))) ....... R3 [R2:L2, U6816:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(x1,x2)),equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x2),x1)))))) ....... U9
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x3), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), x5), x6), x4)), equivalent_2(x6, x5)))) ....... R4 [R3:L1, U9:L0]
% Derivation of unit clause U8673:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x3),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),x5),x6),x4)),equivalent_2(x6,x5)))) ....... U7757
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x7), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), x10), x8)), equivalent_2(x10, x9))))) ....... R3 [R2:L2, U7757:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     ~is_a_theorem_1(equivalent_2(equivalent_2(x0, equivalent_2(equivalent_2(x0, equivalent_2(x1, equivalent_2(equivalent_2(x1, x2), x3))), equivalent_2(x3, x2))), equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x7), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), x9), x10), x8)), equivalent_2(x10, x9))))) ....... R4 [R3:L0, U1:L0]
% Derivation of unit clause U9594:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(x0,equivalent_2(x1,equivalent_2(equivalent_2(x1,x2),x3))),equivalent_2(x3,x2))),equivalent_2(equivalent_2(equivalent_2(x4,x5),equivalent_2(x6,equivalent_2(equivalent_2(x6,x5),x4))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x7),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7,x8),x9),x10),x8)),equivalent_2(x10,x9))))) ....... U8673
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(x4, equivalent_2(equivalent_2(x4, equivalent_2(x5, equivalent_2(equivalent_2(x5, x6), x7))), equivalent_2(x7, x6))), equivalent_2(equivalent_2(equivalent_2(x8, x9), equivalent_2(x10, equivalent_2(equivalent_2(x10, x9), x8))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x11), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x11, x12), x13), x14), x12)), equivalent_2(x14, x13)))))) ....... R3 [R2:L2, U8673:L0]
%    is_a_theorem_1(equivalent_2(x0,equivalent_2(equivalent_2(x0,equivalent_2(equivalent_2(equivalent_2(x1,x2),equivalent_2(x3,equivalent_2(equivalent_2(x3,x2),x1))),equivalent_2(x4,equivalent_2(equivalent_2(x4,x5),x6)))),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,equivalent_2(equivalent_2(x9,x8),x7))),equivalent_2(x6,x5))))) ....... U449
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(x3, equivalent_2(equivalent_2(x3, equivalent_2(x4, x5)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x6), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x6, x7), x5), x4), x7)))))) ....... R4 [R3:L1, U449:L0]
% Derivation of unit clause U10539:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,equivalent_2(x4,x5)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x6),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x6,x7),x5),x4),x7)))))) ....... U9594
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(x7, equivalent_2(equivalent_2(x7, equivalent_2(x8, x9)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x10), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x10, x11), x9), x8), x11))))))) ....... R3 [R2:L2, U9594:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... U1
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), x6), equivalent_2(x7, x8)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x9), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9, x10), x8), x7), x10))), x6))) ....... R4 [R3:L1, U1:L0]
% Derivation of unit clause U11503:
% is_a_theorem_1(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0)))) ....... 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), 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,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),x6),equivalent_2(x7,x8)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0()),a_0()),x9),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),x8),x7),x10))),x6))) ....... U10539
%    ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), x3)) | ~is_a_theorem_1(equivalent_2(x3, equivalent_2(equivalent_2(equivalent_2(x4, x5), equivalent_2(x6, equivalent_2(equivalent_2(x6, x5), x4))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x7, x8), equivalent_2(x9, equivalent_2(equivalent_2(x9, x8), x7))), x10), equivalent_2(x11, x12)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0()), a_0()), x13), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x13, x14), x12), x11), x14))), x10)))) ....... R3 [R2:L2, U10539:L0]
%    is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(x3,equivalent_2(equivalent_2(x3,x4),x5))),equivalent_2(x5,x4)),x6),equivalent_2(equivalent_2(equivalent_2(x7,x8),equivalent_2(x9,equivalent_2(equivalent_2(x9,x8),x7))),equivalent_2(equivalent_2(x6,equivalent_2(x10,equivalent_2(equivalent_2(x10,x11),x12))),equivalent_2(x12,x11))))) ....... U682
%     ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0, x1), equivalent_2(x2, equivalent_2(equivalent_2(x2, x1), x0))), equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3, x4), equivalent_2(x5, equivalent_2(equivalent_2(x5, x4), x3))), equivalent_2(x6, equivalent_2(equivalent_2(x6, x7), x8))), equivalent_2(x8, x7)), equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9, x10), equivalent_2(x11, equivalent_2(equivalent_2(x11, x10), x9))), equivalent_2(a_0(), x12)), equivalent_2(x12, equivalent_2(equivalent_2(c_0(), equivalent_2(equivalent_2(b_0(), c_0()), a_0())), b_0())))))) ....... R4 [R3:L1, U682:L0]
% Derivation of the empty clause:
% ~is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7)),equivalent_2(equivalent_2(equivalent_2(equivalent_2(x9,x10),equivalent_2(x11,equivalent_2(equivalent_2(x11,x10),x9))),equivalent_2(a_0(),x12)),equivalent_2(x12,equivalent_2(equivalent_2(c_0(),equivalent_2(equivalent_2(b_0(),c_0()),a_0())),b_0())))))) ....... U11503
% is_a_theorem_1(equivalent_2(equivalent_2(equivalent_2(x0,x1),equivalent_2(x2,equivalent_2(equivalent_2(x2,x1),x0))),equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(equivalent_2(x3,x4),equivalent_2(x5,equivalent_2(equivalent_2(x5,x4),x3))),equivalent_2(x6,equivalent_2(equivalent_2(x6,x7),x8))),equivalent_2(x8,x7)),equivalent_2(equivalent_2(x9,equivalent_2(x10,equivalent_2(equivalent_2(x10,x11),x12))),equivalent_2(x12,x11))),x9))) ....... U904
%  [] ....... R1 [U11503:L0, U904:L0]
% --------------- End of Proof ---------------
% PROOF FOUND!
% ---------------------------------------------
% |                Statistics                 |
% ---------------------------------------------
% Profile 3: Performance Statistics:
% ==================================
% Total number of generated clauses: 560951
% 	resolvents: 560942	factors: 9
% Number of unit clauses generated: 550308
% % unit clauses generated to total clauses generated: 98.10
% Number of unit clauses constructed and retained at depth [x]:
% =============================================================
% [0] = 2		[2] = 14	[4] = 11488	
% Total = 11504
% Number of generated clauses having [x] literals:
% ------------------------------------------------
% [1] = 550308	[2] = 10632	[3] = 11	
% Average size of a generated clause: 2.0
% Number of unit clauses per predicate list:
% ==========================================
% [0] is_a_theorem_1	(+)155	(-)11349
% 			------------------
% 		Total:	(+)155	(-)11349
% Total number of unit clauses retained: 11504
% Number of clauses skipped because of their length: 10580
% N base clauses skippped in resolve-with-all-base-clauses
% 	because of the shortest resolvents table: 0
% Number of successful unifications: 561095
% Number of unification failures: 2791720
% Number of unit to unit unification failures: 1759043
% 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: 23
% N unit clauses dropped because they exceeded max values: 538650
% N unit clauses dropped because too much nesting: 96299
% 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: 154320
% Total number of terms of all unit clauses in table: 644060
% Max allowed number of states in UCFA: 528000
% Ratio n states used/total allowed states: 0.29
% Ratio n states used/total unit clauses terms: 0.24
% Number of symbols (columns) in UCFA: 39
% Profile 2: Number of calls to:
% ==============================
% PTUnify() = 3352815
% ConstructUnitClause() = 550152
% Profile 1: Time spent in:
% =========================
% ConstructUnitClause() : 2.57 secs
% --------------------------------------------------------
% |                                                      |
%   Inferences per sec: 37397
% |                                                      |
% --------------------------------------------------------
% Elapsed time: 15 secs
% CPU time: 15.42 secs
% 
%------------------------------------------------------------------------------