%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD049-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 : n024.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 28.95s 29.05s
% Output : CNFRefutation 28.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : FLD049-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n024.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:02:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 28.95/29.04 %-------------------------------------------
% 28.95/29.04 % File :CSE---1.7
% 28.95/29.04 % Problem :theBenchmark
% 28.95/29.04 % Transform :cnf
% 28.95/29.04 % Format :tptp:raw
% 28.95/29.04 % Command :java -jar mcs_scs.jar %d %s
% 28.95/29.04
% 28.95/29.04 % Result :Theorem 28.420000s
% 28.95/29.04 % Output :CNFRefutation 28.420000s
% 28.95/29.04 %-------------------------------------------
% 28.95/29.05 %--------------------------------------------------------------------------
% 28.95/29.05 % File : FLD049-4 : TPTP v8.2.0. Bugfixed v2.1.0.
% 28.95/29.05 % Domain : Field Theory (Ordered fields)
% 28.95/29.05 % Problem : Fraction calculation, part 3
% 28.95/29.05 % Version : [Dra93] axioms : Especial.
% 28.95/29.05 % Theorem formulation : Relational with re axiom set.
% 28.95/29.05 % English :
% 28.95/29.05
% 28.95/29.05 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 28.95/29.05 % Source : [Dra93]
% 28.95/29.05 % Names :
% 28.95/29.05
% 28.95/29.05 % Status : Unsatisfiable
% 28.95/29.05 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.0.0, 0.38 v6.4.0, 0.25 v6.3.0, 0.29 v6.2.0, 0.22 v6.1.0, 0.00 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 v5.1.0, 0.27 v5.0.0, 0.36 v4.1.0, 0.25 v4.0.1, 0.40 v4.0.0, 0.29 v3.4.0, 0.50 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.67 v2.5.0, 0.60 v2.3.0, 0.67 v2.2.1, 1.00 v2.1.0
% 28.95/29.05 % Syntax : Number of clauses : 38 ( 15 unt; 3 nHn; 38 RR)
% 28.95/29.05 % Number of literals : 89 ( 0 equ; 52 neg)
% 28.95/29.05 % Maximal clause size : 5 ( 2 avg)
% 28.95/29.05 % Maximal term depth : 2 ( 1 avg)
% 28.95/29.05 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 28.95/29.05 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% 28.95/29.05 % Number of variables : 73 ( 0 sgn)
% 28.95/29.05 % SPC : CNF_UNS_RFO_NEQ_NHN
% 28.95/29.05
% 28.95/29.05 % Comments :
% 28.95/29.05 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 28.95/29.05 %--------------------------------------------------------------------------
% 28.95/29.05 include('Axioms/FLD002-0.ax').
% 28.95/29.05 %--------------------------------------------------------------------------
% 28.95/29.05 cnf(a_is_defined,hypothesis,
% 28.95/29.05 defined(a) ).
% 28.95/29.05
% 28.95/29.05 cnf(b_is_defined,hypothesis,
% 28.95/29.05 defined(b) ).
% 28.95/29.05
% 28.95/29.05 cnf(c_is_defined,hypothesis,
% 28.95/29.05 defined(c) ).
% 28.95/29.05
% 28.95/29.05 cnf(d_is_defined,hypothesis,
% 28.95/29.05 defined(d) ).
% 28.95/29.05
% 28.95/29.05 cnf(k_is_defined,hypothesis,
% 28.95/29.05 defined(k) ).
% 28.95/29.05
% 28.95/29.05 cnf(s_is_defined,hypothesis,
% 28.95/29.05 defined(s) ).
% 28.95/29.05
% 28.95/29.05 cnf(not_sum_7,negated_conjecture,
% 28.95/29.05 ~ sum(additive_identity,b,additive_identity) ).
% 28.95/29.05
% 28.95/29.05 cnf(not_sum_8,negated_conjecture,
% 28.95/29.05 ~ sum(additive_identity,d,additive_identity) ).
% 28.95/29.05
% 28.95/29.05 cnf(product_9,negated_conjecture,
% 28.95/29.05 product(a,multiplicative_inverse(b),s) ).
% 28.95/29.05
% 28.95/29.05 cnf(product_10,negated_conjecture,
% 28.95/29.05 product(c,multiplicative_inverse(d),s) ).
% 28.95/29.05
% 28.95/29.05 cnf(product_11,negated_conjecture,
% 28.95/29.05 product(a,d,k) ).
% 28.95/29.05
% 28.95/29.05 cnf(not_product_12,negated_conjecture,
% 28.95/29.05 ~ product(b,c,k) ).
% 28.95/29.05
% 28.95/29.05 %--------------------------------------------------------------------------
% 28.95/29.05 %-------------------------------------------
% 28.95/29.05 % Proof found
% 28.95/29.05 % SZS status Theorem for theBenchmark
% 28.95/29.05 % SZS output start Proof
% 28.95/29.05 %ClaNum:38(EqnAxiom:0)
% 28.95/29.05 %VarNum:162(SingletonVarNum:73)
% 28.95/29.05 %MaxLitNum:5
% 28.95/29.05 %MaxfuncDepth:1
% 28.95/29.05 %SharedTerms:25
% 28.95/29.05 %goalClause: 9 10 11 13 14 15
% 28.95/29.05 %singleGoalClaCount:6
% 28.95/29.05 [1]P1(a1)
% 28.95/29.05 [2]P1(a4)
% 28.95/29.05 [3]P1(a2)
% 28.95/29.05 [4]P1(a5)
% 28.95/29.05 [5]P1(a7)
% 28.95/29.05 [6]P1(a8)
% 28.95/29.05 [7]P1(a9)
% 28.95/29.05 [8]P1(a10)
% 28.95/29.05 [9]P2(a2,a8,a9)
% 28.95/29.05 [12]~P4(a1,a1,a4)
% 28.95/29.05 [13]~P4(a1,a5,a1)
% 28.95/29.05 [14]~P4(a1,a8,a1)
% 28.95/29.05 [15]~P2(a5,a7,a9)
% 28.95/29.05 [10]P2(a2,f11(a5),a10)
% 28.95/29.05 [11]P2(a7,f11(a8),a10)
% 28.95/29.05 [21]~P1(x211)+P4(a1,x211,x211)
% 28.95/29.05 [22]~P1(x221)+P2(a4,x221,x221)
% 28.95/29.05 [16]~P1(x161)+P1(f6(x161))
% 28.95/29.05 [23]~P1(x231)+P4(f6(x231),x231,a1)
% 28.95/29.05 [30]~P4(x302,x301,x303)+P4(x301,x302,x303)
% 28.95/29.05 [31]~P2(x312,x311,x313)+P2(x311,x312,x313)
% 28.95/29.05 [24]~P1(x241)+P4(a1,x241,a1)+P1(f11(x241))
% 28.95/29.05 [28]~P1(x281)+P2(f11(x281),x281,a4)+P4(a1,x281,a1)
% 28.95/29.05 [27]~P3(x272,x271)+~P3(x271,x272)+P4(a1,x271,x272)
% 28.95/29.05 [18]~P1(x182)+~P1(x181)+P1(f3(x181,x182))
% 28.95/29.05 [19]~P1(x192)+~P1(x191)+P1(f12(x191,x192))
% 28.95/29.05 [25]~P1(x252)+~P1(x251)+P4(x251,x252,f3(x251,x252))
% 28.95/29.05 [26]~P1(x262)+~P1(x261)+P2(x261,x262,f12(x261,x262))
% 28.95/29.05 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 28.95/29.05 [17]P3(x172,x171)+~P1(x171)+~P1(x172)+P3(x171,x172)
% 28.95/29.05 [29]~P2(x293,x292,x291)+P3(a1,x291)+~P3(a1,x292)+~P3(a1,x293)
% 28.95/29.05 [32]~P4(x323,x325,x321)+P3(x321,x322)+~P4(x324,x325,x322)+~P3(x323,x324)
% 28.95/29.05 [33]~P4(x331,x336,x334)+P4(x331,x332,x333)+~P4(x334,x335,x333)+~P4(x336,x335,x332)
% 28.95/29.05 [34]~P4(x346,x344,x341)+P4(x341,x342,x343)+~P4(x344,x342,x345)+~P4(x346,x345,x343)
% 28.95/29.05 [35]~P2(x351,x356,x354)+P2(x351,x352,x353)+~P2(x354,x355,x353)+~P2(x356,x355,x352)
% 28.95/29.05 [36]~P2(x366,x364,x361)+P2(x361,x362,x363)+~P2(x364,x362,x365)+~P2(x366,x365,x363)
% 28.95/29.05 [37]~P2(x375,x377,x372)+~P2(x374,x377,x371)+P4(x371,x372,x373)+~P4(x374,x375,x376)+~P2(x376,x377,x373)
% 28.95/29.05 [38]~P2(x387,x382,x385)+~P2(x386,x382,x384)+P2(x381,x382,x383)+~P4(x384,x385,x383)+~P4(x386,x387,x381)
% 28.95/29.05 %EqnAxiom
% 28.95/29.05
% 28.95/29.05 %-------------------------------------------
% 28.95/29.06 cnf(39,plain,
% 28.95/29.06 (~P2(a7,a5,a9)),
% 28.95/29.06 inference(scs_inference,[],[15,31])).
% 28.95/29.06 cnf(47,plain,
% 28.95/29.06 (~P2(x471,a2,a2)+P2(x471,a9,a9)),
% 28.95/29.06 inference(scs_inference,[],[9,13,15,1,31,30,17,27,35])).
% 28.95/29.06 cnf(70,plain,
% 28.95/29.06 (~P2(x701,a7,a7)+P2(x701,a10,a10)),
% 28.95/29.06 inference(scs_inference,[],[11,4,17,35])).
% 28.95/29.06 cnf(233,plain,
% 28.95/29.06 (P2(a9,x2331,a9)+~P2(x2331,a2,a2)),
% 28.95/29.06 inference(scs_inference,[],[47,31])).
% 28.95/29.06 cnf(265,plain,
% 28.95/29.06 (P2(a10,x2651,a10)+~P2(x2651,a7,a7)),
% 28.95/29.06 inference(scs_inference,[],[70,31])).
% 28.95/29.06 cnf(377,plain,
% 28.95/29.06 (P2(a9,a4,a9)),
% 28.95/29.06 inference(scs_inference,[],[3,233,22])).
% 28.95/29.06 cnf(417,plain,
% 28.95/29.06 (P2(a10,a4,a10)),
% 28.95/29.06 inference(scs_inference,[],[5,265,22])).
% 28.95/29.06 cnf(1934,plain,
% 28.95/29.06 (~P2(a9,x19341,a7)+~P2(x19341,a5,a4)),
% 28.95/29.06 inference(scs_inference,[],[39,377,36])).
% 28.95/29.06 cnf(2048,plain,
% 28.95/29.06 (~P2(a9,f11(a5),a7)),
% 28.95/29.06 inference(scs_inference,[],[13,4,1934,28])).
% 28.95/29.06 cnf(2051,plain,
% 28.95/29.06 (~P2(f11(a5),a2,x20511)+~P2(x20511,a8,a7)),
% 28.95/29.06 inference(scs_inference,[],[9,2048,31,35])).
% 28.95/29.06 cnf(2192,plain,
% 28.95/29.06 (~P2(a10,a8,a7)),
% 28.95/29.06 inference(scs_inference,[],[10,2051,31])).
% 28.95/29.06 cnf(3690,plain,
% 28.95/29.06 (~P2(a4,x36901,a8)+~P2(a10,x36901,a7)),
% 28.95/29.06 inference(scs_inference,[],[417,2192,35])).
% 28.95/29.06 cnf(3737,plain,
% 28.95/29.06 (~P2(a7,x37371,a7)+~P2(f11(a8),x37372,x37371)+~P2(a4,x37372,a8)),
% 28.95/29.06 inference(scs_inference,[],[11,3690,36])).
% 28.95/29.06 cnf(6456,plain,
% 28.95/29.06 (~P2(a4,a8,a8)+~P2(a7,a4,a7)),
% 28.95/29.06 inference(scs_inference,[],[14,6,3737,28])).
% 28.95/29.06 cnf(6472,plain,
% 28.95/29.06 (~P2(a4,a7,a7)+~P2(a4,a8,a8)),
% 28.95/29.06 inference(scs_inference,[],[6456,31])).
% 28.95/29.06 cnf(6488,plain,
% 28.95/29.06 (~P2(a4,a8,a8)),
% 28.95/29.06 inference(scs_inference,[],[5,6472,22])).
% 28.95/29.06 cnf(6489,plain,
% 28.95/29.06 ($false),
% 28.95/29.06 inference(scs_inference,[],[6488,6,22]),
% 28.95/29.06 ['proof']).
% 28.95/29.06 % SZS output end Proof
% 28.95/29.06 % Total time :28.420000s
%------------------------------------------------------------------------------