%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP021-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 : n001.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 1.33s 1.40s
% Output : CNFRefutation 1.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP021-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n001.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.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 20 08:37:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 1.33/1.40 %-------------------------------------------
% 1.33/1.40 % File :CSE---1.7
% 1.33/1.40 % Problem :theBenchmark
% 1.33/1.40 % Transform :cnf
% 1.33/1.40 % Format :tptp:raw
% 1.33/1.40 % Command :java -jar mcs_scs.jar %d %s
% 1.33/1.40
% 1.33/1.40 % Result :Theorem 0.790000s
% 1.33/1.40 % Output :CNFRefutation 0.790000s
% 1.33/1.40 %-------------------------------------------
% 1.33/1.40 %--------------------------------------------------------------------------
% 1.33/1.40 % File : GRP021-1 : TPTP v8.2.0. Released v1.0.0.
% 1.33/1.40 % Domain : Group Theory
% 1.33/1.40 % Problem : X times inverse of X is the identity
% 1.33/1.40 % Version : [MOW76] axioms.
% 1.33/1.40 % English :
% 1.33/1.40
% 1.33/1.40 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 1.33/1.40 % : [OMW76] Overbeek et al. (1976), Complexity and Related Enhance
% 1.33/1.40 % Source : [MOW76]
% 1.33/1.40 % Names : Identity established [MOW76]
% 1.33/1.40 % : Lemma proved [OMW76]
% 1.33/1.40
% 1.33/1.40 % Status : Unsatisfiable
% 1.33/1.40 % Rating : 0.00 v6.0.0, 0.22 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.00 v2.0.0
% 1.33/1.40 % Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 4 RR)
% 1.33/1.40 % Number of literals : 17 ( 2 equ; 9 neg)
% 1.33/1.40 % Maximal clause size : 4 ( 1 avg)
% 1.33/1.40 % Maximal term depth : 3 ( 1 avg)
% 1.33/1.40 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 1.33/1.40 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 1.33/1.40 % Number of variables : 22 ( 0 sgn)
% 1.33/1.40 % SPC : CNF_UNS_RFO_SEQ_HRN
% 1.33/1.40
% 1.33/1.40 % Comments :
% 1.33/1.40 %--------------------------------------------------------------------------
% 1.33/1.40 %----Include group theory axioms
% 1.33/1.40 include('Axioms/GRP003-0.ax').
% 1.33/1.40 %--------------------------------------------------------------------------
% 1.33/1.40 cnf(prove_X_times_inverse_X_is_id,negated_conjecture,
% 1.33/1.40 multiply(a,inverse(a)) != identity ).
% 1.33/1.40
% 1.33/1.40 %--------------------------------------------------------------------------
% 1.33/1.40 %-------------------------------------------
% 1.33/1.40 % Proof found
% 1.33/1.40 % SZS status Theorem for theBenchmark
% 1.33/1.40 % SZS output start Proof
% 1.33/1.40 %ClaNum:18(EqnAxiom:9)
% 1.33/1.40 %VarNum:44(SingletonVarNum:22)
% 1.33/1.40 %MaxLitNum:4
% 1.33/1.40 %MaxfuncDepth:2
% 1.33/1.40 %SharedTerms:5
% 1.33/1.40 %goalClause: 15
% 1.33/1.40 %singleGoalClaCount:1
% 1.33/1.40 [15]~E(f4(a2,f3(a2)),a1)
% 1.33/1.40 [10]P1(x101,a1,x101)
% 1.33/1.40 [11]P1(a1,x111,x111)
% 1.33/1.40 [12]P1(x121,f3(x121),a1)
% 1.33/1.41 [13]P1(f3(x131),x131,a1)
% 1.33/1.41 [14]P1(x141,x142,f4(x141,x142))
% 1.33/1.41 [16]~P1(x163,x164,x161)+E(x161,x162)+~P1(x163,x164,x162)
% 1.33/1.41 [17]~P1(x176,x174,x171)+P1(x171,x172,x173)+~P1(x174,x172,x175)+~P1(x176,x175,x173)
% 1.33/1.41 [18]~P1(x181,x186,x184)+P1(x181,x182,x183)+~P1(x184,x185,x183)+~P1(x186,x185,x182)
% 1.33/1.41 %EqnAxiom
% 1.33/1.41 [1]E(x11,x11)
% 1.33/1.41 [2]E(x22,x21)+~E(x21,x22)
% 1.33/1.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.33/1.41 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 1.33/1.41 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 1.33/1.41 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 1.33/1.41 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 1.33/1.41 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 1.33/1.41 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 1.33/1.41
% 1.33/1.41 %-------------------------------------------
% 1.33/1.41 cnf(19,plain,
% 1.33/1.41 (E(x191,f4(x191,a1))),
% 1.33/1.41 inference(scs_inference,[],[10,14,16])).
% 1.33/1.41 cnf(20,plain,
% 1.33/1.41 (P1(x201,x202,f4(x201,x202))),
% 1.33/1.41 inference(rename_variables,[],[14])).
% 1.33/1.41 cnf(22,plain,
% 1.33/1.41 (P1(f4(x221,a1),a1,x221)),
% 1.33/1.41 inference(scs_inference,[],[10,14,16,7])).
% 1.33/1.41 cnf(24,plain,
% 1.33/1.41 (P1(x241,a1,x241)),
% 1.33/1.41 inference(rename_variables,[],[10])).
% 1.33/1.41 cnf(25,plain,
% 1.33/1.41 (P1(x251,f3(x251),f4(a1,a1))),
% 1.33/1.41 inference(scs_inference,[],[10,14,12,16,7,8,9])).
% 1.33/1.41 cnf(26,plain,
% 1.33/1.41 (P1(x261,f4(a1,a1),x261)),
% 1.33/1.41 inference(scs_inference,[],[10,24,14,20,12,16,7,8,9,18])).
% 1.33/1.41 cnf(30,plain,
% 1.33/1.41 (~E(f4(a2,f3(a2)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[15,10,24,14,20,12,16,7,8,9,18,2,3])).
% 1.33/1.42 cnf(31,plain,
% 1.33/1.42 (E(f4(x311,a1),x311)),
% 1.33/1.42 inference(scs_inference,[],[19,2])).
% 1.33/1.42 cnf(32,plain,
% 1.33/1.42 (E(f3(f4(a1,a1)),a1)),
% 1.33/1.42 inference(scs_inference,[],[19,26,13,2,16])).
% 1.33/1.42 cnf(34,plain,
% 1.33/1.42 (P1(x341,f4(a1,a1),x341)),
% 1.33/1.42 inference(rename_variables,[],[26])).
% 1.33/1.42 cnf(37,plain,
% 1.33/1.42 (P1(x371,f4(a1,a1),f4(x371,a1))),
% 1.33/1.42 inference(scs_inference,[],[15,19,26,34,13,2,16,3,9])).
% 1.33/1.42 cnf(38,plain,
% 1.33/1.42 (P1(x381,f4(a1,a1),x381)),
% 1.33/1.42 inference(rename_variables,[],[26])).
% 1.33/1.42 cnf(39,plain,
% 1.33/1.42 (P1(f4(x391,a1),f4(a1,a1),x391)),
% 1.33/1.42 inference(scs_inference,[],[15,19,26,34,38,13,2,16,3,9,7])).
% 1.33/1.42 cnf(40,plain,
% 1.33/1.42 (P1(x401,f4(a1,a1),x401)),
% 1.33/1.42 inference(rename_variables,[],[26])).
% 1.33/1.42 cnf(41,plain,
% 1.33/1.42 (P1(x411,f4(f4(a1,a1),a1),x411)),
% 1.33/1.42 inference(scs_inference,[],[15,19,26,34,38,40,13,2,16,3,9,7,8])).
% 1.33/1.42 cnf(43,plain,
% 1.33/1.42 (P1(a1,f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[15,19,26,34,38,40,25,11,13,2,16,3,9,7,8,17])).
% 1.33/1.42 cnf(45,plain,
% 1.33/1.42 (P1(x451,f4(a1,a1),x451)),
% 1.33/1.42 inference(rename_variables,[],[26])).
% 1.33/1.42 cnf(48,plain,
% 1.33/1.42 (P1(x481,f4(f4(a1,a1),f4(a1,a1)),x481)),
% 1.33/1.42 inference(scs_inference,[],[15,19,26,34,38,40,45,25,11,13,14,2,16,3,9,7,8,17,18])).
% 1.33/1.42 cnf(51,plain,
% 1.33/1.42 (E(a1,f3(f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[32,2])).
% 1.33/1.42 cnf(52,plain,
% 1.33/1.42 (E(f4(f4(x521,a1),a1),x521)),
% 1.33/1.42 inference(scs_inference,[],[32,37,39,2,16])).
% 1.33/1.42 cnf(55,plain,
% 1.33/1.42 (P1(x551,f4(f4(a1,a1),f4(a1,a1)),f4(x551,a1))),
% 1.33/1.42 inference(scs_inference,[],[31,32,48,37,39,2,16,7])).
% 1.33/1.42 cnf(56,plain,
% 1.33/1.42 (P1(x561,f4(f4(a1,a1),f4(a1,a1)),x561)),
% 1.33/1.42 inference(rename_variables,[],[48])).
% 1.33/1.42 cnf(57,plain,
% 1.33/1.42 (~E(f4(a2,f3(a2)),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[15,31,32,48,37,39,2,16,7,3])).
% 1.33/1.42 cnf(58,plain,
% 1.33/1.42 (P1(f4(x581,a1),f4(f4(a1,a1),f4(a1,a1)),x581)),
% 1.33/1.42 inference(scs_inference,[],[15,31,32,48,56,37,39,2,16,7,3,9])).
% 1.33/1.42 cnf(59,plain,
% 1.33/1.42 (P1(x591,f4(f4(a1,a1),f4(a1,a1)),x591)),
% 1.33/1.42 inference(rename_variables,[],[48])).
% 1.33/1.42 cnf(60,plain,
% 1.33/1.42 (P1(a1,x601,f4(x601,a1))),
% 1.33/1.42 inference(scs_inference,[],[15,31,32,48,56,37,39,11,2,16,7,3,9,8])).
% 1.33/1.42 cnf(61,plain,
% 1.33/1.42 (P1(a1,x611,x611)),
% 1.33/1.42 inference(rename_variables,[],[11])).
% 1.33/1.42 cnf(62,plain,
% 1.33/1.42 (P1(a1,f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[15,31,32,48,56,59,41,37,39,11,61,2,16,7,3,9,8,17])).
% 1.33/1.42 cnf(64,plain,
% 1.33/1.42 (P1(x641,f4(f4(a1,a1),f4(a1,a1)),x641)),
% 1.33/1.42 inference(rename_variables,[],[48])).
% 1.33/1.42 cnf(67,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[15,31,32,48,56,59,64,41,37,39,25,11,61,2,16,7,3,9,8,17,18])).
% 1.33/1.42 cnf(71,plain,
% 1.33/1.42 (E(x711,f4(f4(x711,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[52,2])).
% 1.33/1.42 cnf(72,plain,
% 1.33/1.42 (E(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[52,67,26,2,16])).
% 1.33/1.42 cnf(75,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[52,31,67,26,2,16,9])).
% 1.33/1.42 cnf(76,plain,
% 1.33/1.42 (E(f4(x761,a1),x761)),
% 1.33/1.42 inference(rename_variables,[],[31])).
% 1.33/1.42 cnf(77,plain,
% 1.33/1.42 (P1(f3(f4(a1,a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[52,51,31,67,43,26,2,16,9,7])).
% 1.33/1.42 cnf(78,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[52,51,31,76,67,43,26,2,16,9,7,8])).
% 1.33/1.42 cnf(80,plain,
% 1.33/1.42 (P1(f4(f4(x801,a1),a1),f4(f4(a1,a1),f4(a1,a1)),x801)),
% 1.33/1.42 inference(scs_inference,[],[52,51,31,76,67,55,58,43,48,26,2,16,9,7,8,17])).
% 1.33/1.42 cnf(84,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,a1)),
% 1.33/1.42 inference(scs_inference,[],[52,51,31,76,67,55,58,43,48,26,2,16,9,7,8,17,18])).
% 1.33/1.42 cnf(87,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[72,2])).
% 1.33/1.42 cnf(88,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),f4(a1,a1)),a1)),
% 1.33/1.42 inference(scs_inference,[],[72,62,41,2,16])).
% 1.33/1.42 cnf(91,plain,
% 1.33/1.42 (~E(f4(a2,f3(a2)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[72,30,62,41,2,16,3])).
% 1.33/1.42 cnf(92,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[72,71,30,84,62,41,2,16,3,9])).
% 1.33/1.42 cnf(93,plain,
% 1.33/1.42 (E(x931,f4(f4(x931,a1),a1))),
% 1.33/1.42 inference(rename_variables,[],[71])).
% 1.33/1.42 cnf(94,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),x941,f4(x941,a1))),
% 1.33/1.42 inference(scs_inference,[],[72,71,93,30,84,62,60,41,2,16,3,9,7])).
% 1.33/1.42 cnf(95,plain,
% 1.33/1.42 (E(x951,f4(f4(x951,a1),a1))),
% 1.33/1.42 inference(rename_variables,[],[71])).
% 1.33/1.42 cnf(96,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[72,71,93,95,30,84,62,60,41,2,16,3,9,7,8])).
% 1.33/1.42 cnf(98,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[72,71,93,95,30,80,84,62,60,41,2,16,3,9,7,8,17])).
% 1.33/1.42 cnf(102,plain,
% 1.33/1.42 (P1(f3(f4(a1,a1)),a1,f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[72,71,93,95,77,30,80,84,62,60,41,37,13,2,16,3,9,7,8,17,18])).
% 1.33/1.42 cnf(106,plain,
% 1.33/1.42 (E(a1,f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[88,2])).
% 1.33/1.42 cnf(107,plain,
% 1.33/1.42 (P1(f4(a1,a1),f4(f4(a1,a1),a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[87,88,96,2,7])).
% 1.33/1.42 cnf(108,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[87,88,72,94,96,2,7,9])).
% 1.33/1.42 cnf(109,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),x1091,f4(x1091,a1))),
% 1.33/1.42 inference(rename_variables,[],[94])).
% 1.33/1.42 cnf(110,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[87,88,72,71,94,78,96,2,7,9,8])).
% 1.33/1.42 cnf(112,plain,
% 1.33/1.42 (P1(f4(a1,a1),f3(a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[87,88,72,71,94,109,78,96,12,2,7,9,8,17])).
% 1.33/1.42 cnf(117,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[87,88,72,71,98,94,109,78,96,55,12,2,7,9,8,17,18])).
% 1.33/1.42 cnf(120,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[117,26,16])).
% 1.33/1.42 cnf(123,plain,
% 1.33/1.42 (P1(a1,a1,f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[32,117,102,26,16,7])).
% 1.33/1.42 cnf(124,plain,
% 1.33/1.42 (P1(f3(f4(a1,a1)),a1,a1)),
% 1.33/1.42 inference(scs_inference,[],[52,32,117,102,26,16,7,9])).
% 1.33/1.42 cnf(126,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 1.33/1.42 inference(scs_inference,[],[52,32,72,117,102,75,26,16,7,9,8])).
% 1.33/1.42 cnf(127,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[52,32,72,117,102,112,75,26,16,7,9,8,17])).
% 1.33/1.42 cnf(129,plain,
% 1.33/1.42 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[52,32,72,117,102,112,75,22,77,26,16,7,9,8,17,18])).
% 1.33/1.42 cnf(132,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[52,32,72,117,102,112,75,22,77,26,16,7,9,8,17,18,2])).
% 1.33/1.42 cnf(133,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[127,94,16])).
% 1.33/1.42 cnf(134,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),x1341,f4(x1341,a1))),
% 1.33/1.42 inference(rename_variables,[],[94])).
% 1.33/1.42 cnf(136,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[132,127,94,16,3])).
% 1.33/1.42 cnf(137,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f4(f4(a1,a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[132,110,127,94,16,3,7])).
% 1.33/1.42 cnf(138,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[132,120,110,127,94,16,3,7,9])).
% 1.33/1.42 cnf(139,plain,
% 1.33/1.42 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),a1)),
% 1.33/1.42 inference(scs_inference,[],[132,120,110,127,129,94,16,3,7,9,8])).
% 1.33/1.42 cnf(140,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f3(f3(a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[132,120,110,127,129,94,39,25,16,3,7,9,8,17])).
% 1.33/1.42 cnf(144,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),a1,f3(f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[132,120,110,127,129,124,94,134,39,22,25,16,3,7,9,8,17,18])).
% 1.33/1.42 cnf(148,plain,
% 1.33/1.42 (E(f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[132,120,110,127,129,124,94,134,39,22,25,16,3,7,9,8,17,18,2])).
% 1.33/1.42 cnf(149,plain,
% 1.33/1.42 (E(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[136,2])).
% 1.33/1.42 cnf(150,plain,
% 1.33/1.42 (~E(f4(a2,f3(a2)),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[148,136,57,2,3])).
% 1.33/1.42 cnf(151,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),f4(f4(a1,a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[148,136,133,137,57,2,3,7])).
% 1.33/1.42 cnf(152,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[148,136,133,137,57,2,3,7,8])).
% 1.33/1.42 cnf(153,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[148,136,133,137,57,92,2,3,7,8,9])).
% 1.33/1.42 cnf(154,plain,
% 1.33/1.42 (P1(f4(a1,a1),f3(a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[148,136,133,137,57,92,138,80,2,3,7,8,9,17])).
% 1.33/1.42 cnf(157,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f4(a1,a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[148,136,133,137,57,92,138,107,80,2,3,7,8,9,17,18])).
% 1.33/1.42 cnf(159,plain,
% 1.33/1.42 (E(f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[151,41,16])).
% 1.33/1.42 cnf(162,plain,
% 1.33/1.42 (~E(f4(a2,f3(a2)),f3(a1))),
% 1.33/1.42 inference(scs_inference,[],[19,151,150,41,16,3])).
% 1.33/1.42 cnf(164,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[106,19,151,157,150,41,16,3,9])).
% 1.33/1.42 cnf(165,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[106,120,19,151,152,157,150,41,16,3,9,7])).
% 1.33/1.42 cnf(166,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[106,120,19,151,152,157,150,41,16,3,9,7,8])).
% 1.33/1.42 cnf(167,plain,
% 1.33/1.42 (P1(f4(a1,a1),a1,f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[106,120,19,151,152,157,150,108,48,41,16,3,9,7,8,17])).
% 1.33/1.42 cnf(170,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),a1,f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[106,120,19,151,152,157,150,108,48,41,37,16,3,9,7,8,17,18])).
% 1.33/1.42 cnf(173,plain,
% 1.33/1.42 (E(f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[159,2])).
% 1.33/1.42 cnf(174,plain,
% 1.33/1.42 (E(f4(a1,a1),f3(a1))),
% 1.33/1.42 inference(scs_inference,[],[159,166,58,2,16])).
% 1.33/1.42 cnf(177,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),f4(a1,a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[159,87,166,58,2,16,8])).
% 1.33/1.42 cnf(178,plain,
% 1.33/1.42 (P1(a1,f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[159,87,52,164,166,58,2,16,8,7])).
% 1.33/1.42 cnf(179,plain,
% 1.33/1.42 (E(f4(f4(x1791,a1),a1),x1791)),
% 1.33/1.42 inference(rename_variables,[],[52])).
% 1.33/1.42 cnf(180,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),a1,a1)),
% 1.33/1.42 inference(scs_inference,[],[159,87,52,179,164,166,170,58,2,16,8,7,9])).
% 1.33/1.42 cnf(182,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[159,87,52,179,164,166,170,112,58,2,16,8,7,9,17])).
% 1.33/1.42 cnf(184,plain,
% 1.33/1.42 (P1(a1,f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[159,87,52,179,164,166,170,144,123,112,58,2,16,8,7,9,17,18])).
% 1.33/1.42 cnf(186,plain,
% 1.33/1.42 (E(f3(a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[174,2])).
% 1.33/1.42 cnf(187,plain,
% 1.33/1.42 (E(f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[174,184,11,2,16])).
% 1.33/1.42 cnf(188,plain,
% 1.33/1.42 (P1(a1,x1881,x1881)),
% 1.33/1.42 inference(rename_variables,[],[11])).
% 1.33/1.42 cnf(190,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1),f3(a1))),
% 1.33/1.42 inference(scs_inference,[],[174,165,184,11,2,16,9])).
% 1.33/1.42 cnf(191,plain,
% 1.33/1.42 (P1(a1,f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[174,88,165,184,11,2,16,9,7])).
% 1.33/1.42 cnf(192,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),f3(a1),f4(a1,a1))),
% 1.33/1.42 inference(scs_inference,[],[174,88,177,165,184,11,2,16,9,7,8])).
% 1.33/1.42 cnf(193,plain,
% 1.33/1.42 (P1(f4(a1,a1),f3(a1),f3(a1))),
% 1.33/1.42 inference(scs_inference,[],[174,88,177,165,184,112,39,11,2,16,9,7,8,17])).
% 1.33/1.42 cnf(196,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[174,88,177,165,126,184,112,39,11,188,2,16,9,7,8,17,18])).
% 1.33/1.42 cnf(199,plain,
% 1.33/1.42 (E(f4(f4(a1,a1),a1),f3(f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[187,2])).
% 1.33/1.42 cnf(200,plain,
% 1.33/1.42 (E(f4(f3(a1),a1),a1)),
% 1.33/1.42 inference(scs_inference,[],[187,167,22,2,16])).
% 1.33/1.42 cnf(203,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 1.33/1.42 inference(scs_inference,[],[187,149,190,167,22,2,16,8])).
% 1.33/1.42 cnf(204,plain,
% 1.33/1.42 (P1(f4(f3(a1),a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.42 inference(scs_inference,[],[187,149,136,182,190,167,22,2,16,8,7])).
% 1.33/1.42 cnf(205,plain,
% 1.33/1.42 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f3(a1),a1))),
% 1.33/1.42 inference(scs_inference,[],[187,149,136,182,190,167,22,2,16,8,7,9])).
% 1.33/1.43 cnf(206,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f4(f3(a1),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[187,149,136,182,192,190,167,14,22,2,16,8,7,9,18])).
% 1.33/1.43 cnf(209,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[187,149,136,182,192,190,167,14,22,12,2,16,8,7,9,18,17])).
% 1.33/1.43 cnf(212,plain,
% 1.33/1.43 (E(a1,f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[200,2])).
% 1.33/1.43 cnf(213,plain,
% 1.33/1.43 (E(f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[200,203,48,2,16])).
% 1.33/1.43 cnf(216,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[200,87,196,203,48,2,16,7])).
% 1.33/1.43 cnf(217,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[173,200,87,196,203,205,48,2,16,7,9])).
% 1.33/1.43 cnf(218,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[173,200,87,196,203,205,48,2,16,7,9,8])).
% 1.33/1.43 cnf(219,plain,
% 1.33/1.43 (P1(f3(a1),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[173,200,87,196,203,205,182,48,2,16,7,9,8,17])).
% 1.33/1.43 cnf(221,plain,
% 1.33/1.43 (P1(a1,f4(f3(a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[173,200,87,196,209,203,205,193,191,182,48,2,16,7,9,8,17,18])).
% 1.33/1.43 cnf(223,plain,
% 1.33/1.43 (E(f4(f4(a1,a1),f4(a1,a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[213,2])).
% 1.33/1.43 cnf(224,plain,
% 1.33/1.43 (E(a1,f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[213,180,22,2,16])).
% 1.33/1.43 cnf(227,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[213,159,216,180,22,2,16,8])).
% 1.33/1.43 cnf(228,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[213,159,132,216,204,180,22,2,16,8,9])).
% 1.33/1.43 cnf(229,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(f3(a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[199,213,159,132,216,140,204,180,22,2,16,8,9,7])).
% 1.33/1.43 cnf(230,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[199,213,159,132,216,140,204,180,177,22,2,16,8,9,7,18])).
% 1.33/1.43 cnf(232,plain,
% 1.33/1.43 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(f3(a1),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[199,213,159,132,216,140,206,204,180,177,112,22,2,16,8,9,7,18,17])).
% 1.33/1.43 cnf(234,plain,
% 1.33/1.43 (E(f3(a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[224,2])).
% 1.33/1.43 cnf(235,plain,
% 1.33/1.43 (E(f4(f4(a1,a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[224,170,22,2,16])).
% 1.33/1.43 cnf(238,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[224,149,227,170,22,2,16,9])).
% 1.33/1.43 cnf(239,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[224,149,159,230,227,170,22,2,16,9,7])).
% 1.33/1.43 cnf(240,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[224,149,159,230,227,170,22,2,16,9,7,8])).
% 1.33/1.43 cnf(241,plain,
% 1.33/1.43 (P1(f3(a1),f4(f3(a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[224,149,159,230,227,218,170,22,2,16,9,7,8,17])).
% 1.33/1.43 cnf(243,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[224,149,159,230,227,217,218,139,170,60,22,2,16,9,7,8,17,18])).
% 1.33/1.43 cnf(246,plain,
% 1.33/1.43 (E(f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[235,2])).
% 1.33/1.43 cnf(247,plain,
% 1.33/1.43 (E(f4(f3(a1),a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[235,243,26,2,16])).
% 1.33/1.43 cnf(250,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[235,187,243,26,2,16,7])).
% 1.33/1.43 cnf(251,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[235,187,148,243,238,26,2,16,7,8])).
% 1.33/1.43 cnf(252,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[235,187,148,243,238,26,2,16,7,8,9])).
% 1.33/1.43 cnf(253,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[235,187,148,243,238,239,26,2,16,7,8,9,18])).
% 1.33/1.43 cnf(255,plain,
% 1.33/1.43 (P1(a1,f4(f3(a1),a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[235,187,148,243,238,239,241,154,26,2,16,7,8,9,18,17])).
% 1.33/1.43 cnf(257,plain,
% 1.33/1.43 (E(f3(f4(a1,a1)),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[247,2])).
% 1.33/1.43 cnf(258,plain,
% 1.33/1.43 (E(f4(a1,a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[247,253,48,2,16])).
% 1.33/1.43 cnf(261,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[247,199,251,253,48,2,16,8])).
% 1.33/1.43 cnf(262,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[247,223,199,251,253,48,2,16,8,9])).
% 1.33/1.43 cnf(263,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f4(f3(a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[247,223,212,199,251,253,221,48,2,16,8,9,7])).
% 1.33/1.43 cnf(264,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[247,223,212,199,251,253,221,138,55,48,2,16,8,9,7,17])).
% 1.33/1.43 cnf(267,plain,
% 1.33/1.43 (P1(a1,f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[247,223,212,199,251,252,253,221,138,43,216,55,48,2,16,8,9,7,17,18])).
% 1.33/1.43 cnf(269,plain,
% 1.33/1.43 (E(f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[258,2])).
% 1.33/1.43 cnf(270,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[258,223,261,2,9])).
% 1.33/1.43 cnf(271,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[258,106,223,261,255,2,9,7])).
% 1.33/1.43 cnf(272,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[258,106,223,261,255,240,2,9,7,8])).
% 1.33/1.43 cnf(273,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[258,106,223,261,255,240,263,153,2,9,7,8,18])).
% 1.33/1.43 cnf(275,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[258,106,223,261,250,255,240,263,153,80,2,9,7,8,18,17])).
% 1.33/1.43 cnf(278,plain,
% 1.33/1.43 (E(f3(a1),f4(f3(a1),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[219,14,16])).
% 1.33/1.43 cnf(281,plain,
% 1.33/1.43 (P1(f3(a1),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[186,219,14,16,9])).
% 1.33/1.43 cnf(282,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f4(a1,a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[269,186,219,275,14,16,9,8])).
% 1.33/1.43 cnf(283,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f3(a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[269,186,219,229,275,14,16,9,8,7])).
% 1.33/1.43 cnf(284,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[269,186,219,229,275,11,14,16,9,8,7,18])).
% 1.33/1.43 cnf(287,plain,
% 1.33/1.43 (P1(f3(a1),f3(f3(a1)),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[269,186,219,229,275,25,37,11,14,16,9,8,7,18,17])).
% 1.33/1.43 cnf(291,plain,
% 1.33/1.43 (E(f4(f3(a1),f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[269,186,219,229,275,25,37,11,14,16,9,8,7,18,17,2])).
% 1.33/1.43 cnf(292,plain,
% 1.33/1.43 (E(f4(f4(a1,a1),a1),f4(f3(a1),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[269,186,235,219,229,275,25,37,11,14,16,9,8,7,18,17,2,3])).
% 1.33/1.43 cnf(293,plain,
% 1.33/1.43 (E(f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[292,2])).
% 1.33/1.43 cnf(295,plain,
% 1.33/1.43 (E(f3(f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[292,291,162,284,39,2,3,16])).
% 1.33/1.43 cnf(298,plain,
% 1.33/1.43 (P1(f4(f3(a1),f3(a1)),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[292,291,162,232,284,39,2,3,16,9])).
% 1.33/1.43 cnf(299,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[292,291,173,162,232,284,39,2,3,16,9,7])).
% 1.33/1.43 cnf(300,plain,
% 1.33/1.43 (P1(a1,f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[292,291,173,162,232,284,267,39,2,3,16,9,7,8])).
% 1.33/1.43 cnf(301,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[292,291,173,162,232,284,267,262,41,39,2,3,16,9,7,8,18])).
% 1.33/1.43 cnf(304,plain,
% 1.33/1.43 (P1(a1,f3(f3(a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[292,291,173,162,232,283,284,267,262,282,41,39,2,3,16,9,7,8,18,17])).
% 1.33/1.43 cnf(306,plain,
% 1.33/1.43 (E(f3(a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[295,2])).
% 1.33/1.43 cnf(308,plain,
% 1.33/1.43 (E(f3(f3(a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[295,299,162,26,2,3,16])).
% 1.33/1.43 cnf(309,plain,
% 1.33/1.43 (P1(x3091,f4(a1,a1),x3091)),
% 1.33/1.43 inference(rename_variables,[],[26])).
% 1.33/1.43 cnf(311,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(a1,a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[295,299,162,26,2,3,16,9])).
% 1.33/1.43 cnf(312,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[295,258,299,162,26,2,3,16,9,7])).
% 1.33/1.43 cnf(313,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[295,258,299,162,26,2,3,16,9,7,8])).
% 1.33/1.43 cnf(314,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f3(a1)),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[295,258,299,162,26,309,2,3,16,9,7,8,18])).
% 1.33/1.43 cnf(317,plain,
% 1.33/1.43 (P1(f3(a1),f3(f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[295,258,299,304,273,162,26,309,2,3,16,9,7,8,18,17])).
% 1.33/1.43 cnf(319,plain,
% 1.33/1.43 (E(f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[308,2])).
% 1.33/1.43 cnf(320,plain,
% 1.33/1.43 (E(f3(f3(a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[308,312,13,2,16])).
% 1.33/1.43 cnf(321,plain,
% 1.33/1.43 (P1(f3(x3211),x3211,a1)),
% 1.33/1.43 inference(rename_variables,[],[13])).
% 1.33/1.43 cnf(323,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f3(f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[246,308,312,317,13,2,16,7])).
% 1.33/1.43 cnf(324,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(a1,a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[246,308,312,317,13,2,16,7,9])).
% 1.33/1.43 cnf(325,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[257,246,308,312,313,317,13,2,16,7,9,8])).
% 1.33/1.43 cnf(326,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f4(f3(a1),a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[257,246,308,312,313,317,272,13,321,2,16,7,9,8,18])).
% 1.33/1.43 cnf(327,plain,
% 1.33/1.43 (P1(f3(x3271),x3271,a1)),
% 1.33/1.43 inference(rename_variables,[],[13])).
% 1.33/1.43 cnf(329,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f3(f3(a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[257,246,308,312,313,317,272,283,13,321,327,2,16,7,9,8,18,17])).
% 1.33/1.43 cnf(332,plain,
% 1.33/1.43 (E(a1,f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[320,2])).
% 1.33/1.43 cnf(333,plain,
% 1.33/1.43 (E(f4(a1,a1),f4(f3(f4(a1,a1)),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[320,324,14,2,16])).
% 1.33/1.43 cnf(336,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[320,324,325,14,2,16,9])).
% 1.33/1.43 cnf(337,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f4(a1,a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[319,320,324,325,311,14,2,16,9,7])).
% 1.33/1.43 cnf(338,plain,
% 1.33/1.43 (P1(f4(a1,a1),a1,f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[319,320,200,324,325,311,14,2,16,9,7,8])).
% 1.33/1.43 cnf(339,plain,
% 1.33/1.43 (P1(f3(f3(a1)),a1,a1)),
% 1.33/1.43 inference(scs_inference,[],[319,320,200,324,325,311,329,304,14,2,16,9,7,8,18])).
% 1.33/1.43 cnf(341,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f3(a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[319,320,200,324,325,311,329,209,304,14,2,16,9,7,8,18,17])).
% 1.33/1.43 cnf(343,plain,
% 1.33/1.43 (E(f3(a1),f4(f3(f4(a1,a1)),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[319,320,200,186,324,325,311,329,209,304,14,2,16,9,7,8,18,17,3])).
% 1.33/1.43 cnf(345,plain,
% 1.33/1.43 (E(a1,f4(f3(f4(a1,a1)),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[333,343,224,2,3])).
% 1.33/1.43 cnf(346,plain,
% 1.33/1.43 (P1(a1,f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[333,343,224,88,264,2,3,7])).
% 1.33/1.43 cnf(347,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[333,343,224,199,88,264,2,3,7,9])).
% 1.33/1.43 cnf(348,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[333,343,257,224,199,88,264,270,2,3,7,9,8])).
% 1.33/1.43 cnf(349,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[333,343,257,224,199,88,264,270,98,193,2,3,7,9,8,18])).
% 1.33/1.43 cnf(351,plain,
% 1.33/1.43 (P1(f3(f3(a1)),a1,f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[333,343,257,224,199,88,314,264,270,339,98,193,10,2,3,7,9,8,18,17])).
% 1.33/1.43 cnf(355,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[345,308,341,2,9])).
% 1.33/1.43 cnf(356,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[345,292,308,341,349,2,9,8])).
% 1.33/1.43 cnf(357,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[345,292,308,341,349,2,9,8,7])).
% 1.33/1.43 cnf(358,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[345,292,308,341,349,253,262,2,9,8,7,18])).
% 1.33/1.43 cnf(360,plain,
% 1.33/1.43 (P1(f3(a1),f3(a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[345,292,308,341,349,348,253,262,204,58,2,9,8,7,18,17])).
% 1.33/1.43 cnf(364,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[343,235,228,2,9])).
% 1.33/1.43 cnf(365,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[247,343,235,228,2,9,7])).
% 1.33/1.43 cnf(366,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f3(f3(a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[332,247,343,235,351,228,2,9,7,8])).
% 1.33/1.43 cnf(367,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[332,247,343,235,351,347,228,240,2,9,7,8,18])).
% 1.33/1.43 cnf(369,plain,
% 1.33/1.43 (P1(f3(a1),a1,f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[332,247,343,235,351,347,228,323,240,94,2,9,7,8,18,17])).
% 1.33/1.43 cnf(372,plain,
% 1.33/1.43 (P1(f3(a1),f3(a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[51,360,9])).
% 1.33/1.43 cnf(373,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[51,187,367,360,9,8])).
% 1.33/1.43 cnf(374,plain,
% 1.33/1.43 (P1(a1,f3(f3(a1)),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[51,187,320,367,366,360,9,8,7])).
% 1.33/1.43 cnf(375,plain,
% 1.33/1.43 (P1(f3(f3(a1)),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[51,187,320,367,366,360,337,311,9,8,7,18])).
% 1.33/1.43 cnf(377,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[51,187,320,367,366,360,337,184,311,127,9,8,7,18,17])).
% 1.33/1.43 cnf(379,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[269,377,9])).
% 1.33/1.43 cnf(380,plain,
% 1.33/1.43 (P1(f3(a1),f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[212,269,369,377,9,8])).
% 1.33/1.43 cnf(381,plain,
% 1.33/1.43 (P1(f3(f3(a1)),a1,f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[306,212,269,369,377,9,8,7])).
% 1.33/1.43 cnf(382,plain,
% 1.33/1.43 (P1(a1,f4(f4(a1,a1),a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[306,212,269,373,369,377,178,110,9,8,7,18])).
% 1.33/1.43 cnf(384,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),a1,a1)),
% 1.33/1.43 inference(scs_inference,[],[306,212,269,373,369,377,178,110,144,12,9,8,7,18,17])).
% 1.33/1.43 cnf(387,plain,
% 1.33/1.43 (E(f4(a1,a1),f4(f3(f4(a1,a1)),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[379,14,16])).
% 1.33/1.43 cnf(390,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(f3(a1),f3(a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[234,379,356,14,16,9])).
% 1.33/1.43 cnf(391,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),a1,f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[234,379,356,14,16,9,8])).
% 1.33/1.43 cnf(392,plain,
% 1.33/1.43 (P1(a1,f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[234,379,380,356,14,16,9,8,7])).
% 1.33/1.43 cnf(393,plain,
% 1.33/1.43 (P1(a1,a1,f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[234,379,380,356,384,382,338,14,16,9,8,7,18])).
% 1.33/1.43 cnf(395,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f3(a1),a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[234,379,380,356,384,382,338,41,14,16,9,8,7,18,17])).
% 1.33/1.43 cnf(399,plain,
% 1.33/1.43 (P1(f3(a1),f3(a1),f4(f3(f4(a1,a1)),f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[387,281,9])).
% 1.33/1.43 cnf(400,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(a1,a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[387,173,395,281,9,8])).
% 1.33/1.43 cnf(401,plain,
% 1.33/1.43 (P1(f4(f3(a1),f3(a1)),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[278,387,173,395,281,9,8,7])).
% 1.33/1.43 cnf(402,plain,
% 1.33/1.43 (P1(f3(a1),f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[278,387,173,395,355,287,301,281,9,8,7,18])).
% 1.33/1.43 cnf(404,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f3(a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[278,387,173,395,365,355,287,301,281,13,9,8,7,18,17])).
% 1.33/1.43 cnf(407,plain,
% 1.33/1.43 (E(f3(f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[400,14,16])).
% 1.33/1.43 cnf(410,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[306,400,358,14,16,9])).
% 1.33/1.43 cnf(411,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f3(f3(a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[306,400,404,358,14,16,9,8])).
% 1.33/1.43 cnf(412,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f3(a1),f4(a1,a1))),
% 1.33/1.43 inference(scs_inference,[],[293,306,400,404,401,358,14,16,9,8,7])).
% 1.33/1.43 cnf(413,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f3(a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[293,306,400,357,404,401,358,14,16,9,8,7,18])).
% 1.33/1.43 cnf(415,plain,
% 1.33/1.43 (P1(f3(f4(a1,a1)),f3(f4(a1,a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[293,306,400,357,404,401,358,261,58,14,16,9,8,7,18,17])).
% 1.33/1.43 cnf(418,plain,
% 1.33/1.43 (E(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[293,306,400,357,404,401,358,261,58,14,16,9,8,7,18,17,2])).
% 1.33/1.43 cnf(419,plain,
% 1.33/1.43 (E(f3(f3(a1)),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[402,37,16])).
% 1.33/1.43 cnf(422,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[213,413,402,37,16,9])).
% 1.33/1.43 cnf(423,plain,
% 1.33/1.43 (P1(f3(a1),f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[213,413,402,372,37,16,9,8])).
% 1.33/1.43 cnf(424,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[213,413,402,372,37,16,9,8,7])).
% 1.33/1.43 cnf(425,plain,
% 1.33/1.43 (P1(f3(a1),f3(f4(a1,a1)),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[213,413,402,410,372,37,16,9,8,7,18])).
% 1.33/1.43 cnf(427,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[213,412,413,402,410,372,360,37,10,16,9,8,7,18,17])).
% 1.33/1.43 cnf(430,plain,
% 1.33/1.43 (E(f4(f3(a1),a1),f3(f3(a1)))),
% 1.33/1.43 inference(scs_inference,[],[213,412,413,402,410,372,360,37,10,16,9,8,7,18,17,2])).
% 1.33/1.43 cnf(431,plain,
% 1.33/1.43 (E(f3(f4(a1,a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[423,48,16])).
% 1.33/1.43 cnf(434,plain,
% 1.33/1.43 (P1(f4(a1,a1),f3(f3(a1)),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[418,422,423,48,16,9])).
% 1.33/1.43 cnf(435,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)),a1)),
% 1.33/1.43 inference(scs_inference,[],[418,407,422,423,415,48,16,9,7])).
% 1.33/1.43 cnf(436,plain,
% 1.33/1.43 (P1(f3(a1),f3(f4(a1,a1)),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[418,407,422,423,415,48,16,9,7,8])).
% 1.33/1.43 cnf(437,plain,
% 1.33/1.43 (P1(f3(a1),f4(a1,a1),f4(f4(a1,a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[418,407,422,423,425,391,415,381,48,16,9,7,8,18])).
% 1.33/1.43 cnf(439,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),a1)),
% 1.33/1.43 inference(scs_inference,[],[418,407,422,423,425,391,415,381,355,39,48,16,9,7,8,18,17])).
% 1.33/1.43 cnf(442,plain,
% 1.33/1.43 (E(f3(a1),f3(f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[418,407,422,423,425,391,415,381,355,39,48,16,9,7,8,18,17,2])).
% 1.33/1.43 cnf(443,plain,
% 1.33/1.43 (E(f3(f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.43 inference(scs_inference,[],[424,26,16])).
% 1.33/1.43 cnf(446,plain,
% 1.33/1.43 (P1(f3(a1),f3(f4(a1,a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[431,424,436,26,16,9])).
% 1.33/1.43 cnf(447,plain,
% 1.33/1.43 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[442,431,424,436,364,26,16,9,8])).
% 1.33/1.43 cnf(449,plain,
% 1.33/1.43 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f4(f3(a1),a1))),
% 1.33/1.43 inference(scs_inference,[],[442,431,424,427,437,436,364,326,250,26,16,9,8,7,18])).
% 1.33/1.43 cnf(451,plain,
% 1.33/1.43 (P1(f4(f4(a1,a1),a1),f3(a1),f3(a1))),
% 1.33/1.43 inference(scs_inference,[],[442,431,424,427,437,436,364,392,326,250,11,26,16,9,8,7,18,17])).
% 1.33/1.43 cnf(454,plain,
% 1.33/1.43 (E(f4(f4(a1,a1),f4(a1,a1)),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[442,431,424,427,437,436,364,392,326,250,11,26,16,9,8,7,18,17,2])).
% 1.33/1.44 cnf(455,plain,
% 1.33/1.44 (E(f4(f3(a1),a1),f4(f3(a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[300,11,16])).
% 1.33/1.44 cnf(458,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f4(a1,a1),a1),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[430,449,300,11,16,9])).
% 1.33/1.44 cnf(459,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f3(f4(a1,a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[430,454,449,435,300,11,16,9,7])).
% 1.33/1.44 cnf(460,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f4(f4(a1,a1),a1),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[430,454,246,449,435,375,300,11,16,9,7,8])).
% 1.33/1.44 cnf(461,plain,
% 1.33/1.44 (P1(f4(a1,a1),f3(a1),f3(f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[430,454,246,449,434,435,375,300,377,11,16,9,7,8,18])).
% 1.33/1.44 cnf(463,plain,
% 1.33/1.44 (P1(a1,f3(f4(a1,a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[430,454,246,449,434,435,375,439,446,300,377,11,16,9,7,8,18,17])).
% 1.33/1.44 cnf(465,plain,
% 1.33/1.44 (E(f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[430,454,246,449,434,435,375,439,446,300,377,11,16,9,7,8,18,17,2])).
% 1.33/1.44 cnf(466,plain,
% 1.33/1.44 (P1(f4(a1,a1),f3(a1),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[407,461,9])).
% 1.33/1.44 cnf(467,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f3(f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[407,278,461,9,8])).
% 1.33/1.44 cnf(468,plain,
% 1.33/1.44 (P1(f4(f3(a1),f3(a1)),f3(f4(a1,a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[455,407,278,447,461,9,8,7])).
% 1.33/1.44 cnf(469,plain,
% 1.33/1.44 (P1(a1,f3(a1),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[455,407,278,458,447,461,460,374,9,8,7,18])).
% 1.33/1.44 cnf(471,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f4(a1,a1),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[455,407,278,458,447,461,460,374,94,41,9,8,7,18,17])).
% 1.33/1.44 cnf(475,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f3(a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[257,467,9])).
% 1.33/1.44 cnf(476,plain,
% 1.33/1.44 (P1(f4(f3(a1),f3(a1)),f4(f3(a1),a1),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[257,467,468,9,8])).
% 1.33/1.44 cnf(477,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f4(f3(a1),a1),a1)),
% 1.33/1.44 inference(scs_inference,[],[454,257,467,468,271,9,8,7])).
% 1.33/1.44 cnf(478,plain,
% 1.33/1.44 (P1(a1,f4(f4(a1,a1),a1),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[454,257,467,468,271,346,393,341,9,8,7,18])).
% 1.33/1.44 cnf(480,plain,
% 1.33/1.44 (P1(f4(a1,a1),f3(f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[454,257,467,471,468,271,346,393,413,341,13,9,8,7,18,17])).
% 1.33/1.44 cnf(483,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[430,475,9])).
% 1.33/1.44 cnf(484,plain,
% 1.33/1.44 (P1(f4(f3(a1),f3(a1)),f3(f3(a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[430,475,476,9,8])).
% 1.33/1.44 cnf(485,plain,
% 1.33/1.44 (P1(f3(f4(a1,a1)),f4(f3(a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[430,418,475,476,390,9,8,7])).
% 1.33/1.44 cnf(486,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[430,418,475,476,390,232,192,9,8,7,18])).
% 1.33/1.44 cnf(488,plain,
% 1.33/1.44 (P1(f4(f3(a1),a1),f3(a1),a1)),
% 1.33/1.44 inference(scs_inference,[],[430,418,475,476,390,232,192,401,39,9,8,7,18,17])).
% 1.33/1.44 cnf(491,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),a1),f3(a1),f3(f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[442,451,9])).
% 1.33/1.44 cnf(492,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[455,442,336,451,9,8])).
% 1.33/1.44 cnf(493,plain,
% 1.33/1.44 (P1(f4(f3(a1),f3(a1)),f3(a1),a1)),
% 1.33/1.44 inference(scs_inference,[],[455,442,336,488,451,9,8,7])).
% 1.33/1.44 cnf(496,plain,
% 1.33/1.44 (P1(a1,f4(f3(a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[455,442,463,486,336,488,451,485,75,300,9,8,7,18,17])).
% 1.33/1.44 cnf(498,plain,
% 1.33/1.44 (E(a1,f4(f3(a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[496,11,16])).
% 1.33/1.44 cnf(502,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),a1),f4(f3(a1),a1),a1)),
% 1.33/1.44 inference(scs_inference,[],[419,345,496,411,154,11,16,9,8])).
% 1.33/1.44 cnf(503,plain,
% 1.33/1.44 (P1(f4(f3(a1),a1),f3(f3(a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[419,465,345,496,484,411,154,11,16,9,8,7])).
% 1.33/1.44 cnf(504,plain,
% 1.33/1.44 (P1(a1,f3(f4(a1,a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[419,465,345,491,496,484,411,478,154,375,11,16,9,8,7,18])).
% 1.33/1.44 cnf(506,plain,
% 1.33/1.44 (P1(f3(a1),f4(f3(a1),f3(a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[419,465,345,491,496,484,411,478,486,154,218,375,11,16,9,8,7,18,17])).
% 1.33/1.44 cnf(508,plain,
% 1.33/1.44 (E(f4(f3(a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[419,465,345,491,496,484,411,478,486,154,218,375,11,16,9,8,7,18,17,2])).
% 1.33/1.44 cnf(509,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[466,14,16])).
% 1.33/1.44 cnf(512,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[443,466,483,14,16,9])).
% 1.33/1.44 cnf(513,plain,
% 1.33/1.44 (P1(a1,a1,f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[443,32,466,483,504,14,16,9,8])).
% 1.33/1.44 cnf(514,plain,
% 1.33/1.44 (P1(a1,f3(f3(a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[443,200,32,466,483,503,504,14,16,9,8,7])).
% 1.33/1.44 cnf(515,plain,
% 1.33/1.44 (P1(f4(a1,a1),a1,f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[443,200,32,466,483,480,503,459,504,14,16,9,8,7,18])).
% 1.33/1.44 cnf(517,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[443,200,32,466,483,480,503,459,504,436,25,14,16,9,8,7,18,17])).
% 1.33/1.44 cnf(520,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[443,200,32,466,483,480,503,459,504,436,25,14,16,9,8,7,18,17,2])).
% 1.33/1.44 cnf(521,plain,
% 1.33/1.44 (E(f3(f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[443,200,32,466,483,480,503,459,504,436,25,14,16,9,8,7,18,17,2,3])).
% 1.33/1.44 cnf(522,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),f3(f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[521,2])).
% 1.33/1.44 cnf(523,plain,
% 1.33/1.44 (~E(f4(a2,f3(a2)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[520,521,91,2,3])).
% 1.33/1.44 cnf(524,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[520,509,521,91,512,2,3,9])).
% 1.33/1.44 cnf(525,plain,
% 1.33/1.44 (P1(f4(a1,a1),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[520,509,508,521,91,512,2,3,9,8])).
% 1.33/1.44 cnf(526,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f3(a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[520,509,508,521,91,517,512,2,3,9,8,7])).
% 1.33/1.44 cnf(527,plain,
% 1.33/1.44 (P1(f3(a1),a1,f4(f3(f4(a1,a1)),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[520,509,508,521,91,517,506,512,399,493,2,3,9,8,7,18])).
% 1.33/1.44 cnf(529,plain,
% 1.33/1.44 (P1(f3(a1),f4(f3(a1),a1),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[520,509,508,521,91,517,506,512,399,477,493,514,60,2,3,9,8,7,18,17])).
% 1.33/1.44 cnf(535,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f3(a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[498,492,527,13,16,9])).
% 1.33/1.44 cnf(536,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f4(a1,a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[498,407,526,492,527,13,16,9,8])).
% 1.33/1.44 cnf(537,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[498,522,407,526,492,527,13,16,9,8,7])).
% 1.33/1.44 cnf(541,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f3(a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[498,522,407,526,524,298,492,527,232,13,14,16,9,8,7,18,17])).
% 1.33/1.44 cnf(544,plain,
% 1.33/1.44 (E(f4(a1,a1),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[536,48,16])).
% 1.33/1.44 cnf(547,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),f3(a1)),f4(f4(a1,a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[293,536,535,48,16,9])).
% 1.33/1.44 cnf(548,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f3(a1)),f3(f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[293,454,536,535,48,16,9,8])).
% 1.33/1.44 cnf(549,plain,
% 1.33/1.44 (P1(f4(f3(a1),a1),f3(f4(a1,a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[293,419,454,536,535,537,48,16,9,8,7])).
% 1.33/1.44 cnf(550,plain,
% 1.33/1.44 (P1(f4(a1,a1),f3(f3(a1)),f4(f3(a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[293,419,454,536,535,537,525,469,205,48,16,9,8,7,18])).
% 1.33/1.44 cnf(552,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[293,419,454,536,535,537,525,469,126,205,10,48,16,9,8,7,18,17])).
% 1.33/1.44 cnf(555,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[544,2])).
% 1.33/1.44 cnf(556,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[544,552,55,2,16])).
% 1.33/1.44 cnf(559,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f4(a1,a1),f4(a1,a1)),f4(f4(a1,a1),f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[544,520,552,55,2,16,9])).
% 1.33/1.44 cnf(560,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f4(a1,a1)),f3(a1),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[544,520,552,541,55,2,16,9,7])).
% 1.33/1.44 cnf(561,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[544,520,509,552,541,55,2,16,9,7,8])).
% 1.33/1.44 cnf(564,plain,
% 1.33/1.44 (P1(a1,f3(f4(a1,a1)),f4(f4(a1,a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[544,520,509,549,552,541,502,513,527,55,94,2,16,9,7,8,18,17])).
% 1.33/1.44 cnf(567,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),a1),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[556,2])).
% 1.33/1.44 cnf(568,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[555,556,561,2,9])).
% 1.33/1.44 cnf(569,plain,
% 1.33/1.44 (P1(f4(a1,a1),f4(f3(a1),a1),f4(f4(a1,a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[555,556,465,547,561,2,9,8])).
% 1.33/1.44 cnf(571,plain,
% 1.33/1.44 (P1(f4(f3(a1),a1),f4(a1,a1),f3(f4(a1,a1)))),
% 1.33/1.44 inference(scs_inference,[],[555,556,333,465,547,561,515,395,239,2,9,8,7,18])).
% 1.33/1.44 cnf(574,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[567,319,569,568,9,7])).
% 1.33/1.44 cnf(576,plain,
% 1.33/1.44 (P1(f4(f3(a1),a1),f4(f4(a1,a1),a1),a1)),
% 1.33/1.44 inference(scs_inference,[],[567,319,247,569,571,568,529,326,9,7,8,18])).
% 1.33/1.44 cnf(578,plain,
% 1.33/1.44 (P1(f3(a1),f4(f4(a1,a1),f3(a1)),f3(a1))),
% 1.33/1.44 inference(scs_inference,[],[567,319,247,569,571,568,529,337,326,9,7,8,18,17])).
% 1.33/1.44 cnf(581,plain,
% 1.33/1.44 (P1(f4(f4(a1,a1),f3(a1)),f4(f4(a1,a1),f3(a1)),f4(a1,a1))),
% 1.33/1.44 inference(scs_inference,[],[521,567,574,564,9,7])).
% 1.33/1.44 cnf(583,plain,
% 1.33/1.44 (P1(f3(f3(a1)),f4(a1,a1),f4(f3(a1),a1))),
% 1.33/1.44 inference(scs_inference,[],[521,567,550,548,574,564,9,7,8,18])).
% 1.33/1.44 cnf(585,plain,
% 1.33/1.44 (P1(a1,f4(f4(a1,a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[521,567,550,548,574,564,578,439,9,7,8,18,17])).
% 1.33/1.44 cnf(587,plain,
% 1.33/1.44 (E(a1,f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[585,11,16])).
% 1.33/1.44 cnf(598,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),a1)),
% 1.33/1.44 inference(scs_inference,[],[522,567,559,581,583,560,585,576,541,166,60,11,16,9,7,8,18,17,2])).
% 1.33/1.44 cnf(639,plain,
% 1.33/1.44 (E(a1,f4(x6391,f3(x6391)))),
% 1.33/1.44 inference(scs_inference,[],[12,14,16])).
% 1.33/1.44 cnf(644,plain,
% 1.33/1.44 (P1(x6441,f3(x6441),a1)),
% 1.33/1.44 inference(rename_variables,[],[12])).
% 1.33/1.44 cnf(647,plain,
% 1.33/1.44 (P1(x6471,f3(x6471),f4(a1,a1))),
% 1.33/1.44 inference(rename_variables,[],[25])).
% 1.33/1.44 cnf(650,plain,
% 1.33/1.44 (P1(a1,f3(f3(x6501)),x6501)),
% 1.33/1.44 inference(scs_inference,[],[587,319,12,644,25,647,39,26,11,14,16,9,7,8,18,17])).
% 1.33/1.44 cnf(655,plain,
% 1.33/1.44 (E(f4(f4(a1,a1),f3(a1)),f4(a1,f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[587,598,319,12,644,25,647,39,26,11,14,16,9,7,8,18,17,2,3])).
% 1.33/1.44 cnf(656,plain,
% 1.33/1.44 (E(f4(a1,f3(a1)),f4(f4(a1,a1),f3(a1)))),
% 1.33/1.44 inference(scs_inference,[],[655,2])).
% 1.33/1.44 cnf(658,plain,
% 1.33/1.44 (E(f3(f3(x6581)),x6581)),
% 1.33/1.44 inference(scs_inference,[],[508,655,639,11,650,2,3,16])).
% 1.33/1.44 cnf(676,plain,
% 1.33/1.44 (E(f4(a1,a1),f4(x6761,f3(x6761)))),
% 1.33/1.44 inference(scs_inference,[],[658,656,25,523,14,2,3,16])).
% 1.33/1.44 cnf(692,plain,
% 1.33/1.44 ($false),
% 1.33/1.44 inference(scs_inference,[],[676,30,2]),
% 1.33/1.44 ['proof']).
% 1.33/1.44 % SZS output end Proof
% 1.33/1.44 % Total time :0.790000s
%------------------------------------------------------------------------------