%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP048-2 : 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 : n022.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:38 EDT 2024
% Result : Unsatisfiable 60.92s 60.97s
% Output : CNFRefutation 60.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP048-2 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n022.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 20 13:28:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 60.90/60.96 %-------------------------------------------
% 60.90/60.96 % File :CSE---1.7
% 60.90/60.96 % Problem :theBenchmark
% 60.90/60.96 % Transform :cnf
% 60.90/60.96 % Format :tptp:raw
% 60.90/60.96 % Command :java -jar mcs_scs.jar %d %s
% 60.90/60.96
% 60.90/60.96 % Result :Theorem 60.370000s
% 60.90/60.96 % Output :CNFRefutation 60.370000s
% 60.90/60.96 %-------------------------------------------
% 60.92/60.97 %--------------------------------------------------------------------------
% 60.92/60.97 % File : GRP048-2 : TPTP v8.2.0. Released v1.0.0.
% 60.92/60.97 % Domain : Group Theory
% 60.92/60.97 % Problem : Inverse substitution is dependent
% 60.92/60.97 % Version : [Ver92] axioms.
% 60.92/60.97 % English :
% 60.92/60.97
% 60.92/60.97 % Refs : [Ver92] Veroff (1992), Email to G. Sutcliffe
% 60.92/60.97 % Source : [Ver92]
% 60.92/60.97 % Names : - [Ver92]
% 60.92/60.97
% 60.92/60.97 % Status : Unsatisfiable
% 60.92/60.97 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.22 v5.3.0, 0.25 v5.2.0, 0.08 v5.1.0, 0.19 v5.0.0, 0.13 v4.0.1, 0.00 v2.7.0, 0.25 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.33 v2.1.0, 0.29 v2.0.0
% 60.92/60.97 % Syntax : Number of clauses : 9 ( 5 unt; 0 nHn; 6 RR)
% 60.92/60.97 % Number of literals : 19 ( 0 equ; 11 neg)
% 60.92/60.97 % Maximal clause size : 4 ( 2 avg)
% 60.92/60.97 % Maximal term depth : 2 ( 1 avg)
% 60.92/60.97 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 60.92/60.97 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 60.92/60.97 % Number of variables : 24 ( 0 sgn)
% 60.92/60.97 % SPC : CNF_UNS_RFO_NEQ_HRN
% 60.92/60.97
% 60.92/60.97 % Comments :
% 60.92/60.97 %--------------------------------------------------------------------------
% 60.92/60.97 %----Include Veroff's minimal axiom set
% 60.92/60.97 include('Axioms/GRP005-0.ax').
% 60.92/60.97 %--------------------------------------------------------------------------
% 60.92/60.97 cnf(a_equals_b,hypothesis,
% 60.92/60.97 equalish(a,b) ).
% 60.92/60.97
% 60.92/60.97 cnf(prove_inverse_substitution,negated_conjecture,
% 60.92/60.97 ~ equalish(inverse(a),inverse(b)) ).
% 60.92/60.97
% 60.92/60.97 %--------------------------------------------------------------------------
% 60.92/60.97 %-------------------------------------------
% 60.92/60.97 % Proof found
% 60.92/60.97 % SZS status Theorem for theBenchmark
% 60.92/60.97 % SZS output start Proof
% 60.92/60.97 %ClaNum:9(EqnAxiom:0)
% 60.92/60.97 %VarNum:48(SingletonVarNum:24)
% 60.92/60.97 %MaxLitNum:4
% 60.92/60.97 %MaxfuncDepth:1
% 60.92/60.97 %SharedTerms:7
% 60.92/60.97 %goalClause: 5
% 60.92/60.97 %singleGoalClaCount:1
% 60.92/60.97 [1]P1(a1,a2)
% 60.92/60.97 [5]~P1(f4(a1),f4(a2))
% 60.92/60.97 [2]P2(a3,x21,x21)
% 60.92/60.97 [3]P2(f4(x31),x31,a3)
% 60.92/60.97 [4]P2(x41,x42,f5(x41,x42))
% 60.92/60.97 [6]~P2(x61,x62,x64)+P2(x61,x62,x63)+~P1(x64,x63)
% 60.92/60.97 [7]~P2(x73,x74,x71)+P1(x71,x72)+~P2(x73,x74,x72)
% 60.92/60.97 [8]~P2(x86,x84,x81)+P2(x81,x82,x83)+~P2(x84,x82,x85)+~P2(x86,x85,x83)
% 60.92/60.97 [9]~P2(x91,x96,x94)+P2(x91,x92,x93)+~P2(x94,x95,x93)+~P2(x96,x95,x92)
% 60.92/60.97 %EqnAxiom
% 60.92/60.97
% 60.92/60.98 %-------------------------------------------
% 60.92/60.99 cnf(12,plain,
% 60.92/60.99 (P2(a3,a1,a2)),
% 60.92/60.99 inference(scs_inference,[],[2,1,7,6])).
% 60.92/60.99 cnf(13,plain,
% 60.92/60.99 (P2(a3,x131,x131)),
% 60.92/60.99 inference(rename_variables,[],[2])).
% 60.92/60.99 cnf(15,plain,
% 60.92/60.99 (P2(f5(f4(x151),a3),x151,a3)),
% 60.92/60.99 inference(scs_inference,[],[2,13,4,3,1,7,6,8])).
% 60.92/60.99 cnf(17,plain,
% 60.92/60.99 (P2(x171,x172,f5(x171,x172))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(19,plain,
% 60.92/60.99 (P2(a3,f5(a3,a3),a3)),
% 60.92/60.99 inference(scs_inference,[],[2,13,4,17,3,1,7,6,8,9])).
% 60.92/60.99 cnf(24,plain,
% 60.92/60.99 (P1(x241,f5(a3,x241))),
% 60.92/60.99 inference(scs_inference,[],[2,4,7])).
% 60.92/60.99 cnf(25,plain,
% 60.92/60.99 (P2(x251,x252,f5(x251,x252))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(32,plain,
% 60.92/60.99 (P2(a2,x321,a2)+~P2(a1,x321,a1)),
% 60.92/60.99 inference(scs_inference,[],[2,12,4,25,3,7,9,8])).
% 60.92/60.99 cnf(38,plain,
% 60.92/60.99 (P2(a3,f5(f4(x381),x381),a3)),
% 60.92/60.99 inference(scs_inference,[],[2,4,3,7,6])).
% 60.92/60.99 cnf(41,plain,
% 60.92/60.99 (P2(a3,x411,a3)+~P2(f5(a3,a3),x411,f5(a3,a3))),
% 60.92/60.99 inference(scs_inference,[],[2,4,3,19,7,6,8])).
% 60.92/60.99 cnf(46,plain,
% 60.92/60.99 (P1(a3,f5(f4(x461),x461))),
% 60.92/60.99 inference(scs_inference,[],[3,4,7])).
% 60.92/60.99 cnf(47,plain,
% 60.92/60.99 (P2(x471,x472,f5(x471,x472))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(49,plain,
% 60.92/60.99 (P2(f4(x491),x491,f5(a3,a3))),
% 60.92/60.99 inference(scs_inference,[],[3,24,4,7,6])).
% 60.92/60.99 cnf(52,plain,
% 60.92/60.99 (P2(a3,x521,f5(f4(a3),x521))),
% 60.92/60.99 inference(scs_inference,[],[3,24,2,4,47,7,6,8])).
% 60.92/60.99 cnf(54,plain,
% 60.92/60.99 (P2(f4(x541),x541,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(56,plain,
% 60.92/60.99 (P2(f4(a3),x561,x561)),
% 60.92/60.99 inference(scs_inference,[],[3,54,24,2,4,47,7,6,8,9])).
% 60.92/60.99 cnf(60,plain,
% 60.92/60.99 (P1(x601,f5(f4(a3),x601))),
% 60.92/60.99 inference(scs_inference,[],[2,52,7])).
% 60.92/60.99 cnf(63,plain,
% 60.92/60.99 (P2(f4(x631),x631,f5(f4(x632),x632))),
% 60.92/60.99 inference(scs_inference,[],[3,46,2,52,7,6])).
% 60.92/60.99 cnf(65,plain,
% 60.92/60.99 (P2(f4(f4(x651)),f5(a3,a3),x651)),
% 60.92/60.99 inference(scs_inference,[],[3,46,2,49,52,7,6,9])).
% 60.92/60.99 cnf(70,plain,
% 60.92/60.99 (P2(f4(x701),f5(x701,x702),x702)),
% 60.92/60.99 inference(scs_inference,[],[3,2,4,9])).
% 60.92/60.99 cnf(71,plain,
% 60.92/60.99 (P2(x711,x712,f5(x711,x712))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(73,plain,
% 60.92/60.99 (P1(f5(f4(x731),f5(x731,x732)),x732)),
% 60.92/60.99 inference(scs_inference,[],[3,2,4,71,9,7])).
% 60.92/60.99 cnf(76,plain,
% 60.92/60.99 (P1(a3,x761)+~P2(f5(a3,a3),x761,f5(a3,a3))),
% 60.92/60.99 inference(scs_inference,[],[2,41,7])).
% 60.92/60.99 cnf(77,plain,
% 60.92/60.99 (P2(a3,f5(f4(x771),f5(x771,x772)),x772)),
% 60.92/60.99 inference(scs_inference,[],[73,2,6])).
% 60.92/60.99 cnf(78,plain,
% 60.92/60.99 (P2(a3,x781,x781)),
% 60.92/60.99 inference(rename_variables,[],[2])).
% 60.92/60.99 cnf(80,plain,
% 60.92/60.99 (P2(a3,f5(a3,x801),x801)),
% 60.92/60.99 inference(scs_inference,[],[3,73,2,78,70,6,8])).
% 60.92/60.99 cnf(81,plain,
% 60.92/60.99 (P2(f4(x811),f5(x811,x812),x812)),
% 60.92/60.99 inference(rename_variables,[],[70])).
% 60.92/60.99 cnf(82,plain,
% 60.92/60.99 (P2(f4(x821),x821,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(83,plain,
% 60.92/60.99 (P2(a3,x831,x831)),
% 60.92/60.99 inference(rename_variables,[],[2])).
% 60.92/60.99 cnf(85,plain,
% 60.92/60.99 (P2(f4(f4(x851)),x852,f5(x851,x852))),
% 60.92/60.99 inference(scs_inference,[],[3,82,73,2,78,83,70,81,6,8,9])).
% 60.92/60.99 cnf(92,plain,
% 60.92/60.99 (P2(f4(x921),x921,x922)+~P2(f5(a3,a3),x922,f5(a3,a3))),
% 60.92/60.99 inference(scs_inference,[],[3,76,6])).
% 60.92/60.99 cnf(93,plain,
% 60.92/60.99 (P1(a3,f5(x931,f4(x931)))),
% 60.92/60.99 inference(scs_inference,[],[3,85,7])).
% 60.92/60.99 cnf(95,plain,
% 60.92/60.99 (P2(f4(x951),x951,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(97,plain,
% 60.92/60.99 (P2(f4(x971),x971,f5(x972,f4(x972)))),
% 60.92/60.99 inference(scs_inference,[],[3,95,85,7,6])).
% 60.92/60.99 cnf(100,plain,
% 60.92/60.99 (P2(f4(x1001),x1001,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(101,plain,
% 60.92/60.99 (P2(a3,x1011,x1011)),
% 60.92/60.99 inference(rename_variables,[],[2])).
% 60.92/60.99 cnf(103,plain,
% 60.92/60.99 (P2(f4(a3),x1031,f5(f4(x1032),f5(x1032,x1031)))),
% 60.92/60.99 inference(scs_inference,[],[3,95,100,2,101,77,85,7,6,8,9])).
% 60.92/60.99 cnf(109,plain,
% 60.92/60.99 (P2(f4(a3),x1091,f5(f4(x1092),f5(x1092,x1091)))),
% 60.92/60.99 inference(rename_variables,[],[103])).
% 60.92/60.99 cnf(110,plain,
% 60.92/60.99 (P2(f4(x1101),x1101,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(112,plain,
% 60.92/60.99 (P2(f4(x1121),x1121,f5(f4(x1122),f5(x1122,a3)))),
% 60.92/60.99 inference(scs_inference,[],[3,110,103,7,6])).
% 60.92/60.99 cnf(114,plain,
% 60.92/60.99 (P2(a3,x1141,f5(f4(x1142),f5(x1142,x1141)))),
% 60.92/60.99 inference(scs_inference,[],[3,110,2,103,109,7,6,8])).
% 60.92/60.99 cnf(116,plain,
% 60.92/60.99 (P2(f4(x1161),x1161,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(118,plain,
% 60.92/60.99 (P2(f4(f4(a3)),x1181,x1181)),
% 60.92/60.99 inference(scs_inference,[],[3,110,116,2,56,103,109,7,6,8,9])).
% 60.92/60.99 cnf(123,plain,
% 60.92/60.99 (P1(a3,f4(a3))),
% 60.92/60.99 inference(scs_inference,[],[3,118,7])).
% 60.92/60.99 cnf(125,plain,
% 60.92/60.99 (P2(f4(x1251),x1251,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(127,plain,
% 60.92/60.99 (P2(f4(x1271),x1271,f4(a3))),
% 60.92/60.99 inference(scs_inference,[],[3,125,118,7,6])).
% 60.92/60.99 cnf(129,plain,
% 60.92/60.99 (P2(a3,a3,f4(a3))),
% 60.92/60.99 inference(scs_inference,[],[3,125,2,118,7,6,8])).
% 60.92/60.99 cnf(130,plain,
% 60.92/60.99 (P2(f4(x1301),x1301,a3)),
% 60.92/60.99 inference(rename_variables,[],[3])).
% 60.92/60.99 cnf(131,plain,
% 60.92/60.99 (P2(a3,x1311,x1311)),
% 60.92/60.99 inference(rename_variables,[],[2])).
% 60.92/60.99 cnf(133,plain,
% 60.92/60.99 (P2(f4(a3),f5(f4(x1331),f5(x1331,x1332)),x1332)),
% 60.92/60.99 inference(scs_inference,[],[3,125,130,2,131,118,114,7,6,8,9])).
% 60.92/60.99 cnf(137,plain,
% 60.92/60.99 (P1(x1371,f5(f4(x1372),f5(x1372,x1371)))),
% 60.92/60.99 inference(scs_inference,[],[2,114,7])).
% 60.92/60.99 cnf(140,plain,
% 60.92/60.99 (P2(f4(f4(x1401)),f4(a3),x1401)),
% 60.92/60.99 inference(scs_inference,[],[3,2,127,114,7,9])).
% 60.92/60.99 cnf(144,plain,
% 60.92/60.99 (P1(a2,f5(a2,x1441))+~P2(a1,x1441,a1)),
% 60.92/60.99 inference(scs_inference,[],[4,32,7])).
% 60.92/60.99 cnf(145,plain,
% 60.92/60.99 (P2(a3,f4(a3),a3)),
% 60.92/60.99 inference(scs_inference,[],[3,129,9])).
% 60.92/60.99 cnf(149,plain,
% 60.92/60.99 (P2(f4(a3),x1491,f5(a3,x1491))),
% 60.92/60.99 inference(scs_inference,[],[3,2,80,9])).
% 60.92/60.99 cnf(159,plain,
% 60.92/60.99 (P2(f4(a3),f5(f4(a3),x1591),x1591)),
% 60.92/60.99 inference(scs_inference,[],[3,2,52,9])).
% 60.92/60.99 cnf(163,plain,
% 60.92/60.99 (P2(a3,f5(f4(a3),x1631),x1631)),
% 60.92/60.99 inference(scs_inference,[],[3,2,159,8])).
% 60.92/60.99 cnf(167,plain,
% 60.92/60.99 (~P2(f5(a1,f4(x1671)),x1671,a1)+P2(a2,a3,a2)),
% 60.92/60.99 inference(scs_inference,[],[3,4,32,9])).
% 60.92/60.99 cnf(172,plain,
% 60.92/60.99 (P1(f5(f4(x1721),x1721),f5(a3,a3))),
% 60.92/60.99 inference(scs_inference,[],[4,49,7])).
% 60.92/60.99 cnf(174,plain,
% 60.92/60.99 (P2(x1741,x1742,f5(x1741,x1742))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(176,plain,
% 60.92/60.99 (P2(x1761,x1762,f5(f4(a3),f5(x1761,x1762)))),
% 60.92/60.99 inference(scs_inference,[],[4,174,60,49,7,6])).
% 60.92/60.99 cnf(179,plain,
% 60.92/60.99 (P2(f5(x1791,a3),a3,f5(x1791,a3))),
% 60.92/60.99 inference(scs_inference,[],[4,174,60,2,49,7,6,8])).
% 60.92/60.99 cnf(189,plain,
% 60.92/60.99 (P1(f5(a2,x1891),a2)+~P2(a1,x1891,a1)),
% 60.92/60.99 inference(scs_inference,[],[4,32,7])).
% 60.92/60.99 cnf(192,plain,
% 60.92/60.99 (P2(x1921,x1922,f5(x1921,x1922))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(194,plain,
% 60.92/60.99 (P2(x1941,x1942,f5(a3,f5(x1941,x1942)))),
% 60.92/60.99 inference(scs_inference,[],[4,192,24,127,7,6])).
% 60.92/60.99 cnf(222,plain,
% 60.92/60.99 (P1(f5(a3,x2221),f5(f4(x2222),f5(x2222,x2221)))),
% 60.92/60.99 inference(scs_inference,[],[4,114,7])).
% 60.92/60.99 cnf(231,plain,
% 60.92/60.99 (P1(f5(a3,x2311),f5(f4(a3),x2311))),
% 60.92/60.99 inference(scs_inference,[],[4,52,7])).
% 60.92/60.99 cnf(233,plain,
% 60.92/60.99 (P2(x2331,x2332,f5(x2331,x2332))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(237,plain,
% 60.92/60.99 (P2(x2371,x2372,f5(x2371,x2372))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(238,plain,
% 60.92/60.99 (P2(x2381,x2382,f5(x2381,x2382))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(240,plain,
% 60.92/60.99 (P2(x2401,x2402,f5(f5(x2401,a3),x2402))),
% 60.92/60.99 inference(scs_inference,[],[4,233,238,237,2,159,52,7,8,9])).
% 60.92/60.99 cnf(246,plain,
% 60.92/60.99 (P1(f5(x2461,x2462),f5(f5(x2461,a3),x2462))),
% 60.92/60.99 inference(scs_inference,[],[4,240,7])).
% 60.92/60.99 cnf(247,plain,
% 60.92/60.99 (P2(x2471,x2472,f5(f5(x2471,a3),x2472))),
% 60.92/60.99 inference(rename_variables,[],[240])).
% 60.92/60.99 cnf(251,plain,
% 60.92/60.99 (P2(x2511,x2512,f5(x2511,x2512))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(252,plain,
% 60.92/60.99 (P2(x2521,x2522,f5(x2521,x2522))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(254,plain,
% 60.92/60.99 (P2(x2541,a2,f5(f5(x2541,a3),a1))),
% 60.92/60.99 inference(scs_inference,[],[4,252,251,12,240,247,7,8,9])).
% 60.92/60.99 cnf(275,plain,
% 60.92/60.99 (P2(x2751,x2752,f5(x2751,x2752))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(276,plain,
% 60.92/60.99 (P2(x2761,x2762,f5(x2761,x2762))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(278,plain,
% 60.92/60.99 (P2(x2781,a3,f5(f5(x2781,a3),f4(a3)))),
% 60.92/60.99 inference(scs_inference,[],[4,276,275,145,80,8,9])).
% 60.92/60.99 cnf(279,plain,
% 60.92/60.99 (P2(x2791,x2792,f5(x2791,x2792))),
% 60.92/60.99 inference(rename_variables,[],[4])).
% 60.92/60.99 cnf(282,plain,
% 60.92/60.99 (P1(f5(x2821,a3),f5(f5(x2821,a3),f4(a3)))),
% 60.92/60.99 inference(scs_inference,[],[4,276,279,275,145,80,8,9,7])).
% 60.92/61.00 cnf(294,plain,
% 60.92/61.00 (P2(x2941,x2942,f5(x2941,x2942))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(295,plain,
% 60.92/61.00 (P2(x2951,x2952,f5(x2951,x2952))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(298,plain,
% 60.92/61.00 (P2(x2981,x2982,f5(x2981,x2982))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(301,plain,
% 60.92/61.00 (P1(f5(x3011,x3012),f5(f5(x3011,a3),f5(a3,x3012)))),
% 60.92/61.00 inference(scs_inference,[],[4,295,298,294,52,80,8,9,7])).
% 60.92/61.00 cnf(305,plain,
% 60.92/61.00 (P2(a3,x3051,x3051)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(307,plain,
% 60.92/61.00 (P1(x3071,f5(a3,f5(a3,x3071)))),
% 60.92/61.00 inference(scs_inference,[],[172,2,305,194,6,7])).
% 60.92/61.00 cnf(322,plain,
% 60.92/61.00 (P2(a3,x3221,x3221)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(325,plain,
% 60.92/61.00 (P2(f4(x3251),x3251,f5(a3,a3))),
% 60.92/61.00 inference(rename_variables,[],[49])).
% 60.92/61.00 cnf(327,plain,
% 60.92/61.00 (P2(f5(x3271,f4(x3271)),a3,f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[246,2,322,97,49,325,6,7,8])).
% 60.92/61.00 cnf(369,plain,
% 60.92/61.00 (P2(a3,x3691,x3691)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(371,plain,
% 60.92/61.00 (P1(x3711,f5(f5(a3,a3),x3711))),
% 60.92/61.00 inference(scs_inference,[],[222,2,369,240,6,7])).
% 60.92/61.00 cnf(413,plain,
% 60.92/61.00 (P2(a3,x4131,x4131)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(416,plain,
% 60.92/61.00 (P2(f4(x4161),x4161,f5(a3,a3))),
% 60.92/61.00 inference(rename_variables,[],[49])).
% 60.92/61.00 cnf(418,plain,
% 60.92/61.00 (P2(f5(f4(x4181),f5(x4181,a3)),a3,f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[231,2,413,112,49,416,6,7,8])).
% 60.92/61.00 cnf(500,plain,
% 60.92/61.00 (P1(a2,a1)),
% 60.92/61.00 inference(scs_inference,[],[12,137,2,6,7])).
% 60.92/61.00 cnf(501,plain,
% 60.92/61.00 (P2(a3,x5011,x5011)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(503,plain,
% 60.92/61.00 (P2(a2,x5031,f5(a3,f5(a1,x5031)))),
% 60.92/61.00 inference(scs_inference,[],[12,137,2,501,194,6,7,8])).
% 60.92/61.00 cnf(516,plain,
% 60.92/61.00 (P2(x5161,x5162,f5(f4(a3),f5(x5161,x5162)))),
% 60.92/61.00 inference(rename_variables,[],[176])).
% 60.92/61.00 cnf(518,plain,
% 60.92/61.00 (P2(a2,x5181,f5(f4(a3),f5(a1,x5181)))),
% 60.92/61.00 inference(scs_inference,[],[12,371,2,176,516,6,7,8])).
% 60.92/61.00 cnf(545,plain,
% 60.92/61.00 (P1(a2,f5(a3,a1))),
% 60.92/61.00 inference(scs_inference,[],[12,307,4,6,7])).
% 60.92/61.00 cnf(566,plain,
% 60.92/61.00 (P2(a3,a1,f5(a2,x5661))+~P2(a1,x5661,a1)),
% 60.92/61.00 inference(scs_inference,[],[12,144,6])).
% 60.92/61.00 cnf(581,plain,
% 60.92/61.00 (P2(f5(f4(x5811),x5811),a1,f5(a3,a2))),
% 60.92/61.00 inference(scs_inference,[],[12,63,149,52,7,8])).
% 60.92/61.00 cnf(586,plain,
% 60.92/61.00 (P2(f5(x5861,f4(x5861)),x5862,x5862)),
% 60.92/61.00 inference(scs_inference,[],[97,49,65,8])).
% 60.92/61.00 cnf(591,plain,
% 60.92/61.00 (P2(a2,a3,a2)),
% 60.92/61.00 inference(scs_inference,[],[586,167])).
% 60.92/61.00 cnf(607,plain,
% 60.92/61.00 (P2(a2,x6071,f5(a1,x6071))),
% 60.92/61.00 inference(scs_inference,[],[12,176,163,8])).
% 60.92/61.00 cnf(617,plain,
% 60.92/61.00 (P1(f5(a3,f5(a2,x6171)),f5(a1,x6171))),
% 60.92/61.00 inference(scs_inference,[],[194,607,7])).
% 60.92/61.00 cnf(618,plain,
% 60.92/61.00 (P2(a2,x6181,f5(a1,x6181))),
% 60.92/61.00 inference(rename_variables,[],[607])).
% 60.92/61.00 cnf(619,plain,
% 60.92/61.00 (P2(x6191,x6192,f5(a3,f5(x6191,x6192)))),
% 60.92/61.00 inference(rename_variables,[],[194])).
% 60.92/61.00 cnf(625,plain,
% 60.92/61.00 (P2(a3,f5(a3,f5(a2,x6251)),f5(a1,x6251))),
% 60.92/61.00 inference(scs_inference,[],[12,2,194,619,607,618,7,8,6])).
% 60.92/61.00 cnf(637,plain,
% 60.92/61.00 (P1(f4(a3),f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[127,49,7])).
% 60.92/61.00 cnf(638,plain,
% 60.92/61.00 (P2(f4(x6381),x6381,f5(a3,a3))),
% 60.92/61.00 inference(rename_variables,[],[49])).
% 60.92/61.00 cnf(640,plain,
% 60.92/61.00 (P2(a3,f5(a3,a3),f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[2,127,49,638,7,9])).
% 60.92/61.00 cnf(644,plain,
% 60.92/61.00 (P2(f5(a2,a3),a1,f5(a1,a2))),
% 60.92/61.00 inference(scs_inference,[],[12,2,127,49,638,4,607,7,9,8])).
% 60.92/61.00 cnf(649,plain,
% 60.92/61.00 (P1(f5(a3,a3),f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[49,127,7])).
% 60.92/61.00 cnf(650,plain,
% 60.92/61.00 (P2(f4(x6501),x6501,f4(a3))),
% 60.92/61.00 inference(rename_variables,[],[127])).
% 60.92/61.00 cnf(656,plain,
% 60.92/61.00 (P2(f5(a3,a3),a3,f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[12,2,49,127,650,4,194,7,9,8])).
% 60.92/61.00 cnf(662,plain,
% 60.92/61.00 (P1(f4(a3),a3)),
% 60.92/61.00 inference(scs_inference,[],[127,3,7])).
% 60.92/61.00 cnf(669,plain,
% 60.92/61.00 (P2(f4(a3),a1,a2)),
% 60.92/61.00 inference(scs_inference,[],[12,127,3,4,176,56,7,9,8])).
% 60.92/61.00 cnf(677,plain,
% 60.92/61.00 (P2(a3,f5(a1,x6771),f5(a2,x6771))),
% 60.92/61.00 inference(scs_inference,[],[2,49,4,63,607,7,9])).
% 60.92/61.00 cnf(691,plain,
% 60.92/61.00 (P2(a3,f5(a2,x6911),f5(a1,x6911))),
% 60.92/61.00 inference(scs_inference,[],[2,625,127,97,80,7,9])).
% 60.92/61.00 cnf(695,plain,
% 60.92/61.00 (P2(f4(a3),a1,f5(a3,a2))),
% 60.92/61.00 inference(scs_inference,[],[12,2,625,127,97,149,80,7,9,8])).
% 60.92/61.00 cnf(716,plain,
% 60.92/61.00 (P2(x7161,x7162,f5(x7161,x7162))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(718,plain,
% 60.92/61.00 (P2(a2,x7181,f5(f5(a3,a3),f5(a1,x7181)))),
% 60.92/61.00 inference(scs_inference,[],[12,127,4,716,63,254,240,7,9,8])).
% 60.92/61.00 cnf(723,plain,
% 60.92/61.00 (P1(f5(a2,x7231),f5(a1,x7231))),
% 60.92/61.00 inference(scs_inference,[],[4,607,7])).
% 60.92/61.00 cnf(742,plain,
% 60.92/61.00 (P2(x7421,x7422,f5(x7421,x7422))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(744,plain,
% 60.92/61.00 (P2(f5(a2,a3),a1,f5(f5(a3,a3),f5(a1,a2)))),
% 60.92/61.00 inference(scs_inference,[],[12,127,4,742,112,278,718,7,9,8])).
% 60.92/61.00 cnf(751,plain,
% 60.92/61.00 (P2(x7511,x7512,f5(x7511,x7512))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(758,plain,
% 60.92/61.00 (P2(f5(a3,a3),x7581,x7581)),
% 60.92/61.00 inference(scs_inference,[],[2,49,127,4,751,140,518,718,7,9,8])).
% 60.92/61.00 cnf(770,plain,
% 60.92/61.00 (P2(f5(a3,a3),a1,a2)),
% 60.92/61.00 inference(scs_inference,[],[12,49,4,56,758,7,8])).
% 60.92/61.00 cnf(774,plain,
% 60.92/61.00 (P2(a3,f5(f5(a3,a3),x7741),x7741)),
% 60.92/61.00 inference(scs_inference,[],[12,2,49,4,56,758,7,8,6])).
% 60.92/61.00 cnf(779,plain,
% 60.92/61.00 (P2(a2,x7791,f5(a3,f5(a1,x7791)))),
% 60.92/61.00 inference(rename_variables,[],[503])).
% 60.92/61.00 cnf(780,plain,
% 60.92/61.00 (P2(x7801,x7802,f5(x7801,x7802))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(782,plain,
% 60.92/61.00 (P2(f5(a2,a3),a1,f5(a3,f5(a1,a2)))),
% 60.92/61.00 inference(scs_inference,[],[12,4,780,503,779,7,8])).
% 60.92/61.00 cnf(793,plain,
% 60.92/61.00 (P2(f4(a3),x7931,f5(x7931,f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[127,49,4,85,718,7,8])).
% 60.92/61.00 cnf(816,plain,
% 60.92/61.00 (P2(f5(a3,a3),a1,f5(a3,a2))),
% 60.92/61.00 inference(scs_inference,[],[12,49,149,8])).
% 60.92/61.00 cnf(851,plain,
% 60.92/61.00 (P2(f5(a3,a3),a1,f5(a2,f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[12,49,793,8])).
% 60.92/61.00 cnf(856,plain,
% 60.92/61.00 (P2(f5(a3,a3),x8561,f5(x8561,a3))),
% 60.92/61.00 inference(scs_inference,[],[49,3,85,8])).
% 60.92/61.00 cnf(866,plain,
% 60.92/61.00 (P2(f5(a3,a3),f5(a3,x8661),x8661)),
% 60.92/61.00 inference(scs_inference,[],[2,49,70,8])).
% 60.92/61.00 cnf(880,plain,
% 60.92/61.00 (P2(f5(a3,a3),f4(a3),f4(f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[49,140,65,8])).
% 60.92/61.00 cnf(886,plain,
% 60.92/61.00 (P2(a2,x8861,x8862)+~P2(a1,x8861,f5(f4(x8863),f5(x8863,x8862)))),
% 60.92/61.00 inference(scs_inference,[],[12,77,8])).
% 60.92/61.00 cnf(913,plain,
% 60.92/61.00 (P2(x9131,x9132,f5(x9131,x9132))),
% 60.92/61.00 inference(rename_variables,[],[4])).
% 60.92/61.00 cnf(915,plain,
% 60.92/61.00 (P2(f5(f5(a3,a3),a3),f5(a3,x9151),x9151)),
% 60.92/61.00 inference(scs_inference,[],[2,4,913,866,7,8])).
% 60.92/61.00 cnf(923,plain,
% 60.92/61.00 (P2(a2,x9231,x9232)+~P2(a1,x9231,f5(f5(a3,a3),x9232))),
% 60.92/61.00 inference(scs_inference,[],[12,774,8])).
% 60.92/61.00 cnf(925,plain,
% 60.92/61.00 (P1(f5(a2,x9251),x9252)+~P2(a1,x9251,f5(f5(a3,a3),x9252))),
% 60.92/61.00 inference(scs_inference,[],[12,4,774,8,7])).
% 60.92/61.00 cnf(977,plain,
% 60.92/61.00 (P2(a3,a2,a1)),
% 60.92/61.00 inference(scs_inference,[],[2,500,6])).
% 60.92/61.00 cnf(978,plain,
% 60.92/61.00 (P2(a3,x9781,x9781)),
% 60.92/61.00 inference(rename_variables,[],[2])).
% 60.92/61.00 cnf(986,plain,
% 60.92/61.00 (P1(a2,f5(a2,a3))),
% 60.92/61.00 inference(scs_inference,[],[15,2,978,500,80,591,6,9,8,144])).
% 60.92/61.00 cnf(988,plain,
% 60.92/61.00 (P1(f5(a2,a3),a2)),
% 60.92/61.00 inference(scs_inference,[],[15,2,978,500,80,591,6,9,8,144,189])).
% 60.92/61.00 cnf(1012,plain,
% 60.92/61.00 (P2(a3,a2,f5(a3,a1))),
% 60.92/61.00 inference(scs_inference,[],[2,545,6])).
% 60.92/61.00 cnf(1047,plain,
% 60.92/61.00 (P2(a3,f5(a3,a2),a1)),
% 60.92/61.00 inference(scs_inference,[],[38,2,581,9])).
% 60.92/61.00 cnf(1078,plain,
% 60.92/61.00 (P2(f4(x10781),x10781,f5(a3,a3))),
% 60.92/61.00 inference(rename_variables,[],[49])).
% 60.92/61.00 cnf(1080,plain,
% 60.92/61.00 (P2(f5(a3,a3),x10801,f5(a3,x10801))),
% 60.92/61.00 inference(scs_inference,[],[49,1078,2,246,149,816,6,9,8])).
% 60.92/61.00 cnf(1085,plain,
% 60.92/61.00 (P2(f4(x10851),x10851,f5(f5(a3,a3),f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[49,301,6])).
% 60.92/61.00 cnf(1096,plain,
% 60.92/61.00 (P2(f4(x10961),x10961,f5(f5(a3,a3),f4(a3)))),
% 60.92/61.00 inference(scs_inference,[],[49,282,6])).
% 60.92/61.00 cnf(1100,plain,
% 60.92/61.00 (P2(f4(x11001),x11001,f5(a3,a3))),
% 60.92/61.00 inference(rename_variables,[],[49])).
% 60.92/61.00 cnf(1102,plain,
% 60.92/61.00 (P2(f5(a3,a3),x11021,f5(x11021,f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[49,1100,2,282,656,793,6,9,8])).
% 60.92/61.00 cnf(1243,plain,
% 60.92/61.00 (P2(f4(a3),f4(a3),a3)),
% 60.92/61.00 inference(scs_inference,[],[56,662,6])).
% 60.92/61.00 cnf(1246,plain,
% 60.92/61.00 (P2(f4(a3),f4(a3),f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[56,637,6])).
% 60.92/61.00 cnf(1261,plain,
% 60.92/61.00 (P2(f4(a3),f5(a2,x12611),f5(a1,x12611))),
% 60.92/61.00 inference(scs_inference,[],[56,723,6])).
% 60.92/61.00 cnf(1298,plain,
% 60.92/61.00 (P2(f4(a3),a2,a1)),
% 60.92/61.00 inference(scs_inference,[],[56,500,6])).
% 60.92/61.00 cnf(1305,plain,
% 60.92/61.00 (P2(f4(a3),a2,f5(a3,a1))),
% 60.92/61.00 inference(scs_inference,[],[56,545,6])).
% 60.92/61.00 cnf(1331,plain,
% 60.92/61.00 (P2(f4(f4(x13311)),f5(a3,a3),x13311)),
% 60.92/61.00 inference(rename_variables,[],[65])).
% 60.92/61.00 cnf(1333,plain,
% 60.92/61.00 (P2(f4(f4(a3)),f5(x13331,a3),x13331)),
% 60.92/61.00 inference(scs_inference,[],[65,1331,2,123,856,6,9])).
% 60.92/61.00 cnf(1335,plain,
% 60.92/61.00 (P2(f4(f4(x13351)),f5(a3,a3),x13351)),
% 60.92/61.00 inference(rename_variables,[],[65])).
% 60.92/61.00 cnf(1337,plain,
% 60.92/61.00 (P2(x13371,a3,x13371)),
% 60.92/61.00 inference(scs_inference,[],[65,1331,1335,2,123,179,856,6,9,8])).
% 60.92/61.00 cnf(1360,plain,
% 60.92/61.00 (P2(f4(f4(x13601)),f5(a3,a3),x13601)),
% 60.92/61.00 inference(rename_variables,[],[65])).
% 60.92/61.00 cnf(1362,plain,
% 60.92/61.00 (P2(x13621,f5(a3,a3),x13621)),
% 60.92/61.00 inference(scs_inference,[],[65,1360,500,758,6,8])).
% 60.92/61.00 cnf(1370,plain,
% 60.92/61.00 (P2(f4(f4(x13701)),f5(a3,a3),x13701)),
% 60.92/61.00 inference(rename_variables,[],[65])).
% 60.92/61.00 cnf(1372,plain,
% 60.92/61.00 (P2(x13721,f4(x13721),f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[65,1370,545,127,758,1362,7,6,8])).
% 60.92/61.00 cnf(1378,plain,
% 60.92/61.00 (P2(f4(f4(x13781)),f5(a3,a3),x13781)),
% 60.92/61.00 inference(rename_variables,[],[65])).
% 60.92/61.00 cnf(1380,plain,
% 60.92/61.00 (P2(x13801,f4(x13801),a3)),
% 60.92/61.00 inference(scs_inference,[],[65,1378,3,758,1,6,8])).
% 60.92/61.00 cnf(1387,plain,
% 60.92/61.00 (P2(x13871,f4(x13871),f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[65,49,758,8])).
% 60.92/61.00 cnf(1401,plain,
% 60.92/61.00 (P2(a2,f4(a1),a3)),
% 60.92/61.00 inference(scs_inference,[],[65,112,758,1387,92,8,886])).
% 60.92/61.00 cnf(1439,plain,
% 60.92/61.00 (P2(x14391,f4(x14391),f5(f5(a3,a3),f5(a3,a3)))),
% 60.92/61.00 inference(scs_inference,[],[65,1085,758,8])).
% 60.92/61.00 cnf(1445,plain,
% 60.92/61.00 (P2(a2,f4(a1),f5(a3,a3))),
% 60.92/61.00 inference(scs_inference,[],[65,1085,758,8,925,923])).
% 60.92/61.00 cnf(1460,plain,
% 60.92/61.00 (P2(a2,f4(a1),f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[65,2,1096,758,1439,7,8,925,923])).
% 60.92/61.00 cnf(1486,plain,
% 60.92/61.00 (P2(x14861,f4(a3),x14861)),
% 60.92/61.00 inference(scs_inference,[],[65,758,140,8])).
% 60.92/61.00 cnf(1526,plain,
% 60.92/61.00 (P2(f4(x15261),f5(x15261,x15262),x15262)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1528,plain,
% 60.92/61.00 (P2(f4(x15281),f5(x15281,a3),f4(a3))),
% 60.92/61.00 inference(scs_inference,[],[70,1526,123,793,7,6])).
% 60.92/61.00 cnf(1529,plain,
% 60.92/61.00 (P2(f4(x15291),f5(x15291,x15292),x15292)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1531,plain,
% 60.92/61.00 (P2(f4(a2),f5(a1,a2),a1)),
% 60.92/61.00 inference(scs_inference,[],[70,1526,1529,2,123,644,793,7,6,9])).
% 60.92/61.00 cnf(1553,plain,
% 60.92/61.00 (P2(f4(x15531),f5(x15531,x15532),f5(a3,x15532))),
% 60.92/61.00 inference(scs_inference,[],[70,24,6])).
% 60.92/61.00 cnf(1569,plain,
% 60.92/61.00 (P2(f4(x15691),f5(x15691,x15692),x15692)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1571,plain,
% 60.92/61.00 (P2(f4(a3),f5(x15711,a3),x15711)),
% 60.92/61.00 inference(scs_inference,[],[70,1569,2,662,856,6,9])).
% 60.92/61.00 cnf(1593,plain,
% 60.92/61.00 (P2(f4(x15931),f5(x15931,x15932),x15932)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1595,plain,
% 60.92/61.00 (P2(a3,f5(f5(a3,x15951),f5(a3,a3)),x15951)),
% 60.92/61.00 inference(scs_inference,[],[70,1593,2,637,793,6,9])).
% 60.92/61.00 cnf(1609,plain,
% 60.92/61.00 (P2(f4(x16091),f5(x16091,x16092),x16092)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1611,plain,
% 60.92/61.00 (P2(f4(a3),f5(x16111,f5(a3,a3)),x16111)),
% 60.92/61.00 inference(scs_inference,[],[70,1609,2,723,1102,6,9])).
% 60.92/61.00 cnf(1622,plain,
% 60.92/61.00 (P2(f4(x16221),f5(x16221,x16222),x16222)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1625,plain,
% 60.92/61.00 (P2(f4(x16251),f5(x16251,x16252),x16252)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1628,plain,
% 60.92/61.00 (P2(x16281,f5(a3,a3),f5(a3,x16281))),
% 60.92/61.00 inference(scs_inference,[],[70,1622,1625,2,93,4,851,1611,6,9,8])).
% 60.92/61.00 cnf(1638,plain,
% 60.92/61.00 (P2(f4(x16381),f5(x16381,x16382),x16382)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1641,plain,
% 60.92/61.00 (P2(x16411,a3,f5(a3,x16411))),
% 60.92/61.00 inference(scs_inference,[],[70,1638,2,371,4,744,1571,6,9,8])).
% 60.92/61.00 cnf(1663,plain,
% 60.92/61.00 (P2(f4(x16631),f5(x16631,x16632),x16632)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1666,plain,
% 60.92/61.00 (P2(x16661,x16662,f5(f5(a3,x16661),x16662))),
% 60.92/61.00 inference(scs_inference,[],[70,1663,2,307,176,782,159,6,9,8])).
% 60.92/61.00 cnf(1672,plain,
% 60.92/61.00 (P2(f4(x16721),f5(x16721,x16722),x16722)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1675,plain,
% 60.92/61.00 (P2(f4(x16751),f5(x16751,x16752),x16752)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1678,plain,
% 60.92/61.00 (P2(f4(f4(x16781)),a3,x16781)),
% 60.92/61.00 inference(scs_inference,[],[70,1672,1675,2,46,327,880,65,6,9,8])).
% 60.92/61.00 cnf(1684,plain,
% 60.92/61.00 (P2(f4(x16841),f5(x16841,x16842),x16842)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1687,plain,
% 60.92/61.00 (P2(f4(x16871),f5(x16871,x16872),x16872)),
% 60.92/61.00 inference(rename_variables,[],[70])).
% 60.92/61.00 cnf(1690,plain,
% 60.92/61.00 (P2(f5(x16901,a3),a3,x16901)),
% 60.92/61.00 inference(scs_inference,[],[70,1684,1687,2,988,418,915,65,6,9,8])).
% 60.92/61.00 cnf(1728,plain,
% 60.92/61.00 (P2(f4(x17281),f5(x17281,a2),f5(a2,a3))),
% 60.92/61.00 inference(scs_inference,[],[70,986,6])).
% 60.92/61.00 cnf(1737,plain,
% 60.92/61.00 (P2(f4(x17371),f5(x17371,a2),a1)),
% 60.92/61.00 inference(scs_inference,[],[70,500,6])).
% 60.92/61.00 cnf(1745,plain,
% 60.92/61.00 (P2(f4(x17451),f5(x17451,a2),f5(a3,a1))),
% 60.92/61.00 inference(scs_inference,[],[70,545,6])).
% 60.92/61.00 cnf(1796,plain,
% 60.92/61.00 (P2(f4(x17961),f5(x17961,a1),a2)),
% 60.92/61.00 inference(scs_inference,[],[70,1,6])).
% 60.92/61.00 cnf(1818,plain,
% 60.92/61.00 (P2(x18181,f5(a3,a3),f5(f4(x18182),f5(x18182,x18181)))),
% 60.92/61.00 inference(scs_inference,[],[77,24,1666,1595,6,8])).
% 60.92/61.00 cnf(1822,plain,
% 60.92/61.00 (P2(a2,f5(a3,a3),a1)),
% 60.92/61.00 inference(scs_inference,[],[1818,886])).
% 60.92/61.00 cnf(1883,plain,
% 60.92/61.00 (P2(a3,f5(a3,a2),f5(a2,a3))),
% 60.92/61.00 inference(scs_inference,[],[80,986,6])).
% 60.92/61.00 cnf(1887,plain,
% 60.92/61.00 (P2(a3,f5(a3,a2),f5(a3,a1))),
% 60.92/61.00 inference(scs_inference,[],[80,545,6])).
% 60.92/61.00 cnf(1906,plain,
% 60.92/61.00 (P2(a3,f5(a3,a1),a2)),
% 60.92/61.00 inference(scs_inference,[],[80,1,6])).
% 60.92/61.00 cnf(1912,plain,
% 60.92/61.00 (P2(f4(f4(x19121)),x19122,f5(x19121,x19122))),
% 60.92/61.01 inference(rename_variables,[],[85])).
% 60.92/61.01 cnf(1915,plain,
% 60.92/61.01 (P2(f4(f4(x19151)),x19152,f5(x19151,x19152))),
% 60.92/61.01 inference(rename_variables,[],[85])).
% 60.92/61.01 cnf(1917,plain,
% 60.92/61.01 (P2(f5(x19171,a3),f4(x19171),a3)),
% 60.92/61.01 inference(scs_inference,[],[85,1912,1915,2,617,3,140,7,6,8])).
% 60.92/61.01 cnf(1924,plain,
% 60.92/61.01 (P2(f4(f4(x19241)),x19242,f5(x19241,x19242))),
% 60.92/61.01 inference(rename_variables,[],[85])).
% 60.92/61.01 cnf(1927,plain,
% 60.92/61.01 (P2(f4(f4(x19271)),x19272,f5(x19271,x19272))),
% 60.92/61.01 inference(rename_variables,[],[85])).
% 60.92/61.01 cnf(1929,plain,
% 60.92/61.01 (P2(f5(x19291,a3),f4(x19291),f5(a3,a3))),
% 60.92/61.01 inference(scs_inference,[],[85,1924,1927,2,649,49,1333,7,6,8])).
% 60.92/61.01 cnf(1934,plain,
% 60.92/61.01 (P1(f5(x19341,a3),x19341)),
% 60.92/61.01 inference(scs_inference,[],[85,1678,7])).
% 60.92/61.01 cnf(1992,plain,
% 60.92/61.01 (P2(f5(x19921,a3),f4(a3),x19921)),
% 60.92/61.01 inference(scs_inference,[],[85,2,140,8])).
% 60.92/61.01 cnf(2043,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(x20431,a3),x20431)),
% 60.92/61.01 inference(scs_inference,[],[85,2,1333,8])).
% 60.92/61.01 cnf(2048,plain,
% 60.92/61.01 (P1(f5(f5(a3,a3),f5(x20481,a3)),x20481)),
% 60.92/61.01 inference(scs_inference,[],[4,2043,7])).
% 60.92/61.01 cnf(2051,plain,
% 60.92/61.01 (P2(f5(x20511,a3),f5(a3,a3),x20511)),
% 60.92/61.01 inference(scs_inference,[],[85,2,4,2043,65,7,8])).
% 60.92/61.01 cnf(2057,plain,
% 60.92/61.01 (P1(f5(f5(x20571,a3),f5(a3,a3)),x20571)),
% 60.92/61.01 inference(scs_inference,[],[4,2051,7])).
% 60.92/61.01 cnf(2058,plain,
% 60.92/61.01 (P2(x20581,x20582,f5(x20581,x20582))),
% 60.92/61.01 inference(rename_variables,[],[4])).
% 60.92/61.01 cnf(2060,plain,
% 60.92/61.01 (P2(a3,f5(f5(a3,a3),f5(x20601,a3)),x20601)),
% 60.92/61.01 inference(scs_inference,[],[2,2048,4,2051,7,6])).
% 60.92/61.01 cnf(2061,plain,
% 60.92/61.01 (P2(a3,x20611,x20611)),
% 60.92/61.01 inference(rename_variables,[],[2])).
% 60.92/61.01 cnf(2065,plain,
% 60.92/61.01 (P2(a3,x20651,x20651)),
% 60.92/61.01 inference(rename_variables,[],[2])).
% 60.92/61.01 cnf(2066,plain,
% 60.92/61.01 (P2(x20661,x20662,f5(x20661,x20662))),
% 60.92/61.01 inference(rename_variables,[],[4])).
% 60.92/61.01 cnf(2068,plain,
% 60.92/61.01 (P2(f5(a2,a3),x20681,f5(a1,x20681))),
% 60.92/61.01 inference(scs_inference,[],[2,2061,2065,2048,4,2058,2066,607,254,2051,7,6,9,8])).
% 60.92/61.01 cnf(2074,plain,
% 60.92/61.01 (P2(a3,x20741,x20741)),
% 60.92/61.01 inference(rename_variables,[],[2])).
% 60.92/61.01 cnf(2076,plain,
% 60.92/61.01 (P2(a3,x20761,f5(x20761,a3))),
% 60.92/61.01 inference(scs_inference,[],[2,2074,2057,774,2060,6,9])).
% 60.92/61.01 cnf(2103,plain,
% 60.92/61.01 (P2(a3,f5(x21031,a3),x21031)),
% 60.92/61.01 inference(scs_inference,[],[2,1934,6])).
% 60.92/61.01 cnf(2230,plain,
% 60.92/61.01 (P2(f5(f4(x22301),f5(x22301,a3)),f5(x22302,a3),x22302)),
% 60.92/61.01 inference(scs_inference,[],[103,2,1571,8])).
% 60.92/61.01 cnf(2332,plain,
% 60.92/61.01 (P2(f5(f4(x23321),f5(x23321,a3)),f5(a3,a2),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[112,2,1728,8])).
% 60.92/61.01 cnf(2338,plain,
% 60.92/61.01 (P2(f5(f4(x23381),f5(x23381,a3)),f5(a3,a2),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[112,2,1745,8])).
% 60.92/61.01 cnf(2655,plain,
% 60.92/61.01 (P2(f4(x26551),x26551,f4(a3))),
% 60.92/61.01 inference(rename_variables,[],[127])).
% 60.92/61.01 cnf(2656,plain,
% 60.92/61.01 (P2(f4(x26561),x26561,f4(a3))),
% 60.92/61.01 inference(rename_variables,[],[127])).
% 60.92/61.01 cnf(2658,plain,
% 60.92/61.01 (P2(f4(a3),x26581,f4(f4(x26581)))),
% 60.92/61.01 inference(scs_inference,[],[127,2656,2655,240,1486,9,8])).
% 60.92/61.01 cnf(2827,plain,
% 60.92/61.01 (P2(f4(a3),f5(a1,x28271),f5(a2,x28271))),
% 60.92/61.01 inference(scs_inference,[],[129,2,677,8])).
% 60.92/61.01 cnf(2909,plain,
% 60.92/61.01 (P2(f4(a3),f5(a2,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[133,2,2332,9])).
% 60.92/61.01 cnf(2918,plain,
% 60.92/61.01 (P2(f4(a3),f5(a3,a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[133,2,2338,9])).
% 60.92/61.01 cnf(2924,plain,
% 60.92/61.01 (P2(f4(a3),x29241,f5(x29241,a3))),
% 60.92/61.01 inference(scs_inference,[],[133,2,2230,9])).
% 60.92/61.01 cnf(3043,plain,
% 60.92/61.01 (P2(f5(a3,a3),a2,f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[149,2,1305,793,7,8])).
% 60.92/61.01 cnf(3051,plain,
% 60.92/61.01 (P2(f4(a3),x30511,f5(f5(a3,a3),f5(x30511,a3)))),
% 60.92/61.01 inference(scs_inference,[],[149,4,2103,2658,7,9])).
% 60.92/61.01 cnf(3062,plain,
% 60.92/61.01 (P2(f5(a3,a3),a2,a1)),
% 60.92/61.01 inference(scs_inference,[],[149,2,1298,3051,7,8])).
% 60.92/61.01 cnf(3067,plain,
% 60.92/61.01 (P1(f5(a3,x30671),f5(x30671,a3))),
% 60.92/61.01 inference(scs_inference,[],[149,2924,7])).
% 60.92/61.01 cnf(3070,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a2,x30701),f5(a1,x30701))),
% 60.92/61.01 inference(scs_inference,[],[149,2,1261,2924,7,8])).
% 60.92/61.01 cnf(3159,plain,
% 60.92/61.01 (P1(f5(a3,a1),a2)),
% 60.92/61.01 inference(scs_inference,[],[1012,2,7])).
% 60.92/61.01 cnf(3160,plain,
% 60.92/61.01 (P2(a3,x31601,x31601)),
% 60.92/61.01 inference(rename_variables,[],[2])).
% 60.92/61.01 cnf(3162,plain,
% 60.92/61.01 (P2(a3,a2,f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[1012,2,3067,7,6])).
% 60.92/61.01 cnf(3165,plain,
% 60.92/61.01 (P2(a3,f5(a2,a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[1012,2,3160,3067,2076,7,6,9])).
% 60.92/61.01 cnf(3167,plain,
% 60.92/61.01 (P2(a3,x31671,x31671)),
% 60.92/61.01 inference(rename_variables,[],[2])).
% 60.92/61.01 cnf(3169,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a3,a2),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[1012,2,3160,3167,3067,4,1883,2076,7,6,9,8])).
% 60.92/61.01 cnf(3174,plain,
% 60.92/61.01 (P1(f5(a3,a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[1012,4,7])).
% 60.92/61.01 cnf(3175,plain,
% 60.92/61.01 (P2(x31751,x31752,f5(x31751,x31752))),
% 60.92/61.01 inference(rename_variables,[],[4])).
% 60.92/61.01 cnf(3177,plain,
% 60.92/61.01 (P2(f5(a3,a3),a2,f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[1012,2,4,3175,3162,7,8])).
% 60.92/61.01 cnf(3181,plain,
% 60.92/61.01 (P1(f5(a3,a1),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[1012,2076,7])).
% 60.92/61.01 cnf(3184,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a3,a2),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[1012,2,4,1887,2076,7,8])).
% 60.92/61.01 cnf(3189,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a1,x31891),f5(a2,x31891))),
% 60.92/61.01 inference(scs_inference,[],[2,4,677,8])).
% 60.92/61.01 cnf(3193,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a3,a3),f4(a3))),
% 60.92/61.01 inference(scs_inference,[],[2,4,640,8])).
% 60.92/61.01 cnf(3198,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a2,a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[2,4,3165,8])).
% 60.92/61.01 cnf(3202,plain,
% 60.92/61.01 (P2(f5(a2,a3),f4(a1),f5(a3,a3))),
% 60.92/61.01 inference(scs_inference,[],[2,4,1445,8])).
% 60.92/61.01 cnf(3207,plain,
% 60.92/61.01 (P2(a3,a1,f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[1337,566])).
% 60.92/61.01 cnf(3210,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a2,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3174,3198,1337,566,6])).
% 60.92/61.01 cnf(3212,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a3,a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3174,3198,2909,3193,1337,566,6,9])).
% 60.92/61.01 cnf(3214,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a1),f4(a3))),
% 60.92/61.01 inference(scs_inference,[],[3174,3198,2909,3193,3202,1337,566,6,9,8])).
% 60.92/61.01 cnf(3217,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a2,a3),a1)),
% 60.92/61.01 inference(scs_inference,[],[3062,1929,2924,9])).
% 60.92/61.01 cnf(3218,plain,
% 60.92/61.01 (P2(f5(x32181,a3),f4(x32181),f5(a3,a3))),
% 60.92/61.01 inference(rename_variables,[],[1929])).
% 60.92/61.01 cnf(3221,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a1,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[1531,3062,1929,3218,2068,2924,9,8])).
% 60.92/61.01 cnf(3225,plain,
% 60.92/61.01 (P2(f4(a3),f5(a2,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3221,2827,1246,9])).
% 60.92/61.01 cnf(3228,plain,
% 60.92/61.01 (P2(f5(a3,a2),f4(a2),f5(a3,a3))),
% 60.92/61.01 inference(scs_inference,[],[3210,3221,2827,1917,1246,1080,9,8])).
% 60.92/61.01 cnf(3233,plain,
% 60.92/61.01 (P2(f5(a3,a2),f4(a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3043,3228,127,9])).
% 60.92/61.01 cnf(3236,plain,
% 60.92/61.01 (P2(a3,f5(a3,a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3043,2918,3228,1243,1553,127,9,8])).
% 60.92/61.01 cnf(3237,plain,
% 60.92/61.01 (P2(f4(x32371),f5(x32371,x32372),f5(a3,x32372))),
% 60.92/61.01 inference(rename_variables,[],[1553])).
% 60.92/61.01 cnf(3239,plain,
% 60.92/61.01 (P1(f5(a3,a2),a1)),
% 60.92/61.01 inference(scs_inference,[],[3043,2918,3228,1243,1822,1553,1628,127,9,8,7])).
% 60.92/61.01 cnf(3242,plain,
% 60.92/61.01 (P2(f4(x32421),f5(x32421,a1),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3181,3043,2918,3228,1243,1822,1553,3237,1628,127,9,8,7,6])).
% 60.92/61.01 cnf(3245,plain,
% 60.92/61.01 (P2(f5(a3,a3),f5(a1,a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3217,1641,2068,9])).
% 60.92/61.01 cnf(3249,plain,
% 60.92/61.01 (P2(f5(a2,a3),f4(a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3169,3212,3217,3233,1641,2068,9,8])).
% 60.92/61.01 cnf(3252,plain,
% 60.92/61.01 (P2(f5(a2,a3),f5(a3,a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3245,3202,1553,9])).
% 60.92/61.01 cnf(3255,plain,
% 60.92/61.01 (P2(f5(a2,a3),f4(a1),a3)),
% 60.92/61.01 inference(scs_inference,[],[3245,3214,3242,3202,1243,1553,9,8])).
% 60.92/61.01 cnf(3259,plain,
% 60.92/61.01 (P2(a2,f4(a3),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3207,1401,127,9])).
% 60.92/61.01 cnf(3262,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a2),f4(a3))),
% 60.92/61.01 inference(scs_inference,[],[3184,3207,3228,1401,3193,127,9,8])).
% 60.92/61.01 cnf(3264,plain,
% 60.92/61.01 (P2(f5(a2,a3),f4(a3),a1)),
% 60.92/61.01 inference(scs_inference,[],[3249,3239,6])).
% 60.92/61.01 cnf(3266,plain,
% 60.92/61.01 (P2(a2,f4(a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3252,3249,3239,3259,1528,6,9])).
% 60.92/61.01 cnf(3269,plain,
% 60.92/61.01 (P2(f5(a1,a3),f5(a3,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3252,3249,3070,3239,3259,3212,1528,6,9,8])).
% 60.92/61.01 cnf(3272,plain,
% 60.92/61.01 (P1(f5(a3,a2),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[3252,3177,3249,3070,3239,3259,3212,1080,1528,6,9,8,7])).
% 60.92/61.01 cnf(3276,plain,
% 60.92/61.01 (P2(f5(a1,a3),f5(a3,a3),f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3269,1929,3233,9])).
% 60.92/61.01 cnf(3279,plain,
% 60.92/61.01 (P2(f5(a3,a2),f4(a2),f4(a3))),
% 60.92/61.01 inference(scs_inference,[],[3269,3262,3236,1929,3233,1372,9,8])).
% 60.92/61.01 cnf(3283,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a2,a3),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3225,3279,1728,9])).
% 60.92/61.01 cnf(3286,plain,
% 60.92/61.01 (P2(f5(a3,a1),f5(a3,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3276,3225,3279,3245,3212,1728,9,8])).
% 60.92/61.01 cnf(3289,plain,
% 60.92/61.01 (P2(f5(a3,a1),f5(a3,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3283,3286,3210,9])).
% 60.92/61.01 cnf(3291,plain,
% 60.92/61.01 (P2(a1,a1,f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3283,3286,3264,669,3210,2068,9,8])).
% 60.92/61.01 cnf(3295,plain,
% 60.92/61.01 (P2(f5(a1,a3),f5(a3,a3),a2)),
% 60.92/61.01 inference(scs_inference,[],[3159,3276,6])).
% 60.92/61.01 cnf(3297,plain,
% 60.92/61.01 (P2(f5(a1,a3),a1,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3159,3269,3276,3283,3217,6,9])).
% 60.92/61.01 cnf(3299,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3159,3266,3269,3276,3283,3043,3217,3212,6,9,8])).
% 60.92/61.01 cnf(3304,plain,
% 60.92/61.01 (P2(f5(a1,a3),a3,f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3295,1917,3259,9])).
% 60.92/61.01 cnf(3307,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a2),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3289,3299,3295,3279,1917,3259,9,8])).
% 60.92/61.01 cnf(3310,plain,
% 60.92/61.01 (P2(f5(a1,a3),a3,f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3304,3249,1380,9])).
% 60.92/61.01 cnf(3313,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a1),f5(a3,a3))),
% 60.92/61.01 inference(scs_inference,[],[3255,3304,3165,3249,1641,1380,9,8])).
% 60.92/61.01 cnf(3316,plain,
% 60.92/61.01 (P2(f5(a1,a3),f5(a3,a1),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3310,3283,3165,9])).
% 60.92/61.01 cnf(3319,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a2),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[3272,3307,6])).
% 60.92/61.01 cnf(3325,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a1),a2)),
% 60.92/61.01 inference(scs_inference,[],[3316,3313,3295,8])).
% 60.92/61.01 cnf(3327,plain,
% 60.92/61.01 (P2(f5(a3,a1),a1,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3221,3313,1737,9])).
% 60.92/61.01 cnf(3336,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a3,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[1047,3297,3310,8])).
% 60.92/61.01 cnf(3338,plain,
% 60.92/61.01 (P2(f5(a2,a3),f5(a3,a2),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3336,3169,3189,8])).
% 60.92/61.01 cnf(3344,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a3,a3),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[5,3336,3319,3169,3228,3189,1362,8,7,9])).
% 60.92/61.01 cnf(3351,plain,
% 60.92/61.01 (P2(f5(a3,a2),a2,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3327,3286,3062,8])).
% 60.92/61.01 cnf(3353,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a3,a3),a2)),
% 60.92/61.01 inference(scs_inference,[],[3325,3351,1445,9])).
% 60.92/61.01 cnf(3355,plain,
% 60.92/61.01 (P2(f5(a2,a3),a1,f5(a2,a2))),
% 60.92/61.01 inference(scs_inference,[],[3291,3325,3351,3207,1445,677,9,8])).
% 60.92/61.01 cnf(3358,plain,
% 60.92/61.01 (P1(f5(a1,a1),f5(a2,a2))),
% 60.92/61.01 inference(scs_inference,[],[3355,2068,7])).
% 60.92/61.01 cnf(3368,plain,
% 60.92/61.01 (P2(f5(a3,a2),a3,f5(a3,a1))),
% 60.92/61.01 inference(scs_inference,[],[3353,3266,1917,9])).
% 60.92/61.01 cnf(3371,plain,
% 60.92/61.01 (P2(f5(a2,a1),f5(a3,a3),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3353,3338,3266,1917,2068,9,8])).
% 60.92/61.01 cnf(3374,plain,
% 60.92/61.01 (P2(f5(a2,a3),f5(a1,a3),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3371,3344,3338,9])).
% 60.92/61.01 cnf(3376,plain,
% 60.92/61.01 (P2(f5(a3,a1),f5(a3,a1),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3371,3368,3344,3236,3336,3338,9,8])).
% 60.92/61.01 cnf(3379,plain,
% 60.92/61.01 (P2(a1,f5(a3,a1),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[2918,3264,3338,8])).
% 60.92/61.01 cnf(3381,plain,
% 60.92/61.01 (P2(f4(a3),f5(a1,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[2918,2909,3351,3264,3338,2068,8,9])).
% 60.92/61.01 cnf(3384,plain,
% 60.92/61.01 (P2(f5(a3,a1),f5(a3,a1),f5(a2,a2))),
% 60.92/61.01 inference(scs_inference,[],[3358,3376,6])).
% 60.92/61.01 cnf(3386,plain,
% 60.92/61.01 (P1(f5(a1,a3),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3358,3376,3207,2076,6,7])).
% 60.92/61.01 cnf(3389,plain,
% 60.92/61.01 (P2(f5(a3,a2),a2,f5(a2,a2))),
% 60.92/61.01 inference(scs_inference,[],[3384,3368,1906,9])).
% 60.92/61.01 cnf(3391,plain,
% 60.92/61.01 (P2(f5(a1,a2),f5(a3,a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3374,3384,3368,3269,1906,3338,9,8])).
% 60.92/61.01 cnf(3402,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a2),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3386,3319,6])).
% 60.92/61.01 cnf(3404,plain,
% 60.92/61.01 (P2(a1,f5(a3,a2),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3386,3379,3319,3371,3286,6,9])).
% 60.92/61.01 cnf(3406,plain,
% 60.92/61.01 (P2(f5(a3,a1),a2,f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3386,3389,3379,3319,3371,3070,3184,3286,6,9,8])).
% 60.92/61.01 cnf(3413,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a3),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3402,3376,3262,9])).
% 60.92/61.01 cnf(3415,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3402,3406,3376,3262,1460,3299,9,8])).
% 60.92/61.01 cnf(3423,plain,
% 60.92/61.01 (P2(f5(a2,a3),f5(a3,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3415,3374,1929,9])).
% 60.92/61.01 cnf(3426,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a1,a3),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3415,3374,2909,3381,1929,9,8])).
% 60.92/61.01 cnf(3430,plain,
% 60.92/61.01 (P2(a1,f5(a3,a3),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3423,3426,1531,3391,3242,3245,9,8])).
% 60.92/61.01 cnf(3433,plain,
% 60.92/61.01 (~P2(f4(a3),f4(a1),f4(a2))),
% 60.92/61.01 inference(scs_inference,[],[5,3423,3426,1531,3391,3242,3245,56,9,8,7])).
% 60.92/61.01 cnf(3442,plain,
% 60.92/61.01 (~P2(f4(a2),f5(a3,a3),f4(a1))),
% 60.92/61.01 inference(scs_inference,[],[3433,2051,2924,9])).
% 60.92/61.01 cnf(3449,plain,
% 60.92/61.01 (P2(a3,f5(a1,a1),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3442,3404,1047,3336,1362,6,9])).
% 60.92/61.01 cnf(3451,plain,
% 60.92/61.01 (~P2(f5(a3,a3),f4(a2),f4(a1))),
% 60.92/61.01 inference(scs_inference,[],[3442,3404,1047,3336,2043,2051,1362,6,9,8])).
% 60.92/61.01 cnf(3455,plain,
% 60.92/61.01 (P2(f5(a3,a1),f4(a3),a2)),
% 60.92/61.01 inference(scs_inference,[],[3214,669,127,9])).
% 60.92/61.01 cnf(3458,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a2),a1)),
% 60.92/61.01 inference(scs_inference,[],[3449,3214,3307,669,1047,127,9,8])).
% 60.92/61.01 cnf(3460,plain,
% 60.92/61.01 (P1(f5(a1,a3),a2)),
% 60.92/61.01 inference(scs_inference,[],[3449,3214,3307,669,1047,2924,127,9,8,7])).
% 60.92/61.01 cnf(3467,plain,
% 60.92/61.01 (P2(f5(a2,a3),a2,f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3430,3379,3433,3043,1992,2924,9,8])).
% 60.92/61.01 cnf(3469,plain,
% 60.92/61.01 (P2(a1,a1,f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3467,3430,3062,9])).
% 60.92/61.01 cnf(3471,plain,
% 60.92/61.01 (P2(a1,f5(a2,a3),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3469,3371,3430,9])).
% 60.92/61.01 cnf(3473,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a1),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[3469,3449,3325,3162,3371,3430,9,8])).
% 60.92/61.01 cnf(3475,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a2),a2)),
% 60.92/61.01 inference(scs_inference,[],[3469,3460,3449,3325,3162,3319,3371,3430,9,8,6])).
% 60.92/61.01 cnf(3477,plain,
% 60.92/61.01 (P1(f5(a1,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[695,2924,7])).
% 60.92/61.01 cnf(3485,plain,
% 60.92/61.01 (P2(a3,f5(a2,a3),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3477,691,6])).
% 60.92/61.01 cnf(3488,plain,
% 60.92/61.01 (P2(f5(a2,a2),f4(a2),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3477,3458,2827,695,691,6,8])).
% 60.92/61.01 cnf(3491,plain,
% 60.92/61.01 (P2(a1,f5(a3,a3),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[3471,3473,3202,9])).
% 60.92/61.01 cnf(3493,plain,
% 60.92/61.01 (P2(a2,f5(a3,a1),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3471,3473,3455,3289,2918,3202,9,8])).
% 60.92/61.01 cnf(3505,plain,
% 60.92/61.01 (P2(a3,f5(a1,a2),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3485,3426,3374,9])).
% 60.92/61.01 cnf(3507,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a2),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3488,3485,3426,3070,3169,3374,9,8])).
% 60.92/61.01 cnf(3510,plain,
% 60.92/61.01 (P1(f5(a1,a2),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3488,3485,3467,3426,3070,3169,3374,2068,9,8,7])).
% 60.92/61.01 cnf(3513,plain,
% 60.92/61.01 (P2(a1,f5(a2,a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3510,3471,6])).
% 60.92/61.01 cnf(3515,plain,
% 60.92/61.01 (P2(a1,a3,f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[3510,3507,3471,1917,6,9])).
% 60.92/61.01 cnf(3529,plain,
% 60.92/61.01 (P2(a1,a2,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3491,3297,770,9])).
% 60.92/61.01 cnf(3531,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a1),a1)),
% 60.92/61.01 inference(scs_inference,[],[3491,3505,3473,3297,770,2103,9,8])).
% 60.92/61.01 cnf(3538,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[5,3531,3469,127,2,7,9])).
% 60.92/61.01 cnf(3541,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a1),f5(a2,a3))),
% 60.92/61.01 inference(scs_inference,[],[5,3531,3469,3449,3207,127,2,7,9,8])).
% 60.92/61.01 cnf(3543,plain,
% 60.92/61.01 (P2(a2,f5(a2,a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3493,3538,3413,9])).
% 60.92/61.01 cnf(3551,plain,
% 60.92/61.01 (P2(f5(a1,a1),f5(a3,a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3543,3475,1553,9])).
% 60.92/61.01 cnf(3554,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a1),f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3543,3541,3475,3505,3485,1553,9,8])).
% 60.92/61.01 cnf(3560,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a2),a2)),
% 60.92/61.01 inference(scs_inference,[],[1,3458,6])).
% 60.92/61.01 cnf(3569,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3560,3543,1528,9])).
% 60.92/61.01 cnf(3572,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a2),a1)),
% 60.92/61.01 inference(scs_inference,[],[3560,3543,3507,3217,3221,1528,9,8])).
% 60.92/61.01 cnf(3574,plain,
% 60.92/61.01 (P2(a1,a3,f5(a3,a2))),
% 60.92/61.01 inference(scs_inference,[],[3554,3529,1401,9])).
% 60.92/61.01 cnf(3576,plain,
% 60.92/61.01 (P2(f5(a2,a3),f5(a3,a1),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3554,3529,3515,3404,3236,1401,9,8])).
% 60.92/61.01 cnf(3591,plain,
% 60.92/61.01 (P2(f4(a2),f5(a1,a2),a2)),
% 60.92/61.01 inference(scs_inference,[],[1,1531,6])).
% 60.92/61.01 cnf(3593,plain,
% 60.92/61.01 (P2(a2,f4(a3),a1)),
% 60.92/61.01 inference(scs_inference,[],[1,3572,3493,3262,1531,6,9])).
% 60.92/61.01 cnf(3595,plain,
% 60.92/61.01 (P2(a1,f4(a3),a2)),
% 60.92/61.01 inference(scs_inference,[],[1,3572,3569,3493,3262,1531,1796,6,9,8])).
% 60.92/61.01 cnf(3598,plain,
% 60.92/61.01 (P2(a2,f5(a3,a2),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3593,3513,2909,9])).
% 60.92/61.01 cnf(3600,plain,
% 60.92/61.01 (P2(f5(a3,a2),a3,f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[3593,3513,3574,3491,1641,2909,9,8])).
% 60.92/61.01 cnf(3603,plain,
% 60.92/61.01 (P2(f5(a1,a3),a3,a2)),
% 60.92/61.01 inference(scs_inference,[],[1,3593,3513,3574,3491,1641,2909,1690,9,8,6])).
% 60.92/61.01 cnf(3606,plain,
% 60.92/61.01 (P2(f5(a1,a3),a1,f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3603,3598,1047,9])).
% 60.92/61.01 cnf(3617,plain,
% 60.92/61.01 (P2(f5(a1,a1),f4(a3),f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[1,3593,3529,3291,2043,6,8])).
% 60.92/61.01 cnf(3619,plain,
% 60.92/61.01 (P1(f5(a2,a3),a1)),
% 60.92/61.01 inference(scs_inference,[],[1,3593,3529,3291,977,2043,2076,6,8,7])).
% 60.92/61.01 cnf(3622,plain,
% 60.92/61.01 (P2(f5(a1,a3),a2,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3600,3162,3426,8])).
% 60.92/61.01 cnf(3624,plain,
% 60.92/61.01 (P2(f5(a3,a2),a1,f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3622,3600,977,9])).
% 60.92/61.01 cnf(3636,plain,
% 60.92/61.01 (P2(f5(a1,a2),f4(a1),a1)),
% 60.92/61.01 inference(scs_inference,[],[3619,3541,6])).
% 60.92/61.01 cnf(3649,plain,
% 60.92/61.01 (P2(f5(a2,a1),f4(a3),f5(a1,a1))),
% 60.92/61.01 inference(scs_inference,[],[3576,3606,3636,3595,3622,3313,9,8])).
% 60.92/61.01 cnf(3651,plain,
% 60.92/61.01 (P2(f4(a2),f5(a1,a2),f5(a1,a3))),
% 60.92/61.01 inference(scs_inference,[],[2,3591,3162,8])).
% 60.92/61.01 cnf(3654,plain,
% 60.92/61.01 (P2(f5(a3,a2),f5(a1,a3),f5(a2,a1))),
% 60.92/61.01 inference(scs_inference,[],[3624,3551,3491,9])).
% 60.92/61.01 cnf(3656,plain,
% 60.92/61.01 (P2(f5(a1,a3),f4(a2),f4(a3))),
% 60.92/61.01 inference(scs_inference,[],[3624,3651,3551,3560,3491,127,9,8])).
% 60.92/61.01 cnf(3661,plain,
% 60.92/61.01 (P2(f5(a2,a1),a3,f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3649,3617,1243,9])).
% 60.92/61.01 cnf(3677,plain,
% 60.92/61.01 (P2(f5(a3,a2),a2,f5(a1,a2))),
% 60.92/61.01 inference(scs_inference,[],[3654,3661,3603,9])).
% 60.92/61.01 cnf(3684,plain,
% 60.92/61.01 ($false),
% 60.92/61.01 inference(scs_inference,[],[3,3677,3451,3488,3656,1553,1486,9,8]),
% 60.92/61.01 ['proof']).
% 60.92/61.01 % SZS output end Proof
% 60.92/61.01 % Total time :60.370000s
%------------------------------------------------------------------------------