%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP022-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 : n023.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:38:30 EDT 2024
% Result : Unsatisfiable 40.33s 40.38s
% Output : CNFRefutation 40.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP022-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 : n023.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 : Thu Jun 20 10:13:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.48/0.58 start to proof:theBenchmark
% 40.33/40.37 %-------------------------------------------
% 40.33/40.37 % File :CSE---1.7
% 40.33/40.37 % Problem :theBenchmark
% 40.33/40.37 % Transform :cnf
% 40.33/40.37 % Format :tptp:raw
% 40.33/40.37 % Command :java -jar mcs_scs.jar %d %s
% 40.33/40.37
% 40.33/40.37 % Result :Theorem 39.770000s
% 40.33/40.37 % Output :CNFRefutation 39.770000s
% 40.33/40.38 %-------------------------------------------
% 40.33/40.38 %--------------------------------------------------------------------------
% 40.33/40.38 % File : GRP022-1 : TPTP v8.2.0. Released v1.0.0.
% 40.33/40.38 % Domain : Group Theory
% 40.33/40.38 % Problem : Inverse is an involution
% 40.33/40.38 % Version : [MOW76] axioms.
% 40.33/40.38 % English :
% 40.33/40.38
% 40.33/40.38 % Refs : [Wos65] Wos (1965), Unpublished Note
% 40.33/40.38 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 40.33/40.38 % : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
% 40.33/40.38 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 40.33/40.38 % Source : [MOW76]
% 40.33/40.38 % Names : Identity established [MOW76]
% 40.33/40.38 % : Lemma proved [OMW76]
% 40.33/40.38 % : wos8 [WM76]
% 40.33/40.38
% 40.33/40.38 % Status : Unsatisfiable
% 40.33/40.38 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.00 v2.0.0
% 40.33/40.38 % Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 4 RR)
% 40.33/40.38 % Number of literals : 17 ( 2 equ; 9 neg)
% 40.33/40.38 % Maximal clause size : 4 ( 1 avg)
% 40.33/40.38 % Maximal term depth : 3 ( 1 avg)
% 40.33/40.38 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 40.33/40.38 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 40.33/40.38 % Number of variables : 22 ( 0 sgn)
% 40.33/40.38 % SPC : CNF_UNS_RFO_SEQ_HRN
% 40.33/40.38
% 40.33/40.38 % Comments :
% 40.33/40.38 %--------------------------------------------------------------------------
% 40.33/40.38 %----Include group theory axioms
% 40.33/40.38 include('Axioms/GRP003-0.ax').
% 40.33/40.38 %--------------------------------------------------------------------------
% 40.33/40.38 cnf(prove_inverse_of_inverse_is_original,negated_conjecture,
% 40.33/40.38 inverse(inverse(a)) != a ).
% 40.33/40.38
% 40.33/40.38 %--------------------------------------------------------------------------
% 40.33/40.38 %-------------------------------------------
% 40.33/40.38 % Proof found
% 40.33/40.38 % SZS status Theorem for theBenchmark
% 40.33/40.38 % SZS output start Proof
% 40.33/40.38 %ClaNum:18(EqnAxiom:9)
% 40.33/40.38 %VarNum:44(SingletonVarNum:22)
% 40.33/40.38 %MaxLitNum:4
% 40.33/40.38 %MaxfuncDepth:2
% 40.33/40.38 %SharedTerms:5
% 40.33/40.38 %goalClause: 15
% 40.33/40.38 %singleGoalClaCount:1
% 40.33/40.38 [15]~E(f3(f3(a2)),a2)
% 40.33/40.38 [10]P1(x101,a1,x101)
% 40.33/40.38 [11]P1(a1,x111,x111)
% 40.33/40.38 [12]P1(x121,f3(x121),a1)
% 40.33/40.38 [13]P1(f3(x131),x131,a1)
% 40.33/40.38 [14]P1(x141,x142,f4(x141,x142))
% 40.33/40.38 [16]~P1(x163,x164,x161)+E(x161,x162)+~P1(x163,x164,x162)
% 40.33/40.38 [17]~P1(x176,x174,x171)+P1(x171,x172,x173)+~P1(x174,x172,x175)+~P1(x176,x175,x173)
% 40.33/40.38 [18]~P1(x181,x186,x184)+P1(x181,x182,x183)+~P1(x184,x185,x183)+~P1(x186,x185,x182)
% 40.33/40.38 %EqnAxiom
% 40.33/40.38 [1]E(x11,x11)
% 40.33/40.38 [2]E(x22,x21)+~E(x21,x22)
% 40.33/40.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 40.33/40.38 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 40.33/40.38 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 40.33/40.38 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 40.33/40.38 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 40.33/40.38 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 40.33/40.38 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 40.33/40.38
% 40.33/40.38 %-------------------------------------------
% 40.33/40.39 cnf(19,plain,
% 40.33/40.39 (E(x191,f4(x191,a1))),
% 40.33/40.39 inference(scs_inference,[],[10,14,16])).
% 40.33/40.39 cnf(20,plain,
% 40.33/40.39 (P1(x201,x202,f4(x201,x202))),
% 40.33/40.39 inference(rename_variables,[],[14])).
% 40.33/40.39 cnf(22,plain,
% 40.33/40.39 (P1(f4(x221,a1),a1,x221)),
% 40.33/40.39 inference(scs_inference,[],[10,14,16,7])).
% 40.33/40.39 cnf(24,plain,
% 40.33/40.39 (P1(x241,a1,x241)),
% 40.33/40.39 inference(rename_variables,[],[10])).
% 40.33/40.39 cnf(25,plain,
% 40.33/40.39 (P1(x251,f3(x251),f4(a1,a1))),
% 40.33/40.39 inference(scs_inference,[],[10,14,12,16,7,8,9])).
% 40.33/40.39 cnf(26,plain,
% 40.33/40.39 (P1(x261,f4(a1,a1),x261)),
% 40.33/40.39 inference(scs_inference,[],[10,24,14,20,12,16,7,8,9,18])).
% 40.33/40.39 cnf(30,plain,
% 40.33/40.39 (E(f4(x301,a1),x301)),
% 40.33/40.39 inference(scs_inference,[],[19,2])).
% 40.33/40.39 cnf(32,plain,
% 40.33/40.39 (E(f3(f4(a1,a1)),a1)),
% 40.33/40.39 inference(scs_inference,[],[15,19,26,13,2,3,16])).
% 40.33/40.39 cnf(34,plain,
% 40.33/40.39 (P1(x341,f4(a1,a1),x341)),
% 40.33/40.39 inference(rename_variables,[],[26])).
% 40.33/40.39 cnf(36,plain,
% 40.33/40.39 (P1(a2,f4(a1,a1),f4(a2,a1))),
% 40.33/40.39 inference(scs_inference,[],[15,19,26,34,13,2,3,16,9])).
% 40.33/40.39 cnf(37,plain,
% 40.33/40.39 (P1(x371,f4(a1,a1),x371)),
% 40.33/40.39 inference(rename_variables,[],[26])).
% 40.33/40.39 cnf(38,plain,
% 40.33/40.39 (E(x381,f4(x381,a1))),
% 40.33/40.39 inference(rename_variables,[],[19])).
% 40.33/40.39 cnf(39,plain,
% 40.33/40.39 (P1(x391,f4(f4(a1,a1),a1),x391)),
% 40.33/40.39 inference(scs_inference,[],[15,19,38,26,34,37,13,2,3,16,9,8])).
% 40.33/40.39 cnf(40,plain,
% 40.33/40.39 (E(x401,f4(x401,a1))),
% 40.33/40.39 inference(rename_variables,[],[19])).
% 40.33/40.39 cnf(41,plain,
% 40.33/40.39 (P1(f4(x411,a1),f4(a1,a1),x411)),
% 40.33/40.39 inference(scs_inference,[],[15,19,38,40,26,34,37,13,2,3,16,9,8,7])).
% 40.33/40.39 cnf(42,plain,
% 40.33/40.39 (P1(x421,f4(a1,a1),x421)),
% 40.33/40.39 inference(rename_variables,[],[26])).
% 40.33/40.39 cnf(43,plain,
% 40.33/40.39 (P1(a1,f3(f4(a1,a1)),f4(a1,a1))),
% 40.33/40.39 inference(scs_inference,[],[15,19,38,40,26,34,37,42,25,11,13,2,3,16,9,8,7,17])).
% 40.33/40.39 cnf(45,plain,
% 40.33/40.39 (P1(x451,f4(a1,a1),x451)),
% 40.33/40.39 inference(rename_variables,[],[26])).
% 40.33/40.39 cnf(48,plain,
% 40.33/40.39 (P1(x481,f4(f4(a1,a1),f4(a1,a1)),x481)),
% 40.33/40.39 inference(scs_inference,[],[15,19,38,40,26,34,37,42,45,25,11,13,14,2,3,16,9,8,7,17,18])).
% 40.33/40.39 cnf(51,plain,
% 40.33/40.39 (E(a1,f3(f4(a1,a1)))),
% 40.33/40.39 inference(scs_inference,[],[32,2])).
% 40.33/40.39 cnf(52,plain,
% 40.33/40.39 (E(a1,f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.39 inference(scs_inference,[],[32,48,11,2,16])).
% 40.33/40.39 cnf(53,plain,
% 40.33/40.39 (P1(a1,x531,x531)),
% 40.33/40.39 inference(rename_variables,[],[11])).
% 40.33/40.39 cnf(54,plain,
% 40.33/40.39 (P1(x541,f4(f4(a1,a1),f4(a1,a1)),x541)),
% 40.33/40.39 inference(rename_variables,[],[48])).
% 40.33/40.39 cnf(56,plain,
% 40.33/40.39 (E(f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.39 inference(scs_inference,[],[30,32,48,11,2,16,3])).
% 40.33/40.39 cnf(57,plain,
% 40.33/40.39 (E(f4(x571,a1),x571)),
% 40.33/40.39 inference(rename_variables,[],[30])).
% 40.33/40.39 cnf(58,plain,
% 40.33/40.39 (P1(f4(x581,a1),f4(f4(a1,a1),f4(a1,a1)),x581)),
% 40.33/40.39 inference(scs_inference,[],[30,57,32,48,54,11,2,16,3,9])).
% 40.33/40.39 cnf(59,plain,
% 40.33/40.39 (P1(x591,f4(f4(a1,a1),f4(a1,a1)),x591)),
% 40.33/40.39 inference(rename_variables,[],[48])).
% 40.33/40.39 cnf(60,plain,
% 40.33/40.39 (P1(a1,x601,f4(x601,a1))),
% 40.33/40.39 inference(scs_inference,[],[30,57,32,48,54,11,53,2,16,3,9,8])).
% 40.33/40.39 cnf(61,plain,
% 40.33/40.39 (P1(a1,x611,x611)),
% 40.33/40.39 inference(rename_variables,[],[11])).
% 40.33/40.39 cnf(62,plain,
% 40.33/40.39 (P1(x621,f4(f4(a1,a1),f4(a1,a1)),f4(x621,a1))),
% 40.33/40.39 inference(scs_inference,[],[30,57,32,48,54,59,11,53,2,16,3,9,8,7])).
% 40.33/40.39 cnf(63,plain,
% 40.33/40.39 (P1(x631,f4(f4(a1,a1),f4(a1,a1)),x631)),
% 40.33/40.39 inference(rename_variables,[],[48])).
% 40.33/40.39 cnf(64,plain,
% 40.33/40.39 (P1(a1,f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.39 inference(scs_inference,[],[30,57,32,48,54,59,63,39,11,53,61,2,16,3,9,8,7,17])).
% 40.33/40.39 cnf(66,plain,
% 40.33/40.39 (P1(x661,f4(f4(a1,a1),f4(a1,a1)),x661)),
% 40.33/40.40 inference(rename_variables,[],[48])).
% 40.33/40.40 cnf(69,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[30,57,32,48,54,59,63,66,39,25,11,53,61,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(73,plain,
% 40.33/40.40 (E(f3(f4(a1,a1)),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[56,2])).
% 40.33/40.40 cnf(74,plain,
% 40.33/40.40 (E(f4(f4(x741,a1),a1),x741)),
% 40.33/40.40 inference(scs_inference,[],[56,62,58,2,16])).
% 40.33/40.40 cnf(75,plain,
% 40.33/40.40 (P1(x751,f4(f4(a1,a1),f4(a1,a1)),f4(x751,a1))),
% 40.33/40.40 inference(rename_variables,[],[62])).
% 40.33/40.40 cnf(77,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[56,30,62,58,2,16,3])).
% 40.33/40.40 cnf(79,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[56,30,69,62,58,2,16,3,9])).
% 40.33/40.40 cnf(80,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[56,30,69,62,58,2,16,3,9,8])).
% 40.33/40.40 cnf(81,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[56,30,69,62,58,2,16,3,9,8,7])).
% 40.33/40.40 cnf(82,plain,
% 40.33/40.40 (P1(f4(x821,a1),f4(f4(a1,a1),f4(a1,a1)),x821)),
% 40.33/40.40 inference(rename_variables,[],[58])).
% 40.33/40.40 cnf(83,plain,
% 40.33/40.40 (P1(f4(f4(x831,a1),a1),f4(f4(a1,a1),f4(a1,a1)),x831)),
% 40.33/40.40 inference(scs_inference,[],[56,30,69,62,75,58,82,48,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(87,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,a1)),
% 40.33/40.40 inference(scs_inference,[],[56,30,69,62,75,58,82,48,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(90,plain,
% 40.33/40.40 (E(f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[77,2])).
% 40.33/40.40 cnf(91,plain,
% 40.33/40.40 (E(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[77,79,26,2,16])).
% 40.33/40.40 cnf(92,plain,
% 40.33/40.40 (P1(x921,f4(a1,a1),x921)),
% 40.33/40.40 inference(rename_variables,[],[26])).
% 40.33/40.40 cnf(94,plain,
% 40.33/40.40 (P1(a1,f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[77,19,79,43,26,2,16,9])).
% 40.33/40.40 cnf(95,plain,
% 40.33/40.40 (E(x951,f4(x951,a1))),
% 40.33/40.40 inference(rename_variables,[],[19])).
% 40.33/40.40 cnf(98,plain,
% 40.33/40.40 (P1(f4(x981,a1),f4(f4(a1,a1),a1),x981)),
% 40.33/40.40 inference(scs_inference,[],[15,77,74,19,95,79,41,43,26,2,16,9,3,8])).
% 40.33/40.40 cnf(100,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[15,77,74,19,95,79,41,43,26,2,16,9,3,8,7])).
% 40.33/40.40 cnf(101,plain,
% 40.33/40.40 (P1(f4(x1011,a1),f4(a1,a1),x1011)),
% 40.33/40.40 inference(rename_variables,[],[41])).
% 40.33/40.40 cnf(102,plain,
% 40.33/40.40 (P1(a1,f3(f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[15,77,74,19,95,80,79,41,81,43,26,13,2,16,9,3,8,7,17])).
% 40.33/40.40 cnf(105,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[15,77,74,19,95,80,79,41,101,81,43,26,92,13,2,16,9,3,8,7,17,18])).
% 40.33/40.40 cnf(109,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[91,2])).
% 40.33/40.40 cnf(110,plain,
% 40.33/40.40 (E(f4(f3(a1),a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[91,60,12,2,16])).
% 40.33/40.40 cnf(114,plain,
% 40.33/40.40 (E(a1,f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[91,90,51,60,12,2,16,3])).
% 40.33/40.40 cnf(115,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[73,91,90,51,105,60,12,2,16,3,9])).
% 40.33/40.40 cnf(116,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),a1,f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[73,91,90,51,30,100,105,60,12,2,16,3,9,8])).
% 40.33/40.40 cnf(118,plain,
% 40.33/40.40 (P1(x1181,f4(f4(a1,a1),a1),f4(x1181,a1))),
% 40.33/40.40 inference(scs_inference,[],[73,91,90,51,74,30,100,98,105,60,12,2,16,3,9,8,7])).
% 40.33/40.40 cnf(119,plain,
% 40.33/40.40 (P1(f4(x1191,a1),f4(f4(a1,a1),a1),x1191)),
% 40.33/40.40 inference(rename_variables,[],[98])).
% 40.33/40.40 cnf(120,plain,
% 40.33/40.40 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[73,91,90,51,74,30,100,98,105,60,62,39,12,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(124,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),a1,a1)),
% 40.33/40.40 inference(scs_inference,[],[73,91,90,51,74,30,100,98,119,105,60,62,39,12,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(127,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[52,2])).
% 40.33/40.40 cnf(128,plain,
% 40.33/40.40 (E(f4(f3(a1),a1),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[52,60,25,2,16])).
% 40.33/40.40 cnf(132,plain,
% 40.33/40.40 (P1(f3(a1),f4(f4(a1,a1),a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[52,110,118,60,25,2,16,9])).
% 40.33/40.40 cnf(133,plain,
% 40.33/40.40 (P1(x1331,f4(f4(a1,a1),a1),f4(x1331,a1))),
% 40.33/40.40 inference(rename_variables,[],[118])).
% 40.33/40.40 cnf(134,plain,
% 40.33/40.40 (E(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[52,110,118,60,25,2,16,9,3])).
% 40.33/40.40 cnf(135,plain,
% 40.33/40.40 (P1(f4(a1,a1),f3(f4(a1,a1)),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[109,52,110,120,118,60,25,2,16,9,3,8])).
% 40.33/40.40 cnf(136,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[109,52,110,120,118,102,60,25,2,16,9,3,8,7])).
% 40.33/40.40 cnf(137,plain,
% 40.33/40.40 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[109,52,110,120,118,133,83,102,60,25,13,2,16,9,3,8,7,17])).
% 40.33/40.40 cnf(142,plain,
% 40.33/40.40 (P1(a2,f3(f4(a1,a1)),f4(a2,a1))),
% 40.33/40.40 inference(scs_inference,[],[109,52,110,120,118,133,83,102,36,60,48,25,13,2,16,9,3,8,7,17,18])).
% 40.33/40.40 cnf(145,plain,
% 40.33/40.40 (E(f4(a1,a1),f4(f3(a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[128,2])).
% 40.33/40.40 cnf(146,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[128,64,118,2,16])).
% 40.33/40.40 cnf(149,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,64,118,2,16,3])).
% 40.33/40.40 cnf(150,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,124,64,118,2,16,3,9])).
% 40.33/40.40 cnf(151,plain,
% 40.33/40.40 (P1(f4(a1,a1),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,73,135,124,64,118,2,16,3,9,8])).
% 40.33/40.40 cnf(152,plain,
% 40.33/40.40 (P1(f4(a2,a1),f3(f4(a1,a1)),f4(a2,a1))),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,73,19,135,124,142,64,118,2,16,3,9,8,7])).
% 40.33/40.40 cnf(154,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),a1,a1)),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,73,19,135,124,142,94,64,118,11,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(155,plain,
% 40.33/40.40 (P1(a1,x1551,x1551)),
% 40.33/40.40 inference(rename_variables,[],[11])).
% 40.33/40.40 cnf(157,plain,
% 40.33/40.40 (P1(f4(f3(a1),a1),a1,a1)),
% 40.33/40.40 inference(scs_inference,[],[128,127,114,73,19,135,124,142,87,94,137,64,118,11,155,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(160,plain,
% 40.33/40.40 (E(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[146,2])).
% 40.33/40.40 cnf(161,plain,
% 40.33/40.40 (E(a1,f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[146,157,22,2,16])).
% 40.33/40.40 cnf(165,plain,
% 40.33/40.40 (E(f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[146,149,145,134,116,157,22,2,16,9,3])).
% 40.33/40.40 cnf(166,plain,
% 40.33/40.40 (P1(f4(a1,a1),f4(f3(a1),a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[146,149,145,134,151,116,157,22,2,16,9,3,8])).
% 40.33/40.40 cnf(167,plain,
% 40.33/40.40 (P1(f4(f3(a1),a1),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[146,149,145,134,151,116,157,22,2,16,9,3,8,7])).
% 40.33/40.40 cnf(168,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[146,149,145,134,151,116,157,22,62,14,2,16,9,3,8,7,17])).
% 40.33/40.40 cnf(170,plain,
% 40.33/40.40 (P1(x1701,x1702,f4(x1701,x1702))),
% 40.33/40.40 inference(rename_variables,[],[14])).
% 40.33/40.40 cnf(172,plain,
% 40.33/40.40 (P1(x1721,a1,f4(x1721,f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[146,149,145,134,151,116,157,22,132,62,39,14,170,2,16,9,3,8,7,17,18])).
% 40.33/40.40 cnf(176,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[165,2])).
% 40.33/40.40 cnf(177,plain,
% 40.33/40.40 (E(f4(f4(x1771,a1),f3(a1)),x1771)),
% 40.33/40.40 inference(scs_inference,[],[165,172,22,2,16])).
% 40.33/40.40 cnf(180,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[165,161,127,172,22,2,16,3])).
% 40.33/40.40 cnf(181,plain,
% 40.33/40.40 (P1(f4(a2,a1),f3(f4(a1,a1)),a2)),
% 40.33/40.40 inference(scs_inference,[],[165,161,127,30,152,172,22,2,16,3,9])).
% 40.33/40.40 cnf(183,plain,
% 40.33/40.40 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[165,161,127,30,152,166,172,22,2,16,3,9,8])).
% 40.33/40.40 cnf(184,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[165,161,91,127,30,168,152,166,172,22,2,16,3,9,8,7])).
% 40.33/40.40 cnf(185,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[165,161,91,127,30,168,152,166,172,22,48,14,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(189,plain,
% 40.33/40.40 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[165,161,91,127,30,168,152,166,167,172,22,48,14,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(191,plain,
% 40.33/40.40 (E(x1911,f4(f4(x1911,a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[177,2])).
% 40.33/40.40 cnf(192,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[177,184,26,2,16])).
% 40.33/40.40 cnf(193,plain,
% 40.33/40.40 (P1(x1931,f4(a1,a1),x1931)),
% 40.33/40.40 inference(rename_variables,[],[26])).
% 40.33/40.40 cnf(195,plain,
% 40.33/40.40 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f3(a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[176,177,189,184,26,2,16,9])).
% 40.33/40.40 cnf(198,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[15,176,177,90,189,184,136,26,2,16,9,3,8])).
% 40.33/40.40 cnf(199,plain,
% 40.33/40.40 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[15,176,177,180,90,189,184,136,26,2,16,9,3,8,7])).
% 40.33/40.40 cnf(200,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[15,176,177,180,90,189,184,136,81,26,193,2,16,9,3,8,7,18])).
% 40.33/40.40 cnf(201,plain,
% 40.33/40.40 (P1(x2011,f4(a1,a1),x2011)),
% 40.33/40.40 inference(rename_variables,[],[26])).
% 40.33/40.40 cnf(203,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),f4(a1,a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[15,176,177,180,90,189,184,136,81,26,193,201,12,2,16,9,3,8,7,18,17])).
% 40.33/40.40 cnf(207,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[134,2])).
% 40.33/40.40 cnf(208,plain,
% 40.33/40.40 (E(a1,f4(f4(f4(a1,a1),a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[134,154,172,2,16])).
% 40.33/40.40 cnf(209,plain,
% 40.33/40.40 (P1(x2091,a1,f4(x2091,f3(a1)))),
% 40.33/40.40 inference(rename_variables,[],[172])).
% 40.33/40.40 cnf(211,plain,
% 40.33/40.40 (E(f4(a1,a1),f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[160,134,180,154,172,2,16,3])).
% 40.33/40.40 cnf(212,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),a1,f4(f4(a1,a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[160,191,134,180,154,172,2,16,3,9])).
% 40.33/40.40 cnf(213,plain,
% 40.33/40.40 (E(x2131,f4(f4(x2131,a1),f3(a1)))),
% 40.33/40.40 inference(rename_variables,[],[191])).
% 40.33/40.40 cnf(214,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[160,191,213,134,180,154,172,2,16,3,9,8])).
% 40.33/40.40 cnf(216,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[160,192,191,213,134,180,154,203,172,2,16,3,9,8,7])).
% 40.33/40.40 cnf(217,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[160,192,191,213,134,180,183,154,203,172,209,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(220,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),f3(f4(a1,a1)),a1)),
% 40.33/40.40 inference(scs_inference,[],[160,192,191,213,134,180,183,185,154,203,200,172,209,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(222,plain,
% 40.33/40.40 (E(f3(a1),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[211,2])).
% 40.33/40.40 cnf(223,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[211,212,22,2,16])).
% 40.33/40.40 cnf(226,plain,
% 40.33/40.40 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[211,192,150,212,22,2,16,9])).
% 40.33/40.40 cnf(227,plain,
% 40.33/40.40 (E(f3(f4(a1,a1)),f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[211,192,32,161,150,212,22,2,16,9,3])).
% 40.33/40.40 cnf(228,plain,
% 40.33/40.40 (P1(f3(a1),f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[211,192,32,161,150,199,212,22,2,16,9,3,8])).
% 40.33/40.40 cnf(229,plain,
% 40.33/40.40 (P1(f3(a1),f3(f4(a1,a1)),f4(f3(a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[211,192,32,161,195,150,199,212,22,2,16,9,3,8,7])).
% 40.33/40.40 cnf(230,plain,
% 40.33/40.40 (P1(f3(a1),f4(f3(a1),a1),a1)),
% 40.33/40.40 inference(scs_inference,[],[211,192,32,161,195,220,150,199,212,22,2,16,9,3,8,7,18])).
% 40.33/40.40 cnf(232,plain,
% 40.33/40.40 (P1(f4(f3(a1),a1),a1,f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[211,192,32,161,195,220,150,199,212,118,22,2,16,9,3,8,7,18,17])).
% 40.33/40.40 cnf(235,plain,
% 40.33/40.40 (E(f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[223,2])).
% 40.33/40.40 cnf(236,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),a1),f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[223,232,22,2,16])).
% 40.33/40.40 cnf(239,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.40 inference(scs_inference,[],[223,160,232,22,2,16,3])).
% 40.33/40.40 cnf(240,plain,
% 40.33/40.40 (P1(f3(a1),f3(f4(a1,a1)),f4(a1,a1))),
% 40.33/40.40 inference(scs_inference,[],[223,160,128,232,229,22,2,16,3,9])).
% 40.33/40.40 cnf(242,plain,
% 40.33/40.40 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.40 inference(scs_inference,[],[223,222,227,160,128,232,229,228,22,2,16,3,9,8,7])).
% 40.33/40.40 cnf(243,plain,
% 40.33/40.40 (P1(f4(f4(a1,a1),a1),f3(f4(a1,a1)),f3(a1))),
% 40.33/40.40 inference(scs_inference,[],[223,222,227,160,128,232,229,228,98,94,22,2,16,3,9,8,7,17])).
% 40.33/40.40 cnf(246,plain,
% 40.33/40.40 (P1(f3(a1),f4(f4(a1,a1),a1),f4(a1,f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[223,222,227,160,128,232,229,228,230,98,94,172,22,2,16,3,9,8,7,17,18])).
% 40.33/40.40 cnf(249,plain,
% 40.33/40.40 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.40 inference(scs_inference,[],[239,2])).
% 40.33/40.40 cnf(250,plain,
% 40.33/40.40 (E(f4(a1,f3(a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[239,246,39,2,16])).
% 40.33/40.41 cnf(253,plain,
% 40.33/40.41 (P1(f4(a1,a1),f3(a1),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[239,236,246,242,39,2,16,9])).
% 40.33/40.41 cnf(254,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f3(a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[239,207,236,246,242,39,2,16,9,3])).
% 40.33/40.41 cnf(256,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[239,235,207,236,246,242,39,2,16,9,3,8,7])).
% 40.33/40.41 cnf(257,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[239,235,207,236,246,242,98,39,2,16,9,3,8,7,18])).
% 40.33/40.41 cnf(258,plain,
% 40.33/40.41 (P1(f4(x2581,a1),f4(f4(a1,a1),a1),x2581)),
% 40.33/40.41 inference(rename_variables,[],[98])).
% 40.33/40.41 cnf(260,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),a1),f3(a1),a1)),
% 40.33/40.41 inference(scs_inference,[],[239,235,207,236,246,242,228,98,258,39,2,16,9,3,8,7,18,17])).
% 40.33/40.41 cnf(263,plain,
% 40.33/40.41 (E(f4(f3(a1),a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[254,2])).
% 40.33/40.41 cnf(264,plain,
% 40.33/40.41 (E(f4(a1,a1),f4(f4(f4(a1,a1),f4(a1,a1)),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[254,115,172,2,16])).
% 40.33/40.41 cnf(267,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[254,250,222,115,172,2,16,3])).
% 40.33/40.41 cnf(268,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(a1,f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[254,250,235,222,257,115,172,2,16,3,9])).
% 40.33/40.41 cnf(269,plain,
% 40.33/40.41 (P1(f4(a1,a1),f3(a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[254,250,235,222,257,115,172,2,16,3,9,8])).
% 40.33/40.41 cnf(270,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[254,250,235,222,257,115,172,2,16,3,9,8,7])).
% 40.33/40.41 cnf(271,plain,
% 40.33/40.41 (P1(a1,f4(a1,f3(a1)),a1)),
% 40.33/40.41 inference(scs_inference,[],[254,250,235,222,257,216,115,172,2,16,3,9,8,7,17])).
% 40.33/40.41 cnf(273,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[254,250,235,222,257,260,216,115,198,60,172,2,16,3,9,8,7,17,18])).
% 40.33/40.41 cnf(276,plain,
% 40.33/40.41 (E(f4(a1,a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[267,2])).
% 40.33/40.41 cnf(277,plain,
% 40.33/40.41 (E(a1,f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[267,271,11,2,16])).
% 40.33/40.41 cnf(280,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(a1,f3(a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[267,254,268,271,11,2,16,9])).
% 40.33/40.41 cnf(281,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[267,254,160,268,271,11,2,16,9,3])).
% 40.33/40.41 cnf(282,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[267,254,160,270,268,271,11,2,16,9,3,8])).
% 40.33/40.41 cnf(283,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[267,254,160,270,268,271,11,2,16,9,3,8,7])).
% 40.33/40.41 cnf(286,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f3(a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[267,254,160,270,268,269,243,271,102,185,198,11,2,16,9,3,8,7,18,17])).
% 40.33/40.41 cnf(288,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[281,2])).
% 40.33/40.41 cnf(289,plain,
% 40.33/40.41 (E(x2891,f4(f4(x2891,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[281,83,48,2,16])).
% 40.33/40.41 cnf(292,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[249,281,83,48,2,16,3])).
% 40.33/40.41 cnf(293,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[249,276,281,282,83,48,2,16,3,9])).
% 40.33/40.41 cnf(294,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[249,276,281,282,283,83,48,2,16,3,9,8])).
% 40.33/40.41 cnf(296,plain,
% 40.33/40.41 (P1(a2,f3(a1),a2)),
% 40.33/40.41 inference(scs_inference,[],[249,276,281,282,283,286,273,181,83,48,2,16,3,9,8,7,17])).
% 40.33/40.41 cnf(298,plain,
% 40.33/40.41 (P1(f3(a1),f4(a1,a1),a1)),
% 40.33/40.41 inference(scs_inference,[],[249,276,281,282,283,286,273,181,83,230,271,48,2,16,3,9,8,7,17,18])).
% 40.33/40.41 cnf(300,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f3(a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[292,2])).
% 40.33/40.41 cnf(302,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[288,292,192,226,2,9,3])).
% 40.33/40.41 cnf(303,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[288,292,192,280,226,2,9,3,8])).
% 40.33/40.41 cnf(304,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[288,263,292,192,294,280,226,2,9,3,8,7])).
% 40.33/40.41 cnf(305,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),a1),f4(a1,f3(a1)),a1)),
% 40.33/40.41 inference(scs_inference,[],[288,263,292,192,294,293,280,226,214,26,2,9,3,8,7,18])).
% 40.33/40.41 cnf(308,plain,
% 40.33/40.41 (P1(f4(a1,f3(a1)),f3(a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[288,263,292,192,294,293,280,226,214,269,26,2,9,3,8,7,18,17])).
% 40.33/40.41 cnf(310,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[302,2])).
% 40.33/40.41 cnf(311,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f3(a1)),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[302,217,10,2,16])).
% 40.33/40.41 cnf(314,plain,
% 40.33/40.41 (E(f4(f3(a1),a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[302,300,263,217,10,2,16,3])).
% 40.33/40.41 cnf(317,plain,
% 40.33/40.41 (P1(f4(a1,f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[302,300,264,263,304,298,256,217,10,2,16,3,9,8,7])).
% 40.33/40.41 cnf(318,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[302,300,264,263,304,308,298,256,217,268,10,2,16,3,9,8,7,17])).
% 40.33/40.41 cnf(320,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),a1),f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[302,300,264,263,304,308,298,256,217,305,268,25,10,2,16,3,9,8,7,17,18])).
% 40.33/40.41 cnf(323,plain,
% 40.33/40.41 (E(f3(f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,2])).
% 40.33/40.41 cnf(324,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,314,303,2,9])).
% 40.33/40.41 cnf(325,plain,
% 40.33/40.41 (E(f3(f4(a1,a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,314,277,32,303,2,9,3])).
% 40.33/40.41 cnf(326,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[311,314,289,277,32,303,116,2,9,3,8])).
% 40.33/40.41 cnf(328,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,314,289,277,32,303,318,116,2,9,3,8,7])).
% 40.33/40.41 cnf(329,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f3(a1),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[311,314,289,277,32,303,318,116,2,9,3,8,7,17])).
% 40.33/40.41 cnf(331,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[311,314,289,277,32,303,318,253,282,116,2,9,3,8,7,17,18])).
% 40.33/40.41 cnf(333,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[325,2])).
% 40.33/40.41 cnf(334,plain,
% 40.33/40.41 (E(f3(f4(a1,a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[325,207,91,2,3])).
% 40.33/40.41 cnf(335,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[310,325,207,91,324,2,3,9])).
% 40.33/40.41 cnf(336,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f4(f3(a1),a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[310,325,207,176,91,326,324,2,3,9,8])).
% 40.33/40.41 cnf(337,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[323,310,325,207,176,91,326,324,2,3,9,8,7])).
% 40.33/40.41 cnf(338,plain,
% 40.33/40.41 (P1(f3(a1),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[323,310,325,207,176,91,326,324,240,183,2,3,9,8,7,18])).
% 40.33/40.41 cnf(340,plain,
% 40.33/40.41 (P1(f4(a2,a1),f3(a1),f4(a2,a1))),
% 40.33/40.41 inference(scs_inference,[],[323,310,325,207,176,91,326,324,240,286,152,183,2,3,9,8,7,18,17])).
% 40.33/40.41 cnf(342,plain,
% 40.33/40.41 (E(f4(f3(a1),a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[334,2])).
% 40.33/40.41 cnf(344,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[334,333,314,329,2,9,3])).
% 40.33/40.41 cnf(345,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f4(a1,f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[334,333,314,336,329,2,9,3,8])).
% 40.33/40.41 cnf(346,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f4(f3(a1),a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[334,333,314,336,329,2,9,3,8,7])).
% 40.33/40.41 cnf(347,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[334,333,314,336,335,329,318,2,9,3,8,7,17])).
% 40.33/40.41 cnf(349,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[334,333,314,336,337,335,320,329,280,318,2,9,3,8,7,17,18])).
% 40.33/40.41 cnf(351,plain,
% 40.33/40.41 (E(f4(f4(f4(a1,a1),a1),f3(a1)),a1)),
% 40.33/40.41 inference(scs_inference,[],[208,2])).
% 40.33/40.41 cnf(352,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[208,149,239,2,3])).
% 40.33/40.41 cnf(353,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[342,208,149,239,349,2,3,9])).
% 40.33/40.41 cnf(354,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[342,208,149,239,346,349,2,3,9,8])).
% 40.33/40.41 cnf(359,plain,
% 40.33/40.41 (P1(f3(a1),f3(a1),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[342,208,149,191,239,346,349,340,335,203,243,286,2,3,9,8,7,18,17])).
% 40.33/40.41 cnf(361,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[352,2])).
% 40.33/40.41 cnf(362,plain,
% 40.33/40.41 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[352,323,338,2,9])).
% 40.33/40.41 cnf(363,plain,
% 40.33/40.41 (E(f4(f4(f4(a1,a1),a1),f3(a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[352,351,323,161,338,2,9,3])).
% 40.33/40.41 cnf(364,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[352,351,323,161,354,338,2,9,3,8])).
% 40.33/40.41 cnf(366,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[352,351,323,161,354,347,331,338,64,2,9,3,8,7,17])).
% 40.33/40.41 cnf(368,plain,
% 40.33/40.41 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[352,351,323,161,354,353,347,331,338,324,64,26,2,9,3,8,7,17,18])).
% 40.33/40.41 cnf(371,plain,
% 40.33/40.41 (E(f3(a1),f4(f4(f4(a1,a1),a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[363,2])).
% 40.33/40.41 cnf(375,plain,
% 40.33/40.41 (P1(a2,f3(a1),f4(f4(a2,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[363,289,368,296,12,2,16,9])).
% 40.33/40.41 cnf(379,plain,
% 40.33/40.41 (P1(f4(a1,f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[363,227,289,368,317,345,296,366,253,12,2,16,9,8,7,18])).
% 40.33/40.41 cnf(381,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[363,227,289,364,368,317,345,296,366,337,253,41,12,2,16,9,8,7,18,17])).
% 40.33/40.41 cnf(384,plain,
% 40.33/40.41 (E(f4(f4(f4(a1,a1),f4(a1,a1)),f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[264,2])).
% 40.33/40.41 cnf(385,plain,
% 40.33/40.41 (E(f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[264,381,118,2,16])).
% 40.33/40.41 cnf(388,plain,
% 40.33/40.41 (E(f3(a1),a1)),
% 40.33/40.41 inference(scs_inference,[],[371,264,351,381,118,2,16,3])).
% 40.33/40.41 cnf(394,plain,
% 40.33/40.41 (P1(f3(a1),f3(a1),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[371,264,351,359,381,362,375,337,118,2,16,3,9,8,7,17,18])).
% 40.33/40.41 cnf(396,plain,
% 40.33/40.41 (E(f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[180,2])).
% 40.33/40.41 cnf(397,plain,
% 40.33/40.41 (E(f4(a1,a1),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[180,394,14,2,16])).
% 40.33/40.41 cnf(400,plain,
% 40.33/40.41 (E(f3(a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[361,385,180,394,14,2,16,3])).
% 40.33/40.41 cnf(401,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f3(a1),f4(f4(a1,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[361,385,352,180,394,328,14,2,16,3,9])).
% 40.33/40.41 cnf(408,plain,
% 40.33/40.41 (E(f4(f3(a1),f3(a1)),f4(a1,a1))),
% 40.33/40.41 inference(scs_inference,[],[397,2])).
% 40.33/40.41 cnf(409,plain,
% 40.33/40.41 (E(f3(a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[397,379,48,2,16])).
% 40.33/40.41 cnf(412,plain,
% 40.33/40.41 (E(f3(a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[397,396,109,379,48,2,16,3])).
% 40.33/40.41 cnf(421,plain,
% 40.33/40.41 (E(f4(f4(a1,a1),f3(a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[400,2])).
% 40.33/40.41 cnf(422,plain,
% 40.33/40.41 (E(f4(f4(f4(a1,a1),f4(a1,a1)),f3(a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[384,400,211,2,3])).
% 40.33/40.41 cnf(430,plain,
% 40.33/40.41 (E(f3(a1),f4(f4(f4(a1,a1),f4(a1,a1)),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[422,2])).
% 40.33/40.41 cnf(431,plain,
% 40.33/40.41 (E(f4(f3(a1),f3(a1)),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[408,422,276,2,3])).
% 40.33/40.41 cnf(439,plain,
% 40.33/40.41 (E(f4(a1,f3(a1)),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[431,2])).
% 40.33/40.41 cnf(440,plain,
% 40.33/40.41 (E(f3(a1),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[409,431,2,3])).
% 40.33/40.41 cnf(451,plain,
% 40.33/40.41 (E(x4511,f4(x4511,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[440,10,172,2,16])).
% 40.33/40.41 cnf(454,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),f4(a1,a1),a1)),
% 40.33/40.41 inference(scs_inference,[],[388,440,41,10,172,2,16,9])).
% 40.33/40.41 cnf(455,plain,
% 40.33/40.41 (P1(f4(x4551,a1),f4(a1,a1),x4551)),
% 40.33/40.41 inference(rename_variables,[],[41])).
% 40.33/40.41 cnf(456,plain,
% 40.33/40.41 (E(a1,f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[388,439,440,277,41,10,172,2,16,9,3])).
% 40.33/40.41 cnf(459,plain,
% 40.33/40.41 (P1(f4(x4591,a1),f4(f4(a1,a1),f4(a1,a1)),x4591)),
% 40.33/40.41 inference(rename_variables,[],[58])).
% 40.33/40.41 cnf(460,plain,
% 40.33/40.41 (P1(x4601,f4(a1,a1),f4(x4601,a1))),
% 40.33/40.41 inference(scs_inference,[],[388,439,440,277,263,264,58,459,41,455,39,10,184,172,2,16,9,3,8,7,17])).
% 40.33/40.41 cnf(465,plain,
% 40.33/40.41 (E(f4(x4651,f3(a1)),x4651)),
% 40.33/40.41 inference(scs_inference,[],[451,2])).
% 40.33/40.41 cnf(466,plain,
% 40.33/40.41 (E(a1,f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[451,344,2,3])).
% 40.33/40.41 cnf(467,plain,
% 40.33/40.41 (E(x4671,f4(x4671,f3(a1)))),
% 40.33/40.41 inference(rename_variables,[],[451])).
% 40.33/40.41 cnf(469,plain,
% 40.33/40.41 (E(x4691,f4(x4691,f3(a1)))),
% 40.33/40.41 inference(rename_variables,[],[451])).
% 40.33/40.41 cnf(471,plain,
% 40.33/40.41 (E(x4711,f4(x4711,f3(a1)))),
% 40.33/40.41 inference(rename_variables,[],[451])).
% 40.33/40.41 cnf(472,plain,
% 40.33/40.41 (P1(f4(f4(x4721,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),x4721)),
% 40.33/40.41 inference(scs_inference,[],[451,467,469,471,344,58,98,25,2,3,9,8,7])).
% 40.33/40.41 cnf(482,plain,
% 40.33/40.41 (E(f4(f3(a1),f3(a1)),a1)),
% 40.33/40.41 inference(scs_inference,[],[456,2])).
% 40.33/40.41 cnf(485,plain,
% 40.33/40.41 (E(f4(f3(a1),f3(a1)),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[412,465,456,22,2,9,3])).
% 40.33/40.41 cnf(489,plain,
% 40.33/40.41 (P1(f4(x4891,a1),f4(f4(a1,a1),f4(a1,a1)),x4891)),
% 40.33/40.41 inference(rename_variables,[],[58])).
% 40.33/40.41 cnf(490,plain,
% 40.33/40.41 (P1(a1,x4901,f4(f4(x4901,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[412,465,456,342,397,58,41,22,11,48,472,2,9,3,8,7,18])).
% 40.33/40.41 cnf(494,plain,
% 40.33/40.41 (P1(x4941,f4(f4(a1,a1),a1),f4(f4(x4941,a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[412,465,456,342,397,58,489,41,22,39,11,48,472,62,2,9,3,8,7,18,17])).
% 40.33/40.41 cnf(498,plain,
% 40.33/40.41 (E(f3(f4(a1,a1)),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[485,2])).
% 40.33/40.41 cnf(499,plain,
% 40.33/40.41 (E(f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 40.33/40.41 inference(scs_inference,[],[485,466,482,2,3])).
% 40.33/40.41 cnf(513,plain,
% 40.33/40.41 (E(f4(f3(a1),a1),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[499,2])).
% 40.33/40.41 cnf(530,plain,
% 40.33/40.41 (E(f4(a1,a1),f4(f4(f3(a1),a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[25,490,16])).
% 40.33/40.41 cnf(532,plain,
% 40.33/40.41 (P1(x5321,f3(x5321),f4(a1,a1))),
% 40.33/40.41 inference(rename_variables,[],[25])).
% 40.33/40.41 cnf(537,plain,
% 40.33/40.41 (P1(x5371,f3(x5371),f4(a1,a1))),
% 40.33/40.41 inference(rename_variables,[],[25])).
% 40.33/40.41 cnf(542,plain,
% 40.33/40.41 (P1(x5421,f3(x5421),f4(a1,a1))),
% 40.33/40.41 inference(rename_variables,[],[25])).
% 40.33/40.41 cnf(544,plain,
% 40.33/40.41 (P1(x5441,f4(f3(x5441),a1),a1)),
% 40.33/40.41 inference(scs_inference,[],[513,498,191,25,532,537,542,58,41,98,460,490,401,16,9,8,7,17,18])).
% 40.33/40.41 cnf(578,plain,
% 40.33/40.41 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[421,530,48,41,10,9,8,7])).
% 40.33/40.41 cnf(591,plain,
% 40.33/40.41 (P1(x5911,f4(a1,a1),x5911)),
% 40.33/40.41 inference(rename_variables,[],[26])).
% 40.33/40.41 cnf(604,plain,
% 40.33/40.41 (E(a1,f4(f4(f4(a1,a1),f4(a1,a1)),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[430,388,422,513,176,58,98,48,26,591,25,11,578,3,9,8,7,17,18,2])).
% 40.33/40.41 cnf(633,plain,
% 40.33/40.41 (P1(x6331,a1,x6331)),
% 40.33/40.41 inference(rename_variables,[],[10])).
% 40.33/40.41 cnf(634,plain,
% 40.33/40.41 (P1(x6341,f4(f3(a1),f3(a1)),x6341)),
% 40.33/40.41 inference(scs_inference,[],[333,456,482,52,10,633,3,9,8])).
% 40.33/40.41 cnf(636,plain,
% 40.33/40.41 (P1(f4(x6361,a1),a1,x6361)),
% 40.33/40.41 inference(rename_variables,[],[22])).
% 40.33/40.41 cnf(637,plain,
% 40.33/40.41 (P1(x6371,f3(f4(x6371,a1)),a1)),
% 40.33/40.41 inference(scs_inference,[],[333,456,482,134,52,22,636,10,633,12,11,3,9,8,7,17])).
% 40.33/40.41 cnf(685,plain,
% 40.33/40.41 (P1(x6851,f4(a1,a1),x6851)),
% 40.33/40.41 inference(rename_variables,[],[26])).
% 40.33/40.41 cnf(687,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(a1,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[310,431,26,685,634,9,8,7])).
% 40.33/40.41 cnf(703,plain,
% 40.33/40.41 (P1(x7031,f4(a1,a1),x7031)),
% 40.33/40.41 inference(rename_variables,[],[26])).
% 40.33/40.41 cnf(705,plain,
% 40.33/40.41 (P1(f4(a1,a1),f4(a1,a1),f4(f3(a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[408,146,26,703,472,9,8,7])).
% 40.33/40.41 cnf(706,plain,
% 40.33/40.41 (P1(x7061,f4(a1,a1),x7061)),
% 40.33/40.41 inference(rename_variables,[],[26])).
% 40.33/40.41 cnf(709,plain,
% 40.33/40.41 (P1(x7091,f4(a1,a1),x7091)),
% 40.33/40.41 inference(rename_variables,[],[26])).
% 40.33/40.41 cnf(710,plain,
% 40.33/40.41 (P1(f4(x7101,a1),f4(f4(a1,a1),f4(a1,a1)),x7101)),
% 40.33/40.41 inference(rename_variables,[],[58])).
% 40.33/40.41 cnf(712,plain,
% 40.33/40.41 (P1(f4(x7121,a1),f4(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),x7121)),
% 40.33/40.41 inference(scs_inference,[],[408,146,58,710,26,703,706,709,472,13,14,9,8,7,17,18])).
% 40.33/40.41 cnf(750,plain,
% 40.33/40.41 (P1(f4(a1,f3(a1)),f4(a1,a1),f3(f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[333,421,465,26,3,9])).
% 40.33/40.41 cnf(816,plain,
% 40.33/40.41 (P1(x8161,f4(f3(a1),a1),f4(x8161,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[466,544,172,9,8])).
% 40.33/40.41 cnf(817,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),x8171,x8171)),
% 40.33/40.41 inference(scs_inference,[],[466,544,172,11,9,8,7])).
% 40.33/40.41 cnf(825,plain,
% 40.33/40.41 (E(f4(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[817,712,16])).
% 40.33/40.41 cnf(827,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),x8271,x8271)),
% 40.33/40.41 inference(rename_variables,[],[817])).
% 40.33/40.41 cnf(834,plain,
% 40.33/40.41 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 40.33/40.41 inference(scs_inference,[],[300,604,58,26,10,472,817,827,816,712,16,9,8,7,17])).
% 40.33/40.41 cnf(841,plain,
% 40.33/40.41 (E(x8411,f4(f4(x8411,a1),a1))),
% 40.33/40.41 inference(rename_variables,[],[289])).
% 40.33/40.41 cnf(842,plain,
% 40.33/40.41 (P1(x8421,f4(f4(a1,a1),a1),f4(x8421,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[289,841,825,637,172,2,9,8])).
% 40.33/40.41 cnf(875,plain,
% 40.33/40.41 (E(f4(x8751,a1),f4(x8751,f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[118,842,16])).
% 40.33/40.41 cnf(890,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,77,875,10,26,494,2,9,8,7])).
% 40.33/40.41 cnf(976,plain,
% 40.33/40.41 (P1(a1,x9761,x9761)),
% 40.33/40.41 inference(rename_variables,[],[11])).
% 40.33/40.41 cnf(977,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),x9771,x9771)),
% 40.33/40.41 inference(scs_inference,[],[91,51,26,11,976,9,8,7])).
% 40.33/40.41 cnf(1003,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),x10031,x10031)),
% 40.33/40.41 inference(scs_inference,[],[323,439,172,11,977,9,8,7])).
% 40.33/40.41 cnf(1007,plain,
% 40.33/40.41 (P1(f4(a1,f3(a1)),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[325,292,11,890,687,9,8,7])).
% 40.33/40.41 cnf(1045,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x10451,x10451)),
% 40.33/40.41 inference(scs_inference,[],[52,56,544,460,11,8,9,7])).
% 40.33/40.41 cnf(1059,plain,
% 40.33/40.41 (P1(x10591,f4(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),x10591)),
% 40.33/40.41 inference(scs_inference,[],[439,160,466,58,637,834,1007,1045,712,8,9,7,17])).
% 40.33/40.41 cnf(1064,plain,
% 40.33/40.41 (E(x10641,f4(x10641,f3(a1)))),
% 40.33/40.41 inference(rename_variables,[],[451])).
% 40.33/40.41 cnf(1068,plain,
% 40.33/40.41 (P1(x10681,f4(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1)),f4(x10681,a1))),
% 40.33/40.41 inference(scs_inference,[],[73,451,1064,58,454,1059,750,705,1045,8,9,7,17])).
% 40.33/40.41 cnf(1103,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f3(a1)),x11031,f4(f4(x11031,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[177,1003,8])).
% 40.33/40.41 cnf(1105,plain,
% 40.33/40.41 (P1(a1,f4(f4(x11051,a1),f3(a1)),x11051)),
% 40.33/40.41 inference(scs_inference,[],[177,11,1003,8,9])).
% 40.33/40.41 cnf(1224,plain,
% 40.33/40.41 (E(f4(f4(a1,f3(a1)),f3(a1)),f3(a1))),
% 40.33/40.41 inference(scs_inference,[],[465,250,3])).
% 40.33/40.41 cnf(1231,plain,
% 40.33/40.41 (P1(f3(f4(a1,a1)),x12311,f4(f4(x12311,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[311,1224,1103,2,7])).
% 40.33/40.41 cnf(1238,plain,
% 40.33/40.41 (P1(f4(a1,a1),x12381,f4(f4(x12381,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[73,1231,7])).
% 40.33/40.41 cnf(1327,plain,
% 40.33/40.41 (P1(f4(f3(a1),a1),x13271,f4(f4(x13271,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[110,145,1238,1068,9,7])).
% 40.33/40.41 cnf(1329,plain,
% 40.33/40.41 (P1(f4(f4(a1,a1),f4(a1,a1)),x13291,f4(f4(x13291,a1),f3(a1)))),
% 40.33/40.41 inference(scs_inference,[],[134,1327,7])).
% 40.33/40.41 cnf(1374,plain,
% 40.33/40.41 (E(f4(x13741,f3(a1)),x13741)),
% 40.33/40.41 inference(rename_variables,[],[465])).
% 40.33/40.41 cnf(1377,plain,
% 40.33/40.41 (E(f4(x13771,f3(a1)),x13771)),
% 40.33/40.41 inference(rename_variables,[],[465])).
% 40.33/40.41 cnf(1378,plain,
% 40.33/40.41 (P1(a1,f4(x13781,a1),x13781)),
% 40.33/40.41 inference(scs_inference,[],[465,1374,1377,32,52,1329,1105,3,7,9,8])).
% 40.33/40.41 cnf(1486,plain,
% 40.33/40.41 (~P1(a2,a1,f3(f3(a2)))),
% 40.33/40.41 inference(scs_inference,[],[10,15,16])).
% 40.33/40.41 cnf(1748,plain,
% 40.33/40.41 ($false),
% 40.33/40.41 inference(scs_inference,[],[12,1486,460,544,25,1378,17,18]),
% 40.33/40.41 ['proof']).
% 40.33/40.41 % SZS output end Proof
% 40.33/40.41 % Total time :39.770000s
%------------------------------------------------------------------------------