%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT090-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.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:06 EDT 2024 % Result : Unsatisfiable 118.76s 118.80s % Output : CNFRefutation 118.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : LAT090-1 : TPTP v8.2.0. Released v2.6.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n025.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sat Jun 22 00:26:09 EDT 2024 % 0.12/0.32 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 118.69/118.75 %------------------------------------------- % 118.69/118.75 % File :CSE---1.7 % 118.69/118.75 % Problem :theBenchmark % 118.69/118.75 % Transform :cnf % 118.69/118.75 % Format :tptp:raw % 118.69/118.75 % Command :java -jar mcs_scs.jar %d %s % 118.69/118.75 % 118.69/118.76 % Result :Theorem 118.160000s % 118.69/118.76 % Output :CNFRefutation 118.160000s % 118.69/118.76 %------------------------------------------- % 118.76/118.80 %-------------------------------------------------------------------------- % 118.76/118.80 % File : LAT090-1 : TPTP v8.2.0. Released v2.6.0. % 118.76/118.80 % Domain : Lattice Theory (Weakly Associative Lattices) % 118.76/118.80 % Problem : Absorption basis for WAL, part 3 % 118.76/118.80 % Version : [MP96] (equality) axioms : Especial. % 118.76/118.80 % English : % 118.76/118.80 % 118.76/118.80 % Refs : [McC98] McCune (1998), Email to G. Sutcliffe % 118.76/118.80 % : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq % 118.76/118.80 % Source : [TPTP] % 118.76/118.80 % Names : % 118.76/118.80 % 118.76/118.80 % Status : Unsatisfiable % 118.76/118.80 % 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.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.05 v5.4.0, 0.00 v2.6.0 % 118.76/118.80 % Syntax : Number of clauses : 6 ( 6 unt; 0 nHn; 1 RR) % 118.76/118.80 % Number of literals : 6 ( 6 equ; 1 neg) % 118.76/118.80 % Maximal clause size : 1 ( 1 avg) % 118.76/118.80 % Maximal term depth : 4 ( 2 avg) % 118.76/118.80 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 118.76/118.80 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 118.76/118.80 % Number of variables : 12 ( 5 sgn) % 118.76/118.80 % SPC : CNF_UNS_RFO_PEQ_UEQ % 118.76/118.80 % 118.76/118.80 % Comments : A UEQ part of LAT029-1 % 118.76/118.80 %-------------------------------------------------------------------------- % 118.76/118.80 cnf(wal_absorbtion_1,axiom, % 118.76/118.80 join(meet(A,B),meet(A,join(A,B))) = A ). % 118.76/118.80 % 118.76/118.80 cnf(wal_absorbtion_2,axiom, % 118.76/118.80 join(meet(A,A),meet(B,join(A,A))) = A ). % 118.76/118.80 % 118.76/118.80 cnf(wal_absorbtion_3,axiom, % 118.76/118.80 join(meet(A,B),meet(B,join(A,B))) = B ). % 118.76/118.80 % 118.76/118.80 cnf(wal_absorbtion_4,axiom, % 118.76/118.80 meet(meet(join(A,B),join(C,A)),A) = A ). % 118.76/118.80 % 118.76/118.80 cnf(wal_absorbtion_5,axiom, % 118.76/118.80 join(join(meet(A,B),meet(C,A)),A) = A ). % 118.76/118.80 % 118.76/118.80 cnf(prove_normal_axioms_3,negated_conjecture, % 118.76/118.80 join(a,a) != a ). % 118.76/118.80 % 118.76/118.80 %-------------------------------------------------------------------------- % 118.76/118.80 %------------------------------------------- % 118.76/118.80 % Proof found % 118.76/118.80 % SZS status Theorem for theBenchmark % 118.76/118.80 % SZS output start Proof % 118.82/118.84 %ClaNum:13(EqnAxiom:7) % 118.82/118.84 %VarNum:30(SingletonVarNum:12) % 118.82/118.84 %MaxLitNum:1 % 118.82/118.84 %MaxfuncDepth:3 % 118.82/118.84 %SharedTerms:3 % 118.82/118.84 %goalClause: 13 % 118.82/118.84 %singleGoalClaCount:1 % 118.82/118.84 [13]~E(f2(a3,a3),a3) % 118.82/118.84 [8]E(f2(f1(x81,x82),f1(x82,f2(x81,x82))),x82) % 118.82/118.84 [9]E(f2(f1(x91,x92),f1(x91,f2(x91,x92))),x91) % 118.82/118.84 [10]E(f2(f1(x101,x101),f1(x102,f2(x101,x101))),x101) % 118.82/118.84 [11]E(f1(f1(f2(x111,x112),f2(x113,x111)),x111),x111) % 118.82/118.84 [12]E(f2(f2(f1(x121,x122),f1(x123,x121)),x121),x121) % 118.82/118.84 %EqnAxiom % 118.82/118.84 [1]E(x11,x11) % 118.82/118.84 [2]E(x22,x21)+~E(x21,x22) % 118.82/118.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 118.82/118.84 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 118.82/118.84 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 118.82/118.84 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 118.82/118.84 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 118.82/118.84 % 118.82/118.84 %------------------------------------------- % 118.82/118.89 cnf(14,plain, % 118.82/118.89 (E(x141,f2(f1(x142,x141),f1(x141,f2(x142,x141))))), % 118.82/118.89 inference(scs_inference,[],[8,2])). % 118.82/118.89 cnf(29,plain, % 118.82/118.89 (~E(a3,f2(f1(a3,x291),f1(x292,a3)))), % 118.82/118.89 inference(scs_inference,[],[13,12,2,3,6])). % 118.82/118.89 cnf(34,plain, % 118.82/118.89 (~E(f2(f1(a3,x341),f1(x342,a3)),a3)), % 118.82/118.89 inference(scs_inference,[],[8,29,4,5,7,6,2])). % 118.82/118.89 cnf(92,plain, % 118.82/118.89 (~E(a3,f2(a3,x921))), % 118.82/118.89 inference(scs_inference,[],[34,9,3,7,5])). % 118.82/118.89 cnf(352,plain, % 118.82/118.89 ($false), % 118.82/118.89 inference(scs_inference,[],[14,11,92,3,2,6]), % 118.82/118.89 ['proof']). % 118.82/118.89 % SZS output end Proof % 118.82/118.89 % Total time :118.160000s %------------------------------------------------------------------------------