%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LAT045-1 : TPTP v8.2.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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 10:18:02 EDT 2024
% Result : Unsatisfiable 62.62s 62.72s
% Output : CNFRefutation 62.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.15 % Problem : LAT045-1 : TPTP v8.2.0. Released v2.5.0.
% 0.09/0.15 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.15/0.38 % Computer : n021.cluster.edu
% 0.15/0.38 % Model : x86_64 x86_64
% 0.15/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.38 % Memory : 8042.1875MB
% 0.15/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.38 % CPULimit : 300
% 0.15/0.38 % WCLimit : 300
% 0.15/0.38 % DateTime : Fri Jun 21 22:54:09 EDT 2024
% 0.15/0.38 % CPUTime :
% 0.25/0.57 start to proof:theBenchmark
% 62.62/62.71 %-------------------------------------------
% 62.62/62.72 % File :CSE---1.7
% 62.62/62.72 % Problem :theBenchmark
% 62.62/62.72 % Transform :cnf
% 62.62/62.72 % Format :tptp:raw
% 62.62/62.72 % Command :java -jar mcs_scs.jar %d %s
% 62.62/62.72
% 62.62/62.72 % Result :Theorem 62.030000s
% 62.62/62.72 % Output :CNFRefutation 62.030000s
% 62.62/62.72 %-------------------------------------------
% 62.62/62.72 %--------------------------------------------------------------------------
% 62.62/62.72 % File : LAT045-1 : TPTP v8.2.0. Released v2.5.0.
% 62.62/62.72 % Domain : Lattice Theory
% 62.62/62.72 % Problem : Lattice orthomodular law from modular lattice
% 62.62/62.72 % Version : [McC88] (equality) axioms.
% 62.62/62.72 % English :
% 62.62/62.72
% 62.62/62.72 % Refs : [McC88] McCune (1988), Challenge Equality Problems in Lattice
% 62.62/62.72 % : [RW01] Rose & Wilkinson (2001), Application of Model Search
% 62.62/62.72 % Source : [RW01]
% 62.62/62.72 % Names : eqp-f.in [RW01]
% 62.62/62.72
% 62.62/62.72 % Status : Unsatisfiable
% 62.62/62.72 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.13 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.11 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.12 v6.0.0, 0.24 v5.5.0, 0.21 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.14 v5.1.0, 0.07 v4.1.0, 0.09 v4.0.1, 0.07 v4.0.0, 0.08 v3.7.0, 0.00 v3.3.0, 0.07 v3.1.0, 0.11 v2.7.0, 0.00 v2.5.0
% 62.62/62.72 % Syntax : Number of clauses : 15 ( 15 unt; 0 nHn; 1 RR)
% 62.62/62.72 % Number of literals : 15 ( 15 equ; 1 neg)
% 62.62/62.72 % Maximal clause size : 1 ( 1 avg)
% 62.62/62.72 % Maximal term depth : 4 ( 2 avg)
% 62.62/62.72 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 62.62/62.72 % Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% 62.62/62.72 % Number of variables : 26 ( 2 sgn)
% 62.62/62.72 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 62.62/62.72
% 62.62/62.72 % Comments :
% 62.62/62.72 %--------------------------------------------------------------------------
% 62.62/62.72 %----Include lattice axioms
% 62.62/62.72 include('Axioms/LAT001-0.ax').
% 62.62/62.72 %--------------------------------------------------------------------------
% 62.62/62.72 %----Compatibility (6)
% 62.62/62.72 cnf(compatibility1,axiom,
% 62.62/62.72 complement(join(X,Y)) = meet(complement(X),complement(Y)) ).
% 62.62/62.72
% 62.62/62.72 cnf(compatibility2,axiom,
% 62.62/62.72 complement(meet(X,Y)) = join(complement(X),complement(Y)) ).
% 62.62/62.72
% 62.62/62.72 %----Invertability (5)
% 62.62/62.72 cnf(invertability1,axiom,
% 62.62/62.72 join(complement(X),X) = n1 ).
% 62.62/62.72
% 62.62/62.72 cnf(invertability2,axiom,
% 62.62/62.72 meet(complement(X),X) = n0 ).
% 62.62/62.72
% 62.62/62.72 cnf(invertability3,axiom,
% 62.62/62.72 complement(complement(X)) = X ).
% 62.62/62.72
% 62.62/62.72 %----Modular law (7)
% 62.62/62.72 cnf(modular_law,axiom,
% 62.62/62.72 join(X,meet(Y,join(X,Z))) = meet(join(X,Y),join(X,Z)) ).
% 62.62/62.72
% 62.62/62.72 %----Denial of orthomodular law (8)
% 62.62/62.72 cnf(prove_orthomodular_law,negated_conjecture,
% 62.62/62.72 join(a,meet(complement(a),join(a,b))) != join(a,b) ).
% 62.62/62.72
% 62.62/62.72 %--------------------------------------------------------------------------
% 62.62/62.72 %-------------------------------------------
% 62.62/62.72 % Proof found
% 62.62/62.72 % SZS status Theorem for theBenchmark
% 62.62/62.72 % SZS output start Proof
% 62.62/62.73 %ClaNum:23(EqnAxiom:8)
% 62.62/62.73 %VarNum:56(SingletonVarNum:26)
% 62.62/62.73 %MaxLitNum:1
% 62.62/62.73 %MaxfuncDepth:3
% 62.62/62.73 %SharedTerms:9
% 62.62/62.73 %goalClause: 23
% 62.62/62.73 %singleGoalClaCount:1
% 62.62/62.73 [23]~E(f5(a2,f4(f1(a2),f5(a2,a3))),f5(a2,a3))
% 62.62/62.73 [10]E(f4(x101,x101),x101)
% 62.62/62.73 [11]E(f5(x111,x111),x111)
% 62.62/62.73 [9]E(f1(f1(x91)),x91)
% 62.62/62.73 [12]E(f4(f1(x121),x121),a6)
% 62.62/62.73 [13]E(f5(f1(x131),x131),a7)
% 62.62/62.73 [14]E(f4(x141,x142),f4(x142,x141))
% 62.62/62.73 [15]E(f5(x151,x152),f5(x152,x151))
% 62.62/62.73 [16]E(f4(x161,f5(x161,x162)),x161)
% 62.62/62.73 [17]E(f5(x171,f4(x171,x172)),x171)
% 62.62/62.73 [18]E(f1(f4(x181,x182)),f5(f1(x181),f1(x182)))
% 62.62/62.73 [19]E(f1(f5(x191,x192)),f4(f1(x191),f1(x192)))
% 62.62/62.73 [20]E(f4(f4(x201,x202),x203),f4(x201,f4(x202,x203)))
% 62.62/62.73 [21]E(f5(f5(x211,x212),x213),f5(x211,f5(x212,x213)))
% 62.62/62.73 [22]E(f4(f5(x221,x222),f5(x221,x223)),f5(x221,f4(x222,f5(x221,x223))))
% 62.62/62.73 %EqnAxiom
% 62.62/62.73 [1]E(x11,x11)
% 62.62/62.73 [2]E(x22,x21)+~E(x21,x22)
% 62.62/62.73 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.62/62.73 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 62.62/62.73 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 62.62/62.73 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 62.62/62.73 [7]~E(x71,x72)+E(f4(x71,x73),f4(x72,x73))
% 62.62/62.73 [8]~E(x81,x82)+E(f4(x83,x81),f4(x83,x82))
% 62.62/62.73
% 62.62/62.73 %-------------------------------------------
% 62.62/62.74 cnf(24,plain,
% 62.62/62.74 (E(x241,f4(x241,x241))),
% 62.62/62.74 inference(scs_inference,[],[10,2])).
% 62.62/62.74 cnf(28,plain,
% 62.62/62.74 (E(x281,f5(x281,x281))),
% 62.62/62.74 inference(scs_inference,[],[11,2])).
% 62.62/62.74 cnf(31,plain,
% 62.62/62.74 (E(x311,f1(f1(x311)))),
% 62.62/62.74 inference(scs_inference,[],[9,2])).
% 62.62/62.74 cnf(34,plain,
% 62.62/62.74 (E(x341,f4(x341,f5(x341,x342)))),
% 62.62/62.74 inference(scs_inference,[],[16,2])).
% 62.62/62.74 cnf(35,plain,
% 62.62/62.74 (E(x351,f1(f1(f4(x351,x351))))),
% 62.62/62.74 inference(scs_inference,[],[24,31,16,2,3])).
% 62.62/62.74 cnf(38,plain,
% 62.62/62.74 (E(x381,f4(f5(x381,x381),f5(f5(x381,x381),x382)))),
% 62.62/62.74 inference(scs_inference,[],[28,34,35,2,3])).
% 62.62/62.74 cnf(53,plain,
% 62.62/62.74 (E(x531,f5(x531,f4(x531,x532)))),
% 62.62/62.74 inference(scs_inference,[],[17,2])).
% 62.62/62.74 cnf(87,plain,
% 62.62/62.74 (E(a7,f5(f1(x871),x871))),
% 62.62/62.74 inference(scs_inference,[],[13,2])).
% 62.62/62.74 cnf(126,plain,
% 62.62/62.74 (E(f4(x1261,x1261),f5(x1261,f4(x1261,x1262)))),
% 62.62/62.74 inference(scs_inference,[],[10,53,3])).
% 62.62/62.74 cnf(132,plain,
% 62.62/62.74 (E(f4(a7,a7),f5(f1(x1321),x1321))),
% 62.62/62.74 inference(scs_inference,[],[10,87,3])).
% 62.62/62.74 cnf(161,plain,
% 62.62/62.74 (E(f4(x1611,f5(x1611,x1612)),f4(x1611,x1611))),
% 62.62/62.74 inference(scs_inference,[],[10,34,3,2])).
% 62.62/62.74 cnf(176,plain,
% 62.62/62.74 (E(f5(x1761,f4(x1761,x1762)),f4(f4(x1761,x1761),f4(x1761,x1761)))),
% 62.62/62.74 inference(scs_inference,[],[10,126,3,2])).
% 62.62/62.74 cnf(218,plain,
% 62.62/62.74 (E(f4(f5(x2181,x2181),f5(f5(x2181,x2181),x2182)),f4(x2181,x2181))),
% 62.62/62.74 inference(scs_inference,[],[10,38,3,2])).
% 62.62/62.74 cnf(300,plain,
% 62.62/62.74 (E(f5(x3001,x3001),f5(x3001,f4(x3001,x3002)))),
% 62.62/62.74 inference(scs_inference,[],[11,53,3])).
% 62.62/62.74 cnf(330,plain,
% 62.62/62.74 (E(f5(x3301,x3301),f4(x3301,f5(x3301,x3302)))),
% 62.62/62.74 inference(scs_inference,[],[11,34,3])).
% 62.62/62.74 cnf(345,plain,
% 62.62/62.74 (E(f5(f5(x3451,x3451),f5(x3451,x3451)),f5(x3451,f4(x3451,x3452)))),
% 62.62/62.74 inference(scs_inference,[],[11,300,3])).
% 62.62/62.74 cnf(353,plain,
% 62.62/62.74 (E(f5(x3531,f4(x3531,x3532)),f5(f5(f5(x3531,x3531),f5(x3531,x3531)),f5(f5(x3531,x3531),f5(x3531,x3531))))),
% 62.62/62.74 inference(scs_inference,[],[11,345,3,2])).
% 62.62/62.74 cnf(354,plain,
% 62.62/62.74 (E(f5(f5(x3541,x3541),f5(x3541,x3541)),f4(x3541,f5(x3541,x3542)))),
% 62.62/62.74 inference(scs_inference,[],[11,330,3])).
% 62.62/62.74 cnf(360,plain,
% 62.62/62.74 (E(f5(f5(f5(x3601,x3601),f5(x3601,x3601)),f5(f5(x3601,x3601),f5(x3601,x3601))),f4(x3601,f5(x3601,x3602)))),
% 62.62/62.74 inference(scs_inference,[],[11,354,3])).
% 62.62/62.74 cnf(455,plain,
% 62.62/62.74 (E(f5(f1(x4551),x4551),f5(f4(a7,a7),f4(a7,a7)))),
% 62.62/62.74 inference(scs_inference,[],[11,132,3,2])).
% 62.62/62.74 cnf(564,plain,
% 62.62/62.74 (E(f5(x5641,f4(x5641,x5642)),f4(x5641,f5(x5641,x5643)))),
% 62.62/62.74 inference(scs_inference,[],[353,360,3])).
% 62.62/62.74 cnf(874,plain,
% 62.62/62.74 (E(f1(f1(f4(x8741,x8742))),f4(x8742,x8741))),
% 62.62/62.74 inference(scs_inference,[],[14,31,3,2])).
% 62.62/62.74 cnf(957,plain,
% 62.62/62.74 (E(f5(x9571,f4(x9572,f5(x9571,x9573))),f4(f5(x9571,x9573),f5(x9571,x9572)))),
% 62.62/62.74 inference(scs_inference,[],[14,22,3,2])).
% 62.62/62.74 cnf(1083,plain,
% 62.62/62.74 (E(f5(f4(a7,a7),f4(a7,a7)),f5(x10831,f1(x10831)))),
% 62.62/62.74 inference(scs_inference,[],[15,455,3,2])).
% 62.62/62.74 cnf(1136,plain,
% 62.62/62.74 (E(f4(f4(x11361,x11361),f4(x11361,x11361)),f5(f4(x11361,x11362),x11361))),
% 62.62/62.74 inference(scs_inference,[],[15,176,3,2])).
% 62.62/62.74 cnf(1161,plain,
% 62.62/62.74 (E(f5(f4(x11611,x11612),x11611),f4(x11611,f5(x11611,x11613)))),
% 62.62/62.74 inference(scs_inference,[],[15,564,3])).
% 62.62/62.74 cnf(1197,plain,
% 62.62/62.74 (E(f5(x11971,f1(x11971)),a7)),
% 62.62/62.74 inference(scs_inference,[],[15,13,3])).
% 62.62/62.74 cnf(1200,plain,
% 62.62/62.74 (E(a7,f5(x12001,f1(x12001)))),
% 62.62/62.74 inference(scs_inference,[],[15,13,3,2])).
% 62.62/62.74 cnf(1293,plain,
% 62.62/62.74 (E(f4(x12931,f5(x12932,f1(x12932))),f4(x12931,a7))),
% 62.62/62.74 inference(scs_inference,[],[1197,5,4,7,8])).
% 62.62/62.74 cnf(1302,plain,
% 62.62/62.74 (E(f4(x13021,a7),f4(x13021,f5(x13022,f1(x13022))))),
% 62.62/62.74 inference(scs_inference,[],[1200,4,5,6,7,8])).
% 62.62/62.74 cnf(1383,plain,
% 62.62/62.74 (~E(f4(f5(a2,a3),f5(a2,f1(a2))),f5(a2,a3))),
% 62.62/62.74 inference(scs_inference,[],[23,1136,957,5,4,6,7,8,3])).
% 62.62/62.74 cnf(1481,plain,
% 62.62/62.74 (~E(f5(a2,a3),f4(f5(a2,a3),a7))),
% 62.62/62.74 inference(scs_inference,[],[1083,1383,1293,5,6,4,7,8,3,2])).
% 62.62/62.74 cnf(1510,plain,
% 62.62/62.74 (~E(f1(f1(f4(f5(a2,a3),f5(a2,a3)))),f4(f5(a2,a3),a7))),
% 62.62/62.74 inference(scs_inference,[],[1481,1161,35,5,4,7,6,8,3])).
% 62.62/62.74 cnf(1742,plain,
% 62.62/62.74 (~E(f4(f5(a2,a3),a7),f4(f5(a2,a3),f5(a2,a3)))),
% 62.62/62.74 inference(scs_inference,[],[218,874,1510,8,7,4,6,5,3,2])).
% 62.62/62.74 cnf(1840,plain,
% 62.62/62.74 ($false),
% 62.62/62.74 inference(scs_inference,[],[12,1742,1302,161,4,5,6,8,7,3]),
% 62.62/62.74 ['proof']).
% 62.62/62.74 % SZS output end Proof
% 62.62/62.74 % Total time :62.030000s
%------------------------------------------------------------------------------