%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CAT004-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n029.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 04:40:09 EDT 2024
% Result : Unsatisfiable 116.68s 116.78s
% Output : CNFRefutation 116.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.11 % Problem : CAT004-2 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n029.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Tue Jun 18 11:58:24 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.46/0.53 start to proof:theBenchmark
% 116.68/116.77 %-------------------------------------------
% 116.68/116.77 % File :CSE---1.7
% 116.68/116.77 % Problem :theBenchmark
% 116.68/116.77 % Transform :cnf
% 116.68/116.77 % Format :tptp:raw
% 116.68/116.77 % Command :java -jar mcs_scs.jar %d %s
% 116.68/116.77
% 116.68/116.77 % Result :Theorem 116.170000s
% 116.68/116.77 % Output :CNFRefutation 116.170000s
% 116.68/116.77 %-------------------------------------------
% 116.68/116.78 %--------------------------------------------------------------------------
% 116.68/116.78 % File : CAT004-2 : TPTP v8.2.0. Released v1.0.0.
% 116.68/116.78 % Domain : Category Theory
% 116.68/116.78 % Problem : X and Y epimorphisms, XY well-defined => XY epimorphism
% 116.68/116.78 % Version : [Qua89] (equality) axioms.
% 116.68/116.78 % English : If x and y are epimorphisms and xy is well-defined, then
% 116.68/116.78 % xy is an epimorphism.
% 116.68/116.78
% 116.68/116.78 % Refs : [Qua89] Quaife (1989), Email to L. Wos
% 116.68/116.78 % Source : [ANL]
% 116.68/116.78 % Names : p4.ver2.in [ANL]
% 116.68/116.78
% 116.68/116.78 % Status : Unsatisfiable
% 116.68/116.78 % Rating : 0.00 v8.1.0, 0.05 v7.5.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.09 v7.0.0, 0.08 v6.4.0, 0.14 v6.3.0, 0.20 v6.2.0, 0.30 v6.1.0, 0.09 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.00 v5.3.0, 0.20 v5.2.0, 0.00 v4.1.0, 0.11 v4.0.1, 0.12 v4.0.0, 0.14 v3.7.0, 0.29 v3.5.0, 0.14 v3.4.0, 0.33 v3.3.0, 0.22 v3.2.0, 0.11 v3.1.0, 0.20 v2.7.0, 0.38 v2.6.0, 0.33 v2.5.0, 0.50 v2.4.0, 0.25 v2.3.0, 0.50 v2.2.1, 0.33 v2.2.0, 0.50 v2.1.0, 1.00 v2.0.0
% 116.68/116.78 % Syntax : Number of clauses : 14 ( 9 unt; 0 nHn; 10 RR)
% 116.68/116.78 % Number of literals : 26 ( 26 equ; 13 neg)
% 116.68/116.78 % Maximal clause size : 5 ( 1 avg)
% 116.68/116.78 % Maximal term depth : 3 ( 2 avg)
% 116.68/116.78 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 116.68/116.78 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 116.68/116.78 % Number of variables : 17 ( 0 sgn)
% 116.68/116.78 % SPC : CNF_UNS_RFO_PEQ_NUE
% 116.68/116.78
% 116.68/116.78 % Comments :
% 116.68/116.78 %--------------------------------------------------------------------------
% 116.68/116.78 %----Include Quaife's axioms for category theory
% 116.68/116.78 include('Axioms/CAT002-0.ax').
% 116.68/116.78 %--------------------------------------------------------------------------
% 116.68/116.78 cnf(epimorphism1,hypothesis,
% 116.68/116.78 ( codomain(a) != domain(X)
% 116.68/116.78 | compose(a,X) != Y
% 116.68/116.78 | codomain(a) != domain(Z)
% 116.68/116.78 | compose(a,Z) != Y
% 116.68/116.78 | X = Z ) ).
% 116.68/116.78
% 116.68/116.78 cnf(epimorphism2,hypothesis,
% 116.68/116.78 ( codomain(b) != domain(X)
% 116.68/116.78 | compose(b,X) != Y
% 116.68/116.78 | codomain(b) != domain(Z)
% 116.68/116.78 | compose(b,Z) != Y
% 116.68/116.78 | X = Z ) ).
% 116.68/116.78
% 116.68/116.78 cnf(codomain_of_a_equals_domain_of_b,hypothesis,
% 116.68/116.78 codomain(a) = domain(b) ).
% 116.68/116.78
% 116.68/116.78 cnf(codomain_of_ab_equals_domain_of_h,hypothesis,
% 116.68/116.78 codomain(compose(a,b)) = domain(h) ).
% 116.68/116.78
% 116.68/116.78 cnf(codomain_of_ab_equals_domain_of_g,hypothesis,
% 116.68/116.78 codomain(compose(a,b)) = domain(g) ).
% 116.68/116.78
% 116.68/116.78 cnf(ab_h_equals_ab_g,hypothesis,
% 116.68/116.78 compose(compose(a,b),h) = compose(compose(a,b),g) ).
% 116.68/116.78
% 116.68/116.78 cnf(prove_h_equals_g,negated_conjecture,
% 116.68/116.78 h != g ).
% 116.68/116.78
% 116.68/116.78 %--------------------------------------------------------------------------
% 116.68/116.78 %-------------------------------------------
% 116.68/116.78 % Proof found
% 116.68/116.78 % SZS status Theorem for theBenchmark
% 116.68/116.78 % SZS output start Proof
% 116.68/116.78 %ClaNum:21(EqnAxiom:7)
% 116.68/116.78 %VarNum:46(SingletonVarNum:17)
% 116.68/116.78 %MaxLitNum:5
% 116.68/116.78 %MaxfuncDepth:2
% 116.68/116.78 %SharedTerms:18
% 116.68/116.78 %goalClause: 16
% 116.68/116.78 %singleGoalClaCount:1
% 116.68/116.78 [16]~E(a7,a6)
% 116.68/116.78 [8]E(f3(a1),f4(a2))
% 116.68/116.78 [13]E(f4(f5(a2,a1)),f3(a6))
% 116.68/116.78 [14]E(f4(f5(a2,a1)),f3(a7))
% 116.68/116.78 [15]E(f5(f5(a2,a1),a7),f5(f5(a2,a1),a6))
% 116.68/116.78 [9]E(f3(f4(x91)),f4(x91))
% 116.68/116.78 [10]E(f4(f3(x101)),f3(x101))
% 116.68/116.78 [11]E(f5(x111,f4(x111)),x111)
% 116.68/116.78 [12]E(f5(f3(x121),x121),x121)
% 116.68/116.78 [17]~E(f4(x171),f3(x172))+E(f3(f5(x171,x172)),f3(x171))
% 116.68/116.78 [18]~E(f4(x181),f3(x182))+E(f4(f5(x181,x182)),f4(x182))
% 116.68/116.78 [21]~E(f4(x212),f3(x213))+~E(f4(x211),f3(x212))+E(f5(f5(x211,x212),x213),f5(x211,f5(x212,x213)))
% 116.68/116.78 [19]E(x191,x192)+~E(f5(a2,x191),x193)+~E(f5(a2,x192),x193)+~E(f3(x192),f4(a2))+~E(f3(x191),f4(a2))
% 116.68/116.78 [20]E(x201,x202)+~E(f5(a1,x201),x203)+~E(f5(a1,x202),x203)+~E(f3(x202),f4(a1))+~E(f3(x201),f4(a1))
% 116.68/116.78 %EqnAxiom
% 116.68/116.78 [1]E(x11,x11)
% 116.68/116.78 [2]E(x22,x21)+~E(x21,x22)
% 116.68/116.78 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 116.68/116.78 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 116.68/116.78 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 116.68/116.78 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63))
% 116.68/116.78 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72))
% 116.68/116.78
% 116.68/116.78 %-------------------------------------------
% 116.74/116.79 cnf(22,plain,
% 116.74/116.79 (E(f4(a2),f3(a1))),
% 116.74/116.79 inference(scs_inference,[],[8,2])).
% 116.74/116.79 cnf(23,plain,
% 116.74/116.79 (E(f5(f3(a1),f4(f3(a1))),f4(a2))),
% 116.74/116.79 inference(scs_inference,[],[8,11,2,3])).
% 116.74/116.79 cnf(25,plain,
% 116.74/116.79 (E(f4(a2),f5(f3(a1),f4(f3(a1))))),
% 116.74/116.79 inference(scs_inference,[],[23,2])).
% 116.74/116.79 cnf(26,plain,
% 116.74/116.79 (~E(a7,f5(f3(a6),a6))),
% 116.74/116.79 inference(scs_inference,[],[16,23,12,2,3])).
% 116.74/116.79 cnf(28,plain,
% 116.74/116.79 (E(f4(x281),f3(f4(x281)))),
% 116.74/116.79 inference(scs_inference,[],[9,2])).
% 116.74/116.79 cnf(29,plain,
% 116.74/116.79 (E(f4(f3(f4(x291))),f4(x291))),
% 116.74/116.79 inference(scs_inference,[],[9,10,2,3])).
% 116.74/116.79 cnf(32,plain,
% 116.74/116.79 (E(f4(f3(f4(a2))),f3(a1))),
% 116.74/116.79 inference(scs_inference,[],[29,22,2,3])).
% 116.74/116.79 cnf(35,plain,
% 116.74/116.79 (~E(a7,f5(a6,f4(a6)))),
% 116.74/116.79 inference(scs_inference,[],[16,32,11,2,3])).
% 116.74/116.79 cnf(37,plain,
% 116.74/116.79 (E(f5(f5(a2,a1),a6),f5(f5(a2,a1),a7))),
% 116.74/116.79 inference(scs_inference,[],[15,2])).
% 116.74/116.79 cnf(38,plain,
% 116.74/116.79 (E(f3(a6),f4(f5(a2,a1)))),
% 116.74/116.79 inference(scs_inference,[],[13,2])).
% 116.74/116.79 cnf(39,plain,
% 116.74/116.79 (E(f3(a7),f4(f5(a2,a1)))),
% 116.74/116.79 inference(scs_inference,[],[14,2])).
% 116.74/116.79 cnf(40,plain,
% 116.74/116.79 (E(f5(f3(f3(a6)),f3(a6)),f4(f5(a2,a1)))),
% 116.74/116.79 inference(scs_inference,[],[38,14,12,2,3])).
% 116.74/116.79 cnf(42,plain,
% 116.74/116.80 (E(f4(f5(a2,a1)),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.80 inference(scs_inference,[],[40,2])).
% 116.74/116.80 cnf(43,plain,
% 116.74/116.80 (E(f4(f3(a7)),f4(f5(a2,a1)))),
% 116.74/116.80 inference(scs_inference,[],[40,39,10,2,3])).
% 116.74/116.80 cnf(45,plain,
% 116.74/116.80 (E(f4(f5(a2,a1)),f4(f3(a7)))),
% 116.74/116.80 inference(scs_inference,[],[43,2])).
% 116.74/116.80 cnf(46,plain,
% 116.74/116.80 (E(f4(f3(a7)),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.80 inference(scs_inference,[],[43,42,2,3])).
% 116.74/116.80 cnf(47,plain,
% 116.74/116.80 (E(f5(f3(f3(a6)),f3(a6)),f4(f3(a7)))),
% 116.74/116.80 inference(scs_inference,[],[46,2])).
% 116.74/116.80 cnf(48,plain,
% 116.74/116.80 (E(f5(f3(f3(a6)),f3(a6)),f3(a7))),
% 116.74/116.80 inference(scs_inference,[],[46,40,14,2,3])).
% 116.74/116.80 cnf(49,plain,
% 116.74/116.80 (E(f3(a7),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.80 inference(scs_inference,[],[48,2])).
% 116.74/116.80 cnf(50,plain,
% 116.74/116.80 (E(f3(a6),f4(f3(a7)))),
% 116.74/116.80 inference(scs_inference,[],[48,45,38,2,3])).
% 116.74/116.80 cnf(51,plain,
% 116.74/116.80 (E(f4(f3(a7)),f3(a6))),
% 116.74/116.80 inference(scs_inference,[],[50,2])).
% 116.74/116.80 cnf(52,plain,
% 116.74/116.80 (E(f3(a7),f4(f3(a7)))),
% 116.74/116.80 inference(scs_inference,[],[47,50,49,2,3])).
% 116.74/116.80 cnf(53,plain,
% 116.74/116.80 (E(x531,f5(x531,f4(x531)))),
% 116.74/116.80 inference(scs_inference,[],[11,2])).
% 116.74/116.80 cnf(54,plain,
% 116.74/116.80 (E(f3(a7),f3(a6))),
% 116.74/116.80 inference(scs_inference,[],[52,51,11,2,3])).
% 116.74/116.80 cnf(55,plain,
% 116.74/116.80 (E(f3(a6),f3(a7))),
% 116.74/116.80 inference(scs_inference,[],[54,2])).
% 116.74/116.80 cnf(56,plain,
% 116.74/116.80 (E(x561,f5(f3(x561),x561))),
% 116.74/116.80 inference(scs_inference,[],[12,2])).
% 116.74/116.80 cnf(57,plain,
% 116.74/116.80 (E(f3(x571),f4(f3(x571)))),
% 116.74/116.80 inference(scs_inference,[],[10,2])).
% 116.74/116.80 cnf(58,plain,
% 116.74/116.80 (E(f3(x581),f3(f4(f3(x581))))),
% 116.74/116.80 inference(scs_inference,[],[28,57,3])).
% 116.74/116.80 cnf(60,plain,
% 116.74/116.80 (E(f3(f4(f3(x601))),f3(x601))),
% 116.74/116.80 inference(scs_inference,[],[28,57,3,2])).
% 116.74/116.80 cnf(61,plain,
% 116.74/116.80 (E(f3(f4(f3(a6))),f3(a7))),
% 116.74/116.80 inference(scs_inference,[],[60,55,3])).
% 116.74/116.80 cnf(67,plain,
% 116.74/116.80 (E(f3(f4(a2)),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[8,4,2])).
% 116.74/116.80 cnf(68,plain,
% 116.74/116.80 (E(f3(f3(a1)),f3(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[67,2])).
% 116.74/116.80 cnf(69,plain,
% 116.74/116.80 (E(f3(a1),f3(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[8,28,67,2,3])).
% 116.74/116.80 cnf(72,plain,
% 116.74/116.80 (E(f3(f4(a2)),f3(a1))),
% 116.74/116.80 inference(scs_inference,[],[69,2])).
% 116.74/116.80 cnf(73,plain,
% 116.74/116.80 (E(f3(a1),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[69,67,2,3])).
% 116.74/116.80 cnf(75,plain,
% 116.74/116.80 (E(f3(f3(a1)),f3(a1))),
% 116.74/116.80 inference(scs_inference,[],[73,2])).
% 116.74/116.80 cnf(76,plain,
% 116.74/116.80 (E(f4(f5(a2,a1)),f4(a1))),
% 116.74/116.80 inference(scs_inference,[],[8,18,2])).
% 116.74/116.80 cnf(77,plain,
% 116.74/116.80 (E(f4(a1),f4(f5(a2,a1)))),
% 116.74/116.80 inference(scs_inference,[],[76,2])).
% 116.74/116.80 cnf(78,plain,
% 116.74/116.80 (E(f3(f3(a1)),f4(a2))),
% 116.74/116.80 inference(scs_inference,[],[8,75,76,2,3])).
% 116.74/116.80 cnf(80,plain,
% 116.74/116.80 (E(f4(a2),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[78,2])).
% 116.74/116.80 cnf(81,plain,
% 116.74/116.80 (E(f4(a1),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.80 inference(scs_inference,[],[78,77,42,2,3])).
% 116.74/116.80 cnf(82,plain,
% 116.74/116.80 (E(f4(f4(a2)),f4(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[8,2,5])).
% 116.74/116.80 cnf(84,plain,
% 116.74/116.80 (E(f3(a7),f4(a1))),
% 116.74/116.80 inference(scs_inference,[],[81,39,76,2,3])).
% 116.74/116.80 cnf(85,plain,
% 116.74/116.80 (E(f5(f4(a2),x851),f5(f3(a1),x851))),
% 116.74/116.80 inference(scs_inference,[],[8,2,6])).
% 116.74/116.80 cnf(86,plain,
% 116.74/116.80 (E(f4(a1),f3(a7))),
% 116.74/116.80 inference(scs_inference,[],[84,2])).
% 116.74/116.80 cnf(87,plain,
% 116.74/116.80 (E(f3(f4(f3(a6))),f4(a1))),
% 116.74/116.80 inference(scs_inference,[],[61,84,2,3])).
% 116.74/116.80 cnf(88,plain,
% 116.74/116.80 (E(f5(x881,f4(a2)),f5(x881,f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[8,2,7])).
% 116.74/116.80 cnf(89,plain,
% 116.74/116.80 (E(f5(x891,f3(a1)),f5(x891,f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[88,2])).
% 116.74/116.80 cnf(91,plain,
% 116.74/116.80 (E(f3(f5(a2,a1)),f3(a2))),
% 116.74/116.80 inference(scs_inference,[],[8,2,17])).
% 116.74/116.80 cnf(92,plain,
% 116.74/116.80 (E(f4(f3(a1)),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[82,2])).
% 116.74/116.80 cnf(93,plain,
% 116.74/116.80 (E(f3(a1),f5(f3(f3(a1)),f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[56,89,82,2,3])).
% 116.74/116.80 cnf(97,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f3(a1))),
% 116.74/116.80 inference(scs_inference,[],[93,2])).
% 116.74/116.80 cnf(98,plain,
% 116.74/116.80 (E(f3(a6),f4(a1))),
% 116.74/116.80 inference(scs_inference,[],[58,87,93,2,3])).
% 116.74/116.80 cnf(101,plain,
% 116.74/116.80 (E(f4(a1),f3(a6))),
% 116.74/116.80 inference(scs_inference,[],[98,2])).
% 116.74/116.80 cnf(102,plain,
% 116.74/116.80 (E(f3(a1),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[98,92,57,2,3])).
% 116.74/116.80 cnf(105,plain,
% 116.74/116.80 (E(f4(f4(a2)),f3(a1))),
% 116.74/116.80 inference(scs_inference,[],[102,2])).
% 116.74/116.80 cnf(106,plain,
% 116.74/116.80 (E(f3(f4(a2)),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[72,102,2,3])).
% 116.74/116.80 cnf(107,plain,
% 116.74/116.80 (E(f5(f5(a2,a1),a6),f5(a2,f5(a1,a6)))),
% 116.74/116.80 inference(scs_inference,[],[8,101,2,21])).
% 116.74/116.80 cnf(109,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f4(a2))),
% 116.74/116.80 inference(scs_inference,[],[8,106,97,2,3])).
% 116.74/116.80 cnf(112,plain,
% 116.74/116.80 (E(f4(f4(a2)),f4(a2))),
% 116.74/116.80 inference(scs_inference,[],[8,109,105,2,3])).
% 116.74/116.80 cnf(114,plain,
% 116.74/116.80 (E(f4(a2),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[112,2])).
% 116.74/116.80 cnf(115,plain,
% 116.74/116.80 (E(f4(a1),f4(f3(a7)))),
% 116.74/116.80 inference(scs_inference,[],[112,45,77,2,3])).
% 116.74/116.80 cnf(117,plain,
% 116.74/116.80 (E(f4(f3(a7)),f4(a1))),
% 116.74/116.80 inference(scs_inference,[],[115,2])).
% 116.74/116.80 cnf(118,plain,
% 116.74/116.80 (E(f4(a2),f4(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[115,114,82,2,3])).
% 116.74/116.80 cnf(120,plain,
% 116.74/116.80 (E(f4(f3(a1)),f4(a2))),
% 116.74/116.80 inference(scs_inference,[],[118,2])).
% 116.74/116.80 cnf(121,plain,
% 116.74/116.80 (E(f3(f3(a1)),f5(f3(f3(a1)),f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[118,75,93,2,3])).
% 116.74/116.80 cnf(123,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[121,2])).
% 116.74/116.80 cnf(124,plain,
% 116.74/116.80 (E(f3(f3(a1)),f5(f3(f3(a1)),f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[121,88,2,3])).
% 116.74/116.80 cnf(127,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f3(a1)),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[124,2])).
% 116.74/116.80 cnf(128,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f3(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[124,123,68,2,3])).
% 116.74/116.80 cnf(130,plain,
% 116.74/116.80 (E(f3(f4(a2)),f5(f3(f3(a1)),f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[128,2])).
% 116.74/116.80 cnf(131,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f3(a1)),f4(a2))),
% 116.74/116.80 inference(scs_inference,[],[128,127,78,2,3])).
% 116.74/116.80 cnf(134,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[131,128,106,2,3])).
% 116.74/116.80 cnf(135,plain,
% 116.74/116.80 (E(f4(f4(a2)),f5(f3(f3(a1)),f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[134,2])).
% 116.74/116.80 cnf(136,plain,
% 116.74/116.80 (E(f5(f3(f3(a1)),f4(a2)),f4(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[134,82,2,3])).
% 116.74/116.80 cnf(139,plain,
% 116.74/116.80 (E(f3(f4(a2)),f4(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[136,130,2,3])).
% 116.74/116.80 cnf(141,plain,
% 116.74/116.80 (E(f4(f3(a1)),f3(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[139,2])).
% 116.74/116.80 cnf(142,plain,
% 116.74/116.80 (E(f3(f3(a1)),f4(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[139,68,2,3])).
% 116.74/116.80 cnf(144,plain,
% 116.74/116.80 (E(f4(f3(a1)),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[142,2])).
% 116.74/116.80 cnf(145,plain,
% 116.74/116.80 (E(f3(f3(a1)),f4(f4(a2)))),
% 116.74/116.80 inference(scs_inference,[],[142,92,2,3])).
% 116.74/116.80 cnf(147,plain,
% 116.74/116.80 (E(f4(f4(a2)),f3(f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[145,2])).
% 116.74/116.80 cnf(148,plain,
% 116.74/116.80 (E(f4(f3(a1)),f5(f3(f3(a1)),f3(a1)))),
% 116.74/116.80 inference(scs_inference,[],[144,145,124,2,3])).
% 116.74/116.81 cnf(150,plain,
% 116.74/116.81 (E(f5(f3(f3(a1)),f3(a1)),f4(f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[148,2])).
% 116.74/116.81 cnf(151,plain,
% 116.74/116.81 (E(f4(f4(a2)),f5(f3(f3(a1)),f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[148,147,124,2,3])).
% 116.74/116.81 cnf(153,plain,
% 116.74/116.81 (E(f5(f3(f3(a1)),f3(a1)),f4(f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[151,2])).
% 116.74/116.81 cnf(154,plain,
% 116.74/116.81 (E(f5(f3(f3(a1)),f3(a1)),f3(f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[151,150,141,2,3])).
% 116.74/116.81 cnf(156,plain,
% 116.74/116.81 (E(f5(f5(a2,a1),a7),f5(a2,f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[154,107,15,2,3])).
% 116.74/116.81 cnf(158,plain,
% 116.74/116.81 (E(f5(a2,f5(a1,a6)),f5(f5(a2,a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[156,2])).
% 116.74/116.81 cnf(171,plain,
% 116.74/116.81 (E(f3(a2),f3(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[91,2])).
% 116.74/116.81 cnf(173,plain,
% 116.74/116.81 (E(f5(a2,f5(a1,a6)),f5(f5(a2,a1),a6))),
% 116.74/116.81 inference(scs_inference,[],[107,2])).
% 116.74/116.81 cnf(175,plain,
% 116.74/116.81 (E(f5(f3(a1),x1751),f5(f4(a2),x1751))),
% 116.74/116.81 inference(scs_inference,[],[85,2])).
% 116.74/116.81 cnf(176,plain,
% 116.74/116.81 (E(f4(a2),f5(f4(a2),f4(f3(a1))))),
% 116.74/116.81 inference(scs_inference,[],[25,85,2,3])).
% 116.74/116.81 cnf(179,plain,
% 116.74/116.81 (E(a1,f5(f4(a2),a1))),
% 116.74/116.81 inference(scs_inference,[],[175,176,56,2,3])).
% 116.74/116.81 cnf(182,plain,
% 116.74/116.81 (E(f5(f4(a2),a1),a1)),
% 116.74/116.81 inference(scs_inference,[],[179,2])).
% 116.74/116.81 cnf(192,plain,
% 116.74/116.81 (E(f3(f4(a1)),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[9,81,3])).
% 116.74/116.81 cnf(194,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a6)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[9,81,3,2])).
% 116.74/116.81 cnf(196,plain,
% 116.74/116.81 (E(f3(f4(a1)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[192,47,3])).
% 116.74/116.81 cnf(197,plain,
% 116.74/116.81 (E(f4(f3(a7)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[192,47,3,2])).
% 116.74/116.81 cnf(199,plain,
% 116.74/116.81 (E(f3(a7),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[194,49,3])).
% 116.74/116.81 cnf(200,plain,
% 116.74/116.81 (E(f3(f4(a1)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[194,49,3,2])).
% 116.74/116.81 cnf(202,plain,
% 116.74/116.81 (E(f3(f4(a1)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[200,54,3])).
% 116.74/116.81 cnf(203,plain,
% 116.74/116.81 (E(f3(a6),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[200,54,3,2])).
% 116.74/116.81 cnf(236,plain,
% 116.74/116.81 (E(f4(f3(a6)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[10,203,3])).
% 116.74/116.81 cnf(240,plain,
% 116.74/116.81 (E(f4(f3(a6)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[10,55,3])).
% 116.74/116.81 cnf(242,plain,
% 116.74/116.81 (E(f3(a7),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[10,55,3,2])).
% 116.74/116.81 cnf(244,plain,
% 116.74/116.81 (E(f4(f3(a7)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[10,242,3])).
% 116.74/116.81 cnf(246,plain,
% 116.74/116.81 (E(f4(f3(a6)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[10,242,3,2])).
% 116.74/116.81 cnf(255,plain,
% 116.74/116.81 (E(f4(f3(a6)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[10,98,3])).
% 116.74/116.81 cnf(257,plain,
% 116.74/116.81 (E(f4(a1),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[10,98,3,2])).
% 116.74/116.81 cnf(267,plain,
% 116.74/116.81 (E(f4(f3(a6)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[10,38,3])).
% 116.74/116.81 cnf(269,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[10,38,3,2])).
% 116.74/116.81 cnf(280,plain,
% 116.74/116.81 (~E(a6,f5(f3(a7),a7))),
% 116.74/116.81 inference(scs_inference,[],[16,12,2,3])).
% 116.74/116.81 cnf(284,plain,
% 116.74/116.81 (E(f3(x2841),f3(f5(x2841,f4(x2841))))),
% 116.74/116.81 inference(scs_inference,[],[11,2,4])).
% 116.74/116.81 cnf(286,plain,
% 116.74/116.81 (E(f5(f4(a1),f4(f4(a1))),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[11,284,101,2,3])).
% 116.74/116.81 cnf(288,plain,
% 116.74/116.81 (E(f4(x2881),f4(f5(x2881,f4(x2881))))),
% 116.74/116.81 inference(scs_inference,[],[11,2,5])).
% 116.74/116.81 cnf(290,plain,
% 116.74/116.81 (E(f5(a1,f4(a1)),f5(f4(a2),a1))),
% 116.74/116.81 inference(scs_inference,[],[11,286,179,2,3])).
% 116.74/116.81 cnf(292,plain,
% 116.74/116.81 (E(f5(x2921,x2922),f5(f5(x2921,f4(x2921)),x2922))),
% 116.74/116.81 inference(scs_inference,[],[11,2,6])).
% 116.74/116.81 cnf(293,plain,
% 116.74/116.81 (E(f5(f5(x2931,f4(x2931)),x2932),f5(x2931,x2932))),
% 116.74/116.81 inference(scs_inference,[],[292,2])).
% 116.74/116.81 cnf(294,plain,
% 116.74/116.81 (E(f5(f4(a2),f4(f4(a2))),f3(a1))),
% 116.74/116.81 inference(scs_inference,[],[11,292,22,2,3])).
% 116.74/116.81 cnf(296,plain,
% 116.74/116.81 (E(f5(x2961,x2962),f5(x2961,f5(x2962,f4(x2962))))),
% 116.74/116.81 inference(scs_inference,[],[11,2,7])).
% 116.74/116.81 cnf(297,plain,
% 116.74/116.81 (E(f5(f4(a2),a1),f5(a1,f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[290,2])).
% 116.74/116.81 cnf(298,plain,
% 116.74/116.81 (~E(a7,f5(f5(a6,f4(a6)),f4(a6)))),
% 116.74/116.81 inference(scs_inference,[],[293,290,35,2,3])).
% 116.74/116.81 cnf(302,plain,
% 116.74/116.81 (E(f5(f3(a6),f4(f3(a6))),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[11,294,55,2,3])).
% 116.74/116.81 cnf(305,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(a6),f4(f3(a6))))),
% 116.74/116.81 inference(scs_inference,[],[302,2])).
% 116.74/116.81 cnf(323,plain,
% 116.74/116.81 (E(f4(f5(x3231,f4(x3231))),f4(x3231))),
% 116.74/116.81 inference(scs_inference,[],[288,2])).
% 116.74/116.81 cnf(325,plain,
% 116.74/116.81 (E(f5(x3251,f5(x3252,f4(x3252))),f5(x3251,x3252))),
% 116.74/116.81 inference(scs_inference,[],[296,2])).
% 116.74/116.81 cnf(326,plain,
% 116.74/116.81 (~E(a7,f5(f3(a6),f5(a6,f4(a6))))),
% 116.74/116.81 inference(scs_inference,[],[296,26,2,3])).
% 116.74/116.81 cnf(328,plain,
% 116.74/116.81 (~E(a6,a7)),
% 116.74/116.81 inference(scs_inference,[],[56,280,3])).
% 116.74/116.81 cnf(331,plain,
% 116.74/116.81 (E(f3(x3311),f3(f5(f3(x3311),x3311)))),
% 116.74/116.81 inference(scs_inference,[],[12,2,4])).
% 116.74/116.81 cnf(333,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,331,199,2,3])).
% 116.74/116.81 cnf(335,plain,
% 116.74/116.81 (E(f5(x3351,x3352),f5(f5(f3(x3351),x3351),x3352))),
% 116.74/116.81 inference(scs_inference,[],[12,2,6])).
% 116.74/116.81 cnf(336,plain,
% 116.74/116.81 (E(f3(f4(a1)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[333,2])).
% 116.74/116.81 cnf(337,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[12,257,333,2,3])).
% 116.74/116.81 cnf(339,plain,
% 116.74/116.81 (E(f5(x3391,x3392),f5(x3391,f5(f3(x3392),x3392)))),
% 116.74/116.81 inference(scs_inference,[],[12,2,7])).
% 116.74/116.81 cnf(340,plain,
% 116.74/116.81 (E(f5(x3401,f5(f3(x3402),x3402)),f5(x3401,x3402))),
% 116.74/116.81 inference(scs_inference,[],[339,2])).
% 116.74/116.81 cnf(341,plain,
% 116.74/116.81 (E(f5(f3(f4(a2)),f4(a2)),f4(f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[12,339,114,2,3])).
% 116.74/116.81 cnf(344,plain,
% 116.74/116.81 (E(f4(f4(a2)),f5(f3(f4(a2)),f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[341,2])).
% 116.74/116.81 cnf(345,plain,
% 116.74/116.81 (E(f5(f3(f4(a2)),f4(a2)),f4(f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,341,118,2,3])).
% 116.74/116.81 cnf(348,plain,
% 116.74/116.81 (E(f4(f3(a1)),f5(f3(f4(a2)),f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[345,2])).
% 116.74/116.81 cnf(349,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[12,345,115,2,3])).
% 116.74/116.81 cnf(352,plain,
% 116.74/116.81 (E(f4(f3(a7)),f5(f3(f4(a1)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[349,2])).
% 116.74/116.81 cnf(353,plain,
% 116.74/116.81 (E(f5(f3(f3(a2)),f3(a2)),f3(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,349,171,2,3])).
% 116.74/116.81 cnf(357,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[12,353,242,2,3])).
% 116.74/116.81 cnf(360,plain,
% 116.74/116.81 (E(f4(f3(a6)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[357,2])).
% 116.74/116.81 cnf(361,plain,
% 116.74/116.81 (E(f5(f3(f4(x3611)),f4(x3611)),f3(f4(x3611)))),
% 116.74/116.81 inference(scs_inference,[],[12,357,28,2,3])).
% 116.74/116.81 cnf(364,plain,
% 116.74/116.81 (E(f3(f4(x3641)),f5(f3(f4(x3641)),f4(x3641)))),
% 116.74/116.81 inference(scs_inference,[],[361,2])).
% 116.74/116.81 cnf(365,plain,
% 116.74/116.81 (E(f5(f3(f3(x3651)),f3(x3651)),f4(f3(x3651)))),
% 116.74/116.81 inference(scs_inference,[],[12,361,57,2,3])).
% 116.74/116.81 cnf(368,plain,
% 116.74/116.81 (E(f4(f3(x3681)),f5(f3(f3(x3681)),f3(x3681)))),
% 116.74/116.81 inference(scs_inference,[],[365,2])).
% 116.74/116.81 cnf(369,plain,
% 116.74/116.81 (E(f5(f3(f4(a2)),f4(a2)),f3(f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,365,80,2,3])).
% 116.74/116.81 cnf(372,plain,
% 116.74/116.81 (E(f4(f3(a6)),f5(f3(f4(a1)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[337,2])).
% 116.74/116.81 cnf(373,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,337,39,2,3])).
% 116.74/116.81 cnf(377,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[12,369,101,2,3])).
% 116.74/116.81 cnf(380,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[373,2])).
% 116.74/116.81 cnf(381,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[12,373,77,2,3])).
% 116.74/116.81 cnf(385,plain,
% 116.74/116.81 (E(f5(f3(f4(a2)),f4(a2)),f3(a1))),
% 116.74/116.81 inference(scs_inference,[],[12,381,22,2,3])).
% 116.74/116.81 cnf(388,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f4(a1)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[377,2])).
% 116.74/116.81 cnf(389,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[12,377,54,2,3])).
% 116.74/116.81 cnf(393,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[12,385,86,2,3])).
% 116.74/116.81 cnf(396,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[389,2])).
% 116.74/116.81 cnf(397,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[12,389,84,2,3])).
% 116.74/116.81 cnf(400,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f4(a1)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[393,2])).
% 116.74/116.81 cnf(402,plain,
% 116.74/116.81 (E(f4(a1),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[397,2])).
% 116.74/116.81 cnf(404,plain,
% 116.74/116.81 (E(f5(f5(f3(x4041),x4041),x4042),f5(x4041,x4042))),
% 116.74/116.81 inference(scs_inference,[],[335,2])).
% 116.74/116.81 cnf(409,plain,
% 116.74/116.81 (E(f5(f4(a2),f5(a1,f4(a1))),a1)),
% 116.74/116.81 inference(scs_inference,[],[325,182,3])).
% 116.74/116.81 cnf(413,plain,
% 116.74/116.81 (E(f5(f4(a2),f5(f3(a1),a1)),a1)),
% 116.74/116.81 inference(scs_inference,[],[340,409,182,2,3])).
% 116.74/116.81 cnf(417,plain,
% 116.74/116.81 (E(f5(f5(f3(a2),a2),f5(a1,a6)),f5(f5(a2,a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[404,158,413,2,3])).
% 116.74/116.81 cnf(420,plain,
% 116.74/116.81 (E(f5(f5(a2,a1),a7),f5(f5(f3(a2),a2),f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[417,2])).
% 116.74/116.81 cnf(421,plain,
% 116.74/116.81 (E(f5(f5(a2,f4(a2)),f5(a1,a6)),f5(f5(a2,a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[417,293,158,2,3])).
% 116.74/116.81 cnf(424,plain,
% 116.74/116.81 (E(f5(f5(a2,a1),a7),f5(f5(a2,f4(a2)),f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[421,2])).
% 116.74/116.81 cnf(425,plain,
% 116.74/116.81 (E(f4(f5(a1,f4(a1))),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[323,421,101,2,3])).
% 116.74/116.81 cnf(428,plain,
% 116.74/116.81 (E(f3(a6),f4(f5(a1,f4(a1))))),
% 116.74/116.81 inference(scs_inference,[],[425,2])).
% 116.74/116.81 cnf(445,plain,
% 116.74/116.81 (~E(a6,f5(a7,f4(a7)))),
% 116.74/116.81 inference(scs_inference,[],[16,11,2,3])).
% 116.74/116.81 cnf(465,plain,
% 116.74/116.81 (~E(a7,f5(f3(a6),f5(f3(a6),a6)))),
% 116.74/116.81 inference(scs_inference,[],[26,340,3])).
% 116.74/116.81 cnf(478,plain,
% 116.74/116.81 (E(f5(f5(a2,a1),a6),f5(f5(f3(a2),a2),f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[37,420,3])).
% 116.74/116.81 cnf(481,plain,
% 116.74/116.81 (E(f5(f5(a2,a1),a6),f5(f5(a2,f4(a2)),f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[37,424,3])).
% 116.74/116.81 cnf(497,plain,
% 116.74/116.81 (E(a2,f5(a2,f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[53,88,3])).
% 116.74/116.81 cnf(507,plain,
% 116.74/116.81 (E(f5(x5071,f3(a6)),f5(x5071,f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[54,2,7])).
% 116.74/116.81 cnf(508,plain,
% 116.74/116.81 (E(f5(x5081,f3(a7)),f5(x5081,f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[507,2])).
% 116.74/116.81 cnf(509,plain,
% 116.74/116.81 (E(f3(a7),f4(f5(a1,f4(a1))))),
% 116.74/116.81 inference(scs_inference,[],[54,428,507,2,3])).
% 116.74/116.81 cnf(510,plain,
% 116.74/116.81 (E(f3(f3(a6)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[54,2,4])).
% 116.74/116.81 cnf(512,plain,
% 116.74/116.81 (E(f4(f3(a6)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[360,508,509,2,3])).
% 116.74/116.81 cnf(514,plain,
% 116.74/116.81 (E(f5(f3(a6),x5141),f5(f3(a7),x5141))),
% 116.74/116.81 inference(scs_inference,[],[54,2,6])).
% 116.74/116.81 cnf(515,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[512,2])).
% 116.74/116.81 cnf(516,plain,
% 116.74/116.81 (E(f4(f3(a7)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[244,512,2,3])).
% 116.74/116.81 cnf(518,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[516,2])).
% 116.74/116.81 cnf(519,plain,
% 116.74/116.81 (E(f3(a7),f3(f5(a6,f4(a6))))),
% 116.74/116.81 inference(scs_inference,[],[54,516,284,2,3])).
% 116.74/116.81 cnf(522,plain,
% 116.74/116.81 (E(f3(f3(a7)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[510,2])).
% 116.74/116.81 cnf(523,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[510,518,117,2,3])).
% 116.74/116.81 cnf(524,plain,
% 116.74/116.81 (E(f4(a7),f4(f5(f3(a6),a7)))),
% 116.74/116.81 inference(scs_inference,[],[240,2,18])).
% 116.74/116.81 cnf(525,plain,
% 116.74/116.81 (E(f3(f5(a6,f4(a6))),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[519,2])).
% 116.74/116.81 cnf(526,plain,
% 116.74/116.81 (E(f3(a7),f3(f5(f3(a6),a6)))),
% 116.74/116.81 inference(scs_inference,[],[54,519,331,2,3])).
% 116.74/116.81 cnf(529,plain,
% 116.74/116.81 (E(f3(f5(f3(a6),a6)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[526,2])).
% 116.74/116.81 cnf(530,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[269,526,512,2,3])).
% 116.74/116.81 cnf(532,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[530,2])).
% 116.74/116.81 cnf(533,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[530,515,236,2,3])).
% 116.74/116.81 cnf(535,plain,
% 116.74/116.81 (E(f3(f4(a1)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[533,2])).
% 116.74/116.81 cnf(536,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[533,200,2,3])).
% 116.74/116.81 cnf(538,plain,
% 116.74/116.81 (E(f4(a1),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[523,2])).
% 116.74/116.81 cnf(539,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[54,523,536,2,3])).
% 116.74/116.81 cnf(541,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[539,2])).
% 116.74/116.81 cnf(542,plain,
% 116.74/116.81 (E(f3(f5(a6,f4(a6))),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[539,525,84,2,3])).
% 116.74/116.81 cnf(545,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[54,542,541,2,3])).
% 116.74/116.81 cnf(548,plain,
% 116.74/116.81 (E(f3(f5(f3(a6),a6)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[529,524,84,2,3])).
% 116.74/116.81 cnf(551,plain,
% 116.74/116.81 (~E(a6,f5(f3(a6),a7))),
% 116.74/116.81 inference(scs_inference,[],[548,514,280,2,3])).
% 116.74/116.81 cnf(554,plain,
% 116.74/116.81 (E(f5(f3(a7),x5541),f5(f3(a6),x5541))),
% 116.74/116.81 inference(scs_inference,[],[514,2])).
% 116.74/116.81 cnf(555,plain,
% 116.74/116.81 (E(f4(f3(a6)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[368,507,514,2,3])).
% 116.74/116.81 cnf(559,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[555,2])).
% 116.74/116.81 cnf(560,plain,
% 116.74/116.81 (~E(a7,f5(f3(a7),f5(a6,f4(a6))))),
% 116.74/116.81 inference(scs_inference,[],[555,554,326,2,3])).
% 116.74/116.81 cnf(563,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[255,559,3])).
% 116.74/116.81 cnf(566,plain,
% 116.74/116.81 (~E(a7,f5(f3(a7),f5(f3(a6),a6)))),
% 116.74/116.81 inference(scs_inference,[],[554,465,3])).
% 116.74/116.81 cnf(569,plain,
% 116.74/116.81 (~E(a7,f5(f3(a7),a6))),
% 116.74/116.81 inference(scs_inference,[],[339,566,3])).
% 116.74/116.81 cnf(572,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[563,115,3])).
% 116.74/116.81 cnf(573,plain,
% 116.74/116.81 (E(f4(f3(a7)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[563,115,3,2])).
% 116.74/116.81 cnf(575,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[572,197,3])).
% 116.74/116.81 cnf(576,plain,
% 116.74/116.81 (E(f3(f4(a1)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[572,197,3,2])).
% 116.74/116.81 cnf(579,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[575,202,3,2])).
% 116.74/116.81 cnf(581,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[54,579,3])).
% 116.74/116.81 cnf(582,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[54,579,3,2])).
% 116.74/116.81 cnf(584,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[582,39,3])).
% 116.74/116.81 cnf(585,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[582,39,3,2])).
% 116.74/116.81 cnf(626,plain,
% 116.74/116.81 (E(f4(f4(a1)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[84,2,5])).
% 116.74/116.81 cnf(627,plain,
% 116.74/116.81 (E(f4(f3(a7)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[626,2])).
% 116.74/116.81 cnf(628,plain,
% 116.74/116.81 (E(f5(f4(a1),x6281),f5(f3(a7),x6281))),
% 116.74/116.81 inference(scs_inference,[],[84,2,6])).
% 116.74/116.81 cnf(629,plain,
% 116.74/116.81 (E(f5(f3(a7),x6291),f5(f4(a1),x6291))),
% 116.74/116.81 inference(scs_inference,[],[628,2])).
% 116.74/116.81 cnf(632,plain,
% 116.74/116.81 (E(f5(x6321,f4(a1)),f5(x6321,f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[84,2,7])).
% 116.74/116.81 cnf(633,plain,
% 116.74/116.81 (E(f5(x6331,f3(a7)),f5(x6331,f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[632,2])).
% 116.74/116.81 cnf(634,plain,
% 116.74/116.81 (~E(a7,f5(f4(a1),f5(a6,f4(a6))))),
% 116.74/116.81 inference(scs_inference,[],[628,560,632,2,3])).
% 116.74/116.81 cnf(636,plain,
% 116.74/116.81 (E(f3(f4(a1)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[84,2,4])).
% 116.74/116.81 cnf(637,plain,
% 116.74/116.81 (E(f3(f3(a7)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[636,2])).
% 116.74/116.81 cnf(638,plain,
% 116.74/116.81 (E(f3(f4(a1)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[522,636,2,3])).
% 116.74/116.81 cnf(640,plain,
% 116.74/116.81 (E(f3(f3(a6)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[638,2])).
% 116.74/116.81 cnf(641,plain,
% 116.74/116.81 (E(f3(f3(a7)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[336,638,637,2,3])).
% 116.74/116.81 cnf(643,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[641,2])).
% 116.74/116.81 cnf(644,plain,
% 116.74/116.81 (E(f3(f3(a6)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[535,641,640,2,3])).
% 116.74/116.81 cnf(645,plain,
% 116.74/116.81 (E(f3(f5(a1,a7)),f3(a1))),
% 116.74/116.81 inference(scs_inference,[],[84,2,17])).
% 116.74/116.81 cnf(646,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[644,2])).
% 116.74/116.81 cnf(647,plain,
% 116.74/116.81 (E(f3(f3(a7)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[644,522,2,3])).
% 116.74/116.81 cnf(649,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[647,2])).
% 116.74/116.81 cnf(650,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[380,647,633,2,3])).
% 116.74/116.81 cnf(653,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f4(a1)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[650,2])).
% 116.74/116.81 cnf(654,plain,
% 116.74/116.81 (E(f4(f3(a6)),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[267,650,2,3])).
% 116.74/116.81 cnf(656,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f4(a1)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[654,2])).
% 116.74/116.81 cnf(657,plain,
% 116.74/116.81 (E(f3(a6),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[396,654,643,2,3])).
% 116.74/116.81 cnf(659,plain,
% 116.74/116.81 (E(f3(f3(a7)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[657,2])).
% 116.74/116.81 cnf(660,plain,
% 116.74/116.81 (E(f3(a7),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[545,646,657,2,3])).
% 116.74/116.81 cnf(662,plain,
% 116.74/116.81 (E(f3(f3(a6)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[660,2])).
% 116.74/116.81 cnf(663,plain,
% 116.74/116.81 (E(f4(a1),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[538,649,660,2,3])).
% 116.74/116.81 cnf(666,plain,
% 116.74/116.81 (E(f3(f3(a6)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[84,663,662,2,3])).
% 116.74/116.81 cnf(669,plain,
% 116.74/116.81 (E(f3(f3(a6)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[666,659,510,2,3])).
% 116.74/116.81 cnf(671,plain,
% 116.74/116.81 (E(f3(a6),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[669,2])).
% 116.74/116.81 cnf(672,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f4(a1)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[656,669,255,2,3])).
% 116.74/116.81 cnf(674,plain,
% 116.74/116.81 (E(f4(a1),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[672,2])).
% 116.74/116.81 cnf(675,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a6)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[672,194,638,2,3])).
% 116.74/116.81 cnf(677,plain,
% 116.74/116.81 (E(f3(f3(a6)),f5(f3(f3(a6)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[675,2])).
% 116.74/116.81 cnf(678,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[84,675,674,2,3])).
% 116.74/116.81 cnf(680,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f4(a1)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[678,2])).
% 116.74/116.81 cnf(681,plain,
% 116.74/116.81 (E(f3(a7),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[84,678,663,2,3])).
% 116.74/116.81 cnf(683,plain,
% 116.74/116.81 (E(f3(f3(a7)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[681,2])).
% 116.74/116.81 cnf(684,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f4(a1)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[681,680,2,3])).
% 116.74/116.81 cnf(685,plain,
% 116.74/116.81 (E(f3(f3(a7)),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[684,2])).
% 116.74/116.81 cnf(686,plain,
% 116.74/116.81 (E(f3(f3(a7)),f5(f3(f4(a1)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[400,684,683,2,3])).
% 116.74/116.81 cnf(688,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[686,2])).
% 116.74/116.81 cnf(689,plain,
% 116.74/116.81 (E(f3(f3(a7)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[686,685,653,2,3])).
% 116.74/116.81 cnf(692,plain,
% 116.74/116.81 (E(f4(f3(a7)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[352,688,689,2,3])).
% 116.74/116.81 cnf(694,plain,
% 116.74/116.81 (E(f3(f3(a7)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[692,2])).
% 116.74/116.81 cnf(695,plain,
% 116.74/116.81 (E(f5(a1,f3(a7)),f5(f4(a2),a1))),
% 116.74/116.81 inference(scs_inference,[],[692,290,633,2,3])).
% 116.74/116.81 cnf(698,plain,
% 116.74/116.81 (E(f5(f4(a2),a1),f5(a1,f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[695,2])).
% 116.74/116.81 cnf(699,plain,
% 116.74/116.81 (E(f3(f3(a7)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[573,695,694,2,3])).
% 116.74/116.81 cnf(701,plain,
% 116.74/116.81 (E(f4(f3(a6)),f3(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[699,654,684,2,3])).
% 116.74/116.81 cnf(703,plain,
% 116.74/116.81 (E(f3(f3(a7)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[701,2])).
% 116.74/116.81 cnf(704,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[701,530,646,2,3])).
% 116.74/116.81 cnf(706,plain,
% 116.74/116.81 (E(f3(f3(a6)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[704,2])).
% 116.74/116.81 cnf(707,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f3(a7)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[584,704,2,3])).
% 116.74/116.81 cnf(710,plain,
% 116.74/116.81 (E(f5(a1,f3(a7)),a1)),
% 116.74/116.81 inference(scs_inference,[],[707,695,182,2,3])).
% 116.74/116.81 cnf(712,plain,
% 116.74/116.81 (E(a1,f5(a1,f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[710,2])).
% 116.74/116.81 cnf(713,plain,
% 116.74/116.81 (E(f5(f3(a1),a1),f5(a1,f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[710,698,175,2,3])).
% 116.74/116.81 cnf(716,plain,
% 116.74/116.81 (E(f3(f3(a6)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[713,677,47,2,3])).
% 116.74/116.81 cnf(719,plain,
% 116.74/116.81 (E(f3(f3(a6)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[627,716,2,3])).
% 116.74/116.81 cnf(721,plain,
% 116.74/116.81 (E(f4(f4(a1)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[719,2])).
% 116.74/116.81 cnf(722,plain,
% 116.74/116.81 (E(f3(f4(a1)),f5(f3(f4(a1)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[364,719,632,2,3])).
% 116.74/116.81 cnf(726,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f3(a7)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[722,2])).
% 116.74/116.81 cnf(727,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f4(a1)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[722,199,2,3])).
% 116.74/116.81 cnf(729,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f3(a7)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[727,2])).
% 116.74/116.81 cnf(730,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f3(a7)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[727,726,196,2,3])).
% 116.74/116.81 cnf(732,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f3(a7)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[84,730,729,2,3])).
% 116.74/116.81 cnf(735,plain,
% 116.74/116.81 (E(f4(f4(a1)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[706,732,721,2,3])).
% 116.74/116.81 cnf(737,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[735,2])).
% 116.74/116.81 cnf(738,plain,
% 116.74/116.81 (E(f3(a6),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[735,671,719,2,3])).
% 116.74/116.81 cnf(740,plain,
% 116.74/116.81 (E(f4(f4(a1)),f3(a6))),
% 116.74/116.81 inference(scs_inference,[],[738,2])).
% 116.74/116.81 cnf(741,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a6)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[532,738,737,2,3])).
% 116.74/116.81 cnf(743,plain,
% 116.74/116.81 (E(f4(f4(a1)),f5(f3(f3(a7)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[741,2])).
% 116.74/116.81 cnf(744,plain,
% 116.74/116.81 (E(f3(f4(a1)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[741,535,2,3])).
% 116.74/116.81 cnf(745,plain,
% 116.74/116.81 (E(f4(f4(a1)),f3(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[744,2])).
% 116.74/116.81 cnf(746,plain,
% 116.74/116.81 (E(f4(f4(a1)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[743,744,536,2,3])).
% 116.74/116.81 cnf(749,plain,
% 116.74/116.81 (E(f4(f4(a1)),f5(f3(f3(a6)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[576,745,746,2,3])).
% 116.74/116.81 cnf(752,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f4(a1)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[749,203,722,2,3])).
% 116.74/116.81 cnf(755,plain,
% 116.74/116.81 (E(f5(f3(f3(a7)),f3(a7)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[752,333,744,2,3])).
% 116.74/116.81 cnf(757,plain,
% 116.74/116.81 (E(f4(f4(a1)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[755,2])).
% 116.74/116.81 cnf(758,plain,
% 116.74/116.81 (E(f4(a1),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[402,755,2,3])).
% 116.74/116.81 cnf(760,plain,
% 116.74/116.81 (E(f4(f4(a1)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[757,758,357,2,3])).
% 116.74/116.81 cnf(762,plain,
% 116.74/116.81 (E(f4(f3(a6)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[760,2])).
% 116.74/116.81 cnf(763,plain,
% 116.74/116.81 (E(f5(f3(f4(a1)),f4(a1)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[760,361,638,2,3])).
% 116.74/116.81 cnf(767,plain,
% 116.74/116.81 (E(f4(f3(a6)),f3(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[372,763,2,3])).
% 116.74/116.81 cnf(769,plain,
% 116.74/116.81 (E(f3(f3(a6)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[767,2])).
% 116.74/116.81 cnf(770,plain,
% 116.74/116.81 (E(f3(f3(a7)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[703,767,762,2,3])).
% 116.74/116.81 cnf(773,plain,
% 116.74/116.81 (E(f3(f3(a6)),f5(f3(f3(a7)),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[770,769,360,2,3])).
% 116.74/116.81 cnf(776,plain,
% 116.74/116.81 (E(f3(a7),f5(f3(f3(a6)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[581,773,633,2,3])).
% 116.74/116.81 cnf(779,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f3(a7))),
% 116.74/116.81 inference(scs_inference,[],[776,2])).
% 116.74/116.81 cnf(780,plain,
% 116.74/116.81 (E(f4(f5(a2,a1)),f5(f3(f3(a6)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[585,776,633,2,3])).
% 116.74/116.81 cnf(782,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f4(f5(a2,a1)))),
% 116.74/116.81 inference(scs_inference,[],[780,2])).
% 116.74/116.81 cnf(783,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f4(a1))),
% 116.74/116.81 inference(scs_inference,[],[84,780,779,2,3])).
% 116.74/116.81 cnf(785,plain,
% 116.74/116.81 (E(f4(a1),f5(f3(f3(a6)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[783,2])).
% 116.74/116.81 cnf(786,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f4(f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[783,782,269,2,3])).
% 116.74/116.81 cnf(789,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f4(f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[786,246,2,3])).
% 116.74/116.81 cnf(792,plain,
% 116.74/116.81 (E(f5(f3(f3(a6)),f4(a1)),f4(f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[789,627,2,3])).
% 116.74/116.81 cnf(795,plain,
% 116.74/116.81 (E(f5(f3(a7),f3(a6)),f5(f4(a1),f3(a7)))),
% 116.74/116.81 inference(scs_inference,[],[792,629,507,2,3])).
% 116.74/116.81 cnf(799,plain,
% 116.74/116.81 (E(f5(f4(a1),f3(a7)),f5(f3(a7),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[795,2])).
% 116.74/116.81 cnf(809,plain,
% 116.74/116.81 (E(f3(a1),f3(f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[645,2])).
% 116.74/116.81 cnf(874,plain,
% 116.74/116.81 (E(f5(f3(f3(a1)),f4(a2)),f3(f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[97,809,3])).
% 116.74/116.81 cnf(877,plain,
% 116.74/116.81 (E(f4(f4(a2)),f3(f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[135,874,3])).
% 116.74/116.81 cnf(881,plain,
% 116.74/116.81 (E(f3(f5(a1,a7)),f5(f3(f3(a1)),f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[153,877,3,2])).
% 116.74/116.81 cnf(888,plain,
% 116.74/116.81 (E(f4(a6),f4(f5(f4(a1),a6)))),
% 116.74/116.81 inference(scs_inference,[],[740,2,18])).
% 116.74/116.81 cnf(890,plain,
% 116.74/116.81 (E(f3(f5(a1,a7)),f4(a2))),
% 116.74/116.81 inference(scs_inference,[],[881,888,131,2,3])).
% 116.74/116.81 cnf(903,plain,
% 116.74/116.81 (E(f5(f4(a1),x9031),f5(f3(a6),x9031))),
% 116.74/116.81 inference(scs_inference,[],[98,2,6])).
% 116.74/116.81 cnf(904,plain,
% 116.74/116.81 (E(f5(f3(a6),x9041),f5(f4(a1),x9041))),
% 116.74/116.81 inference(scs_inference,[],[903,2])).
% 116.74/116.81 cnf(905,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f3(a6)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[98,785,903,2,3])).
% 116.74/116.81 cnf(906,plain,
% 116.74/116.81 (E(f5(x9061,f4(a1)),f5(x9061,f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[98,2,7])).
% 116.74/116.81 cnf(908,plain,
% 116.74/116.81 (E(f5(f3(a6),f3(a7)),f5(f3(a7),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[799,904,905,2,3])).
% 116.74/116.81 cnf(912,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f3(a7)),f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[98,908,674,2,3])).
% 116.74/116.81 cnf(913,plain,
% 116.74/116.81 (E(f3(f5(a1,a6)),f3(a1))),
% 116.74/116.81 inference(scs_inference,[],[98,2,17])).
% 116.74/116.81 cnf(915,plain,
% 116.74/116.81 (~E(a6,f5(f4(a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[912,903,551,2,3])).
% 116.74/116.81 cnf(918,plain,
% 116.74/116.81 (E(f5(x9181,f3(a6)),f5(x9181,f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[906,2])).
% 116.74/116.81 cnf(919,plain,
% 116.74/116.81 (E(f3(a6),f5(f3(f4(a1)),f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[388,906,2,3])).
% 116.74/116.81 cnf(923,plain,
% 116.74/116.81 (E(f5(a1,f3(a6)),f5(f4(a2),a1))),
% 116.74/116.81 inference(scs_inference,[],[918,919,290,2,3])).
% 116.74/116.81 cnf(926,plain,
% 116.74/116.81 (E(f5(f4(a2),a1),f5(a1,f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[923,2])).
% 116.74/116.81 cnf(927,plain,
% 116.74/116.81 (E(f5(f5(f3(a1),a1),f3(a6)),f5(f4(a2),a1))),
% 116.74/116.81 inference(scs_inference,[],[923,404,2,3])).
% 116.74/116.81 cnf(931,plain,
% 116.74/116.81 (E(f5(f5(f3(a1),a1),f3(a6)),f5(a1,f4(a1)))),
% 116.74/116.81 inference(scs_inference,[],[927,297,2,3])).
% 116.74/116.81 cnf(934,plain,
% 116.74/116.81 (E(a1,f5(a1,f3(a6)))),
% 116.74/116.81 inference(scs_inference,[],[931,926,179,2,3])).
% 116.74/116.81 cnf(936,plain,
% 116.74/116.81 (E(f5(a1,f3(a6)),a1)),
% 116.74/116.81 inference(scs_inference,[],[934,2])).
% 116.74/116.81 cnf(950,plain,
% 116.74/116.81 (E(f3(a1),f3(f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[913,2])).
% 116.74/116.81 cnf(974,plain,
% 116.74/116.81 (E(f3(f5(a1,a6)),f4(f4(a2)))),
% 116.74/116.81 inference(scs_inference,[],[105,950,3,2])).
% 116.74/116.81 cnf(980,plain,
% 116.74/116.81 (E(f5(f3(f4(a2)),f4(a2)),f3(f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[344,974,3,2])).
% 116.74/116.81 cnf(983,plain,
% 116.74/116.81 (E(f3(f5(a1,a6)),f4(f3(a1)))),
% 116.74/116.81 inference(scs_inference,[],[348,980,3,2])).
% 116.74/116.81 cnf(985,plain,
% 116.74/116.81 (E(f3(f5(a1,a6)),f4(a2))),
% 116.74/116.81 inference(scs_inference,[],[983,120,3])).
% 116.74/116.81 cnf(1153,plain,
% 116.74/116.81 (E(f3(f5(a1,f3(a7))),f3(a1))),
% 116.74/116.81 inference(scs_inference,[],[710,4])).
% 116.74/116.81 cnf(1155,plain,
% 116.74/116.81 (E(f5(a2,x11551),f5(f5(a2,f3(a1)),x11551))),
% 116.74/116.81 inference(scs_inference,[],[497,710,4,5,6])).
% 116.74/116.81 cnf(1162,plain,
% 116.74/116.81 (~E(f5(a1,a6),f5(a1,f5(a7,f4(a7))))),
% 116.74/116.81 inference(scs_inference,[],[328,497,915,305,710,904,296,14,98,84,4,5,6,7,18,2,3,20])).
% 116.74/116.81 cnf(1172,plain,
% 116.74/116.81 (E(f5(f5(a1,f3(a6)),x11721),f5(a1,x11721))),
% 116.74/116.81 inference(scs_inference,[],[936,712,105,18,7,4,6])).
% 116.74/116.81 cnf(1175,plain,
% 116.74/116.81 (E(f3(f5(a1,f3(a7))),f4(a2))),
% 116.74/116.81 inference(scs_inference,[],[8,936,298,1153,712,105,18,7,4,6,5,2,3])).
% 116.74/116.81 cnf(1176,plain,
% 116.74/116.81 (~E(f5(a1,a6),f5(f5(f3(a1),a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[8,936,298,1153,328,335,712,105,98,84,18,7,4,6,5,2,3,20])).
% 116.74/116.81 cnf(1189,plain,
% 116.74/116.81 (E(f5(a1,x11891),f5(f5(a1,f3(a6)),x11891))),
% 116.74/116.81 inference(scs_inference,[],[934,7,6])).
% 116.74/116.81 cnf(1198,plain,
% 116.74/116.81 (~E(f5(a7,f4(a7)),f5(f3(a7),a6))),
% 116.74/116.81 inference(scs_inference,[],[634,569,710,53,5,7,6,2,3])).
% 116.74/116.81 cnf(1202,plain,
% 116.74/116.81 (E(f5(a1,x12021),f5(f5(f4(a2),a1),x12021))),
% 116.74/116.81 inference(scs_inference,[],[179,5,7,6])).
% 116.74/116.81 cnf(1203,plain,
% 116.74/116.81 (~E(f5(f3(a7),a6),f5(a7,f4(a7)))),
% 116.74/116.81 inference(scs_inference,[],[1198,179,5,7,6,2])).
% 116.74/116.81 cnf(1210,plain,
% 116.74/116.81 (~E(f5(f3(a6),a6),f5(a7,f4(a7)))),
% 116.74/116.81 inference(scs_inference,[],[1203,1162,554,182,712,7,5,6,2,3])).
% 116.74/116.81 cnf(1216,plain,
% 116.74/116.81 (E(f5(a1,x12161),f5(f5(a1,f3(a6)),x12161))),
% 116.74/116.81 inference(rename_variables,[],[1189])).
% 116.74/116.81 cnf(1217,plain,
% 116.74/116.81 (~E(f5(a1,a6),f5(f5(a1,f3(a6)),a7))),
% 116.74/116.81 inference(scs_inference,[],[1210,1189,1216,926,328,712,98,84,7,6,2,3,20])).
% 116.74/116.81 cnf(1220,plain,
% 116.74/116.81 (~E(f5(f5(a1,f3(a6)),a7),f5(a1,a6))),
% 116.74/116.81 inference(scs_inference,[],[1217,2])).
% 116.74/116.81 cnf(1230,plain,
% 116.74/116.81 (~E(f5(a1,a7),f5(a1,a6))),
% 116.74/116.81 inference(scs_inference,[],[1220,1176,1172,2,3])).
% 116.74/116.81 cnf(1235,plain,
% 116.74/116.81 (~E(f5(a1,a6),f5(a1,a7))),
% 116.74/116.81 inference(scs_inference,[],[1230,2])).
% 116.74/116.81 cnf(1251,plain,
% 116.74/116.81 (~E(f5(f5(a1,f3(a6)),a6),f5(a1,a7))),
% 116.74/116.81 inference(scs_inference,[],[1235,445,1189,2,3])).
% 116.74/116.81 cnf(1254,plain,
% 116.74/116.81 (~E(f5(f4(a1),a6),f5(a7,f4(a7)))),
% 116.74/116.81 inference(scs_inference,[],[1251,1203,629,2,3])).
% 116.74/116.81 cnf(1259,plain,
% 116.74/116.81 (~E(f5(a7,f4(a7)),f5(f4(a1),a6))),
% 116.74/116.81 inference(scs_inference,[],[1254,2])).
% 116.74/116.81 cnf(1262,plain,
% 116.74/116.81 (~E(f5(a2,f5(a1,a7)),f5(f5(a2,a1),a6))),
% 116.74/116.81 inference(scs_inference,[],[1254,1230,1202,890,985,173,2,3,19])).
% 116.74/116.81 cnf(1267,plain,
% 116.74/116.81 (~E(f5(f5(a2,a1),a6),f5(a2,f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[1262,2])).
% 116.74/116.81 cnf(1268,plain,
% 116.74/116.81 (~E(f5(f5(f3(a2),a2),f5(a1,a6)),f5(a2,f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[1262,478,2,3])).
% 116.74/116.81 cnf(1274,plain,
% 116.74/116.81 (~E(f5(f5(f3(a7),a7),f4(a7)),f5(f4(a1),a6))),
% 116.74/116.81 inference(scs_inference,[],[1259,1268,335,2,3])).
% 116.74/116.81 cnf(1277,plain,
% 116.74/116.81 (~E(f5(f5(a2,f4(a2)),f5(a1,a6)),f5(a2,f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[1267,481,1274,2,3])).
% 116.74/116.81 cnf(1279,plain,
% 116.74/116.81 (~E(f5(a6,f4(a6)),f5(f4(a1),a7))),
% 116.74/116.81 inference(scs_inference,[],[1277,915,53,2,3])).
% 116.74/116.81 cnf(1281,plain,
% 116.74/116.81 (~E(f5(f4(a1),a7),f5(a6,f4(a6)))),
% 116.74/116.81 inference(scs_inference,[],[1279,2])).
% 116.74/116.81 cnf(1282,plain,
% 116.74/116.81 (~E(f5(a2,f5(a1,a6)),f5(a2,f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[1279,1267,107,2,3])).
% 116.74/116.81 cnf(1286,plain,
% 116.74/116.81 (~E(f5(a2,f5(a1,a7)),f5(a2,f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[1282,2])).
% 116.74/116.81 cnf(1287,plain,
% 116.74/116.81 (~E(f5(f3(a6),a6),f5(f3(a6),a7))),
% 116.74/116.81 inference(scs_inference,[],[1282,551,56,2,3])).
% 116.74/116.81 cnf(1292,plain,
% 116.74/116.81 (~E(f5(f3(a6),a7),f5(f3(a6),a6))),
% 116.74/116.81 inference(scs_inference,[],[1287,2])).
% 116.74/116.81 cnf(1296,plain,
% 116.74/116.81 (~E(f5(f3(a6),a7),f5(a6,f4(a6)))),
% 116.74/116.81 inference(scs_inference,[],[1281,326,903,2,3])).
% 116.74/116.81 cnf(1299,plain,
% 116.74/116.81 (~E(f5(f4(a1),a7),f5(f3(a6),a6))),
% 116.74/116.81 inference(scs_inference,[],[1292,1296,904,2,3])).
% 116.74/116.81 cnf(1303,plain,
% 116.74/116.81 (~E(f5(f5(a2,f3(a1)),f5(a1,a7)),f5(a2,f5(a1,a6)))),
% 116.74/116.81 inference(scs_inference,[],[1286,1299,1155,2,3])).
% 116.74/116.81 cnf(1309,plain,
% 116.74/116.81 (~E(f5(f5(a2,a1),a7),f5(a2,f5(a1,a7)))),
% 116.74/116.81 inference(scs_inference,[],[1303,1282,158,2,3])).
% 116.74/116.81 cnf(1494,plain,
% 116.74/116.81 ($false),
% 116.74/116.81 inference(scs_inference,[],[22,293,86,1230,1175,1309,2,3,21]),
% 116.74/116.81 ['proof']).
% 116.74/116.81 % SZS output end Proof
% 116.74/116.81 % Total time :116.170000s
%------------------------------------------------------------------------------