%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP162-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:39:04 EDT 2024
% Result : Unsatisfiable 73.14s 73.17s
% Output : CNFRefutation 73.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GRP162-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 20 07:01:39 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 73.10/73.16 %-------------------------------------------
% 73.10/73.16 % File :CSE---1.7
% 73.10/73.16 % Problem :theBenchmark
% 73.10/73.16 % Transform :cnf
% 73.10/73.16 % Format :tptp:raw
% 73.10/73.16 % Command :java -jar mcs_scs.jar %d %s
% 73.10/73.16
% 73.10/73.16 % Result :Theorem 72.540000s
% 73.10/73.16 % Output :CNFRefutation 72.540000s
% 73.10/73.16 %-------------------------------------------
% 73.14/73.17 %--------------------------------------------------------------------------
% 73.14/73.17 % File : GRP162-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 73.14/73.17 % Domain : Group Theory (Lattice Ordered)
% 73.14/73.17 % Problem : Prove transitivity axiom using the LUB transformation
% 73.14/73.17 % Version : [Fuc94] (equality) axioms.
% 73.14/73.17 % English : This problem proves the original transitivity axiom from the
% 73.14/73.17 % equational axiomatization.
% 73.14/73.17
% 73.14/73.17 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 73.14/73.17 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 73.14/73.17 % Source : [Sch95]
% 73.14/73.17 % Names : ax_transa [Sch95]
% 73.14/73.17
% 73.14/73.17 % Status : Unsatisfiable
% 73.14/73.17 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v2.0.0
% 73.14/73.17 % Syntax : Number of clauses : 18 ( 18 unt; 0 nHn; 3 RR)
% 73.14/73.17 % Number of literals : 18 ( 18 equ; 1 neg)
% 73.14/73.17 % Maximal clause size : 1 ( 1 avg)
% 73.14/73.17 % Maximal term depth : 3 ( 1 avg)
% 73.14/73.17 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 73.14/73.17 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 73.14/73.17 % Number of variables : 33 ( 2 sgn)
% 73.14/73.17 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 73.14/73.17
% 73.14/73.17 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 73.14/73.17 % least_upper_bound > identity > a > b > c
% 73.14/73.17 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 73.14/73.17 %--------------------------------------------------------------------------
% 73.14/73.17 %----Include equality group theory axioms
% 73.14/73.17 include('Axioms/GRP004-0.ax').
% 73.14/73.17 %----Include Lattice ordered group (equality) axioms
% 73.14/73.17 include('Axioms/GRP004-2.ax').
% 73.14/73.17 %--------------------------------------------------------------------------
% 73.14/73.17 cnf(ax_transa_1,hypothesis,
% 73.14/73.17 least_upper_bound(a,b) = b ).
% 73.14/73.17
% 73.14/73.17 cnf(ax_transa_2,hypothesis,
% 73.14/73.17 least_upper_bound(b,c) = c ).
% 73.14/73.17
% 73.14/73.17 cnf(prove_ax_transa,negated_conjecture,
% 73.14/73.17 least_upper_bound(a,c) != c ).
% 73.14/73.17
% 73.14/73.17 %--------------------------------------------------------------------------
% 73.14/73.17 %-------------------------------------------
% 73.14/73.17 % Proof found
% 73.14/73.17 % SZS status Theorem for theBenchmark
% 73.14/73.17 % SZS output start Proof
% 73.14/73.17 %ClaNum:28(EqnAxiom:10)
% 73.14/73.17 %VarNum:72(SingletonVarNum:33)
% 73.14/73.17 %MaxLitNum:1
% 73.14/73.17 %MaxfuncDepth:2
% 73.14/73.17 %SharedTerms:10
% 73.14/73.17 %goalClause: 28
% 73.14/73.17 %singleGoalClaCount:1
% 73.14/73.17 [11]E(f3(a1,a2),a2)
% 73.14/73.17 [12]E(f3(a2,a4),a4)
% 73.14/73.17 [28]~E(f3(a1,a4),a4)
% 73.14/73.17 [13]E(f8(a5,x131),x131)
% 73.14/73.17 [14]E(f6(x141,x141),x141)
% 73.14/73.17 [15]E(f3(x151,x151),x151)
% 73.14/73.17 [16]E(f8(f7(x161),x161),a5)
% 73.14/73.17 [17]E(f6(x171,x172),f6(x172,x171))
% 73.14/73.17 [18]E(f3(x181,x182),f3(x182,x181))
% 73.14/73.17 [19]E(f6(x191,f3(x191,x192)),x191)
% 73.14/73.17 [20]E(f3(x201,f6(x201,x202)),x201)
% 73.14/73.17 [21]E(f6(f6(x211,x212),x213),f6(x211,f6(x212,x213)))
% 73.14/73.17 [22]E(f3(f3(x221,x222),x223),f3(x221,f3(x222,x223)))
% 73.14/73.17 [23]E(f8(f8(x231,x232),x233),f8(x231,f8(x232,x233)))
% 73.14/73.17 [24]E(f6(f8(x241,x242),f8(x241,x243)),f8(x241,f6(x242,x243)))
% 73.14/73.17 [25]E(f3(f8(x251,x252),f8(x251,x253)),f8(x251,f3(x252,x253)))
% 73.14/73.17 [26]E(f6(f8(x261,x262),f8(x263,x262)),f8(f6(x261,x263),x262))
% 73.14/73.17 [27]E(f3(f8(x271,x272),f8(x273,x272)),f8(f3(x271,x273),x272))
% 73.14/73.17 %EqnAxiom
% 73.14/73.17 [1]E(x11,x11)
% 73.14/73.17 [2]E(x22,x21)+~E(x21,x22)
% 73.14/73.17 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 73.14/73.17 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 73.14/73.17 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 73.14/73.17 [6]~E(x61,x62)+E(f8(x61,x63),f8(x62,x63))
% 73.14/73.18 [7]~E(x71,x72)+E(f8(x73,x71),f8(x73,x72))
% 73.14/73.18 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83))
% 73.14/73.18 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92))
% 73.14/73.18 [10]~E(x101,x102)+E(f7(x101),f7(x102))
% 73.14/73.18
% 73.14/73.18 %-------------------------------------------
% 73.14/73.18 cnf(29,plain,
% 73.14/73.18 (E(x291,f6(x291,x291))),
% 73.14/73.18 inference(scs_inference,[],[14,2])).
% 73.14/73.18 cnf(30,plain,
% 73.14/73.18 (~E(f3(a1,a4),f6(a4,a4))),
% 73.14/73.18 inference(scs_inference,[],[28,14,2,3])).
% 73.14/73.18 cnf(32,plain,
% 73.14/73.18 (E(x321,f3(x321,x321))),
% 73.14/73.18 inference(scs_inference,[],[15,2])).
% 73.14/73.18 cnf(35,plain,
% 73.14/73.18 (~E(a1,a4)),
% 73.14/73.18 inference(scs_inference,[],[28,15,2,3,4])).
% 73.14/73.18 cnf(36,plain,
% 73.14/73.18 (E(x361,f8(a5,x361))),
% 73.14/73.18 inference(scs_inference,[],[13,2])).
% 73.14/73.18 cnf(39,plain,
% 73.14/73.18 (E(f8(x391,f6(x392,x393)),f6(f8(x391,x392),f8(x391,x393)))),
% 73.14/73.18 inference(scs_inference,[],[24,2])).
% 73.14/73.18 cnf(40,plain,
% 73.14/73.18 (E(f8(x401,x402),f8(x401,f6(x402,x402)))),
% 73.14/73.18 inference(scs_inference,[],[29,24,2,3])).
% 73.14/73.18 cnf(43,plain,
% 73.14/73.18 (E(f8(x431,f6(x432,x432)),f8(x431,x432))),
% 73.14/73.18 inference(scs_inference,[],[40,2])).
% 73.14/73.18 cnf(44,plain,
% 73.14/73.18 (E(f6(x441,x442),f6(f8(a5,x441),f8(a5,x442)))),
% 73.14/73.18 inference(scs_inference,[],[39,36,40,2,3])).
% 73.14/73.18 cnf(47,plain,
% 73.14/73.18 (E(f6(f8(a5,x471),f8(a5,x472)),f6(x471,x472))),
% 73.14/73.18 inference(scs_inference,[],[44,2])).
% 73.14/73.18 cnf(50,plain,
% 73.14/73.18 (E(f8(x501,f3(x502,x503)),f3(f8(x501,x502),f8(x501,x503)))),
% 73.14/73.18 inference(scs_inference,[],[25,2])).
% 73.14/73.18 cnf(51,plain,
% 73.14/73.18 (~E(f3(a1,a4),f6(f8(a5,a4),f8(a5,a4)))),
% 73.14/73.18 inference(scs_inference,[],[47,30,25,2,3])).
% 73.14/73.18 cnf(53,plain,
% 73.14/73.18 (E(f8(f6(x531,x532),x533),f6(f8(x531,x533),f8(x532,x533)))),
% 73.14/73.18 inference(scs_inference,[],[26,2])).
% 73.14/73.18 cnf(56,plain,
% 73.14/73.18 (E(f8(f3(x561,x562),x563),f3(f8(x561,x563),f8(x562,x563)))),
% 73.14/73.18 inference(scs_inference,[],[27,2])).
% 73.14/73.18 cnf(57,plain,
% 73.14/73.18 (E(f3(x571,x572),f3(f8(a5,x571),f8(a5,x572)))),
% 73.14/73.18 inference(scs_inference,[],[50,36,27,2,3])).
% 73.14/73.18 cnf(60,plain,
% 73.14/73.18 (E(f3(f8(a5,x601),f8(a5,x602)),f3(x601,x602))),
% 73.14/73.18 inference(scs_inference,[],[57,2])).
% 73.14/73.18 cnf(61,plain,
% 73.14/73.18 (~E(f3(a1,a4),f8(f6(a5,a5),a4))),
% 73.14/73.18 inference(scs_inference,[],[53,57,51,2,3])).
% 73.14/73.18 cnf(63,plain,
% 73.14/73.18 (E(x631,f6(x631,f3(x631,x632)))),
% 73.14/73.18 inference(scs_inference,[],[19,2])).
% 73.14/73.18 cnf(64,plain,
% 73.14/73.18 (E(f8(f3(x641,x642),f6(x643,x643)),f3(f8(x641,x643),f8(x642,x643)))),
% 73.14/73.18 inference(scs_inference,[],[56,43,19,2,3])).
% 73.14/73.18 cnf(67,plain,
% 73.14/73.18 (E(f3(f8(x671,x672),f8(x673,x672)),f8(f3(x671,x673),f6(x672,x672)))),
% 73.14/73.18 inference(scs_inference,[],[64,2])).
% 73.14/73.18 cnf(68,plain,
% 73.14/73.18 (E(x681,f6(f3(x681,x681),f3(f3(x681,x681),x682)))),
% 73.14/73.18 inference(scs_inference,[],[32,63,64,2,3])).
% 73.14/73.18 cnf(70,plain,
% 73.14/73.18 (E(f6(f3(x701,x701),f3(f3(x701,x701),x702)),x701)),
% 73.14/73.18 inference(scs_inference,[],[68,2])).
% 73.14/73.18 cnf(73,plain,
% 73.14/73.18 (E(x731,f3(x731,f6(x731,x732)))),
% 73.14/73.18 inference(scs_inference,[],[20,2])).
% 73.14/73.18 cnf(74,plain,
% 73.14/73.18 (~E(f3(a1,a4),f6(f3(a4,a4),f3(f3(a4,a4),x741)))),
% 73.14/73.18 inference(scs_inference,[],[28,70,20,2,3])).
% 73.14/73.19 cnf(76,plain,
% 73.14/73.19 (E(f6(x761,f6(x762,x763)),f6(f6(x761,x762),x763))),
% 73.14/73.19 inference(scs_inference,[],[21,2])).
% 73.14/73.19 cnf(77,plain,
% 73.14/73.19 (E(f8(x771,x772),f8(f3(x771,x771),f6(x772,x772)))),
% 73.14/73.19 inference(scs_inference,[],[67,32,21,2,3])).
% 73.14/73.19 cnf(80,plain,
% 73.14/73.19 (E(f8(f3(x801,x801),f6(x802,x802)),f8(x801,x802))),
% 73.14/73.19 inference(scs_inference,[],[77,2])).
% 73.14/73.19 cnf(81,plain,
% 73.14/73.19 (E(f6(x811,x812),f6(f6(f6(x811,x812),x811),x812))),
% 73.14/73.19 inference(scs_inference,[],[76,29,77,2,3])).
% 73.14/73.19 cnf(85,plain,
% 73.14/73.19 (E(f8(x851,f3(x852,x852)),f8(f3(x851,x851),f6(x852,x852)))),
% 73.14/73.19 inference(scs_inference,[],[67,50,81,2,3])).
% 73.14/73.19 cnf(91,plain,
% 73.14/73.19 (E(f3(x911,f3(x912,x913)),f3(f3(x911,x912),x913))),
% 73.14/73.19 inference(scs_inference,[],[22,2])).
% 73.14/73.19 cnf(92,plain,
% 73.14/73.19 (~E(f3(a1,a4),f8(f3(f6(a5,a5),f6(a5,a5)),f6(a4,a4)))),
% 73.14/73.19 inference(scs_inference,[],[80,61,22,2,3])).
% 73.14/73.19 cnf(94,plain,
% 73.14/73.19 (E(f8(x941,f8(x942,x943)),f8(f8(x941,x942),x943))),
% 73.14/73.19 inference(scs_inference,[],[23,2])).
% 73.14/73.19 cnf(97,plain,
% 73.14/73.19 (E(a2,f3(a1,a2))),
% 73.14/73.19 inference(scs_inference,[],[11,2])).
% 73.14/73.19 cnf(100,plain,
% 73.14/73.19 (E(a4,f3(a2,a4))),
% 73.14/73.19 inference(scs_inference,[],[12,2])).
% 73.14/73.19 cnf(101,plain,
% 73.14/73.19 (E(f6(f3(a2,a2),f3(f3(a2,a2),x1011)),f3(a1,a2))),
% 73.14/73.19 inference(scs_inference,[],[97,70,12,2,3])).
% 73.14/73.19 cnf(104,plain,
% 73.14/73.19 (E(f6(f3(a4,a4),f3(f3(a4,a4),x1041)),f3(a2,a4))),
% 73.14/73.19 inference(scs_inference,[],[100,70,101,2,3])).
% 73.14/73.19 cnf(106,plain,
% 73.14/73.19 (E(f3(a2,a4),f6(f3(a4,a4),f3(f3(a4,a4),x1061)))),
% 73.14/73.19 inference(scs_inference,[],[104,2])).
% 73.14/73.19 cnf(109,plain,
% 73.14/73.19 (E(a5,f8(f7(x1091),x1091))),
% 73.14/73.19 inference(scs_inference,[],[16,2])).
% 73.14/73.19 cnf(112,plain,
% 73.14/73.19 (~E(f3(a1,a4),f3(a2,a4))),
% 73.14/73.19 inference(scs_inference,[],[106,74,3])).
% 73.14/73.19 cnf(115,plain,
% 73.14/73.19 (~E(f3(a1,a4),f3(f8(a5,a2),f8(a5,a4)))),
% 73.14/73.19 inference(scs_inference,[],[60,112,3])).
% 73.14/73.19 cnf(127,plain,
% 73.14/73.19 (~E(f3(a1,a4),f8(a5,f3(a2,a4)))),
% 73.14/73.19 inference(scs_inference,[],[50,115,3])).
% 73.14/73.19 cnf(137,plain,
% 73.14/73.19 (~E(f3(a1,a4),f8(f6(a5,a5),f3(a4,a4)))),
% 73.14/73.19 inference(scs_inference,[],[85,92,3])).
% 73.14/73.19 cnf(139,plain,
% 73.14/73.19 (~E(f3(a1,a4),f8(f6(a5,a5),f6(f3(a4,a4),f3(a4,a4))))),
% 73.14/73.19 inference(scs_inference,[],[43,137,3])).
% 73.14/73.19 cnf(145,plain,
% 73.14/73.19 (~E(f3(a1,a4),f6(a4,f3(a4,x1451)))),
% 73.14/73.19 inference(scs_inference,[],[28,19,3])).
% 73.14/73.19 cnf(149,plain,
% 73.14/73.19 (E(f8(a5,a5),f8(f7(x1491),x1491))),
% 73.14/73.19 inference(scs_inference,[],[13,109,3])).
% 73.14/73.19 cnf(151,plain,
% 73.14/73.19 (E(f8(f7(x1511),x1511),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[13,109,3,2])).
% 73.14/73.19 cnf(152,plain,
% 73.14/73.19 (E(f8(a5,f8(f7(x1521),x1521)),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[13,151,3])).
% 73.14/73.19 cnf(154,plain,
% 73.14/73.19 (E(f8(a5,a5),f8(a5,f8(f7(x1541),x1541)))),
% 73.14/73.19 inference(scs_inference,[],[13,151,3,2])).
% 73.14/73.19 cnf(157,plain,
% 73.14/73.19 (E(f8(f7(x1571),x1571),f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[13,149,3,2])).
% 73.14/73.19 cnf(158,plain,
% 73.14/73.19 (E(f8(a5,f8(f7(x1581),x1581)),a5)),
% 73.14/73.19 inference(scs_inference,[],[13,16,3])).
% 73.14/73.19 cnf(160,plain,
% 73.14/73.19 (E(a5,f8(a5,f8(f7(x1601),x1601)))),
% 73.14/73.19 inference(scs_inference,[],[13,16,3,2])).
% 73.14/73.19 cnf(163,plain,
% 73.14/73.19 (E(f8(a5,f8(f7(x1631),x1631)),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[14,160,3,2])).
% 73.14/73.19 cnf(164,plain,
% 73.14/73.19 (E(f6(a5,a5),f8(f7(x1641),x1641))),
% 73.14/73.19 inference(scs_inference,[],[14,109,3])).
% 73.14/73.19 cnf(166,plain,
% 73.14/73.19 (E(f8(f7(x1661),x1661),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[14,109,3,2])).
% 73.14/73.19 cnf(169,plain,
% 73.14/73.19 (E(f8(f7(x1691),x1691),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[14,164,3,2])).
% 73.14/73.19 cnf(170,plain,
% 73.14/73.19 (E(f6(f8(a5,a5),f8(a5,a5)),f8(f7(x1701),x1701))),
% 73.14/73.19 inference(scs_inference,[],[14,149,3])).
% 73.14/73.19 cnf(172,plain,
% 73.14/73.19 (E(f8(f7(x1721),x1721),f6(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[14,149,3,2])).
% 73.14/73.19 cnf(175,plain,
% 73.14/73.19 (E(f8(a5,f8(f7(x1751),x1751)),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[15,160,3,2])).
% 73.14/73.19 cnf(176,plain,
% 73.14/73.19 (E(f3(a5,a5),f8(f7(x1761),x1761))),
% 73.14/73.19 inference(scs_inference,[],[15,109,3])).
% 73.14/73.19 cnf(178,plain,
% 73.14/73.19 (E(f8(f7(x1781),x1781),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[15,109,3,2])).
% 73.14/73.19 cnf(181,plain,
% 73.14/73.19 (E(f8(f7(x1811),x1811),f3(f3(a5,a5),f3(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[15,176,3,2])).
% 73.14/73.19 cnf(184,plain,
% 73.14/73.19 (E(f8(f7(x1841),x1841),f3(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[15,164,3,2])).
% 73.14/73.19 cnf(187,plain,
% 73.14/73.19 (E(f8(f7(x1871),x1871),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[15,149,3,2])).
% 73.14/73.19 cnf(188,plain,
% 73.14/73.19 (E(f8(f7(x1881),x1881),f8(f8(a5,a5),a5))),
% 73.14/73.19 inference(scs_inference,[],[94,157,3])).
% 73.14/73.19 cnf(190,plain,
% 73.14/73.19 (E(f8(f8(a5,a5),a5),f8(f7(x1901),x1901))),
% 73.14/73.19 inference(scs_inference,[],[94,157,3,2])).
% 73.14/73.19 cnf(193,plain,
% 73.14/73.19 (E(a5,f8(f8(a5,a5),a5))),
% 73.14/73.19 inference(scs_inference,[],[16,190,3,2])).
% 73.14/73.19 cnf(196,plain,
% 73.14/73.19 (E(f6(a5,a5),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[163,154,3,2])).
% 73.14/73.19 cnf(197,plain,
% 73.14/73.19 (E(f8(a5,a5),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[175,154,3])).
% 73.14/73.19 cnf(202,plain,
% 73.14/73.19 (E(f3(a5,a5),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[196,197,3,2])).
% 73.14/73.19 cnf(203,plain,
% 73.14/73.19 (E(a5,f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[193,23,3])).
% 73.14/73.19 cnf(205,plain,
% 73.14/73.19 (E(f8(a5,f8(a5,a5)),a5)),
% 73.14/73.19 inference(scs_inference,[],[193,23,3,2])).
% 73.14/73.19 cnf(206,plain,
% 73.14/73.19 (E(f3(x2061,f3(x2062,x2063)),f3(x2062,f3(x2063,x2061)))),
% 73.14/73.19 inference(scs_inference,[],[18,22,3])).
% 73.14/73.19 cnf(221,plain,
% 73.14/73.19 (E(f8(f8(a5,a5),a5),f6(a5,f3(a5,x2211)))),
% 73.14/73.19 inference(scs_inference,[],[19,193,3,2])).
% 73.14/73.19 cnf(224,plain,
% 73.14/73.19 (E(f8(f7(x2241),x2241),f6(a5,f3(a5,x2242)))),
% 73.14/73.19 inference(scs_inference,[],[19,109,3,2])).
% 73.14/73.19 cnf(231,plain,
% 73.14/73.19 (E(f6(a5,f3(a5,x2311)),f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[19,203,3])).
% 73.14/73.19 cnf(233,plain,
% 73.14/73.19 (E(f8(a5,f8(a5,a5)),f6(a5,f3(a5,x2331)))),
% 73.14/73.19 inference(scs_inference,[],[19,203,3,2])).
% 73.14/73.19 cnf(246,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x2461)),f8(f8(a5,a5),a5))),
% 73.14/73.19 inference(scs_inference,[],[20,193,3])).
% 73.14/73.19 cnf(248,plain,
% 73.14/73.19 (E(f8(f8(a5,a5),a5),f3(a5,f6(a5,x2481)))),
% 73.14/73.19 inference(scs_inference,[],[20,193,3,2])).
% 73.14/73.19 cnf(251,plain,
% 73.14/73.19 (E(f8(f7(x2511),x2511),f3(a5,f6(a5,x2512)))),
% 73.14/73.19 inference(scs_inference,[],[20,109,3,2])).
% 73.14/73.19 cnf(260,plain,
% 73.14/73.19 (E(f8(a5,f8(a5,a5)),f3(a5,f6(a5,x2601)))),
% 73.14/73.19 inference(scs_inference,[],[20,203,3,2])).
% 73.14/73.19 cnf(264,plain,
% 73.14/73.19 (E(f8(f8(a5,f7(x2641)),x2641),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[23,163,3])).
% 73.14/73.19 cnf(268,plain,
% 73.14/73.19 (E(f8(f8(a5,f7(x2681)),x2681),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[23,175,264,2,3])).
% 73.14/73.19 cnf(272,plain,
% 73.14/73.19 (E(f8(f8(a5,f7(x2721)),x2721),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[23,268,152,2,3])).
% 73.14/73.19 cnf(276,plain,
% 73.14/73.19 (E(f8(f8(a5,f7(x2761)),x2761),a5)),
% 73.14/73.19 inference(scs_inference,[],[23,272,158,2,3])).
% 73.14/73.19 cnf(303,plain,
% 73.14/73.19 (E(f3(x3031,x3032),f3(x3031,f3(x3032,f3(x3031,x3032))))),
% 73.14/73.19 inference(scs_inference,[],[32,22,3])).
% 73.14/73.19 cnf(307,plain,
% 73.14/73.19 (E(x3071,f3(x3071,f3(x3071,f3(x3071,x3071))))),
% 73.14/73.19 inference(scs_inference,[],[32,303,3])).
% 73.14/73.19 cnf(338,plain,
% 73.14/73.19 (~E(a1,f6(f3(a4,a4),f3(f3(a4,a4),x3381)))),
% 73.14/73.19 inference(scs_inference,[],[35,70,3])).
% 73.14/73.19 cnf(340,plain,
% 73.14/73.19 (~E(a1,f3(a2,a4))),
% 73.14/73.19 inference(scs_inference,[],[106,338,3])).
% 73.14/73.19 cnf(358,plain,
% 73.14/73.19 (E(f8(a5,a5),f6(a5,f3(a5,x3581)))),
% 73.14/73.19 inference(scs_inference,[],[36,233,3])).
% 73.14/73.19 cnf(360,plain,
% 73.14/73.19 (E(f6(a5,f3(a5,x3601)),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[36,233,3,2])).
% 73.14/73.19 cnf(361,plain,
% 73.14/73.19 (E(f8(a5,a5),f3(a5,f6(a5,x3611)))),
% 73.14/73.19 inference(scs_inference,[],[36,260,3])).
% 73.14/73.19 cnf(363,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x3631)),f8(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[36,260,3,2])).
% 73.14/73.19 cnf(372,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f6(a5,f3(a5,x3721)))),
% 73.14/73.19 inference(scs_inference,[],[221,80,3])).
% 73.14/73.19 cnf(374,plain,
% 73.14/73.19 (E(f6(a5,f3(a5,x3741)),f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[221,80,3,2])).
% 73.14/73.19 cnf(377,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f8(f7(x3771),x3771))),
% 73.14/73.19 inference(scs_inference,[],[224,374,3,2])).
% 73.14/73.19 cnf(378,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[178,377,3])).
% 73.14/73.19 cnf(380,plain,
% 73.14/73.19 (E(f3(a5,a5),f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[178,377,3,2])).
% 73.14/73.19 cnf(385,plain,
% 73.14/73.19 (E(f6(a5,f3(a5,x3851)),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[380,372,3,2])).
% 73.14/73.19 cnf(387,plain,
% 73.14/73.19 (E(f6(a5,a5),f6(a5,f3(a5,x3871)))),
% 73.14/73.19 inference(scs_inference,[],[385,202,3,2])).
% 73.14/73.19 cnf(390,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[387,374,3,2])).
% 73.14/73.19 cnf(392,plain,
% 73.14/73.19 (E(f8(a5,a5),f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[390,196,3,2])).
% 73.14/73.19 cnf(393,plain,
% 73.14/73.19 (E(a5,f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[36,392,3])).
% 73.14/73.19 cnf(395,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),a5)),
% 73.14/73.19 inference(scs_inference,[],[36,392,3,2])).
% 73.14/73.19 cnf(397,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[205,393,3,2])).
% 73.14/73.19 cnf(398,plain,
% 73.14/73.19 (E(f3(a5,a5),f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[397,380,3])).
% 73.14/73.19 cnf(399,plain,
% 73.14/73.19 (E(f8(a5,f8(a5,a5)),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[397,380,3,2])).
% 73.14/73.19 cnf(401,plain,
% 73.14/73.19 (E(f6(a5,a5),f8(a5,f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[399,202,3,2])).
% 73.14/73.19 cnf(403,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x4031)),f6(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[401,260,3,2])).
% 73.14/73.19 cnf(409,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x4091)),f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[397,260,3,2])).
% 73.14/73.19 cnf(411,plain,
% 73.14/73.19 (E(f3(a5,a5),f3(a5,f6(a5,x4111)))),
% 73.14/73.19 inference(scs_inference,[],[409,378,3,2])).
% 73.14/73.19 cnf(422,plain,
% 73.14/73.19 (E(f8(f7(x4221),x4221),f8(a5,f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[39,170,3,2])).
% 73.14/73.19 cnf(448,plain,
% 73.14/73.19 (E(f6(a5,f3(a5,x4481)),f3(a5,f6(a5,x4482)))),
% 73.14/73.19 inference(scs_inference,[],[403,387,3,2])).
% 73.14/73.19 cnf(459,plain,
% 73.14/73.19 (E(f8(f7(x4591),f6(x4591,x4591)),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,169,3])).
% 73.14/73.19 cnf(462,plain,
% 73.14/73.19 (E(f6(f6(a5,a5),f6(a5,a5)),f8(f7(x4621),f6(x4621,x4621)))),
% 73.14/73.19 inference(scs_inference,[],[43,169,3,2])).
% 73.14/73.19 cnf(463,plain,
% 73.14/73.19 (E(f8(f7(x4631),f6(x4631,x4631)),f3(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,184,3])).
% 73.14/73.19 cnf(472,plain,
% 73.14/73.19 (E(f3(f8(a5,a5),f8(a5,a5)),f8(f7(x4721),f6(x4721,x4721)))),
% 73.14/73.19 inference(scs_inference,[],[43,187,3,2])).
% 73.14/73.19 cnf(473,plain,
% 73.14/73.19 (E(f8(f7(x4731),f6(x4731,x4731)),f6(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,172,3])).
% 73.14/73.19 cnf(476,plain,
% 73.14/73.19 (E(f6(f8(a5,a5),f8(a5,a5)),f8(f7(x4761),f6(x4761,x4761)))),
% 73.14/73.19 inference(scs_inference,[],[43,172,3,2])).
% 73.14/73.19 cnf(477,plain,
% 73.14/73.19 (E(f8(f6(a5,a5),a5),f8(f7(x4771),f6(x4771,x4771)))),
% 73.14/73.19 inference(scs_inference,[],[476,53,3])).
% 73.14/73.19 cnf(479,plain,
% 73.14/73.19 (E(f8(f7(x4791),f6(x4791,x4791)),f8(f6(a5,a5),a5))),
% 73.14/73.19 inference(scs_inference,[],[476,53,3,2])).
% 73.14/73.19 cnf(480,plain,
% 73.14/73.19 (E(f8(f7(x4801),f6(x4801,x4801)),f3(f3(a5,a5),f3(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,181,3])).
% 73.14/73.19 cnf(483,plain,
% 73.14/73.19 (E(f3(f3(a5,a5),f3(a5,a5)),f8(f7(x4831),f6(x4831,x4831)))),
% 73.14/73.19 inference(scs_inference,[],[43,181,3,2])).
% 73.14/73.19 cnf(487,plain,
% 73.14/73.19 (E(f8(a5,f6(a5,a5)),f8(f7(x4871),f6(x4871,x4871)))),
% 73.14/73.19 inference(scs_inference,[],[43,422,3,2])).
% 73.14/73.19 cnf(491,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x4911)),f8(f7(x4912),f6(x4912,x4912)))),
% 73.14/73.19 inference(scs_inference,[],[43,251,3,2])).
% 73.14/73.19 cnf(495,plain,
% 73.14/73.19 (E(f8(f7(x4951),f6(x4951,x4951)),a5)),
% 73.14/73.19 inference(scs_inference,[],[73,491,3,2])).
% 73.14/73.19 cnf(498,plain,
% 73.14/73.19 (E(f3(a5,f6(a5,x4981)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,248,3,2])).
% 73.14/73.19 cnf(501,plain,
% 73.14/73.19 (E(f8(f8(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 73.14/73.19 inference(scs_inference,[],[411,498,3,2])).
% 73.14/73.19 cnf(516,plain,
% 73.14/73.19 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f8(a5,f6(a5,a5)))),
% 73.14/73.19 inference(scs_inference,[],[43,392,3,2])).
% 73.14/73.19 cnf(520,plain,
% 73.14/73.19 (E(f6(a5,a5),f8(f7(x5201),f6(x5201,x5201)))),
% 73.14/73.19 inference(scs_inference,[],[43,166,3,2])).
% 73.14/73.19 cnf(524,plain,
% 73.14/73.19 (E(f8(a5,f8(a5,a5)),f8(f7(x5241),f6(x5241,x5241)))),
% 73.14/73.19 inference(scs_inference,[],[43,157,3,2])).
% 73.14/73.20 cnf(527,plain,
% 73.14/73.20 (E(f8(f7(x5271),x5271),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[43,190,3,2])).
% 73.14/73.20 cnf(531,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f8(f7(x5311),f6(x5311,x5311)))),
% 73.14/73.20 inference(scs_inference,[],[43,527,3,2])).
% 73.14/73.20 cnf(534,plain,
% 73.14/73.20 (E(f8(f7(x5341),f6(x5341,x5341)),f6(a5,f3(a5,x5342)))),
% 73.14/73.20 inference(scs_inference,[],[448,491,3,2])).
% 73.14/73.20 cnf(537,plain,
% 73.14/73.20 (E(f8(a5,a5),f8(f7(x5371),f6(x5371,x5371)))),
% 73.14/73.20 inference(scs_inference,[],[534,360,3,2])).
% 73.14/73.20 cnf(540,plain,
% 73.14/73.20 (E(f3(a5,a5),f8(f7(x5401),f6(x5401,x5401)))),
% 73.14/73.20 inference(scs_inference,[],[385,534,3,2])).
% 73.14/73.20 cnf(544,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[73,498,3,2])).
% 73.14/73.20 cnf(552,plain,
% 73.14/73.20 (E(f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[501,380,3,2])).
% 73.14/73.20 cnf(577,plain,
% 73.14/73.20 (E(f8(f7(x5771),f6(x5771,x5771)),f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[43,477,3,2])).
% 73.14/73.20 cnf(581,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f8(f7(x5811),f6(x5811,x5811)))),
% 73.14/73.20 inference(scs_inference,[],[43,188,3,2])).
% 73.14/73.20 cnf(582,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x5821)),f6(x5821,x5821)),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,264,3])).
% 73.14/73.20 cnf(585,plain,
% 73.14/73.20 (E(f6(a5,a5),f8(f8(a5,f7(x5851)),f6(x5851,x5851)))),
% 73.14/73.20 inference(scs_inference,[],[582,2])).
% 73.14/73.20 cnf(586,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x5861)),f6(x5861,x5861)),f3(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,582,268,2,3])).
% 73.14/73.20 cnf(589,plain,
% 73.14/73.20 (E(f3(a5,a5),f8(f8(a5,f7(x5891)),f6(x5891,x5891)))),
% 73.14/73.20 inference(scs_inference,[],[586,2])).
% 73.14/73.20 cnf(590,plain,
% 73.14/73.20 (E(f3(a5,f6(a5,x5901)),f8(f8(a5,f7(x5902)),f6(x5902,x5902)))),
% 73.14/73.20 inference(scs_inference,[],[585,403,586,2,3])).
% 73.14/73.20 cnf(591,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x5911)),f6(x5911,x5911)),f3(a5,f6(a5,x5912)))),
% 73.14/73.20 inference(scs_inference,[],[590,2])).
% 73.14/73.20 cnf(592,plain,
% 73.14/73.20 (E(f8(f7(x5921),x5921),f8(f8(a5,f7(x5922)),f6(x5922,x5922)))),
% 73.14/73.20 inference(scs_inference,[],[251,590,2,3])).
% 73.14/73.20 cnf(595,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x5951)),f6(x5951,x5951)),f8(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[591,363,592,2,3])).
% 73.14/73.20 cnf(597,plain,
% 73.14/73.20 (E(f8(a5,a5),f8(f8(a5,f7(x5971)),f6(x5971,x5971)))),
% 73.14/73.20 inference(scs_inference,[],[595,2])).
% 73.14/73.20 cnf(598,plain,
% 73.14/73.20 (E(f3(a5,a5),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[411,595,246,2,3])).
% 73.14/73.20 cnf(600,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f3(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[598,2])).
% 73.14/73.20 cnf(601,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f8(f8(a5,f7(x6011)),f6(x6011,x6011)))),
% 73.14/73.20 inference(scs_inference,[],[43,597,598,2,3])).
% 73.14/73.20 cnf(603,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6031)),f6(x6031,x6031)),f8(a5,f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[601,2])).
% 73.14/73.20 cnf(604,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f8(f8(a5,f7(x6041)),f6(x6041,x6041)))),
% 73.14/73.20 inference(scs_inference,[],[600,589,601,2,3])).
% 73.14/73.20 cnf(605,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6051)),f6(x6051,x6051)),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[604,2])).
% 73.14/73.20 cnf(606,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[248,403,604,2,3])).
% 73.14/73.20 cnf(608,plain,
% 73.14/73.20 (E(f6(a5,a5),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[606,2])).
% 73.14/73.20 cnf(609,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6091)),f6(x6091,x6091)),f8(f7(x6092),f6(x6092,x6092)))),
% 73.14/73.20 inference(scs_inference,[],[591,491,606,2,3])).
% 73.14/73.20 cnf(611,plain,
% 73.14/73.20 (E(f8(f7(x6111),f6(x6111,x6111)),f8(f8(a5,f7(x6112)),f6(x6112,x6112)))),
% 73.14/73.20 inference(scs_inference,[],[609,2])).
% 73.14/73.20 cnf(612,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,609,606,2,3])).
% 73.14/73.20 cnf(614,plain,
% 73.14/73.20 (E(f6(a5,a5),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[612,2])).
% 73.14/73.20 cnf(615,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(f6(a5,a5),f6(a5,a5))),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,612,2,3])).
% 73.14/73.20 cnf(618,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f8(f8(a5,f7(x6181)),f6(x6181,x6181)))),
% 73.14/73.20 inference(scs_inference,[],[43,615,604,2,3])).
% 73.14/73.20 cnf(620,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6201)),f6(x6201,x6201)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[618,2])).
% 73.14/73.20 cnf(621,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f6(a5,f3(a5,x6211)))),
% 73.14/73.20 inference(scs_inference,[],[43,618,358,2,3])).
% 73.14/73.20 cnf(624,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f3(a5,f6(a5,x6241)))),
% 73.14/73.20 inference(scs_inference,[],[43,621,361,2,3])).
% 73.14/73.20 cnf(627,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6271)),f6(x6271,x6271)),a5)),
% 73.14/73.20 inference(scs_inference,[],[43,624,276,2,3])).
% 73.14/73.20 cnf(630,plain,
% 73.14/73.20 (E(a5,f8(f8(a5,f7(x6301)),f6(x6301,x6301)))),
% 73.14/73.20 inference(scs_inference,[],[627,2])).
% 73.14/73.20 cnf(631,plain,
% 73.14/73.20 (E(f6(a5,f3(a5,x6311)),f8(f8(a5,f7(x6312)),f6(x6312,x6312)))),
% 73.14/73.20 inference(scs_inference,[],[448,627,590,2,3])).
% 73.14/73.20 cnf(633,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6331)),f6(x6331,x6331)),f6(a5,f3(a5,x6332)))),
% 73.14/73.20 inference(scs_inference,[],[631,2])).
% 73.14/73.20 cnf(634,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f3(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,631,197,2,3])).
% 73.14/73.20 cnf(636,plain,
% 73.14/73.20 (E(f3(a5,a5),f8(a5,f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[634,2])).
% 73.14/73.20 cnf(637,plain,
% 73.14/73.20 (E(f8(a5,f6(f6(a5,a5),f6(a5,a5))),f3(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[43,634,2,3])).
% 73.14/73.20 cnf(640,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f8(a5,f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[636,600,637,2,3])).
% 73.14/73.20 cnf(641,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[640,2])).
% 73.14/73.20 cnf(642,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6421)),f6(x6421,x6421)),f8(a5,f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[633,640,231,2,3])).
% 73.14/73.20 cnf(644,plain,
% 73.14/73.20 (E(f8(a5,f8(a5,a5)),f8(f8(a5,f7(x6441)),f6(x6441,x6441)))),
% 73.14/73.20 inference(scs_inference,[],[642,2])).
% 73.14/73.20 cnf(647,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[520,577,3,2])).
% 73.14/73.20 cnf(648,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[647,614,3])).
% 73.14/73.20 cnf(649,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[647,614,3,2])).
% 73.14/73.20 cnf(651,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f8(f3(f8(a5,a5),f8(a5,a5)),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[552,649,3,2])).
% 73.14/73.20 cnf(653,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[516,651,3,2])).
% 73.14/73.20 cnf(655,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f8(f8(a5,f7(x6551)),f6(x6551,x6551)))),
% 73.14/73.20 inference(scs_inference,[],[653,603,3,2])).
% 73.14/73.20 cnf(657,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[608,647,3,2])).
% 73.14/73.20 cnf(660,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),a5),f8(a5,f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[524,479,3,2])).
% 73.14/73.20 cnf(662,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6621)),f6(x6621,x6621)),f8(f6(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[660,644,3,2])).
% 73.14/73.20 cnf(663,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[395,651,3])).
% 73.14/73.20 cnf(664,plain,
% 73.14/73.20 (E(a5,f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[395,651,3,2])).
% 73.14/73.20 cnf(669,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),a5),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[531,479,3,2])).
% 73.14/73.20 cnf(672,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f8(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[537,577,3,2])).
% 73.14/73.20 cnf(674,plain,
% 73.14/73.20 (E(a5,f8(f6(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[669,544,3,2])).
% 73.14/73.20 cnf(677,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[540,577,3,2])).
% 73.14/73.20 cnf(685,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x6851)),f6(x6851,x6851)),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[472,611,3,2])).
% 73.14/73.20 cnf(686,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[655,685,3])).
% 73.14/73.20 cnf(699,plain,
% 73.14/73.20 (E(f8(a5,f6(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[630,603,3,2])).
% 73.14/73.20 cnf(702,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),a5),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[662,585,3,2])).
% 73.14/73.20 cnf(704,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f8(f6(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[702,608,3,2])).
% 73.14/73.20 cnf(708,plain,
% 73.14/73.20 (E(f8(a5,f8(a5,a5)),f8(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[677,398,3,2])).
% 73.14/73.20 cnf(713,plain,
% 73.14/73.20 (E(f3(f6(a5,a5),f6(a5,a5)),f8(a5,f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[487,463,3,2])).
% 73.14/73.20 cnf(715,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f3(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[713,641,3,2])).
% 73.14/73.20 cnf(717,plain,
% 73.14/73.20 (E(f3(f6(a5,a5),f6(a5,a5)),f8(f8(a5,f7(x7171)),f6(x7171,x7171)))),
% 73.14/73.20 inference(scs_inference,[],[715,605,3,2])).
% 73.14/73.20 cnf(719,plain,
% 73.14/73.20 (E(a5,f3(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[699,713,3,2])).
% 73.14/73.20 cnf(722,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f3(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[620,717,3,2])).
% 73.14/73.20 cnf(726,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f8(a5,f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[708,648,3,2])).
% 73.14/73.20 cnf(728,plain,
% 73.14/73.20 (E(f3(f8(a5,a5),f8(a5,a5)),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[657,686,3,2])).
% 73.14/73.20 cnf(730,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),a5),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[728,704,3,2])).
% 73.14/73.20 cnf(732,plain,
% 73.14/73.20 (E(f3(f8(a5,a5),f8(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[674,730,3,2])).
% 73.14/73.20 cnf(734,plain,
% 73.14/73.20 (E(f3(f6(a5,a5),f6(a5,a5)),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[719,732,3,2])).
% 73.14/73.20 cnf(736,plain,
% 73.14/73.20 (E(f3(f8(a5,a5),f8(a5,a5)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[734,722,3,2])).
% 73.14/73.20 cnf(738,plain,
% 73.14/73.20 (E(f8(a5,f8(a5,a5)),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[726,736,3,2])).
% 73.14/73.20 cnf(751,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),a5),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[581,459,3])).
% 73.14/73.20 cnf(753,plain,
% 73.14/73.20 (E(f6(f6(a5,a5),f6(a5,a5)),f8(f8(a5,a5),a5))),
% 73.14/73.20 inference(scs_inference,[],[581,459,3,2])).
% 73.14/73.20 cnf(755,plain,
% 73.14/73.20 (E(f8(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[753,657,3,2])).
% 73.14/73.20 cnf(756,plain,
% 73.14/73.20 (E(a5,f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[755,664,3])).
% 73.14/73.20 cnf(757,plain,
% 73.14/73.20 (E(f6(f6(a5,a5),f6(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[755,664,3,2])).
% 73.14/73.20 cnf(758,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f8(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[672,649,3])).
% 73.14/73.20 cnf(759,plain,
% 73.14/73.20 (E(f8(a5,a5),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[672,649,3,2])).
% 73.14/73.20 cnf(769,plain,
% 73.14/73.20 (E(f8(f8(a5,f7(x7691)),f6(x7691,x7691)),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[462,611,3,2])).
% 73.14/73.20 cnf(777,plain,
% 73.14/73.20 (E(f6(f6(a5,a5),f6(a5,a5)),f8(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[597,769,3,2])).
% 73.14/73.20 cnf(779,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f6(f6(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[777,759,3,2])).
% 73.14/73.20 cnf(782,plain,
% 73.14/73.20 (E(a5,f3(f3(a5,a5),f3(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[483,495,3,2])).
% 73.14/73.20 cnf(792,plain,
% 73.14/73.20 (E(f6(f6(a5,a5),f6(a5,a5)),f3(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[728,751,3,2])).
% 73.14/73.20 cnf(799,plain,
% 73.14/73.20 (E(f3(f3(a5,a5),f3(a5,a5)),f6(a5,a5))),
% 73.14/73.20 inference(scs_inference,[],[520,480,3,2])).
% 73.14/73.20 cnf(801,plain,
% 73.14/73.20 (E(f8(f8(a5,a5),f6(a5,a5)),f3(f3(a5,a5),f3(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[799,614,3,2])).
% 73.14/73.20 cnf(816,plain,
% 73.14/73.20 (E(f6(f8(a5,a5),f8(a5,a5)),f8(a5,f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[524,473,3,2])).
% 73.14/73.20 cnf(818,plain,
% 73.14/73.20 (E(f3(f8(a5,a5),f8(a5,a5)),f6(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[816,738,3,2])).
% 73.14/73.20 cnf(819,plain,
% 73.14/73.20 (E(f6(f6(a5,a5),f6(a5,a5)),f6(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[818,792,3])).
% 73.14/73.20 cnf(833,plain,
% 73.14/73.20 (E(f6(f8(a5,a5),f8(a5,a5)),f8(f8(a5,a5),f6(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[779,819,3,2])).
% 73.14/73.20 cnf(835,plain,
% 73.14/73.20 (E(f3(f3(a5,a5),f3(a5,a5)),f6(f8(a5,a5),f8(a5,a5)))),
% 73.14/73.20 inference(scs_inference,[],[833,801,3,2])).
% 73.14/73.20 cnf(846,plain,
% 73.14/73.20 (E(f6(f8(a5,a5),f8(a5,a5)),a5)),
% 73.14/73.20 inference(scs_inference,[],[782,835,3,2])).
% 73.14/73.20 cnf(1207,plain,
% 73.14/73.20 (~E(a4,f3(a1,a4))),
% 73.14/73.20 inference(scs_inference,[],[28,758,10,5,6,7,8,9,4,2])).
% 73.14/73.20 cnf(1208,plain,
% 73.14/73.20 (~E(f3(a1,f3(a1,f3(a1,a1))),f3(a2,a4))),
% 73.14/73.20 inference(scs_inference,[],[28,340,758,307,10,5,6,7,8,9,4,2,3])).
% 73.14/73.20 cnf(1238,plain,
% 73.14/73.20 (~E(f3(a1,f3(f3(a1,a1),a1)),f3(a2,a4))),
% 73.14/73.20 inference(scs_inference,[],[663,127,206,1208,8,5,6,7,10,9,4,2,3])).
% 73.14/73.20 cnf(1287,plain,
% 73.14/73.20 (~E(f3(a2,a4),f3(a1,a4))),
% 73.14/73.20 inference(scs_inference,[],[1207,756,145,100,5,8,7,10,6,4,9,2,3])).
% 73.14/73.20 cnf(1362,plain,
% 73.14/73.20 (E(f3(a2,x13621),f3(f3(a1,a2),x13621))),
% 73.14/73.20 inference(scs_inference,[],[97,5,8,10,6,7,4])).
% 73.14/73.20 cnf(1386,plain,
% 73.14/73.20 (~E(f3(f3(a1,a2),a4),f3(a1,a4))),
% 73.14/73.20 inference(scs_inference,[],[1287,1362,1238,757,5,8,6,7,10,4,9,2,3])).
% 73.14/73.20 cnf(1395,plain,
% 73.14/73.20 (~E(f3(a1,a4),f3(f3(a1,a2),a4))),
% 73.14/73.20 inference(scs_inference,[],[1386,846,5,8,7,6,10,4,9,2])).
% 73.14/73.20 cnf(1430,plain,
% 73.14/73.20 (E(f3(x14301,a4),f3(x14301,f3(a2,a4)))),
% 73.14/73.20 inference(scs_inference,[],[100,5])).
% 73.14/73.20 cnf(1594,plain,
% 73.14/73.20 ($false),
% 73.14/73.20 inference(scs_inference,[],[1395,139,1430,91,193,8,5,7,10,6,4,9,2,3]),
% 73.14/73.20 ['proof']).
% 73.14/73.20 % SZS output end Proof
% 73.14/73.20 % Total time :72.540000s
%------------------------------------------------------------------------------