%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD056-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 : n032.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:30 EDT 2024
% Result : Unsatisfiable 0.13s 0.51s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.08 % Problem : FLD056-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.05/0.08 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.28 % Computer : n032.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Wed Jun 19 10:26:53 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.13/0.47 start to proof:theBenchmark
% 0.13/0.50 %-------------------------------------------
% 0.13/0.50 % File :CSE---1.7
% 0.13/0.50 % Problem :theBenchmark
% 0.13/0.50 % Transform :cnf
% 0.13/0.50 % Format :tptp:raw
% 0.13/0.50 % Command :java -jar mcs_scs.jar %d %s
% 0.13/0.50
% 0.13/0.50 % Result :Theorem 0.000000s
% 0.13/0.50 % Output :CNFRefutation 0.000000s
% 0.13/0.50 %-------------------------------------------
% 0.13/0.51 %--------------------------------------------------------------------------
% 0.13/0.51 % File : FLD056-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.13/0.51 % Domain : Field Theory (Ordered fields)
% 0.13/0.51 % Problem : Reflexivity of the order relation
% 0.13/0.51 % Version : [Dra93] axioms : Especial.
% 0.13/0.51 % Theorem formulation : Functional with glxx axiom set.
% 0.13/0.51 % English :
% 0.13/0.51
% 0.13/0.51 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 0.13/0.51 % Source : [Dra93]
% 0.13/0.51 % Names :
% 0.13/0.51
% 0.13/0.51 % Status : Unsatisfiable
% 0.13/0.51 % Rating : 0.00 v3.3.0, 0.33 v3.2.0, 0.00 v2.1.0
% 0.13/0.51 % Syntax : Number of clauses : 29 ( 5 unt; 3 nHn; 29 RR)
% 0.13/0.51 % Number of literals : 75 ( 0 equ; 45 neg)
% 0.13/0.51 % Maximal clause size : 4 ( 2 avg)
% 0.13/0.51 % Maximal term depth : 3 ( 1 avg)
% 0.13/0.51 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 0.13/0.51 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 0.13/0.51 % Number of variables : 50 ( 0 sgn)
% 0.13/0.51 % SPC : CNF_UNS_RFO_NEQ_NHN
% 0.13/0.51
% 0.13/0.51 % Comments :
% 0.13/0.51 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 0.13/0.51 %--------------------------------------------------------------------------
% 0.13/0.51 include('Axioms/FLD001-0.ax').
% 0.13/0.51 %--------------------------------------------------------------------------
% 0.13/0.51 cnf(a_is_defined,hypothesis,
% 0.13/0.51 defined(a) ).
% 0.13/0.51
% 0.13/0.51 cnf(not_less_or_equal_2,negated_conjecture,
% 0.13/0.51 ~ less_or_equal(a,a) ).
% 0.13/0.51
% 0.13/0.51 %--------------------------------------------------------------------------
% 0.13/0.51 %-------------------------------------------
% 0.13/0.51 % Proof found
% 0.13/0.51 % SZS status Theorem for theBenchmark
% 0.13/0.51 % SZS output start Proof
% 0.13/0.51 %ClaNum:29(EqnAxiom:0)
% 0.13/0.51 %VarNum:128(SingletonVarNum:50)
% 0.13/0.51 %MaxLitNum:4
% 0.13/0.51 %MaxfuncDepth:2
% 0.13/0.51 %SharedTerms:8
% 0.13/0.51 %goalClause: 5
% 0.13/0.51 %singleGoalClaCount:1
% 0.13/0.51 [1]P1(a1)
% 0.13/0.51 [2]P1(a4)
% 0.13/0.51 [3]P1(a2)
% 0.13/0.51 [4]~P2(a1,a4)
% 0.13/0.51 [5]~P3(a2,a2)
% 0.13/0.51 [7]~P1(x71)+P2(x71,x71)
% 0.13/0.51 [6]~P1(x61)+P1(f5(x61))
% 0.13/0.51 [11]~P1(x111)+P2(f3(a1,x111),x111)
% 0.13/0.51 [12]~P1(x121)+P2(f7(a4,x121),x121)
% 0.13/0.51 [15]~P1(x151)+P2(f3(x151,f5(x151)),a1)
% 0.13/0.51 [9]~P2(x92,x91)+P2(x91,x92)
% 0.13/0.51 [8]~P1(x81)+P2(x81,a1)+P1(f6(x81))
% 0.13/0.51 [20]~P1(x201)+P2(x201,a1)+P2(f7(x201,f6(x201)),a4)
% 0.13/0.51 [17]~P3(x172,x171)+~P3(x171,x172)+P2(x171,x172)
% 0.13/0.51 [13]~P1(x132)+~P1(x131)+P1(f3(x131,x132))
% 0.13/0.51 [14]~P1(x142)+~P1(x141)+P1(f7(x141,x142))
% 0.13/0.51 [21]~P3(a1,x212)+~P3(a1,x211)+P3(a1,f7(x211,x212))
% 0.13/0.51 [22]~P1(x222)+~P1(x221)+P2(f3(x221,x222),f3(x222,x221))
% 0.13/0.51 [23]~P1(x232)+~P1(x231)+P2(f7(x231,x232),f7(x232,x231))
% 0.13/0.51 [16]~P2(x161,x163)+P2(x161,x162)+~P2(x163,x162)
% 0.13/0.51 [18]~P3(x183,x182)+P3(x181,x182)+~P2(x183,x181)
% 0.13/0.51 [19]~P3(x191,x193)+P3(x191,x192)+~P3(x193,x192)
% 0.13/0.51 [24]~P1(x242)+~P2(x241,x243)+P2(f3(x241,x242),f3(x243,x242))
% 0.13/0.51 [25]~P1(x252)+~P2(x251,x253)+P2(f7(x251,x252),f7(x253,x252))
% 0.13/0.51 [26]~P1(x262)+~P3(x261,x263)+P3(f3(x261,x262),f3(x263,x262))
% 0.13/0.51 [10]P3(x102,x101)+~P1(x101)+~P1(x102)+P3(x101,x102)
% 0.13/0.51 [27]~P1(x273)+~P1(x272)+~P1(x271)+P2(f3(x271,f3(x272,x273)),f3(f3(x271,x272),x273))
% 0.13/0.51 [28]~P1(x283)+~P1(x282)+~P1(x281)+P2(f7(x281,f7(x282,x283)),f7(f7(x281,x282),x283))
% 0.13/0.51 [29]~P1(x293)+~P1(x292)+~P1(x291)+P2(f3(f7(x291,x292),f7(x293,x292)),f7(f3(x291,x293),x292))
% 0.13/0.51 %EqnAxiom
% 0.13/0.51
% 0.13/0.51 %-------------------------------------------
% 0.13/0.51 cnf(30,plain,
% 0.13/0.51 ($false),
% 0.13/0.51 inference(scs_inference,[],[5,3,10]),
% 0.13/0.51 ['proof']).
% 0.13/0.51 % SZS output end Proof
% 0.13/0.51 % Total time :0.000000s
%------------------------------------------------------------------------------