%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LDA003-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n013.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 11:43:25 EDT 2024 % Result : Unsatisfiable 4.07s 4.15s % Output : CNFRefutation 4.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : LDA003-1 : TPTP v8.2.0. Released v1.0.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 13:08:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 4.07/4.15 %------------------------------------------- % 4.07/4.15 % File :CSE---1.7 % 4.07/4.15 % Problem :theBenchmark % 4.07/4.15 % Transform :cnf % 4.07/4.15 % Format :tptp:raw % 4.07/4.15 % Command :java -jar mcs_scs.jar %d %s % 4.07/4.15 % 4.07/4.15 % Result :Theorem 3.550000s % 4.07/4.15 % Output :CNFRefutation 3.550000s % 4.07/4.15 %------------------------------------------- % 4.07/4.15 %-------------------------------------------------------------------------- % 4.07/4.15 % File : LDA003-1 : TPTP v8.2.0. Released v1.0.0. % 4.07/4.15 % Domain : LD-Algebras (Left segments) % 4.07/4.15 % Problem : Show that 3 is a left segment of U = 2*2 % 4.07/4.15 % Version : [Jec93] axioms. % 4.07/4.15 % English : % 4.07/4.15 % 4.07/4.15 % Refs : [Jec93] Jech (1993), LD-Algebras % 4.07/4.15 % Source : [Jec93] % 4.07/4.15 % Names : Problem 3 [Jec93] % 4.07/4.15 % 4.07/4.15 % Status : Unsatisfiable % 4.07/4.15 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0 % 4.07/4.15 % Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 5 RR) % 4.07/4.15 % Number of literals : 9 ( 4 equ; 3 neg) % 4.07/4.15 % Maximal clause size : 3 ( 1 avg) % 4.07/4.15 % Maximal term depth : 3 ( 1 avg) % 4.07/4.15 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty) % 4.07/4.15 % Number of functors : 5 ( 5 usr; 4 con; 0-2 aty) % 4.07/4.15 % Number of variables : 8 ( 1 sgn) % 4.07/4.15 % SPC : CNF_UNS_RFO_SEQ_HRN % 4.07/4.15 % 4.07/4.15 % Comments : % 4.07/4.15 %-------------------------------------------------------------------------- % 4.07/4.15 %----A1: x(yz)=xy(xz) % 4.07/4.15 cnf(a1,axiom, % 4.07/4.15 f(X,f(Y,Z)) = f(f(X,Y),f(X,Z)) ). % 4.07/4.15 % 4.07/4.15 %----x is a left segment of xy % 4.07/4.15 cnf(a2,axiom, % 4.07/4.15 left(X,f(X,Y)) ). % 4.07/4.15 % 4.07/4.15 %----transitive % 4.07/4.15 cnf(a3,axiom, % 4.07/4.15 ( ~ left(X,Y) % 4.07/4.15 | ~ left(Y,Z) % 4.07/4.15 | left(X,Z) ) ). % 4.07/4.15 % 4.07/4.15 cnf(clause_4,axiom, % 4.07/4.15 n2 = f(n1,n1) ). % 4.07/4.15 % 4.07/4.15 cnf(clause_5,axiom, % 4.07/4.15 n3 = f(n2,n1) ). % 4.07/4.15 % 4.07/4.15 cnf(clause_6,axiom, % 4.07/4.15 u = f(n2,n2) ). % 4.07/4.15 % 4.07/4.15 %----3 is a left segment of U % 4.07/4.15 cnf(prove_equation,negated_conjecture, % 4.07/4.15 ~ left(n3,u) ). % 4.07/4.15 % 4.07/4.15 %-------------------------------------------------------------------------- % 4.07/4.15 %------------------------------------------- % 4.07/4.15 % Proof found % 4.07/4.15 % SZS status Theorem for theBenchmark % 4.07/4.15 % SZS output start Proof % 4.07/4.16 %ClaNum:14(EqnAxiom:7) % 4.07/4.16 %VarNum:16(SingletonVarNum:8) % 4.07/4.16 %MaxLitNum:3 % 4.07/4.16 %MaxfuncDepth:2 % 4.07/4.16 %SharedTerms:11 % 4.07/4.16 %goalClause: 13 % 4.07/4.16 %singleGoalClaCount:1 % 4.07/4.16 [13]~P1(a4,a5) % 4.07/4.16 [8]E(f2(a1,a1),a3) % 4.07/4.16 [9]E(f2(a3,a1),a4) % 4.07/4.16 [10]E(f2(a3,a3),a5) % 4.07/4.16 [11]P1(x111,f2(x111,x112)) % 4.07/4.16 [12]E(f2(f2(x121,x122),f2(x121,x123)),f2(x121,f2(x122,x123))) % 4.07/4.16 [14]~P1(x141,x143)+P1(x141,x142)+~P1(x143,x142) % 4.07/4.16 %EqnAxiom % 4.07/4.16 [1]E(x11,x11) % 4.07/4.16 [2]E(x22,x21)+~E(x21,x22) % 4.07/4.16 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 4.07/4.16 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 4.07/4.16 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 4.07/4.16 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63) % 4.07/4.16 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71) % 4.07/4.16 % 4.07/4.16 %------------------------------------------- % 4.07/4.16 cnf(15,plain, % 4.07/4.16 (E(f2(x151,f2(x152,x153)),f2(f2(x151,x152),f2(x151,x153)))), % 4.07/4.16 inference(scs_inference,[],[12,2])). % 4.07/4.16 cnf(17,plain, % 4.07/4.16 (P1(x171,f2(x171,x172))), % 4.07/4.16 inference(rename_variables,[],[11])). % 4.07/4.16 cnf(18,plain, % 4.07/4.16 (~P1(x181,x182)+P1(x181,f2(x182,x183))), % 4.07/4.16 inference(scs_inference,[],[13,11,17,12,2,7,14])). % 4.07/4.16 cnf(21,plain, % 4.07/4.16 (~E(a4,a3)), % 4.07/4.16 inference(scs_inference,[],[13,11,17,12,10,2,7,14,3,4])). % 4.07/4.16 cnf(22,plain, % 4.07/4.16 (P1(x221,f2(f2(x221,x222),x223))), % 4.07/4.16 inference(scs_inference,[],[11,18])). % 4.07/4.16 cnf(24,plain, % 4.07/4.16 (E(a3,f2(a1,a1))), % 4.07/4.16 inference(scs_inference,[],[8,11,18,2])). % 4.07/4.16 cnf(25,plain, % 4.07/4.16 (~E(f2(f2(a4,x251),x252),a5)), % 4.12/4.16 inference(scs_inference,[],[13,8,11,18,2,7])). % 4.12/4.16 cnf(28,plain, % 4.12/4.16 (P1(x281,f2(x281,x282))), % 4.12/4.16 inference(rename_variables,[],[11])). % 4.12/4.16 cnf(29,plain, % 4.12/4.16 (P1(a4,f2(f2(f2(a4,x291),x292),x293))), % 4.12/4.16 inference(scs_inference,[],[13,21,8,11,28,18,2,7,3,6,14])). % 4.12/4.16 cnf(35,plain, % 4.12/4.16 (E(a4,f2(a3,a1))), % 4.12/4.16 inference(scs_inference,[],[22,9,18,2])). % 4.12/4.16 cnf(41,plain, % 4.12/4.16 (~E(f2(f2(a4,x411),x412),f2(a3,a3))), % 4.12/4.16 inference(scs_inference,[],[13,22,29,25,9,10,11,18,2,6,14,7,3])). % 4.12/4.16 cnf(240,plain, % 4.12/4.16 (E(f2(x2401,a4),f2(x2401,f2(a3,a1)))), % 4.12/4.16 inference(scs_inference,[],[9,5,2])). % 4.12/4.16 cnf(241,plain, % 4.12/4.16 (E(f2(x2411,f2(a3,a1)),f2(x2411,a4))), % 4.12/4.16 inference(scs_inference,[],[240,2])). % 4.12/4.16 cnf(247,plain, % 4.12/4.16 (E(f2(a3,f2(x2471,a1)),f2(f2(a3,x2471),a4))), % 4.12/4.16 inference(scs_inference,[],[15,241,3])). % 4.12/4.16 cnf(522,plain, % 4.12/4.16 (E(f2(f2(a3,a1),x5221),f2(a4,x5221))), % 4.12/4.16 inference(scs_inference,[],[35,2,4])). % 4.12/4.16 cnf(526,plain, % 4.12/4.16 (~E(f2(a3,a3),f2(a4,f2(x5261,x5262)))), % 4.12/4.16 inference(scs_inference,[],[41,15,2,3])). % 4.12/4.16 cnf(532,plain, % 4.12/4.16 (~E(f2(a3,a3),f2(a4,a4))), % 4.12/4.16 inference(scs_inference,[],[240,526,3])). % 4.12/4.16 cnf(536,plain, % 4.12/4.16 (~E(f2(a3,a3),f2(f2(a3,a1),a4))), % 4.12/4.16 inference(scs_inference,[],[532,522,3])). % 4.12/4.16 cnf(541,plain, % 4.12/4.16 ($false), % 4.12/4.16 inference(scs_inference,[],[24,247,536,3,5]), % 4.12/4.16 ['proof']). % 4.12/4.16 % SZS output end Proof % 4.12/4.16 % Total time :3.550000s %------------------------------------------------------------------------------