%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KLE005+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 09:59:46 EDT 2024
% Result : Theorem 10.46s 10.60s
% Output : CNFRefutation 10.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.09 % Problem : KLE005+1 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.09 % Command : java -jar /export/starexec/sandbox2/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 : Thu Jun 20 21:52:09 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark
% 10.46/10.59 %-------------------------------------------
% 10.46/10.59 % File :CSE---1.7
% 10.46/10.59 % Problem :theBenchmark
% 10.46/10.59 % Transform :cnf
% 10.46/10.59 % Format :tptp:raw
% 10.46/10.59 % Command :java -jar mcs_scs.jar %d %s
% 10.46/10.59
% 10.46/10.59 % Result :Theorem 10.120000s
% 10.46/10.59 % Output :CNFRefutation 10.120000s
% 10.46/10.59 %-------------------------------------------
% 10.46/10.60 %------------------------------------------------------------------------------
% 10.46/10.60 % File : KLE005+1 : TPTP v8.2.0. Released v4.0.0.
% 10.46/10.60 % Domain : Kleene Algebra (Idempotent Test Semirings)
% 10.46/10.60 % Problem : Complement - 0 is the complement of 1
% 10.46/10.60 % Version : [Hoe08] axioms.
% 10.46/10.60 % English :
% 10.46/10.60
% 10.46/10.60 % Refs : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% 10.46/10.60 % Source : [Hoe08]
% 10.46/10.60 % Names :
% 10.46/10.60
% 10.46/10.60 % Status : Theorem
% 10.46/10.60 % Rating : 0.06 v8.1.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.17 v6.0.0, 0.13 v5.5.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.10 v5.0.0, 0.08 v4.1.0, 0.04 v4.0.0
% 10.46/10.60 % Syntax : Number of formulae : 17 ( 12 unt; 0 def)
% 10.46/10.60 % Number of atoms : 25 ( 18 equ)
% 10.46/10.60 % Maximal formula atoms : 4 ( 1 avg)
% 10.46/10.60 % Number of connectives : 9 ( 1 ~; 0 |; 2 &)
% 10.46/10.60 % ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% 10.46/10.60 % Maximal formula depth : 6 ( 3 avg)
% 10.46/10.60 % Maximal term depth : 3 ( 1 avg)
% 10.46/10.60 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty)
% 10.46/10.60 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 10.46/10.60 % Number of variables : 29 ( 28 !; 1 ?)
% 10.46/10.60 % SPC : FOF_THM_RFO_SEQ
% 10.46/10.60
% 10.46/10.60 % Comments : Equational encoding
% 10.46/10.60 %------------------------------------------------------------------------------
% 10.46/10.60 %---Include axioms for idempotent test semiring
% 10.46/10.60 include('Axioms/KLE001+0.ax').
% 10.46/10.60 %---Include test axioms
% 10.46/10.60 include('Axioms/KLE001+1.ax').
% 10.46/10.60 %------------------------------------------------------------------------------
% 10.46/10.60 fof(goals,conjecture,
% 10.46/10.60 c(one) = zero ).
% 10.46/10.60
% 10.46/10.60 %------------------------------------------------------------------------------
% 10.46/10.60 %-------------------------------------------
% 10.46/10.60 % Proof found
% 10.46/10.60 % SZS status Theorem for theBenchmark
% 10.46/10.60 % SZS output start Proof
% 10.53/10.60 %ClaNum:37(EqnAxiom:14)
% 10.53/10.60 %VarNum:89(SingletonVarNum:40)
% 10.53/10.60 %MaxLitNum:4
% 10.53/10.60 %MaxfuncDepth:2
% 10.53/10.60 %SharedTerms:4
% 10.53/10.60 %goalClause: 26
% 10.53/10.60 %singleGoalClaCount:1
% 10.53/10.60 [26]~E(f4(a6),a1)
% 10.53/10.60 [15]E(f2(x151,a1),a1)
% 10.53/10.60 [16]E(f2(a1,x161),a1)
% 10.53/10.60 [17]E(f3(x171,a1),x171)
% 10.53/10.60 [18]E(f2(x181,a6),x181)
% 10.53/10.60 [19]E(f2(a6,x191),x191)
% 10.53/10.60 [20]E(f3(x201,x201),x201)
% 10.53/10.60 [21]E(f3(x211,x212),f3(x212,x211))
% 10.53/10.60 [22]E(f3(f3(x221,x222),x223),f3(x221,f3(x222,x223)))
% 10.53/10.60 [23]E(f2(f2(x231,x232),x233),f2(x231,f2(x232,x233)))
% 10.53/10.60 [24]E(f3(f2(x241,x242),f2(x241,x243)),f2(x241,f3(x242,x243)))
% 10.53/10.60 [25]E(f3(f2(x251,x252),f2(x253,x252)),f2(f3(x251,x253),x252))
% 10.53/10.60 [27]P1(x271)+E(f4(x271),a1)
% 10.53/10.60 [29]~P1(x291)+P2(f5(x291),x291)
% 10.53/10.60 [28]P1(x281)+~P2(x282,x281)
% 10.53/10.60 [32]~P2(x322,x321)+E(f3(x321,x322),a6)
% 10.53/10.60 [33]~P2(x332,x331)+E(f2(x331,x332),a1)
% 10.53/10.60 [34]~P2(x341,x342)+E(f2(x341,x342),a1)
% 10.53/10.60 [35]~P3(x351,x352)+E(f3(x351,x352),x352)
% 10.53/10.60 [36]P3(x361,x362)+~E(f3(x361,x362),x362)
% 10.53/10.60 [30]~P1(x301)+P2(x301,x302)+~E(f4(x301),x302)
% 10.53/10.60 [31]~P1(x311)+~P2(x311,x312)+E(f4(x311),x312)
% 10.53/10.60 [37]P2(x371,x372)+~E(f3(x372,x371),a6)+~E(f2(x371,x372),a1)+~E(f2(x372,x371),a1)
% 10.53/10.60 %EqnAxiom
% 10.53/10.60 [1]E(x11,x11)
% 10.53/10.60 [2]E(x22,x21)+~E(x21,x22)
% 10.53/10.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 10.53/10.60 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 10.53/10.60 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 10.53/10.60 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 10.53/10.60 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 10.53/10.60 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 10.53/10.60 [9]~E(x91,x92)+E(f5(x91),f5(x92))
% 10.53/10.60 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 10.53/10.60 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 10.53/10.60 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 10.53/10.60 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133)
% 10.53/10.60 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141)
% 10.53/10.60
% 10.53/10.60 %-------------------------------------------
% 10.53/10.61 cnf(38,plain,
% 10.53/10.61 (~P1(x381)+P2(x381,f4(x381))),
% 10.53/10.61 inference(equality_inference,[],[30])).
% 10.53/10.61 cnf(39,plain,
% 10.53/10.61 (P1(a6)),
% 10.53/10.61 inference(scs_inference,[],[26,27])).
% 10.53/10.61 cnf(47,plain,
% 10.53/10.61 (E(f3(x471,x471),x471)),
% 10.53/10.61 inference(rename_variables,[],[20])).
% 10.53/10.61 cnf(57,plain,
% 10.53/10.61 (P2(a1,x571)+~E(a6,x571)),
% 10.53/10.61 inference(scs_inference,[],[26,20,47,17,18,19,27,2,36,31,3,13,14,37,10,11,12])).
% 10.53/10.61 cnf(331,plain,
% 10.53/10.61 (E(x3311,f2(x3311,a6))),
% 10.53/10.61 inference(scs_inference,[],[18,2])).
% 10.53/10.61 cnf(348,plain,
% 10.53/10.61 (E(x3481,f2(a6,x3481))),
% 10.53/10.61 inference(scs_inference,[],[331,19,57,2])).
% 10.53/10.61 cnf(1502,plain,
% 10.53/10.61 (E(f2(a6,f4(a6)),a1)),
% 10.53/10.61 inference(scs_inference,[],[39,34,38])).
% 10.53/10.61 cnf(1504,plain,
% 10.53/10.61 ($false),
% 10.53/10.61 inference(scs_inference,[],[26,348,1502,2,3]),
% 10.53/10.61 ['proof']).
% 10.53/10.61 % SZS output end Proof
% 10.53/10.61 % Total time :10.120000s
%------------------------------------------------------------------------------