%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD025-5 : 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 : n010.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:17 EDT 2024
% Result : Unsatisfiable 2.54s 2.64s
% Output : CNFRefutation 2.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : FLD025-5 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n010.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 10:06:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.48/0.57 start to proof:theBenchmark
% 2.54/2.63 %-------------------------------------------
% 2.54/2.63 % File :CSE---1.7
% 2.54/2.63 % Problem :theBenchmark
% 2.54/2.63 % Transform :cnf
% 2.54/2.63 % Format :tptp:raw
% 2.54/2.63 % Command :java -jar mcs_scs.jar %d %s
% 2.54/2.63
% 2.54/2.63 % Result :Theorem 2.010000s
% 2.54/2.63 % Output :CNFRefutation 2.010000s
% 2.54/2.63 %-------------------------------------------
% 2.54/2.63 %--------------------------------------------------------------------------
% 2.54/2.63 % File : FLD025-5 : TPTP v8.2.0. Bugfixed v2.1.0.
% 2.54/2.63 % Domain : Field Theory (Ordered fields)
% 2.54/2.63 % Problem : The resulting equation of a multiplication of two equations
% 2.54/2.63 % Version : [Dra93] axioms : Especial.
% 2.54/2.63 % Theorem formulation : Relational variant with re axiom set.
% 2.54/2.63 % English :
% 2.54/2.63
% 2.54/2.63 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 2.54/2.63 % Source : [Dra93]
% 2.54/2.63 % Names :
% 2.54/2.63
% 2.54/2.63 % Status : Unsatisfiable
% 2.54/2.63 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 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.00 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.00 v2.2.1, 0.33 v2.1.0
% 2.54/2.63 % Syntax : Number of clauses : 37 ( 14 unt; 3 nHn; 37 RR)
% 2.54/2.63 % Number of literals : 88 ( 0 equ; 50 neg)
% 2.54/2.63 % Maximal clause size : 5 ( 2 avg)
% 2.54/2.63 % Maximal term depth : 2 ( 1 avg)
% 2.54/2.63 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 2.54/2.63 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% 2.54/2.63 % Number of variables : 73 ( 0 sgn)
% 2.54/2.63 % SPC : CNF_UNS_RFO_NEQ_NHN
% 2.54/2.63
% 2.54/2.63 % Comments :
% 2.54/2.63 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 2.54/2.63 %--------------------------------------------------------------------------
% 2.54/2.63 include('Axioms/FLD002-0.ax').
% 2.54/2.63 %--------------------------------------------------------------------------
% 2.54/2.63 cnf(a_is_defined,hypothesis,
% 2.54/2.63 defined(a) ).
% 2.54/2.63
% 2.54/2.63 cnf(b_is_defined,hypothesis,
% 2.54/2.63 defined(b) ).
% 2.54/2.63
% 2.54/2.63 cnf(c_is_defined,hypothesis,
% 2.54/2.63 defined(c) ).
% 2.54/2.63
% 2.54/2.63 cnf(d_is_defined,hypothesis,
% 2.54/2.63 defined(d) ).
% 2.54/2.63
% 2.54/2.63 cnf(u_is_defined,hypothesis,
% 2.54/2.63 defined(u) ).
% 2.54/2.63
% 2.54/2.63 cnf(v_is_defined,hypothesis,
% 2.54/2.63 defined(v) ).
% 2.54/2.63
% 2.54/2.63 cnf(product_7,negated_conjecture,
% 2.54/2.63 product(multiplicative_identity,a,b) ).
% 2.54/2.63
% 2.54/2.63 cnf(product_8,negated_conjecture,
% 2.54/2.64 product(multiplicative_identity,c,d) ).
% 2.54/2.64
% 2.54/2.64 cnf(product_9,negated_conjecture,
% 2.54/2.64 product(a,c,u) ).
% 2.54/2.64
% 2.54/2.64 cnf(product_10,negated_conjecture,
% 2.54/2.64 product(d,b,v) ).
% 2.54/2.64
% 2.54/2.64 cnf(not_product_11,negated_conjecture,
% 2.54/2.64 ~ product(multiplicative_identity,u,v) ).
% 2.54/2.64
% 2.54/2.64 %--------------------------------------------------------------------------
% 2.54/2.64 %-------------------------------------------
% 2.54/2.64 % Proof found
% 2.54/2.64 % SZS status Theorem for theBenchmark
% 2.54/2.64 % SZS output start Proof
% 2.54/2.64 %ClaNum:37(EqnAxiom:0)
% 2.54/2.64 %VarNum:162(SingletonVarNum:73)
% 2.54/2.64 %MaxLitNum:5
% 2.54/2.64 %MaxfuncDepth:1
% 2.54/2.64 %SharedTerms:22
% 2.54/2.64 %goalClause: 9 10 11 12 14
% 2.54/2.64 %singleGoalClaCount:5
% 2.54/2.64 [1]P1(a1)
% 2.54/2.64 [2]P1(a4)
% 2.54/2.64 [3]P1(a2)
% 2.54/2.64 [4]P1(a5)
% 2.54/2.64 [5]P1(a7)
% 2.54/2.64 [6]P1(a8)
% 2.54/2.64 [7]P1(a9)
% 2.54/2.64 [8]P1(a12)
% 2.54/2.64 [9]P2(a4,a2,a5)
% 2.54/2.64 [10]P2(a4,a7,a8)
% 2.54/2.64 [11]P2(a2,a7,a9)
% 2.54/2.64 [12]P2(a8,a5,a12)
% 2.54/2.64 [13]~P4(a1,a1,a4)
% 2.54/2.64 [14]~P2(a4,a9,a12)
% 2.54/2.64 [20]~P1(x201)+P4(a1,x201,x201)
% 2.54/2.64 [21]~P1(x211)+P2(a4,x211,x211)
% 2.54/2.64 [15]~P1(x151)+P1(f6(x151))
% 2.54/2.64 [22]~P1(x221)+P4(f6(x221),x221,a1)
% 2.54/2.64 [29]~P4(x292,x291,x293)+P4(x291,x292,x293)
% 2.54/2.64 [30]~P2(x302,x301,x303)+P2(x301,x302,x303)
% 2.54/2.64 [23]~P1(x231)+P4(a1,x231,a1)+P1(f11(x231))
% 2.54/2.64 [27]~P1(x271)+P2(f11(x271),x271,a4)+P4(a1,x271,a1)
% 2.54/2.64 [26]~P3(x262,x261)+~P3(x261,x262)+P4(a1,x261,x262)
% 2.54/2.64 [17]~P1(x172)+~P1(x171)+P1(f3(x171,x172))
% 2.54/2.64 [18]~P1(x182)+~P1(x181)+P1(f10(x181,x182))
% 2.54/2.64 [24]~P1(x242)+~P1(x241)+P4(x241,x242,f3(x241,x242))
% 2.54/2.64 [25]~P1(x252)+~P1(x251)+P2(x251,x252,f10(x251,x252))
% 2.54/2.64 [19]~P3(x191,x193)+P3(x191,x192)+~P3(x193,x192)
% 2.54/2.64 [16]P3(x162,x161)+~P1(x161)+~P1(x162)+P3(x161,x162)
% 2.54/2.64 [28]~P2(x283,x282,x281)+P3(a1,x281)+~P3(a1,x282)+~P3(a1,x283)
% 2.54/2.64 [31]~P4(x313,x315,x311)+P3(x311,x312)+~P4(x314,x315,x312)+~P3(x313,x314)
% 2.54/2.64 [32]~P4(x321,x326,x324)+P4(x321,x322,x323)+~P4(x324,x325,x323)+~P4(x326,x325,x322)
% 2.54/2.64 [33]~P4(x336,x334,x331)+P4(x331,x332,x333)+~P4(x334,x332,x335)+~P4(x336,x335,x333)
% 2.54/2.64 [34]~P2(x341,x346,x344)+P2(x341,x342,x343)+~P2(x344,x345,x343)+~P2(x346,x345,x342)
% 2.54/2.64 [35]~P2(x356,x354,x351)+P2(x351,x352,x353)+~P2(x354,x352,x355)+~P2(x356,x355,x353)
% 2.54/2.64 [36]~P2(x365,x367,x362)+~P2(x364,x367,x361)+P4(x361,x362,x363)+~P4(x364,x365,x366)+~P2(x366,x367,x363)
% 2.54/2.64 [37]~P2(x377,x372,x375)+~P2(x376,x372,x374)+P2(x371,x372,x373)+~P4(x374,x375,x373)+~P4(x376,x377,x371)
% 2.54/2.64 %EqnAxiom
% 2.54/2.64
% 2.54/2.64 %-------------------------------------------
% 2.54/2.64 cnf(38,plain,
% 2.54/2.64 (~P2(a9,a4,a12)),
% 2.54/2.64 inference(scs_inference,[],[14,30])).
% 2.54/2.64 cnf(93,plain,
% 2.54/2.64 (P2(a9,x931,a9)+~P2(a7,x931,a7)),
% 2.54/2.64 inference(scs_inference,[],[11,5,16,35])).
% 2.54/2.64 cnf(350,plain,
% 2.54/2.64 (~P2(x3501,a7,a7)+P2(a9,x3501,a9)),
% 2.54/2.64 inference(scs_inference,[],[93,30])).
% 2.54/2.64 cnf(576,plain,
% 2.54/2.64 (P2(x5761,a9,a9)+~P2(x5761,a7,a7)),
% 2.54/2.64 inference(scs_inference,[],[350,30])).
% 2.54/2.64 cnf(788,plain,
% 2.54/2.64 (P2(a4,a9,a9)),
% 2.54/2.64 inference(scs_inference,[],[5,576,21])).
% 2.54/2.64 cnf(857,plain,
% 2.54/2.64 (~P2(a8,x8571,a9)+~P2(x8571,a4,a5)),
% 2.54/2.64 inference(scs_inference,[],[12,38,35])).
% 2.54/2.64 cnf(1113,plain,
% 2.54/2.64 (~P2(a8,a2,a9)),
% 2.54/2.64 inference(scs_inference,[],[9,857,30])).
% 2.54/2.64 cnf(1118,plain,
% 2.54/2.64 (~P2(a2,a4,a2)),
% 2.54/2.64 inference(scs_inference,[],[10,11,788,1113,30,35,34])).
% 2.54/2.64 cnf(1123,plain,
% 2.54/2.64 ($false),
% 2.54/2.64 inference(scs_inference,[],[3,1118,30,21]),
% 2.54/2.64 ['proof']).
% 2.54/2.64 % SZS output end Proof
% 2.54/2.64 % Total time :2.010000s
%------------------------------------------------------------------------------