%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD067-2 : 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 : n025.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 60.06s 60.18s
% Output : CNFRefutation 60.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : FLD067-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.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 : Wed Jun 19 11:02:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.20/0.57 start to proof:theBenchmark
% 60.00/60.17 %-------------------------------------------
% 60.00/60.17 % File :CSE---1.7
% 60.00/60.17 % Problem :theBenchmark
% 60.00/60.17 % Transform :cnf
% 60.00/60.17 % Format :tptp:raw
% 60.00/60.17 % Command :java -jar mcs_scs.jar %d %s
% 60.00/60.17
% 60.00/60.17 % Result :Theorem 59.470000s
% 60.00/60.17 % Output :CNFRefutation 59.470000s
% 60.00/60.17 %-------------------------------------------
% 60.06/60.18 %--------------------------------------------------------------------------
% 60.06/60.18 % File : FLD067-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 60.06/60.18 % Domain : Field Theory (Ordered fields)
% 60.06/60.18 % Problem : Side change in an order relation, part 1
% 60.06/60.18 % Version : [Dra93] axioms : Especial.
% 60.06/60.18 % Theorem formulation : Relational with glxx axiom set.
% 60.06/60.18 % English :
% 60.06/60.18
% 60.06/60.18 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 60.06/60.18 % Source : [Dra93]
% 60.06/60.18 % Names :
% 60.06/60.18
% 60.06/60.18 % Status : Unsatisfiable
% 60.06/60.18 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.17 v7.1.0, 0.50 v7.0.0, 0.12 v6.4.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.22 v6.1.0, 0.29 v5.5.0, 0.38 v5.4.0, 0.40 v5.2.0, 0.20 v5.1.0, 0.27 v5.0.0, 0.43 v4.1.0, 0.25 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.20 v2.4.0, 0.40 v2.3.0, 0.67 v2.2.1, 0.67 v2.1.0
% 60.06/60.18 % Syntax : Number of clauses : 33 ( 9 unt; 3 nHn; 33 RR)
% 60.06/60.18 % Number of literals : 79 ( 0 equ; 45 neg)
% 60.06/60.18 % Maximal clause size : 4 ( 2 avg)
% 60.06/60.18 % Maximal term depth : 3 ( 1 avg)
% 60.06/60.18 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 60.06/60.18 % Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% 60.06/60.18 % Number of variables : 50 ( 0 sgn)
% 60.06/60.18 % SPC : CNF_UNS_RFO_NEQ_NHN
% 60.06/60.18
% 60.06/60.18 % Comments :
% 60.06/60.18 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 60.06/60.18 %--------------------------------------------------------------------------
% 60.06/60.18 include('Axioms/FLD001-0.ax').
% 60.06/60.18 %--------------------------------------------------------------------------
% 60.06/60.18 cnf(a_is_defined,hypothesis,
% 60.06/60.18 defined(a) ).
% 60.06/60.18
% 60.06/60.18 cnf(b_is_defined,hypothesis,
% 60.06/60.18 defined(b) ).
% 60.06/60.18
% 60.06/60.18 cnf(u_is_defined,hypothesis,
% 60.06/60.18 defined(u) ).
% 60.06/60.18
% 60.06/60.18 cnf(less_or_equal_4,negated_conjecture,
% 60.06/60.18 less_or_equal(a,b) ).
% 60.06/60.18
% 60.06/60.18 cnf(add_equals_u_5,negated_conjecture,
% 60.06/60.18 equalish(add(b,additive_inverse(a)),u) ).
% 60.06/60.18
% 60.06/60.18 cnf(not_less_or_equal_6,negated_conjecture,
% 60.06/60.18 ~ less_or_equal(additive_identity,u) ).
% 60.06/60.18
% 60.06/60.18 %--------------------------------------------------------------------------
% 60.06/60.18 %-------------------------------------------
% 60.06/60.18 % Proof found
% 60.06/60.18 % SZS status Theorem for theBenchmark
% 60.06/60.18 % SZS output start Proof
% 60.06/60.18 %ClaNum:33(EqnAxiom:0)
% 60.06/60.18 %VarNum:128(SingletonVarNum:50)
% 60.06/60.18 %MaxLitNum:4
% 60.06/60.18 %MaxfuncDepth:2
% 60.06/60.18 %SharedTerms:16
% 60.06/60.18 %goalClause: 6 7 9
% 60.06/60.18 %singleGoalClaCount:3
% 60.06/60.18 [1]P1(a1)
% 60.06/60.18 [2]P1(a4)
% 60.06/60.18 [3]P1(a2)
% 60.06/60.18 [4]P1(a5)
% 60.06/60.18 [5]P1(a7)
% 60.06/60.18 [6]P2(a2,a5)
% 60.06/60.18 [8]~P3(a1,a4)
% 60.06/60.18 [9]~P2(a1,a7)
% 60.06/60.18 [7]P3(f3(a5,f6(a2)),a7)
% 60.06/60.18 [11]~P1(x111)+P3(x111,x111)
% 60.06/60.18 [10]~P1(x101)+P1(f6(x101))
% 60.06/60.18 [15]~P1(x151)+P3(f3(a1,x151),x151)
% 60.06/60.18 [16]~P1(x161)+P3(f9(a4,x161),x161)
% 60.06/60.18 [19]~P1(x191)+P3(f3(x191,f6(x191)),a1)
% 60.06/60.18 [13]~P3(x132,x131)+P3(x131,x132)
% 60.06/60.18 [12]~P1(x121)+P3(x121,a1)+P1(f8(x121))
% 60.06/60.18 [24]~P1(x241)+P3(x241,a1)+P3(f9(x241,f8(x241)),a4)
% 60.06/60.18 [21]~P2(x212,x211)+~P2(x211,x212)+P3(x211,x212)
% 60.06/60.18 [17]~P1(x172)+~P1(x171)+P1(f3(x171,x172))
% 60.06/60.18 [18]~P1(x182)+~P1(x181)+P1(f9(x181,x182))
% 60.06/60.18 [25]~P2(a1,x252)+~P2(a1,x251)+P2(a1,f9(x251,x252))
% 60.06/60.18 [26]~P1(x262)+~P1(x261)+P3(f3(x261,x262),f3(x262,x261))
% 60.06/60.18 [27]~P1(x272)+~P1(x271)+P3(f9(x271,x272),f9(x272,x271))
% 60.06/60.18 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 60.06/60.18 [22]~P2(x223,x222)+P2(x221,x222)+~P3(x223,x221)
% 60.06/60.18 [23]~P2(x231,x233)+P2(x231,x232)+~P2(x233,x232)
% 60.06/60.18 [28]~P1(x282)+~P3(x281,x283)+P3(f3(x281,x282),f3(x283,x282))
% 60.06/60.18 [29]~P1(x292)+~P3(x291,x293)+P3(f9(x291,x292),f9(x293,x292))
% 60.06/60.18 [30]~P1(x302)+~P2(x301,x303)+P2(f3(x301,x302),f3(x303,x302))
% 60.06/60.18 [14]P2(x142,x141)+~P1(x141)+~P1(x142)+P2(x141,x142)
% 60.06/60.18 [31]~P1(x313)+~P1(x312)+~P1(x311)+P3(f3(x311,f3(x312,x313)),f3(f3(x311,x312),x313))
% 60.06/60.18 [32]~P1(x323)+~P1(x322)+~P1(x321)+P3(f9(x321,f9(x322,x323)),f9(f9(x321,x322),x323))
% 60.06/60.18 [33]~P1(x333)+~P1(x332)+~P1(x331)+P3(f3(f9(x331,x332),f9(x333,x332)),f9(f3(x331,x333),x332))
% 60.06/60.18 %EqnAxiom
% 60.06/60.18
% 60.06/60.18 %-------------------------------------------
% 60.06/60.19 cnf(34,plain,
% 60.06/60.19 (~P3(a4,a1)),
% 60.06/60.19 inference(scs_inference,[],[8,13])).
% 60.06/60.19 cnf(36,plain,
% 60.06/60.19 (P2(a1,a1)),
% 60.06/60.19 inference(scs_inference,[],[1,8,13,14])).
% 60.06/60.19 cnf(45,plain,
% 60.06/60.19 (P2(a4,a4)),
% 60.06/60.19 inference(scs_inference,[],[2,36,21,14])).
% 60.06/60.20 cnf(54,plain,
% 60.06/60.20 (P2(a2,a2)),
% 60.06/60.20 inference(scs_inference,[],[3,45,21,14])).
% 60.06/60.20 cnf(56,plain,
% 60.06/60.20 (~P2(f3(a5,f6(a2)),x561)+P2(a7,x561)),
% 60.06/60.20 inference(scs_inference,[],[7,3,45,21,14,22])).
% 60.06/60.20 cnf(61,plain,
% 60.06/60.20 (P2(a5,a5)),
% 60.06/60.20 inference(scs_inference,[],[4,54,21,14])).
% 60.06/60.20 cnf(63,plain,
% 60.06/60.20 (~P3(x631,f3(a5,f6(a2)))+P3(x631,a7)),
% 60.06/60.20 inference(scs_inference,[],[7,4,54,21,14,20])).
% 60.06/60.20 cnf(69,plain,
% 60.06/60.20 (P2(a7,a7)),
% 60.06/60.20 inference(scs_inference,[],[61,5,21,14])).
% 60.06/60.20 cnf(119,plain,
% 60.06/60.20 (P2(a7,a1)),
% 60.06/60.20 inference(scs_inference,[],[9,5,1,14])).
% 60.06/60.20 cnf(121,plain,
% 60.06/60.20 (~P1(f6(a2))+P2(a7,f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[61,56,30])).
% 60.06/60.20 cnf(124,plain,
% 60.06/60.20 (P2(a7,f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[3,121,10])).
% 60.06/60.20 cnf(127,plain,
% 60.06/60.20 (~P2(f3(a5,f6(a2)),a7)+P2(f3(a5,f6(a2)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[124,21,22])).
% 60.06/60.20 cnf(179,plain,
% 60.06/60.20 (~P3(a7,f3(a5,f6(a2)))+P2(f3(a5,f6(a2)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[69,127,22])).
% 60.06/60.20 cnf(436,plain,
% 60.06/60.20 (P2(f3(a2,f6(a2)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[3,6,10,30])).
% 60.06/60.20 cnf(437,plain,
% 60.06/60.20 (~P2(x4371,f3(a2,f6(a2)))+P2(x4371,f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[436,23])).
% 60.06/60.20 cnf(459,plain,
% 60.06/60.20 (P3(f3(a1,f6(a4)),f6(a4))),
% 60.06/60.20 inference(scs_inference,[],[2,10,15])).
% 60.06/60.20 cnf(731,plain,
% 60.06/60.20 (P1(f6(f9(a1,a1)))),
% 60.06/60.20 inference(scs_inference,[],[1,10,18])).
% 60.06/60.20 cnf(834,plain,
% 60.06/60.20 (P3(f9(f3(a1,f6(a4)),f6(a4)),f9(f6(a4),f6(a4)))),
% 60.06/60.20 inference(scs_inference,[],[2,459,10,29])).
% 60.06/60.20 cnf(837,plain,
% 60.06/60.20 (~P2(f9(f3(a1,f6(a4)),f6(a4)),f3(a2,f6(a2)))+P2(f9(f6(a4),f6(a4)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[834,22,437])).
% 60.06/60.20 cnf(854,plain,
% 60.06/60.20 (~P2(f3(a5,f6(a2)),x8541)+P2(f9(f6(a4),f6(a4)),x8541)+~P2(f9(f3(a1,f6(a4)),f6(a4)),f3(a2,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[837,23])).
% 60.06/60.20 cnf(931,plain,
% 60.06/60.20 (P3(f8(a4),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[34,2,11,12])).
% 60.06/60.20 cnf(940,plain,
% 60.06/60.20 (P2(f3(a5,f6(a2)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[7,13,179])).
% 60.06/60.20 cnf(941,plain,
% 60.06/60.20 (P3(f3(a5,f6(a2)),f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[940,21])).
% 60.06/60.20 cnf(1014,plain,
% 60.06/60.20 (P3(a4,f9(a4,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,13,16])).
% 60.06/60.20 cnf(1015,plain,
% 60.06/60.20 (P2(f9(a4,a4),a4)),
% 60.06/60.20 inference(scs_inference,[],[45,1014,22])).
% 60.06/60.20 cnf(1048,plain,
% 60.06/60.20 (P3(a1,f3(a4,f6(a4)))),
% 60.06/60.20 inference(scs_inference,[],[2,13,19])).
% 60.06/60.20 cnf(1106,plain,
% 60.06/60.20 (P3(a7,f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[941,13,63])).
% 60.06/60.20 cnf(1122,plain,
% 60.06/60.20 (P2(f3(a5,f6(a2)),a1)),
% 60.06/60.20 inference(scs_inference,[],[119,1106,22])).
% 60.06/60.20 cnf(1151,plain,
% 60.06/60.20 (P1(f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[8,2,13,12])).
% 60.06/60.20 cnf(1171,plain,
% 60.06/60.20 (P2(f3(a2,f6(a2)),a1)),
% 60.06/60.20 inference(scs_inference,[],[436,1122,23])).
% 60.06/60.20 cnf(1216,plain,
% 60.06/60.20 (P3(a4,f9(a4,f8(a4)))),
% 60.06/60.20 inference(scs_inference,[],[34,2,13,24])).
% 60.06/60.20 cnf(1217,plain,
% 60.06/60.20 (P2(f9(a4,f8(a4)),a4)),
% 60.06/60.20 inference(scs_inference,[],[45,1216,22])).
% 60.06/60.20 cnf(1316,plain,
% 60.06/60.20 (P2(f3(a5,f6(a2)),a7)),
% 60.06/60.20 inference(scs_inference,[],[69,1106,22])).
% 60.06/60.20 cnf(1320,plain,
% 60.06/60.20 (~P2(a1,f3(a5,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[69,9,1106,22,854,23])).
% 60.06/60.20 cnf(1325,plain,
% 60.06/60.20 (~P2(a1,f3(a2,f6(a2)))),
% 60.06/60.20 inference(scs_inference,[],[1320,436,23])).
% 60.06/60.20 cnf(1680,plain,
% 60.06/60.20 (~P3(a1,f3(a1,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,8,15,20])).
% 60.06/60.20 cnf(1683,plain,
% 60.06/60.20 (P3(f3(a1,f8(a4)),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[34,2,15,12])).
% 60.06/60.20 cnf(1684,plain,
% 60.06/60.20 (~P2(f3(a1,f8(a4)),x16841)+P2(f8(a4),x16841)),
% 60.06/60.20 inference(scs_inference,[],[1683,22])).
% 60.06/60.20 cnf(1690,plain,
% 60.06/60.20 (~P3(x16901,f3(a1,f8(a4)))+P3(x16901,f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[1683,20])).
% 60.06/60.20 cnf(1696,plain,
% 60.06/60.20 (P3(f3(f8(a4),a1),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[1,1151,1690,26])).
% 60.06/60.20 cnf(1703,plain,
% 60.06/60.20 (~P3(x17031,f3(f8(a4),a1))+P3(x17031,f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[1696,20])).
% 60.06/60.20 cnf(1709,plain,
% 60.06/60.20 (P3(f8(a4),x17091)+~P3(x17091,f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[1703,13])).
% 60.06/60.20 cnf(1710,plain,
% 60.06/60.20 (P3(f8(a4),f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[931,1,1709,28])).
% 60.06/60.20 cnf(1754,plain,
% 60.06/60.20 (P3(f3(a1,a4),f9(a4,f8(a4)))),
% 60.06/60.20 inference(scs_inference,[],[2,1216,15,20])).
% 60.06/60.20 cnf(1801,plain,
% 60.06/60.20 (P3(f3(a1,f8(a4)),f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[1683,1710,20])).
% 60.06/60.20 cnf(1803,plain,
% 60.06/60.20 (~P2(f3(a1,f8(a4)),x18031)+P2(f3(f8(a4),a1),x18031)),
% 60.06/60.20 inference(scs_inference,[],[1683,1710,20,22])).
% 60.06/60.20 cnf(1834,plain,
% 60.06/60.20 (P3(f3(a1,f9(a4,a4)),f9(a4,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,15,18])).
% 60.06/60.20 cnf(1862,plain,
% 60.06/60.20 (P3(f9(f3(a1,a4),a4),f9(a4,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,15,29])).
% 60.06/60.20 cnf(1917,plain,
% 60.06/60.20 (~P3(a1,f9(a4,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,8,16,20])).
% 60.06/60.20 cnf(1920,plain,
% 60.06/60.20 (~P3(a1,f3(a1,f9(a4,a4)))),
% 60.06/60.20 inference(scs_inference,[],[1834,1917,13,20])).
% 60.06/60.20 cnf(1922,plain,
% 60.06/60.20 (P3(f9(a4,f8(a4)),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[34,2,16,12])).
% 60.06/60.20 cnf(1927,plain,
% 60.06/60.20 (~P3(a1,f9(f3(a1,a4),a4))),
% 60.06/60.20 inference(scs_inference,[],[1217,1862,1920,1922,1917,13,22,20])).
% 60.06/60.20 cnf(1936,plain,
% 60.06/60.20 (P3(a4,f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[1216,1927,1922,13,20])).
% 60.06/60.20 cnf(2052,plain,
% 60.06/60.20 (P3(f3(a1,a4),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[1754,1922,20])).
% 60.06/60.20 cnf(2091,plain,
% 60.06/60.20 (P3(f9(a4,f8(a4)),f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[1922,1710,20])).
% 60.06/60.20 cnf(2094,plain,
% 60.06/60.20 (P3(a4,f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[1216,2091,20])).
% 60.06/60.20 cnf(2108,plain,
% 60.06/60.20 (P3(f3(a1,a4),f3(f8(a4),a1))),
% 60.06/60.20 inference(scs_inference,[],[2052,1710,20])).
% 60.06/60.20 cnf(2182,plain,
% 60.06/60.20 (P3(f3(f8(a4),f6(f8(a4))),a1)),
% 60.06/60.20 inference(scs_inference,[],[34,2,19,12])).
% 60.06/60.20 cnf(2185,plain,
% 60.06/60.20 (~P3(a4,f3(f8(a4),f6(f8(a4))))),
% 60.06/60.20 inference(scs_inference,[],[9,34,2182,22,20])).
% 60.06/60.20 cnf(2189,plain,
% 60.06/60.20 (~P2(f3(a4,f6(a4)),a7)),
% 60.06/60.20 inference(scs_inference,[],[2,9,19,22])).
% 60.06/60.20 cnf(2197,plain,
% 60.06/60.20 (P3(f3(f3(a4,f6(a4)),a4),f3(a1,a4))),
% 60.06/60.20 inference(scs_inference,[],[2,19,28])).
% 60.06/60.20 cnf(2200,plain,
% 60.06/60.20 (~P3(f3(f3(a4,f6(a4)),a4),a1)),
% 60.06/60.20 inference(scs_inference,[],[1680,2197,20,13])).
% 60.06/60.20 cnf(2251,plain,
% 60.06/60.20 (P3(f3(f3(a4,f6(a4)),a4),f8(a4))),
% 60.06/60.20 inference(scs_inference,[],[2052,2197,20])).
% 60.06/60.20 cnf(2324,plain,
% 60.06/60.20 (P3(f3(a1,a7),a7)),
% 60.06/60.20 inference(scs_inference,[],[731,5,10,15])).
% 60.06/60.20 cnf(2326,plain,
% 60.06/60.20 (P3(f9(a4,a7),a7)),
% 60.06/60.20 inference(scs_inference,[],[731,5,10,15,16])).
% 60.06/60.21 cnf(2330,plain,
% 60.06/60.21 (P3(f8(a4),f3(a1,a4))),
% 60.06/60.21 inference(scs_inference,[],[2108,731,5,10,15,16,19,1709])).
% 60.06/60.21 cnf(2332,plain,
% 60.06/60.21 (P3(f3(f8(a4),a1),f3(a1,a4))),
% 60.06/60.21 inference(scs_inference,[],[2108,731,5,10,15,16,19,1709,13])).
% 60.06/60.21 cnf(2334,plain,
% 60.06/60.21 (P1(f9(f8(a4),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[2108,731,1151,5,10,15,16,19,1709,13,18])).
% 60.06/60.21 cnf(2346,plain,
% 60.06/60.21 (P2(a1,f9(a1,a1))),
% 60.06/60.21 inference(scs_inference,[],[7,2108,731,36,1151,5,10,15,16,19,1709,13,18,26,27,28,29,17,25])).
% 60.06/60.21 cnf(2348,plain,
% 60.06/60.21 (P2(f3(a2,f6(a2)),a7)),
% 60.06/60.21 inference(scs_inference,[],[7,2108,731,36,436,1151,1316,5,10,15,16,19,1709,13,18,26,27,28,29,17,25,23])).
% 60.06/60.21 cnf(2350,plain,
% 60.06/60.21 (~P3(a7,a1)),
% 60.06/60.21 inference(scs_inference,[],[7,2108,1320,124,731,36,436,1151,1316,5,10,15,16,19,1709,13,18,26,27,28,29,17,25,23,22])).
% 60.06/60.21 cnf(2352,plain,
% 60.06/60.21 (~P3(f8(a4),f3(f8(a4),f6(f8(a4))))),
% 60.06/60.21 inference(scs_inference,[],[7,2108,2185,1936,1320,124,731,36,436,1151,1316,5,10,15,16,19,1709,13,18,26,27,28,29,17,25,23,22,20])).
% 60.06/60.21 cnf(2369,plain,
% 60.06/60.21 (P3(f9(a4,a5),a5)),
% 60.06/60.21 inference(scs_inference,[],[2334,4,10,16])).
% 60.06/60.21 cnf(2371,plain,
% 60.06/60.21 (P3(f8(a4),a4)),
% 60.06/60.21 inference(scs_inference,[],[2334,2094,4,10,16,1709])).
% 60.06/60.21 cnf(2373,plain,
% 60.06/60.21 (P3(f3(a1,a5),a5)),
% 60.06/60.21 inference(scs_inference,[],[2334,2094,4,10,16,1709,15])).
% 60.06/60.21 cnf(2383,plain,
% 60.06/60.21 (P1(f9(a5,a5))),
% 60.06/60.21 inference(scs_inference,[],[7,2324,2334,2094,4,10,16,1709,15,19,13,26,28,18])).
% 60.06/60.21 cnf(2387,plain,
% 60.06/60.21 (P1(f8(a7))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2324,2334,2094,4,5,10,16,1709,15,19,13,26,28,18,27,12])).
% 60.06/60.21 cnf(2389,plain,
% 60.06/60.21 (P1(f3(a5,a5))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2324,2334,2094,4,5,10,16,1709,15,19,13,26,28,18,27,12,17])).
% 60.06/60.21 cnf(2391,plain,
% 60.06/60.21 (P2(a1,f9(f9(a1,a1),f9(a1,a1)))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2346,2324,2334,2094,4,5,10,16,1709,15,19,13,26,28,18,27,12,17,25])).
% 60.06/60.21 cnf(2397,plain,
% 60.06/60.21 (~P3(f3(a2,f6(a2)),f3(a4,f6(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2346,2324,1325,2189,2334,2348,2094,1151,4,5,10,16,1709,15,19,13,26,28,18,27,12,17,25,30,23,22])).
% 60.06/60.21 cnf(2407,plain,
% 60.06/60.21 (P2(f8(a4),f3(f9(a1,a1),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2330,2346,2324,1325,2189,2334,2348,2352,2094,1151,4,5,10,16,1709,15,19,13,26,28,18,27,12,17,25,30,23,22,20,32,33,31,1684])).
% 60.06/60.21 cnf(2409,plain,
% 60.06/60.21 (P2(f3(f8(a4),a1),f3(f9(a1,a1),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2350,2330,2346,2324,1325,2189,2334,2348,2352,2094,1151,4,5,10,16,1709,15,19,13,26,28,18,27,12,17,25,30,23,22,20,32,33,31,1684,1803])).
% 60.06/60.21 cnf(2440,plain,
% 60.06/60.21 (P1(f9(f3(a5,a5),f3(a5,a5)))),
% 60.06/60.21 inference(scs_inference,[],[7,2389,2326,1801,10,1709,16,15,19,11,13,29,28,26,27,18])).
% 60.06/60.21 cnf(2448,plain,
% 60.06/60.21 (P2(a4,f3(f9(a1,a1),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2371,2389,2326,2407,2391,1801,1325,10,1709,16,15,19,11,13,29,28,26,27,18,17,30,23,22])).
% 60.06/60.21 cnf(2450,plain,
% 60.06/60.21 (~P3(f8(a4),a1)),
% 60.06/60.21 inference(scs_inference,[],[7,2371,2389,2326,2407,2391,2200,1801,1325,2251,10,1709,16,15,19,11,13,29,28,26,27,18,17,30,23,22,20])).
% 60.06/60.21 cnf(2460,plain,
% 60.06/60.21 (P1(f8(f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2371,2389,2326,2407,2391,2200,1801,1325,2251,1151,1,10,1709,16,15,19,11,13,29,28,26,27,18,17,30,23,22,20,32,33,31,24,12])).
% 60.06/60.21 cnf(2467,plain,
% 60.06/60.21 (P1(f6(f9(a5,a5)))),
% 60.06/60.21 inference(scs_inference,[],[2383,10])).
% 60.06/60.21 cnf(2469,plain,
% 60.06/60.21 (P3(f9(a4,f9(a5,a5)),f9(a5,a5))),
% 60.06/60.21 inference(scs_inference,[],[2383,10,16])).
% 60.06/60.21 cnf(2473,plain,
% 60.06/60.21 (P3(f3(a1,f9(a5,a5)),f9(a5,a5))),
% 60.06/60.21 inference(scs_inference,[],[2383,2091,10,16,1709,15])).
% 60.06/60.21 cnf(2491,plain,
% 60.06/60.21 (P1(f9(f9(a5,a5),f9(a5,a5)))),
% 60.06/60.21 inference(scs_inference,[],[7,2450,2383,2369,2460,2091,1151,10,16,1709,15,19,11,13,29,26,24,28,27,18])).
% 60.06/60.21 cnf(2499,plain,
% 60.06/60.21 (P2(f3(a1,a4),f3(f9(a1,a1),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2450,2383,2369,2332,2460,2448,2409,2391,2091,1171,1151,10,16,1709,15,19,11,13,29,26,24,28,27,18,17,30,23,22])).
% 60.06/60.21 cnf(2520,plain,
% 60.06/60.21 (P1(f6(f8(a7)))),
% 60.06/60.21 inference(scs_inference,[],[2387,16,15,19,10])).
% 60.06/60.21 cnf(2540,plain,
% 60.06/60.21 (~P2(f9(f9(a1,a1),f9(a1,a1)),f3(a5,f6(a2)))),
% 60.06/60.21 inference(scs_inference,[],[7,2387,2373,2467,2499,2391,1320,16,15,19,10,11,13,29,26,28,27,18,17,30,23])).
% 60.06/60.21 cnf(2557,plain,
% 60.06/60.21 (P3(f3(a1,a1),a1)),
% 60.06/60.21 inference(scs_inference,[],[1,15])).
% 60.06/60.21 cnf(2563,plain,
% 60.06/60.21 (P3(f9(a4,a1),a1)),
% 60.06/60.21 inference(scs_inference,[],[2491,1,15,10,19,16])).
% 60.06/60.21 cnf(2575,plain,
% 60.06/60.21 (P1(f9(a7,a7))),
% 60.06/60.21 inference(scs_inference,[],[7,2469,2491,2520,5,1,15,10,19,16,11,13,29,26,27,18])).
% 60.06/60.21 cnf(2577,plain,
% 60.06/60.21 (P1(f3(a7,a7))),
% 60.06/60.21 inference(scs_inference,[],[7,2469,2491,2520,5,1,15,10,19,16,11,13,29,26,27,18,17])).
% 60.06/60.21 cnf(2579,plain,
% 60.06/60.21 (P2(f3(a2,f6(a2)),f9(a1,a1))),
% 60.06/60.21 inference(scs_inference,[],[7,2469,2491,2520,1171,2346,5,1,15,10,19,16,11,13,29,26,27,18,17,23])).
% 60.06/60.21 cnf(2612,plain,
% 60.06/60.21 (P1(f3(f3(a7,a7),f3(a7,a7)))),
% 60.06/60.21 inference(scs_inference,[],[7,2577,2557,2440,10,16,15,19,13,26,29,27,28,18,17])).
% 60.06/60.21 cnf(2616,plain,
% 60.06/60.21 (~P2(f9(f9(a1,a1),f9(a1,a1)),a7)),
% 60.06/60.21 inference(scs_inference,[],[7,2577,2557,2579,2440,2540,124,10,16,15,19,13,26,29,27,28,18,17,30,23])).
% 60.06/60.21 cnf(2645,plain,
% 60.06/60.21 (P1(f9(f9(a7,a7),f9(a7,a7)))),
% 60.06/60.21 inference(scs_inference,[],[7,2563,2612,2575,16,19,10,15,13,26,29,28,27,18])).
% 60.06/60.21 cnf(2649,plain,
% 60.06/60.21 (P2(f9(a4,a4),f3(f9(a1,a1),f8(a4)))),
% 60.06/60.21 inference(scs_inference,[],[7,2563,2612,2448,2575,1015,16,19,10,15,13,26,29,28,27,18,17,23])).
% 60.06/60.21 cnf(2682,plain,
% 60.06/60.21 ($false),
% 60.06/60.21 inference(scs_inference,[],[2473,2645,2649,2616,2397,2348,1048,2575,1,3,19,15,10,16,13,26,27,18,17,30,22,20]),
% 60.06/60.21 ['proof']).
% 60.06/60.21 % SZS output end Proof
% 60.06/60.21 % Total time :59.470000s
%------------------------------------------------------------------------------