%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD031-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 : n014.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:19 EDT 2024
% Result : Unsatisfiable 125.31s 125.41s
% Output : CNFRefutation 125.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : FLD031-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Jun 19 10:44:09 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.48/0.58 start to proof:theBenchmark
% 125.31/125.40 %-------------------------------------------
% 125.31/125.40 % File :CSE---1.7
% 125.31/125.40 % Problem :theBenchmark
% 125.31/125.40 % Transform :cnf
% 125.31/125.40 % Format :tptp:raw
% 125.31/125.40 % Command :java -jar mcs_scs.jar %d %s
% 125.31/125.40
% 125.31/125.40 % Result :Theorem 124.720000s
% 125.31/125.40 % Output :CNFRefutation 124.720000s
% 125.31/125.40 %-------------------------------------------
% 125.31/125.41 %--------------------------------------------------------------------------
% 125.31/125.41 % File : FLD031-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 125.31/125.41 % Domain : Field Theory (Ordered fields)
% 125.31/125.41 % Problem : If a is one, then the multiplicative inverse of a is also one
% 125.31/125.41 % Version : [Dra93] axioms : Especial.
% 125.31/125.41 % Theorem formulation : Functional with glxx axiom set.
% 125.31/125.41 % English :
% 125.31/125.41
% 125.31/125.41 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 125.31/125.41 % Source : [Dra93]
% 125.31/125.41 % Names :
% 125.31/125.41
% 125.31/125.41 % Status : Unsatisfiable
% 125.31/125.41 % Rating : 0.00 v8.1.0, 0.14 v7.5.0, 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.38 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.29 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
% 125.31/125.41 % Syntax : Number of clauses : 31 ( 7 unt; 3 nHn; 31 RR)
% 125.31/125.41 % Number of literals : 77 ( 0 equ; 46 neg)
% 125.31/125.41 % Maximal clause size : 4 ( 2 avg)
% 125.31/125.41 % Maximal term depth : 3 ( 1 avg)
% 125.31/125.41 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 125.31/125.41 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 125.31/125.41 % Number of variables : 50 ( 0 sgn)
% 125.31/125.41 % SPC : CNF_UNS_RFO_NEQ_NHN
% 125.31/125.41
% 125.31/125.41 % Comments :
% 125.31/125.41 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 125.31/125.41 %--------------------------------------------------------------------------
% 125.31/125.41 include('Axioms/FLD001-0.ax').
% 125.31/125.41 %--------------------------------------------------------------------------
% 125.31/125.41 cnf(a_is_defined,hypothesis,
% 125.31/125.41 defined(a) ).
% 125.31/125.41
% 125.31/125.41 cnf(a_equals_multiplicative_identity_2,negated_conjecture,
% 125.31/125.41 equalish(a,multiplicative_identity) ).
% 125.31/125.41
% 125.31/125.41 cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
% 125.31/125.41 ~ equalish(a,additive_identity) ).
% 125.31/125.41
% 125.31/125.41 cnf(multiplicative_inverses_not_equal,negated_conjecture,
% 125.31/125.41 ~ equalish(multiplicative_inverse(a),multiplicative_identity) ).
% 125.31/125.41
% 125.31/125.41 %--------------------------------------------------------------------------
% 125.31/125.41 %-------------------------------------------
% 125.31/125.41 % Proof found
% 125.31/125.41 % SZS status Theorem for theBenchmark
% 125.31/125.41 % SZS output start Proof
% 125.31/125.42 %ClaNum:31(EqnAxiom:0)
% 125.31/125.42 %VarNum:128(SingletonVarNum:50)
% 125.31/125.42 %MaxLitNum:4
% 125.31/125.42 %MaxfuncDepth:2
% 125.31/125.42 %SharedTerms:11
% 125.31/125.42 %goalClause: 4 6 7
% 125.31/125.42 %singleGoalClaCount:3
% 125.31/125.42 [1]P1(a1)
% 125.31/125.42 [2]P1(a4)
% 125.31/125.42 [3]P1(a2)
% 125.31/125.42 [4]P2(a2,a4)
% 125.31/125.42 [5]~P2(a1,a4)
% 125.31/125.42 [6]~P2(a2,a1)
% 125.31/125.42 [7]~P2(f6(a2),a4)
% 125.31/125.42 [9]~P1(x91)+P2(x91,x91)
% 125.31/125.42 [8]~P1(x81)+P1(f5(x81))
% 125.31/125.42 [13]~P1(x131)+P2(f3(a1,x131),x131)
% 125.31/125.42 [14]~P1(x141)+P2(f7(a4,x141),x141)
% 125.31/125.42 [17]~P1(x171)+P2(f3(x171,f5(x171)),a1)
% 125.31/125.42 [11]~P2(x112,x111)+P2(x111,x112)
% 125.31/125.42 [10]~P1(x101)+P2(x101,a1)+P1(f6(x101))
% 125.31/125.42 [22]~P1(x221)+P2(x221,a1)+P2(f7(x221,f6(x221)),a4)
% 125.31/125.42 [19]~P3(x192,x191)+~P3(x191,x192)+P2(x191,x192)
% 125.31/125.42 [15]~P1(x152)+~P1(x151)+P1(f3(x151,x152))
% 125.31/125.42 [16]~P1(x162)+~P1(x161)+P1(f7(x161,x162))
% 125.31/125.42 [23]~P3(a1,x232)+~P3(a1,x231)+P3(a1,f7(x231,x232))
% 125.31/125.42 [24]~P1(x242)+~P1(x241)+P2(f3(x241,x242),f3(x242,x241))
% 125.31/125.42 [25]~P1(x252)+~P1(x251)+P2(f7(x251,x252),f7(x252,x251))
% 125.31/125.42 [18]~P2(x181,x183)+P2(x181,x182)+~P2(x183,x182)
% 125.31/125.42 [20]~P3(x203,x202)+P3(x201,x202)+~P2(x203,x201)
% 125.31/125.42 [21]~P3(x211,x213)+P3(x211,x212)+~P3(x213,x212)
% 125.31/125.42 [26]~P1(x262)+~P2(x261,x263)+P2(f3(x261,x262),f3(x263,x262))
% 125.31/125.42 [27]~P1(x272)+~P2(x271,x273)+P2(f7(x271,x272),f7(x273,x272))
% 125.31/125.42 [28]~P1(x282)+~P3(x281,x283)+P3(f3(x281,x282),f3(x283,x282))
% 125.31/125.42 [12]P3(x122,x121)+~P1(x121)+~P1(x122)+P3(x121,x122)
% 125.31/125.42 [29]~P1(x293)+~P1(x292)+~P1(x291)+P2(f3(x291,f3(x292,x293)),f3(f3(x291,x292),x293))
% 125.31/125.42 [30]~P1(x303)+~P1(x302)+~P1(x301)+P2(f7(x301,f7(x302,x303)),f7(f7(x301,x302),x303))
% 125.31/125.42 [31]~P1(x313)+~P1(x312)+~P1(x311)+P2(f3(f7(x311,x312),f7(x313,x312)),f7(f3(x311,x313),x312))
% 125.31/125.42 %EqnAxiom
% 125.31/125.42
% 125.31/125.42 %-------------------------------------------
% 125.31/125.43 cnf(32,plain,
% 125.31/125.43 (~P2(a1,a2)),
% 125.31/125.43 inference(scs_inference,[],[6,11])).
% 125.31/125.43 cnf(34,plain,
% 125.31/125.43 (~P2(f6(a2),a2)),
% 125.31/125.43 inference(scs_inference,[],[4,6,7,11,18])).
% 125.31/125.43 cnf(36,plain,
% 125.31/125.43 (P3(a1,a1)),
% 125.31/125.43 inference(scs_inference,[],[4,6,7,1,11,18,12])).
% 125.31/125.43 cnf(38,plain,
% 125.31/125.43 (~P3(a2,x381)+P3(a4,x381)),
% 125.31/125.43 inference(scs_inference,[],[4,6,7,1,11,18,12,20])).
% 125.31/125.43 cnf(44,plain,
% 125.31/125.43 (P3(a4,a4)),
% 125.31/125.43 inference(scs_inference,[],[7,2,11,12])).
% 125.31/125.43 cnf(50,plain,
% 125.31/125.43 (P3(a2,a2)),
% 125.31/125.43 inference(scs_inference,[],[34,3,11,12])).
% 125.31/125.43 cnf(52,plain,
% 125.31/125.43 (P3(a4,a2)),
% 125.31/125.43 inference(scs_inference,[],[4,34,3,11,12,20])).
% 125.31/125.43 cnf(56,plain,
% 125.31/125.43 (~P2(a4,a1)),
% 125.31/125.43 inference(scs_inference,[],[5,11])).
% 125.31/125.43 cnf(69,plain,
% 125.31/125.43 (P3(f3(a4,a4),f3(a2,a4))),
% 125.31/125.43 inference(scs_inference,[],[50,2,38,28])).
% 125.31/125.43 cnf(70,plain,
% 125.31/125.43 (~P3(x701,f3(a4,a4))+P3(x701,f3(a2,a4))),
% 125.31/125.43 inference(scs_inference,[],[69,21])).
% 125.31/125.43 cnf(79,plain,
% 125.31/125.43 (P2(f3(a1,f5(a1)),f5(a1))),
% 125.31/125.43 inference(scs_inference,[],[1,13,8])).
% 125.31/125.43 cnf(93,plain,
% 125.31/125.43 (P3(f5(a1),f3(a2,a4))+~P3(f3(a1,f5(a1)),f3(a4,a4))),
% 125.31/125.43 inference(scs_inference,[],[79,20,70])).
% 125.31/125.43 cnf(136,plain,
% 125.31/125.43 (~P3(f3(a1,f5(a1)),f3(a4,a4))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[3,93,28])).
% 125.31/125.43 cnf(151,plain,
% 125.31/125.43 (~P2(x1511,f3(a1,f5(a1)))+~P3(x1511,f3(a4,a4))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[136,20])).
% 125.31/125.43 cnf(153,plain,
% 125.31/125.43 (P1(f3(f5(a1),f5(a1)))),
% 125.31/125.43 inference(scs_inference,[],[1,15,8])).
% 125.31/125.43 cnf(187,plain,
% 125.31/125.43 (~P1(f5(a1))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))+~P3(f3(f5(a1),a1),f3(a4,a4))),
% 125.31/125.43 inference(scs_inference,[],[1,151,24])).
% 125.31/125.43 cnf(189,plain,
% 125.31/125.43 (~P3(f3(f5(a1),a1),f3(a4,a4))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[1,187,8])).
% 125.31/125.43 cnf(190,plain,
% 125.31/125.43 (~P2(x1901,f3(f5(a1),a1))+~P3(x1901,f3(a4,a4))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[189,20])).
% 125.31/125.43 cnf(191,plain,
% 125.31/125.43 (~P2(f3(a4,a4),f3(f5(a1),a1))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[44,2,190,28])).
% 125.31/125.43 cnf(192,plain,
% 125.31/125.43 (~P2(f3(f5(a1),a1),f3(a4,a4))+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[191,11])).
% 125.31/125.43 cnf(193,plain,
% 125.31/125.43 (~P2(x1931,f3(a4,a4))+~P2(f3(f5(a1),a1),x1931)+P3(f3(f5(a1),a2),f3(f3(a2,a4),a2))),
% 125.31/125.43 inference(scs_inference,[],[192,18])).
% 125.31/125.43 cnf(249,plain,
% 125.31/125.43 (P2(f3(a1,f5(a2)),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[3,8,13])).
% 125.31/125.43 cnf(258,plain,
% 125.31/125.43 (~P2(x2581,f3(a1,f5(a2)))+P2(x2581,f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[249,18])).
% 125.31/125.43 cnf(260,plain,
% 125.31/125.43 (~P2(a4,f3(a1,f5(a2)))+P3(f5(a2),a2)),
% 125.31/125.43 inference(scs_inference,[],[52,249,18,20])).
% 125.31/125.43 cnf(264,plain,
% 125.31/125.43 (~P1(f3(a1,f5(a2)))+P2(f7(a4,f3(a1,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[258,14])).
% 125.31/125.43 cnf(265,plain,
% 125.31/125.43 (~P2(f3(a1,f5(a2)),a4)+P3(f5(a2),a2)),
% 125.31/125.43 inference(scs_inference,[],[260,11])).
% 125.31/125.43 cnf(266,plain,
% 125.31/125.43 (~P3(x2661,f5(a2))+P3(x2661,a2)+~P2(f3(a1,f5(a2)),a4)),
% 125.31/125.43 inference(scs_inference,[],[265,21])).
% 125.31/125.43 cnf(269,plain,
% 125.31/125.43 (~P1(f5(a2))+P2(f7(a4,f3(a1,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[1,264,15])).
% 125.31/125.43 cnf(270,plain,
% 125.31/125.43 (P2(f5(a2),f7(a4,f3(a1,f5(a2))))+~P1(f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[269,11])).
% 125.31/125.43 cnf(276,plain,
% 125.31/125.43 (P1(f5(f7(a2,a2)))),
% 125.31/125.43 inference(scs_inference,[],[3,8,16])).
% 125.31/125.43 cnf(279,plain,
% 125.31/125.43 (P2(f7(a4,f5(a2)),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[3,8,14])).
% 125.31/125.43 cnf(288,plain,
% 125.31/125.43 (~P2(x2881,f7(a4,f5(a2)))+P2(x2881,f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[279,18])).
% 125.31/125.43 cnf(294,plain,
% 125.31/125.43 (~P1(f7(a4,f5(a2)))+P2(f3(a1,f7(a4,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[288,13])).
% 125.31/125.43 cnf(299,plain,
% 125.31/125.43 (~P1(f5(a2))+P2(f3(a1,f7(a4,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[2,294,16])).
% 125.31/125.43 cnf(300,plain,
% 125.31/125.43 (P2(f5(a2),f3(a1,f7(a4,f5(a2))))+~P1(f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[299,11])).
% 125.31/125.43 cnf(462,plain,
% 125.31/125.43 (P2(f5(a2),f7(a4,f3(a1,f5(a2))))),
% 125.31/125.43 inference(scs_inference,[],[3,8,270])).
% 125.31/125.43 cnf(463,plain,
% 125.31/125.43 (~P3(f5(a2),x4631)+P3(f7(a4,f3(a1,f5(a2))),x4631)),
% 125.31/125.43 inference(scs_inference,[],[462,20])).
% 125.31/125.43 cnf(532,plain,
% 125.31/125.43 (P2(f5(a2),f3(a1,f7(a4,f5(a2))))),
% 125.31/125.43 inference(scs_inference,[],[3,8,300])).
% 125.31/125.43 cnf(533,plain,
% 125.31/125.43 (~P3(f5(a2),x5331)+P3(f3(a1,f7(a4,f5(a2))),x5331)),
% 125.31/125.43 inference(scs_inference,[],[532,20])).
% 125.31/125.43 cnf(707,plain,
% 125.31/125.43 (P2(f3(a2,f5(a2)),f3(a4,f5(a2)))),
% 125.31/125.43 inference(scs_inference,[],[3,4,8,26])).
% 125.31/125.43 cnf(708,plain,
% 125.31/125.43 (~P2(x7081,f3(a2,f5(a2)))+P2(x7081,f3(a4,f5(a2)))),
% 125.31/125.43 inference(scs_inference,[],[707,18])).
% 125.31/125.43 cnf(713,plain,
% 125.31/125.43 (P2(f3(a4,f5(a2)),x7131)+~P2(x7131,f3(a2,f5(a2)))),
% 125.31/125.43 inference(scs_inference,[],[708,11])).
% 125.31/125.43 cnf(822,plain,
% 125.31/125.43 (P2(f7(a2,f5(a2)),f7(a4,f5(a2)))),
% 125.31/125.43 inference(scs_inference,[],[3,4,8,27])).
% 125.31/125.43 cnf(823,plain,
% 125.31/125.43 (P2(f7(a2,f5(a2)),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[279,822,18])).
% 125.31/125.43 cnf(835,plain,
% 125.31/125.43 (~P2(x8351,f7(a2,f5(a2)))+P2(x8351,f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[823,18])).
% 125.31/125.43 cnf(856,plain,
% 125.31/125.43 (~P1(f7(a2,f5(a2)))+P2(f3(a1,f7(a2,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[835,13])).
% 125.31/125.43 cnf(873,plain,
% 125.31/125.43 (~P1(f5(a2))+P2(f3(a1,f7(a2,f5(a2))),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[3,856,16])).
% 125.31/125.43 cnf(874,plain,
% 125.31/125.43 (P2(f5(a2),f3(a1,f7(a2,f5(a2))))+~P1(f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[873,11])).
% 125.31/125.43 cnf(950,plain,
% 125.31/125.43 (P2(f5(a2),f3(a1,f7(a2,f5(a2))))),
% 125.31/125.43 inference(scs_inference,[],[3,8,874])).
% 125.31/125.43 cnf(951,plain,
% 125.31/125.43 (~P3(f5(a2),x9511)+P3(f3(a1,f7(a2,f5(a2))),x9511)),
% 125.31/125.43 inference(scs_inference,[],[950,20])).
% 125.31/125.43 cnf(977,plain,
% 125.31/125.43 (P3(f5(a2),f5(a2))),
% 125.31/125.43 inference(scs_inference,[],[3,8,12])).
% 125.31/125.43 cnf(982,plain,
% 125.31/125.43 (P3(f7(a4,f3(a1,f5(a2))),f5(a2))),
% 125.31/125.44 inference(scs_inference,[],[977,951,533,463])).
% 125.31/125.44 cnf(1241,plain,
% 125.31/125.44 (P2(a2,f7(a4,a2))),
% 125.31/125.44 inference(scs_inference,[],[3,11,14])).
% 125.31/125.44 cnf(1306,plain,
% 125.31/125.44 (P2(a1,f3(a2,f5(a2)))),
% 125.31/125.44 inference(scs_inference,[],[3,11,17])).
% 125.31/125.44 cnf(1311,plain,
% 125.31/125.44 (P3(f3(a2,f5(a2)),a1)),
% 125.31/125.44 inference(scs_inference,[],[56,1306,36,713,18,20])).
% 125.31/125.44 cnf(1337,plain,
% 125.31/125.44 (P2(f7(a4,a2),f7(a2,a2))),
% 125.31/125.44 inference(scs_inference,[],[4,3,11,27])).
% 125.31/125.44 cnf(1338,plain,
% 125.31/125.44 (P2(a2,f7(a2,a2))),
% 125.31/125.44 inference(scs_inference,[],[1241,1337,18])).
% 125.31/125.44 cnf(1685,plain,
% 125.31/125.44 (P1(f6(a2))),
% 125.31/125.44 inference(scs_inference,[],[32,3,11,10])).
% 125.31/125.44 cnf(1688,plain,
% 125.31/125.44 (P2(f7(a2,f6(a2)),a4)),
% 125.31/125.44 inference(scs_inference,[],[32,3,11,22])).
% 125.31/125.44 cnf(1689,plain,
% 125.31/125.44 (~P2(f6(a2),f7(a2,f6(a2)))),
% 125.31/125.44 inference(scs_inference,[],[7,1688,18])).
% 125.31/125.44 cnf(1709,plain,
% 125.31/125.44 (P2(a4,f7(a4,f6(a4)))),
% 125.31/125.44 inference(scs_inference,[],[56,2,11,22])).
% 125.31/125.44 cnf(1710,plain,
% 125.31/125.44 (P2(a2,f7(a4,f6(a4)))),
% 125.31/125.44 inference(scs_inference,[],[4,1709,18])).
% 125.31/125.44 cnf(1712,plain,
% 125.31/125.44 (P3(f7(a4,f6(a4)),a2)),
% 125.31/125.44 inference(scs_inference,[],[4,52,1709,18,20])).
% 125.31/125.44 cnf(2163,plain,
% 125.31/125.44 (P2(f3(a1,f6(a4)),f6(a4))),
% 125.31/125.44 inference(scs_inference,[],[56,2,13,10])).
% 125.31/125.44 cnf(2170,plain,
% 125.31/125.44 (~P3(f3(a1,f6(a4)),x21701)+P3(f6(a4),x21701)),
% 125.31/125.44 inference(scs_inference,[],[2163,20])).
% 125.31/125.44 cnf(2301,plain,
% 125.31/125.44 (P2(f3(a1,a2),f7(a4,a2))),
% 125.31/125.44 inference(scs_inference,[],[3,1241,13,18])).
% 125.31/125.44 cnf(2346,plain,
% 125.31/125.44 (P2(f3(a1,a1),a1)),
% 125.31/125.44 inference(scs_inference,[],[276,1,8,13])).
% 125.31/125.44 cnf(2348,plain,
% 125.31/125.44 (P2(f7(a4,f6(a2)),f6(a2))),
% 125.31/125.44 inference(scs_inference,[],[276,1685,1,8,13,14])).
% 125.31/125.44 cnf(2352,plain,
% 125.31/125.44 (P2(a1,f3(a4,f5(a2)))),
% 125.31/125.44 inference(scs_inference,[],[276,1306,1685,1,8,13,14,17,708])).
% 125.31/125.44 cnf(2354,plain,
% 125.31/125.44 (P2(f7(a4,a2),f3(a1,a2))),
% 125.31/125.44 inference(scs_inference,[],[2301,276,1306,1685,1,8,13,14,17,708,11])).
% 125.31/125.44 cnf(2356,plain,
% 125.31/125.44 (P1(f3(f6(a2),f6(a2)))),
% 125.31/125.44 inference(scs_inference,[],[2301,276,1306,1685,1,8,13,14,17,708,11,15])).
% 125.31/125.44 cnf(2360,plain,
% 125.31/125.44 (P1(f6(a4))),
% 125.31/125.44 inference(scs_inference,[],[2301,276,1306,1685,56,1,2,8,13,14,17,708,11,15,16,10])).
% 125.31/125.44 cnf(2372,plain,
% 125.31/125.44 (P3(a1,f7(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2301,276,36,1306,1685,56,1,2,8,13,14,17,708,11,15,16,10,24,25,26,27,22,23])).
% 125.31/125.44 cnf(2396,plain,
% 125.31/125.44 (P2(f3(a1,a4),a4)),
% 125.31/125.44 inference(scs_inference,[],[2356,2,8,13])).
% 125.31/125.44 cnf(2400,plain,
% 125.31/125.44 (P2(f7(a4,f6(a4)),f6(a4))),
% 125.31/125.44 inference(scs_inference,[],[2360,2356,2,8,13,17,14])).
% 125.31/125.44 cnf(2402,plain,
% 125.31/125.44 (P2(a1,f3(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2360,2346,2356,2,8,13,17,14,11])).
% 125.31/125.44 cnf(2406,plain,
% 125.31/125.44 (P3(a1,f7(f7(a1,a1),f7(a1,a1)))),
% 125.31/125.44 inference(scs_inference,[],[2372,2360,2346,2356,2,8,13,17,14,11,15,23])).
% 125.31/125.44 cnf(2416,plain,
% 125.31/125.44 (P1(f7(f6(a4),f6(a4)))),
% 125.31/125.44 inference(scs_inference,[],[2354,2372,2360,2346,2356,2,8,13,17,14,11,15,23,25,24,26,27,16])).
% 125.31/125.44 cnf(2428,plain,
% 125.31/125.44 (P2(f3(a4,f3(a4,a4)),f3(f3(a4,a4),a4))),
% 125.31/125.44 inference(scs_inference,[],[2354,2372,2360,2346,2356,2352,1311,2,8,13,17,14,11,15,23,25,24,26,27,16,28,21,18,20,30,29])).
% 125.31/125.44 cnf(2432,plain,
% 125.31/125.44 (P3(f6(a4),f3(f7(a1,a1),f6(a4)))),
% 125.31/125.44 inference(scs_inference,[],[2354,2372,2360,2346,2356,2352,1311,2,8,13,17,14,11,15,23,25,24,26,27,16,28,21,18,20,30,29,31,2170])).
% 125.31/125.44 cnf(2441,plain,
% 125.31/125.44 (P2(f3(a1,a2),a2)),
% 125.31/125.44 inference(scs_inference,[],[2416,3,8,13])).
% 125.31/125.44 cnf(2443,plain,
% 125.31/125.44 (P2(f7(a4,a1),a1)),
% 125.31/125.44 inference(scs_inference,[],[2416,1,3,8,13,14])).
% 125.31/125.44 cnf(2449,plain,
% 125.31/125.44 (P1(f3(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2396,2416,1,3,8,13,14,17,11,15])).
% 125.31/125.44 cnf(2459,plain,
% 125.31/125.44 (P1(f7(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2402,2396,2416,2360,1,2,3,8,13,14,17,11,15,25,27,26,24,16])).
% 125.31/125.44 cnf(2489,plain,
% 125.31/125.44 (P2(f7(a4,f3(a1,a1)),f3(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2449,8,13,17,14])).
% 125.31/125.44 cnf(2491,plain,
% 125.31/125.44 (P2(a1,f7(a4,a1))),
% 125.31/125.44 inference(scs_inference,[],[2449,2443,8,13,17,14,11])).
% 125.31/125.44 cnf(2499,plain,
% 125.31/125.44 (P2(f7(f3(a1,a2),f3(a1,a1)),f7(a2,f3(a1,a1)))),
% 125.31/125.44 inference(scs_inference,[],[2441,2449,2443,8,13,17,14,11,15,25,16,27])).
% 125.31/125.44 cnf(2517,plain,
% 125.31/125.44 (P1(f5(f7(a1,a1)))),
% 125.31/125.44 inference(scs_inference,[],[2459,8])).
% 125.31/125.44 cnf(2519,plain,
% 125.31/125.44 (P2(f3(a1,f7(a1,a1)),f7(a1,a1))),
% 125.31/125.44 inference(scs_inference,[],[2459,8,13])).
% 125.31/125.44 cnf(2549,plain,
% 125.31/125.44 (P2(f7(a4,a4),a4)),
% 125.31/125.44 inference(scs_inference,[],[2517,2,8,14])).
% 125.31/125.44 cnf(2555,plain,
% 125.31/125.44 (P2(f7(a4,a4),f7(a4,a4))),
% 125.31/125.44 inference(scs_inference,[],[2489,2517,2,8,14,17,11,25])).
% 125.31/125.44 cnf(2557,plain,
% 125.31/125.44 (P1(f3(a4,a4))),
% 125.31/125.44 inference(scs_inference,[],[2489,2517,2,8,14,17,11,25,15])).
% 125.31/125.44 cnf(2563,plain,
% 125.31/125.44 (P1(f7(a4,a4))),
% 125.31/125.44 inference(scs_inference,[],[2489,2517,2459,2,8,14,17,11,25,15,24,26,16])).
% 125.31/125.44 cnf(2567,plain,
% 125.31/125.44 (~P2(f7(a4,f6(a4)),a1)),
% 125.31/125.44 inference(scs_inference,[],[6,2489,2517,2432,1710,2459,2,8,14,17,11,25,15,24,26,16,28,18])).
% 125.31/125.44 cnf(2575,plain,
% 125.31/125.44 (P1(f5(f3(a4,a4)))),
% 125.31/125.44 inference(scs_inference,[],[2557,8])).
% 125.31/125.44 cnf(2583,plain,
% 125.31/125.44 (P2(a4,f7(a4,a4))),
% 125.31/125.44 inference(scs_inference,[],[2557,2563,2549,8,13,17,14,11])).
% 125.31/125.44 cnf(2595,plain,
% 125.31/125.44 (P1(f7(f3(a4,a4),f3(a4,a4)))),
% 125.31/125.44 inference(scs_inference,[],[2557,2555,2563,2549,8,13,17,14,11,25,15,26,24,27,16])).
% 125.31/125.44 cnf(2605,plain,
% 125.31/125.44 (P1(f6(f6(a4)))),
% 125.31/125.44 inference(scs_inference,[],[2557,2555,2563,2549,2400,2567,2360,8,13,17,14,11,25,15,26,24,27,16,18,9,193,22,10])).
% 125.31/125.44 cnf(2615,plain,
% 125.31/125.44 (P2(f7(a4,f7(a4,a4)),f7(a4,a4))),
% 125.31/125.44 inference(scs_inference,[],[2575,2605,2563,8,9,17,14])).
% 125.31/125.44 cnf(2625,plain,
% 125.31/125.44 (P2(f7(a4,f7(a4,a4)),f7(f7(a4,a4),f7(a4,a4)))),
% 125.31/125.44 inference(scs_inference,[],[2583,2519,2575,2605,2563,8,9,17,14,11,25,15,26,27])).
% 125.31/125.44 cnf(2629,plain,
% 125.31/125.44 (~P2(f7(a2,a2),a1)),
% 125.31/125.44 inference(scs_inference,[],[6,2583,2519,2575,2605,1338,2563,8,9,17,14,11,25,15,26,27,16,18])).
% 125.31/125.44 cnf(2631,plain,
% 125.31/125.44 (P3(f7(a4,a1),f7(f7(a1,a1),f7(a1,a1)))),
% 125.31/125.44 inference(scs_inference,[],[6,2583,2519,2575,2605,1338,2491,2563,2406,8,9,17,14,11,25,15,26,27,16,18,20])).
% 125.31/125.44 cnf(2647,plain,
% 125.31/125.44 (P1(f3(a2,a2))),
% 125.31/125.44 inference(scs_inference,[],[2615,2595,3,8,14,11,15])).
% 125.31/125.44 cnf(2649,plain,
% 125.31/125.44 (P1(f7(a2,a2))),
% 125.31/125.44 inference(scs_inference,[],[2615,2595,3,8,14,11,15,16])).
% 125.31/125.44 cnf(2653,plain,
% 125.31/125.44 (P2(f7(a4,f7(a4,a4)),a4)),
% 125.31/125.44 inference(scs_inference,[],[2615,2595,2631,2549,2557,3,8,14,11,15,16,28,18])).
% 125.31/125.44 cnf(2661,plain,
% 125.31/125.44 (P1(f6(f7(a2,a2)))),
% 125.31/125.44 inference(scs_inference,[],[2629,2615,2595,2631,2549,2557,982,3,8,14,11,15,16,28,18,17,266,22,10])).
% 125.31/125.44 cnf(2677,plain,
% 125.31/125.44 (P2(f7(a4,f3(a2,a2)),f3(a2,a2))),
% 125.31/125.44 inference(scs_inference,[],[2647,2649,2661,8,17,14])).
% 125.31/125.44 cnf(2717,plain,
% 125.31/125.44 (P2(f6(a2),f7(a4,f6(a2)))),
% 125.31/125.44 inference(scs_inference,[],[2348,11])).
% 125.31/125.44 cnf(2727,plain,
% 125.31/125.44 (P2(f3(a2,a2),f7(a4,f3(a2,a2)))),
% 125.31/125.44 inference(scs_inference,[],[2677,11])).
% 125.31/125.44 cnf(2787,plain,
% 125.31/125.44 (P2(a4,f7(a4,f7(a4,a4)))),
% 125.31/125.44 inference(scs_inference,[],[2653,11])).
% 125.31/125.44 cnf(2859,plain,
% 125.31/125.44 (P2(f7(a4,a1),f7(f7(a4,f7(a4,a4)),a1))),
% 125.31/125.44 inference(scs_inference,[],[1,2727,2787,2428,2400,1712,2647,11,8,25,26,20,16,27])).
% 125.31/125.44 cnf(2994,plain,
% 125.31/125.44 (~P2(f7(a4,f6(a2)),f7(a2,f6(a2)))),
% 125.31/125.44 inference(scs_inference,[],[2499,1689,2717,153,11,8,18])).
% 125.31/125.44 cnf(4763,plain,
% 125.31/125.44 ($false),
% 125.31/125.44 inference(scs_inference,[],[4,1685,2787,2631,2625,2859,2994,11,20,18,27]),
% 125.31/125.44 ['proof']).
% 125.31/125.44 % SZS output end Proof
% 125.31/125.44 % Total time :124.720000s
%------------------------------------------------------------------------------