%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN015-2 : 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 : 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 19:04:15 EDT 2024 % Result : Unsatisfiable 2.77s 2.87s % Output : CNFRefutation 2.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN015-2 : TPTP v8.2.0. Released v1.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n023.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 23:05:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.55 start to proof:theBenchmark % 2.77/2.86 %------------------------------------------- % 2.77/2.86 % File :CSE---1.7 % 2.77/2.86 % Problem :theBenchmark % 2.77/2.86 % Transform :cnf % 2.77/2.86 % Format :tptp:raw % 2.77/2.86 % Command :java -jar mcs_scs.jar %d %s % 2.77/2.86 % 2.77/2.86 % Result :Theorem 2.260000s % 2.77/2.86 % Output :CNFRefutation 2.260000s % 2.77/2.86 %------------------------------------------- % 2.77/2.86 %-------------------------------------------------------------------------- % 2.77/2.86 % File : SYN015-2 : TPTP v8.2.0. Released v1.0.0. % 2.77/2.86 % Domain : Syntactic % 2.77/2.86 % Problem : A problem in quantification theory % 2.77/2.86 % Version : [Wan65] axioms : Reduced & Augmented > Especial. % 2.77/2.86 % Theorem formulation : Modified. % 2.77/2.86 % English : % 2.77/2.86 % 2.77/2.86 % Refs : [Wos65] Wos (1965), Unpublished Note % 2.77/2.86 % : [Wan65] Wang (1965), Formalization and Automatic Theorem-Provi % 2.77/2.86 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 2.77/2.86 % Source : [SPRFN] % 2.77/2.86 % Names : Problem 33 [Wos65] % 2.77/2.86 % : wos33 [WM76] % 2.77/2.86 % 2.77/2.86 % Status : Unsatisfiable % 2.77/2.86 % Rating : 0.00 v7.4.0, 0.17 v7.0.0, 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.20 v5.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.12 v4.0.1, 0.00 v4.0.0, 0.14 v3.4.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.20 v2.4.0, 0.00 v2.2.1, 0.25 v2.1.0, 0.00 v2.0.0 % 2.77/2.86 % Syntax : Number of clauses : 26 ( 7 unt; 13 nHn; 23 RR) % 2.77/2.86 % Number of literals : 70 ( 0 equ; 30 neg) % 2.77/2.86 % Maximal clause size : 6 ( 2 avg) % 2.77/2.86 % Maximal term depth : 2 ( 1 avg) % 2.77/2.86 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty) % 2.77/2.86 % Number of functors : 6 ( 6 usr; 4 con; 0-1 aty) % 2.77/2.86 % Number of variables : 29 ( 0 sgn) % 2.77/2.86 % SPC : CNF_UNS_RFO_NEQ_NHN % 2.77/2.86 % 2.77/2.86 % Comments : % 2.77/2.86 %-------------------------------------------------------------------------- % 2.77/2.86 cnf(reflexivityish,axiom, % 2.77/2.86 equalish(X,X) ). % 2.77/2.86 % 2.77/2.86 cnf(symmetryish,axiom, % 2.77/2.86 ( ~ equalish(X,Y) % 2.77/2.86 | equalish(Y,X) ) ). % 2.77/2.87 % 2.77/2.87 cnf(transitivityish,axiom, % 2.77/2.87 ( ~ equalish(X,Y) % 2.77/2.87 | ~ equalish(Y,Z) % 2.77/2.87 | equalish(X,Z) ) ). % 2.77/2.87 % 2.77/2.87 cnf(element_substitutionish1,axiom, % 2.77/2.87 ( ~ equalish(A,B) % 2.77/2.87 | ~ element(C,A) % 2.77/2.87 | element(C,B) ) ). % 2.77/2.87 % 2.77/2.87 cnf(element_substitutionish2,axiom, % 2.77/2.87 ( ~ element(A,B) % 2.77/2.87 | ~ equalish(A,C) % 2.77/2.87 | element(C,B) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_3,negated_conjecture, % 2.77/2.87 ( ~ element(A,a) % 2.77/2.87 | equalish(A,k) % 2.77/2.87 | equalish(A,a) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_4,negated_conjecture, % 2.77/2.87 ( ~ equalish(A,k) % 2.77/2.87 | element(A,a) % 2.77/2.87 | equalish(A,a) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_5,negated_conjecture, % 2.77/2.87 ( ~ equalish(f(A),m) % 2.77/2.87 | ~ element(A,m) % 2.77/2.87 | equalish(A,m) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_6,negated_conjecture, % 2.77/2.87 ( ~ equalish(f(A),A) % 2.77/2.87 | ~ element(A,m) % 2.77/2.87 | equalish(A,m) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_7,negated_conjecture, % 2.77/2.87 ( element(A,f(A)) % 2.77/2.87 | ~ element(A,m) % 2.77/2.87 | equalish(A,m) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_8,negated_conjecture, % 2.77/2.87 ( element(f(A),A) % 2.77/2.87 | ~ element(A,m) % 2.77/2.87 | equalish(A,m) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_9,negated_conjecture, % 2.77/2.87 ( ~ element(A,B) % 2.77/2.87 | ~ element(B,A) % 2.77/2.87 | equalish(A,B) % 2.77/2.87 | equalish(A,m) % 2.77/2.87 | element(B,m) % 2.77/2.87 | equalish(B,m) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_10,negated_conjecture, % 2.77/2.87 ( ~ equalish(g(A),n) % 2.77/2.87 | element(A,n) % 2.77/2.87 | equalish(A,n) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_11,negated_conjecture, % 2.77/2.87 ( ~ equalish(g(A),A) % 2.77/2.87 | element(A,n) % 2.77/2.87 | equalish(A,n) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_12,negated_conjecture, % 2.77/2.87 ( element(A,g(A)) % 2.77/2.87 | element(A,n) % 2.77/2.87 | equalish(A,n) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_13,negated_conjecture, % 2.77/2.87 ( element(g(A),A) % 2.77/2.87 | element(A,n) % 2.77/2.87 | equalish(A,n) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_14,negated_conjecture, % 2.77/2.87 ( ~ element(A,B) % 2.77/2.87 | ~ element(B,A) % 2.77/2.87 | equalish(A,B) % 2.77/2.87 | equalish(A,n) % 2.77/2.87 | ~ element(B,n) % 2.77/2.87 | equalish(B,n) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_15,negated_conjecture, % 2.77/2.87 ( ~ equalish(A,m) % 2.77/2.87 | element(A,k) % 2.77/2.87 | equalish(A,k) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_16,negated_conjecture, % 2.77/2.87 ( ~ equalish(A,n) % 2.77/2.87 | element(A,k) % 2.77/2.87 | equalish(A,k) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_17,negated_conjecture, % 2.77/2.87 ( ~ element(A,k) % 2.77/2.87 | equalish(A,n) % 2.77/2.87 | equalish(A,m) % 2.77/2.87 | equalish(A,k) ) ). % 2.77/2.87 % 2.77/2.87 cnf(c_18,negated_conjecture, % 2.77/2.87 ~ equalish(n,a) ). % 2.77/2.87 % 2.77/2.87 cnf(c_19,negated_conjecture, % 2.77/2.87 ~ equalish(m,n) ). % 2.77/2.87 % 2.77/2.87 %----This is the only difference from wos32 - SYN014-1.p % 2.77/2.87 cnf(c_20,negated_conjecture, % 2.77/2.87 ~ equalish(n,k) ). % 2.77/2.87 % 2.77/2.87 cnf(c_21,negated_conjecture, % 2.77/2.87 ~ equalish(m,a) ). % 2.77/2.87 % 2.77/2.87 cnf(c_22,negated_conjecture, % 2.77/2.87 ~ equalish(k,a) ). % 2.77/2.87 % 2.77/2.87 cnf(c_23,negated_conjecture, % 2.77/2.87 equalish(m,k) ). % 2.77/2.87 % 2.77/2.87 %-------------------------------------------------------------------------- % 2.77/2.87 %------------------------------------------- % 2.77/2.87 % Proof found % 2.77/2.87 % SZS status Theorem for theBenchmark % 2.77/2.87 % SZS output start Proof % 2.77/2.87 %ClaNum:26(EqnAxiom:0) % 2.77/2.87 %VarNum:88(SingletonVarNum:29) % 2.77/2.87 %MaxLitNum:6 % 2.77/2.87 %MaxfuncDepth:1 % 2.77/2.87 %SharedTerms:10 % 2.77/2.87 %goalClause: 1 3 4 5 6 7 9 10 11 12 13 14 15 16 17 18 19 23 24 25 26 % 2.77/2.87 %singleGoalClaCount:6 % 2.77/2.87 [1]P1(a1,a2) % 2.77/2.87 [3]~P1(a2,a3) % 2.77/2.87 [4]~P1(a1,a3) % 2.77/2.87 [5]~P1(a1,a6) % 2.77/2.87 [6]~P1(a6,a3) % 2.77/2.87 [7]~P1(a6,a2) % 2.77/2.87 [2]P1(x21,x21) % 2.77/2.87 [8]~P1(x82,x81)+P1(x81,x82) % 2.77/2.87 [9]P1(x91,a2)+~P2(x91,a3)+P1(x91,a3) % 2.77/2.87 [10]P2(x101,a3)+~P1(x101,a2)+P1(x101,a3) % 2.77/2.87 [11]P2(x111,a2)+~P1(x111,a1)+P1(x111,a2) % 2.77/2.87 [12]P2(x121,a2)+~P1(x121,a6)+P1(x121,a2) % 2.77/2.87 [13]P2(x131,a6)+P2(x131,f4(x131))+P1(x131,a6) % 2.77/2.87 [14]P2(x141,a6)+P2(f4(x141),x141)+P1(x141,a6) % 2.77/2.87 [15]P2(x151,f5(x151))+~P2(x151,a1)+P1(x151,a1) % 2.77/2.87 [16]P2(f5(x161),x161)+~P2(x161,a1)+P1(x161,a1) % 2.77/2.87 [17]P2(x171,a6)+P1(x171,a6)+~P1(f4(x171),a6) % 2.77/2.87 [18]P2(x181,a6)+~P1(f4(x181),x181)+P1(x181,a6) % 2.77/2.87 [23]~P2(x231,a1)+P1(x231,a1)+~P1(f5(x231),a1) % 2.77/2.87 [24]~P2(x241,a1)+~P1(f5(x241),x241)+P1(x241,a1) % 2.77/2.87 [20]~P1(x201,x203)+P1(x201,x202)+~P1(x203,x202) % 2.77/2.87 [21]~P2(x213,x212)+P2(x211,x212)+~P1(x213,x211) % 2.77/2.87 [22]~P2(x221,x223)+P2(x221,x222)+~P1(x223,x222) % 2.77/2.87 [19]P1(x191,a1)+P1(x191,a6)+~P2(x191,a2)+P1(x191,a2) % 2.77/2.87 [25]~P2(x252,x251)+~P2(x251,x252)+P1(x251,x252)+P1(x252,a1)+P1(x251,a1)+P2(x252,a1) % 2.77/2.87 [26]~P2(x262,x261)+~P2(x261,x262)+P1(x261,x262)+P1(x262,a6)+P1(x261,a6)+~P2(x262,a6) % 2.77/2.87 %EqnAxiom % 2.77/2.87 % 2.77/2.87 %------------------------------------------- % 2.77/2.87 cnf(31,plain, % 2.77/2.87 (P2(a6,a2)), % 2.77/2.87 inference(scs_inference,[],[1,3,4,7,2,8,10,12])). % 2.77/2.87 cnf(36,plain, % 2.77/2.87 (~P2(x361,a1)+P2(x361,a2)), % 2.77/2.87 inference(scs_inference,[],[1,3,4,7,2,8,10,12,21,22])). % 2.77/2.87 cnf(59,plain, % 2.77/2.87 (~P1(a6,a1)), % 2.77/2.87 inference(scs_inference,[],[5,8])). % 2.77/2.87 cnf(920,plain, % 2.77/2.87 (P2(a6,a1)), % 2.77/2.87 inference(scs_inference,[],[1,31,8,22])). % 2.77/2.87 cnf(921,plain, % 2.77/2.87 (P2(a6,f5(a6))), % 2.77/2.87 inference(scs_inference,[],[59,920,15])). % 2.77/2.87 cnf(923,plain, % 2.77/2.87 (P2(f5(a6),a6)), % 2.77/2.87 inference(scs_inference,[],[59,920,15,16])). % 2.77/2.87 cnf(940,plain, % 2.77/2.87 (~P1(a1,f5(a6))), % 2.77/2.87 inference(scs_inference,[],[920,59,8,23])). % 2.77/2.87 cnf(941,plain, % 2.77/2.87 (~P1(f5(a6),a1)), % 2.77/2.87 inference(scs_inference,[],[940,8])). % 2.77/2.87 cnf(1667,plain, % 2.77/2.87 (~P1(f5(a6),a6)), % 2.77/2.87 inference(scs_inference,[],[1,7,920,20,24])). % 2.77/2.87 cnf(1668,plain, % 2.77/2.87 (~P1(a6,f5(a6))), % 2.77/2.87 inference(scs_inference,[],[1667,8])). % 2.77/2.87 cnf(1670,plain, % 2.77/2.87 (~P2(f5(a6),a2)+P1(f5(a6),a2)), % 2.77/2.87 inference(scs_inference,[],[941,1667,8,19])). % 2.77/2.87 cnf(1691,plain, % 2.77/2.87 (P1(a2,f5(a6))+~P2(f5(a6),a2)), % 2.77/2.87 inference(scs_inference,[],[1670,8])). % 2.77/2.87 cnf(1723,plain, % 2.77/2.87 (~P2(f5(a6),a2)), % 2.77/2.87 inference(scs_inference,[],[1,940,1691,20])). % 2.77/2.87 cnf(1724,plain, % 2.77/2.87 (~P2(f5(a6),a1)), % 2.77/2.87 inference(scs_inference,[],[1723,36])). % 2.77/2.87 cnf(1976,plain, % 2.77/2.87 ($false), % 2.77/2.87 inference(scs_inference,[],[1724,2,941,59,923,921,1668,21,25]), % 2.77/2.87 ['proof']). % 2.77/2.87 % SZS output end Proof % 2.77/2.87 % Total time :2.260000s %------------------------------------------------------------------------------