%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD006-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:08 EDT 2024
% Result : Unsatisfiable 0.12s 0.51s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : FLD006-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.00/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:45:38 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.12/0.47 start to proof:theBenchmark
% 0.12/0.51 %-------------------------------------------
% 0.12/0.51 % File :CSE---1.7
% 0.12/0.51 % Problem :theBenchmark
% 0.12/0.51 % Transform :cnf
% 0.12/0.51 % Format :tptp:raw
% 0.12/0.51 % Command :java -jar mcs_scs.jar %d %s
% 0.12/0.51
% 0.12/0.51 % Result :Theorem 0.000000s
% 0.12/0.51 % Output :CNFRefutation 0.000000s
% 0.12/0.51 %-------------------------------------------
% 0.12/0.51 %--------------------------------------------------------------------------
% 0.12/0.51 % File : FLD006-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.12/0.51 % Domain : Field Theory (Ordered fields)
% 0.12/0.51 % Problem : In the additive group it holds: inverse(identity)=identity
% 0.12/0.51 % Version : [Dra93] axioms : Especial.
% 0.12/0.51 % Theorem formulation : Functional with glxx axiom set.
% 0.12/0.51 % English :
% 0.12/0.51
% 0.12/0.51 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 0.12/0.51 % Source : [Dra93]
% 0.12/0.51 % Names :
% 0.12/0.51
% 0.12/0.51 % Status : Unsatisfiable
% 0.12/0.51 % Rating : 0.00 v2.4.0, 0.00 v2.1.0
% 0.12/0.51 % Syntax : Number of clauses : 28 ( 4 unt; 3 nHn; 28 RR)
% 0.12/0.51 % Number of literals : 74 ( 0 equ; 45 neg)
% 0.12/0.51 % Maximal clause size : 4 ( 2 avg)
% 0.12/0.51 % Maximal term depth : 3 ( 1 avg)
% 0.12/0.51 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 0.12/0.51 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 0.12/0.51 % Number of variables : 50 ( 0 sgn)
% 0.12/0.51 % SPC : CNF_UNS_RFO_NEQ_NHN
% 0.12/0.51
% 0.12/0.51 % Comments :
% 0.12/0.51 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 0.12/0.51 %--------------------------------------------------------------------------
% 0.12/0.51 include('Axioms/FLD001-0.ax').
% 0.12/0.51 %--------------------------------------------------------------------------
% 0.12/0.51 cnf(additive_inverse_not_equal_to_additive_identity_1,negated_conjecture,
% 0.12/0.51 ~ equalish(additive_inverse(additive_identity),additive_identity) ).
% 0.12/0.51
% 0.12/0.51 %--------------------------------------------------------------------------
% 0.12/0.51 %-------------------------------------------
% 0.12/0.51 % Proof found
% 0.12/0.51 % SZS status Theorem for theBenchmark
% 0.12/0.51 % SZS output start Proof
% 0.12/0.51 %ClaNum:28(EqnAxiom:0)
% 0.12/0.51 %VarNum:128(SingletonVarNum:50)
% 0.12/0.51 %MaxLitNum:4
% 0.12/0.51 %MaxfuncDepth:2
% 0.12/0.51 %SharedTerms:7
% 0.12/0.51 %goalClause: 4
% 0.12/0.51 %singleGoalClaCount:1
% 0.12/0.51 [1]P1(a1)
% 0.12/0.51 [2]P1(a3)
% 0.12/0.51 [3]~P2(a1,a3)
% 0.12/0.51 [4]~P2(f4(a1),a1)
% 0.12/0.51 [6]~P1(x61)+P2(x61,x61)
% 0.12/0.51 [5]~P1(x51)+P1(f4(x51))
% 0.12/0.51 [10]~P1(x101)+P2(f2(a1,x101),x101)
% 0.12/0.51 [11]~P1(x111)+P2(f6(a3,x111),x111)
% 0.12/0.51 [14]~P1(x141)+P2(f2(x141,f4(x141)),a1)
% 0.12/0.51 [8]~P2(x82,x81)+P2(x81,x82)
% 0.12/0.51 [7]~P1(x71)+P2(x71,a1)+P1(f5(x71))
% 0.12/0.51 [19]~P1(x191)+P2(x191,a1)+P2(f6(x191,f5(x191)),a3)
% 0.12/0.51 [16]~P3(x162,x161)+~P3(x161,x162)+P2(x161,x162)
% 0.12/0.51 [12]~P1(x122)+~P1(x121)+P1(f2(x121,x122))
% 0.12/0.51 [13]~P1(x132)+~P1(x131)+P1(f6(x131,x132))
% 0.12/0.51 [20]~P3(a1,x202)+~P3(a1,x201)+P3(a1,f6(x201,x202))
% 0.12/0.51 [21]~P1(x212)+~P1(x211)+P2(f2(x211,x212),f2(x212,x211))
% 0.12/0.51 [22]~P1(x222)+~P1(x221)+P2(f6(x221,x222),f6(x222,x221))
% 0.12/0.51 [15]~P2(x151,x153)+P2(x151,x152)+~P2(x153,x152)
% 0.12/0.51 [17]~P3(x173,x172)+P3(x171,x172)+~P2(x173,x171)
% 0.12/0.51 [18]~P3(x181,x183)+P3(x181,x182)+~P3(x183,x182)
% 0.12/0.52 [23]~P1(x232)+~P2(x231,x233)+P2(f2(x231,x232),f2(x233,x232))
% 0.12/0.52 [24]~P1(x242)+~P2(x241,x243)+P2(f6(x241,x242),f6(x243,x242))
% 0.12/0.52 [25]~P1(x252)+~P3(x251,x253)+P3(f2(x251,x252),f2(x253,x252))
% 0.12/0.52 [9]P3(x92,x91)+~P1(x91)+~P1(x92)+P3(x91,x92)
% 0.12/0.52 [26]~P1(x263)+~P1(x262)+~P1(x261)+P2(f2(x261,f2(x262,x263)),f2(f2(x261,x262),x263))
% 0.12/0.52 [27]~P1(x273)+~P1(x272)+~P1(x271)+P2(f6(x271,f6(x272,x273)),f6(f6(x271,x272),x273))
% 0.12/0.52 [28]~P1(x283)+~P1(x282)+~P1(x281)+P2(f2(f6(x281,x282),f6(x283,x282)),f6(f2(x281,x283),x282))
% 0.12/0.52 %EqnAxiom
% 0.12/0.52
% 0.12/0.52 %-------------------------------------------
% 0.12/0.52 cnf(29,plain,
% 0.12/0.52 (~P2(a1,f4(a1))),
% 0.12/0.52 inference(scs_inference,[],[4,8])).
% 0.12/0.52 cnf(50,plain,
% 0.12/0.52 (P2(f2(a1,f4(a1)),f4(a1))),
% 0.12/0.52 inference(scs_inference,[],[1,10,5])).
% 0.12/0.52 cnf(53,plain,
% 0.12/0.52 (~P2(f2(a1,f4(a1)),a1)),
% 0.12/0.52 inference(scs_inference,[],[29,50,15,8])).
% 0.12/0.52 cnf(59,plain,
% 0.12/0.52 ($false),
% 0.12/0.52 inference(scs_inference,[],[1,53,14]),
% 0.12/0.52 ['proof']).
% 0.12/0.52 % SZS output end Proof
% 0.12/0.52 % Total time :0.000000s
%------------------------------------------------------------------------------