%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD067-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 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 05:55:34 EDT 2024
% Result : Unsatisfiable 59.11s 59.60s
% Output : CNFRefutation 59.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : FLD067-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n020.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Jun 19 11:37:38 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.49/0.58 start to proof:theBenchmark
% 59.11/59.59 %-------------------------------------------
% 59.11/59.59 % File :CSE---1.7
% 59.11/59.59 % Problem :theBenchmark
% 59.11/59.59 % Transform :cnf
% 59.11/59.59 % Format :tptp:raw
% 59.11/59.59 % Command :java -jar mcs_scs.jar %d %s
% 59.11/59.59
% 59.11/59.59 % Result :Theorem 58.550000s
% 59.11/59.59 % Output :CNFRefutation 58.550000s
% 59.11/59.59 %-------------------------------------------
% 59.11/59.59 %--------------------------------------------------------------------------
% 59.11/59.59 % File : FLD067-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 59.11/59.59 % Domain : Field Theory (Ordered fields)
% 59.11/59.59 % Problem : Side change in an order relation, part 1
% 59.11/59.59 % Version : [Dra93] axioms : Especial.
% 59.11/59.59 % Theorem formulation : Functional with glxx axiom set.
% 59.11/59.59 % English :
% 59.11/59.59
% 59.11/59.59 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 59.11/59.59 % Source : [Dra93]
% 59.11/59.59 % Names :
% 59.11/59.59
% 59.11/59.59 % Status : Unsatisfiable
% 59.11/59.59 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.20 v5.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.36 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.33 v2.1.0
% 59.11/59.59 % Syntax : Number of clauses : 31 ( 7 unt; 3 nHn; 31 RR)
% 59.11/59.60 % Number of literals : 77 ( 0 equ; 45 neg)
% 59.11/59.60 % Maximal clause size : 4 ( 2 avg)
% 59.11/59.60 % Maximal term depth : 3 ( 1 avg)
% 59.11/59.60 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 59.11/59.60 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 59.11/59.60 % Number of variables : 50 ( 0 sgn)
% 59.11/59.60 % SPC : CNF_UNS_RFO_NEQ_NHN
% 59.11/59.60
% 59.11/59.60 % Comments :
% 59.11/59.60 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 59.11/59.60 %--------------------------------------------------------------------------
% 59.11/59.60 include('Axioms/FLD001-0.ax').
% 59.11/59.60 %--------------------------------------------------------------------------
% 59.11/59.60 cnf(a_is_defined,hypothesis,
% 59.11/59.60 defined(a) ).
% 59.11/59.60
% 59.11/59.60 cnf(b_is_defined,hypothesis,
% 59.11/59.60 defined(b) ).
% 59.11/59.60
% 59.11/59.60 cnf(less_or_equal_3,negated_conjecture,
% 59.11/59.60 less_or_equal(a,b) ).
% 59.11/59.60
% 59.11/59.60 cnf(not_less_or_equal_4,negated_conjecture,
% 59.11/59.60 ~ less_or_equal(additive_identity,add(b,additive_inverse(a))) ).
% 59.11/59.60
% 59.11/59.60 %--------------------------------------------------------------------------
% 59.11/59.60 %-------------------------------------------
% 59.11/59.60 % Proof found
% 59.11/59.60 % SZS status Theorem for theBenchmark
% 59.11/59.60 % SZS output start Proof
% 59.11/59.60 %ClaNum:31(EqnAxiom:0)
% 59.11/59.60 %VarNum:128(SingletonVarNum:50)
% 59.11/59.60 %MaxLitNum:4
% 59.11/59.60 %MaxfuncDepth:2
% 59.11/59.60 %SharedTerms:13
% 59.11/59.60 %goalClause: 5 7
% 59.11/59.60 %singleGoalClaCount:2
% 59.11/59.60 [1]P1(a1)
% 59.11/59.60 [2]P1(a4)
% 59.11/59.60 [3]P1(a2)
% 59.11/59.60 [4]P1(a5)
% 59.11/59.60 [5]P2(a2,a5)
% 59.11/59.60 [6]~P3(a1,a4)
% 59.11/59.60 [7]~P2(a1,f3(a5,f6(a2)))
% 59.11/59.60 [9]~P1(x91)+P3(x91,x91)
% 59.11/59.60 [8]~P1(x81)+P1(f6(x81))
% 59.11/59.60 [13]~P1(x131)+P3(f3(a1,x131),x131)
% 59.11/59.60 [14]~P1(x141)+P3(f8(a4,x141),x141)
% 59.11/59.60 [17]~P1(x171)+P3(f3(x171,f6(x171)),a1)
% 59.11/59.60 [11]~P3(x112,x111)+P3(x111,x112)
% 59.11/59.60 [10]~P1(x101)+P3(x101,a1)+P1(f7(x101))
% 59.11/59.60 [22]~P1(x221)+P3(x221,a1)+P3(f8(x221,f7(x221)),a4)
% 59.11/59.60 [19]~P2(x192,x191)+~P2(x191,x192)+P3(x191,x192)
% 59.11/59.60 [15]~P1(x152)+~P1(x151)+P1(f3(x151,x152))
% 59.11/59.60 [16]~P1(x162)+~P1(x161)+P1(f8(x161,x162))
% 59.11/59.60 [23]~P2(a1,x232)+~P2(a1,x231)+P2(a1,f8(x231,x232))
% 59.11/59.60 [24]~P1(x242)+~P1(x241)+P3(f3(x241,x242),f3(x242,x241))
% 59.11/59.60 [25]~P1(x252)+~P1(x251)+P3(f8(x251,x252),f8(x252,x251))
% 59.11/59.60 [18]~P3(x181,x183)+P3(x181,x182)+~P3(x183,x182)
% 59.11/59.60 [20]~P2(x203,x202)+P2(x201,x202)+~P3(x203,x201)
% 59.11/59.60 [21]~P2(x211,x213)+P2(x211,x212)+~P2(x213,x212)
% 59.11/59.60 [26]~P1(x262)+~P3(x261,x263)+P3(f3(x261,x262),f3(x263,x262))
% 59.11/59.60 [27]~P1(x272)+~P3(x271,x273)+P3(f8(x271,x272),f8(x273,x272))
% 59.11/59.60 [28]~P1(x282)+~P2(x281,x283)+P2(f3(x281,x282),f3(x283,x282))
% 59.11/59.60 [12]P2(x122,x121)+~P1(x121)+~P1(x122)+P2(x121,x122)
% 59.11/59.60 [29]~P1(x293)+~P1(x292)+~P1(x291)+P3(f3(x291,f3(x292,x293)),f3(f3(x291,x292),x293))
% 59.11/59.60 [30]~P1(x303)+~P1(x302)+~P1(x301)+P3(f8(x301,f8(x302,x303)),f8(f8(x301,x302),x303))
% 59.11/59.60 [31]~P1(x313)+~P1(x312)+~P1(x311)+P3(f3(f8(x311,x312),f8(x313,x312)),f8(f3(x311,x313),x312))
% 59.11/59.60 %EqnAxiom
% 59.11/59.60
% 59.11/59.60 %-------------------------------------------
% 59.11/59.61 cnf(32,plain,
% 59.11/59.61 (~P3(a4,a1)),
% 59.11/59.61 inference(scs_inference,[],[6,11])).
% 59.11/59.61 cnf(34,plain,
% 59.11/59.61 (P2(a1,a1)),
% 59.11/59.61 inference(scs_inference,[],[1,6,11,12])).
% 59.11/59.61 cnf(43,plain,
% 59.11/59.61 (P2(a4,a4)),
% 59.11/59.61 inference(scs_inference,[],[2,34,19,12])).
% 59.11/59.61 cnf(45,plain,
% 59.11/59.61 (~P2(x451,a2)+P2(x451,a5)),
% 59.11/59.61 inference(scs_inference,[],[5,2,34,19,12,21])).
% 59.11/59.61 cnf(69,plain,
% 59.11/59.61 (P3(f3(a1,f6(a4)),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[2,13,8])).
% 59.11/59.61 cnf(75,plain,
% 59.11/59.61 (P3(f8(a4,f6(a4)),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[2,14,8])).
% 59.11/59.61 cnf(81,plain,
% 59.11/59.61 (~P3(x811,f3(a1,f6(a4)))+P3(x811,f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[69,18])).
% 59.11/59.61 cnf(86,plain,
% 59.11/59.61 (~P3(x861,f8(a4,f6(a4)))+P3(x861,f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[75,18])).
% 59.11/59.61 cnf(94,plain,
% 59.11/59.61 (P3(f3(f6(a2),f6(f6(a2))),a1)),
% 59.11/59.61 inference(scs_inference,[],[3,17,8])).
% 59.11/59.61 cnf(108,plain,
% 59.11/59.61 (~P1(f6(a4))+P3(f8(f6(a4),a4),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[2,86,25])).
% 59.11/59.61 cnf(114,plain,
% 59.11/59.61 (P3(f6(a4),f8(f6(a4),a4))+~P1(f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[108,11])).
% 59.11/59.61 cnf(116,plain,
% 59.11/59.61 (P3(f3(a1,f6(a4)),f8(f6(a4),a4))+~P1(f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[69,114,18])).
% 59.11/59.61 cnf(117,plain,
% 59.11/59.61 (P3(f8(f6(a4),a4),f3(a1,f6(a4)))+~P1(f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[116,11])).
% 59.11/59.61 cnf(183,plain,
% 59.11/59.61 (P3(f3(a1,f6(a5)),f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[4,8,13])).
% 59.11/59.61 cnf(184,plain,
% 59.11/59.61 (~P2(f3(a1,f6(a5)),x1841)+P2(f6(a5),x1841)),
% 59.11/59.61 inference(scs_inference,[],[183,20])).
% 59.11/59.61 cnf(189,plain,
% 59.11/59.61 (~P1(f6(a5))+P2(f6(a5),f3(a1,f6(a5)))),
% 59.11/59.61 inference(scs_inference,[],[34,184,28])).
% 59.11/59.61 cnf(190,plain,
% 59.11/59.61 (~P3(x1901,f3(a1,f6(a5)))+P3(x1901,f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[183,18])).
% 59.11/59.61 cnf(210,plain,
% 59.11/59.61 (P3(f8(a4,f6(a5)),f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[4,8,14])).
% 59.11/59.61 cnf(211,plain,
% 59.11/59.61 (~P2(f8(a4,f6(a5)),x2111)+P2(f6(a5),x2111)),
% 59.11/59.61 inference(scs_inference,[],[210,20])).
% 59.11/59.61 cnf(216,plain,
% 59.11/59.61 (P2(f6(a5),a5)+~P2(f8(a4,f6(a5)),a2)),
% 59.11/59.61 inference(scs_inference,[],[211,45])).
% 59.11/59.61 cnf(217,plain,
% 59.11/59.61 (~P3(x2171,f8(a4,f6(a5)))+P3(x2171,f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[210,18])).
% 59.11/59.61 cnf(222,plain,
% 59.11/59.61 (~P2(x2221,f6(a5))+P2(x2221,a5)+~P2(f8(a4,f6(a5)),a2)),
% 59.11/59.61 inference(scs_inference,[],[216,21])).
% 59.11/59.61 cnf(369,plain,
% 59.11/59.61 (P3(f8(f6(a4),a4),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[2,8,108])).
% 59.11/59.61 cnf(376,plain,
% 59.11/59.61 (~P3(x3761,f8(f6(a4),a4))+P3(x3761,f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[369,18])).
% 59.11/59.61 cnf(382,plain,
% 59.11/59.61 (P3(f8(f8(a4,f6(a4)),a4),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[75,2,376,27])).
% 59.11/59.61 cnf(389,plain,
% 59.11/59.61 (~P3(x3891,f8(f8(a4,f6(a4)),a4))+P3(x3891,f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[382,18])).
% 59.11/59.61 cnf(395,plain,
% 59.11/59.61 (~P3(x3951,f8(a4,f6(a4)))+P3(f8(x3951,a4),f6(a4))),
% 59.11/59.61 inference(scs_inference,[],[2,389,27])).
% 59.11/59.61 cnf(427,plain,
% 59.11/59.61 (P3(f6(a4),f8(f6(a4),a4))),
% 59.11/59.61 inference(scs_inference,[],[2,8,114])).
% 59.11/59.61 cnf(428,plain,
% 59.11/59.61 (P3(f8(a4,f6(a4)),f8(f6(a4),a4))),
% 59.11/59.61 inference(scs_inference,[],[75,427,18])).
% 59.11/59.61 cnf(436,plain,
% 59.11/59.61 (P3(f3(a1,f6(a4)),f8(f6(a4),a4))),
% 59.11/59.61 inference(scs_inference,[],[69,427,18])).
% 59.11/59.61 cnf(444,plain,
% 59.11/59.61 (~P2(f3(a1,f6(a4)),x4441)+P2(f8(f6(a4),a4),x4441)),
% 59.11/59.61 inference(scs_inference,[],[436,20])).
% 59.11/59.61 cnf(449,plain,
% 59.11/59.61 (~P3(x4491,f8(a4,f6(a4)))+P3(x4491,f8(f6(a4),a4))),
% 59.11/59.61 inference(scs_inference,[],[428,18])).
% 59.11/59.61 cnf(462,plain,
% 59.11/59.61 (P3(f8(f6(a4),a4),x4621)+~P3(x4621,f8(a4,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[449,11])).
% 59.11/59.61 cnf(506,plain,
% 59.11/59.61 (P3(f8(f6(a4),a4),f3(a1,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[2,8,117])).
% 59.11/59.61 cnf(515,plain,
% 59.11/59.61 (P3(f8(a4,f6(a4)),f3(a1,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[428,506,18])).
% 59.11/59.61 cnf(520,plain,
% 59.11/59.61 (~P3(x5201,f8(a4,f6(a4)))+P3(x5201,f3(a1,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[515,18])).
% 59.11/59.61 cnf(532,plain,
% 59.11/59.61 (P3(f3(a1,f6(a4)),x5321)+~P3(x5321,f8(a4,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[520,11])).
% 59.11/59.61 cnf(585,plain,
% 59.11/59.61 (P2(f6(a5),f3(a1,f6(a5)))),
% 59.11/59.61 inference(scs_inference,[],[4,8,189])).
% 59.11/59.61 cnf(588,plain,
% 59.11/59.61 (P3(f3(a1,f6(a5)),f3(a1,f6(a5)))+~P2(f3(a1,f6(a5)),f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[585,21,19])).
% 59.11/59.61 cnf(595,plain,
% 59.11/59.61 (~P3(x5951,f3(a1,f6(a5)))+~P2(x5951,f6(a5))+P3(f3(a1,f6(a5)),f3(a1,f6(a5)))),
% 59.11/59.61 inference(scs_inference,[],[588,20])).
% 59.11/59.61 cnf(597,plain,
% 59.11/59.61 (P3(f3(a1,f6(a5)),f3(a1,f6(a5)))+~P2(f6(a5),f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[183,595,11])).
% 59.11/59.61 cnf(759,plain,
% 59.11/59.61 (~P1(f6(a2))+P2(f3(a5,f6(a2)),a1)),
% 59.11/59.61 inference(scs_inference,[],[7,4,1,12,15])).
% 59.11/59.61 cnf(762,plain,
% 59.11/59.61 (~P2(x7621,f3(a5,f6(a2)))+P2(x7621,a1)+~P1(f6(a2))),
% 59.11/59.61 inference(scs_inference,[],[759,21])).
% 59.11/59.61 cnf(768,plain,
% 59.11/59.61 (~P1(f6(a2))+P2(f3(a2,f6(a2)),a1)),
% 59.11/59.61 inference(scs_inference,[],[5,762,28])).
% 59.11/59.61 cnf(769,plain,
% 59.11/59.61 (P2(f3(a2,f6(a2)),a1)),
% 59.11/59.61 inference(scs_inference,[],[3,768,8])).
% 59.11/59.61 cnf(983,plain,
% 59.11/59.61 (P1(f3(f6(a1),f6(a1)))),
% 59.11/59.61 inference(scs_inference,[],[1,8,15])).
% 59.11/59.61 cnf(1039,plain,
% 59.11/59.61 (P2(f3(a2,f6(a2)),f3(a5,f6(a2)))),
% 59.11/59.61 inference(scs_inference,[],[3,5,8,28])).
% 59.11/59.61 cnf(1113,plain,
% 59.11/59.61 (P2(f3(f3(a2,f6(a2)),f6(a5)),f3(a1,f6(a5)))),
% 59.11/59.61 inference(scs_inference,[],[4,769,8,28])).
% 59.11/59.61 cnf(1170,plain,
% 59.11/59.61 (P2(f6(a5),f6(a5))),
% 59.11/59.61 inference(scs_inference,[],[4,8,12])).
% 59.11/59.61 cnf(1171,plain,
% 59.11/59.61 (P3(f3(a1,f6(a5)),f3(a1,f6(a5)))),
% 59.11/59.61 inference(scs_inference,[],[1170,597])).
% 59.11/59.61 cnf(1178,plain,
% 59.11/59.61 (P2(f3(a1,f6(a4)),f3(a1,f6(a4)))),
% 59.11/59.61 inference(scs_inference,[],[2,34,8,28])).
% 59.11/59.61 cnf(1181,plain,
% 59.11/59.62 (P2(f6(a4),f3(a1,f6(a4)))),
% 59.11/59.62 inference(scs_inference,[],[69,1178,444,20])).
% 59.11/59.62 cnf(1422,plain,
% 59.11/59.62 (P3(a4,f3(a1,a4))),
% 59.11/59.62 inference(scs_inference,[],[2,11,13])).
% 59.11/59.62 cnf(1665,plain,
% 59.11/59.62 (P3(f8(a4,f6(a5)),f8(a4,f6(a5)))),
% 59.11/59.62 inference(scs_inference,[],[210,11,18])).
% 59.11/59.62 cnf(1669,plain,
% 59.11/59.62 (P3(f6(a4),f8(a4,f6(a4)))),
% 59.11/59.62 inference(scs_inference,[],[515,11,81])).
% 59.11/59.62 cnf(1674,plain,
% 59.11/59.62 (P3(f8(f6(a4),a4),f8(a4,f6(a4)))),
% 59.11/59.62 inference(scs_inference,[],[1181,75,1669,18,20,462])).
% 59.11/59.62 cnf(1676,plain,
% 59.11/59.62 (P3(f3(a1,f6(a4)),f8(a4,f6(a4)))),
% 59.11/59.62 inference(scs_inference,[],[1181,75,1669,18,20,462,532])).
% 59.11/59.62 cnf(1710,plain,
% 59.11/59.62 (P3(f6(a5),f3(a1,f6(a5)))),
% 59.11/59.62 inference(scs_inference,[],[1171,11,190])).
% 59.11/59.62 cnf(1713,plain,
% 59.11/59.62 (~P2(f8(a4,f6(a5)),x17131)+P2(f3(a1,f6(a5)),x17131)),
% 59.11/59.62 inference(scs_inference,[],[210,1710,18,20])).
% 59.11/59.62 cnf(1728,plain,
% 59.11/59.62 (P3(f6(a5),f8(a4,f6(a5)))),
% 59.11/59.62 inference(scs_inference,[],[1665,11,217])).
% 59.11/59.62 cnf(1746,plain,
% 59.11/59.62 (P1(f7(a4))),
% 59.11/59.62 inference(scs_inference,[],[6,2,11,10])).
% 59.11/59.62 cnf(1747,plain,
% 59.11/59.62 (P2(f7(a4),f7(a4))),
% 59.11/59.62 inference(scs_inference,[],[1746,12])).
% 59.11/59.62 cnf(1750,plain,
% 59.11/59.62 (P3(f8(a4,f7(a4)),a4)),
% 59.11/59.62 inference(scs_inference,[],[6,2,11,22])).
% 59.11/59.62 cnf(1753,plain,
% 59.11/59.62 (~P3(f8(a4,f7(a4)),a1)),
% 59.11/59.62 inference(scs_inference,[],[6,1750,18,11])).
% 59.11/59.62 cnf(1772,plain,
% 59.11/59.62 (P3(a4,f8(a4,f7(a4)))),
% 59.11/59.62 inference(scs_inference,[],[32,2,11,22])).
% 59.11/59.62 cnf(1773,plain,
% 59.11/59.62 (P2(f8(a4,f7(a4)),a4)),
% 59.11/59.62 inference(scs_inference,[],[43,1772,20])).
% 59.11/59.62 cnf(1813,plain,
% 59.11/59.62 (P2(f3(a1,f6(a5)),f6(a5))),
% 59.11/59.62 inference(scs_inference,[],[1170,1728,20,1713])).
% 59.11/59.62 cnf(1860,plain,
% 59.11/59.62 (P3(f8(a4,f7(a4)),f3(a1,a4))),
% 59.11/59.62 inference(scs_inference,[],[1750,1422,18])).
% 59.11/59.62 cnf(1914,plain,
% 59.11/59.62 (P2(f3(f6(a2),f6(f6(a2))),a1)),
% 59.11/59.62 inference(scs_inference,[],[94,34,11,20])).
% 59.11/59.62 cnf(2040,plain,
% 59.11/59.62 (P3(f6(a4),f8(f3(a1,f6(a4)),a4))),
% 59.11/59.62 inference(scs_inference,[],[1676,11,395])).
% 59.11/59.62 cnf(2062,plain,
% 59.11/59.62 (P2(f3(f3(a2,f6(a2)),f6(a5)),f6(a5))),
% 59.11/59.62 inference(scs_inference,[],[1113,1813,21])).
% 59.11/59.62 cnf(2256,plain,
% 59.11/59.62 (P3(f3(a1,f7(a4)),f7(a4))),
% 59.11/59.62 inference(scs_inference,[],[983,1746,8,13])).
% 59.11/59.62 cnf(2258,plain,
% 59.11/59.62 (P3(f8(a4,f7(a4)),f7(a4))),
% 59.11/59.62 inference(scs_inference,[],[983,1746,8,13,14])).
% 59.11/59.62 cnf(2274,plain,
% 59.11/59.62 (P2(a1,f8(a1,a1))),
% 59.11/59.62 inference(scs_inference,[],[2040,1747,983,1674,1746,34,8,13,14,17,395,11,16,24,25,28,23])).
% 59.11/59.62 cnf(2276,plain,
% 59.11/59.62 (P1(f3(f7(a4),f7(a4)))),
% 59.11/59.62 inference(scs_inference,[],[2040,1747,983,1674,1746,34,8,13,14,17,395,11,16,24,25,28,23,15])).
% 59.11/59.62 cnf(2280,plain,
% 59.11/59.62 (~P3(f3(a2,f6(a2)),a1)),
% 59.11/59.62 inference(scs_inference,[],[7,2040,1747,983,1674,1746,34,1039,8,13,14,17,395,11,16,24,25,28,23,15,21,20])).
% 59.11/59.62 cnf(2292,plain,
% 59.11/59.62 (P3(f7(a4),a1)+P3(f8(f7(a4),f7(f7(a4))),a4)),
% 59.11/59.62 inference(scs_inference,[],[7,2040,1860,1753,1747,983,1674,1746,34,4,1039,8,13,14,17,395,11,16,24,25,28,23,15,21,20,18,29,30,31,10,22])).
% 59.11/59.62 cnf(2294,plain,
% 59.11/59.62 (P3(a4,f8(f7(a4),f7(f7(a4))))+P3(f7(a4),a1)),
% 59.11/59.62 inference(scs_inference,[],[2292,11])).
% 59.11/59.62 cnf(2297,plain,
% 59.11/59.62 (P3(f8(a4,a5),a5)),
% 59.11/59.62 inference(scs_inference,[],[2276,4,8,14])).
% 59.11/59.62 cnf(2301,plain,
% 59.11/59.62 (P3(f3(a1,a5),a5)),
% 59.11/59.62 inference(scs_inference,[],[2276,4,8,14,17,13])).
% 59.11/59.62 cnf(2313,plain,
% 59.11/59.62 (P1(f8(a5,a5))),
% 59.11/59.62 inference(scs_inference,[],[2258,2276,1746,4,8,14,17,13,11,26,27,24,25,16])).
% 59.11/59.62 cnf(2315,plain,
% 59.11/59.62 (P2(f3(a1,f7(a4)),f3(f8(a1,a1),f7(a4)))),
% 59.11/59.62 inference(scs_inference,[],[2274,2258,2276,1746,4,8,14,17,13,11,26,27,24,25,16,28])).
% 59.11/59.62 cnf(2317,plain,
% 59.11/59.62 (P2(a1,f8(f8(a1,a1),f8(a1,a1)))),
% 59.11/59.62 inference(scs_inference,[],[2274,2258,2276,1746,4,8,14,17,13,11,26,27,24,25,16,28,23])).
% 59.11/59.62 cnf(2319,plain,
% 59.11/59.62 (P1(f3(a5,a5))),
% 59.11/59.62 inference(scs_inference,[],[2274,2258,2276,1746,4,8,14,17,13,11,26,27,24,25,16,28,23,15])).
% 59.11/59.62 cnf(2323,plain,
% 59.11/59.62 (P2(f7(a4),a4)),
% 59.11/59.62 inference(scs_inference,[],[2274,2258,2276,1914,1746,1773,4,8,14,17,13,11,26,27,24,25,16,28,23,15,21,20])).
% 59.11/59.62 cnf(2336,plain,
% 59.11/59.62 (P1(f7(f7(a4)))),
% 59.11/59.62 inference(scs_inference,[],[2274,2258,2276,1753,1914,2062,1746,1773,4,3,8,14,17,13,11,26,27,24,25,16,28,23,15,21,20,18,29,30,31,2294,222,10])).
% 59.11/59.62 cnf(2349,plain,
% 59.11/59.62 (P3(f8(a4,f3(a5,a5)),f3(a5,a5))),
% 59.11/59.62 inference(scs_inference,[],[2319,2336,8,17,14])).
% 59.11/59.62 cnf(2363,plain,
% 59.11/59.62 (P1(f8(f3(a5,a5),f3(a5,a5)))),
% 59.11/59.62 inference(scs_inference,[],[2297,2319,2256,2336,8,17,14,13,11,24,26,27,25,16])).
% 59.11/59.62 cnf(2371,plain,
% 59.11/59.62 (P2(f7(a4),f3(f8(a1,a1),f7(a4)))),
% 59.11/59.62 inference(scs_inference,[],[7,2297,2319,2323,2256,2336,2317,2315,8,17,14,13,11,24,26,27,25,16,28,15,21,20])).
% 59.11/59.62 cnf(2406,plain,
% 59.11/59.62 (P1(f3(f8(a5,a5),f8(a5,a5)))),
% 59.11/59.62 inference(scs_inference,[],[2301,2349,2363,2371,2313,8,14,17,13,11,27,24,25,16,28,15])).
% 59.11/59.62 cnf(2429,plain,
% 59.11/59.62 ($false),
% 59.11/59.62 inference(scs_inference,[],[2406,2280,3,8,14,17]),
% 59.11/59.62 ['proof']).
% 59.11/59.62 % SZS output end Proof
% 59.11/59.62 % Total time :58.550000s
%------------------------------------------------------------------------------