%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD010-1 : TPTP v8.2.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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:10 EDT 2024
% Result : Unsatisfiable 10.80s 10.93s
% Output : CNFRefutation 10.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : FLD010-1 : TPTP v8.2.0. Bugfixed v2.7.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 11:22:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.43/0.62 start to proof:theBenchmark
% 10.80/10.92 %-------------------------------------------
% 10.80/10.92 % File :CSE---1.7
% 10.80/10.92 % Problem :theBenchmark
% 10.80/10.92 % Transform :cnf
% 10.80/10.92 % Format :tptp:raw
% 10.80/10.92 % Command :java -jar mcs_scs.jar %d %s
% 10.80/10.92
% 10.80/10.92 % Result :Theorem 10.260000s
% 10.80/10.92 % Output :CNFRefutation 10.260000s
% 10.80/10.92 %-------------------------------------------
% 10.80/10.92 %--------------------------------------------------------------------------
% 10.80/10.92 % File : FLD010-1 : TPTP v8.2.0. Bugfixed v2.7.0.
% 10.80/10.92 % Domain : Field Theory (Ordered fields)
% 10.80/10.92 % Problem : In the multiplicative group inverse(identity)=identity
% 10.80/10.92 % Version : [Dra93] axioms : Especial.
% 10.80/10.92 % Theorem formulation : Functional with glxx axiom set.
% 10.80/10.92 % English :
% 10.80/10.92
% 10.80/10.92 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 10.80/10.92 % Source : [Dra93]
% 10.80/10.92 % Names :
% 10.80/10.92
% 10.80/10.92 % Status : Unsatisfiable
% 10.80/10.93 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.00 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.21 v4.1.0, 0.12 v4.0.1, 0.00 v2.7.0
% 10.80/10.93 % Syntax : Number of clauses : 28 ( 4 unt; 3 nHn; 28 RR)
% 10.80/10.93 % Number of literals : 74 ( 0 equ; 45 neg)
% 10.80/10.93 % Maximal clause size : 4 ( 2 avg)
% 10.80/10.93 % Maximal term depth : 3 ( 1 avg)
% 10.80/10.93 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 10.80/10.93 % Number of functors : 6 ( 6 usr; 2 con; 0-2 aty)
% 10.80/10.93 % Number of variables : 50 ( 0 sgn)
% 10.80/10.93 % SPC : CNF_UNS_RFO_NEQ_NHN
% 10.80/10.93
% 10.80/10.93 % Comments :
% 10.80/10.93 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 10.80/10.93 % : v2.7.0 - Removed duplicate clause
% 10.80/10.93 % additive_id_not_equal_to_multiplicative_id_1 (now in axioms)
% 10.80/10.93 %--------------------------------------------------------------------------
% 10.80/10.93 include('Axioms/FLD001-0.ax').
% 10.80/10.93 %--------------------------------------------------------------------------
% 10.80/10.93 cnf(multiplicative_inv_not_equal_to_multiplicative_id_2,negated_conjecture,
% 10.80/10.93 ~ equalish(multiplicative_inverse(multiplicative_identity),multiplicative_identity) ).
% 10.80/10.93
% 10.80/10.93 %--------------------------------------------------------------------------
% 10.80/10.93 %-------------------------------------------
% 10.80/10.93 % Proof found
% 10.80/10.93 % SZS status Theorem for theBenchmark
% 10.80/10.93 % SZS output start Proof
% 10.80/10.93 %ClaNum:28(EqnAxiom:0)
% 10.80/10.93 %VarNum:128(SingletonVarNum:50)
% 10.80/10.93 %MaxLitNum:4
% 10.80/10.93 %MaxfuncDepth:2
% 10.80/10.93 %SharedTerms:7
% 10.80/10.93 %goalClause: 4
% 10.80/10.93 %singleGoalClaCount:1
% 10.80/10.93 [1]P1(a1)
% 10.80/10.93 [2]P1(a3)
% 10.80/10.93 [3]~P2(a1,a3)
% 10.80/10.93 [4]~P2(f5(a3),a3)
% 10.80/10.93 [6]~P1(x61)+P2(x61,x61)
% 10.80/10.93 [5]~P1(x51)+P1(f4(x51))
% 10.80/10.93 [10]~P1(x101)+P2(f2(a1,x101),x101)
% 10.80/10.93 [11]~P1(x111)+P2(f6(a3,x111),x111)
% 10.80/10.93 [14]~P1(x141)+P2(f2(x141,f4(x141)),a1)
% 10.80/10.93 [8]~P2(x82,x81)+P2(x81,x82)
% 10.80/10.93 [7]~P1(x71)+P2(x71,a1)+P1(f5(x71))
% 10.80/10.93 [19]~P1(x191)+P2(x191,a1)+P2(f6(x191,f5(x191)),a3)
% 10.80/10.93 [16]~P3(x162,x161)+~P3(x161,x162)+P2(x161,x162)
% 10.80/10.93 [12]~P1(x122)+~P1(x121)+P1(f2(x121,x122))
% 10.80/10.93 [13]~P1(x132)+~P1(x131)+P1(f6(x131,x132))
% 10.80/10.93 [20]~P3(a1,x202)+~P3(a1,x201)+P3(a1,f6(x201,x202))
% 10.80/10.93 [21]~P1(x212)+~P1(x211)+P2(f2(x211,x212),f2(x212,x211))
% 10.80/10.93 [22]~P1(x222)+~P1(x221)+P2(f6(x221,x222),f6(x222,x221))
% 10.80/10.93 [15]~P2(x151,x153)+P2(x151,x152)+~P2(x153,x152)
% 10.80/10.93 [17]~P3(x173,x172)+P3(x171,x172)+~P2(x173,x171)
% 10.80/10.93 [18]~P3(x181,x183)+P3(x181,x182)+~P3(x183,x182)
% 10.80/10.93 [23]~P1(x232)+~P2(x231,x233)+P2(f2(x231,x232),f2(x233,x232))
% 10.80/10.93 [24]~P1(x242)+~P2(x241,x243)+P2(f6(x241,x242),f6(x243,x242))
% 10.80/10.93 [25]~P1(x252)+~P3(x251,x253)+P3(f2(x251,x252),f2(x253,x252))
% 10.80/10.93 [9]P3(x92,x91)+~P1(x91)+~P1(x92)+P3(x91,x92)
% 10.80/10.93 [26]~P1(x263)+~P1(x262)+~P1(x261)+P2(f2(x261,f2(x262,x263)),f2(f2(x261,x262),x263))
% 10.80/10.93 [27]~P1(x273)+~P1(x272)+~P1(x271)+P2(f6(x271,f6(x272,x273)),f6(f6(x271,x272),x273))
% 10.80/10.93 [28]~P1(x283)+~P1(x282)+~P1(x281)+P2(f2(f6(x281,x282),f6(x283,x282)),f6(f2(x281,x283),x282))
% 10.80/10.93 %EqnAxiom
% 10.80/10.93
% 10.80/10.93 %-------------------------------------------
% 10.80/10.93 cnf(1317,plain,
% 10.80/10.93 (P1(f5(a3))),
% 10.80/10.93 inference(scs_inference,[],[3,2,8,7])).
% 10.80/10.93 cnf(1321,plain,
% 10.80/10.93 (P2(f6(a3,f5(a3)),a3)),
% 10.80/10.93 inference(scs_inference,[],[3,2,8,19])).
% 10.80/10.93 cnf(1324,plain,
% 10.80/10.93 (~P2(f6(a3,f5(a3)),f5(a3))),
% 10.80/10.93 inference(scs_inference,[],[4,1321,15,8])).
% 10.80/10.93 cnf(1332,plain,
% 10.80/10.93 ($false),
% 10.80/10.93 inference(scs_inference,[],[1324,1317,11]),
% 10.80/10.93 ['proof']).
% 10.80/10.94 % SZS output end Proof
% 10.80/10.94 % Total time :10.260000s
%------------------------------------------------------------------------------