%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LAT039-1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:01 EDT 2024
% Result : Unsatisfiable 0.64s 0.90s
% Output : CNFRefutation 0.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT039-1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sat Jun 22 00:25:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.60/0.66 start to proof:theBenchmark
% 0.64/0.90 %-------------------------------------------
% 0.64/0.90 % File :CSE---1.7
% 0.64/0.90 % Problem :theBenchmark
% 0.64/0.90 % Transform :cnf
% 0.64/0.90 % Format :tptp:raw
% 0.64/0.90 % Command :java -jar mcs_scs.jar %d %s
% 0.64/0.90
% 0.64/0.90 % Result :Theorem 0.200000s
% 0.64/0.90 % Output :CNFRefutation 0.200000s
% 0.64/0.90 %-------------------------------------------
% 0.64/0.90 %--------------------------------------------------------------------------
% 0.64/0.90 % File : LAT039-1 : TPTP v8.2.0. Released v2.4.0.
% 0.64/0.90 % Domain : Lattice Theory
% 0.64/0.90 % Problem : Every distributive lattice is modular
% 0.64/0.90 % Version : [McC88] (equality) axioms.
% 0.64/0.90 % Theorem formulation : Modularity is expressed by:
% 0.64/0.90 % x <= y -> x v (y & z) = y & (x v z)
% 0.64/0.90 % English :
% 0.64/0.90
% 0.64/0.90 % Refs : [DeN00] DeNivelle (2000), Email to G. Sutcliffe
% 0.64/0.90 % [McC88] McCune (1988), Challenge Equality Problems in Lattice
% 0.64/0.90 % Source : [DeN00]
% 0.64/0.90 % Names : lattice-mod-2 [DeN00]
% 0.64/0.90
% 0.64/0.90 % Status : Unsatisfiable
% 0.64/0.90 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.05 v7.5.0, 0.04 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v2.4.0
% 0.64/0.90 % Syntax : Number of clauses : 12 ( 12 unt; 0 nHn; 2 RR)
% 0.64/0.90 % Number of literals : 12 ( 12 equ; 1 neg)
% 0.64/0.90 % Maximal clause size : 1 ( 1 avg)
% 0.64/0.90 % Maximal term depth : 3 ( 2 avg)
% 0.64/0.90 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 0.64/0.90 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 0.64/0.90 % Number of variables : 22 ( 2 sgn)
% 0.64/0.90 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 0.64/0.90
% 0.64/0.90 % Comments :
% 0.64/0.90 %--------------------------------------------------------------------------
% 0.64/0.90 %----Include lattice theory axioms
% 0.64/0.90 include('Axioms/LAT001-0.ax').
% 0.64/0.90 %--------------------------------------------------------------------------
% 0.64/0.90 cnf(dist_join,hypothesis,
% 0.64/0.90 join(X,meet(Y,Z)) = meet(join(X,Y),join(X,Z)) ).
% 0.64/0.90
% 0.64/0.90 cnf(dist_meet,hypothesis,
% 0.64/0.90 meet(X,join(Y,Z)) = join(meet(X,Y),meet(X,Z)) ).
% 0.64/0.90
% 0.64/0.90 cnf(lhs,hypothesis,
% 0.64/0.90 join(xx,yy) = yy ).
% 0.64/0.90
% 0.64/0.90 cnf(rhs,negated_conjecture,
% 0.64/0.90 join(xx,meet(yy,zz)) != meet(yy,join(xx,zz)) ).
% 0.64/0.90
% 0.64/0.90 %--------------------------------------------------------------------------
% 0.64/0.90 %-------------------------------------------
% 0.64/0.90 % Proof found
% 0.64/0.90 % SZS status Theorem for theBenchmark
% 0.64/0.90 % SZS output start Proof
% 0.64/0.91 %ClaNum:19(EqnAxiom:7)
% 0.64/0.91 %VarNum:48(SingletonVarNum:22)
% 0.64/0.91 %MaxLitNum:1
% 0.64/0.91 %MaxfuncDepth:2
% 0.64/0.91 %SharedTerms:9
% 0.64/0.91 %goalClause: 19
% 0.64/0.91 %singleGoalClaCount:1
% 0.64/0.91 [8]E(f2(a1,a4),a4)
% 0.64/0.91 [19]~E(f3(a4,f2(a1,a5)),f2(a1,f3(a4,a5)))
% 0.64/0.91 [9]E(f3(x91,x91),x91)
% 0.64/0.91 [10]E(f2(x101,x101),x101)
% 0.64/0.91 [11]E(f3(x111,x112),f3(x112,x111))
% 0.64/0.91 [12]E(f2(x121,x122),f2(x122,x121))
% 0.64/0.91 [13]E(f3(x131,f2(x131,x132)),x131)
% 0.64/0.91 [14]E(f2(x141,f3(x141,x142)),x141)
% 0.64/0.91 [15]E(f3(f3(x151,x152),x153),f3(x151,f3(x152,x153)))
% 0.64/0.91 [16]E(f2(f2(x161,x162),x163),f2(x161,f2(x162,x163)))
% 0.64/0.91 [17]E(f2(f3(x171,x172),f3(x171,x173)),f3(x171,f2(x172,x173)))
% 0.64/0.91 [18]E(f3(f2(x181,x182),f2(x181,x183)),f2(x181,f3(x182,x183)))
% 0.64/0.91 %EqnAxiom
% 0.64/0.91 [1]E(x11,x11)
% 0.64/0.91 [2]E(x22,x21)+~E(x21,x22)
% 0.64/0.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.64/0.91 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 0.64/0.91 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 0.64/0.91 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 0.64/0.91 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 0.64/0.91
% 0.64/0.91 %-------------------------------------------
% 0.64/0.91 cnf(20,plain,
% 0.64/0.91 (E(x201,f3(x201,x201))),
% 0.64/0.91 inference(scs_inference,[],[9,2])).
% 0.64/0.91 cnf(23,plain,
% 0.64/0.91 (E(x231,f2(x231,x231))),
% 0.64/0.91 inference(scs_inference,[],[10,2])).
% 0.64/0.91 cnf(24,plain,
% 0.64/0.91 (E(f2(x241,x241),f3(x241,x241))),
% 0.64/0.91 inference(scs_inference,[],[20,10,2,3])).
% 0.64/0.91 cnf(26,plain,
% 0.64/0.91 (E(f3(x261,x261),f2(x261,x261))),
% 0.64/0.91 inference(scs_inference,[],[24,2])).
% 0.64/0.91 cnf(27,plain,
% 0.64/0.91 (E(x271,f2(f3(x271,x271),f3(x271,x271)))),
% 0.64/0.91 inference(scs_inference,[],[23,20,24,2,3])).
% 0.64/0.91 cnf(29,plain,
% 0.64/0.91 (E(f2(f3(x291,x291),f3(x291,x291)),x291)),
% 0.64/0.91 inference(scs_inference,[],[27,2])).
% 0.64/0.91 cnf(30,plain,
% 0.64/0.91 (E(f3(x301,x301),f2(f2(x301,x301),f2(x301,x301)))),
% 0.64/0.91 inference(scs_inference,[],[26,23,27,2,3])).
% 0.64/0.91 cnf(32,plain,
% 0.64/0.92 (E(f2(f2(x321,x321),f2(x321,x321)),f3(x321,x321))),
% 0.64/0.92 inference(scs_inference,[],[30,2])).
% 0.64/0.92 cnf(33,plain,
% 0.64/0.92 (E(f2(f3(x331,x331),f3(x331,x331)),f2(x331,x331))),
% 0.64/0.92 inference(scs_inference,[],[29,23,30,2,3])).
% 0.64/0.92 cnf(35,plain,
% 0.64/0.92 (E(f2(x351,x351),f2(f3(x351,x351),f3(x351,x351)))),
% 0.64/0.92 inference(scs_inference,[],[33,2])).
% 0.64/0.92 cnf(36,plain,
% 0.64/0.92 (E(f3(f2(x361,x361),f2(x361,x361)),f3(x361,x361))),
% 0.64/0.92 inference(scs_inference,[],[32,26,33,2,3])).
% 0.64/0.92 cnf(38,plain,
% 0.64/0.92 (E(f3(x381,x381),f3(f2(x381,x381),f2(x381,x381)))),
% 0.64/0.92 inference(scs_inference,[],[36,2])).
% 0.64/0.92 cnf(39,plain,
% 0.64/0.92 (E(f2(x391,x391),f3(f3(x391,x391),f3(x391,x391)))),
% 0.64/0.92 inference(scs_inference,[],[35,36,24,2,3])).
% 0.64/0.92 cnf(41,plain,
% 0.64/0.92 (E(f3(f3(x411,x411),f3(x411,x411)),f2(x411,x411))),
% 0.64/0.92 inference(scs_inference,[],[39,2])).
% 0.64/0.92 cnf(42,plain,
% 0.64/0.92 (E(f2(x421,x421),f3(x421,f2(x421,x421)))),
% 0.64/0.92 inference(scs_inference,[],[35,39,17,2,3])).
% 0.64/0.92 cnf(44,plain,
% 0.64/0.92 (E(f3(x441,f2(x441,x441)),f2(x441,x441))),
% 0.64/0.92 inference(scs_inference,[],[42,2])).
% 0.64/0.92 cnf(45,plain,
% 0.64/0.92 (E(f3(f3(x451,x451),f3(x451,x451)),f3(f2(x451,x451),f2(x451,x451)))),
% 0.64/0.92 inference(scs_inference,[],[41,20,42,2,3])).
% 0.64/0.92 cnf(47,plain,
% 0.64/0.92 (E(f3(f2(x471,x471),f2(x471,x471)),f3(f3(x471,x471),f3(x471,x471)))),
% 0.64/0.92 inference(scs_inference,[],[45,2])).
% 0.64/0.92 cnf(48,plain,
% 0.64/0.92 (E(f3(f2(x481,x481),f2(f2(x481,x481),f2(x481,x481))),f3(x481,x481))),
% 0.64/0.92 inference(scs_inference,[],[44,32,45,2,3])).
% 0.64/0.92 cnf(50,plain,
% 0.64/0.92 (E(f3(x501,x501),f3(f2(x501,x501),f2(f2(x501,x501),f2(x501,x501))))),
% 0.64/0.92 inference(scs_inference,[],[48,2])).
% 0.64/0.92 cnf(51,plain,
% 0.64/0.92 (E(f3(f2(x511,x511),f2(x511,x511)),f2(f3(x511,x511),f3(x511,x511)))),
% 0.64/0.92 inference(scs_inference,[],[47,26,48,2,3])).
% 0.64/0.92 cnf(53,plain,
% 0.64/0.92 (E(f2(f3(x531,x531),f3(x531,x531)),f3(f2(x531,x531),f2(x531,x531)))),
% 0.64/0.92 inference(scs_inference,[],[51,2])).
% 0.64/0.92 cnf(54,plain,
% 0.64/0.92 (E(f3(f3(x541,x541),f3(x541,x541)),f3(x541,f2(x541,x541)))),
% 0.64/0.92 inference(scs_inference,[],[41,51,42,2,3])).
% 0.64/0.92 cnf(56,plain,
% 0.64/0.92 (E(f3(x561,f2(x561,x561)),f3(f3(x561,x561),f3(x561,x561)))),
% 0.64/0.92 inference(scs_inference,[],[54,2])).
% 0.64/0.92 cnf(59,plain,
% 0.64/0.92 (E(f2(x591,f3(x592,x593)),f3(f2(x591,x592),f2(x591,x593)))),
% 0.64/0.92 inference(scs_inference,[],[18,2])).
% 0.64/0.92 cnf(60,plain,
% 0.64/0.92 (E(f2(f3(x601,x601),f3(x601,x601)),f2(f2(x601,x601),f2(x601,x601)))),
% 0.64/0.92 inference(scs_inference,[],[53,26,18,2,3])).
% 0.64/0.92 cnf(62,plain,
% 0.64/0.92 (E(f2(f2(x621,x621),f2(x621,x621)),f2(f3(x621,x621),f3(x621,x621)))),
% 0.64/0.92 inference(scs_inference,[],[60,2])).
% 0.64/0.92 cnf(63,plain,
% 0.64/0.92 (E(f3(x631,f2(x631,x631)),f3(f2(x631,x631),f2(x631,x631)))),
% 0.64/0.92 inference(scs_inference,[],[56,60,45,2,3])).
% 0.64/0.92 cnf(65,plain,
% 0.64/0.92 (E(f3(f2(x651,x651),f2(x651,x651)),f3(x651,f2(x651,x651)))),
% 0.64/0.92 inference(scs_inference,[],[63,2])).
% 0.64/0.92 cnf(66,plain,
% 0.64/0.92 (E(f2(f2(x661,x661),f2(x661,x661)),f3(f3(x661,x661),f3(x661,x661)))),
% 0.64/0.92 inference(scs_inference,[],[62,63,24,2,3])).
% 0.64/0.92 cnf(69,plain,
% 0.64/0.92 (E(f3(x691,x691),f3(x691,f2(x691,x691)))),
% 0.64/0.92 inference(scs_inference,[],[65,38,66,2,3])).
% 0.64/0.92 cnf(71,plain,
% 0.64/0.92 (E(f3(x711,f2(x711,x711)),f3(x711,x711))),
% 0.64/0.92 inference(scs_inference,[],[69,2])).
% 0.64/0.92 cnf(72,plain,
% 0.64/0.92 (E(f2(x721,f3(x721,x721)),f3(f3(x721,x721),f3(x721,x721)))),
% 0.64/0.92 inference(scs_inference,[],[59,47,69,2,3])).
% 0.64/0.92 cnf(75,plain,
% 0.64/0.92 (E(f3(f3(x751,x751),f3(x751,x751)),f2(x751,f3(x751,x751)))),
% 0.64/0.92 inference(scs_inference,[],[72,2])).
% 0.64/0.92 cnf(76,plain,
% 0.64/0.92 (E(f3(f3(x761,x761),f2(f3(x761,x761),f3(x761,x761))),f2(x761,x761))),
% 0.64/0.92 inference(scs_inference,[],[71,41,72,2,3])).
% 0.64/0.92 cnf(78,plain,
% 0.64/0.92 (E(f2(x781,x781),f3(f3(x781,x781),f2(f3(x781,x781),f3(x781,x781))))),
% 0.64/0.92 inference(scs_inference,[],[76,2])).
% 0.64/0.92 cnf(79,plain,
% 0.64/0.92 (E(f3(x791,f2(x791,x791)),f2(f2(x791,x791),f2(x791,x791)))),
% 0.64/0.92 inference(scs_inference,[],[71,76,30,2,3])).
% 0.64/0.92 cnf(81,plain,
% 0.64/0.92 (E(f2(f2(x811,x811),f2(x811,x811)),f3(x811,f2(x811,x811)))),
% 0.64/0.92 inference(scs_inference,[],[79,2])).
% 0.64/0.92 cnf(82,plain,
% 0.64/0.92 (E(f3(x821,f2(x821,x821)),f2(x821,f3(x821,x821)))),
% 0.64/0.92 inference(scs_inference,[],[75,56,79,2,3])).
% 0.64/0.92 cnf(84,plain,
% 0.64/0.92 (E(f2(x841,f3(x841,x841)),f3(x841,f2(x841,x841)))),
% 0.64/0.92 inference(scs_inference,[],[82,2])).
% 0.64/0.92 cnf(85,plain,
% 0.64/0.92 (E(f2(f2(x851,x851),f2(x851,x851)),f2(x851,f3(x851,x851)))),
% 0.64/0.92 inference(scs_inference,[],[81,82,2,3])).
% 0.64/0.92 cnf(88,plain,
% 0.64/0.92 (E(f2(x881,f3(x881,x881)),f2(x881,x881))),
% 0.64/0.92 inference(scs_inference,[],[84,44,85,2,3])).
% 0.64/0.92 cnf(91,plain,
% 0.64/0.92 (E(f3(x911,x911),f2(f2(x911,x911),f3(f2(x911,x911),f2(x911,x911))))),
% 0.64/0.92 inference(scs_inference,[],[50,88,82,2,3])).
% 0.64/0.92 cnf(94,plain,
% 0.64/0.92 (E(f2(x941,x941),f2(f3(x941,x941),f3(f3(x941,x941),f3(x941,x941))))),
% 0.64/0.92 inference(scs_inference,[],[78,91,82,2,3])).
% 0.64/0.92 cnf(99,plain,
% 0.64/0.92 (~E(a4,f2(a1,a4))),
% 0.64/0.92 inference(scs_inference,[],[19,94,18,2,3,6])).
% 0.64/0.92 cnf(112,plain,
% 0.64/0.92 ($false),
% 0.64/0.92 inference(scs_inference,[],[99,8,2]),
% 0.64/0.92 ['proof']).
% 0.64/0.92 % SZS output end Proof
% 0.64/0.92 % Total time :0.200000s
%------------------------------------------------------------------------------