%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP020-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.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:29 EDT 2024
% Result : Unsatisfiable 2.33s 2.41s
% Output : CNFRefutation 2.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : GRP020-1 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.08 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.26 % Computer : n020.cluster.edu
% 0.08/0.26 % Model : x86_64 x86_64
% 0.08/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.26 % Memory : 8042.1875MB
% 0.08/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.26 % CPULimit : 300
% 0.08/0.26 % WCLimit : 300
% 0.08/0.26 % DateTime : Thu Jun 20 10:17:08 EDT 2024
% 0.08/0.27 % CPUTime :
% 0.12/0.42 start to proof:theBenchmark
% 2.31/2.40 %-------------------------------------------
% 2.31/2.40 % File :CSE---1.7
% 2.31/2.40 % Problem :theBenchmark
% 2.31/2.40 % Transform :cnf
% 2.31/2.40 % Format :tptp:raw
% 2.31/2.40 % Command :java -jar mcs_scs.jar %d %s
% 2.31/2.40
% 2.31/2.40 % Result :Theorem 1.950000s
% 2.31/2.40 % Output :CNFRefutation 1.950000s
% 2.31/2.40 %-------------------------------------------
% 2.33/2.41 %--------------------------------------------------------------------------
% 2.33/2.41 % File : GRP020-1 : TPTP v8.2.0. Released v1.0.0.
% 2.33/2.41 % Domain : Group Theory
% 2.33/2.41 % Problem : Inverse of X times X is the identity
% 2.33/2.41 % Version : [MOW76] axioms.
% 2.33/2.41 % English :
% 2.33/2.41
% 2.33/2.41 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 2.33/2.41 % : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
% 2.33/2.41 % Source : [MOW76]
% 2.33/2.41 % Names : Identity established [MOW76]
% 2.33/2.41 % : Lemma proved [OMW76]
% 2.33/2.41
% 2.33/2.41 % Status : Unsatisfiable
% 2.33/2.41 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v2.0.0
% 2.33/2.41 % Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 4 RR)
% 2.33/2.41 % Number of literals : 17 ( 2 equ; 9 neg)
% 2.33/2.41 % Maximal clause size : 4 ( 1 avg)
% 2.33/2.41 % Maximal term depth : 3 ( 1 avg)
% 2.33/2.41 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 2.33/2.41 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 2.33/2.41 % Number of variables : 22 ( 0 sgn)
% 2.33/2.41 % SPC : CNF_UNS_RFO_SEQ_HRN
% 2.33/2.41
% 2.33/2.41 % Comments :
% 2.33/2.41 %--------------------------------------------------------------------------
% 2.33/2.41 %----Include group theory axioms
% 2.33/2.41 include('Axioms/GRP003-0.ax').
% 2.33/2.41 %--------------------------------------------------------------------------
% 2.33/2.41 cnf(prove_inverse_X_times_X_is_id,negated_conjecture,
% 2.33/2.41 multiply(inverse(a),a) != identity ).
% 2.33/2.41
% 2.33/2.41 %--------------------------------------------------------------------------
% 2.33/2.41 %-------------------------------------------
% 2.33/2.41 % Proof found
% 2.33/2.41 % SZS status Theorem for theBenchmark
% 2.33/2.41 % SZS output start Proof
% 2.33/2.41 %ClaNum:18(EqnAxiom:9)
% 2.33/2.41 %VarNum:44(SingletonVarNum:22)
% 2.33/2.41 %MaxLitNum:4
% 2.33/2.41 %MaxfuncDepth:2
% 2.33/2.41 %SharedTerms:5
% 2.33/2.41 %goalClause: 15
% 2.33/2.41 %singleGoalClaCount:1
% 2.33/2.41 [15]~E(f4(f3(a2),a2),a1)
% 2.33/2.41 [10]P1(x101,a1,x101)
% 2.33/2.41 [11]P1(a1,x111,x111)
% 2.33/2.41 [12]P1(x121,f3(x121),a1)
% 2.33/2.41 [13]P1(f3(x131),x131,a1)
% 2.33/2.41 [14]P1(x141,x142,f4(x141,x142))
% 2.33/2.41 [16]~P1(x163,x164,x161)+E(x161,x162)+~P1(x163,x164,x162)
% 2.33/2.41 [17]~P1(x176,x174,x171)+P1(x171,x172,x173)+~P1(x174,x172,x175)+~P1(x176,x175,x173)
% 2.33/2.41 [18]~P1(x181,x186,x184)+P1(x181,x182,x183)+~P1(x184,x185,x183)+~P1(x186,x185,x182)
% 2.33/2.41 %EqnAxiom
% 2.33/2.41 [1]E(x11,x11)
% 2.33/2.41 [2]E(x22,x21)+~E(x21,x22)
% 2.33/2.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.33/2.41 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 2.33/2.41 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 2.33/2.41 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 2.33/2.41 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 2.33/2.41 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 2.33/2.41 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 2.33/2.41
% 2.33/2.41 %-------------------------------------------
% 2.34/2.42 cnf(19,plain,
% 2.34/2.42 (E(x191,f4(x191,a1))),
% 2.34/2.42 inference(scs_inference,[],[10,14,16])).
% 2.34/2.42 cnf(20,plain,
% 2.34/2.42 (P1(x201,x202,f4(x201,x202))),
% 2.34/2.42 inference(rename_variables,[],[14])).
% 2.34/2.42 cnf(22,plain,
% 2.34/2.42 (P1(f4(x221,a1),a1,x221)),
% 2.34/2.42 inference(scs_inference,[],[10,14,16,7])).
% 2.34/2.42 cnf(24,plain,
% 2.34/2.42 (P1(x241,a1,x241)),
% 2.34/2.42 inference(rename_variables,[],[10])).
% 2.34/2.42 cnf(25,plain,
% 2.34/2.42 (P1(x251,f3(x251),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[10,14,12,16,7,8,9])).
% 2.34/2.42 cnf(26,plain,
% 2.34/2.42 (P1(x261,f4(a1,a1),x261)),
% 2.34/2.42 inference(scs_inference,[],[10,24,14,20,12,16,7,8,9,18])).
% 2.34/2.42 cnf(30,plain,
% 2.34/2.42 (~E(f4(f3(a2),a2),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[15,10,24,14,20,12,16,7,8,9,18,2,3])).
% 2.34/2.42 cnf(31,plain,
% 2.34/2.42 (E(f4(x311,a1),x311)),
% 2.34/2.42 inference(scs_inference,[],[19,2])).
% 2.34/2.42 cnf(32,plain,
% 2.34/2.42 (E(f3(f4(a1,a1)),a1)),
% 2.34/2.42 inference(scs_inference,[],[19,26,13,2,16])).
% 2.34/2.42 cnf(34,plain,
% 2.34/2.42 (P1(x341,f4(a1,a1),x341)),
% 2.34/2.42 inference(rename_variables,[],[26])).
% 2.34/2.42 cnf(36,plain,
% 2.34/2.42 (P1(x361,f4(a1,a1),f4(x361,a1))),
% 2.34/2.42 inference(scs_inference,[],[19,26,34,13,2,16,9])).
% 2.34/2.42 cnf(37,plain,
% 2.34/2.42 (P1(x371,f4(a1,a1),x371)),
% 2.34/2.42 inference(rename_variables,[],[26])).
% 2.34/2.42 cnf(38,plain,
% 2.34/2.42 (P1(x381,f4(f4(a1,a1),a1),x381)),
% 2.34/2.42 inference(scs_inference,[],[19,26,34,37,13,2,16,9,8])).
% 2.34/2.42 cnf(39,plain,
% 2.34/2.42 (E(x391,f4(x391,a1))),
% 2.34/2.42 inference(rename_variables,[],[19])).
% 2.34/2.42 cnf(41,plain,
% 2.34/2.42 (P1(f4(x411,a1),f4(a1,a1),x411)),
% 2.34/2.42 inference(scs_inference,[],[19,39,26,34,37,30,13,2,16,9,8,3,7])).
% 2.34/2.42 cnf(42,plain,
% 2.34/2.42 (P1(x421,f4(a1,a1),x421)),
% 2.34/2.42 inference(rename_variables,[],[26])).
% 2.34/2.42 cnf(43,plain,
% 2.34/2.42 (P1(a1,f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[19,39,26,34,37,42,25,30,11,13,2,16,9,8,3,7,17])).
% 2.34/2.42 cnf(45,plain,
% 2.34/2.42 (P1(x451,f4(a1,a1),x451)),
% 2.34/2.42 inference(rename_variables,[],[26])).
% 2.34/2.42 cnf(48,plain,
% 2.34/2.42 (P1(x481,f4(f4(a1,a1),f4(a1,a1)),x481)),
% 2.34/2.42 inference(scs_inference,[],[19,39,26,34,37,42,45,25,30,11,13,14,2,16,9,8,3,7,17,18])).
% 2.34/2.42 cnf(51,plain,
% 2.34/2.42 (E(a1,f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[32,2])).
% 2.34/2.42 cnf(52,plain,
% 2.34/2.42 (E(f4(f4(x521,a1),a1),x521)),
% 2.34/2.42 inference(scs_inference,[],[32,36,41,2,16])).
% 2.34/2.42 cnf(55,plain,
% 2.34/2.42 (P1(a1,x551,f4(x551,a1))),
% 2.34/2.42 inference(scs_inference,[],[31,32,36,41,11,2,16,8])).
% 2.34/2.42 cnf(56,plain,
% 2.34/2.42 (P1(a1,x561,x561)),
% 2.34/2.42 inference(rename_variables,[],[11])).
% 2.34/2.42 cnf(57,plain,
% 2.34/2.42 (P1(f4(x571,a1),f4(f4(a1,a1),f4(a1,a1)),x571)),
% 2.34/2.42 inference(scs_inference,[],[31,32,48,36,41,11,2,16,8,9])).
% 2.34/2.42 cnf(58,plain,
% 2.34/2.42 (P1(x581,f4(f4(a1,a1),f4(a1,a1)),x581)),
% 2.34/2.42 inference(rename_variables,[],[48])).
% 2.34/2.42 cnf(59,plain,
% 2.34/2.42 (P1(x591,f4(f4(a1,a1),f4(a1,a1)),f4(x591,a1))),
% 2.34/2.42 inference(scs_inference,[],[31,32,48,58,36,41,11,2,16,8,9,7])).
% 2.34/2.42 cnf(60,plain,
% 2.34/2.42 (P1(x601,f4(f4(a1,a1),f4(a1,a1)),x601)),
% 2.34/2.42 inference(rename_variables,[],[48])).
% 2.34/2.42 cnf(61,plain,
% 2.34/2.42 (~E(f4(f3(a2),a2),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[15,31,32,48,58,36,41,11,2,16,8,9,7,3])).
% 2.34/2.42 cnf(62,plain,
% 2.34/2.42 (P1(a1,f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[15,31,32,48,58,60,38,36,41,11,56,2,16,8,9,7,3,17])).
% 2.34/2.42 cnf(64,plain,
% 2.34/2.42 (P1(x641,f4(f4(a1,a1),f4(a1,a1)),x641)),
% 2.34/2.42 inference(rename_variables,[],[48])).
% 2.34/2.42 cnf(67,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[15,31,32,48,58,60,64,38,36,41,25,11,56,2,16,8,9,7,3,17,18])).
% 2.34/2.42 cnf(71,plain,
% 2.34/2.42 (E(x711,f4(f4(x711,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[52,2])).
% 2.34/2.42 cnf(72,plain,
% 2.34/2.42 (E(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[52,67,26,2,16])).
% 2.34/2.42 cnf(75,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[52,19,67,26,2,16,9])).
% 2.34/2.42 cnf(76,plain,
% 2.34/2.42 (E(x761,f4(x761,a1))),
% 2.34/2.42 inference(rename_variables,[],[19])).
% 2.34/2.42 cnf(77,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[52,19,76,67,26,2,16,9,8])).
% 2.34/2.42 cnf(79,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[52,51,19,76,67,43,26,2,16,9,8,7])).
% 2.34/2.42 cnf(80,plain,
% 2.34/2.42 (P1(f4(f4(x801,a1),a1),f4(f4(a1,a1),f4(a1,a1)),x801)),
% 2.34/2.42 inference(scs_inference,[],[52,51,19,76,67,59,57,43,48,26,2,16,9,8,7,17])).
% 2.34/2.42 cnf(84,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,a1)),
% 2.34/2.42 inference(scs_inference,[],[52,51,19,76,67,59,57,43,48,26,2,16,9,8,7,17,18])).
% 2.34/2.42 cnf(87,plain,
% 2.34/2.42 (E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[72,2])).
% 2.34/2.42 cnf(88,plain,
% 2.34/2.42 (E(f4(f3(a1),a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[72,55,12,2,16])).
% 2.34/2.42 cnf(90,plain,
% 2.34/2.42 (P1(a1,x901,f4(x901,a1))),
% 2.34/2.42 inference(rename_variables,[],[55])).
% 2.34/2.42 cnf(92,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[72,71,84,55,12,2,16,9])).
% 2.34/2.42 cnf(93,plain,
% 2.34/2.42 (E(x931,f4(f4(x931,a1),a1))),
% 2.34/2.42 inference(rename_variables,[],[71])).
% 2.34/2.42 cnf(94,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[72,71,93,84,55,12,2,16,9,8])).
% 2.34/2.42 cnf(95,plain,
% 2.34/2.42 (E(x951,f4(f4(x951,a1),a1))),
% 2.34/2.42 inference(rename_variables,[],[71])).
% 2.34/2.42 cnf(97,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),x971,f4(x971,a1))),
% 2.34/2.42 inference(scs_inference,[],[72,71,93,95,84,55,90,30,12,2,16,9,8,3,7])).
% 2.34/2.42 cnf(99,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[72,71,93,95,80,84,62,55,90,30,12,2,16,9,8,3,7,17])).
% 2.34/2.42 cnf(103,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[72,71,93,95,79,80,84,62,55,90,30,36,12,13,2,16,9,8,3,7,17,18])).
% 2.34/2.42 cnf(107,plain,
% 2.34/2.42 (E(a1,f4(f3(a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[88,2])).
% 2.34/2.42 cnf(108,plain,
% 2.34/2.42 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[88,75,26,2,16])).
% 2.34/2.42 cnf(112,plain,
% 2.34/2.42 (E(f4(f4(x1121,a1),a1),x1121)),
% 2.34/2.42 inference(rename_variables,[],[52])).
% 2.34/2.42 cnf(113,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[88,52,112,75,77,26,2,16,8,9])).
% 2.34/2.42 cnf(116,plain,
% 2.34/2.42 (P1(f4(a1,a1),f4(f4(a1,a1),a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[15,87,88,52,112,75,77,94,26,2,16,8,9,3,7])).
% 2.34/2.42 cnf(117,plain,
% 2.34/2.42 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[15,87,88,52,112,99,75,77,94,48,26,2,16,8,9,3,7,17])).
% 2.34/2.42 cnf(120,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[15,87,88,52,112,99,75,77,94,79,48,26,25,2,16,8,9,3,7,17,18])).
% 2.34/2.42 cnf(123,plain,
% 2.34/2.42 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[108,2])).
% 2.34/2.42 cnf(124,plain,
% 2.34/2.42 (E(f4(f4(a1,a1),f4(a1,a1)),a1)),
% 2.34/2.42 inference(scs_inference,[],[108,117,57,2,16])).
% 2.34/2.42 cnf(127,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[108,72,120,117,57,2,16,9])).
% 2.34/2.42 cnf(128,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[108,72,120,117,57,2,16,9,8])).
% 2.34/2.42 cnf(129,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),f4(a1,a1)),x1291,f4(x1291,a1))),
% 2.34/2.42 inference(scs_inference,[],[108,72,120,117,97,57,2,16,9,8,7])).
% 2.34/2.42 cnf(130,plain,
% 2.34/2.42 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[108,72,120,117,97,59,38,57,2,16,9,8,7,17])).
% 2.34/2.42 cnf(134,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[108,72,120,117,97,59,38,41,57,2,16,9,8,7,17,18])).
% 2.34/2.42 cnf(138,plain,
% 2.34/2.42 (E(a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[124,2])).
% 2.34/2.42 cnf(139,plain,
% 2.34/2.42 (E(f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[124,134,97,2,16])).
% 2.34/2.42 cnf(142,plain,
% 2.34/2.42 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[123,124,134,130,97,2,16,8])).
% 2.34/2.42 cnf(143,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[123,124,134,130,127,97,2,16,8,9])).
% 2.34/2.42 cnf(144,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),f4(a1,a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[123,124,134,130,127,113,97,2,16,8,9,7])).
% 2.34/2.42 cnf(145,plain,
% 2.34/2.42 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[123,124,134,130,127,113,116,22,97,2,16,8,9,7,17])).
% 2.34/2.42 cnf(148,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[123,124,134,130,128,127,113,116,22,97,2,16,8,9,7,17,18])).
% 2.34/2.42 cnf(150,plain,
% 2.34/2.42 (E(f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[139,2])).
% 2.34/2.42 cnf(151,plain,
% 2.34/2.42 (E(f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.42 inference(scs_inference,[],[139,145,38,2,16])).
% 2.34/2.42 cnf(154,plain,
% 2.34/2.42 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.42 inference(scs_inference,[],[139,145,142,38,2,16,9])).
% 2.34/2.42 cnf(155,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.42 inference(scs_inference,[],[139,148,145,142,38,2,16,9,8])).
% 2.34/2.42 cnf(156,plain,
% 2.34/2.42 (P1(f4(a1,a1),x1561,f4(x1561,a1))),
% 2.34/2.42 inference(scs_inference,[],[139,87,148,145,142,129,38,2,16,9,8,7])).
% 2.34/2.42 cnf(157,plain,
% 2.34/2.42 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),a1),a1)),
% 2.34/2.42 inference(scs_inference,[],[139,87,148,145,142,129,103,22,38,2,16,9,8,7,18])).
% 2.34/2.42 cnf(160,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[151,2])).
% 2.34/2.43 cnf(161,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[151,150,154,2,8])).
% 2.34/2.43 cnf(162,plain,
% 2.34/2.43 (P1(f4(a1,a1),a1,f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[151,150,154,156,2,8,9])).
% 2.34/2.43 cnf(163,plain,
% 2.34/2.43 (P1(f4(a1,a1),x1631,f4(x1631,a1))),
% 2.34/2.43 inference(rename_variables,[],[156])).
% 2.34/2.43 cnf(164,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),x1641,f4(x1641,a1))),
% 2.34/2.43 inference(scs_inference,[],[151,150,154,156,163,2,8,9,7])).
% 2.34/2.43 cnf(165,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),a1,a1)),
% 2.34/2.43 inference(scs_inference,[],[151,150,154,143,156,163,13,2,8,9,7,17])).
% 2.34/2.43 cnf(169,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[151,150,154,143,156,163,157,62,13,2,8,9,7,17,18])).
% 2.34/2.43 cnf(171,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[150,142,8])).
% 2.34/2.43 cnf(172,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[138,150,144,142,8,9])).
% 2.34/2.43 cnf(173,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[138,150,144,169,142,8,9,7])).
% 2.34/2.43 cnf(174,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),x1741,f4(f4(x1741,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[138,150,161,164,144,169,142,156,8,9,7,17])).
% 2.34/2.43 cnf(177,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),a1,f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[138,150,155,161,164,144,169,162,165,142,156,8,9,7,17,18])).
% 2.34/2.43 cnf(179,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[160,171,8])).
% 2.34/2.43 cnf(180,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),a1,a1)),
% 2.34/2.43 inference(scs_inference,[],[160,124,171,173,8,9])).
% 2.34/2.43 cnf(181,plain,
% 2.34/2.43 (P1(a1,a1,f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[160,124,171,92,173,8,9,7])).
% 2.34/2.43 cnf(182,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[160,124,172,171,92,173,117,80,8,9,7,17])).
% 2.34/2.43 cnf(185,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[160,124,172,171,92,173,117,127,80,8,9,7,17,18])).
% 2.34/2.43 cnf(187,plain,
% 2.34/2.43 (P1(a1,f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[107,181,8])).
% 2.34/2.43 cnf(188,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),a1,f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[107,181,180,8,9])).
% 2.34/2.43 cnf(189,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),a1,f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[107,181,180,8,9,7])).
% 2.34/2.43 cnf(190,plain,
% 2.34/2.43 (P1(a1,f3(f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[107,181,180,43,13,8,9,7,17])).
% 2.34/2.43 cnf(193,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[107,185,181,180,129,43,13,8,9,7,17,18])).
% 2.34/2.43 cnf(196,plain,
% 2.34/2.43 (E(f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[188,164,16])).
% 2.34/2.43 cnf(199,plain,
% 2.34/2.43 (P1(a1,f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[160,188,164,11,16,8])).
% 2.34/2.43 cnf(201,plain,
% 2.34/2.43 (P1(a1,f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[160,138,188,190,164,11,16,8,9])).
% 2.34/2.43 cnf(202,plain,
% 2.34/2.43 (P1(f4(a1,a1),a1,f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[160,138,188,190,164,11,16,8,9,7])).
% 2.34/2.43 cnf(203,plain,
% 2.34/2.43 (P1(a1,f4(f3(a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[160,138,193,188,190,144,164,11,16,8,9,7,17])).
% 2.34/2.43 cnf(205,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[160,138,179,193,188,190,144,164,162,11,16,8,9,7,17,18])).
% 2.34/2.43 cnf(207,plain,
% 2.34/2.43 (E(f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[160,138,179,193,188,190,144,164,162,11,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(208,plain,
% 2.34/2.43 (P1(a1,f4(f3(a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[207,199,8])).
% 2.34/2.43 cnf(209,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[207,51,199,113,8,9])).
% 2.34/2.43 cnf(210,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f4(f3(a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[207,51,199,203,113,8,9,7])).
% 2.34/2.43 cnf(211,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f3(f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[207,51,174,199,201,203,113,80,8,9,7,17])).
% 2.34/2.43 cnf(215,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[207,51,182,174,199,201,203,113,80,8,9,7,17,18])).
% 2.34/2.43 cnf(217,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[209,26,16])).
% 2.34/2.43 cnf(220,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[71,209,202,26,16,8])).
% 2.34/2.43 cnf(222,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[207,71,209,202,193,26,16,8,9])).
% 2.34/2.43 cnf(223,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[207,71,209,202,179,193,26,16,8,9,7])).
% 2.34/2.43 cnf(224,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[207,71,209,205,202,210,179,193,156,26,16,8,9,7,17])).
% 2.34/2.43 cnf(227,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[207,71,209,205,202,210,179,193,79,156,26,16,8,9,7,17,18])).
% 2.34/2.43 cnf(229,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[207,71,209,205,202,210,179,193,79,156,26,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(230,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[223,41,16])).
% 2.34/2.43 cnf(233,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[108,220,223,41,16,8])).
% 2.34/2.43 cnf(234,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[217,108,220,223,41,16,8,9])).
% 2.34/2.43 cnf(235,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[229,217,108,220,227,223,41,16,8,9,7])).
% 2.34/2.43 cnf(236,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f3(f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[229,217,108,177,220,227,223,201,41,80,16,8,9,7,17])).
% 2.34/2.43 cnf(239,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[229,217,108,177,220,227,223,222,99,201,41,80,16,8,9,7,17,18])).
% 2.34/2.43 cnf(241,plain,
% 2.34/2.43 (E(f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[229,217,108,177,220,227,223,222,99,201,41,80,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(242,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[229,217,108,177,220,227,223,222,99,201,41,80,16,8,9,7,17,18,2,3])).
% 2.34/2.43 cnf(243,plain,
% 2.34/2.43 (E(f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[242,2])).
% 2.34/2.43 cnf(244,plain,
% 2.34/2.43 (~E(f4(f3(a2),a2),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[242,241,61,2,3])).
% 2.34/2.43 cnf(245,plain,
% 2.34/2.43 (E(f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[242,241,61,233,59,2,3,16])).
% 2.34/2.43 cnf(248,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(a1,a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[196,242,241,61,224,233,59,2,3,16,8])).
% 2.34/2.43 cnf(249,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[196,242,230,241,61,215,224,233,59,2,3,16,8,9])).
% 2.34/2.43 cnf(250,plain,
% 2.34/2.43 (P1(f3(a1),a1,f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[196,242,230,241,61,215,224,233,59,2,3,16,8,9,7])).
% 2.34/2.43 cnf(251,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[196,242,230,241,61,215,235,224,233,59,164,2,3,16,8,9,7,17])).
% 2.34/2.43 cnf(254,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f3(a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[196,242,230,241,61,215,235,224,233,234,182,59,164,2,3,16,8,9,7,17,18])).
% 2.34/2.43 cnf(256,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[245,2])).
% 2.34/2.43 cnf(257,plain,
% 2.34/2.43 (E(f4(a1,a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[245,248,14,2,16])).
% 2.34/2.43 cnf(260,plain,
% 2.34/2.43 (P1(a1,f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[245,248,208,14,2,16,8])).
% 2.34/2.43 cnf(261,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[245,52,248,251,208,14,2,16,8,9])).
% 2.34/2.43 cnf(263,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[245,87,52,248,251,239,208,14,2,16,8,9,7])).
% 2.34/2.43 cnf(264,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[245,87,52,248,251,239,208,249,203,14,2,16,8,9,7,17])).
% 2.34/2.43 cnf(266,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[245,87,52,248,251,239,208,189,249,203,169,14,2,16,8,9,7,17,18])).
% 2.34/2.43 cnf(269,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[257,256,266,2,8])).
% 2.34/2.43 cnf(270,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[257,256,243,266,264,2,8,9])).
% 2.34/2.43 cnf(271,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[257,256,243,266,211,264,2,8,9,7])).
% 2.34/2.43 cnf(272,plain,
% 2.34/2.43 (P1(a1,f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[257,256,243,266,211,236,264,174,2,8,9,7,17])).
% 2.34/2.43 cnf(275,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[257,256,243,266,187,211,236,264,250,235,174,2,8,9,7,17,18])).
% 2.34/2.43 cnf(277,plain,
% 2.34/2.43 (E(f4(a1,a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[275,38,16])).
% 2.34/2.43 cnf(278,plain,
% 2.34/2.43 (P1(x2781,f4(f4(a1,a1),a1),x2781)),
% 2.34/2.43 inference(rename_variables,[],[38])).
% 2.34/2.43 cnf(280,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[256,275,38,16,8])).
% 2.34/2.43 cnf(281,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f3(a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[229,256,275,269,38,16,8,9])).
% 2.34/2.43 cnf(282,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[229,256,275,269,155,38,16,8,9,7])).
% 2.34/2.43 cnf(283,plain,
% 2.34/2.43 (P1(f3(a1),f3(f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[229,256,275,269,155,249,190,38,16,8,9,7,17])).
% 2.34/2.43 cnf(285,plain,
% 2.34/2.43 (P1(a1,f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[229,256,275,269,155,55,249,190,38,278,16,8,9,7,17,18])).
% 2.34/2.43 cnf(289,plain,
% 2.34/2.43 (E(f3(a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[229,256,275,269,155,55,249,190,38,278,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(290,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[277,282,9])).
% 2.34/2.43 cnf(291,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(a1,a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[277,196,282,254,9,8])).
% 2.34/2.43 cnf(292,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[277,196,261,282,254,9,8,7])).
% 2.34/2.43 cnf(293,plain,
% 2.34/2.43 (P1(a1,f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[277,196,261,282,254,10,9,8,7,17])).
% 2.34/2.43 cnf(296,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[277,196,261,282,254,283,271,129,10,9,8,7,17,18])).
% 2.34/2.43 cnf(299,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[189,22,16])).
% 2.34/2.43 cnf(300,plain,
% 2.34/2.43 (P1(f4(x3001,a1),a1,x3001)),
% 2.34/2.43 inference(rename_variables,[],[22])).
% 2.34/2.43 cnf(302,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[138,296,189,22,16,9])).
% 2.34/2.43 cnf(303,plain,
% 2.34/2.43 (P1(f3(a1),a1,f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[88,138,296,280,189,22,16,9,8])).
% 2.34/2.43 cnf(304,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[88,138,242,296,280,189,22,16,9,8,7])).
% 2.34/2.43 cnf(305,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),a1,a1)),
% 2.34/2.43 inference(scs_inference,[],[88,138,242,263,296,280,189,22,300,16,9,8,7,17])).
% 2.34/2.43 cnf(308,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[88,138,242,263,281,296,290,280,145,189,22,300,16,9,8,7,17,18])).
% 2.34/2.43 cnf(310,plain,
% 2.34/2.43 (E(f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[88,138,242,263,281,296,290,280,145,189,22,300,16,9,8,7,17,18,2])).
% 2.34/2.43 cnf(311,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[302,129,16])).
% 2.34/2.43 cnf(314,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[257,308,302,129,16,9])).
% 2.34/2.43 cnf(315,plain,
% 2.34/2.43 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[257,196,308,302,270,129,16,9,8])).
% 2.34/2.43 cnf(316,plain,
% 2.34/2.43 (P1(f4(f4(f3(a1),a1),f4(a1,a1)),f3(a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[257,196,308,302,270,129,16,9,8,7])).
% 2.34/2.43 cnf(317,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[257,196,308,302,270,285,129,16,9,8,7,17])).
% 2.34/2.43 cnf(319,plain,
% 2.34/2.43 (P1(f3(a1),f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[257,196,308,302,270,260,285,303,154,129,16,9,8,7,17,18])).
% 2.34/2.43 cnf(321,plain,
% 2.34/2.43 (E(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[257,196,308,302,270,260,285,303,154,129,16,9,8,7,17,18,2])).
% 2.34/2.43 cnf(322,plain,
% 2.34/2.43 (E(a1,f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[291,41,16])).
% 2.34/2.43 cnf(325,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[277,315,291,41,16,8])).
% 2.34/2.43 cnf(326,plain,
% 2.34/2.43 (P1(f4(f4(f3(a1),a1),f4(a1,a1)),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[277,315,316,291,41,16,8,9])).
% 2.34/2.43 cnf(327,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[277,315,316,314,291,41,16,8,9,7])).
% 2.34/2.43 cnf(328,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[277,315,316,314,317,291,281,41,16,8,9,7,17])).
% 2.34/2.43 cnf(330,plain,
% 2.34/2.43 (P1(a1,a1,f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[277,315,316,314,317,291,293,263,281,41,16,8,9,7,17,18])).
% 2.34/2.43 cnf(332,plain,
% 2.34/2.43 (E(f3(a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[277,315,316,314,317,291,293,263,281,41,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(333,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[328,164,16])).
% 2.34/2.43 cnf(336,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[217,328,164,16,7])).
% 2.34/2.43 cnf(337,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[217,328,164,16,7,9])).
% 2.34/2.43 cnf(338,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[217,319,328,164,16,7,9,8])).
% 2.34/2.43 cnf(339,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[217,319,328,164,16,7,9,8,17])).
% 2.34/2.43 cnf(341,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[217,319,328,236,164,16,7,9,8,17,18])).
% 2.34/2.43 cnf(343,plain,
% 2.34/2.43 (E(f4(f3(a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[217,319,328,236,164,16,7,9,8,17,18,2])).
% 2.34/2.43 cnf(344,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[311,338,8])).
% 2.34/2.43 cnf(345,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[311,299,339,338,8,7])).
% 2.34/2.43 cnf(346,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[311,299,339,338,8,7,9])).
% 2.34/2.43 cnf(347,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[311,299,339,338,264,317,8,7,9,17])).
% 2.34/2.43 cnf(349,plain,
% 2.34/2.43 (P1(a1,f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[311,299,339,338,337,272,264,317,8,7,9,17,18])).
% 2.34/2.43 cnf(351,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[289,346,8])).
% 2.34/2.43 cnf(352,plain,
% 2.34/2.43 (P1(a1,f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[289,299,349,346,8,9])).
% 2.34/2.43 cnf(353,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[289,311,299,349,336,346,8,9,7])).
% 2.34/2.43 cnf(354,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f3(a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[289,311,299,349,336,346,302,48,8,9,7,17])).
% 2.34/2.43 cnf(355,plain,
% 2.34/2.43 (P1(x3551,f4(f4(a1,a1),f4(a1,a1)),x3551)),
% 2.34/2.43 inference(rename_variables,[],[48])).
% 2.34/2.43 cnf(357,plain,
% 2.34/2.43 (P1(a1,f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[289,311,299,349,336,346,330,302,48,355,8,9,7,17,18])).
% 2.34/2.43 cnf(360,plain,
% 2.34/2.43 (E(f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[347,14,16])).
% 2.34/2.43 cnf(363,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[310,347,345,14,16,8])).
% 2.34/2.43 cnf(364,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[310,322,347,357,345,14,16,8,7])).
% 2.34/2.43 cnf(365,plain,
% 2.34/2.43 (P1(f3(a1),f3(a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[310,322,311,347,357,345,325,14,16,8,7,9])).
% 2.34/2.43 cnf(366,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[310,322,311,347,357,345,325,280,36,14,16,8,7,9,17])).
% 2.34/2.43 cnf(369,plain,
% 2.34/2.43 (P1(f3(a1),f3(f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[310,322,311,347,357,344,353,345,325,354,280,36,14,16,8,7,9,17,18])).
% 2.34/2.43 cnf(371,plain,
% 2.34/2.43 (E(f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[310,322,311,347,357,344,353,345,325,354,280,36,14,16,8,7,9,17,18,2])).
% 2.34/2.43 cnf(372,plain,
% 2.34/2.43 (E(a1,f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[310,322,311,347,357,344,353,345,325,354,280,36,14,16,8,7,9,17,18,2,3])).
% 2.34/2.43 cnf(373,plain,
% 2.34/2.43 (E(f4(f3(a1),f3(a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[372,2])).
% 2.34/2.43 cnf(375,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[343,372,371,244,364,2,3,9])).
% 2.34/2.43 cnf(376,plain,
% 2.34/2.43 (P1(f3(a1),f3(f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[343,372,371,244,364,366,2,3,9,8])).
% 2.34/2.43 cnf(377,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f4(a1,a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[333,343,372,371,244,364,366,341,2,3,9,8,7])).
% 2.34/2.43 cnf(378,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[333,343,372,371,244,363,364,366,341,172,59,2,3,9,8,7,17])).
% 2.34/2.43 cnf(381,plain,
% 2.34/2.43 (P1(f3(a1),f4(f3(a1),a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[333,343,372,371,244,363,364,366,365,341,172,353,59,2,3,9,8,7,17,18])).
% 2.34/2.43 cnf(383,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[321,381,8])).
% 2.34/2.43 cnf(384,plain,
% 2.34/2.43 (P1(f3(a1),f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[321,381,376,8,9])).
% 2.34/2.43 cnf(385,plain,
% 2.34/2.43 (P1(a1,f3(f4(a1,a1)),f4(f3(a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[321,332,381,376,8,9,7])).
% 2.34/2.43 cnf(386,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(f3(a1),a1),f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[321,332,381,376,326,327,8,9,7,18])).
% 2.34/2.43 cnf(388,plain,
% 2.34/2.43 (P1(f3(a1),f4(f4(a1,a1),a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[245,292,8])).
% 2.34/2.43 cnf(389,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[360,245,351,292,8,9])).
% 2.34/2.43 cnf(390,plain,
% 2.34/2.43 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[360,372,245,351,352,292,8,9,7])).
% 2.34/2.43 cnf(391,plain,
% 2.34/2.43 (P1(a1,f4(f4(f3(a1),a1),f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[360,372,245,386,351,352,292,304,8,9,7,17])).
% 2.34/2.43 cnf(393,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[360,372,245,386,351,352,292,304,305,8,9,7,17,18])).
% 2.34/2.43 cnf(395,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[230,161,8])).
% 2.34/2.43 cnf(396,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[230,289,393,161,8,9])).
% 2.34/2.43 cnf(397,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[230,289,343,393,161,8,9,7])).
% 2.34/2.43 cnf(398,plain,
% 2.34/2.43 (P1(f4(a1,a1),f4(f4(f3(a1),a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[230,289,343,393,391,161,303,8,9,7,17])).
% 2.34/2.43 cnf(400,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[230,289,343,393,391,161,269,336,303,8,9,7,17,18])).
% 2.34/2.43 cnf(402,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[243,396,8])).
% 2.34/2.43 cnf(403,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[243,321,396,8,7])).
% 2.34/2.43 cnf(404,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[243,322,321,396,157,8,7,9])).
% 2.34/2.43 cnf(405,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[243,322,321,378,396,395,157,38,8,7,9,17])).
% 2.34/2.43 cnf(408,plain,
% 2.34/2.43 (P1(a1,f4(a1,a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[243,322,321,378,396,395,157,187,346,38,8,7,9,17,18])).
% 2.34/2.43 cnf(410,plain,
% 2.34/2.43 (E(f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[389,97,16])).
% 2.34/2.43 cnf(413,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[310,389,397,97,16,8])).
% 2.34/2.43 cnf(414,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.43 inference(scs_inference,[],[310,389,397,97,16,8,9])).
% 2.34/2.43 cnf(415,plain,
% 2.34/2.43 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[310,372,389,408,397,97,16,8,9,7])).
% 2.34/2.43 cnf(416,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[310,372,402,389,408,397,302,97,57,16,8,9,7,17])).
% 2.34/2.43 cnf(419,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[310,372,402,389,377,408,397,302,97,57,16,8,9,7,17,18])).
% 2.34/2.43 cnf(421,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[310,372,402,389,377,408,397,302,97,57,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(422,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[421,404,8])).
% 2.34/2.43 cnf(423,plain,
% 2.34/2.43 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[421,404,8,7])).
% 2.34/2.43 cnf(424,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[421,404,405,8,7,9])).
% 2.34/2.43 cnf(425,plain,
% 2.34/2.43 (P1(f4(a1,a1),f3(a1),a1)),
% 2.34/2.43 inference(scs_inference,[],[421,398,404,405,316,41,8,7,9,17])).
% 2.34/2.43 cnf(428,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),a1),f3(a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[421,398,404,405,375,316,41,8,7,9,17,18])).
% 2.34/2.43 cnf(430,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[400,14,16])).
% 2.34/2.43 cnf(433,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.43 inference(scs_inference,[],[241,400,403,14,16,8])).
% 2.34/2.43 cnf(434,plain,
% 2.34/2.43 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[241,400,415,403,14,16,8,9])).
% 2.34/2.43 cnf(435,plain,
% 2.34/2.43 (P1(a1,f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[373,241,400,415,403,423,14,16,8,9,7])).
% 2.34/2.43 cnf(436,plain,
% 2.34/2.43 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 2.34/2.43 inference(scs_inference,[],[373,241,400,415,403,383,423,12,14,16,8,9,7,17])).
% 2.34/2.43 cnf(439,plain,
% 2.34/2.43 (P1(f4(f3(a1),a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[373,241,400,415,403,383,419,423,315,12,14,16,8,9,7,17,18])).
% 2.34/2.43 cnf(441,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),f3(a1)),f3(f4(a1,a1)))),
% 2.34/2.43 inference(scs_inference,[],[373,241,400,415,403,383,419,423,315,12,14,16,8,9,7,17,18,2])).
% 2.34/2.43 cnf(442,plain,
% 2.34/2.43 (E(f3(a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[373,241,400,415,403,383,419,423,315,12,14,16,8,9,7,17,18,2,3])).
% 2.34/2.43 cnf(443,plain,
% 2.34/2.43 (E(f4(f4(a1,a1),f3(a1)),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[442,2])).
% 2.34/2.43 cnf(445,plain,
% 2.34/2.43 (E(f3(f4(a1,a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.43 inference(scs_inference,[],[441,442,434,61,26,2,3,16])).
% 2.34/2.43 cnf(448,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.43 inference(scs_inference,[],[441,430,442,434,413,61,26,2,3,16,7])).
% 2.34/2.43 cnf(449,plain,
% 2.34/2.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[441,430,442,433,434,413,61,26,2,3,16,7,8])).
% 2.34/2.44 cnf(450,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,430,442,433,434,413,61,26,2,3,16,7,8,9])).
% 2.34/2.44 cnf(451,plain,
% 2.34/2.44 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,430,442,433,434,413,61,337,48,26,2,3,16,7,8,9,17])).
% 2.34/2.44 cnf(454,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,430,442,433,434,384,413,390,61,337,48,26,2,3,16,7,8,9,17,18])).
% 2.34/2.44 cnf(456,plain,
% 2.34/2.44 (E(f4(f3(a1),f3(a1)),f3(f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[445,2])).
% 2.34/2.44 cnf(457,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[445,454,26,2,16])).
% 2.34/2.44 cnf(460,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[410,445,454,450,26,2,16,7])).
% 2.34/2.44 cnf(461,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[410,445,454,450,428,26,2,16,7,9])).
% 2.34/2.44 cnf(462,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[410,445,332,454,450,428,439,26,2,16,7,9,8])).
% 2.34/2.44 cnf(463,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[410,445,332,454,450,428,439,425,10,26,2,16,7,9,8,17])).
% 2.34/2.44 cnf(466,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[410,445,332,454,450,428,439,425,270,403,10,26,2,16,7,9,8,17,18])).
% 2.34/2.44 cnf(468,plain,
% 2.34/2.44 (E(f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[457,2])).
% 2.34/2.44 cnf(469,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[457,460,97,2,16])).
% 2.34/2.44 cnf(472,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[457,460,449,97,2,16,7])).
% 2.34/2.44 cnf(473,plain,
% 2.34/2.44 (P1(f4(a1,a1),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[457,460,449,451,97,2,16,7,9])).
% 2.34/2.44 cnf(474,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[457,460,449,466,451,97,2,16,7,9,8])).
% 2.34/2.44 cnf(475,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[457,460,449,466,451,116,22,97,2,16,7,9,8,17])).
% 2.34/2.44 cnf(478,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[457,460,449,466,451,414,424,385,116,22,97,2,16,7,9,8,17,18])).
% 2.34/2.44 cnf(480,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[469,2])).
% 2.34/2.44 cnf(481,plain,
% 2.34/2.44 (E(f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[469,473,156,2,16])).
% 2.34/2.44 cnf(484,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[469,360,474,473,156,2,16,7])).
% 2.34/2.44 cnf(485,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[469,468,360,474,461,473,156,2,16,7,9])).
% 2.34/2.44 cnf(486,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[469,468,360,472,474,461,473,156,2,16,7,9,8])).
% 2.34/2.44 cnf(487,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[469,468,360,472,478,422,474,461,473,156,11,2,16,7,9,8,17])).
% 2.34/2.44 cnf(490,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[469,468,360,472,478,422,474,461,473,462,77,156,11,2,16,7,9,8,17,18])).
% 2.34/2.44 cnf(492,plain,
% 2.34/2.44 (E(f4(f3(a1),a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[481,2])).
% 2.34/2.44 cnf(493,plain,
% 2.34/2.44 (E(f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[481,475,38,2,16])).
% 2.34/2.44 cnf(496,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[481,442,475,435,38,2,16,9])).
% 2.34/2.44 cnf(497,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[480,481,442,475,485,435,38,2,16,9,7])).
% 2.34/2.44 cnf(498,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[480,481,442,475,485,435,38,2,16,9,7,8])).
% 2.34/2.44 cnf(499,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(a1,a1),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[480,481,442,490,475,485,435,454,57,38,2,16,9,7,8,17])).
% 2.34/2.44 cnf(502,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[480,481,442,490,475,485,416,435,454,57,38,2,16,9,7,8,17,18])).
% 2.34/2.44 cnf(504,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[493,2])).
% 2.34/2.44 cnf(505,plain,
% 2.34/2.44 (E(f4(a1,a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[493,486,38,2,16])).
% 2.34/2.44 cnf(508,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[493,443,486,498,38,2,16,7])).
% 2.34/2.44 cnf(509,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[493,443,289,486,498,502,38,2,16,7,9])).
% 2.34/2.44 cnf(510,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[493,443,289,486,498,502,38,2,16,7,9,8])).
% 2.34/2.44 cnf(511,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[493,443,289,486,498,502,496,378,11,38,2,16,7,9,8,17])).
% 2.34/2.44 cnf(514,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[493,443,289,486,498,502,487,496,378,474,11,38,2,16,7,9,8,17,18])).
% 2.34/2.44 cnf(516,plain,
% 2.34/2.44 (E(f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[505,2])).
% 2.34/2.44 cnf(517,plain,
% 2.34/2.44 (E(a1,f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[505,391,11,2,16])).
% 2.34/2.44 cnf(520,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[492,505,511,391,11,2,16,9])).
% 2.34/2.44 cnf(521,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[492,505,456,511,484,391,11,2,16,9,7])).
% 2.34/2.44 cnf(522,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[492,505,456,511,484,391,11,2,16,9,7,8])).
% 2.34/2.44 cnf(523,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(f3(a1),a1),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[492,505,456,511,484,499,391,398,41,11,2,16,9,7,8,17])).
% 2.34/2.44 cnf(526,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[492,505,456,511,484,514,499,391,398,395,41,11,2,16,9,7,8,17,18])).
% 2.34/2.44 cnf(529,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(a1,a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[504,517,520,2,7])).
% 2.34/2.44 cnf(530,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[504,516,517,520,2,7,9])).
% 2.34/2.44 cnf(531,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[504,516,517,333,522,520,2,7,9,8])).
% 2.34/2.44 cnf(532,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),f4(f3(a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[504,516,517,333,521,522,520,171,41,2,7,9,8,17])).
% 2.34/2.44 cnf(535,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[504,516,517,333,521,522,520,508,171,499,41,2,7,9,8,17,18])).
% 2.34/2.44 cnf(537,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[243,535,9])).
% 2.34/2.44 cnf(538,plain,
% 2.34/2.44 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[371,243,526,535,9,7])).
% 2.34/2.44 cnf(539,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[371,493,243,526,529,535,9,7,8])).
% 2.34/2.44 cnf(540,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[371,493,243,526,529,535,510,9,7,8,17])).
% 2.34/2.44 cnf(542,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[371,493,243,526,529,535,510,315,9,7,8,17,18])).
% 2.34/2.44 cnf(544,plain,
% 2.34/2.44 (E(f4(a1,a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[530,14,16])).
% 2.34/2.44 cnf(547,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[505,530,540,14,16,9])).
% 2.34/2.44 cnf(548,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[504,505,530,540,448,14,16,9,7])).
% 2.34/2.44 cnf(549,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[504,505,530,540,448,14,16,9,7,8])).
% 2.34/2.44 cnf(550,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[504,505,530,540,448,144,14,16,9,7,8,17])).
% 2.34/2.44 cnf(552,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[504,505,530,540,539,448,450,144,14,16,9,7,8,17,18])).
% 2.34/2.44 cnf(554,plain,
% 2.34/2.44 (E(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[504,505,530,540,539,448,450,144,14,16,9,7,8,17,18,2])).
% 2.34/2.44 cnf(555,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[552,14,16])).
% 2.34/2.44 cnf(558,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[373,552,547,14,16,9])).
% 2.34/2.44 cnf(559,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[373,332,552,547,537,14,16,9,7])).
% 2.34/2.44 cnf(560,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),a1,f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[373,332,552,549,547,537,14,16,9,7,8])).
% 2.34/2.44 cnf(561,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[373,332,552,549,547,537,142,12,14,16,9,7,8,17])).
% 2.34/2.44 cnf(564,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[373,332,552,549,547,537,511,142,12,14,16,9,7,8,17,18])).
% 2.34/2.44 cnf(566,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[373,332,552,549,547,537,511,142,12,14,16,9,7,8,17,18,2])).
% 2.34/2.44 cnf(567,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[360,388,7])).
% 2.34/2.44 cnf(568,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[566,360,497,388,7,9])).
% 2.34/2.44 cnf(569,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[566,360,480,497,542,388,7,9,8])).
% 2.34/2.44 cnf(570,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f3(a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[566,360,480,564,497,542,388,57,7,9,8,17])).
% 2.34/2.44 cnf(573,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),a1,a1)),
% 2.34/2.44 inference(scs_inference,[],[566,360,480,564,550,497,542,388,560,558,57,7,9,8,17,18])).
% 2.34/2.44 cnf(575,plain,
% 2.34/2.44 (E(a1,f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[573,10,16])).
% 2.34/2.44 cnf(578,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[442,538,573,10,16,7])).
% 2.34/2.44 cnf(579,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[442,548,538,573,10,16,7,9])).
% 2.34/2.44 cnf(580,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[566,442,436,548,538,573,10,16,7,9,8])).
% 2.34/2.44 cnf(581,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[566,442,436,548,538,568,573,539,10,16,7,9,8,17])).
% 2.34/2.44 cnf(583,plain,
% 2.34/2.44 (P1(f3(a1),f4(a1,a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[566,442,509,436,548,538,569,568,573,539,99,10,16,7,9,8,17,18])).
% 2.34/2.44 cnf(585,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[566,442,509,436,548,538,569,568,573,539,99,10,16,7,9,8,17,18,2])).
% 2.34/2.44 cnf(586,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[566,463,7])).
% 2.34/2.44 cnf(587,plain,
% 2.34/2.44 (P1(f3(a1),f4(a1,a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[544,566,583,463,7,9])).
% 2.34/2.44 cnf(588,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[544,566,583,463,7,9,8])).
% 2.34/2.44 cnf(589,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(a1,a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[544,566,579,583,463,172,57,7,9,8,17])).
% 2.34/2.44 cnf(592,plain,
% 2.34/2.44 (P1(f3(a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[544,566,579,532,583,463,559,369,172,57,7,9,8,17,18])).
% 2.34/2.44 cnf(594,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[32,580,7])).
% 2.34/2.44 cnf(595,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[481,32,581,580,7,9])).
% 2.34/2.44 cnf(596,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[481,32,493,581,589,580,7,9,8])).
% 2.34/2.44 cnf(597,plain,
% 2.34/2.44 (P1(a1,f4(f4(f3(a1),a1),f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[481,32,493,581,589,580,570,523,22,7,9,8,17])).
% 2.34/2.44 cnf(600,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[481,32,493,581,589,580,570,523,550,55,22,7,9,8,17,18])).
% 2.34/2.44 cnf(603,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f4(f3(a1),a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[410,531,7])).
% 2.34/2.44 cnf(604,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[410,531,586,7,9])).
% 2.34/2.44 cnf(605,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[555,410,531,586,596,7,9,8])).
% 2.34/2.44 cnf(606,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[555,410,531,586,596,594,560,7,9,8,17])).
% 2.34/2.44 cnf(608,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),a1,f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[555,410,531,586,561,596,594,357,560,7,9,8,17,18])).
% 2.34/2.44 cnf(610,plain,
% 2.34/2.44 (E(f4(f3(a1),a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[608,10,16])).
% 2.34/2.44 cnf(613,plain,
% 2.34/2.44 (P1(a1,f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[585,608,604,10,16,7])).
% 2.34/2.44 cnf(614,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[585,492,608,604,10,16,7,9])).
% 2.34/2.44 cnf(615,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[585,492,603,608,604,10,16,7,9,8])).
% 2.34/2.44 cnf(616,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[585,492,603,606,608,604,351,10,16,7,9,8,17])).
% 2.34/2.44 cnf(618,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[585,492,603,606,608,604,567,293,351,10,16,7,9,8,17,18])).
% 2.34/2.44 cnf(620,plain,
% 2.34/2.44 (E(f4(f4(a1,a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[585,492,603,606,608,604,567,293,351,10,16,7,9,8,17,18,2])).
% 2.34/2.44 cnf(621,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f4(a1,a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[620,578,7])).
% 2.34/2.44 cnf(622,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[620,610,578,600,7,9])).
% 2.34/2.44 cnf(623,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),f3(a1)),f3(f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[620,610,578,600,208,7,9,8])).
% 2.34/2.44 cnf(627,plain,
% 2.34/2.44 (P1(f3(a1),a1,f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[620,610,578,615,600,616,605,94,338,208,129,7,9,8,17,18])).
% 2.34/2.44 cnf(629,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,614,7])).
% 2.34/2.44 cnf(630,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,610,595,614,7,9])).
% 2.34/2.44 cnf(631,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[575,441,610,627,595,614,7,9,8])).
% 2.34/2.44 cnf(632,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[575,441,610,627,595,614,128,449,164,7,9,8,17])).
% 2.34/2.44 cnf(635,plain,
% 2.34/2.44 (P1(f3(a1),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[575,441,610,592,627,595,623,614,128,449,164,7,9,8,17,18])).
% 2.34/2.44 cnf(637,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[333,629,7])).
% 2.34/2.44 cnf(638,plain,
% 2.34/2.44 (P1(a1,f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[516,333,629,622,7,8])).
% 2.34/2.44 cnf(639,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[516,555,333,630,629,622,7,8,9])).
% 2.34/2.44 cnf(640,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[516,555,333,621,630,629,622,606,41,7,8,9,17])).
% 2.34/2.44 cnf(643,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[516,555,333,621,635,630,629,622,606,202,41,7,8,9,17,18])).
% 2.34/2.44 cnf(645,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[585,549,7])).
% 2.34/2.44 cnf(646,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[585,549,568,7,9])).
% 2.34/2.44 cnf(647,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),a1,f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[585,640,549,568,7,9,8])).
% 2.34/2.44 cnf(648,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[585,632,640,549,568,497,48,7,9,8,17])).
% 2.34/2.44 cnf(651,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[585,632,618,640,638,637,549,568,497,48,7,9,8,17,18])).
% 2.34/2.44 cnf(653,plain,
% 2.34/2.44 (E(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[587,26,16])).
% 2.34/2.44 cnf(656,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[230,587,532,26,16,7])).
% 2.34/2.44 cnf(657,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[468,230,587,532,547,26,16,7,8])).
% 2.34/2.44 cnf(658,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[468,230,587,532,547,26,16,7,8,9])).
% 2.34/2.44 cnf(659,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[468,230,648,587,266,532,547,156,26,16,7,8,9,17])).
% 2.34/2.44 cnf(662,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[468,230,651,648,587,266,531,564,532,547,156,26,16,7,8,9,17,18])).
% 2.34/2.44 cnf(664,plain,
% 2.34/2.44 (E(f3(a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[468,230,651,648,587,266,531,564,532,547,156,26,16,7,8,9,17,18,2])).
% 2.34/2.44 cnf(665,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[481,522,7])).
% 2.34/2.44 cnf(666,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[481,445,522,177,7,9])).
% 2.34/2.44 cnf(667,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[664,481,445,522,304,177,7,9,8])).
% 2.34/2.44 cnf(668,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[664,481,445,645,647,522,304,177,97,7,9,8,17])).
% 2.34/2.44 cnf(671,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[664,481,445,662,658,645,647,490,522,304,177,97,7,9,8,17,18])).
% 2.34/2.44 cnf(673,plain,
% 2.34/2.44 (P1(f3(a1),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[371,514,7])).
% 2.34/2.44 cnf(674,plain,
% 2.34/2.44 (P1(f3(a1),f4(a1,a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[554,371,667,514,7,8])).
% 2.34/2.44 cnf(676,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f3(a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[554,371,657,666,667,514,559,80,7,8,9,17])).
% 2.34/2.44 cnf(679,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[554,371,657,659,631,666,667,514,640,559,80,7,8,9,17,18])).
% 2.34/2.44 cnf(681,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(a1,a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[516,676,8])).
% 2.34/2.44 cnf(682,plain,
% 2.34/2.44 (P1(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[664,516,673,676,8,7])).
% 2.34/2.44 cnf(687,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[664,516,544,643,613,668,673,676,615,13,8,7,9,17,18])).
% 2.34/2.44 cnf(689,plain,
% 2.34/2.44 (P1(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f4(a1,a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[664,674,7])).
% 2.34/2.44 cnf(690,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f3(f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[456,664,674,422,7,8])).
% 2.34/2.44 cnf(691,plain,
% 2.34/2.44 (P1(f3(a1),f4(a1,a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[517,456,664,674,422,7,8,9])).
% 2.34/2.44 cnf(692,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[517,456,664,665,674,521,422,26,7,8,9,17])).
% 2.34/2.44 cnf(695,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[517,456,664,665,674,521,325,422,463,26,7,8,9,17,18])).
% 2.34/2.44 cnf(700,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[575,691,165,26,16,8])).
% 2.34/2.44 cnf(702,plain,
% 2.34/2.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[575,620,691,656,165,605,26,16,8,7,9])).
% 2.34/2.44 cnf(708,plain,
% 2.34/2.44 (E(f3(a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[575,620,679,687,690,691,656,283,165,605,11,26,16,8,7,9,17,18,2])).
% 2.34/2.44 cnf(709,plain,
% 2.34/2.44 (E(a1,f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[689,26,16])).
% 2.34/2.44 cnf(713,plain,
% 2.34/2.44 (P1(f4(a1,a1),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[708,504,689,416,614,26,16,8,7])).
% 2.34/2.44 cnf(714,plain,
% 2.34/2.44 (P1(a1,f4(a1,a1),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[708,504,689,416,614,408,26,16,8,7,9])).
% 2.34/2.44 cnf(715,plain,
% 2.34/2.44 (P1(a1,f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[708,504,689,700,341,416,614,408,164,26,16,8,7,9,17])).
% 2.34/2.44 cnf(720,plain,
% 2.34/2.44 (E(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[709,2])).
% 2.34/2.44 cnf(721,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(f3(a1),a1),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[709,708,425,2,8])).
% 2.34/2.44 cnf(722,plain,
% 2.34/2.44 (P1(f4(a1,a1),f3(a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[709,708,425,2,8,9])).
% 2.34/2.44 cnf(724,plain,
% 2.34/2.44 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[709,469,708,671,502,425,94,10,2,8,9,7,17])).
% 2.34/2.44 cnf(727,plain,
% 2.34/2.44 (P1(a1,a1,f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[709,469,708,671,715,646,451,502,425,94,10,2,8,9,7,17,18])).
% 2.34/2.44 cnf(729,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[441,498,8])).
% 2.34/2.44 cnf(730,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),f3(a1),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[441,510,498,8,7])).
% 2.34/2.44 cnf(732,plain,
% 2.34/2.44 (P1(f4(a1,a1),f3(a1),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[441,588,682,702,510,498,14,8,7,9,17])).
% 2.34/2.44 cnf(735,plain,
% 2.34/2.44 (P1(a1,f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[441,588,682,722,702,714,510,326,498,14,8,7,9,17,18])).
% 2.34/2.44 cnf(737,plain,
% 2.34/2.44 (P1(f3(f4(a1,a1)),f3(a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[443,580,8])).
% 2.34/2.44 cnf(740,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),a1,a1)),
% 2.34/2.44 inference(scs_inference,[],[443,695,580,630,568,84,13,8,7,9,17])).
% 2.34/2.44 cnf(745,plain,
% 2.34/2.44 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[555,569,8])).
% 2.34/2.44 cnf(746,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[555,569,549,8,7])).
% 2.34/2.44 cnf(747,plain,
% 2.34/2.44 (P1(a1,f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[555,569,638,549,8,7,9])).
% 2.34/2.44 cnf(751,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),a1,f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[555,729,721,681,597,569,173,638,549,48,8,7,9,17,18])).
% 2.34/2.44 cnf(755,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f3(a1),a1))),
% 2.34/2.44 inference(scs_inference,[],[620,700,596,568,7,8,9])).
% 2.34/2.44 cnf(756,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),a1,f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[620,692,740,700,596,568,10,7,8,9,17])).
% 2.34/2.44 cnf(759,plain,
% 2.34/2.44 (P1(a1,f4(f3(a1),f3(a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[620,692,724,747,740,679,700,596,568,10,7,8,9,17,18])).
% 2.34/2.44 cnf(763,plain,
% 2.34/2.44 (P1(x7631,f3(x7631),f4(f4(f3(a1),a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[517,303,408,12,8,7,9])).
% 2.34/2.44 cnf(767,plain,
% 2.34/2.44 (P1(f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[517,639,713,745,594,182,303,408,12,22,8,7,9,17,18])).
% 2.34/2.44 cnf(769,plain,
% 2.34/2.44 (P1(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),x7691,f4(x7691,a1))),
% 2.34/2.44 inference(scs_inference,[],[709,55,7])).
% 2.34/2.44 cnf(770,plain,
% 2.34/2.44 (P1(f4(x7701,a1),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),x7701)),
% 2.34/2.44 inference(scs_inference,[],[709,55,22,7,8])).
% 2.34/2.44 cnf(771,plain,
% 2.34/2.44 (P1(x7711,f3(x7711),f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[709,55,12,22,7,8,9])).
% 2.34/2.44 cnf(776,plain,
% 2.34/2.44 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(f3(a1),f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[709,763,746,767,737,657,55,12,22,7,8,9,17,18])).
% 2.34/2.44 cnf(778,plain,
% 2.34/2.44 (P1(f4(x7781,a1),f3(a1),x7781)),
% 2.34/2.44 inference(scs_inference,[],[653,770,8])).
% 2.34/2.44 cnf(779,plain,
% 2.34/2.44 (P1(f3(a1),x7791,f4(x7791,a1))),
% 2.34/2.44 inference(scs_inference,[],[653,769,770,8,7])).
% 2.34/2.44 cnf(780,plain,
% 2.34/2.44 (P1(x7801,f3(x7801),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[653,771,769,770,8,7,9])).
% 2.34/2.44 cnf(781,plain,
% 2.34/2.44 (P1(f4(f4(f4(a1,a1),f3(a1)),f4(a1,a1)),f3(a1),a1)),
% 2.34/2.44 inference(scs_inference,[],[653,771,769,770,730,41,8,7,9,17])).
% 2.34/2.44 cnf(787,plain,
% 2.34/2.44 (E(f4(f3(a1),f4(a1,a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[653,771,769,770,776,730,732,727,41,8,7,9,17,18,16])).
% 2.34/2.44 cnf(789,plain,
% 2.34/2.44 (E(a1,f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[653,771,769,770,776,730,732,727,41,8,7,9,17,18,16,2])).
% 2.34/2.44 cnf(790,plain,
% 2.34/2.44 (~E(f4(f3(a2),a2),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[15,653,771,769,770,776,730,732,727,41,8,7,9,17,18,16,2,3])).
% 2.34/2.44 cnf(793,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),f3(a1),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[789,751,759,570,7,8,9])).
% 2.34/2.44 cnf(794,plain,
% 2.34/2.44 (P1(a1,f3(f3(a1)),a1)),
% 2.34/2.44 inference(scs_inference,[],[789,780,751,759,781,570,7,8,9,17])).
% 2.34/2.44 cnf(799,plain,
% 2.34/2.44 (E(f4(f3(a1),f4(a1,a1)),f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[793,778,16])).
% 2.34/2.44 cnf(800,plain,
% 2.34/2.44 (P1(f4(x8001,a1),f3(a1),x8001)),
% 2.34/2.44 inference(rename_variables,[],[778])).
% 2.34/2.44 cnf(804,plain,
% 2.34/2.44 (E(x8041,f4(f4(x8041,a1),a1))),
% 2.34/2.44 inference(rename_variables,[],[71])).
% 2.34/2.44 cnf(813,plain,
% 2.34/2.44 (E(f3(a1),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[720,71,804,755,793,778,800,779,756,794,735,16,8,7,9,17,18,2])).
% 2.34/2.44 cnf(822,plain,
% 2.34/2.44 (E(f3(a1),f4(x8221,f3(x8221)))),
% 2.34/2.44 inference(scs_inference,[],[780,14,16])).
% 2.34/2.44 cnf(828,plain,
% 2.34/2.44 (P1(x8281,f3(x8281),f3(a1))),
% 2.34/2.44 inference(rename_variables,[],[780])).
% 2.34/2.44 cnf(829,plain,
% 2.34/2.44 (P1(x8291,f3(x8291),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[813,299,780,828,80,14,16,7,8,9])).
% 2.34/2.44 cnf(830,plain,
% 2.34/2.44 (P1(f3(a1),f3(f3(x8301)),x8301)),
% 2.34/2.44 inference(scs_inference,[],[813,299,780,828,80,12,10,14,16,7,8,9,17])).
% 2.34/2.44 cnf(834,plain,
% 2.34/2.44 (P1(f3(f4(x8341,a1)),x8341,f3(a1))),
% 2.34/2.44 inference(scs_inference,[],[813,299,780,828,778,80,12,13,10,14,16,7,8,9,17,18])).
% 2.34/2.44 cnf(839,plain,
% 2.34/2.44 (E(f4(f3(a1),f4(a1,a1)),f4(a1,f3(a1)))),
% 2.34/2.44 inference(scs_inference,[],[813,799,299,780,828,778,80,12,13,10,14,16,7,8,9,17,18,2,3])).
% 2.34/2.44 cnf(841,plain,
% 2.34/2.44 (E(f4(f3(a1),f4(a1,a1)),f4(x8411,f3(x8411)))),
% 2.34/2.44 inference(scs_inference,[],[799,839,822,2,3])).
% 2.34/2.44 cnf(842,plain,
% 2.34/2.44 (E(f4(a1,a1),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[799,839,822,25,829,2,3,16])).
% 2.34/2.44 cnf(847,plain,
% 2.34/2.44 (P1(f4(x8471,a1),f4(f3(a1),f4(a1,a1)),x8471)),
% 2.34/2.44 inference(scs_inference,[],[787,799,813,839,822,778,25,48,829,2,3,16,7,8])).
% 2.34/2.44 cnf(852,plain,
% 2.34/2.44 (P1(f4(f3(x8521),a1),x8521,f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[787,799,813,151,839,822,778,25,780,48,829,830,2,3,16,7,8,9,17,18])).
% 2.34/2.44 cnf(856,plain,
% 2.34/2.44 (E(f4(x8561,f3(x8561)),f4(f3(a1),f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[841,2])).
% 2.34/2.44 cnf(858,plain,
% 2.34/2.44 (E(f3(f3(a1)),f4(a1,a1))),
% 2.34/2.44 inference(scs_inference,[],[789,841,778,852,2,3,16])).
% 2.34/2.44 cnf(860,plain,
% 2.34/2.44 (P1(f4(x8601,a1),f3(a1),x8601)),
% 2.34/2.44 inference(rename_variables,[],[778])).
% 2.34/2.44 cnf(866,plain,
% 2.34/2.44 (P1(f3(a1),x8661,x8661)),
% 2.34/2.44 inference(scs_inference,[],[787,87,207,789,841,780,25,80,778,860,38,852,834,2,3,16,7,8,9,17])).
% 2.34/2.44 cnf(879,plain,
% 2.34/2.44 (P1(x8791,f3(x8791),f3(a1))),
% 2.34/2.44 inference(rename_variables,[],[780])).
% 2.34/2.44 cnf(894,plain,
% 2.34/2.44 (~E(a2,f3(f3(a2)))),
% 2.34/2.44 inference(scs_inference,[],[787,242,51,842,856,780,879,80,11,12,48,13,790,866,829,2,3,16,7,8,9,17,18,6])).
% 2.34/2.44 cnf(898,plain,
% 2.34/2.44 (P1(f4(f3(a1),a1),x8981,x8981)),
% 2.34/2.44 inference(scs_inference,[],[107,858,11,30,2,3,7])).
% 2.34/2.44 cnf(995,plain,
% 2.34/2.44 (E(x9951,f4(x9951,f4(a1,a1)))),
% 2.34/2.44 inference(scs_inference,[],[26,14,16])).
% 2.34/2.44 cnf(1014,plain,
% 2.34/2.44 (E(f4(a1,a1),f4(x10141,f3(x10141)))),
% 2.34/2.44 inference(scs_inference,[],[15,995,25,14,2,3,16])).
% 2.34/2.44 cnf(1027,plain,
% 2.34/2.44 (P1(x10271,f4(a1,a1),f3(f3(x10271)))),
% 2.34/2.44 inference(scs_inference,[],[15,516,108,995,25,12,26,763,847,898,10,11,14,2,3,16,7,8,9,17,18])).
% 2.34/2.44 cnf(1032,plain,
% 2.34/2.44 ($false),
% 2.34/2.44 inference(scs_inference,[],[1014,26,1027,894,2,16]),
% 2.34/2.44 ['proof']).
% 2.34/2.44 % SZS output end Proof
% 2.34/2.44 % Total time :1.950000s
%------------------------------------------------------------------------------