%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP158-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:39:03 EDT 2024
% Result : Unsatisfiable 178.96s 178.93s
% Output : CNFRefutation 178.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP158-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 07:38:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 178.87/178.92 %-------------------------------------------
% 178.87/178.92 % File :CSE---1.7
% 178.87/178.92 % Problem :theBenchmark
% 178.87/178.92 % Transform :cnf
% 178.87/178.92 % Format :tptp:raw
% 178.87/178.92 % Command :java -jar mcs_scs.jar %d %s
% 178.87/178.92
% 178.87/178.92 % Result :Theorem 178.320000s
% 178.87/178.92 % Output :CNFRefutation 178.320000s
% 178.87/178.92 %-------------------------------------------
% 178.96/178.93 %--------------------------------------------------------------------------
% 178.96/178.93 % File : GRP158-1 : TPTP v8.2.0. Bugfixed v1.2.1.
% 178.96/178.93 % Domain : Group Theory (Lattice Ordered)
% 178.96/178.93 % Problem : Prove monotonicity axiom using the GLB transformation
% 178.96/178.93 % Version : [Fuc94] (equality) axioms.
% 178.96/178.93 % English : This problem proves the original monotonicity axiom from the
% 178.96/178.93 % equational axiomatization.
% 178.96/178.93
% 178.96/178.93 % Refs : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri
% 178.96/178.93 % : [Sch95] Schulz (1995), Explanation Based Learning for Distribu
% 178.96/178.93 % Source : [Sch95]
% 178.96/178.93 % Names : ax_mono2b [Sch95]
% 178.96/178.93
% 178.96/178.93 % Status : Unsatisfiable
% 178.96/178.93 % 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 v2.0.0
% 178.96/178.93 % Syntax : Number of clauses : 17 ( 17 unt; 0 nHn; 2 RR)
% 178.96/178.93 % Number of literals : 17 ( 17 equ; 1 neg)
% 178.96/178.93 % Maximal clause size : 1 ( 1 avg)
% 178.96/178.93 % Maximal term depth : 3 ( 2 avg)
% 178.96/178.93 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 178.96/178.93 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 178.96/178.93 % Number of variables : 33 ( 2 sgn)
% 178.96/178.93 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 178.96/178.93
% 178.96/178.93 % Comments : ORDERING LPO inverse > product > greatest_lower_bound >
% 178.96/178.93 % least_upper_bound > identity > a > b > c
% 178.96/178.93 % Bugfixes : v1.2.1 - Duplicate axioms in GRP004-2.ax removed.
% 178.96/178.93 %--------------------------------------------------------------------------
% 178.96/178.93 %----Include equality group theory axioms
% 178.96/178.93 include('Axioms/GRP004-0.ax').
% 178.96/178.93 %----Include Lattice ordered group (equality) axioms
% 178.96/178.93 include('Axioms/GRP004-2.ax').
% 178.96/178.93 %--------------------------------------------------------------------------
% 178.96/178.93 cnf(ax_mono2b_1,hypothesis,
% 178.96/178.93 greatest_lower_bound(a,b) = a ).
% 178.96/178.93
% 178.96/178.93 cnf(prove_ax_mono2b,negated_conjecture,
% 178.96/178.93 greatest_lower_bound(multiply(c,a),multiply(c,b)) != multiply(c,a) ).
% 178.96/178.93
% 178.96/178.93 %--------------------------------------------------------------------------
% 178.96/178.93 %-------------------------------------------
% 178.96/178.93 % Proof found
% 178.96/178.93 % SZS status Theorem for theBenchmark
% 178.96/178.93 % SZS output start Proof
% 178.96/178.94 %ClaNum:27(EqnAxiom:10)
% 178.96/178.94 %VarNum:72(SingletonVarNum:33)
% 178.96/178.94 %MaxLitNum:1
% 178.96/178.94 %MaxfuncDepth:2
% 178.96/178.94 %SharedTerms:10
% 178.96/178.94 %goalClause: 27
% 178.96/178.94 %singleGoalClaCount:1
% 178.96/178.94 [11]E(f3(a1,a2),a1)
% 178.96/178.94 [27]~E(f3(f6(a4,a1),f6(a4,a2)),f6(a4,a1))
% 178.96/178.94 [12]E(f6(a5,x121),x121)
% 178.96/178.94 [13]E(f3(x131,x131),x131)
% 178.96/178.94 [14]E(f7(x141,x141),x141)
% 178.96/178.94 [15]E(f6(f8(x151),x151),a5)
% 178.96/178.94 [16]E(f3(x161,x162),f3(x162,x161))
% 178.96/178.94 [17]E(f7(x171,x172),f7(x172,x171))
% 178.96/178.94 [18]E(f3(x181,f7(x181,x182)),x181)
% 178.96/178.94 [19]E(f7(x191,f3(x191,x192)),x191)
% 178.96/178.94 [20]E(f3(f3(x201,x202),x203),f3(x201,f3(x202,x203)))
% 178.96/178.94 [21]E(f7(f7(x211,x212),x213),f7(x211,f7(x212,x213)))
% 178.96/178.94 [22]E(f6(f6(x221,x222),x223),f6(x221,f6(x222,x223)))
% 178.96/178.94 [23]E(f3(f6(x231,x232),f6(x231,x233)),f6(x231,f3(x232,x233)))
% 178.96/178.94 [24]E(f7(f6(x241,x242),f6(x241,x243)),f6(x241,f7(x242,x243)))
% 178.96/178.94 [25]E(f3(f6(x251,x252),f6(x253,x252)),f6(f3(x251,x253),x252))
% 178.96/178.94 [26]E(f7(f6(x261,x262),f6(x263,x262)),f6(f7(x261,x263),x262))
% 178.96/178.94 %EqnAxiom
% 178.96/178.94 [1]E(x11,x11)
% 178.96/178.94 [2]E(x22,x21)+~E(x21,x22)
% 178.96/178.94 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 178.96/178.94 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 178.96/178.94 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 178.96/178.94 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 178.96/178.94 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 178.96/178.94 [8]~E(x81,x82)+E(f7(x81,x83),f7(x82,x83))
% 178.96/178.94 [9]~E(x91,x92)+E(f7(x93,x91),f7(x93,x92))
% 178.96/178.94 [10]~E(x101,x102)+E(f8(x101),f8(x102))
% 178.96/178.94
% 178.96/178.94 %-------------------------------------------
% 178.96/178.95 cnf(28,plain,
% 178.96/178.95 (E(x281,f3(x281,x281))),
% 178.96/178.95 inference(scs_inference,[],[13,2])).
% 178.96/178.95 cnf(31,plain,
% 178.96/178.95 (~E(f6(a4,a2),f6(a4,a1))),
% 178.96/178.95 inference(scs_inference,[],[27,13,2,3,5])).
% 178.96/178.95 cnf(32,plain,
% 178.96/178.95 (~E(a2,a1)),
% 178.96/178.95 inference(scs_inference,[],[27,13,2,3,5,7])).
% 178.96/178.95 cnf(33,plain,
% 178.96/178.95 (E(x331,f7(x331,x331))),
% 178.96/178.95 inference(scs_inference,[],[14,2])).
% 178.96/178.95 cnf(36,plain,
% 178.96/178.95 (E(x361,f6(a5,x361))),
% 178.96/178.95 inference(scs_inference,[],[12,2])).
% 178.96/178.95 cnf(39,plain,
% 178.96/178.95 (E(f6(x391,f3(x392,x393)),f3(f6(x391,x392),f6(x391,x393)))),
% 178.96/178.95 inference(scs_inference,[],[23,2])).
% 178.96/178.95 cnf(40,plain,
% 178.96/178.95 (E(f6(x401,x402),f6(x401,f3(x402,x402)))),
% 178.96/178.95 inference(scs_inference,[],[28,23,2,3])).
% 178.96/178.95 cnf(43,plain,
% 178.96/178.95 (E(f6(x431,f3(x432,x432)),f6(x431,x432))),
% 178.96/178.95 inference(scs_inference,[],[40,2])).
% 178.96/178.95 cnf(46,plain,
% 178.96/178.95 (E(f6(x461,f7(x462,x463)),f7(f6(x461,x462),f6(x461,x463)))),
% 178.96/178.95 inference(scs_inference,[],[24,2])).
% 178.96/178.95 cnf(47,plain,
% 178.96/178.95 (E(f6(x471,x472),f6(x471,f7(x472,x472)))),
% 178.96/178.95 inference(scs_inference,[],[33,24,2,3])).
% 178.96/178.95 cnf(50,plain,
% 178.96/178.95 (E(f6(x501,f7(x502,x502)),f6(x501,x502))),
% 178.96/178.95 inference(scs_inference,[],[47,2])).
% 178.96/178.95 cnf(54,plain,
% 178.96/178.95 (E(f6(x541,x542),f6(f3(x541,x541),x542))),
% 178.96/178.95 inference(scs_inference,[],[28,25,2,3])).
% 178.96/178.95 cnf(57,plain,
% 178.96/178.95 (E(f6(f3(x571,x571),x572),f6(x571,x572))),
% 178.96/178.95 inference(scs_inference,[],[54,2])).
% 178.96/178.95 cnf(61,plain,
% 178.96/178.95 (E(f6(x611,x612),f6(f7(x611,x611),x612))),
% 178.96/178.95 inference(scs_inference,[],[33,26,2,3])).
% 178.96/178.95 cnf(64,plain,
% 178.96/178.95 (E(f6(f7(x641,x641),x642),f6(x641,x642))),
% 178.96/178.95 inference(scs_inference,[],[61,2])).
% 178.96/178.95 cnf(67,plain,
% 178.96/178.95 (E(x671,f3(x671,f7(x671,x672)))),
% 178.96/178.95 inference(scs_inference,[],[18,2])).
% 178.96/178.95 cnf(68,plain,
% 178.96/178.95 (E(f3(x681,x682),f3(x681,f3(x682,f3(x681,x682))))),
% 178.96/178.95 inference(scs_inference,[],[28,18,20,2,3])).
% 178.96/178.95 cnf(71,plain,
% 178.96/178.95 (E(f3(x711,f3(x712,f3(x711,x712))),f3(x711,x712))),
% 178.96/178.95 inference(scs_inference,[],[68,2])).
% 178.96/178.95 cnf(72,plain,
% 178.96/178.95 (E(f7(x721,x722),f7(x721,f7(x722,f7(x721,x722))))),
% 178.96/178.95 inference(scs_inference,[],[33,68,21,2,3])).
% 178.96/178.95 cnf(75,plain,
% 178.96/178.95 (E(f7(x751,f7(x752,f7(x751,x752))),f7(x751,x752))),
% 178.96/178.95 inference(scs_inference,[],[72,2])).
% 178.96/178.95 cnf(78,plain,
% 178.96/178.95 (E(x781,f7(x781,f3(x781,x782)))),
% 178.96/178.95 inference(scs_inference,[],[19,2])).
% 178.96/178.95 cnf(79,plain,
% 178.96/178.95 (~E(a2,f3(a1,a2))),
% 178.96/178.95 inference(scs_inference,[],[32,19,11,2,3])).
% 178.96/178.95 cnf(80,plain,
% 178.96/178.95 (E(a5,f6(f8(x801),x801))),
% 178.96/178.95 inference(scs_inference,[],[15,2])).
% 178.96/178.95 cnf(81,plain,
% 178.96/178.95 (~E(a2,f3(a1,f3(a2,f3(a1,a2))))),
% 178.96/178.95 inference(scs_inference,[],[71,79,15,2,3])).
% 178.96/178.95 cnf(83,plain,
% 178.96/178.95 (E(f3(x831,f3(x832,x833)),f3(f3(x831,x832),x833))),
% 178.96/178.95 inference(scs_inference,[],[20,2])).
% 178.96/178.95 cnf(84,plain,
% 178.96/178.95 (E(f3(a5,f7(a5,x841)),f6(f8(x842),x842))),
% 178.96/178.95 inference(scs_inference,[],[80,18,20,2,3])).
% 178.96/178.95 cnf(86,plain,
% 178.96/178.95 (E(f6(f8(x861),x861),f3(a5,f7(a5,x862)))),
% 178.96/178.95 inference(scs_inference,[],[84,2])).
% 178.96/178.95 cnf(87,plain,
% 178.96/178.95 (E(f7(a5,f3(a5,x871)),f6(f8(x872),x872))),
% 178.96/178.95 inference(scs_inference,[],[80,84,19,2,3])).
% 178.96/178.95 cnf(89,plain,
% 178.96/178.95 (E(f6(f8(x891),x891),f7(a5,f3(a5,x892)))),
% 178.96/178.95 inference(scs_inference,[],[87,2])).
% 178.96/178.95 cnf(90,plain,
% 178.96/178.95 (E(f6(f8(x901),f3(x901,x901)),f3(a5,f7(a5,x902)))),
% 178.96/178.95 inference(scs_inference,[],[43,86,87,2,3])).
% 178.96/178.95 cnf(93,plain,
% 178.96/178.95 (E(f3(a5,f7(a5,x931)),f6(f8(x932),f3(x932,x932)))),
% 178.96/178.95 inference(scs_inference,[],[90,2])).
% 178.96/178.95 cnf(94,plain,
% 178.96/178.95 (E(f6(f8(x941),f7(x941,x941)),f7(a5,f3(a5,x942)))),
% 178.96/178.95 inference(scs_inference,[],[50,89,90,2,3])).
% 178.96/178.95 cnf(97,plain,
% 178.96/178.95 (E(f7(a5,f3(a5,x971)),f6(f8(x972),f7(x972,x972)))),
% 178.96/178.95 inference(scs_inference,[],[94,2])).
% 178.96/178.95 cnf(98,plain,
% 178.96/178.95 (E(a5,f6(f8(x981),f3(x981,x981)))),
% 178.96/178.95 inference(scs_inference,[],[67,93,94,2,3])).
% 178.96/178.95 cnf(101,plain,
% 178.96/178.95 (E(f6(f8(x1011),f3(x1011,x1011)),a5)),
% 178.96/178.95 inference(scs_inference,[],[98,2])).
% 178.96/178.95 cnf(103,plain,
% 178.96/178.95 (E(f7(x1031,f7(x1032,x1033)),f7(f7(x1031,x1032),x1033))),
% 178.96/178.95 inference(scs_inference,[],[21,2])).
% 178.96/178.95 cnf(104,plain,
% 178.96/178.95 (E(f6(f3(f8(x1041),f8(x1041)),f3(x1041,x1041)),a5)),
% 178.96/178.95 inference(scs_inference,[],[57,101,21,2,3])).
% 178.96/178.95 cnf(106,plain,
% 178.96/178.95 (E(a5,f6(f3(f8(x1061),f8(x1061)),f3(x1061,x1061)))),
% 178.96/178.95 inference(scs_inference,[],[104,2])).
% 178.96/178.95 cnf(107,plain,
% 178.96/178.95 (E(f6(f7(f8(x1071),f8(x1071)),f3(x1071,x1071)),a5)),
% 178.96/178.95 inference(scs_inference,[],[64,101,104,2,3])).
% 178.96/178.95 cnf(109,plain,
% 178.96/178.95 (E(a5,f6(f7(f8(x1091),f8(x1091)),f3(x1091,x1091)))),
% 178.96/178.95 inference(scs_inference,[],[107,2])).
% 178.96/178.95 cnf(110,plain,
% 178.96/178.95 (E(f6(f8(x1101),f3(x1101,x1101)),f6(f3(f8(x1102),f8(x1102)),f3(x1102,x1102)))),
% 178.96/178.95 inference(scs_inference,[],[106,101,107,2,3])).
% 178.96/178.95 cnf(111,plain,
% 178.96/178.95 (E(f6(f3(f8(x1111),f8(x1111)),f3(x1111,x1111)),f6(f8(x1112),f3(x1112,x1112)))),
% 178.96/178.95 inference(scs_inference,[],[110,2])).
% 178.96/178.95 cnf(112,plain,
% 178.96/178.95 (E(f6(f8(x1121),f3(x1121,x1121)),f6(f7(f8(x1122),f8(x1122)),f3(x1122,x1122)))),
% 178.96/178.95 inference(scs_inference,[],[109,101,110,2,3])).
% 178.96/178.95 cnf(113,plain,
% 178.96/178.95 (E(f6(f7(f8(x1131),f8(x1131)),f3(x1131,x1131)),f6(f8(x1132),f3(x1132,x1132)))),
% 178.96/178.95 inference(scs_inference,[],[112,2])).
% 178.96/178.95 cnf(114,plain,
% 178.96/178.95 (E(f6(f8(x1141),f3(x1141,x1141)),f7(a5,f3(a5,x1142)))),
% 178.96/178.95 inference(scs_inference,[],[43,89,112,2,3])).
% 178.96/178.95 cnf(117,plain,
% 178.96/178.95 (E(f7(a5,f3(a5,x1171)),f6(f8(x1172),f3(x1172,x1172)))),
% 178.96/178.95 inference(scs_inference,[],[114,2])).
% 178.96/178.95 cnf(118,plain,
% 178.96/178.95 (E(f6(f8(x1181),f7(x1181,x1181)),f3(a5,f7(a5,x1182)))),
% 178.96/178.95 inference(scs_inference,[],[50,86,114,2,3])).
% 178.96/178.95 cnf(121,plain,
% 178.96/178.95 (E(f3(a5,f7(a5,x1211)),f6(f8(x1212),f7(x1212,x1212)))),
% 178.96/178.95 inference(scs_inference,[],[118,2])).
% 178.96/178.95 cnf(122,plain,
% 178.96/178.95 (E(f6(f8(x1221),f3(x1221,x1221)),f6(f8(x1222),x1222))),
% 178.96/178.95 inference(scs_inference,[],[80,101,118,2,3])).
% 178.96/178.95 cnf(123,plain,
% 178.96/178.95 (E(f6(f8(x1231),x1231),f6(f8(x1232),f3(x1232,x1232)))),
% 178.96/178.95 inference(scs_inference,[],[122,2])).
% 178.96/178.95 cnf(124,plain,
% 178.96/178.95 (E(f6(f3(f8(x1241),f8(x1241)),f3(x1241,x1241)),f6(f8(x1242),x1242))),
% 178.96/178.95 inference(scs_inference,[],[111,122,2,3])).
% 178.96/178.95 cnf(126,plain,
% 178.96/178.95 (E(f6(f8(x1261),x1261),f6(f3(f8(x1262),f8(x1262)),f3(x1262,x1262)))),
% 178.96/178.95 inference(scs_inference,[],[124,2])).
% 178.96/178.95 cnf(127,plain,
% 178.96/178.95 (E(f6(f7(f8(x1271),f8(x1271)),f3(x1271,x1271)),f3(a5,f7(a5,x1272)))),
% 178.96/178.95 inference(scs_inference,[],[113,124,90,2,3])).
% 178.96/178.95 cnf(129,plain,
% 178.96/178.95 (E(f3(a5,f7(a5,x1291)),f6(f7(f8(x1292),f8(x1292)),f3(x1292,x1292)))),
% 178.96/178.95 inference(scs_inference,[],[127,2])).
% 178.96/178.95 cnf(130,plain,
% 178.96/178.95 (E(f6(f8(x1301),x1301),f6(f7(f8(x1302),f8(x1302)),f3(x1302,x1302)))),
% 178.96/178.95 inference(scs_inference,[],[123,127,112,2,3])).
% 178.96/178.95 cnf(132,plain,
% 178.96/178.95 (E(f6(f7(f8(x1321),f8(x1321)),f3(x1321,x1321)),f6(f8(x1322),x1322))),
% 178.96/178.95 inference(scs_inference,[],[130,2])).
% 178.96/178.95 cnf(133,plain,
% 178.96/178.95 (E(f7(a5,f3(a5,x1331)),f6(f3(f8(x1332),f8(x1332)),f3(x1332,x1332)))),
% 178.96/178.95 inference(scs_inference,[],[117,130,110,2,3])).
% 178.96/178.95 cnf(136,plain,
% 178.96/178.95 (E(f6(f7(f8(x1361),f8(x1361)),f3(x1361,x1361)),f7(a5,f3(a5,x1362)))),
% 178.96/178.95 inference(scs_inference,[],[132,89,133,2,3])).
% 178.96/178.95 cnf(139,plain,
% 178.96/178.95 (E(f3(a5,f7(a5,x1391)),f7(a5,f3(a5,x1392)))),
% 178.96/178.95 inference(scs_inference,[],[129,136,2,3])).
% 178.96/178.95 cnf(141,plain,
% 178.96/178.95 (E(f7(a5,f3(a5,x1411)),f3(a5,f7(a5,x1412)))),
% 178.96/178.95 inference(scs_inference,[],[139,2])).
% 178.96/178.95 cnf(144,plain,
% 178.96/178.95 (E(f6(x1441,f6(x1442,x1443)),f6(f6(x1441,x1442),x1443))),
% 178.96/178.95 inference(scs_inference,[],[22,2])).
% 178.96/178.95 cnf(147,plain,
% 178.96/178.95 (E(a1,f3(a1,a2))),
% 178.96/178.96 inference(scs_inference,[],[11,2])).
% 178.96/178.96 cnf(151,plain,
% 178.96/178.96 (E(f3(a5,f7(a5,x1511)),f6(f3(f8(x1512),f8(x1512)),f3(x1512,x1512)))),
% 178.96/178.96 inference(scs_inference,[],[57,90,3,2])).
% 178.96/178.96 cnf(154,plain,
% 178.96/178.96 (E(f7(a5,f3(a5,x1541)),f6(f7(f8(x1542),f8(x1542)),f7(x1542,x1542)))),
% 178.96/178.96 inference(scs_inference,[],[64,94,3,2])).
% 178.96/178.96 cnf(155,plain,
% 178.96/178.96 (~E(a2,f3(f3(a2,f3(a1,a2)),a1))),
% 178.96/178.96 inference(scs_inference,[],[81,16,3])).
% 178.96/178.96 cnf(157,plain,
% 178.96/178.96 (~E(a2,f3(a2,f3(f3(a1,a2),a1)))),
% 178.96/178.96 inference(scs_inference,[],[83,155,3])).
% 178.96/178.96 cnf(159,plain,
% 178.96/178.96 (~E(a2,f3(f3(f3(a1,a2),a1),a2))),
% 178.96/178.96 inference(scs_inference,[],[157,16,3])).
% 178.96/178.96 cnf(161,plain,
% 178.96/178.96 (~E(a2,f3(f3(a1,a2),f3(a1,a2)))),
% 178.96/178.96 inference(scs_inference,[],[83,159,3])).
% 178.96/178.96 cnf(163,plain,
% 178.96/178.96 (E(f3(a1,a2),f7(a1,f3(a1,x1631)))),
% 178.96/178.96 inference(scs_inference,[],[11,78,3])).
% 178.96/178.96 cnf(173,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f3(f8(x1731),f8(x1731)),f3(x1731,x1731)))),
% 178.96/178.96 inference(scs_inference,[],[12,106,3])).
% 178.96/178.96 cnf(175,plain,
% 178.96/178.96 (E(f6(f3(f8(x1751),f8(x1751)),f3(x1751,x1751)),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,106,3,2])).
% 178.96/178.96 cnf(176,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f7(f8(x1761),f8(x1761)),f3(x1761,x1761)))),
% 178.96/178.96 inference(scs_inference,[],[12,109,3])).
% 178.96/178.96 cnf(178,plain,
% 178.96/178.96 (E(f6(f7(f8(x1781),f8(x1781)),f3(x1781,x1781)),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,109,3,2])).
% 178.96/178.96 cnf(179,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f8(x1791),x1791))),
% 178.96/178.96 inference(scs_inference,[],[12,80,3])).
% 178.96/178.96 cnf(181,plain,
% 178.96/178.96 (E(f6(f8(x1811),x1811),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,80,3,2])).
% 178.96/178.96 cnf(182,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x1821),x1821)),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,181,3])).
% 178.96/178.96 cnf(185,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x1851),f3(x1851,x1851))),a5)),
% 178.96/178.96 inference(scs_inference,[],[12,101,3])).
% 178.96/178.96 cnf(187,plain,
% 178.96/178.96 (E(a5,f6(a5,f6(f8(x1871),f3(x1871,x1871))))),
% 178.96/178.96 inference(scs_inference,[],[12,101,3,2])).
% 178.96/178.96 cnf(190,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x1901),f3(x1901,x1901))),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,187,3,2])).
% 178.96/178.96 cnf(197,plain,
% 178.96/178.96 (E(f6(a5,f6(a5,a5)),f6(f3(f8(x1971),f8(x1971)),f3(x1971,x1971)))),
% 178.96/178.96 inference(scs_inference,[],[12,173,3])).
% 178.96/178.96 cnf(199,plain,
% 178.96/178.96 (E(f6(f3(f8(x1991),f8(x1991)),f3(x1991,x1991)),f6(a5,f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[12,173,3,2])).
% 178.96/178.96 cnf(200,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f8(x2001),f3(x2001,x2001)))),
% 178.96/178.96 inference(scs_inference,[],[12,98,3])).
% 178.96/178.96 cnf(202,plain,
% 178.96/178.96 (E(f6(f8(x2021),f3(x2021,x2021)),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[12,98,3,2])).
% 178.96/178.96 cnf(203,plain,
% 178.96/178.96 (E(f6(a5,f6(a5,a5)),f6(f8(x2031),f3(x2031,x2031)))),
% 178.96/178.96 inference(scs_inference,[],[12,200,3])).
% 178.96/178.96 cnf(205,plain,
% 178.96/178.96 (E(f6(f8(x2051),f3(x2051,x2051)),f6(a5,f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[12,200,3,2])).
% 178.96/178.96 cnf(206,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x2061),x2061)),a5)),
% 178.96/178.96 inference(scs_inference,[],[12,15,3])).
% 178.96/178.96 cnf(208,plain,
% 178.96/178.96 (E(a5,f6(a5,f6(f8(x2081),x2081)))),
% 178.96/178.96 inference(scs_inference,[],[12,15,3,2])).
% 178.96/178.96 cnf(211,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x2111),x2111)),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[13,208,3,2])).
% 178.96/178.96 cnf(214,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x2141),f3(x2141,x2141))),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[13,187,3,2])).
% 178.96/178.96 cnf(215,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f3(f8(x2151),f8(x2151)),f3(x2151,x2151)))),
% 178.96/178.96 inference(scs_inference,[],[13,106,3])).
% 178.96/178.96 cnf(218,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f7(f8(x2181),f8(x2181)),f3(x2181,x2181)))),
% 178.96/178.96 inference(scs_inference,[],[13,109,3])).
% 178.96/178.96 cnf(220,plain,
% 178.96/178.96 (E(f6(f7(f8(x2201),f8(x2201)),f3(x2201,x2201)),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[13,109,3,2])).
% 178.96/178.96 cnf(221,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f8(x2211),x2211))),
% 178.96/178.96 inference(scs_inference,[],[13,80,3])).
% 178.96/178.96 cnf(223,plain,
% 178.96/178.96 (E(f6(f8(x2231),x2231),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[13,80,3,2])).
% 178.96/178.96 cnf(226,plain,
% 178.96/178.96 (E(f6(f8(x2261),x2261),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,221,3,2])).
% 178.96/178.96 cnf(229,plain,
% 178.96/178.96 (E(f6(f7(f8(x2291),f8(x2291)),f3(x2291,x2291)),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,218,3,2])).
% 178.96/178.96 cnf(232,plain,
% 178.96/178.96 (E(f6(f3(f8(x2321),f8(x2321)),f3(x2321,x2321)),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,215,3,2])).
% 178.96/178.96 cnf(235,plain,
% 178.96/178.96 (E(f6(f8(x2351),f3(x2351,x2351)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,200,3,2])).
% 178.96/178.96 cnf(238,plain,
% 178.96/178.96 (E(f6(f8(x2381),x2381),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,179,3,2])).
% 178.96/178.96 cnf(244,plain,
% 178.96/178.96 (E(f6(f3(f8(x2441),f8(x2441)),f3(x2441,x2441)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,173,3,2])).
% 178.96/178.96 cnf(245,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f8(x2451),f3(x2451,x2451)))),
% 178.96/178.96 inference(scs_inference,[],[13,98,3])).
% 178.96/178.96 cnf(250,plain,
% 178.96/178.96 (E(f6(f8(x2501),f3(x2501,x2501)),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[13,245,3,2])).
% 178.96/178.96 cnf(253,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x2531),x2531)),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[14,208,3,2])).
% 178.96/178.96 cnf(256,plain,
% 178.96/178.96 (E(f6(a5,f6(f8(x2561),f3(x2561,x2561))),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[14,187,3,2])).
% 178.96/178.96 cnf(260,plain,
% 178.96/178.96 (E(f7(a5,a5),f6(f7(f8(x2601),f8(x2601)),f3(x2601,x2601)))),
% 178.96/178.96 inference(scs_inference,[],[14,109,3])).
% 178.96/178.96 cnf(262,plain,
% 178.96/178.96 (E(f6(f7(f8(x2621),f8(x2621)),f3(x2621,x2621)),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[14,109,3,2])).
% 178.96/178.96 cnf(265,plain,
% 178.96/178.96 (E(f6(f8(x2651),x2651),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[14,80,3,2])).
% 178.96/178.96 cnf(271,plain,
% 178.96/178.96 (E(f6(f7(f8(x2711),f8(x2711)),f3(x2711,x2711)),f7(f7(a5,a5),f7(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,260,3,2])).
% 178.96/178.96 cnf(277,plain,
% 178.96/178.96 (E(f6(f8(x2771),f3(x2771,x2771)),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,245,3,2])).
% 178.96/178.96 cnf(280,plain,
% 178.96/178.96 (E(f6(f8(x2801),x2801),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,221,3,2])).
% 178.96/178.96 cnf(283,plain,
% 178.96/178.96 (E(f6(f7(f8(x2831),f8(x2831)),f3(x2831,x2831)),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,218,3,2])).
% 178.96/178.96 cnf(295,plain,
% 178.96/178.96 (E(f6(f7(f8(x2951),f8(x2951)),f3(x2951,x2951)),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,176,3,2])).
% 178.96/178.96 cnf(298,plain,
% 178.96/178.96 (E(f6(f3(f8(x2981),f8(x2981)),f3(x2981,x2981)),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[14,173,3,2])).
% 178.96/178.96 cnf(301,plain,
% 178.96/178.96 (E(f6(f8(x3011),f3(x3011,x3011)),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[14,98,3,2])).
% 178.96/178.96 cnf(308,plain,
% 178.96/178.96 (E(f3(a5,f7(a5,x3081)),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[295,129,3])).
% 178.96/178.96 cnf(310,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f3(a5,f7(a5,x3101)))),
% 178.96/178.96 inference(scs_inference,[],[295,129,3,2])).
% 178.96/178.96 cnf(316,plain,
% 178.96/178.96 (E(f6(f8(x3161),f7(x3161,x3161)),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[310,121,3,2])).
% 178.96/178.96 cnf(322,plain,
% 178.96/178.96 (E(f6(f3(f8(x3221),f8(x3221)),f3(x3221,x3221)),f3(f7(a5,x3222),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,151,3,2])).
% 178.96/178.96 cnf(325,plain,
% 178.96/178.96 (E(f3(f7(a5,x3251),a5),f6(f8(x3252),x3252))),
% 178.96/178.96 inference(scs_inference,[],[126,322,3,2])).
% 178.96/178.96 cnf(326,plain,
% 178.96/178.96 (E(f3(f7(a5,x3261),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[280,325,3])).
% 178.96/178.96 cnf(328,plain,
% 178.96/178.96 (E(f7(f3(a5,a5),f3(a5,a5)),f3(f7(a5,x3281),a5))),
% 178.96/178.96 inference(scs_inference,[],[280,325,3,2])).
% 178.96/178.96 cnf(331,plain,
% 178.96/178.96 (E(f6(f8(x3311),f3(x3311,x3311)),f3(f7(a5,x3312),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,93,3,2])).
% 178.96/178.96 cnf(334,plain,
% 178.96/178.96 (E(f6(f7(f8(x3341),f8(x3341)),f3(x3341,x3341)),f3(f7(a5,x3342),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,129,3,2])).
% 178.96/178.96 cnf(335,plain,
% 178.96/178.96 (E(f3(f7(a5,x3351),a5),f6(f8(x3352),f7(x3352,x3352)))),
% 178.96/178.96 inference(scs_inference,[],[16,121,3])).
% 178.96/178.96 cnf(337,plain,
% 178.96/178.96 (E(f6(f8(x3371),f7(x3371,x3371)),f3(f7(a5,x3372),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,121,3,2])).
% 178.96/178.96 cnf(340,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f3(f7(a5,x3401),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,308,3,2])).
% 178.96/178.96 cnf(343,plain,
% 178.96/178.96 (E(f7(f3(a5,a5),f3(a5,a5)),f3(a5,f7(a5,x3431)))),
% 178.96/178.96 inference(scs_inference,[],[16,326,3,2])).
% 178.96/178.96 cnf(346,plain,
% 178.96/178.96 (E(f7(a5,f3(a5,x3461)),f3(f7(a5,x3462),a5))),
% 178.96/178.96 inference(scs_inference,[],[16,139,3,2])).
% 178.96/178.96 cnf(350,plain,
% 178.96/178.96 (E(f7(f7(x3501,x3502),x3503),f7(f7(x3502,x3503),x3501))),
% 178.96/178.96 inference(scs_inference,[],[17,103,3,2])).
% 178.96/178.96 cnf(353,plain,
% 178.96/178.96 (E(f6(f7(f8(x3531),f8(x3531)),f7(x3531,x3531)),f7(f3(a5,x3532),a5))),
% 178.96/178.96 inference(scs_inference,[],[17,154,3,2])).
% 178.96/178.96 cnf(356,plain,
% 178.96/178.96 (E(f7(f3(a5,x3561),a5),f7(a5,f3(a5,x3562)))),
% 178.96/178.96 inference(scs_inference,[],[353,154,3,2])).
% 178.96/178.96 cnf(359,plain,
% 178.96/178.96 (E(f3(a5,f7(a5,x3591)),f7(f3(a5,x3592),a5))),
% 178.96/178.96 inference(scs_inference,[],[17,141,3,2])).
% 178.96/178.96 cnf(362,plain,
% 178.96/178.96 (E(f3(f7(a5,x3621),a5),f7(f3(a5,x3622),a5))),
% 178.96/178.96 inference(scs_inference,[],[17,346,3,2])).
% 178.96/178.96 cnf(365,plain,
% 178.96/178.96 (E(f7(f3(a5,x3651),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[343,359,3,2])).
% 178.96/178.96 cnf(368,plain,
% 178.96/178.96 (E(f7(f3(a5,x3681),a5),f6(f7(f8(x3682),f8(x3682)),f3(x3682,x3682)))),
% 178.96/178.96 inference(scs_inference,[],[334,362,3,2])).
% 178.96/178.96 cnf(371,plain,
% 178.96/178.96 (E(f3(f3(a5,a5),f3(a5,a5)),f7(f3(a5,x3711),a5))),
% 178.96/178.96 inference(scs_inference,[],[229,368,3,2])).
% 178.96/178.96 cnf(374,plain,
% 178.96/178.96 (E(f7(f7(a5,a5),f7(a5,a5)),f7(f3(a5,x3741),a5))),
% 178.96/178.96 inference(scs_inference,[],[271,368,3,2])).
% 178.96/178.96 cnf(376,plain,
% 178.96/178.96 (E(f7(f3(a5,x3761),a5),f6(f8(x3762),f3(x3762,x3762)))),
% 178.96/178.96 inference(scs_inference,[],[250,371,3,2])).
% 178.96/178.96 cnf(379,plain,
% 178.96/178.96 (E(f7(a5,a5),f7(f3(a5,x3791),a5))),
% 178.96/178.96 inference(scs_inference,[],[301,376,3,2])).
% 178.96/178.96 cnf(381,plain,
% 178.96/178.96 (E(f7(f3(a5,x3811),a5),f6(f3(f8(x3812),f8(x3812)),f3(x3812,x3812)))),
% 178.96/178.96 inference(scs_inference,[],[232,371,3,2])).
% 178.96/178.96 cnf(384,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f7(f3(a5,x3841),a5))),
% 178.96/178.96 inference(scs_inference,[],[298,381,3,2])).
% 178.96/178.96 cnf(387,plain,
% 178.96/178.96 (E(f6(f8(x3871),f7(x3871,x3871)),f7(f3(a5,x3872),a5))),
% 178.96/178.96 inference(scs_inference,[],[17,97,3,2])).
% 178.96/178.96 cnf(389,plain,
% 178.96/178.96 (E(f7(f3(a5,x3891),a5),f6(f8(x3892),x3892))),
% 178.96/178.96 inference(scs_inference,[],[226,371,3,2])).
% 178.96/178.96 cnf(392,plain,
% 178.96/178.96 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f3(a5,x3921),a5))),
% 178.96/178.96 inference(scs_inference,[],[238,389,3,2])).
% 178.96/178.96 cnf(396,plain,
% 178.96/178.96 (E(f6(f8(x3961),f3(x3961,x3961)),f6(f8(x3962),f7(x3962,x3962)))),
% 178.96/178.96 inference(scs_inference,[],[331,335,3])).
% 178.96/178.96 cnf(398,plain,
% 178.96/178.96 (E(f6(f8(x3981),f7(x3981,x3981)),f6(f8(x3982),f3(x3982,x3982)))),
% 178.96/178.96 inference(scs_inference,[],[331,335,3,2])).
% 178.96/178.96 cnf(401,plain,
% 178.96/178.96 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f8(x4011),f7(x4011,x4011)))),
% 178.96/178.96 inference(scs_inference,[],[398,277,3,2])).
% 178.96/178.96 cnf(404,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[401,316,3,2])).
% 178.96/178.96 cnf(407,plain,
% 178.96/178.96 (E(f6(f8(x4071),x4071),f6(f8(x4072),f7(x4072,x4072)))),
% 178.96/178.96 inference(scs_inference,[],[337,325,3,2])).
% 178.96/178.96 cnf(410,plain,
% 178.96/178.96 (E(f6(f8(x4101),f7(x4101,x4101)),f6(f7(f8(x4102),f8(x4102)),f3(x4102,x4102)))),
% 178.96/178.96 inference(scs_inference,[],[407,132,3,2])).
% 178.96/178.96 cnf(413,plain,
% 178.96/178.96 (E(f3(a5,a5),f7(f3(a5,x4131),a5))),
% 178.96/178.96 inference(scs_inference,[],[223,389,3,2])).
% 178.96/178.96 cnf(414,plain,
% 178.96/178.96 (E(f6(f8(x4141),f7(x4141,x4141)),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[410,220,3])).
% 178.96/178.96 cnf(416,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f8(x4161),f7(x4161,x4161)))),
% 178.96/178.96 inference(scs_inference,[],[410,220,3,2])).
% 178.96/178.96 cnf(419,plain,
% 178.96/178.96 (E(f7(a5,a5),f6(f8(x4191),f7(x4191,x4191)))),
% 178.96/178.96 inference(scs_inference,[],[262,410,3,2])).
% 178.96/178.96 cnf(422,plain,
% 178.96/178.96 (E(f3(f7(a5,x4221),a5),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[419,337,3,2])).
% 178.96/178.96 cnf(425,plain,
% 178.96/178.96 (E(f7(a5,a5),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[422,328,3,2])).
% 178.96/178.96 cnf(428,plain,
% 178.96/178.96 (E(f7(a5,a5),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[340,422,3,2])).
% 178.96/178.96 cnf(431,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[416,316,3,2])).
% 178.96/178.96 cnf(434,plain,
% 178.96/178.96 (E(f6(f8(x4341),f7(x4341,x4341)),f6(f3(f8(x4342),f8(x4342)),f3(x4342,x4342)))),
% 178.96/178.96 inference(scs_inference,[],[111,396,3,2])).
% 178.96/178.96 cnf(435,plain,
% 178.96/178.96 (E(f6(f8(x4351),f7(x4351,x4351)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[434,244,3])).
% 178.96/178.96 cnf(437,plain,
% 178.96/178.96 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f8(x4371),f7(x4371,x4371)))),
% 178.96/178.96 inference(scs_inference,[],[434,244,3,2])).
% 178.96/178.96 cnf(441,plain,
% 178.96/178.96 (E(f3(f6(a5,a5),f6(a5,a5)),f3(f7(a5,x4411),a5))),
% 178.96/178.96 inference(scs_inference,[],[437,337,3])).
% 178.96/178.96 cnf(443,plain,
% 178.96/178.96 (E(f3(f7(a5,x4431),a5),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[437,337,3,2])).
% 178.96/178.96 cnf(449,plain,
% 178.96/178.96 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[401,435,3,2])).
% 178.96/178.96 cnf(450,plain,
% 178.96/178.96 (E(f7(a5,a5),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[419,414,3])).
% 178.96/178.96 cnf(455,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[437,316,3,2])).
% 178.96/178.96 cnf(469,plain,
% 178.96/178.96 (E(f7(x4691,f7(x4692,f7(x4691,x4692))),f7(x4692,x4691))),
% 178.96/178.96 inference(scs_inference,[],[17,72,3,2])).
% 178.96/178.96 cnf(473,plain,
% 178.96/178.96 (E(f7(x4731,f7(x4732,x4733)),f7(x4733,f7(x4731,x4732)))),
% 178.96/178.96 inference(scs_inference,[],[17,21,3,2])).
% 178.96/178.96 cnf(486,plain,
% 178.96/178.96 (E(f7(a5,f7(a5,f7(a5,a5))),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[75,450,3])).
% 178.96/178.96 cnf(495,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x4951)),f3(x4951,x4951)),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[22,190,3])).
% 178.96/178.96 cnf(497,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f6(a5,f8(x4971)),f3(x4971,x4971)))),
% 178.96/178.96 inference(scs_inference,[],[495,2])).
% 178.96/178.96 cnf(498,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x4981)),f3(x4981,x4981)),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[22,214,495,2,3])).
% 178.96/178.96 cnf(500,plain,
% 178.96/178.96 (E(f3(a5,a5),f6(f6(a5,f8(x5001)),f3(x5001,x5001)))),
% 178.96/178.96 inference(scs_inference,[],[498,2])).
% 178.96/178.96 cnf(501,plain,
% 178.96/178.96 (E(f6(f8(x5011),f3(x5011,x5011)),f6(f6(a5,f8(x5012)),f3(x5012,x5012)))),
% 178.96/178.96 inference(scs_inference,[],[202,497,498,2,3])).
% 178.96/178.96 cnf(502,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x5021)),f3(x5021,x5021)),f6(f8(x5022),f3(x5022,x5022)))),
% 178.96/178.96 inference(scs_inference,[],[501,2])).
% 178.96/178.96 cnf(503,plain,
% 178.96/178.96 (E(f7(f6(a5,a5),f6(a5,a5)),f6(f6(a5,f8(x5031)),f3(x5031,x5031)))),
% 178.96/178.96 inference(scs_inference,[],[431,500,501,2,3])).
% 178.96/178.96 cnf(505,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x5051)),f3(x5051,x5051)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[235,502,503,2,3])).
% 178.96/178.96 cnf(507,plain,
% 178.96/178.96 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f6(a5,f8(x5071)),f3(x5071,x5071)))),
% 178.96/178.96 inference(scs_inference,[],[505,2])).
% 178.96/178.96 cnf(508,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x5081)),f3(x5081,x5081)),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[22,256,505,2,3])).
% 178.96/178.96 cnf(510,plain,
% 178.96/178.96 (E(f7(a5,a5),f6(f6(a5,f8(x5101)),f3(x5101,x5101)))),
% 178.96/178.96 inference(scs_inference,[],[508,2])).
% 178.96/178.96 cnf(511,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x5111)),x5111),f3(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[22,211,508,2,3])).
% 178.96/178.96 cnf(515,plain,
% 178.96/178.96 (E(f6(f6(a5,f8(x5151)),x5151),f7(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[22,253,511,2,3])).
% 178.96/178.96 cnf(519,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(f8(x5191),f3(x5191,x5191)))),
% 178.96/178.96 inference(scs_inference,[],[22,203,515,2,3])).
% 178.96/178.96 cnf(521,plain,
% 178.96/178.96 (E(f6(f8(x5211),f3(x5211,x5211)),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[519,2])).
% 178.96/178.96 cnf(522,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(f3(f8(x5221),f8(x5221)),f3(x5221,x5221)))),
% 178.96/178.96 inference(scs_inference,[],[22,197,519,2,3])).
% 178.96/178.96 cnf(524,plain,
% 178.96/178.96 (E(f6(f3(f8(x5241),f8(x5241)),f3(x5241,x5241)),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[522,2])).
% 178.96/178.96 cnf(525,plain,
% 178.96/178.96 (E(f6(f7(f8(x5251),f8(x5251)),f3(x5251,x5251)),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[521,113,522,2,3])).
% 178.96/178.96 cnf(527,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(f7(f8(x5271),f8(x5271)),f3(x5271,x5271)))),
% 178.96/178.96 inference(scs_inference,[],[525,2])).
% 178.96/178.96 cnf(528,plain,
% 178.96/178.96 (E(f6(f8(x5281),f7(x5281,x5281)),f6(a5,f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[205,398,525,2,3])).
% 178.96/178.96 cnf(530,plain,
% 178.96/178.96 (E(f6(a5,f6(a5,a5)),f6(f8(x5301),f7(x5301,x5301)))),
% 178.96/178.96 inference(scs_inference,[],[528,2])).
% 178.96/178.96 cnf(531,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[178,527,528,2,3])).
% 178.96/178.96 cnf(533,plain,
% 178.96/178.96 (E(f6(a5,a5),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[531,2])).
% 178.96/178.96 cnf(534,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(f8(x5341),f7(x5341,x5341)))),
% 178.96/178.96 inference(scs_inference,[],[22,530,531,2,3])).
% 178.96/178.96 cnf(536,plain,
% 178.96/178.96 (E(f6(f8(x5361),f7(x5361,x5361)),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[534,2])).
% 178.96/178.96 cnf(537,plain,
% 178.96/178.96 (E(f6(f8(x5371),x5371),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[524,126,534,2,3])).
% 178.96/178.96 cnf(539,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f6(f8(x5391),x5391))),
% 178.96/178.96 inference(scs_inference,[],[537,2])).
% 178.96/178.96 cnf(540,plain,
% 178.96/178.96 (E(f3(a5,f7(a5,x5401)),f6(a5,f6(a5,a5)))),
% 178.96/178.96 inference(scs_inference,[],[199,151,537,2,3])).
% 178.96/178.96 cnf(542,plain,
% 178.96/178.96 (E(f6(a5,f6(a5,a5)),f3(a5,f7(a5,x5421)))),
% 178.96/178.96 inference(scs_inference,[],[540,2])).
% 178.96/178.96 cnf(543,plain,
% 178.96/178.96 (E(f7(f3(a5,x5431),a5),f6(a5,a5))),
% 178.96/178.96 inference(scs_inference,[],[175,381,540,2,3])).
% 178.96/178.96 cnf(545,plain,
% 178.96/178.96 (E(f6(a5,a5),f7(f3(a5,x5451),a5))),
% 178.96/178.96 inference(scs_inference,[],[543,2])).
% 178.96/178.96 cnf(546,plain,
% 178.96/178.96 (E(a5,f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[533,36,543,2,3])).
% 178.96/178.96 cnf(548,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),a5)),
% 178.96/178.96 inference(scs_inference,[],[546,2])).
% 178.96/178.96 cnf(549,plain,
% 178.96/178.96 (E(f6(f6(a5,a5),a5),f3(a5,f7(a5,x5491)))),
% 178.96/178.96 inference(scs_inference,[],[22,542,546,2,3])).
% 178.96/178.96 cnf(551,plain,
% 178.96/178.96 (E(f3(a5,f7(a5,x5511)),f6(f6(a5,a5),a5))),
% 178.96/178.96 inference(scs_inference,[],[549,2])).
% 178.96/178.96 cnf(552,plain,
% 178.96/178.97 (E(f6(a5,f6(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[144,548,549,2,3])).
% 178.96/178.97 cnf(554,plain,
% 178.96/178.97 (E(a5,f6(a5,f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[552,2])).
% 178.96/178.97 cnf(555,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[283,527,552,2,3])).
% 178.96/178.97 cnf(557,plain,
% 178.96/178.97 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[555,2])).
% 178.96/178.97 cnf(558,plain,
% 178.96/178.97 (E(f6(f8(x5581),f7(x5581,x5581)),a5)),
% 178.96/178.97 inference(scs_inference,[],[536,548,555,2,3])).
% 178.96/178.97 cnf(559,plain,
% 178.96/178.97 (E(a5,f6(f8(x5591),f7(x5591,x5591)))),
% 178.96/178.97 inference(scs_inference,[],[558,2])).
% 178.96/178.97 cnf(560,plain,
% 178.96/178.97 (E(f7(f3(a5,a5),f3(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[557,548,558,2,3])).
% 178.96/178.97 cnf(562,plain,
% 178.96/178.97 (E(a5,f7(f3(a5,x5621),a5))),
% 178.96/178.97 inference(scs_inference,[],[387,559,560,2,3])).
% 178.96/178.97 cnf(564,plain,
% 178.96/178.97 (E(f7(f3(a5,x5641),a5),a5)),
% 178.96/178.97 inference(scs_inference,[],[562,2])).
% 178.96/178.97 cnf(565,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x5651)),x5651),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[22,182,562,2,3])).
% 178.96/178.97 cnf(569,plain,
% 178.96/178.97 (E(f7(f3(a5,x5691),a5),f6(a5,f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[554,564,565,2,3])).
% 178.96/178.97 cnf(570,plain,
% 178.96/178.97 (E(f6(a5,f6(a5,a5)),f7(f3(a5,x5701),a5))),
% 178.96/178.97 inference(scs_inference,[],[569,2])).
% 178.96/178.97 cnf(571,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x5711)),f3(x5711,x5711)),a5)),
% 178.96/178.97 inference(scs_inference,[],[22,569,185,2,3])).
% 178.96/178.97 cnf(573,plain,
% 178.96/178.97 (E(a5,f6(f6(a5,f8(x5731)),f3(x5731,x5731)))),
% 178.96/178.97 inference(scs_inference,[],[571,2])).
% 178.96/178.97 cnf(574,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f7(f3(a5,x5741),a5))),
% 178.96/178.97 inference(scs_inference,[],[22,570,571,2,3])).
% 178.96/178.97 cnf(576,plain,
% 178.96/178.97 (E(f7(f3(a5,x5761),a5),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[574,2])).
% 178.96/178.97 cnf(577,plain,
% 178.96/178.97 (E(f7(f3(a5,x5771),a5),f6(f6(a5,f8(x5772)),f3(x5772,x5772)))),
% 178.96/178.97 inference(scs_inference,[],[573,564,574,2,3])).
% 178.96/178.97 cnf(578,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x5781)),f3(x5781,x5781)),f7(f3(a5,x5782),a5))),
% 178.96/178.97 inference(scs_inference,[],[577,2])).
% 178.96/178.97 cnf(579,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x5791)),x5791),a5)),
% 178.96/178.97 inference(scs_inference,[],[22,577,206,2,3])).
% 178.96/178.97 cnf(583,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f3(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[507,579,498,2,3])).
% 178.96/178.97 cnf(585,plain,
% 178.96/178.97 (E(f3(a5,a5),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[583,2])).
% 178.96/178.97 cnf(586,plain,
% 178.96/178.97 (E(f7(a5,a5),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[510,583,495,2,3])).
% 178.96/178.97 cnf(588,plain,
% 178.96/178.97 (E(f6(a5,a5),f7(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[586,2])).
% 178.96/178.97 cnf(589,plain,
% 178.96/178.97 (E(f7(a5,f7(a5,f7(a5,a5))),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[469,586,2,3])).
% 178.96/178.97 cnf(591,plain,
% 178.96/178.97 (E(f6(a5,a5),f7(a5,f7(a5,f7(a5,a5))))),
% 178.96/178.97 inference(scs_inference,[],[589,2])).
% 178.96/178.97 cnf(592,plain,
% 178.96/178.97 (E(f6(a5,a5),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[425,588,589,2,3])).
% 178.96/178.97 cnf(593,plain,
% 178.96/178.97 (E(f7(f3(a5,a5),f3(a5,a5)),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[592,2])).
% 178.96/178.97 cnf(594,plain,
% 178.96/178.97 (E(f7(a5,a5),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[428,455,592,2,3])).
% 178.96/178.97 cnf(595,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f7(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[594,2])).
% 178.96/178.97 cnf(596,plain,
% 178.96/178.97 (E(f7(f7(a5,a5),f7(a5,a5)),f7(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[365,374,594,2,3])).
% 178.96/178.97 cnf(598,plain,
% 178.96/178.97 (E(f7(f3(a5,a5),f3(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[596,2])).
% 178.96/178.97 cnf(599,plain,
% 178.96/178.97 (E(f7(a5,a5),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[379,576,596,2,3])).
% 178.96/178.97 cnf(601,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f7(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[599,2])).
% 178.96/178.97 cnf(602,plain,
% 178.96/178.97 (E(f7(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[404,557,599,2,3])).
% 178.96/178.97 cnf(603,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[602,2])).
% 178.96/178.97 cnf(604,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f7(f7(a5,a5),f7(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[449,598,602,2,3])).
% 178.96/178.97 cnf(605,plain,
% 178.96/178.97 (E(f7(f7(a5,a5),f7(a5,a5)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[604,2])).
% 178.96/178.97 cnf(606,plain,
% 178.96/178.97 (E(f3(a5,f7(a5,x6061)),f7(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[601,551,604,2,3])).
% 178.96/178.97 cnf(607,plain,
% 178.96/178.97 (E(f7(a5,a5),f3(a5,f7(a5,x6071)))),
% 178.96/178.97 inference(scs_inference,[],[606,2])).
% 178.96/178.97 cnf(608,plain,
% 178.96/178.97 (E(f6(a5,f6(a5,a5)),f7(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[603,144,606,2,3])).
% 178.96/178.97 cnf(611,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f3(a5,f7(a5,x6111)))),
% 178.96/178.97 inference(scs_inference,[],[595,607,608,2,3])).
% 178.96/178.97 cnf(612,plain,
% 178.96/178.97 (E(f3(a5,f7(a5,x6121)),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[611,2])).
% 178.96/178.97 cnf(613,plain,
% 178.96/178.97 (E(f7(f3(a5,a5),f3(a5,a5)),f6(f6(a5,f8(x6131)),f3(x6131,x6131)))),
% 178.96/178.97 inference(scs_inference,[],[593,497,611,2,3])).
% 178.96/178.97 cnf(615,plain,
% 178.96/178.97 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f6(a5,f8(x6151)),f3(x6151,x6151)))),
% 178.96/178.97 inference(scs_inference,[],[605,507,613,2,3])).
% 178.96/178.97 cnf(617,plain,
% 178.96/178.97 (E(f6(f8(x6171),x6171),f6(f6(a5,f8(x6172)),f3(x6172,x6172)))),
% 178.96/178.97 inference(scs_inference,[],[265,510,615,2,3])).
% 178.96/178.97 cnf(619,plain,
% 178.96/178.97 (E(f7(f6(a5,a5),f6(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[384,564,617,2,3])).
% 178.96/178.97 cnf(622,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[392,576,619,2,3])).
% 178.96/178.97 cnf(624,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[622,2])).
% 178.96/178.97 cnf(625,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f6(f6(a5,f8(x6251)),f3(x6251,x6251)))),
% 178.96/178.97 inference(scs_inference,[],[573,548,622,2,3])).
% 178.96/178.97 cnf(626,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x6261)),f3(x6261,x6261)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[625,2])).
% 178.96/178.97 cnf(627,plain,
% 178.96/178.97 (E(f3(a5,a5),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[413,576,625,2,3])).
% 178.96/178.97 cnf(629,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f3(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[627,2])).
% 178.96/178.97 cnf(630,plain,
% 178.96/178.97 (E(f6(a5,a5),f7(a5,f3(a5,x6301)))),
% 178.96/178.97 inference(scs_inference,[],[545,356,627,2,3])).
% 178.96/178.97 cnf(632,plain,
% 178.96/178.97 (E(f7(a5,f3(a5,x6321)),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[630,2])).
% 178.96/178.97 cnf(633,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x6331)),f3(x6331,x6331)),f7(a5,f3(a5,x6332)))),
% 178.96/178.97 inference(scs_inference,[],[578,356,630,2,3])).
% 178.96/178.97 cnf(636,plain,
% 178.96/178.97 (E(f7(a5,f3(a5,x6361)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[632,533,633,2,3])).
% 178.96/178.97 cnf(638,plain,
% 178.96/178.97 (E(f3(a5,a5),f3(f7(a5,x6381),a5))),
% 178.96/178.97 inference(scs_inference,[],[585,441,636,2,3])).
% 178.96/178.97 cnf(640,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f7(f7(a5,a5),f7(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[624,638,604,2,3])).
% 178.96/178.97 cnf(641,plain,
% 178.96/178.97 (E(f7(f7(a5,a5),f7(a5,a5)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[640,2])).
% 178.96/178.97 cnf(642,plain,
% 178.96/178.97 (E(f3(f7(a5,x6421),a5),f6(f6(a5,f8(x6422)),f3(x6422,x6422)))),
% 178.96/178.97 inference(scs_inference,[],[443,507,640,2,3])).
% 178.96/178.97 cnf(643,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x6431)),f3(x6431,x6431)),f3(f7(a5,x6432),a5))),
% 178.96/178.97 inference(scs_inference,[],[642,2])).
% 178.96/178.97 cnf(644,plain,
% 178.96/178.97 (E(f3(a5,f7(a5,x6441)),f6(f6(a5,f8(x6442)),f3(x6442,x6442)))),
% 178.96/178.97 inference(scs_inference,[],[612,507,642,2,3])).
% 178.96/178.97 cnf(645,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x6451)),f3(x6451,x6451)),f3(a5,f7(a5,x6452)))),
% 178.96/178.97 inference(scs_inference,[],[644,2])).
% 178.96/178.97 cnf(646,plain,
% 178.96/178.97 (E(f7(f7(a5,a5),f7(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[641,548,644,2,3])).
% 178.96/178.97 cnf(648,plain,
% 178.96/178.97 (E(f6(f6(a5,f8(x6481)),f3(x6481,x6481)),f6(f8(x6482),f7(x6482,x6482)))),
% 178.96/178.97 inference(scs_inference,[],[645,121,646,2,3])).
% 178.96/178.97 cnf(651,plain,
% 178.96/178.97 (E(f7(a5,f7(f7(a5,a5),a5)),f6(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[473,648,589,2,3])).
% 178.96/178.97 cnf(654,plain,
% 178.96/178.97 (E(f6(a5,a5),f3(a5,a5))),
% 178.96/178.97 inference(scs_inference,[],[591,651,486,2,3])).
% 178.96/178.97 cnf(664,plain,
% 178.96/178.97 (E(f3(f7(a5,x6641),a5),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[629,638,3,2])).
% 178.96/178.97 cnf(665,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),a5),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[539,226,3])).
% 178.96/178.97 cnf(667,plain,
% 178.96/178.97 (E(f3(f3(a5,a5),f3(a5,a5)),f6(f6(a5,a5),a5))),
% 178.96/178.97 inference(scs_inference,[],[539,226,3,2])).
% 178.96/178.97 cnf(675,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[667,624,3,2])).
% 178.96/178.97 cnf(677,plain,
% 178.96/178.97 (E(f3(f3(a5,a5),f3(a5,a5)),f6(f6(a5,f8(x6771)),f3(x6771,x6771)))),
% 178.96/178.97 inference(scs_inference,[],[626,665,3,2])).
% 178.96/178.97 cnf(682,plain,
% 178.96/178.97 (E(a5,f3(f7(a5,x6821),a5))),
% 178.96/178.97 inference(scs_inference,[],[664,548,3,2])).
% 178.96/178.97 cnf(699,plain,
% 178.96/178.97 (E(f3(f7(a5,x6991),a5),f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[643,677,3,2])).
% 178.96/178.97 cnf(700,plain,
% 178.96/178.97 (E(a5,f3(f3(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[699,682,3])).
% 178.96/178.97 cnf(702,plain,
% 178.96/178.97 (E(f3(f3(a5,a5),f3(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[699,682,3,2])).
% 178.96/178.97 cnf(709,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[675,702,3])).
% 178.96/178.97 cnf(710,plain,
% 178.96/178.97 (E(a5,f3(f6(a5,a5),f6(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[675,702,3,2])).
% 178.96/178.97 cnf(759,plain,
% 178.96/178.97 (~E(a2,f3(a1,a1))),
% 178.96/178.97 inference(scs_inference,[],[31,43,3,7])).
% 178.96/178.97 cnf(762,plain,
% 178.96/178.97 (~E(a2,f7(a1,a1))),
% 178.96/178.97 inference(scs_inference,[],[31,50,3,7])).
% 178.96/178.97 cnf(763,plain,
% 178.96/178.97 (~E(a2,f7(a1,f7(a1,f7(a1,a1))))),
% 178.96/178.97 inference(scs_inference,[],[75,762,3])).
% 178.96/178.97 cnf(765,plain,
% 178.96/178.97 (~E(a2,f7(a1,f7(f7(a1,a1),a1)))),
% 178.96/178.97 inference(scs_inference,[],[473,763,3])).
% 178.96/178.97 cnf(767,plain,
% 178.96/178.97 (~E(f6(a4,a2),f6(f3(a4,a4),a1))),
% 178.96/178.97 inference(scs_inference,[],[31,57,3])).
% 178.96/178.97 cnf(769,plain,
% 178.96/178.97 (~E(f6(a4,a2),f6(f7(a4,a4),a1))),
% 178.96/178.97 inference(scs_inference,[],[31,64,3])).
% 178.96/178.97 cnf(771,plain,
% 178.96/178.97 (~E(a2,f7(f7(a1,a1),f7(a1,a1)))),
% 178.96/178.97 inference(scs_inference,[],[473,765,3])).
% 178.96/178.97 cnf(773,plain,
% 178.96/178.97 (~E(a2,f7(f7(f7(a1,a1),a1),a1))),
% 178.96/178.97 inference(scs_inference,[],[350,771,3])).
% 178.96/178.97 cnf(775,plain,
% 178.96/178.97 (~E(a2,f7(f7(a1,f7(a1,a1)),a1))),
% 178.96/178.97 inference(scs_inference,[],[350,773,3])).
% 178.96/178.97 cnf(777,plain,
% 178.96/178.97 (~E(f6(a4,a2),f3(f6(a4,a1),f7(f6(a4,a1),x7771)))),
% 178.96/178.97 inference(scs_inference,[],[31,18,3])).
% 178.96/178.97 cnf(789,plain,
% 178.96/178.97 (~E(f6(a4,a2),f7(f6(a4,a1),f6(a4,a1)))),
% 178.96/178.97 inference(scs_inference,[],[31,14,3])).
% 178.96/178.97 cnf(791,plain,
% 178.96/178.97 (~E(a2,f6(a5,a1))),
% 178.96/178.97 inference(scs_inference,[],[32,12,3])).
% 178.96/178.97 cnf(825,plain,
% 178.96/178.97 (~E(a2,f3(a1,f3(a1,f3(a1,a1))))),
% 178.96/178.97 inference(scs_inference,[],[71,759,3])).
% 178.96/178.97 cnf(894,plain,
% 178.96/178.97 (E(a5,f6(a5,f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[39,709,3,2])).
% 178.96/178.97 cnf(996,plain,
% 178.96/178.97 (E(f3(f6(a5,a5),f6(a5,a5)),f6(f6(a5,a5),f3(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[43,624,3,2])).
% 178.96/178.97 cnf(998,plain,
% 178.96/178.97 (E(f6(f6(a5,a5),f3(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[710,996,3,2])).
% 178.96/178.97 cnf(1105,plain,
% 178.96/178.97 (E(f3(f7(a5,x11051),a5),f6(a5,f7(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[46,340,3,2])).
% 178.96/178.97 cnf(1120,plain,
% 178.96/178.97 (E(f6(a5,f7(a5,a5)),f6(f8(x11201),f3(x11201,x11201)))),
% 178.96/178.97 inference(scs_inference,[],[331,1105,3,2])).
% 178.96/178.97 cnf(1129,plain,
% 178.96/178.97 (E(f6(a5,f7(a5,a5)),a5)),
% 178.96/178.97 inference(scs_inference,[],[1120,101,3])).
% 178.96/178.97 cnf(1131,plain,
% 178.96/178.97 (E(a5,f6(a5,f7(a5,a5)))),
% 178.96/178.97 inference(scs_inference,[],[1120,101,3,2])).
% 178.96/178.97 cnf(1216,plain,
% 178.96/178.97 (E(f6(x12161,a1),f6(x12161,f3(a1,a2)))),
% 178.96/178.97 inference(scs_inference,[],[147,10,4,6,8,9,5,7])).
% 178.96/178.97 cnf(1223,plain,
% 178.96/178.97 (E(f6(a5,x12231),f6(f3(f3(a5,a5),f3(a5,a5)),x12231))),
% 178.96/178.97 inference(scs_inference,[],[700,4,10,9,6])).
% 178.96/178.97 cnf(1227,plain,
% 178.96/178.97 (~E(f6(a5,a1),a2)),
% 178.96/178.97 inference(scs_inference,[],[791,700,4,10,9,6,8,5,7,2])).
% 178.96/178.97 cnf(1237,plain,
% 178.96/178.97 (~E(f6(f7(a4,a4),a1),f6(a4,a2))),
% 178.96/178.97 inference(scs_inference,[],[894,769,10,4,9,8,6,5,7,2])).
% 178.96/178.97 cnf(1238,plain,
% 178.96/178.97 (~E(f6(a5,f3(a1,a2)),a2)),
% 178.96/178.97 inference(scs_inference,[],[1227,894,769,1216,10,4,9,8,6,5,7,2,3])).
% 178.96/178.97 cnf(1259,plain,
% 178.96/178.97 (~E(f6(f3(f7(a4,a4),f7(a4,a4)),a1),f6(a4,a2))),
% 178.96/178.97 inference(scs_inference,[],[1237,767,1129,54,10,4,9,8,6,5,7,2,3])).
% 178.96/178.97 cnf(1268,plain,
% 178.96/178.97 (~E(f3(f3(a1,a2),f3(a1,a2)),a2)),
% 178.96/178.97 inference(scs_inference,[],[161,1131,4,10,9,6,8,5,7,2])).
% 178.96/178.97 cnf(1299,plain,
% 178.96/178.97 (~E(f6(f3(f3(a5,a5),f3(a5,a5)),f3(a1,a2)),a2)),
% 178.96/178.97 inference(scs_inference,[],[789,1238,1223,654,10,4,9,8,6,5,7,2,3])).
% 178.96/178.97 cnf(1459,plain,
% 178.96/178.97 (~E(f6(a5,a2),f7(f7(a1,f7(a1,a1)),a1))),
% 178.96/178.97 inference(scs_inference,[],[1299,775,586,36,4,10,6,8,9,5,7,2,3])).
% 178.96/178.97 cnf(1499,plain,
% 178.96/178.97 (~E(f6(a5,a2),f3(a1,f3(a1,f3(a1,a1))))),
% 178.96/178.97 inference(scs_inference,[],[1259,825,998,36,10,4,6,9,8,5,7,2,3])).
% 178.96/178.97 cnf(1542,plain,
% 178.96/178.97 (E(f3(f3(a1,a2),x15421),f3(a1,x15421))),
% 178.96/178.97 inference(scs_inference,[],[11,10,4])).
% 178.96/178.97 cnf(1543,plain,
% 178.96/178.97 (E(f6(f3(a1,a2),x15431),f6(a1,x15431))),
% 178.96/178.97 inference(scs_inference,[],[11,10,4,6])).
% 178.96/178.97 cnf(1546,plain,
% 178.96/178.97 (E(f3(x15461,f3(a1,a2)),f3(x15461,a1))),
% 178.96/178.97 inference(scs_inference,[],[11,10,4,6,9,8,5])).
% 178.96/178.97 cnf(1547,plain,
% 178.96/178.97 (E(f6(x15471,f3(a1,a2)),f6(x15471,a1))),
% 178.96/178.97 inference(scs_inference,[],[11,10,4,6,9,8,5,7])).
% 178.96/178.97 cnf(1559,plain,
% 178.96/178.97 (~E(f3(a1,f3(a1,a2)),a2)),
% 178.96/178.97 inference(scs_inference,[],[1542,1268,1499,702,10,4,6,8,9,5,7,2,3])).
% 178.96/178.97 cnf(1568,plain,
% 178.96/178.97 (~E(a2,f3(a1,f3(a1,a2)))),
% 178.96/178.97 inference(scs_inference,[],[1559,98,10,4,6,8,9,5,7,2])).
% 178.96/178.97 cnf(1576,plain,
% 178.96/178.97 (E(f7(x15761,f3(x15762,f7(x15762,x15763))),f7(x15761,x15762))),
% 178.96/178.97 inference(scs_inference,[],[18,10,6,8,4,9])).
% 178.96/178.97 cnf(1580,plain,
% 178.96/178.97 (~E(f7(a2,a2),f3(a1,f3(a1,a2)))),
% 178.96/178.97 inference(scs_inference,[],[1568,1459,18,33,10,6,8,4,9,5,7,2,3])).
% 178.96/178.97 cnf(1589,plain,
% 178.96/178.97 (~E(f3(a1,f3(a1,a2)),f7(a2,a2))),
% 178.96/178.97 inference(scs_inference,[],[1580,19,10,8,6,4,9,5,7,2])).
% 178.96/178.97 cnf(1601,plain,
% 178.96/178.97 (~E(f3(a1,a1),f7(a2,a2))),
% 178.96/178.97 inference(scs_inference,[],[1546,1589,777,15,10,8,4,6,9,5,7,2,3])).
% 178.96/178.97 cnf(1611,plain,
% 178.96/178.97 (E(f3(a1,a2),f7(a1,a1))),
% 178.96/178.97 inference(scs_inference,[],[1601,163,1576,36,10,8,4,6,9,5,7,2,3])).
% 178.96/178.97 cnf(1619,plain,
% 178.96/178.97 (E(f3(x16191,f3(a1,a2)),f3(x16191,f7(a1,a1)))),
% 178.96/178.97 inference(scs_inference,[],[1611,10,8,4,6,9,5])).
% 178.96/178.97 cnf(1785,plain,
% 178.96/178.97 (E(f7(f6(a5,f6(a5,a5)),f6(a5,f6(a5,a5))),a5)),
% 178.96/178.97 inference(scs_inference,[],[14,552,1619,2,3])).
% 178.96/178.97 cnf(2267,plain,
% 178.96/178.97 (E(f7(f6(f3(a1,a2),x22671),f6(f3(a1,a2),x22671)),f6(a1,x22671))),
% 178.96/178.97 inference(scs_inference,[],[14,1543,1785,2,3])).
% 178.96/178.97 cnf(2270,plain,
% 178.96/178.97 ($false),
% 178.96/178.97 inference(scs_inference,[],[27,23,1547,2267,2,3]),
% 178.96/178.97 ['proof']).
% 178.96/178.97 % SZS output end Proof
% 178.96/178.97 % Total time :178.320000s
%------------------------------------------------------------------------------