%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ROB016-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 14:10:25 EDT 2024
% Result : Unsatisfiable 76.80s 76.89s
% Output : CNFRefutation 76.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ROB016-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n021.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 18:37:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.59 start to proof:theBenchmark
% 76.80/76.87 %-------------------------------------------
% 76.80/76.87 % File :CSE---1.7
% 76.80/76.87 % Problem :theBenchmark
% 76.80/76.87 % Transform :cnf
% 76.80/76.87 % Format :tptp:raw
% 76.80/76.87 % Command :java -jar mcs_scs.jar %d %s
% 76.80/76.87
% 76.80/76.87 % Result :Theorem 76.250000s
% 76.80/76.87 % Output :CNFRefutation 76.250000s
% 76.80/76.87 %-------------------------------------------
% 76.80/76.88 %--------------------------------------------------------------------------
% 76.80/76.88 % File : ROB016-1 : TPTP v8.2.0. Released v1.0.0.
% 76.80/76.88 % Domain : Robbins Algebra
% 76.80/76.88 % Problem : If -(d + e) = -e then -(e + k(d + -(d + -e))) = -e, for k>0
% 76.80/76.88 % Version : [Win90] (equality) axioms.
% 76.80/76.88 % English :
% 76.80/76.88
% 76.80/76.88 % Refs : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% 76.80/76.88 % Source : [Win90]
% 76.80/76.88 % Names : Corollary 3.7 [Win90]
% 76.80/76.88
% 76.80/76.88 % Status : Unsatisfiable
% 76.80/76.88 % Rating : 0.00 v7.0.0, 0.14 v6.3.0, 0.17 v6.2.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.50 v5.4.0, 0.47 v5.3.0, 0.67 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.11 v4.0.1, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 76.80/76.88 % Syntax : Number of clauses : 11 ( 8 unt; 0 nHn; 6 RR)
% 76.80/76.88 % Number of literals : 15 ( 9 equ; 5 neg)
% 76.80/76.88 % Maximal clause size : 3 ( 1 avg)
% 76.80/76.88 % Maximal term depth : 8 ( 2 avg)
% 76.80/76.88 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty)
% 76.80/76.88 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 76.80/76.88 % Number of variables : 14 ( 0 sgn)
% 76.80/76.88 % SPC : CNF_UNS_RFO_SEQ_HRN
% 76.80/76.88
% 76.80/76.88 % Comments : The extra lemma is required for the proof.
% 76.80/76.88 %--------------------------------------------------------------------------
% 76.80/76.88 %----Include axioms for Robbins algebra
% 76.80/76.88 include('Axioms/ROB001-0.ax').
% 76.80/76.88 %----Include axioms for Robbins algebra numbers
% 76.80/76.88 include('Axioms/ROB001-1.ax').
% 76.80/76.88 %--------------------------------------------------------------------------
% 76.80/76.88 cnf(condition,hypothesis,
% 76.80/76.88 negate(add(d,e)) = negate(e) ).
% 76.80/76.88
% 76.80/76.88 cnf(k_positive,axiom,
% 76.80/76.88 positive_integer(k) ).
% 76.80/76.88
% 76.80/76.88 %----Lemma 3.6 required
% 76.80/76.89 cnf(lemma_3_6,axiom,
% 76.80/76.89 ( negate(add(negate(Y),negate(add(X,negate(Y))))) != X
% 76.80/76.89 | ~ positive_integer(Vk)
% 76.80/76.89 | negate(add(Y,multiply(Vk,add(X,negate(add(X,negate(Y))))))) = negate(Y) ) ).
% 76.80/76.89
% 76.80/76.89 cnf(prove_result,negated_conjecture,
% 76.80/76.89 negate(add(e,multiply(k,add(d,negate(add(d,negate(e))))))) != negate(e) ).
% 76.80/76.89
% 76.80/76.89 %--------------------------------------------------------------------------
% 76.80/76.89 %-------------------------------------------
% 76.80/76.89 % Proof found
% 76.80/76.89 % SZS status Theorem for theBenchmark
% 76.80/76.89 % SZS output start Proof
% 76.80/76.89 %ClaNum:21(EqnAxiom:10)
% 76.80/76.89 %VarNum:36(SingletonVarNum:14)
% 76.80/76.89 %MaxLitNum:3
% 76.80/76.89 %MaxfuncDepth:7
% 76.80/76.89 %SharedTerms:16
% 76.80/76.89 %goalClause: 18
% 76.80/76.89 %singleGoalClaCount:1
% 76.80/76.89 [11]P1(a1)
% 76.80/76.89 [12]P1(a2)
% 76.80/76.89 [14]E(f7(f4(a3,a5)),f7(a5))
% 76.80/76.89 [18]~E(f7(f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5))))))),f7(a5))
% 76.80/76.89 [13]E(f6(a1,x131),x131)
% 76.80/76.89 [15]E(f4(x151,x152),f4(x152,x151))
% 76.80/76.89 [17]E(f7(f4(f7(f4(x171,x172)),f7(f4(x171,f7(x172))))),x171)
% 76.80/76.89 [16]E(f4(f4(x161,x162),x163),f4(x161,f4(x162,x163)))
% 76.80/76.89 [19]~P1(x191)+P1(f8(x191))
% 76.80/76.89 [20]~P1(x201)+E(f4(x201,f6(x202,x201)),f6(f8(x202),x201))
% 76.80/76.89 [21]~P1(x212)+~E(f7(f4(f7(x211),f7(f4(x213,f7(x211))))),x213)+E(f7(f4(x211,f6(x212,f4(x213,f7(f4(x213,f7(x211))))))),f7(x211))
% 76.80/76.89 %EqnAxiom
% 76.80/76.89 [1]E(x11,x11)
% 76.80/76.89 [2]E(x22,x21)+~E(x21,x22)
% 76.80/76.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 76.80/76.89 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 76.80/76.89 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 76.80/76.89 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 76.80/76.89 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 76.80/76.89 [8]~E(x81,x82)+E(f7(x81),f7(x82))
% 76.80/76.89 [9]~E(x91,x92)+E(f8(x91),f8(x92))
% 76.80/76.89 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 76.80/76.89
% 76.80/76.89 %-------------------------------------------
% 76.91/76.91 cnf(22,plain,
% 76.91/76.91 (E(x221,f6(a1,x221))),
% 76.91/76.91 inference(scs_inference,[],[13,2])).
% 76.91/76.91 cnf(23,plain,
% 76.91/76.91 (~E(f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))),a5)),
% 76.91/76.91 inference(scs_inference,[],[18,13,2,8])).
% 76.91/76.91 cnf(24,plain,
% 76.91/76.91 (~E(f7(f4(f7(a5),f7(f4(a3,f7(a5))))),a3)),
% 76.91/76.91 inference(scs_inference,[],[18,13,12,2,8,21])).
% 76.91/76.91 cnf(29,plain,
% 76.91/76.91 (E(f4(x291,f4(x292,x293)),f4(f4(x291,x292),x293))),
% 76.91/76.91 inference(scs_inference,[],[16,2])).
% 76.91/76.91 cnf(30,plain,
% 76.91/76.91 (P1(f6(a1,a1))),
% 76.91/76.91 inference(scs_inference,[],[22,11,16,2,10])).
% 76.91/76.91 cnf(32,plain,
% 76.91/76.91 (E(f7(f4(f7(f4(f4(f4(x321,x322),x323),x324)),f7(f4(f4(f4(x321,x322),x323),f7(x324))))),f4(x321,f4(x322,x323)))),
% 76.91/76.91 inference(scs_inference,[],[22,11,16,17,2,10,3])).
% 76.91/76.91 cnf(35,plain,
% 76.91/76.91 (P1(f6(a1,f6(a1,a1)))),
% 76.91/76.91 inference(scs_inference,[],[32,22,30,2,10])).
% 76.91/76.91 cnf(38,plain,
% 76.91/76.91 (~E(f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))),f4(a3,a5))),
% 76.91/76.91 inference(scs_inference,[],[18,32,22,30,14,2,10,3,8])).
% 76.91/76.91 cnf(39,plain,
% 76.91/76.91 (E(f7(a5),f7(f4(a3,a5)))),
% 76.91/76.91 inference(scs_inference,[],[14,2])).
% 76.91/76.91 cnf(40,plain,
% 76.91/76.91 (P1(f6(a1,f6(a1,f6(a1,a1))))),
% 76.91/76.91 inference(scs_inference,[],[22,35,14,2,10])).
% 76.91/76.91 cnf(42,plain,
% 76.91/76.91 (~E(f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))),f4(a5,a3))),
% 76.91/76.91 inference(scs_inference,[],[22,38,35,15,14,2,10,3])).
% 76.91/76.91 cnf(44,plain,
% 76.91/76.91 (~E(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),a3)),
% 76.91/76.91 inference(scs_inference,[],[22,38,35,15,14,2,10,3,7])).
% 76.91/76.91 cnf(45,plain,
% 76.91/76.91 (E(x451,f7(f4(f7(f4(x451,x452)),f7(f4(x451,f7(x452))))))),
% 76.91/76.91 inference(scs_inference,[],[17,2])).
% 76.91/76.91 cnf(46,plain,
% 76.91/76.91 (P1(f6(a1,f6(a1,f6(a1,f6(a1,a1)))))),
% 76.91/76.91 inference(scs_inference,[],[22,40,17,2,10])).
% 76.91/76.91 cnf(48,plain,
% 76.91/76.91 (P1(f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,a1))))))),
% 76.91/76.91 inference(scs_inference,[],[22,46,10])).
% 76.91/76.91 cnf(50,plain,
% 76.91/76.91 (P1(f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,a1)))))))),
% 76.91/76.91 inference(scs_inference,[],[22,48,10])).
% 76.91/76.91 cnf(74,plain,
% 76.91/76.91 (E(f8(f4(f4(x741,x742),x743)),f8(f4(x741,f4(x742,x743))))),
% 76.91/76.91 inference(scs_inference,[],[29,9,2])).
% 76.91/76.91 cnf(75,plain,
% 76.91/76.91 (E(f8(f4(x751,f4(x752,x753))),f8(f4(f4(x751,x752),x753)))),
% 76.91/76.91 inference(scs_inference,[],[74,2])).
% 76.91/76.91 cnf(76,plain,
% 76.91/76.91 (E(f6(a1,f8(f4(f4(x761,x762),x763))),f8(f4(x761,f4(x762,x763))))),
% 76.91/76.91 inference(scs_inference,[],[13,74,2,3])).
% 76.91/76.91 cnf(78,plain,
% 76.91/76.91 (P1(f7(f4(f7(f4(a1,x781)),f7(f4(a1,f7(x781))))))),
% 76.91/76.91 inference(scs_inference,[],[11,45,13,74,2,3,10])).
% 76.91/76.91 cnf(81,plain,
% 76.91/76.91 (E(f8(f4(x811,f4(x812,x813))),f6(a1,f8(f4(f4(x811,x812),x813))))),
% 76.91/76.91 inference(scs_inference,[],[76,2])).
% 76.91/76.91 cnf(82,plain,
% 76.91/76.91 (E(f8(f4(x821,f4(x822,f4(x823,x824)))),f6(a1,f8(f4(f4(f4(x821,x822),x823),x824))))),
% 76.91/76.91 inference(scs_inference,[],[75,76,2,3])).
% 76.91/76.91 cnf(95,plain,
% 76.91/76.91 (E(f6(a1,f8(f4(f4(f4(x951,x952),x953),x954))),f8(f4(x951,f4(x952,f4(x953,x954)))))),
% 76.91/76.91 inference(scs_inference,[],[82,2])).
% 76.91/76.91 cnf(96,plain,
% 76.91/76.91 (E(f8(f4(f4(f4(x961,x962),x963),x964)),f8(f4(x961,f4(x962,f4(x963,x964)))))),
% 76.91/76.91 inference(scs_inference,[],[22,82,2,3])).
% 76.91/76.91 cnf(115,plain,
% 76.91/76.91 (E(f6(f4(f4(x1151,x1152),x1153),x1154),f6(f4(x1151,f4(x1152,x1153)),x1154))),
% 76.91/76.91 inference(scs_inference,[],[29,4,2])).
% 76.91/76.91 cnf(116,plain,
% 76.91/76.91 (E(f8(f4(x1161,f4(x1162,f4(x1163,x1164)))),f8(f4(f4(f4(x1161,x1162),x1163),x1164)))),
% 76.91/76.91 inference(scs_inference,[],[96,2])).
% 76.91/76.91 cnf(117,plain,
% 76.91/76.91 (E(f8(f4(f4(f4(x1171,x1172),x1173),x1174)),f6(a1,f8(f4(f4(x1171,x1172),f4(x1173,x1174)))))),
% 76.91/76.91 inference(scs_inference,[],[96,81,2,3])).
% 76.91/76.91 cnf(135,plain,
% 76.91/76.91 (E(f6(x1351,f4(f7(a5),x1352)),f6(x1351,f4(f7(f4(a3,a5)),x1352)))),
% 76.91/76.91 inference(scs_inference,[],[39,5,6])).
% 76.91/76.91 cnf(137,plain,
% 76.91/76.91 (E(f8(f4(x1371,f4(x1372,f4(x1373,f4(x1374,x1375))))),f8(f4(f4(f4(f4(x1371,x1372),x1373),x1374),x1375)))),
% 76.91/76.91 inference(scs_inference,[],[116,117,75,2,3])).
% 76.91/76.91 cnf(158,plain,
% 76.91/76.91 (E(f4(f8(a1),f6(x1581,f8(a1))),f6(f8(x1581),f8(a1)))),
% 76.91/76.91 inference(scs_inference,[],[11,20,19])).
% 76.91/76.91 cnf(159,plain,
% 76.91/76.91 (E(f8(f4(f4(f4(f4(x1591,x1592),x1593),x1594),x1595)),f8(f4(x1591,f4(x1592,f4(x1593,f4(x1594,x1595))))))),
% 76.91/76.91 inference(scs_inference,[],[137,2])).
% 76.91/76.91 cnf(160,plain,
% 76.91/76.91 (E(f6(a1,f6(f4(f4(x1601,x1602),x1603),x1604)),f6(f4(x1601,f4(x1602,x1603)),x1604))),
% 76.91/76.91 inference(scs_inference,[],[137,13,115,2,3])).
% 76.91/76.91 cnf(183,plain,
% 76.91/76.91 (E(f6(f4(x1831,f4(x1832,x1833)),x1834),f6(a1,f6(f4(f4(x1831,x1832),x1833),x1834)))),
% 76.91/76.91 inference(scs_inference,[],[160,2])).
% 76.91/76.91 cnf(184,plain,
% 76.91/76.91 (E(f8(f4(f4(f4(f4(x1841,x1842),x1843),x1844),x1845)),f6(a1,f8(f4(f4(x1841,x1842),f4(x1843,f4(x1844,x1845))))))),
% 76.91/76.91 inference(scs_inference,[],[159,160,81,2,3])).
% 76.91/76.91 cnf(217,plain,
% 76.91/76.91 (E(f6(a1,f8(f4(f4(f4(x2171,x2172),x2173),x2174))),f6(a1,f8(f4(f4(x2171,x2172),f4(x2173,x2174)))))),
% 76.91/76.91 inference(scs_inference,[],[95,184,81,2,3])).
% 76.91/76.91 cnf(249,plain,
% 76.91/76.91 (E(f4(f7(a5),x2491),f6(a1,f4(f7(f4(a3,a5)),x2491)))),
% 76.91/76.91 inference(scs_inference,[],[22,217,135,2,3])).
% 76.91/76.91 cnf(262,plain,
% 76.91/76.91 (E(f6(a1,f4(f7(f4(a3,a5)),x2621)),f4(f7(a5),x2621))),
% 76.91/76.91 inference(scs_inference,[],[249,2])).
% 76.91/76.91 cnf(263,plain,
% 76.91/76.91 (E(f4(f6(x2631,f8(a1)),f8(a1)),f6(f8(x2631),f8(a1)))),
% 76.91/76.91 inference(scs_inference,[],[249,15,158,2,3])).
% 76.91/76.91 cnf(268,plain,
% 76.91/76.91 (E(f4(f7(f4(a3,a5)),x2681),f4(f7(a5),x2681))),
% 76.91/76.91 inference(scs_inference,[],[22,263,262,2,3])).
% 76.91/76.91 cnf(278,plain,
% 76.91/76.91 (E(f6(a1,f6(f4(f4(f4(x2781,x2782),x2783),x2784),x2785)),f6(f4(x2781,f4(x2782,f4(x2783,x2784))),x2785))),
% 76.91/76.91 inference(scs_inference,[],[268,160,115,2,3])).
% 76.91/76.91 cnf(289,plain,
% 76.91/76.91 (E(f6(f4(f4(f4(x2891,x2892),x2893),x2894),x2895),f6(f4(x2891,f4(x2892,f4(x2893,x2894))),x2895))),
% 76.91/76.91 inference(scs_inference,[],[22,278,2,3])).
% 76.91/76.91 cnf(303,plain,
% 76.91/76.91 (E(f6(f4(x3031,f4(x3032,f4(x3033,x3034))),x3035),f6(f4(f4(f4(x3031,x3032),x3033),x3034),x3035))),
% 76.91/76.91 inference(scs_inference,[],[289,2])).
% 76.91/76.91 cnf(304,plain,
% 76.91/76.91 (E(f6(f4(f4(f4(x3041,x3042),x3043),x3044),x3045),f6(a1,f6(f4(f4(x3041,x3042),f4(x3043,x3044)),x3045)))),
% 76.91/76.91 inference(scs_inference,[],[289,183,2,3])).
% 76.91/76.91 cnf(308,plain,
% 76.91/76.91 (E(f6(a1,f6(f4(f4(x3081,x3082),f4(x3083,x3084)),x3085)),f6(f4(f4(f4(x3081,x3082),x3083),x3084),x3085))),
% 76.91/76.91 inference(scs_inference,[],[304,2])).
% 76.91/76.91 cnf(309,plain,
% 76.91/76.91 (E(f6(f4(x3091,f4(x3092,f4(x3093,x3094))),x3095),f6(f4(f4(x3091,x3092),f4(x3093,x3094)),x3095))),
% 76.91/76.91 inference(scs_inference,[],[303,304,115,2,3])).
% 76.91/76.91 cnf(313,plain,
% 76.91/76.91 (E(f6(x3131,f4(f7(f4(a3,a5)),x3132)),f6(x3131,f4(f7(a5),x3132)))),
% 76.91/76.91 inference(scs_inference,[],[135,2])).
% 76.91/76.91 cnf(314,plain,
% 76.91/76.91 (E(f6(a1,f6(f4(f4(x3141,x3142),f4(x3143,f4(x3144,f4(x3145,x3146)))),x3147)),f6(f4(f4(f4(f4(x3141,x3142),x3143),x3144),f4(x3145,x3146)),x3147))),
% 76.91/76.91 inference(scs_inference,[],[309,308,135,2,3])).
% 76.91/76.91 cnf(322,plain,
% 76.91/76.91 (E(f4(f7(f4(a3,a5)),x3221),f6(a1,f4(f7(a5),x3221)))),
% 76.91/76.91 inference(scs_inference,[],[22,313,314,2,3])).
% 76.91/76.91 cnf(332,plain,
% 76.91/76.91 (E(f6(a1,f4(f7(a5),x3321)),f4(f7(f4(a3,a5)),x3321))),
% 76.91/76.91 inference(scs_inference,[],[322,2])).
% 76.91/76.91 cnf(765,plain,
% 76.91/76.91 (P1(f7(f4(f7(f4(a2,x7651)),f7(f4(a2,f7(x7651))))))),
% 76.91/76.91 inference(scs_inference,[],[12,45,10])).
% 76.91/76.91 cnf(768,plain,
% 76.91/76.91 (P1(f6(a1,a2))),
% 76.91/76.91 inference(scs_inference,[],[12,22,10])).
% 76.91/76.91 cnf(801,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f4(f7(a5),x8011))),f4(f7(f4(a3,a5)),x8011))),
% 76.91/76.91 inference(scs_inference,[],[13,332,3])).
% 76.91/76.91 cnf(1042,plain,
% 76.91/76.91 (E(f6(a1,x10421),f7(f4(f7(f4(x10421,x10422)),f7(f4(x10421,f7(x10422))))))),
% 76.91/76.91 inference(scs_inference,[],[13,45,3])).
% 76.91/76.91 cnf(1044,plain,
% 76.91/76.91 (E(f7(f4(f7(f4(x10441,x10442)),f7(f4(x10441,f7(x10442))))),f6(a1,x10441))),
% 76.91/76.91 inference(scs_inference,[],[13,45,3,2])).
% 76.91/76.91 cnf(1186,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,x11861)),f7(f4(f7(f4(x11861,x11862)),f7(f4(x11861,f7(x11862))))))),
% 76.91/76.91 inference(scs_inference,[],[13,1042,3])).
% 76.91/76.91 cnf(1188,plain,
% 76.91/76.91 (E(f7(f4(f7(f4(x11881,x11882)),f7(f4(x11881,f7(x11882))))),f6(a1,f6(a1,x11881)))),
% 76.91/76.91 inference(scs_inference,[],[13,1042,3,2])).
% 76.91/76.91 cnf(1261,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,x12611)),f6(a1,f7(f4(f7(f4(x12611,x12612)),f7(f4(x12611,f7(x12612)))))))),
% 76.91/76.91 inference(scs_inference,[],[13,1188,3,2])).
% 76.91/76.91 cnf(1322,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f6(a1,x13221))),f7(f4(f7(f4(x13221,x13222)),f7(f4(x13221,f7(x13222))))))),
% 76.91/76.91 inference(scs_inference,[],[13,1186,3])).
% 76.91/76.91 cnf(1324,plain,
% 76.91/76.91 (E(f7(f4(f7(f4(x13241,x13242)),f7(f4(x13241,f7(x13242))))),f6(a1,f6(a1,f6(a1,x13241))))),
% 76.91/76.91 inference(scs_inference,[],[13,1186,3,2])).
% 76.91/76.91 cnf(1404,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f6(a1,f6(a1,x14041)))),f7(f4(f7(f4(x14041,x14042)),f7(f4(x14041,f7(x14042))))))),
% 76.91/76.91 inference(scs_inference,[],[13,1322,3])).
% 76.91/76.91 cnf(1416,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,x14161))))),f7(f4(f7(f4(x14161,x14162)),f7(f4(x14161,f7(x14162))))))),
% 76.91/76.91 inference(scs_inference,[],[13,1404,3])).
% 76.91/76.91 cnf(1420,plain,
% 76.91/76.91 (E(f7(f4(f7(f4(x14201,x14202)),f7(f4(x14201,f7(x14202))))),f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,x14201))))))),
% 76.91/76.91 inference(scs_inference,[],[1416,2])).
% 76.91/76.91 cnf(1421,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f6(a1,f4(f7(a5),x14211)))),f4(f7(f4(a3,a5)),x14211))),
% 76.91/76.91 inference(scs_inference,[],[13,1416,801,2,3])).
% 76.91/76.91 cnf(1426,plain,
% 76.91/76.91 (E(f4(f7(f4(a3,a5)),x14261),f6(a1,f6(a1,f6(a1,f4(f7(a5),x14261)))))),
% 76.91/76.91 inference(scs_inference,[],[1421,2])).
% 76.91/76.91 cnf(5991,plain,
% 76.91/76.91 (E(f6(a1,f6(a1,f6(a1,f4(f7(a5),x59911)))),f6(a1,f4(f7(a5),x59911)))),
% 76.91/76.91 inference(scs_inference,[],[332,1426,3,2])).
% 76.91/76.91 cnf(6819,plain,
% 76.91/76.91 (E(f4(f6(a1,a2),f6(x68191,f6(a1,a2))),f6(f8(x68191),f6(a1,a2)))),
% 76.91/76.91 inference(scs_inference,[],[768,5991,9,4,5,6,20])).
% 76.91/76.91 cnf(6822,plain,
% 76.91/76.91 (~E(a3,f7(f4(f7(a5),f7(f4(a3,f7(a5))))))),
% 76.91/76.91 inference(scs_inference,[],[768,24,5991,9,4,5,6,20,7,2])).
% 76.91/76.91 cnf(6824,plain,
% 76.91/76.91 (P1(f8(f6(a1,a2)))),
% 76.91/76.91 inference(scs_inference,[],[768,24,5991,9,4,5,6,20,7,2,8,19])).
% 76.91/76.91 cnf(6826,plain,
% 76.91/76.91 (~E(f4(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),a5),a5)),
% 76.91/76.91 inference(scs_inference,[],[768,24,23,5991,15,9,4,5,6,20,7,2,8,19,3])).
% 76.91/76.91 cnf(6832,plain,
% 76.91/76.91 (E(f4(a1,f6(x68321,a1)),f6(f8(x68321),a1))),
% 76.91/76.91 inference(scs_inference,[],[11,6819,9,20])).
% 76.91/76.91 cnf(6839,plain,
% 76.91/76.91 (~E(a3,f6(a2,f4(a3,f7(f4(a3,f7(a5))))))),
% 76.91/76.91 inference(scs_inference,[],[11,6819,44,9,20,4,6,5,7,8,2])).
% 76.91/76.91 cnf(6840,plain,
% 76.91/76.91 (P1(f8(a1))),
% 76.91/76.91 inference(scs_inference,[],[11,6819,44,9,20,4,6,5,7,8,2,19])).
% 76.91/76.91 cnf(6843,plain,
% 76.91/76.91 (E(x68431,f7(f4(f7(f4(x68431,x68432)),f7(f4(x68431,f7(x68432))))))),
% 76.91/76.91 inference(rename_variables,[],[45])).
% 76.91/76.91 cnf(6844,plain,
% 76.91/76.91 (P1(f7(f4(f7(f4(f8(f6(a1,a2)),x68441)),f7(f4(f8(f6(a1,a2)),f7(x68441))))))),
% 76.91/76.91 inference(scs_inference,[],[11,6824,6819,44,45,6843,9,20,4,6,5,7,8,2,19,3,10])).
% 76.91/76.91 cnf(6847,plain,
% 76.91/76.91 (E(f8(f4(a1,f6(x68471,a1))),f8(f6(f8(x68471),a1)))),
% 76.91/76.91 inference(scs_inference,[],[6832,9])).
% 76.91/76.91 cnf(6848,plain,
% 76.91/76.91 (E(f4(f6(a1,a1),f6(x68481,f6(a1,a1))),f6(f8(x68481),f6(a1,a1)))),
% 76.91/76.91 inference(scs_inference,[],[6832,30,9,20])).
% 76.91/76.91 cnf(6850,plain,
% 76.91/76.92 (E(f6(f4(a1,f6(x68501,a1)),x68502),f6(f6(f8(x68501),a1),x68502))),
% 76.91/76.92 inference(scs_inference,[],[6832,30,9,20,4])).
% 76.91/76.92 cnf(6851,plain,
% 76.91/76.92 (E(f4(f4(a1,f6(x68511,a1)),x68512),f4(f6(f8(x68511),a1),x68512))),
% 76.91/76.92 inference(scs_inference,[],[6832,30,9,20,4,6])).
% 76.91/76.92 cnf(6852,plain,
% 76.91/76.92 (E(f6(x68521,f4(a1,f6(x68522,a1))),f6(x68521,f6(f8(x68522),a1)))),
% 76.91/76.92 inference(scs_inference,[],[6832,30,9,20,4,6,5])).
% 76.91/76.92 cnf(6853,plain,
% 76.91/76.92 (E(f4(x68531,f4(a1,f6(x68532,a1))),f4(x68531,f6(f8(x68532),a1)))),
% 76.91/76.92 inference(scs_inference,[],[6832,30,9,20,4,6,5,7])).
% 76.91/76.92 cnf(6854,plain,
% 76.91/76.92 (E(f7(f4(a1,f6(x68541,a1))),f7(f6(f8(x68541),a1)))),
% 76.91/76.92 inference(scs_inference,[],[6832,30,9,20,4,6,5,7,8])).
% 76.91/76.92 cnf(6855,plain,
% 76.91/76.92 (~E(a5,f4(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),a5))),
% 76.91/76.92 inference(scs_inference,[],[6832,6826,30,9,20,4,6,5,7,8,2])).
% 76.91/76.92 cnf(6856,plain,
% 76.91/76.92 (P1(f8(f8(a1)))),
% 76.91/76.92 inference(scs_inference,[],[6840,6832,6826,30,9,20,4,6,5,7,8,2,19])).
% 76.91/76.92 cnf(6858,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a3,x68581)),f7(f4(a3,f7(x68581))))),f7(f4(f7(a5),f7(f4(a3,f7(a5))))))),
% 76.91/76.92 inference(scs_inference,[],[6840,6832,6822,6826,30,45,9,20,4,6,5,7,8,2,19,3])).
% 76.91/76.92 cnf(6861,plain,
% 76.91/76.92 (E(f8(f4(f6(a1,a1),f6(x68611,f6(a1,a1)))),f8(f6(f8(x68611),f6(a1,a1))))),
% 76.91/76.92 inference(scs_inference,[],[6848,9])).
% 76.91/76.92 cnf(6865,plain,
% 76.91/76.92 (E(f4(f4(f6(a1,a1),f6(x68651,f6(a1,a1))),x68652),f4(f6(f8(x68651),f6(a1,a1)),x68652))),
% 76.91/76.92 inference(scs_inference,[],[6856,6848,9,20,4,6])).
% 76.91/76.92 cnf(6870,plain,
% 76.91/76.92 (P1(f8(f8(f8(a1))))),
% 76.91/76.92 inference(scs_inference,[],[6856,6848,6858,9,20,4,6,5,7,8,2,19])).
% 76.91/76.92 cnf(6884,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(a1)))))),
% 76.91/76.92 inference(scs_inference,[],[6870,6850,42,9,20,4,6,5,7,8,2,19])).
% 76.91/76.92 cnf(6886,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a3,x68861)),f7(f4(a3,f7(x68861))))),f6(a2,f4(a3,f7(f4(a3,f7(a5))))))),
% 76.91/76.92 inference(scs_inference,[],[6870,6850,6839,42,45,9,20,4,6,5,7,8,2,19,3])).
% 76.91/76.92 cnf(6898,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(f8(a1))))))),
% 76.91/76.92 inference(scs_inference,[],[6851,6884,6886,9,20,6,4,5,7,2,8,19])).
% 76.91/76.92 cnf(6900,plain,
% 76.91/76.92 (E(f4(f4(a1,f6(x69001,a1)),f4(a1,f6(x69002,a1))),f4(f6(f8(x69001),a1),f6(f8(x69002),a1)))),
% 76.91/76.92 inference(scs_inference,[],[6851,6853,6884,6886,9,20,6,4,5,7,2,8,19,3])).
% 76.91/76.92 cnf(6917,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a5,x69171)),f7(f4(a5,f7(x69171))))),f4(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),a5))),
% 76.91/76.92 inference(scs_inference,[],[6852,6898,6855,6824,38,45,9,20,4,6,5,7,8,2,19,3])).
% 76.91/76.92 cnf(6924,plain,
% 76.91/76.92 (E(f6(f8(f4(a1,f6(x69241,a1))),x69242),f6(f8(f6(f8(x69241),a1)),x69242))),
% 76.91/76.92 inference(scs_inference,[],[6847,35,9,20,6,4])).
% 76.91/76.92 cnf(6927,plain,
% 76.91/76.92 (~E(f4(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),a5),f7(f4(f7(f4(a5,x69271)),f7(f4(a5,f7(x69271))))))),
% 76.91/76.92 inference(scs_inference,[],[6847,6917,35,9,20,6,4,5,7,2])).
% 76.91/76.92 cnf(6943,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,f6(a1,a1)))))),
% 76.91/76.92 inference(scs_inference,[],[6854,40,23,9,20,4,6,5,7,8,2,19])).
% 76.91/76.92 cnf(6945,plain,
% 76.91/76.92 (~E(f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))),f7(f4(f7(f4(a5,x69451)),f7(f4(a5,f7(x69451))))))),
% 76.91/76.92 inference(scs_inference,[],[6854,6927,40,23,15,9,20,4,6,5,7,8,2,19,3])).
% 76.91/76.92 cnf(6955,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a5,x69551)),f7(f4(a5,f7(x69551))))),f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))))),
% 76.91/76.92 inference(scs_inference,[],[6943,6900,6945,9,20,6,4,5,7,2])).
% 76.91/76.92 cnf(6957,plain,
% 76.91/76.92 (P1(f8(f8(f6(a1,f6(a1,f6(a1,a1))))))),
% 76.91/76.92 inference(scs_inference,[],[6943,6900,6945,9,20,6,4,5,7,2,8,19])).
% 76.91/76.92 cnf(6959,plain,
% 76.91/76.92 (E(f4(f4(a1,f6(x69591,a1)),f4(a1,f6(x69592,a1))),f4(f6(f8(x69592),a1),f6(f8(x69591),a1)))),
% 76.91/76.92 inference(scs_inference,[],[6943,6900,6945,15,9,20,6,4,5,7,2,8,19,3])).
% 76.91/76.92 cnf(6972,plain,
% 76.91/76.92 (P1(f8(f8(f8(f6(a1,f6(a1,f6(a1,a1)))))))),
% 76.91/76.92 inference(scs_inference,[],[6959,6957,46,9,20,6,4,5,7,8,19])).
% 76.91/76.92 cnf(6982,plain,
% 76.91/76.92 (E(f4(a2,f6(x69821,a2)),f6(f8(x69821),a2))),
% 76.91/76.92 inference(scs_inference,[],[6861,6972,12,19,9,20])).
% 76.91/76.92 cnf(6991,plain,
% 76.91/76.92 (P1(f8(a2))),
% 76.91/76.92 inference(scs_inference,[],[12,19])).
% 76.91/76.92 cnf(6993,plain,
% 76.91/76.92 (E(f4(f8(a2),f6(x69931,f8(a2))),f6(f8(x69931),f8(a2)))),
% 76.91/76.92 inference(scs_inference,[],[12,19,20])).
% 76.91/76.92 cnf(6995,plain,
% 76.91/76.92 (E(f8(f4(a2,f6(x69951,a2))),f8(f6(f8(x69951),a2)))),
% 76.91/76.92 inference(scs_inference,[],[12,6982,19,20,9])).
% 76.91/76.92 cnf(6996,plain,
% 76.91/76.92 (E(f4(f4(a2,f6(x69961,a2)),x69962),f4(f6(f8(x69961),a2),x69962))),
% 76.91/76.92 inference(scs_inference,[],[12,6982,19,20,9,6])).
% 76.91/76.92 cnf(6999,plain,
% 76.91/76.92 (E(f4(x69991,f4(a2,f6(x69992,a2))),f4(x69991,f6(f8(x69992),a2)))),
% 76.91/76.92 inference(scs_inference,[],[12,6982,19,20,9,6,4,5,7])).
% 76.91/76.92 cnf(7000,plain,
% 76.91/76.92 (E(f7(f4(a2,f6(x70001,a2))),f7(f6(f8(x70001),a2)))),
% 76.91/76.92 inference(scs_inference,[],[12,6982,19,20,9,6,4,5,7,8])).
% 76.91/76.92 cnf(7005,plain,
% 76.91/76.92 (P1(f8(f8(a2)))),
% 76.91/76.92 inference(scs_inference,[],[6991,19])).
% 76.91/76.92 cnf(7018,plain,
% 76.91/76.92 (P1(f7(f4(f7(f4(f8(a2),x70181)),f7(f4(f8(a2),f7(x70181))))))),
% 76.91/76.92 inference(scs_inference,[],[6991,6993,6924,45,19,20,9,6,4,5,7,8,3,10])).
% 76.91/76.92 cnf(7021,plain,
% 76.91/76.92 (P1(f8(f8(f8(a2))))),
% 76.91/76.92 inference(scs_inference,[],[7005,19])).
% 76.91/76.92 cnf(7034,plain,
% 76.91/76.92 (~E(f7(f4(f7(a5),f7(f4(a3,f7(a5))))),f6(a1,a3))),
% 76.91/76.92 inference(scs_inference,[],[7005,6996,6858,1044,19,9,6,20,4,5,7,8,3,2])).
% 76.91/76.92 cnf(7036,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(a2)))))),
% 76.91/76.92 inference(scs_inference,[],[7021,19])).
% 76.91/76.92 cnf(7050,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(f8(a2))))))),
% 76.91/76.92 inference(scs_inference,[],[7036,19])).
% 76.91/76.92 cnf(7061,plain,
% 76.91/76.92 (~E(f6(a2,f4(a3,f7(f4(a3,f7(a5))))),f6(a1,a3))),
% 76.91/76.92 inference(scs_inference,[],[6999,7036,6886,1044,19,6,9,4,5,7,8,3,2])).
% 76.91/76.92 cnf(7063,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(f8(f8(a2)))))))),
% 76.91/76.92 inference(scs_inference,[],[7050,19])).
% 76.91/76.92 cnf(7073,plain,
% 76.91/76.92 (P1(f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,f8(a2)))))))),
% 76.91/76.92 inference(scs_inference,[],[6995,7050,7018,1420,45,19,6,9,4,5,7,8,3,10])).
% 76.91/76.92 cnf(7085,plain,
% 76.91/76.92 (~E(f6(a1,f6(a1,a5)),f4(a5,f6(a2,f4(a3,f7(f4(a3,f7(a5)))))))),
% 76.91/76.92 inference(scs_inference,[],[7000,7063,6955,1188,19,6,9,4,5,7,8,3])).
% 76.91/76.92 cnf(7090,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,f6(a1,f6(a1,f6(a1,f8(a2))))))))),
% 76.91/76.92 inference(scs_inference,[],[7073,19])).
% 76.91/76.92 cnf(7135,plain,
% 76.91/76.92 (P1(f6(a1,f6(a1,f6(a1,f8(f6(a1,a2))))))),
% 76.91/76.92 inference(scs_inference,[],[6865,7085,6844,1261,50,1324,19,8,6,9,4,5,7,3,10])).
% 76.91/76.92 cnf(7139,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,f6(a1,f8(f6(a1,a2)))))))),
% 76.91/76.92 inference(scs_inference,[],[7135,19])).
% 76.91/76.92 cnf(7142,plain,
% 76.91/76.92 (E(f4(f6(a1,x71421),x71422),f4(x71421,x71422))),
% 76.91/76.92 inference(scs_inference,[],[13,7135,19,8,6])).
% 76.91/76.92 cnf(7143,plain,
% 76.91/76.92 (E(f8(f6(a1,x71431)),f8(x71431))),
% 76.91/76.92 inference(scs_inference,[],[13,7135,19,8,6,9])).
% 76.91/76.92 cnf(7144,plain,
% 76.91/76.92 (E(f6(f6(a1,x71441),x71442),f6(x71441,x71442))),
% 76.91/76.92 inference(scs_inference,[],[13,7135,19,8,6,9,4])).
% 76.91/76.92 cnf(7145,plain,
% 76.91/76.92 (E(f6(x71451,f6(a1,x71452)),f6(x71451,x71452))),
% 76.91/76.92 inference(scs_inference,[],[13,7135,19,8,6,9,4,5])).
% 76.91/76.92 cnf(7146,plain,
% 76.91/76.92 (E(f4(x71461,f6(a1,x71462)),f4(x71461,x71462))),
% 76.91/76.92 inference(scs_inference,[],[13,7135,19,8,6,9,4,5,7])).
% 76.91/76.92 cnf(7154,plain,
% 76.91/76.92 (E(f4(f4(f6(a1,x71541),x71542),x71543),f4(f4(x71541,x71542),x71543))),
% 76.91/76.92 inference(scs_inference,[],[7142,7139,19,8,6])).
% 76.91/76.92 cnf(7156,plain,
% 76.91/76.92 (E(f6(f4(f6(a1,x71561),x71562),x71563),f6(f4(x71561,x71562),x71563))),
% 76.91/76.92 inference(scs_inference,[],[7142,7139,19,8,6,9,4])).
% 76.91/76.92 cnf(7172,plain,
% 76.91/76.92 (E(f6(f6(a1,a1),x71721),x71721)),
% 76.91/76.92 inference(scs_inference,[],[13,7144,78,19,8,6,9,4,5,7,3])).
% 76.91/76.92 cnf(7178,plain,
% 76.91/76.92 (E(f4(f6(x71781,f6(a1,x71782)),x71783),f4(f6(x71781,x71782),x71783))),
% 76.91/76.92 inference(scs_inference,[],[7145,765,19,8,6])).
% 76.91/76.92 cnf(7179,plain,
% 76.91/76.92 (E(f8(f6(x71791,f6(a1,x71792))),f8(f6(x71791,x71792)))),
% 76.91/76.92 inference(scs_inference,[],[7145,765,19,8,6,9])).
% 76.91/76.92 cnf(7187,plain,
% 76.91/76.92 (P1(f8(f6(a1,a1)))),
% 76.91/76.92 inference(scs_inference,[],[30,19])).
% 76.91/76.92 cnf(7199,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,f6(a1,f6(a1,f8(a2)))))))),
% 76.91/76.92 inference(scs_inference,[],[7146,7143,7154,7090,30,19,8,20,6,9,4,5,7,3,10])).
% 76.91/76.92 cnf(7202,plain,
% 76.91/76.92 (P1(f8(f8(f6(a1,a1))))),
% 76.91/76.92 inference(scs_inference,[],[7187,19])).
% 76.91/76.92 cnf(7216,plain,
% 76.91/76.92 (P1(f8(f8(f8(f6(a1,a1)))))),
% 76.91/76.92 inference(scs_inference,[],[7202,19])).
% 76.91/76.92 cnf(7218,plain,
% 76.91/76.92 (E(f7(f6(f6(a1,a1),x72181)),f7(x72181))),
% 76.91/76.92 inference(scs_inference,[],[7172,7202,19,8])).
% 76.91/76.92 cnf(7223,plain,
% 76.91/76.92 (E(f6(f6(f6(a1,a1),x72231),x72232),f6(x72231,x72232))),
% 76.91/76.92 inference(scs_inference,[],[7172,7202,19,8,20,6,9,4])).
% 76.91/76.92 cnf(7226,plain,
% 76.91/76.92 (E(f6(f6(a1,a1),f6(a1,x72261)),x72261)),
% 76.91/76.92 inference(scs_inference,[],[13,7172,7202,19,8,20,6,9,4,5,7,3])).
% 76.91/76.92 cnf(7229,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(f6(a1,a1))))))),
% 76.91/76.92 inference(scs_inference,[],[7216,19])).
% 76.91/76.92 cnf(7231,plain,
% 76.91/76.92 (E(f7(f6(f6(a1,a1),f6(a1,x72311))),f7(x72311))),
% 76.91/76.92 inference(scs_inference,[],[7226,7216,19,8])).
% 76.91/76.92 cnf(7251,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,f6(a1,f8(a2))))))),
% 76.91/76.92 inference(scs_inference,[],[7218,7231,7179,7229,7199,19,8,9,6,4,5,7,3,10])).
% 76.91/76.92 cnf(7254,plain,
% 76.91/76.92 (P1(f8(f8(f6(a1,f6(a1,f6(a1,f8(a2)))))))),
% 76.91/76.92 inference(scs_inference,[],[7251,19])).
% 76.91/76.92 cnf(7278,plain,
% 76.91/76.92 (E(f4(x72781,f7(f4(a3,a5))),f4(x72781,f7(a5)))),
% 76.91/76.92 inference(scs_inference,[],[14,5,7])).
% 76.91/76.92 cnf(7283,plain,
% 76.91/76.92 (E(f8(f7(f4(a3,a5))),f8(f7(a5)))),
% 76.91/76.92 inference(scs_inference,[],[14,7223,7254,5,7,19,8,6,9])).
% 76.91/76.92 cnf(7388,plain,
% 76.91/76.92 (P1(f8(f6(a1,f6(a1,a1))))),
% 76.91/76.92 inference(scs_inference,[],[7283,35,5,19])).
% 76.91/76.92 cnf(7397,plain,
% 76.91/76.92 (P1(f7(f4(f7(f4(f8(a1),x73971)),f7(f4(f8(a1),f7(x73971))))))),
% 76.91/76.92 inference(scs_inference,[],[7283,6840,35,45,5,19,7,8,20,9,6,4,10])).
% 76.91/76.92 cnf(7404,plain,
% 76.91/76.92 (P1(f8(f8(f6(a1,f6(a1,a1)))))),
% 76.91/76.92 inference(scs_inference,[],[7388,7156,9,6,4,5,19])).
% 76.91/76.92 cnf(7411,plain,
% 76.91/76.92 (E(f8(f4(x74111,x74112)),f8(f4(x74112,x74111)))),
% 76.91/76.92 inference(scs_inference,[],[15,9])).
% 76.91/76.92 cnf(7412,plain,
% 76.91/76.92 (E(f4(f4(x74121,x74122),x74123),f4(f4(x74122,x74121),x74123))),
% 76.91/76.92 inference(scs_inference,[],[15,9,6])).
% 76.91/76.92 cnf(7413,plain,
% 76.91/76.92 (E(f6(f4(x74131,x74132),x74133),f6(f4(x74132,x74131),x74133))),
% 76.91/76.92 inference(scs_inference,[],[15,9,6,4])).
% 76.91/76.92 cnf(7414,plain,
% 76.91/76.92 (E(f6(x74141,f4(x74142,x74143)),f6(x74141,f4(x74143,x74142)))),
% 76.91/76.92 inference(scs_inference,[],[15,9,6,4,5])).
% 76.91/76.92 cnf(7415,plain,
% 76.91/76.92 (P1(f8(f8(f8(f6(a1,f6(a1,a1))))))),
% 76.91/76.92 inference(scs_inference,[],[15,7404,9,6,4,5,19])).
% 76.91/76.92 cnf(7418,plain,
% 76.91/76.92 (E(f7(f4(x74181,x74182)),f7(f4(x74182,x74181)))),
% 76.91/76.92 inference(scs_inference,[],[15,7404,9,6,4,5,19,7,8])).
% 76.91/76.92 cnf(7423,plain,
% 76.91/76.92 (P1(f8(f8(f8(f8(f6(a1,f6(a1,a1)))))))),
% 76.91/76.92 inference(scs_inference,[],[7411,7415,9,6,4,19])).
% 76.91/76.92 cnf(7430,plain,
% 76.91/76.92 (~E(f6(a1,a3),f7(f4(f7(f4(a3,f7(a5))),f7(a5))))),
% 76.91/76.92 inference(scs_inference,[],[7411,7418,7034,7415,9,6,4,19,5,7,8,3,2])).
% 76.91/76.92 cnf(7443,plain,
% 76.91/76.92 (P1(f7(f4(f7(f4(f8(a1),f7(x74431))),f7(f4(f8(a1),x74431)))))),
% 76.91/76.92 inference(scs_inference,[],[7412,7414,7061,7397,7423,7418,9,6,4,19,5,7,8,3,2,10])).
% 76.91/76.92 cnf(7454,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a3,x74541)),f7(f4(a3,f7(x74541))))),f7(f4(f7(f4(a3,f7(a5))),f7(a5))))),
% 76.91/76.92 inference(scs_inference,[],[7413,7430,7443,1042,9,6,4,19,5,7,8,3])).
% 76.91/76.92 cnf(7502,plain,
% 76.91/76.92 (~E(f7(f4(f7(f4(a3,f7(x75021))),f7(f4(a3,x75021)))),f7(f4(f7(f4(a3,f7(a5))),f7(a5))))),
% 76.91/76.92 inference(scs_inference,[],[7178,7454,7418,9,6,4,5,7,8,3])).
% 76.91/76.92 cnf(7696,plain,
% 76.91/76.92 ($false),
% 76.91/76.92 inference(scs_inference,[],[7278,7502,8]),
% 76.91/76.92 ['proof']).
% 76.91/76.92 % SZS output end Proof
% 76.91/76.92 % Total time :76.250000s
%------------------------------------------------------------------------------