%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD050-4 : 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 : n019.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:27 EDT 2024
% Result : Unsatisfiable 16.00s 16.14s
% Output : CNFRefutation 16.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : FLD050-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 11:54:38 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.57/0.61 start to proof:theBenchmark
% 16.00/16.13 %-------------------------------------------
% 16.00/16.13 % File :CSE---1.7
% 16.00/16.13 % Problem :theBenchmark
% 16.00/16.13 % Transform :cnf
% 16.00/16.13 % Format :tptp:raw
% 16.00/16.13 % Command :java -jar mcs_scs.jar %d %s
% 16.00/16.13
% 16.00/16.13 % Result :Theorem 15.460000s
% 16.00/16.13 % Output :CNFRefutation 15.460000s
% 16.00/16.13 %-------------------------------------------
% 16.00/16.14 %--------------------------------------------------------------------------
% 16.00/16.14 % File : FLD050-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 16.00/16.14 % Domain : Field Theory (Ordered fields)
% 16.00/16.14 % Problem : Fraction calculation, part 4
% 16.00/16.14 % Version : [Dra93] axioms : Especial.
% 16.00/16.14 % Theorem formulation : Relational with re axiom set.
% 16.00/16.14 % English :
% 16.00/16.14
% 16.00/16.14 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 16.00/16.14 % Source : [Dra93]
% 16.00/16.14 % Names :
% 16.00/16.14
% 16.00/16.14 % Status : Unsatisfiable
% 16.00/16.14 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.17 v7.4.0, 0.00 v7.0.0, 0.25 v6.3.0, 0.00 v6.2.0, 0.11 v6.1.0, 0.00 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 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 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.67 v2.5.0, 0.20 v2.4.0, 0.60 v2.3.0, 0.67 v2.2.1, 1.00 v2.1.0
% 16.00/16.14 % Syntax : Number of clauses : 38 ( 15 unt; 3 nHn; 38 RR)
% 16.00/16.14 % Number of literals : 89 ( 0 equ; 52 neg)
% 16.00/16.14 % Maximal clause size : 5 ( 2 avg)
% 16.00/16.14 % Maximal term depth : 2 ( 1 avg)
% 16.00/16.14 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 16.00/16.14 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% 16.00/16.14 % Number of variables : 73 ( 0 sgn)
% 16.00/16.14 % SPC : CNF_UNS_RFO_NEQ_NHN
% 16.00/16.14
% 16.00/16.14 % Comments :
% 16.00/16.14 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 16.00/16.14 %--------------------------------------------------------------------------
% 16.00/16.14 include('Axioms/FLD002-0.ax').
% 16.00/16.14 %--------------------------------------------------------------------------
% 16.00/16.14 cnf(a_is_defined,hypothesis,
% 16.00/16.14 defined(a) ).
% 16.00/16.14
% 16.00/16.14 cnf(b_is_defined,hypothesis,
% 16.00/16.14 defined(b) ).
% 16.00/16.14
% 16.00/16.14 cnf(c_is_defined,hypothesis,
% 16.00/16.14 defined(c) ).
% 16.00/16.14
% 16.00/16.14 cnf(d_is_defined,hypothesis,
% 16.00/16.14 defined(d) ).
% 16.00/16.14
% 16.00/16.14 cnf(k_is_defined,hypothesis,
% 16.00/16.14 defined(k) ).
% 16.00/16.14
% 16.00/16.14 cnf(s_is_defined,hypothesis,
% 16.00/16.14 defined(s) ).
% 16.00/16.14
% 16.00/16.14 cnf(not_sum_7,negated_conjecture,
% 16.00/16.14 ~ sum(additive_identity,b,additive_identity) ).
% 16.00/16.14
% 16.00/16.14 cnf(not_sum_8,negated_conjecture,
% 16.00/16.14 ~ sum(additive_identity,d,additive_identity) ).
% 16.00/16.14
% 16.00/16.14 cnf(product_9,negated_conjecture,
% 16.00/16.14 product(a,multiplicative_inverse(b),s) ).
% 16.00/16.14
% 16.00/16.14 cnf(product_10,negated_conjecture,
% 16.00/16.14 product(a,d,k) ).
% 16.00/16.14
% 16.00/16.14 cnf(product_11,negated_conjecture,
% 16.00/16.14 product(b,c,k) ).
% 16.00/16.14
% 16.00/16.14 cnf(not_product_12,negated_conjecture,
% 16.00/16.14 ~ product(c,multiplicative_inverse(d),s) ).
% 16.00/16.14
% 16.00/16.14 %--------------------------------------------------------------------------
% 16.00/16.14 %-------------------------------------------
% 16.00/16.14 % Proof found
% 16.00/16.14 % SZS status Theorem for theBenchmark
% 16.00/16.14 % SZS output start Proof
% 16.00/16.14 %ClaNum:38(EqnAxiom:0)
% 16.00/16.14 %VarNum:162(SingletonVarNum:73)
% 16.00/16.14 %MaxLitNum:5
% 16.00/16.14 %MaxfuncDepth:1
% 16.00/16.14 %SharedTerms:25
% 16.00/16.14 %goalClause: 9 10 11 13 14 15
% 16.00/16.14 %singleGoalClaCount:6
% 16.00/16.14 [1]P1(a1)
% 16.00/16.14 [2]P1(a4)
% 16.00/16.14 [3]P1(a2)
% 16.00/16.14 [4]P1(a5)
% 16.00/16.14 [5]P1(a7)
% 16.00/16.14 [6]P1(a8)
% 16.00/16.14 [7]P1(a9)
% 16.00/16.14 [8]P1(a10)
% 16.00/16.14 [9]P2(a2,a8,a9)
% 16.00/16.14 [10]P2(a5,a7,a9)
% 16.00/16.14 [12]~P4(a1,a1,a4)
% 16.00/16.14 [13]~P4(a1,a5,a1)
% 16.00/16.14 [14]~P4(a1,a8,a1)
% 16.00/16.14 [11]P2(a2,f11(a5),a10)
% 16.00/16.14 [15]~P2(a7,f11(a8),a10)
% 16.00/16.14 [21]~P1(x211)+P4(a1,x211,x211)
% 16.00/16.14 [22]~P1(x221)+P2(a4,x221,x221)
% 16.00/16.14 [16]~P1(x161)+P1(f6(x161))
% 16.00/16.14 [23]~P1(x231)+P4(f6(x231),x231,a1)
% 16.00/16.14 [30]~P4(x302,x301,x303)+P4(x301,x302,x303)
% 16.00/16.14 [31]~P2(x312,x311,x313)+P2(x311,x312,x313)
% 16.00/16.14 [24]~P1(x241)+P4(a1,x241,a1)+P1(f11(x241))
% 16.00/16.14 [28]~P1(x281)+P2(f11(x281),x281,a4)+P4(a1,x281,a1)
% 16.00/16.14 [27]~P3(x272,x271)+~P3(x271,x272)+P4(a1,x271,x272)
% 16.00/16.14 [18]~P1(x182)+~P1(x181)+P1(f3(x181,x182))
% 16.00/16.14 [19]~P1(x192)+~P1(x191)+P1(f12(x191,x192))
% 16.00/16.14 [25]~P1(x252)+~P1(x251)+P4(x251,x252,f3(x251,x252))
% 16.00/16.14 [26]~P1(x262)+~P1(x261)+P2(x261,x262,f12(x261,x262))
% 16.00/16.14 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 16.00/16.14 [17]P3(x172,x171)+~P1(x171)+~P1(x172)+P3(x171,x172)
% 16.00/16.14 [29]~P2(x293,x292,x291)+P3(a1,x291)+~P3(a1,x292)+~P3(a1,x293)
% 16.00/16.14 [32]~P4(x323,x325,x321)+P3(x321,x322)+~P4(x324,x325,x322)+~P3(x323,x324)
% 16.00/16.14 [33]~P4(x331,x336,x334)+P4(x331,x332,x333)+~P4(x334,x335,x333)+~P4(x336,x335,x332)
% 16.00/16.14 [34]~P4(x346,x344,x341)+P4(x341,x342,x343)+~P4(x344,x342,x345)+~P4(x346,x345,x343)
% 16.00/16.14 [35]~P2(x351,x356,x354)+P2(x351,x352,x353)+~P2(x354,x355,x353)+~P2(x356,x355,x352)
% 16.00/16.14 [36]~P2(x366,x364,x361)+P2(x361,x362,x363)+~P2(x364,x362,x365)+~P2(x366,x365,x363)
% 16.00/16.14 [37]~P2(x375,x377,x372)+~P2(x374,x377,x371)+P4(x371,x372,x373)+~P4(x374,x375,x376)+~P2(x376,x377,x373)
% 16.00/16.14 [38]~P2(x387,x382,x385)+~P2(x386,x382,x384)+P2(x381,x382,x383)+~P4(x384,x385,x383)+~P4(x386,x387,x381)
% 16.00/16.14 %EqnAxiom
% 16.00/16.14
% 16.00/16.14 %-------------------------------------------
% 16.00/16.15 cnf(82,plain,
% 16.00/16.15 (~P2(x821,a2,a2)+P2(x821,a10,a10)),
% 16.00/16.15 inference(scs_inference,[],[11,6,17,35])).
% 16.00/16.15 cnf(313,plain,
% 16.00/16.15 (P2(a10,x3131,a10)+~P2(x3131,a2,a2)),
% 16.00/16.15 inference(scs_inference,[],[82,31])).
% 16.00/16.15 cnf(465,plain,
% 16.00/16.15 (P2(a10,a4,a10)),
% 16.00/16.15 inference(scs_inference,[],[3,313,22])).
% 16.00/16.15 cnf(782,plain,
% 16.00/16.15 (~P2(a10,x7821,a7)+~P2(x7821,f11(a8),a4)),
% 16.00/16.15 inference(scs_inference,[],[15,465,36])).
% 16.00/16.15 cnf(810,plain,
% 16.00/16.15 (~P2(f11(a8),x8101,a4)+~P2(a10,x8101,a7)),
% 16.00/16.15 inference(scs_inference,[],[782,31])).
% 16.00/16.15 cnf(874,plain,
% 16.00/16.15 (~P2(a10,a8,a7)),
% 16.00/16.15 inference(scs_inference,[],[14,6,810,28])).
% 16.00/16.15 cnf(875,plain,
% 16.00/16.15 (~P2(a8,a10,a7)),
% 16.00/16.15 inference(scs_inference,[],[874,31])).
% 16.00/16.15 cnf(877,plain,
% 16.00/16.15 (~P2(a8,a2,x8771)+~P2(x8771,f11(a5),a7)),
% 16.00/16.15 inference(scs_inference,[],[11,874,31,35])).
% 16.00/16.15 cnf(1101,plain,
% 16.00/16.15 (~P2(f11(a5),x11011,a7)+~P2(a8,a2,x11011)),
% 16.00/16.15 inference(scs_inference,[],[877,31])).
% 16.00/16.15 cnf(1133,plain,
% 16.00/16.15 (~P2(f11(a5),a2,x11331)+~P2(x11331,a8,a7)+~P2(a8,a2,a9)),
% 16.00/16.15 inference(scs_inference,[],[9,1101,35])).
% 16.00/16.15 cnf(3674,plain,
% 16.00/16.15 (~P2(f11(a5),a9,a7)),
% 16.00/16.15 inference(scs_inference,[],[9,11,875,31,1133,35,1101])).
% 16.00/16.15 cnf(3680,plain,
% 16.00/16.15 (~P2(f11(a5),a5,x36801)+~P2(x36801,a7,a7)),
% 16.00/16.15 inference(scs_inference,[],[11,10,3674,31,35])).
% 16.00/16.15 cnf(3936,plain,
% 16.00/16.15 (~P2(a4,a7,a7)),
% 16.00/16.15 inference(scs_inference,[],[13,4,3680,28])).
% 16.00/16.15 cnf(3937,plain,
% 16.00/16.15 ($false),
% 16.00/16.15 inference(scs_inference,[],[3936,5,22]),
% 16.00/16.15 ['proof']).
% 16.00/16.15 % SZS output end Proof
% 16.00/16.15 % Total time :15.460000s
%------------------------------------------------------------------------------