%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP155-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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:39:02 EDT 2024
% Result : Unsatisfiable 63.56s 63.69s
% Output : CNFRefutation 63.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GRP155-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.03/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.30 % Computer : n032.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Thu Jun 20 08:07:08 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.15/0.51 start to proof:theBenchmark
% 63.56/63.68 %-------------------------------------------
% 63.56/63.68 % File :CSE---1.7
% 63.56/63.68 % Problem :theBenchmark
% 63.56/63.68 % Transform :cnf
% 63.56/63.68 % Format :tptp:raw
% 63.56/63.68 % Command :java -jar mcs_scs.jar %d %s
% 63.56/63.68
% 63.56/63.68 % Result :Theorem 63.130000s
% 63.56/63.68 % Output :CNFRefutation 63.130000s
% 63.56/63.68 %-------------------------------------------
% 63.56/63.69 %--------------------------------------------------------------------------
% 63.56/63.69 % File : GRP155-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 63.56/63.69 % Domain : Group Theory (Lattice Ordered)
% 63.56/63.69 % Problem : Prove monotonicity axiom using the GLB transformation
% 63.56/63.69 % Version : [Fuc94] (equality) axioms.
% 63.56/63.69 % English : This problem proves the original monotonicity axiom from the
% 63.56/63.69 % equational axiomatization.
% 63.56/63.69
% 63.56/63.69 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 63.56/63.69 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 63.56/63.69 % Source : [Sch95]
% 63.56/63.69 % Names : ax_mono1b [Sch95]
% 63.56/63.69
% 63.56/63.69 % Status : Unsatisfiable
% 63.56/63.69 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.00 v2.0.0
% 63.56/63.69 % Syntax : Number of clauses : 17 ( 17 unt; 0 nHn; 2 RR)
% 63.56/63.69 % Number of literals : 17 ( 17 equ; 1 neg)
% 63.56/63.69 % Maximal clause size : 1 ( 1 avg)
% 63.56/63.69 % Maximal term depth : 3 ( 2 avg)
% 63.56/63.69 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 63.56/63.69 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 63.56/63.69 % Number of variables : 33 ( 2 sgn)
% 63.56/63.69 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 63.56/63.69
% 63.56/63.69 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 63.56/63.69 % least_upper_bound > identity > a > b > c
% 63.56/63.69 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 63.56/63.69 %--------------------------------------------------------------------------
% 63.56/63.69 %----Include equality group theory axioms
% 63.56/63.69 include('Axioms/GRP004-0.ax').
% 63.56/63.69 %----Include Lattice ordered group (equality) axioms
% 63.56/63.69 include('Axioms/GRP004-2.ax').
% 63.56/63.69 %--------------------------------------------------------------------------
% 63.56/63.69 cnf(ax_mono1b,hypothesis,
% 63.56/63.69 greatest_lower_bound(a,b) = a ).
% 63.56/63.69
% 63.56/63.69 cnf(prove_ax_mono1b,negated_conjecture,
% 63.56/63.69 greatest_lower_bound(multiply(a,c),multiply(b,c)) != multiply(a,c) ).
% 63.56/63.69
% 63.56/63.69 %--------------------------------------------------------------------------
% 63.56/63.69 %-------------------------------------------
% 63.56/63.69 % Proof found
% 63.56/63.69 % SZS status Theorem for theBenchmark
% 63.56/63.69 % SZS output start Proof
% 63.56/63.70 %ClaNum:27(EqnAxiom:10)
% 63.56/63.70 %VarNum:72(SingletonVarNum:33)
% 63.56/63.70 %MaxLitNum:1
% 63.56/63.70 %MaxfuncDepth:2
% 63.56/63.70 %SharedTerms:10
% 63.56/63.70 %goalClause: 27
% 63.56/63.70 %singleGoalClaCount:1
% 63.56/63.70 [11]E(f3(a1,a2),a1)
% 63.56/63.70 [27]~E(f3(f6(a1,a4),f6(a2,a4)),f6(a1,a4))
% 63.56/63.70 [12]E(f6(a5,x121),x121)
% 63.56/63.70 [13]E(f3(x131,x131),x131)
% 63.56/63.70 [14]E(f7(x141,x141),x141)
% 63.56/63.70 [15]E(f6(f8(x151),x151),a5)
% 63.56/63.70 [16]E(f3(x161,x162),f3(x162,x161))
% 63.56/63.70 [17]E(f7(x171,x172),f7(x172,x171))
% 63.56/63.70 [18]E(f3(x181,f7(x181,x182)),x181)
% 63.56/63.70 [19]E(f7(x191,f3(x191,x192)),x191)
% 63.56/63.70 [20]E(f3(f3(x201,x202),x203),f3(x201,f3(x202,x203)))
% 63.56/63.70 [21]E(f7(f7(x211,x212),x213),f7(x211,f7(x212,x213)))
% 63.56/63.70 [22]E(f6(f6(x221,x222),x223),f6(x221,f6(x222,x223)))
% 63.56/63.70 [23]E(f3(f6(x231,x232),f6(x231,x233)),f6(x231,f3(x232,x233)))
% 63.56/63.70 [24]E(f7(f6(x241,x242),f6(x241,x243)),f6(x241,f7(x242,x243)))
% 63.56/63.70 [25]E(f3(f6(x251,x252),f6(x253,x252)),f6(f3(x251,x253),x252))
% 63.56/63.70 [26]E(f7(f6(x261,x262),f6(x263,x262)),f6(f7(x261,x263),x262))
% 63.56/63.70 %EqnAxiom
% 63.56/63.70 [1]E(x11,x11)
% 63.56/63.70 [2]E(x22,x21)+~E(x21,x22)
% 63.56/63.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 63.56/63.70 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 63.56/63.70 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 63.56/63.70 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 63.56/63.70 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 63.56/63.70 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83))
% 63.56/63.70 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92))
% 63.56/63.70 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 63.56/63.70
% 63.56/63.70 %-------------------------------------------
% 63.56/63.70 cnf(28,plain,
% 63.56/63.70 (E(x281,f3(x281,x281))),
% 63.56/63.70 inference(scs_inference,[],[13,2])).
% 63.56/63.70 cnf(33,plain,
% 63.56/63.70 (E(x331,f7(x331,x331))),
% 63.56/63.70 inference(scs_inference,[],[14,2])).
% 63.56/63.70 cnf(34,plain,
% 63.56/63.71 (~E(f3(f6(a1,a4),f6(a2,a4)),f7(f6(a1,a4),f6(a1,a4)))),
% 63.56/63.71 inference(scs_inference,[],[27,14,2,3])).
% 63.56/63.71 cnf(36,plain,
% 63.56/63.71 (E(x361,f6(a5,x361))),
% 63.56/63.71 inference(scs_inference,[],[12,2])).
% 63.56/63.71 cnf(40,plain,
% 63.56/63.71 (E(f6(x401,x402),f6(x401,f3(x402,x402)))),
% 63.56/63.71 inference(scs_inference,[],[28,23,2,3])).
% 63.56/63.71 cnf(43,plain,
% 63.56/63.71 (E(f6(x431,f3(x432,x432)),f6(x431,x432))),
% 63.56/63.71 inference(scs_inference,[],[40,2])).
% 63.56/63.71 cnf(47,plain,
% 63.56/63.71 (E(f6(x471,x472),f6(x471,f7(x472,x472)))),
% 63.56/63.71 inference(scs_inference,[],[33,24,2,3])).
% 63.56/63.71 cnf(50,plain,
% 63.56/63.71 (E(f6(x501,f7(x502,x502)),f6(x501,x502))),
% 63.56/63.71 inference(scs_inference,[],[47,2])).
% 63.56/63.71 cnf(53,plain,
% 63.56/63.71 (E(f6(f3(x531,x532),x533),f3(f6(x531,x533),f6(x532,x533)))),
% 63.56/63.71 inference(scs_inference,[],[25,2])).
% 63.56/63.71 cnf(54,plain,
% 63.56/63.71 (E(f6(x541,x542),f6(f3(x541,x541),x542))),
% 63.56/63.71 inference(scs_inference,[],[28,25,2,3])).
% 63.56/63.71 cnf(57,plain,
% 63.56/63.71 (E(f6(f3(x571,x571),x572),f6(x571,x572))),
% 63.56/63.71 inference(scs_inference,[],[54,2])).
% 63.56/63.71 cnf(60,plain,
% 63.56/63.71 (E(f6(f7(x601,x602),x603),f7(f6(x601,x603),f6(x602,x603)))),
% 63.56/63.71 inference(scs_inference,[],[26,2])).
% 63.56/63.71 cnf(61,plain,
% 63.56/63.71 (E(f6(x611,x612),f6(f7(x611,x611),x612))),
% 63.56/63.71 inference(scs_inference,[],[33,26,2,3])).
% 63.56/63.71 cnf(64,plain,
% 63.56/63.71 (E(f6(f7(x641,x641),x642),f6(x641,x642))),
% 63.56/63.71 inference(scs_inference,[],[61,2])).
% 63.56/63.71 cnf(65,plain,
% 63.56/63.71 (~E(f3(f6(a1,a4),f6(a2,a4)),f6(f7(a1,a1),a4))),
% 63.56/63.71 inference(scs_inference,[],[60,61,34,2,3])).
% 63.56/63.71 cnf(67,plain,
% 63.56/63.71 (E(x671,f3(x671,f7(x671,x672)))),
% 63.56/63.71 inference(scs_inference,[],[18,2])).
% 63.56/63.71 cnf(68,plain,
% 63.56/63.71 (E(f3(x681,x682),f3(x681,f3(x682,f3(x681,x682))))),
% 63.56/63.71 inference(scs_inference,[],[28,18,20,2,3])).
% 63.56/63.71 cnf(72,plain,
% 63.56/63.71 (E(f7(x721,x722),f7(x721,f7(x722,f7(x721,x722))))),
% 63.56/63.71 inference(scs_inference,[],[33,68,21,2,3])).
% 63.56/63.71 cnf(80,plain,
% 63.56/63.71 (E(a5,f6(f8(x801),x801))),
% 63.56/63.71 inference(scs_inference,[],[15,2])).
% 63.56/63.71 cnf(84,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x841)),f6(f8(x842),x842))),
% 63.56/63.71 inference(scs_inference,[],[80,18,20,2,3])).
% 63.56/63.71 cnf(86,plain,
% 63.56/63.71 (E(f6(f8(x861),x861),f3(a5,f7(a5,x862)))),
% 63.56/63.71 inference(scs_inference,[],[84,2])).
% 63.56/63.71 cnf(87,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x871)),f6(f8(x872),x872))),
% 63.56/63.71 inference(scs_inference,[],[80,84,19,2,3])).
% 63.56/63.71 cnf(89,plain,
% 63.56/63.71 (E(f6(f8(x891),x891),f7(a5,f3(a5,x892)))),
% 63.56/63.71 inference(scs_inference,[],[87,2])).
% 63.56/63.71 cnf(90,plain,
% 63.56/63.71 (E(f6(f8(x901),f3(x901,x901)),f3(a5,f7(a5,x902)))),
% 63.56/63.71 inference(scs_inference,[],[43,86,87,2,3])).
% 63.56/63.71 cnf(93,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x931)),f6(f8(x932),f3(x932,x932)))),
% 63.56/63.71 inference(scs_inference,[],[90,2])).
% 63.56/63.71 cnf(94,plain,
% 63.56/63.71 (E(f6(f8(x941),f7(x941,x941)),f7(a5,f3(a5,x942)))),
% 63.56/63.71 inference(scs_inference,[],[50,89,90,2,3])).
% 63.56/63.71 cnf(97,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x971)),f6(f8(x972),f7(x972,x972)))),
% 63.56/63.71 inference(scs_inference,[],[94,2])).
% 63.56/63.71 cnf(98,plain,
% 63.56/63.71 (E(a5,f6(f8(x981),f3(x981,x981)))),
% 63.56/63.71 inference(scs_inference,[],[67,93,94,2,3])).
% 63.56/63.71 cnf(101,plain,
% 63.56/63.71 (E(f6(f8(x1011),f3(x1011,x1011)),a5)),
% 63.56/63.71 inference(scs_inference,[],[98,2])).
% 63.56/63.71 cnf(104,plain,
% 63.56/63.71 (E(f6(f3(f8(x1041),f8(x1041)),f3(x1041,x1041)),a5)),
% 63.56/63.71 inference(scs_inference,[],[57,101,21,2,3])).
% 63.56/63.71 cnf(106,plain,
% 63.56/63.71 (E(a5,f6(f3(f8(x1061),f8(x1061)),f3(x1061,x1061)))),
% 63.56/63.71 inference(scs_inference,[],[104,2])).
% 63.56/63.71 cnf(107,plain,
% 63.56/63.71 (E(f6(f7(f8(x1071),f8(x1071)),f3(x1071,x1071)),a5)),
% 63.56/63.71 inference(scs_inference,[],[64,101,104,2,3])).
% 63.56/63.71 cnf(109,plain,
% 63.56/63.71 (E(a5,f6(f7(f8(x1091),f8(x1091)),f3(x1091,x1091)))),
% 63.56/63.71 inference(scs_inference,[],[107,2])).
% 63.56/63.71 cnf(110,plain,
% 63.56/63.71 (E(f6(f8(x1101),f3(x1101,x1101)),f6(f3(f8(x1102),f8(x1102)),f3(x1102,x1102)))),
% 63.56/63.71 inference(scs_inference,[],[106,101,107,2,3])).
% 63.56/63.71 cnf(111,plain,
% 63.56/63.71 (E(f6(f3(f8(x1111),f8(x1111)),f3(x1111,x1111)),f6(f8(x1112),f3(x1112,x1112)))),
% 63.56/63.71 inference(scs_inference,[],[110,2])).
% 63.56/63.71 cnf(112,plain,
% 63.56/63.71 (E(f6(f8(x1121),f3(x1121,x1121)),f6(f7(f8(x1122),f8(x1122)),f3(x1122,x1122)))),
% 63.56/63.71 inference(scs_inference,[],[109,101,110,2,3])).
% 63.56/63.71 cnf(113,plain,
% 63.56/63.71 (E(f6(f7(f8(x1131),f8(x1131)),f3(x1131,x1131)),f6(f8(x1132),f3(x1132,x1132)))),
% 63.56/63.71 inference(scs_inference,[],[112,2])).
% 63.56/63.71 cnf(114,plain,
% 63.56/63.71 (E(f6(f8(x1141),f3(x1141,x1141)),f7(a5,f3(a5,x1142)))),
% 63.56/63.71 inference(scs_inference,[],[43,89,112,2,3])).
% 63.56/63.71 cnf(117,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x1171)),f6(f8(x1172),f3(x1172,x1172)))),
% 63.56/63.71 inference(scs_inference,[],[114,2])).
% 63.56/63.71 cnf(118,plain,
% 63.56/63.71 (E(f6(f8(x1181),f7(x1181,x1181)),f3(a5,f7(a5,x1182)))),
% 63.56/63.71 inference(scs_inference,[],[50,86,114,2,3])).
% 63.56/63.71 cnf(121,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x1211)),f6(f8(x1212),f7(x1212,x1212)))),
% 63.56/63.71 inference(scs_inference,[],[118,2])).
% 63.56/63.71 cnf(122,plain,
% 63.56/63.71 (E(f6(f8(x1221),f3(x1221,x1221)),f6(f8(x1222),x1222))),
% 63.56/63.71 inference(scs_inference,[],[80,101,118,2,3])).
% 63.56/63.71 cnf(123,plain,
% 63.56/63.71 (E(f6(f8(x1231),x1231),f6(f8(x1232),f3(x1232,x1232)))),
% 63.56/63.71 inference(scs_inference,[],[122,2])).
% 63.56/63.71 cnf(124,plain,
% 63.56/63.71 (E(f6(f3(f8(x1241),f8(x1241)),f3(x1241,x1241)),f6(f8(x1242),x1242))),
% 63.56/63.71 inference(scs_inference,[],[111,122,2,3])).
% 63.56/63.71 cnf(126,plain,
% 63.56/63.71 (E(f6(f8(x1261),x1261),f6(f3(f8(x1262),f8(x1262)),f3(x1262,x1262)))),
% 63.56/63.71 inference(scs_inference,[],[124,2])).
% 63.56/63.71 cnf(127,plain,
% 63.56/63.71 (E(f6(f7(f8(x1271),f8(x1271)),f3(x1271,x1271)),f3(a5,f7(a5,x1272)))),
% 63.56/63.71 inference(scs_inference,[],[113,124,90,2,3])).
% 63.56/63.71 cnf(129,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x1291)),f6(f7(f8(x1292),f8(x1292)),f3(x1292,x1292)))),
% 63.56/63.71 inference(scs_inference,[],[127,2])).
% 63.56/63.71 cnf(130,plain,
% 63.56/63.71 (E(f6(f8(x1301),x1301),f6(f7(f8(x1302),f8(x1302)),f3(x1302,x1302)))),
% 63.56/63.71 inference(scs_inference,[],[123,127,112,2,3])).
% 63.56/63.71 cnf(132,plain,
% 63.56/63.71 (E(f6(f7(f8(x1321),f8(x1321)),f3(x1321,x1321)),f6(f8(x1322),x1322))),
% 63.56/63.71 inference(scs_inference,[],[130,2])).
% 63.56/63.71 cnf(133,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x1331)),f6(f3(f8(x1332),f8(x1332)),f3(x1332,x1332)))),
% 63.56/63.71 inference(scs_inference,[],[117,130,110,2,3])).
% 63.56/63.71 cnf(136,plain,
% 63.56/63.71 (E(f6(f7(f8(x1361),f8(x1361)),f3(x1361,x1361)),f7(a5,f3(a5,x1362)))),
% 63.56/63.71 inference(scs_inference,[],[132,89,133,2,3])).
% 63.56/63.71 cnf(139,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x1391)),f7(a5,f3(a5,x1392)))),
% 63.56/63.71 inference(scs_inference,[],[129,136,2,3])).
% 63.56/63.71 cnf(141,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x1411)),f3(a5,f7(a5,x1412)))),
% 63.56/63.71 inference(scs_inference,[],[139,2])).
% 63.56/63.71 cnf(144,plain,
% 63.56/63.71 (E(f6(x1441,f6(x1442,x1443)),f6(f6(x1441,x1442),x1443))),
% 63.56/63.71 inference(scs_inference,[],[22,2])).
% 63.56/63.71 cnf(147,plain,
% 63.56/63.71 (E(a1,f3(a1,a2))),
% 63.56/63.71 inference(scs_inference,[],[11,2])).
% 63.56/63.71 cnf(151,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x1511)),f6(f3(f8(x1512),f8(x1512)),f3(x1512,x1512)))),
% 63.56/63.71 inference(scs_inference,[],[57,90,3,2])).
% 63.56/63.71 cnf(154,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x1541)),f6(f7(f8(x1542),f8(x1542)),f7(x1542,x1542)))),
% 63.56/63.71 inference(scs_inference,[],[64,94,3,2])).
% 63.56/63.71 cnf(173,plain,
% 63.56/63.71 (E(f6(a5,a5),f6(f3(f8(x1731),f8(x1731)),f3(x1731,x1731)))),
% 63.56/63.71 inference(scs_inference,[],[12,106,3])).
% 63.56/63.71 cnf(175,plain,
% 63.56/63.71 (E(f6(f3(f8(x1751),f8(x1751)),f3(x1751,x1751)),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,106,3,2])).
% 63.56/63.71 cnf(176,plain,
% 63.56/63.71 (E(f6(a5,a5),f6(f7(f8(x1761),f8(x1761)),f3(x1761,x1761)))),
% 63.56/63.71 inference(scs_inference,[],[12,109,3])).
% 63.56/63.71 cnf(178,plain,
% 63.56/63.71 (E(f6(f7(f8(x1781),f8(x1781)),f3(x1781,x1781)),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,109,3,2])).
% 63.56/63.71 cnf(179,plain,
% 63.56/63.71 (E(f6(a5,a5),f6(f8(x1791),x1791))),
% 63.56/63.71 inference(scs_inference,[],[12,80,3])).
% 63.56/63.71 cnf(181,plain,
% 63.56/63.71 (E(f6(f8(x1811),x1811),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,80,3,2])).
% 63.56/63.71 cnf(182,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x1821),x1821)),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,181,3])).
% 63.56/63.71 cnf(185,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x1851),f3(x1851,x1851))),a5)),
% 63.56/63.71 inference(scs_inference,[],[12,101,3])).
% 63.56/63.71 cnf(187,plain,
% 63.56/63.71 (E(a5,f6(a5,f6(f8(x1871),f3(x1871,x1871))))),
% 63.56/63.71 inference(scs_inference,[],[12,101,3,2])).
% 63.56/63.71 cnf(190,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x1901),f3(x1901,x1901))),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,187,3,2])).
% 63.56/63.71 cnf(197,plain,
% 63.56/63.71 (E(f6(a5,f6(a5,a5)),f6(f3(f8(x1971),f8(x1971)),f3(x1971,x1971)))),
% 63.56/63.71 inference(scs_inference,[],[12,173,3])).
% 63.56/63.71 cnf(199,plain,
% 63.56/63.71 (E(f6(f3(f8(x1991),f8(x1991)),f3(x1991,x1991)),f6(a5,f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[12,173,3,2])).
% 63.56/63.71 cnf(200,plain,
% 63.56/63.71 (E(f6(a5,a5),f6(f8(x2001),f3(x2001,x2001)))),
% 63.56/63.71 inference(scs_inference,[],[12,98,3])).
% 63.56/63.71 cnf(202,plain,
% 63.56/63.71 (E(f6(f8(x2021),f3(x2021,x2021)),f6(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[12,98,3,2])).
% 63.56/63.71 cnf(203,plain,
% 63.56/63.71 (E(f6(a5,f6(a5,a5)),f6(f8(x2031),f3(x2031,x2031)))),
% 63.56/63.71 inference(scs_inference,[],[12,200,3])).
% 63.56/63.71 cnf(205,plain,
% 63.56/63.71 (E(f6(f8(x2051),f3(x2051,x2051)),f6(a5,f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[12,200,3,2])).
% 63.56/63.71 cnf(206,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x2061),x2061)),a5)),
% 63.56/63.71 inference(scs_inference,[],[12,15,3])).
% 63.56/63.71 cnf(208,plain,
% 63.56/63.71 (E(a5,f6(a5,f6(f8(x2081),x2081)))),
% 63.56/63.71 inference(scs_inference,[],[12,15,3,2])).
% 63.56/63.71 cnf(211,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x2111),x2111)),f3(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[13,208,3,2])).
% 63.56/63.71 cnf(214,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x2141),f3(x2141,x2141))),f3(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[13,187,3,2])).
% 63.56/63.71 cnf(215,plain,
% 63.56/63.71 (E(f3(a5,a5),f6(f3(f8(x2151),f8(x2151)),f3(x2151,x2151)))),
% 63.56/63.71 inference(scs_inference,[],[13,106,3])).
% 63.56/63.71 cnf(218,plain,
% 63.56/63.71 (E(f3(a5,a5),f6(f7(f8(x2181),f8(x2181)),f3(x2181,x2181)))),
% 63.56/63.71 inference(scs_inference,[],[13,109,3])).
% 63.56/63.71 cnf(220,plain,
% 63.56/63.71 (E(f6(f7(f8(x2201),f8(x2201)),f3(x2201,x2201)),f3(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[13,109,3,2])).
% 63.56/63.71 cnf(221,plain,
% 63.56/63.71 (E(f3(a5,a5),f6(f8(x2211),x2211))),
% 63.56/63.71 inference(scs_inference,[],[13,80,3])).
% 63.56/63.71 cnf(223,plain,
% 63.56/63.71 (E(f6(f8(x2231),x2231),f3(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[13,80,3,2])).
% 63.56/63.71 cnf(226,plain,
% 63.56/63.71 (E(f6(f8(x2261),x2261),f3(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,221,3,2])).
% 63.56/63.71 cnf(229,plain,
% 63.56/63.71 (E(f6(f7(f8(x2291),f8(x2291)),f3(x2291,x2291)),f3(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,218,3,2])).
% 63.56/63.71 cnf(232,plain,
% 63.56/63.71 (E(f6(f3(f8(x2321),f8(x2321)),f3(x2321,x2321)),f3(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,215,3,2])).
% 63.56/63.71 cnf(235,plain,
% 63.56/63.71 (E(f6(f8(x2351),f3(x2351,x2351)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,200,3,2])).
% 63.56/63.71 cnf(238,plain,
% 63.56/63.71 (E(f6(f8(x2381),x2381),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,179,3,2])).
% 63.56/63.71 cnf(244,plain,
% 63.56/63.71 (E(f6(f3(f8(x2441),f8(x2441)),f3(x2441,x2441)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,173,3,2])).
% 63.56/63.71 cnf(245,plain,
% 63.56/63.71 (E(f3(a5,a5),f6(f8(x2451),f3(x2451,x2451)))),
% 63.56/63.71 inference(scs_inference,[],[13,98,3])).
% 63.56/63.71 cnf(250,plain,
% 63.56/63.71 (E(f6(f8(x2501),f3(x2501,x2501)),f3(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[13,245,3,2])).
% 63.56/63.71 cnf(253,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x2531),x2531)),f7(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[14,208,3,2])).
% 63.56/63.71 cnf(256,plain,
% 63.56/63.71 (E(f6(a5,f6(f8(x2561),f3(x2561,x2561))),f7(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[14,187,3,2])).
% 63.56/63.71 cnf(260,plain,
% 63.56/63.71 (E(f7(a5,a5),f6(f7(f8(x2601),f8(x2601)),f3(x2601,x2601)))),
% 63.56/63.71 inference(scs_inference,[],[14,109,3])).
% 63.56/63.71 cnf(262,plain,
% 63.56/63.71 (E(f6(f7(f8(x2621),f8(x2621)),f3(x2621,x2621)),f7(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[14,109,3,2])).
% 63.56/63.71 cnf(265,plain,
% 63.56/63.71 (E(f6(f8(x2651),x2651),f7(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[14,80,3,2])).
% 63.56/63.71 cnf(271,plain,
% 63.56/63.71 (E(f6(f7(f8(x2711),f8(x2711)),f3(x2711,x2711)),f7(f7(a5,a5),f7(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,260,3,2])).
% 63.56/63.71 cnf(277,plain,
% 63.56/63.71 (E(f6(f8(x2771),f3(x2771,x2771)),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,245,3,2])).
% 63.56/63.71 cnf(280,plain,
% 63.56/63.71 (E(f6(f8(x2801),x2801),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,221,3,2])).
% 63.56/63.71 cnf(283,plain,
% 63.56/63.71 (E(f6(f7(f8(x2831),f8(x2831)),f3(x2831,x2831)),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,218,3,2])).
% 63.56/63.71 cnf(295,plain,
% 63.56/63.71 (E(f6(f7(f8(x2951),f8(x2951)),f3(x2951,x2951)),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,176,3,2])).
% 63.56/63.71 cnf(298,plain,
% 63.56/63.71 (E(f6(f3(f8(x2981),f8(x2981)),f3(x2981,x2981)),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[14,173,3,2])).
% 63.56/63.71 cnf(301,plain,
% 63.56/63.71 (E(f6(f8(x3011),f3(x3011,x3011)),f7(a5,a5))),
% 63.56/63.71 inference(scs_inference,[],[14,98,3,2])).
% 63.56/63.71 cnf(308,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x3081)),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[295,129,3])).
% 63.56/63.71 cnf(310,plain,
% 63.56/63.71 (E(f7(f6(a5,a5),f6(a5,a5)),f3(a5,f7(a5,x3101)))),
% 63.56/63.71 inference(scs_inference,[],[295,129,3,2])).
% 63.56/63.71 cnf(316,plain,
% 63.56/63.71 (E(f6(f8(x3161),f7(x3161,x3161)),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[310,121,3,2])).
% 63.56/63.71 cnf(322,plain,
% 63.56/63.71 (E(f6(f3(f8(x3221),f8(x3221)),f3(x3221,x3221)),f3(f7(a5,x3222),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,151,3,2])).
% 63.56/63.71 cnf(325,plain,
% 63.56/63.71 (E(f3(f7(a5,x3251),a5),f6(f8(x3252),x3252))),
% 63.56/63.71 inference(scs_inference,[],[126,322,3,2])).
% 63.56/63.71 cnf(326,plain,
% 63.56/63.71 (E(f3(f7(a5,x3261),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[280,325,3])).
% 63.56/63.71 cnf(328,plain,
% 63.56/63.71 (E(f7(f3(a5,a5),f3(a5,a5)),f3(f7(a5,x3281),a5))),
% 63.56/63.71 inference(scs_inference,[],[280,325,3,2])).
% 63.56/63.71 cnf(331,plain,
% 63.56/63.71 (E(f6(f8(x3311),f3(x3311,x3311)),f3(f7(a5,x3312),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,93,3,2])).
% 63.56/63.71 cnf(334,plain,
% 63.56/63.71 (E(f6(f7(f8(x3341),f8(x3341)),f3(x3341,x3341)),f3(f7(a5,x3342),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,129,3,2])).
% 63.56/63.71 cnf(335,plain,
% 63.56/63.71 (E(f3(f7(a5,x3351),a5),f6(f8(x3352),f7(x3352,x3352)))),
% 63.56/63.71 inference(scs_inference,[],[16,121,3])).
% 63.56/63.71 cnf(337,plain,
% 63.56/63.71 (E(f6(f8(x3371),f7(x3371,x3371)),f3(f7(a5,x3372),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,121,3,2])).
% 63.56/63.71 cnf(340,plain,
% 63.56/63.71 (E(f7(f6(a5,a5),f6(a5,a5)),f3(f7(a5,x3401),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,308,3,2])).
% 63.56/63.71 cnf(343,plain,
% 63.56/63.71 (E(f7(f3(a5,a5),f3(a5,a5)),f3(a5,f7(a5,x3431)))),
% 63.56/63.71 inference(scs_inference,[],[16,326,3,2])).
% 63.56/63.71 cnf(346,plain,
% 63.56/63.71 (E(f7(a5,f3(a5,x3461)),f3(f7(a5,x3462),a5))),
% 63.56/63.71 inference(scs_inference,[],[16,139,3,2])).
% 63.56/63.71 cnf(353,plain,
% 63.56/63.71 (E(f6(f7(f8(x3531),f8(x3531)),f7(x3531,x3531)),f7(f3(a5,x3532),a5))),
% 63.56/63.71 inference(scs_inference,[],[17,154,3,2])).
% 63.56/63.71 cnf(356,plain,
% 63.56/63.71 (E(f7(f3(a5,x3561),a5),f7(a5,f3(a5,x3562)))),
% 63.56/63.71 inference(scs_inference,[],[353,154,3,2])).
% 63.56/63.71 cnf(359,plain,
% 63.56/63.71 (E(f3(a5,f7(a5,x3591)),f7(f3(a5,x3592),a5))),
% 63.56/63.71 inference(scs_inference,[],[17,141,3,2])).
% 63.56/63.71 cnf(362,plain,
% 63.56/63.71 (E(f3(f7(a5,x3621),a5),f7(f3(a5,x3622),a5))),
% 63.56/63.71 inference(scs_inference,[],[17,346,3,2])).
% 63.56/63.71 cnf(365,plain,
% 63.56/63.71 (E(f7(f3(a5,x3651),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.71 inference(scs_inference,[],[343,359,3,2])).
% 63.56/63.71 cnf(368,plain,
% 63.56/63.71 (E(f7(f3(a5,x3681),a5),f6(f7(f8(x3682),f8(x3682)),f3(x3682,x3682)))),
% 63.56/63.71 inference(scs_inference,[],[334,362,3,2])).
% 63.56/63.71 cnf(371,plain,
% 63.56/63.71 (E(f3(f3(a5,a5),f3(a5,a5)),f7(f3(a5,x3711),a5))),
% 63.56/63.72 inference(scs_inference,[],[229,368,3,2])).
% 63.56/63.72 cnf(374,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),f7(f3(a5,x3741),a5))),
% 63.56/63.72 inference(scs_inference,[],[271,368,3,2])).
% 63.56/63.72 cnf(376,plain,
% 63.56/63.72 (E(f7(f3(a5,x3761),a5),f6(f8(x3762),f3(x3762,x3762)))),
% 63.56/63.72 inference(scs_inference,[],[250,371,3,2])).
% 63.56/63.72 cnf(379,plain,
% 63.56/63.72 (E(f7(a5,a5),f7(f3(a5,x3791),a5))),
% 63.56/63.72 inference(scs_inference,[],[301,376,3,2])).
% 63.56/63.72 cnf(381,plain,
% 63.56/63.72 (E(f7(f3(a5,x3811),a5),f6(f3(f8(x3812),f8(x3812)),f3(x3812,x3812)))),
% 63.56/63.72 inference(scs_inference,[],[232,371,3,2])).
% 63.56/63.72 cnf(384,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f7(f3(a5,x3841),a5))),
% 63.56/63.72 inference(scs_inference,[],[298,381,3,2])).
% 63.56/63.72 cnf(387,plain,
% 63.56/63.72 (E(f6(f8(x3871),f7(x3871,x3871)),f7(f3(a5,x3872),a5))),
% 63.56/63.72 inference(scs_inference,[],[17,97,3,2])).
% 63.56/63.72 cnf(389,plain,
% 63.56/63.72 (E(f7(f3(a5,x3891),a5),f6(f8(x3892),x3892))),
% 63.56/63.72 inference(scs_inference,[],[226,371,3,2])).
% 63.56/63.72 cnf(392,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f3(a5,x3921),a5))),
% 63.56/63.72 inference(scs_inference,[],[238,389,3,2])).
% 63.56/63.72 cnf(396,plain,
% 63.56/63.72 (E(f6(f8(x3961),f3(x3961,x3961)),f6(f8(x3962),f7(x3962,x3962)))),
% 63.56/63.72 inference(scs_inference,[],[331,335,3])).
% 63.56/63.72 cnf(398,plain,
% 63.56/63.72 (E(f6(f8(x3981),f7(x3981,x3981)),f6(f8(x3982),f3(x3982,x3982)))),
% 63.56/63.72 inference(scs_inference,[],[331,335,3,2])).
% 63.56/63.72 cnf(401,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f8(x4011),f7(x4011,x4011)))),
% 63.56/63.72 inference(scs_inference,[],[398,277,3,2])).
% 63.56/63.72 cnf(404,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[401,316,3,2])).
% 63.56/63.72 cnf(407,plain,
% 63.56/63.72 (E(f6(f8(x4071),x4071),f6(f8(x4072),f7(x4072,x4072)))),
% 63.56/63.72 inference(scs_inference,[],[337,325,3,2])).
% 63.56/63.72 cnf(410,plain,
% 63.56/63.72 (E(f6(f8(x4101),f7(x4101,x4101)),f6(f7(f8(x4102),f8(x4102)),f3(x4102,x4102)))),
% 63.56/63.72 inference(scs_inference,[],[407,132,3,2])).
% 63.56/63.72 cnf(413,plain,
% 63.56/63.72 (E(f3(a5,a5),f7(f3(a5,x4131),a5))),
% 63.56/63.72 inference(scs_inference,[],[223,389,3,2])).
% 63.56/63.72 cnf(416,plain,
% 63.56/63.72 (E(f3(a5,a5),f6(f8(x4161),f7(x4161,x4161)))),
% 63.56/63.72 inference(scs_inference,[],[410,220,3,2])).
% 63.56/63.72 cnf(419,plain,
% 63.56/63.72 (E(f7(a5,a5),f6(f8(x4191),f7(x4191,x4191)))),
% 63.56/63.72 inference(scs_inference,[],[262,410,3,2])).
% 63.56/63.72 cnf(422,plain,
% 63.56/63.72 (E(f3(f7(a5,x4221),a5),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[419,337,3,2])).
% 63.56/63.72 cnf(425,plain,
% 63.56/63.72 (E(f7(a5,a5),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[422,328,3,2])).
% 63.56/63.72 cnf(428,plain,
% 63.56/63.72 (E(f7(a5,a5),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[340,422,3,2])).
% 63.56/63.72 cnf(431,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[416,316,3,2])).
% 63.56/63.72 cnf(434,plain,
% 63.56/63.72 (E(f6(f8(x4341),f7(x4341,x4341)),f6(f3(f8(x4342),f8(x4342)),f3(x4342,x4342)))),
% 63.56/63.72 inference(scs_inference,[],[111,396,3,2])).
% 63.56/63.72 cnf(435,plain,
% 63.56/63.72 (E(f6(f8(x4351),f7(x4351,x4351)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[434,244,3])).
% 63.56/63.72 cnf(437,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f8(x4371),f7(x4371,x4371)))),
% 63.56/63.72 inference(scs_inference,[],[434,244,3,2])).
% 63.56/63.72 cnf(441,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f3(f7(a5,x4411),a5))),
% 63.56/63.72 inference(scs_inference,[],[437,337,3])).
% 63.56/63.72 cnf(443,plain,
% 63.56/63.72 (E(f3(f7(a5,x4431),a5),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[437,337,3,2])).
% 63.56/63.72 cnf(449,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[401,435,3,2])).
% 63.56/63.72 cnf(455,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[437,316,3,2])).
% 63.56/63.72 cnf(469,plain,
% 63.56/63.72 (E(f7(x4691,f7(x4692,f7(x4691,x4692))),f7(x4692,x4691))),
% 63.56/63.72 inference(scs_inference,[],[17,72,3,2])).
% 63.56/63.72 cnf(495,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x4951)),f3(x4951,x4951)),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,190,3])).
% 63.56/63.72 cnf(497,plain,
% 63.56/63.72 (E(f6(a5,a5),f6(f6(a5,f8(x4971)),f3(x4971,x4971)))),
% 63.56/63.72 inference(scs_inference,[],[495,2])).
% 63.56/63.72 cnf(498,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x4981)),f3(x4981,x4981)),f3(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,214,495,2,3])).
% 63.56/63.72 cnf(500,plain,
% 63.56/63.72 (E(f3(a5,a5),f6(f6(a5,f8(x5001)),f3(x5001,x5001)))),
% 63.56/63.72 inference(scs_inference,[],[498,2])).
% 63.56/63.72 cnf(501,plain,
% 63.56/63.72 (E(f6(f8(x5011),f3(x5011,x5011)),f6(f6(a5,f8(x5012)),f3(x5012,x5012)))),
% 63.56/63.72 inference(scs_inference,[],[202,497,498,2,3])).
% 63.56/63.72 cnf(502,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5021)),f3(x5021,x5021)),f6(f8(x5022),f3(x5022,x5022)))),
% 63.56/63.72 inference(scs_inference,[],[501,2])).
% 63.56/63.72 cnf(503,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f6(f6(a5,f8(x5031)),f3(x5031,x5031)))),
% 63.56/63.72 inference(scs_inference,[],[431,500,501,2,3])).
% 63.56/63.72 cnf(505,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5051)),f3(x5051,x5051)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[235,502,503,2,3])).
% 63.56/63.72 cnf(507,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f6(a5,f8(x5071)),f3(x5071,x5071)))),
% 63.56/63.72 inference(scs_inference,[],[505,2])).
% 63.56/63.72 cnf(508,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5081)),f3(x5081,x5081)),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,256,505,2,3])).
% 63.56/63.72 cnf(510,plain,
% 63.56/63.72 (E(f7(a5,a5),f6(f6(a5,f8(x5101)),f3(x5101,x5101)))),
% 63.56/63.72 inference(scs_inference,[],[508,2])).
% 63.56/63.72 cnf(511,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5111)),x5111),f3(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,211,508,2,3])).
% 63.56/63.72 cnf(515,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5151)),x5151),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,253,511,2,3])).
% 63.56/63.72 cnf(519,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(f8(x5191),f3(x5191,x5191)))),
% 63.56/63.72 inference(scs_inference,[],[22,203,515,2,3])).
% 63.56/63.72 cnf(521,plain,
% 63.56/63.72 (E(f6(f8(x5211),f3(x5211,x5211)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[519,2])).
% 63.56/63.72 cnf(522,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(f3(f8(x5221),f8(x5221)),f3(x5221,x5221)))),
% 63.56/63.72 inference(scs_inference,[],[22,197,519,2,3])).
% 63.56/63.72 cnf(524,plain,
% 63.56/63.72 (E(f6(f3(f8(x5241),f8(x5241)),f3(x5241,x5241)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[522,2])).
% 63.56/63.72 cnf(525,plain,
% 63.56/63.72 (E(f6(f7(f8(x5251),f8(x5251)),f3(x5251,x5251)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[521,113,522,2,3])).
% 63.56/63.72 cnf(527,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(f7(f8(x5271),f8(x5271)),f3(x5271,x5271)))),
% 63.56/63.72 inference(scs_inference,[],[525,2])).
% 63.56/63.72 cnf(528,plain,
% 63.56/63.72 (E(f6(f8(x5281),f7(x5281,x5281)),f6(a5,f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[205,398,525,2,3])).
% 63.56/63.72 cnf(530,plain,
% 63.56/63.72 (E(f6(a5,f6(a5,a5)),f6(f8(x5301),f7(x5301,x5301)))),
% 63.56/63.72 inference(scs_inference,[],[528,2])).
% 63.56/63.72 cnf(531,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[178,527,528,2,3])).
% 63.56/63.72 cnf(533,plain,
% 63.56/63.72 (E(f6(a5,a5),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[531,2])).
% 63.56/63.72 cnf(534,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(f8(x5341),f7(x5341,x5341)))),
% 63.56/63.72 inference(scs_inference,[],[22,530,531,2,3])).
% 63.56/63.72 cnf(536,plain,
% 63.56/63.72 (E(f6(f8(x5361),f7(x5361,x5361)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[534,2])).
% 63.56/63.72 cnf(537,plain,
% 63.56/63.72 (E(f6(f8(x5371),x5371),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[524,126,534,2,3])).
% 63.56/63.72 cnf(540,plain,
% 63.56/63.72 (E(f3(a5,f7(a5,x5401)),f6(a5,f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[199,151,537,2,3])).
% 63.56/63.72 cnf(542,plain,
% 63.56/63.72 (E(f6(a5,f6(a5,a5)),f3(a5,f7(a5,x5421)))),
% 63.56/63.72 inference(scs_inference,[],[540,2])).
% 63.56/63.72 cnf(543,plain,
% 63.56/63.72 (E(f7(f3(a5,x5431),a5),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[175,381,540,2,3])).
% 63.56/63.72 cnf(545,plain,
% 63.56/63.72 (E(f6(a5,a5),f7(f3(a5,x5451),a5))),
% 63.56/63.72 inference(scs_inference,[],[543,2])).
% 63.56/63.72 cnf(546,plain,
% 63.56/63.72 (E(a5,f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[533,36,543,2,3])).
% 63.56/63.72 cnf(548,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),a5)),
% 63.56/63.72 inference(scs_inference,[],[546,2])).
% 63.56/63.72 cnf(549,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f3(a5,f7(a5,x5491)))),
% 63.56/63.72 inference(scs_inference,[],[22,542,546,2,3])).
% 63.56/63.72 cnf(551,plain,
% 63.56/63.72 (E(f3(a5,f7(a5,x5511)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[549,2])).
% 63.56/63.72 cnf(552,plain,
% 63.56/63.72 (E(f6(a5,f6(a5,a5)),a5)),
% 63.56/63.72 inference(scs_inference,[],[144,548,549,2,3])).
% 63.56/63.72 cnf(554,plain,
% 63.56/63.72 (E(a5,f6(a5,f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[552,2])).
% 63.56/63.72 cnf(555,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[283,527,552,2,3])).
% 63.56/63.72 cnf(557,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[555,2])).
% 63.56/63.72 cnf(558,plain,
% 63.56/63.72 (E(f6(f8(x5581),f7(x5581,x5581)),a5)),
% 63.56/63.72 inference(scs_inference,[],[536,548,555,2,3])).
% 63.56/63.72 cnf(559,plain,
% 63.56/63.72 (E(a5,f6(f8(x5591),f7(x5591,x5591)))),
% 63.56/63.72 inference(scs_inference,[],[558,2])).
% 63.56/63.72 cnf(560,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),a5)),
% 63.56/63.72 inference(scs_inference,[],[557,548,558,2,3])).
% 63.56/63.72 cnf(562,plain,
% 63.56/63.72 (E(a5,f7(f3(a5,x5621),a5))),
% 63.56/63.72 inference(scs_inference,[],[387,559,560,2,3])).
% 63.56/63.72 cnf(564,plain,
% 63.56/63.72 (E(f7(f3(a5,x5641),a5),a5)),
% 63.56/63.72 inference(scs_inference,[],[562,2])).
% 63.56/63.72 cnf(565,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5651)),x5651),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[22,182,562,2,3])).
% 63.56/63.72 cnf(569,plain,
% 63.56/63.72 (E(f7(f3(a5,x5691),a5),f6(a5,f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[554,564,565,2,3])).
% 63.56/63.72 cnf(570,plain,
% 63.56/63.72 (E(f6(a5,f6(a5,a5)),f7(f3(a5,x5701),a5))),
% 63.56/63.72 inference(scs_inference,[],[569,2])).
% 63.56/63.72 cnf(571,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5711)),f3(x5711,x5711)),a5)),
% 63.56/63.72 inference(scs_inference,[],[22,569,185,2,3])).
% 63.56/63.72 cnf(573,plain,
% 63.56/63.72 (E(a5,f6(f6(a5,f8(x5731)),f3(x5731,x5731)))),
% 63.56/63.72 inference(scs_inference,[],[571,2])).
% 63.56/63.72 cnf(574,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f7(f3(a5,x5741),a5))),
% 63.56/63.72 inference(scs_inference,[],[22,570,571,2,3])).
% 63.56/63.72 cnf(576,plain,
% 63.56/63.72 (E(f7(f3(a5,x5761),a5),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[574,2])).
% 63.56/63.72 cnf(577,plain,
% 63.56/63.72 (E(f7(f3(a5,x5771),a5),f6(f6(a5,f8(x5772)),f3(x5772,x5772)))),
% 63.56/63.72 inference(scs_inference,[],[573,564,574,2,3])).
% 63.56/63.72 cnf(578,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5781)),f3(x5781,x5781)),f7(f3(a5,x5782),a5))),
% 63.56/63.72 inference(scs_inference,[],[577,2])).
% 63.56/63.72 cnf(579,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x5791)),x5791),a5)),
% 63.56/63.72 inference(scs_inference,[],[22,577,206,2,3])).
% 63.56/63.72 cnf(583,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[507,579,498,2,3])).
% 63.56/63.72 cnf(585,plain,
% 63.56/63.72 (E(f3(a5,a5),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[583,2])).
% 63.56/63.72 cnf(586,plain,
% 63.56/63.72 (E(f7(a5,a5),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[510,583,495,2,3])).
% 63.56/63.72 cnf(588,plain,
% 63.56/63.72 (E(f6(a5,a5),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[586,2])).
% 63.56/63.72 cnf(589,plain,
% 63.56/63.72 (E(f7(a5,f7(a5,f7(a5,a5))),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[469,586,2,3])).
% 63.56/63.72 cnf(592,plain,
% 63.56/63.72 (E(f6(a5,a5),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[425,588,589,2,3])).
% 63.56/63.72 cnf(593,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[592,2])).
% 63.56/63.72 cnf(594,plain,
% 63.56/63.72 (E(f7(a5,a5),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[428,455,592,2,3])).
% 63.56/63.72 cnf(595,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[594,2])).
% 63.56/63.72 cnf(596,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[365,374,594,2,3])).
% 63.56/63.72 cnf(598,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[596,2])).
% 63.56/63.72 cnf(599,plain,
% 63.56/63.72 (E(f7(a5,a5),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[379,576,596,2,3])).
% 63.56/63.72 cnf(601,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[599,2])).
% 63.56/63.72 cnf(602,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[404,557,599,2,3])).
% 63.56/63.72 cnf(603,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[602,2])).
% 63.56/63.72 cnf(604,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[449,598,602,2,3])).
% 63.56/63.72 cnf(605,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[604,2])).
% 63.56/63.72 cnf(606,plain,
% 63.56/63.72 (E(f3(a5,f7(a5,x6061)),f7(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[601,551,604,2,3])).
% 63.56/63.72 cnf(607,plain,
% 63.56/63.72 (E(f7(a5,a5),f3(a5,f7(a5,x6071)))),
% 63.56/63.72 inference(scs_inference,[],[606,2])).
% 63.56/63.72 cnf(608,plain,
% 63.56/63.72 (E(f6(a5,f6(a5,a5)),f7(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[603,144,606,2,3])).
% 63.56/63.72 cnf(611,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f3(a5,f7(a5,x6111)))),
% 63.56/63.72 inference(scs_inference,[],[595,607,608,2,3])).
% 63.56/63.72 cnf(612,plain,
% 63.56/63.72 (E(f3(a5,f7(a5,x6121)),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[611,2])).
% 63.56/63.72 cnf(613,plain,
% 63.56/63.72 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f6(a5,f8(x6131)),f3(x6131,x6131)))),
% 63.56/63.72 inference(scs_inference,[],[593,497,611,2,3])).
% 63.56/63.72 cnf(615,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f6(a5,f8(x6151)),f3(x6151,x6151)))),
% 63.56/63.72 inference(scs_inference,[],[605,507,613,2,3])).
% 63.56/63.72 cnf(617,plain,
% 63.56/63.72 (E(f6(f8(x6171),x6171),f6(f6(a5,f8(x6172)),f3(x6172,x6172)))),
% 63.56/63.72 inference(scs_inference,[],[265,510,615,2,3])).
% 63.56/63.72 cnf(619,plain,
% 63.56/63.72 (E(f7(f6(a5,a5),f6(a5,a5)),a5)),
% 63.56/63.72 inference(scs_inference,[],[384,564,617,2,3])).
% 63.56/63.72 cnf(622,plain,
% 63.56/63.72 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[392,576,619,2,3])).
% 63.56/63.72 cnf(624,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f3(f6(a5,a5),f6(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[622,2])).
% 63.56/63.72 cnf(625,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f6(f6(a5,f8(x6251)),f3(x6251,x6251)))),
% 63.56/63.72 inference(scs_inference,[],[573,548,622,2,3])).
% 63.56/63.72 cnf(627,plain,
% 63.56/63.72 (E(f3(a5,a5),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[413,576,625,2,3])).
% 63.56/63.72 cnf(630,plain,
% 63.56/63.72 (E(f6(a5,a5),f7(a5,f3(a5,x6301)))),
% 63.56/63.72 inference(scs_inference,[],[545,356,627,2,3])).
% 63.56/63.72 cnf(632,plain,
% 63.56/63.72 (E(f7(a5,f3(a5,x6321)),f6(a5,a5))),
% 63.56/63.72 inference(scs_inference,[],[630,2])).
% 63.56/63.72 cnf(633,plain,
% 63.56/63.72 (E(f6(f6(a5,f8(x6331)),f3(x6331,x6331)),f7(a5,f3(a5,x6332)))),
% 63.56/63.72 inference(scs_inference,[],[578,356,630,2,3])).
% 63.56/63.72 cnf(636,plain,
% 63.56/63.72 (E(f7(a5,f3(a5,x6361)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[632,533,633,2,3])).
% 63.56/63.72 cnf(638,plain,
% 63.56/63.72 (E(f3(a5,a5),f3(f7(a5,x6381),a5))),
% 63.56/63.72 inference(scs_inference,[],[585,441,636,2,3])).
% 63.56/63.72 cnf(640,plain,
% 63.56/63.72 (E(f6(f6(a5,a5),a5),f7(f7(a5,a5),f7(a5,a5)))),
% 63.56/63.72 inference(scs_inference,[],[624,638,604,2,3])).
% 63.56/63.72 cnf(641,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f6(a5,a5),a5))),
% 63.56/63.72 inference(scs_inference,[],[640,2])).
% 63.56/63.72 cnf(642,plain,
% 63.56/63.72 (E(f3(f7(a5,x6421),a5),f6(f6(a5,f8(x6422)),f3(x6422,x6422)))),
% 63.56/63.72 inference(scs_inference,[],[443,507,640,2,3])).
% 63.56/63.72 cnf(644,plain,
% 63.56/63.72 (E(f3(a5,f7(a5,x6441)),f6(f6(a5,f8(x6442)),f3(x6442,x6442)))),
% 63.56/63.72 inference(scs_inference,[],[612,507,642,2,3])).
% 63.56/63.72 cnf(646,plain,
% 63.56/63.72 (E(f7(f7(a5,a5),f7(a5,a5)),a5)),
% 63.56/63.72 inference(scs_inference,[],[641,548,644,2,3])).
% 63.56/63.72 cnf(1177,plain,
% 63.56/63.72 (E(f6(a1,x11771),f6(f3(a1,a2),x11771))),
% 63.56/63.72 inference(scs_inference,[],[147,10,4,7,8,9,5,6])).
% 63.56/63.72 cnf(1178,plain,
% 63.56/63.72 (~E(f6(a1,a4),f3(f6(a1,a4),f6(a2,a4)))),
% 63.56/63.72 inference(scs_inference,[],[27,147,10,4,7,8,9,5,6,2])).
% 63.56/63.72 cnf(1339,plain,
% 63.56/63.72 ($false),
% 63.56/63.72 inference(scs_inference,[],[1178,65,646,1177,53,10,7,9,6,8,4,5,2,3]),
% 63.56/63.72 ['proof']).
% 63.56/63.72 % SZS output end Proof
% 63.56/63.72 % Total time :63.130000s
%------------------------------------------------------------------------------