%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD028-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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:18 EDT 2024
% Result : Unsatisfiable 58.76s 58.85s
% Output : CNFRefutation 58.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : FLD028-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n024.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Wed Jun 19 10:31:39 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.16/0.52 start to proof:theBenchmark
% 58.76/58.84 %-------------------------------------------
% 58.76/58.84 % File :CSE---1.7
% 58.76/58.84 % Problem :theBenchmark
% 58.76/58.84 % Transform :cnf
% 58.76/58.84 % Format :tptp:raw
% 58.76/58.84 % Command :java -jar mcs_scs.jar %d %s
% 58.76/58.84
% 58.76/58.84 % Result :Theorem 58.270000s
% 58.76/58.84 % Output :CNFRefutation 58.270000s
% 58.76/58.84 %-------------------------------------------
% 58.76/58.85 %--------------------------------------------------------------------------
% 58.76/58.85 % File : FLD028-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 58.76/58.85 % Domain : Field Theory (Ordered fields)
% 58.76/58.85 % Problem : The solution of a multiplicative linear equation is unique
% 58.76/58.85 % Version : [Dra93] axioms : Especial.
% 58.76/58.85 % Theorem formulation : Functional with re axiom set.
% 58.76/58.85 % English :
% 58.76/58.85
% 58.76/58.85 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 58.76/58.85 % Source : [Dra93]
% 58.76/58.85 % Names :
% 58.76/58.85
% 58.76/58.85 % Status : Unsatisfiable
% 58.76/58.85 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.14 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.20 v2.4.0, 0.40 v2.3.0, 0.33 v2.2.1, 0.67 v2.1.0
% 58.76/58.85 % Syntax : Number of clauses : 34 ( 11 unt; 3 nHn; 34 RR)
% 58.76/58.85 % Number of literals : 85 ( 0 equ; 51 neg)
% 58.76/58.85 % Maximal clause size : 5 ( 2 avg)
% 58.76/58.85 % Maximal term depth : 2 ( 1 avg)
% 58.76/58.85 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 58.76/58.85 % Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% 58.76/58.85 % Number of variables : 73 ( 0 sgn)
% 58.76/58.85 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.76/58.85
% 58.76/58.85 % Comments :
% 58.76/58.85 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 58.76/58.85 %--------------------------------------------------------------------------
% 58.76/58.85 include('Axioms/FLD002-0.ax').
% 58.76/58.85 %--------------------------------------------------------------------------
% 58.76/58.85 cnf(a_is_defined,hypothesis,
% 58.76/58.85 defined(a) ).
% 58.76/58.85
% 58.76/58.85 cnf(b_is_defined,hypothesis,
% 58.76/58.85 defined(b) ).
% 58.76/58.85
% 58.76/58.85 cnf(u_is_defined,hypothesis,
% 58.76/58.85 defined(u) ).
% 58.76/58.85
% 58.76/58.85 cnf(v_is_defined,hypothesis,
% 58.76/58.85 defined(v) ).
% 58.76/58.85
% 58.76/58.85 cnf(not_sum_5,negated_conjecture,
% 58.76/58.85 ~ sum(additive_identity,a,additive_identity) ).
% 58.76/58.85
% 58.76/58.85 cnf(product_6,negated_conjecture,
% 58.76/58.85 product(a,u,b) ).
% 58.76/58.85
% 58.76/58.85 cnf(product_7,negated_conjecture,
% 58.76/58.85 product(a,v,b) ).
% 58.76/58.85
% 58.76/58.85 cnf(not_product_8,negated_conjecture,
% 58.76/58.85 ~ product(multiplicative_identity,u,v) ).
% 58.76/58.85
% 58.76/58.85 %--------------------------------------------------------------------------
% 58.76/58.85 %-------------------------------------------
% 58.76/58.85 % Proof found
% 58.76/58.85 % SZS status Theorem for theBenchmark
% 58.76/58.85 % SZS output start Proof
% 58.76/58.85 %ClaNum:34(EqnAxiom:0)
% 58.76/58.85 %VarNum:162(SingletonVarNum:73)
% 58.76/58.85 %MaxLitNum:5
% 58.76/58.85 %MaxfuncDepth:1
% 58.76/58.85 %SharedTerms:17
% 58.76/58.85 %goalClause: 7 8 10 11
% 58.76/58.85 %singleGoalClaCount:4
% 58.76/58.85 [1]P1(a1)
% 58.76/58.85 [2]P1(a4)
% 58.76/58.85 [3]P1(a2)
% 58.76/58.85 [4]P1(a5)
% 58.76/58.85 [5]P1(a7)
% 58.76/58.85 [6]P1(a10)
% 58.76/58.85 [7]P2(a2,a7,a5)
% 58.76/58.85 [8]P2(a2,a10,a5)
% 58.76/58.85 [9]~P4(a1,a1,a4)
% 58.76/58.85 [10]~P4(a1,a2,a1)
% 58.76/58.85 [11]~P2(a4,a7,a10)
% 58.76/58.85 [17]~P1(x171)+P4(a1,x171,x171)
% 58.76/58.85 [18]~P1(x181)+P2(a4,x181,x181)
% 58.76/58.85 [12]~P1(x121)+P1(f6(x121))
% 58.76/58.85 [19]~P1(x191)+P4(f6(x191),x191,a1)
% 58.76/58.85 [26]~P4(x262,x261,x263)+P4(x261,x262,x263)
% 58.76/58.85 [27]~P2(x272,x271,x273)+P2(x271,x272,x273)
% 58.76/58.85 [20]~P1(x201)+P4(a1,x201,a1)+P1(f9(x201))
% 58.76/58.85 [24]~P1(x241)+P2(f9(x241),x241,a4)+P4(a1,x241,a1)
% 58.76/58.85 [23]~P3(x232,x231)+~P3(x231,x232)+P4(a1,x231,x232)
% 58.76/58.85 [14]~P1(x142)+~P1(x141)+P1(f3(x141,x142))
% 58.76/58.85 [15]~P1(x152)+~P1(x151)+P1(f8(x151,x152))
% 58.76/58.85 [21]~P1(x212)+~P1(x211)+P4(x211,x212,f3(x211,x212))
% 58.76/58.85 [22]~P1(x222)+~P1(x221)+P2(x221,x222,f8(x221,x222))
% 58.76/58.85 [16]~P3(x161,x163)+P3(x161,x162)+~P3(x163,x162)
% 58.76/58.85 [13]P3(x132,x131)+~P1(x131)+~P1(x132)+P3(x131,x132)
% 58.76/58.85 [25]~P2(x253,x252,x251)+P3(a1,x251)+~P3(a1,x252)+~P3(a1,x253)
% 58.76/58.85 [28]~P4(x283,x285,x281)+P3(x281,x282)+~P4(x284,x285,x282)+~P3(x283,x284)
% 58.76/58.85 [29]~P4(x291,x296,x294)+P4(x291,x292,x293)+~P4(x294,x295,x293)+~P4(x296,x295,x292)
% 58.76/58.85 [30]~P4(x306,x304,x301)+P4(x301,x302,x303)+~P4(x304,x302,x305)+~P4(x306,x305,x303)
% 58.76/58.85 [31]~P2(x311,x316,x314)+P2(x311,x312,x313)+~P2(x314,x315,x313)+~P2(x316,x315,x312)
% 58.76/58.85 [32]~P2(x326,x324,x321)+P2(x321,x322,x323)+~P2(x324,x322,x325)+~P2(x326,x325,x323)
% 58.76/58.85 [33]~P2(x335,x337,x332)+~P2(x334,x337,x331)+P4(x331,x332,x333)+~P4(x334,x335,x336)+~P2(x336,x337,x333)
% 58.76/58.85 [34]~P2(x347,x342,x345)+~P2(x346,x342,x344)+P2(x341,x342,x343)+~P4(x344,x345,x343)+~P4(x346,x347,x341)
% 58.76/58.85 %EqnAxiom
% 58.76/58.85
% 58.76/58.85 %-------------------------------------------
% 58.76/58.86 cnf(35,plain,
% 58.76/58.86 (~P2(a7,a4,a10)),
% 58.76/58.86 inference(scs_inference,[],[11,27])).
% 58.76/58.86 cnf(39,plain,
% 58.76/58.86 (P3(a1,a1)),
% 58.76/58.86 inference(scs_inference,[],[10,11,1,27,26,13])).
% 58.76/58.86 cnf(43,plain,
% 58.76/58.86 (~P2(x431,a2,a2)+P2(x431,a5,a5)),
% 58.76/58.86 inference(scs_inference,[],[7,10,11,1,27,26,13,23,31])).
% 58.76/58.86 cnf(48,plain,
% 58.76/58.86 (P3(a4,a4)),
% 58.76/58.86 inference(scs_inference,[],[2,13])).
% 58.76/58.86 cnf(55,plain,
% 58.76/58.86 (P3(a2,a2)),
% 58.76/58.86 inference(scs_inference,[],[3,13])).
% 58.76/58.86 cnf(97,plain,
% 58.76/58.86 (P4(a1,f6(a4),f6(a4))),
% 58.76/58.86 inference(scs_inference,[],[2,17,12])).
% 58.76/58.86 cnf(209,plain,
% 58.76/58.86 (P2(a5,x2091,a5)+~P2(x2091,a2,a2)),
% 58.76/58.86 inference(scs_inference,[],[43,27])).
% 58.76/58.86 cnf(273,plain,
% 58.76/58.86 (P2(a5,a4,a5)),
% 58.76/58.86 inference(scs_inference,[],[3,209,18])).
% 58.76/58.86 cnf(1833,plain,
% 58.76/58.86 (P2(a4,f6(a4),f6(a4))),
% 58.76/58.86 inference(scs_inference,[],[2,12,18])).
% 58.76/58.86 cnf(1952,plain,
% 58.76/58.86 (P4(a1,f6(a5),f6(a5))),
% 58.76/58.86 inference(scs_inference,[],[4,12,17])).
% 58.76/58.86 cnf(2100,plain,
% 58.76/58.86 (P2(a4,f6(a5),f6(a5))),
% 58.76/58.86 inference(scs_inference,[],[4,12,18])).
% 58.76/58.86 cnf(2183,plain,
% 58.76/58.86 (P4(f6(f6(a4)),f6(a4),a1)),
% 58.76/58.86 inference(scs_inference,[],[2,12,19])).
% 58.76/58.86 cnf(2186,plain,
% 58.76/58.86 (~P4(a2,f6(a4),f6(a4))),
% 58.76/58.86 inference(scs_inference,[],[10,2183,30,26])).
% 58.76/58.86 cnf(2203,plain,
% 58.76/58.86 (P4(f6(f6(a5)),f6(a5),a1)),
% 58.76/58.86 inference(scs_inference,[],[4,12,19])).
% 58.76/58.86 cnf(2206,plain,
% 58.76/58.86 (~P4(a2,f6(a5),f6(a5))),
% 58.76/58.86 inference(scs_inference,[],[10,2203,30,26])).
% 58.76/58.86 cnf(2622,plain,
% 58.76/58.86 (P4(a10,a1,a10)),
% 58.76/58.86 inference(scs_inference,[],[6,17,26])).
% 58.76/58.86 cnf(2884,plain,
% 58.76/58.86 (~P4(a1,a1,x28841)+P4(a10,x28841,a10)),
% 58.76/58.86 inference(scs_inference,[],[2622,29])).
% 58.76/58.86 cnf(2897,plain,
% 58.76/58.86 (P4(x28971,a10,a10)+~P4(a1,a1,x28971)),
% 58.76/58.86 inference(scs_inference,[],[2884,26])).
% 58.76/58.86 cnf(2925,plain,
% 58.76/58.86 (P4(a1,a10,a10)),
% 58.76/58.86 inference(scs_inference,[],[1,2897,17])).
% 58.76/58.86 cnf(3334,plain,
% 58.76/58.86 (~P4(a1,a1,a2)),
% 58.76/58.86 inference(scs_inference,[],[2186,97,30])).
% 58.76/58.86 cnf(3561,plain,
% 58.76/58.86 (~P2(a7,a4,x35611)+P2(a2,x35611,a5)),
% 58.76/58.86 inference(scs_inference,[],[7,273,31])).
% 58.76/58.86 cnf(3564,plain,
% 58.76/58.86 (~P2(a10,a4,x35641)+P2(a2,x35641,a5)),
% 58.76/58.86 inference(scs_inference,[],[8,273,31])).
% 58.76/58.86 cnf(3572,plain,
% 58.76/58.86 (~P2(a4,a4,x35721)+P2(a5,x35721,a5)),
% 58.76/58.86 inference(scs_inference,[],[273,31])).
% 58.76/58.86 cnf(3595,plain,
% 58.76/58.86 (P2(x35951,a2,a5)+~P2(a7,a4,x35951)),
% 58.76/58.86 inference(scs_inference,[],[3561,27])).
% 58.76/58.86 cnf(3615,plain,
% 58.76/58.86 (P2(x36151,a2,a5)+~P2(a10,a4,x36151)),
% 58.76/58.86 inference(scs_inference,[],[3564,27])).
% 58.76/58.86 cnf(3663,plain,
% 58.76/58.86 (P2(x36631,a5,a5)+~P2(a4,a4,x36631)),
% 58.76/58.86 inference(scs_inference,[],[3572,27])).
% 58.76/58.86 cnf(3679,plain,
% 58.76/58.86 (P2(f8(a7,a4),a2,a5)),
% 58.76/58.86 inference(scs_inference,[],[2,5,3595,22])).
% 58.76/58.86 cnf(3743,plain,
% 58.76/58.86 (P2(f8(a10,a4),a2,a5)),
% 58.76/58.86 inference(scs_inference,[],[2,6,3615,22])).
% 58.76/58.86 cnf(3798,plain,
% 58.76/58.86 (P2(f8(a4,a4),a5,a5)),
% 58.76/58.86 inference(scs_inference,[],[2,3663,22])).
% 58.76/58.86 cnf(3881,plain,
% 58.76/58.86 (P2(a7,a2,a5)),
% 58.76/58.86 inference(scs_inference,[],[7,27])).
% 58.76/58.86 cnf(3887,plain,
% 58.76/58.86 (P2(a10,a2,a5)),
% 58.76/58.86 inference(scs_inference,[],[8,27])).
% 58.76/58.86 cnf(3894,plain,
% 58.76/58.86 (P2(a2,f8(a7,a4),a5)),
% 58.76/58.86 inference(scs_inference,[],[3679,27])).
% 58.76/58.86 cnf(3914,plain,
% 58.76/58.86 (~P2(a1,a2,x39141)+P4(x39141,a5,a5)),
% 58.76/58.86 inference(scs_inference,[],[2925,3798,3887,3894,48,27,31,32,28,33])).
% 58.76/58.86 cnf(3919,plain,
% 58.76/58.86 (~P2(a1,a4,a2)),
% 58.76/58.86 inference(scs_inference,[],[2206,2100,1952,27,33])).
% 58.76/58.86 cnf(4006,plain,
% 58.76/58.86 (P2(f9(a2),a2,a4)),
% 58.76/58.86 inference(scs_inference,[],[10,3,24])).
% 58.76/58.86 cnf(4015,plain,
% 58.76/58.86 (P2(a2,f9(a2),a4)),
% 58.76/58.86 inference(scs_inference,[],[4006,27])).
% 58.76/58.86 cnf(4017,plain,
% 58.76/58.86 (~P2(a5,f9(a2),a10)),
% 58.76/58.86 inference(scs_inference,[],[35,3881,4006,27,31])).
% 58.76/58.86 cnf(4052,plain,
% 58.76/58.86 (P2(a4,x40521,a4)+~P2(f9(a2),x40521,f9(a2))),
% 58.76/58.86 inference(scs_inference,[],[4015,32])).
% 58.76/58.86 cnf(4129,plain,
% 58.76/58.86 (P4(a5,x41291,a5)+~P2(a1,a2,x41291)),
% 58.76/58.86 inference(scs_inference,[],[3914,26])).
% 58.76/58.86 cnf(4227,plain,
% 58.76/58.86 (P4(a5,f8(a1,a2),a5)),
% 58.76/58.86 inference(scs_inference,[],[3,1,4129,22])).
% 58.76/58.86 cnf(5078,plain,
% 58.76/58.86 (~P2(x50781,f9(a2),f9(a2))+P2(a4,x50781,a4)),
% 58.76/58.86 inference(scs_inference,[],[4052,27])).
% 58.76/58.86 cnf(5548,plain,
% 58.76/58.86 (~P1(f9(a2))+P2(a4,a4,a4)),
% 58.76/58.86 inference(scs_inference,[],[5078,18])).
% 58.76/58.86 cnf(5564,plain,
% 58.76/58.86 (P2(a4,a4,a4)),
% 58.76/58.86 inference(scs_inference,[],[10,3,5548,20])).
% 58.76/58.86 cnf(5566,plain,
% 58.76/58.86 (~P2(a4,x55661,a7)+~P2(a4,x55661,a10)),
% 58.76/58.86 inference(scs_inference,[],[11,5564,31])).
% 58.76/58.86 cnf(5582,plain,
% 58.76/58.86 (~P2(a4,a10,a7)),
% 58.76/58.86 inference(scs_inference,[],[6,5566,18])).
% 58.76/58.86 cnf(5808,plain,
% 58.76/58.86 (~P2(a4,a1,a2)),
% 58.76/58.86 inference(scs_inference,[],[3919,4,12,27])).
% 58.76/58.86 cnf(5810,plain,
% 58.76/58.86 (P2(a4,a1,a1)),
% 58.76/58.86 inference(scs_inference,[],[3919,4,1,12,27,18])).
% 58.76/58.86 cnf(5814,plain,
% 58.76/58.86 (P4(f6(a5),a5,a1)),
% 58.76/58.86 inference(scs_inference,[],[3919,4,1,12,27,18,17,19])).
% 58.76/58.86 cnf(5816,plain,
% 58.76/58.86 (P1(f3(a5,a5))),
% 58.76/58.86 inference(scs_inference,[],[3919,4,1,12,27,18,17,19,14])).
% 58.76/58.86 cnf(5830,plain,
% 58.76/58.86 (~P4(f6(a5),a5,a2)),
% 58.76/58.86 inference(scs_inference,[],[3919,3798,3334,4,1,3,1952,10,39,12,27,18,17,19,14,15,22,20,21,23,31,29])).
% 58.76/58.86 cnf(5832,plain,
% 58.76/58.86 (~P2(f9(a2),a5,a7)),
% 58.76/58.86 inference(scs_inference,[],[3919,5582,4006,3798,3334,4,1,3,1952,8,10,39,12,27,18,17,19,14,15,22,20,21,23,31,29,32])).
% 58.76/58.86 cnf(5848,plain,
% 58.76/58.86 (~P2(a5,f9(a2),a7)),
% 58.76/58.86 inference(scs_inference,[],[5832,2,12,27])).
% 58.76/58.86 cnf(5854,plain,
% 58.76/58.86 (P4(f6(a4),a4,a1)),
% 58.76/58.86 inference(scs_inference,[],[5816,5832,2,12,27,17,18,19])).
% 58.76/58.86 cnf(5856,plain,
% 58.76/58.86 (P4(a4,a4,f3(a4,a4))),
% 58.76/58.86 inference(scs_inference,[],[5816,5832,2,12,27,17,18,19,21])).
% 58.76/58.86 cnf(5858,plain,
% 58.76/58.86 (P2(a4,a4,f8(a4,a4))),
% 58.76/58.86 inference(scs_inference,[],[5816,5832,2,12,27,17,18,19,21,22])).
% 58.76/58.87 cnf(5860,plain,
% 58.76/58.87 (P1(f3(a4,a4))),
% 58.76/58.87 inference(scs_inference,[],[5816,5832,2,12,27,17,18,19,21,22,14])).
% 58.76/58.87 cnf(5862,plain,
% 58.76/58.87 (P1(f8(a4,a4))),
% 58.76/58.87 inference(scs_inference,[],[5816,5832,2,12,27,17,18,19,21,22,14,15])).
% 58.76/58.87 cnf(5864,plain,
% 58.76/58.87 (P4(a1,a4,a4)),
% 58.76/58.87 inference(scs_inference,[],[5816,5832,2,48,12,27,17,18,19,21,22,14,15,23])).
% 58.76/58.87 cnf(5872,plain,
% 58.76/58.87 (P3(f3(a4,a4),f3(a4,a4))),
% 58.76/58.87 inference(scs_inference,[],[5816,5814,5830,5832,4017,5564,3743,2,4015,4227,48,12,27,17,18,19,21,22,14,15,23,29,31,32,28])).
% 58.76/58.87 cnf(5874,plain,
% 58.76/58.87 (~P2(a1,f6(a4),a2)),
% 58.76/58.87 inference(scs_inference,[],[5816,5814,5830,5832,4017,5564,3743,2186,1833,2,4015,4227,48,12,27,17,18,19,21,22,14,15,23,29,31,32,28,33])).
% 58.76/58.87 cnf(5897,plain,
% 58.76/58.87 (P1(f3(a7,a7))),
% 58.76/58.87 inference(scs_inference,[],[5862,5860,5874,5,12,27,18,17,19,15,21,14])).
% 58.76/58.87 cnf(5907,plain,
% 58.76/58.87 (~P2(f8(a4,a4),a1,a2)),
% 58.76/58.87 inference(scs_inference,[],[5810,5808,5864,5872,5862,5860,5874,5858,5856,5848,5854,3743,5,4015,12,27,18,17,19,15,21,14,22,23,29,32,31])).
% 58.76/58.87 cnf(5942,plain,
% 58.76/58.87 (~P2(a4,a7,a7)),
% 58.76/58.87 inference(scs_inference,[],[7,5897,5907,5832,4006,6,55,12,27,17,18,19,22,15,14,21,23,31])).
% 58.76/58.87 cnf(6152,plain,
% 58.76/58.87 ($false),
% 58.76/58.87 inference(scs_inference,[],[5942,5,18]),
% 58.76/58.87 ['proof']).
% 58.76/58.87 % SZS output end Proof
% 58.76/58.87 % Total time :58.270000s
%------------------------------------------------------------------------------