%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : BOO011-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n008.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 04:35:46 EDT 2024
% Result : Unsatisfiable 0.62s 0.68s
% Output : CNFRefutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : BOO011-1 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.36 % Computer : n008.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Tue Jun 18 19:12:54 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.48/0.64 start to proof:theBenchmark
% 0.62/0.67 %-------------------------------------------
% 0.62/0.67 % File :CSE---1.7
% 0.62/0.67 % Problem :theBenchmark
% 0.62/0.67 % Transform :cnf
% 0.62/0.67 % Format :tptp:raw
% 0.62/0.67 % Command :java -jar mcs_scs.jar %d %s
% 0.62/0.67
% 0.62/0.67 % Result :Theorem 0.000000s
% 0.62/0.67 % Output :CNFRefutation 0.000000s
% 0.62/0.67 %-------------------------------------------
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 % File : BOO011-1 : TPTP v8.2.0. Released v1.0.0.
% 0.62/0.68 % Domain : Boolean Algebra
% 0.62/0.68 % Problem : Inverse of additive identity = Multiplicative identity
% 0.62/0.68 % Version : [MOW76] axioms.
% 0.62/0.68 % English : The inverse of the additive identity is the multiplicative
% 0.62/0.68 % identity.
% 0.62/0.68
% 0.62/0.68 % Refs : [Whi61] Whitesitt (1961), Boolean Algebra and Its Applications
% 0.62/0.68 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 0.62/0.68 % Source : [MOW76]
% 0.62/0.68 % Names : B7 [MOW76]
% 0.62/0.68 % : prob7.ver1 [ANL]
% 0.62/0.68
% 0.62/0.68 % Status : Unsatisfiable
% 0.62/0.68 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v2.0.0
% 0.62/0.68 % Syntax : Number of clauses : 23 ( 11 unt; 0 nHn; 13 RR)
% 0.62/0.68 % Number of literals : 61 ( 3 equ; 39 neg)
% 0.62/0.68 % Maximal clause size : 5 ( 2 avg)
% 0.62/0.68 % Maximal term depth : 2 ( 1 avg)
% 0.62/0.68 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 0.62/0.68 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 0.62/0.68 % Number of variables : 82 ( 0 sgn)
% 0.62/0.68 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.62/0.68
% 0.62/0.68 % Comments :
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 %----Include Boolean algebra axioms
% 0.62/0.68 include('Axioms/BOO002-0.ax').
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 cnf(prove_equation,negated_conjecture,
% 0.62/0.68 inverse(additive_identity) != multiplicative_identity ).
% 0.62/0.68
% 0.62/0.68 %--------------------------------------------------------------------------
% 0.62/0.68 %-------------------------------------------
% 0.62/0.68 % Proof found
% 0.62/0.68 % SZS status Theorem for theBenchmark
% 0.62/0.68 % SZS output start Proof
% 0.62/0.68 %ClaNum:37(EqnAxiom:14)
% 0.62/0.68 %VarNum:172(SingletonVarNum:82)
% 0.62/0.68 %MaxLitNum:5
% 0.62/0.68 %MaxfuncDepth:1
% 0.62/0.68 %SharedTerms:4
% 0.62/0.68 %goalClause: 25
% 0.62/0.68 %singleGoalClaCount:1
% 0.62/0.68 [25]~E(f4(a1),a3)
% 0.62/0.68 [15]P1(x151,a1,x151)
% 0.62/0.68 [16]P2(x161,a3,x161)
% 0.62/0.68 [17]P1(a1,x171,x171)
% 0.62/0.68 [18]P2(a3,x181,x181)
% 0.62/0.68 [19]P1(x191,f4(x191),a3)
% 0.62/0.68 [20]P2(x201,f4(x201),a1)
% 0.62/0.68 [21]P1(f4(x211),x211,a3)
% 0.62/0.68 [22]P2(f4(x221),x221,a1)
% 0.62/0.68 [23]P1(x231,x232,f2(x231,x232))
% 0.62/0.68 [24]P2(x241,x242,f5(x241,x242))
% 0.62/0.68 [26]~P1(x262,x261,x263)+P1(x261,x262,x263)
% 0.62/0.68 [27]~P2(x272,x271,x273)+P2(x271,x272,x273)
% 0.62/0.68 [28]~P1(x283,x284,x281)+E(x281,x282)+~P1(x283,x284,x282)
% 0.62/0.68 [29]~P2(x293,x294,x291)+E(x291,x292)+~P2(x293,x294,x292)
% 0.62/0.68 [30]~P2(x307,x305,x303)+~P2(x306,x304,x301)+P1(x301,x302,x303)+~P1(x304,x302,x305)+~P1(x306,x302,x307)
% 0.62/0.68 [31]~P2(x317,x315,x312)+~P2(x317,x314,x311)+P1(x311,x312,x313)+~P1(x314,x315,x316)+~P2(x317,x316,x313)
% 0.62/0.68 [32]~P2(x325,x327,x322)+~P2(x324,x327,x321)+P1(x321,x322,x323)+~P1(x324,x325,x326)+~P2(x326,x327,x323)
% 0.62/0.68 [33]~P2(x337,x335,x333)+~P2(x336,x334,x332)+P1(x331,x332,x333)+~P1(x331,x334,x335)+~P1(x331,x336,x337)
% 0.62/0.68 [34]~P2(x347,x342,x345)+~P2(x346,x342,x344)+P2(x341,x342,x343)+~P1(x344,x345,x343)+~P1(x346,x347,x341)
% 0.62/0.68 [35]~P2(x357,x356,x354)+P2(x351,x352,x353)+~P1(x354,x355,x353)+~P1(x356,x355,x352)+~P1(x357,x355,x351)
% 0.62/0.68 [36]~P2(x367,x366,x365)+P2(x361,x362,x363)+~P1(x364,x365,x363)+~P1(x364,x366,x362)+~P1(x364,x367,x361)
% 0.62/0.68 [37]~P2(x371,x377,x375)+~P2(x371,x376,x374)+P2(x371,x372,x373)+~P1(x374,x375,x373)+~P1(x376,x377,x372)
% 0.62/0.68 %EqnAxiom
% 0.62/0.68 [1]E(x11,x11)
% 0.62/0.68 [2]E(x22,x21)+~E(x21,x22)
% 0.62/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.62/0.68 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 0.62/0.68 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 0.62/0.68 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 0.62/0.68 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73))
% 0.62/0.68 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82))
% 0.62/0.68 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 0.62/0.68 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 0.62/0.68 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 0.62/0.68 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 0.62/0.68 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 0.62/0.68 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 0.62/0.68
% 0.62/0.68 %-------------------------------------------
% 0.62/0.68 cnf(38,plain,
% 0.62/0.68 ($false),
% 0.62/0.68 inference(scs_inference,[],[15,25,21,28]),
% 0.62/0.68 ['proof']).
% 0.62/0.68 % SZS output end Proof
% 0.62/0.68 % Total time :0.000000s
%------------------------------------------------------------------------------