%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN014-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 : n018.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 1.55s 1.64s % Output : CNFRefutation 1.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN014-2 : TPTP v8.2.0. Released v1.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n018.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 : Sun Jun 23 21:36:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 1.55/1.63 %------------------------------------------- % 1.55/1.63 % File :CSE---1.7 % 1.55/1.63 % Problem :theBenchmark % 1.55/1.63 % Transform :cnf % 1.55/1.63 % Format :tptp:raw % 1.55/1.63 % Command :java -jar mcs_scs.jar %d %s % 1.55/1.63 % 1.55/1.63 % Result :Theorem 1.040000s % 1.55/1.63 % Output :CNFRefutation 1.040000s % 1.55/1.63 %------------------------------------------- % 1.55/1.63 %-------------------------------------------------------------------------- % 1.55/1.63 % File : SYN014-2 : TPTP v8.2.0. Released v1.0.0. % 1.55/1.63 % Domain : Syntactic % 1.55/1.63 % Problem : A problem in quantification theory % 1.55/1.63 % Version : [Wan65] axioms : Reduced & Augmented > Especial. % 1.55/1.63 % Theorem formulation : Modified. % 1.55/1.63 % English : % 1.55/1.63 % 1.55/1.63 % Refs : [Wos65] Wos (1965), Unpublished Note % 1.55/1.63 % : [Wan65] Wang (1965), Formalization and Automatic Theorem-Provi % 1.55/1.63 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 1.55/1.63 % Source : [SPRFN] % 1.55/1.63 % Names : Problem 32 [Wos65] % 1.55/1.63 % : wos32 [WM76] % 1.55/1.63 % 1.55/1.63 % Status : Unsatisfiable % 1.55/1.63 % Rating : 0.00 v2.2.1, 0.25 v2.1.0, 0.00 v2.0.0 % 1.55/1.63 % Syntax : Number of clauses : 26 ( 7 unt; 13 nHn; 23 RR) % 1.55/1.63 % Number of literals : 70 ( 0 equ; 29 neg) % 1.55/1.63 % Maximal clause size : 6 ( 2 avg) % 1.55/1.63 % Maximal term depth : 2 ( 1 avg) % 1.55/1.63 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty) % 1.55/1.63 % Number of functors : 6 ( 6 usr; 4 con; 0-1 aty) % 1.55/1.63 % Number of variables : 29 ( 0 sgn) % 1.55/1.63 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.55/1.63 % 1.55/1.63 % Comments : % 1.55/1.63 %-------------------------------------------------------------------------- % 1.55/1.63 cnf(reflexivityish,axiom, % 1.55/1.63 equalish(X,X) ). % 1.55/1.63 % 1.55/1.63 cnf(symmetryish,axiom, % 1.55/1.63 ( ~ equalish(X,Y) % 1.55/1.63 | equalish(Y,X) ) ). % 1.55/1.63 % 1.55/1.63 cnf(transitivityish,axiom, % 1.55/1.63 ( ~ equalish(X,Y) % 1.55/1.63 | ~ equalish(Y,Z) % 1.55/1.63 | equalish(X,Z) ) ). % 1.55/1.63 % 1.55/1.63 cnf(element_substitutionish1,axiom, % 1.55/1.63 ( ~ equalish(A,B) % 1.55/1.63 | ~ element(C,A) % 1.55/1.63 | element(C,B) ) ). % 1.55/1.63 % 1.55/1.63 cnf(element_substitutionish2,axiom, % 1.55/1.63 ( ~ element(A,B) % 1.55/1.63 | ~ equalish(A,C) % 1.55/1.63 | element(C,B) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_3,negated_conjecture, % 1.55/1.63 ( ~ element(A,a) % 1.55/1.63 | equalish(A,k) % 1.55/1.63 | equalish(A,a) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_4,negated_conjecture, % 1.55/1.63 ( ~ equalish(A,k) % 1.55/1.63 | element(A,a) % 1.55/1.63 | equalish(A,a) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_5,negated_conjecture, % 1.55/1.63 ( ~ equalish(f(A),m) % 1.55/1.63 | ~ element(A,m) % 1.55/1.63 | equalish(A,m) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_6,negated_conjecture, % 1.55/1.63 ( ~ equalish(f(A),A) % 1.55/1.63 | ~ element(A,m) % 1.55/1.63 | equalish(A,m) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_7,negated_conjecture, % 1.55/1.63 ( element(A,f(A)) % 1.55/1.63 | ~ element(A,m) % 1.55/1.63 | equalish(A,m) ) ). % 1.55/1.63 % 1.55/1.63 cnf(c_8,negated_conjecture, % 1.55/1.63 ( element(f(A),A) % 1.55/1.63 | ~ element(A,m) % 1.55/1.63 | equalish(A,m) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_9,negated_conjecture, % 1.55/1.64 ( ~ element(A,B) % 1.55/1.64 | ~ element(B,A) % 1.55/1.64 | equalish(A,B) % 1.55/1.64 | equalish(A,m) % 1.55/1.64 | element(B,m) % 1.55/1.64 | equalish(B,m) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_10,negated_conjecture, % 1.55/1.64 ( ~ equalish(g(A),n) % 1.55/1.64 | element(A,n) % 1.55/1.64 | equalish(A,n) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_11,negated_conjecture, % 1.55/1.64 ( ~ equalish(g(A),A) % 1.55/1.64 | element(A,n) % 1.55/1.64 | equalish(A,n) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_12,negated_conjecture, % 1.55/1.64 ( element(A,g(A)) % 1.55/1.64 | element(A,n) % 1.55/1.64 | equalish(A,n) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_13,negated_conjecture, % 1.55/1.64 ( element(g(A),A) % 1.55/1.64 | element(A,n) % 1.55/1.64 | equalish(A,n) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_14,negated_conjecture, % 1.55/1.64 ( ~ element(A,B) % 1.55/1.64 | ~ element(B,A) % 1.55/1.64 | equalish(A,B) % 1.55/1.64 | equalish(A,n) % 1.55/1.64 | ~ element(B,n) % 1.55/1.64 | equalish(B,n) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_15,negated_conjecture, % 1.55/1.64 ( ~ equalish(A,m) % 1.55/1.64 | element(A,k) % 1.55/1.64 | equalish(A,k) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_16,negated_conjecture, % 1.55/1.64 ( ~ equalish(A,n) % 1.55/1.64 | element(A,k) % 1.55/1.64 | equalish(A,k) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_17,negated_conjecture, % 1.55/1.64 ( ~ element(A,k) % 1.55/1.64 | equalish(A,n) % 1.55/1.64 | equalish(A,m) % 1.55/1.64 | equalish(A,k) ) ). % 1.55/1.64 % 1.55/1.64 cnf(c_18,negated_conjecture, % 1.55/1.64 ~ equalish(n,a) ). % 1.55/1.64 % 1.55/1.64 cnf(c_19,negated_conjecture, % 1.55/1.64 ~ equalish(m,n) ). % 1.55/1.64 % 1.55/1.64 %----This is the only difference from wos33 - SYN015-1.p % 1.55/1.64 cnf(c_20,negated_conjecture, % 1.55/1.64 equalish(n,k) ). % 1.55/1.64 % 1.55/1.64 cnf(c_21,negated_conjecture, % 1.55/1.64 ~ equalish(m,a) ). % 1.55/1.64 % 1.55/1.64 cnf(c_22,negated_conjecture, % 1.55/1.64 ~ equalish(k,a) ). % 1.55/1.64 % 1.55/1.64 cnf(c_23,negated_conjecture, % 1.55/1.64 equalish(m,k) ). % 1.55/1.64 % 1.55/1.64 %-------------------------------------------------------------------------- % 1.55/1.64 %------------------------------------------- % 1.55/1.64 % Proof found % 1.55/1.64 % SZS status Theorem for theBenchmark % 1.55/1.64 % SZS output start Proof % 1.55/1.64 %ClaNum:26(EqnAxiom:0) % 1.55/1.64 %VarNum:88(SingletonVarNum:29) % 1.55/1.64 %MaxLitNum:6 % 1.55/1.64 %MaxfuncDepth:1 % 1.55/1.64 %SharedTerms:10 % 1.55/1.64 %goalClause: 1 2 4 5 6 7 9 10 11 12 13 14 15 16 17 18 19 23 24 25 26 % 1.55/1.64 %singleGoalClaCount:6 % 1.55/1.64 [1]P1(a1,a2) % 1.55/1.64 [2]P1(a6,a2) % 1.55/1.64 [4]~P1(a2,a3) % 1.55/1.64 [5]~P1(a1,a3) % 1.55/1.64 [6]~P1(a1,a6) % 1.55/1.64 [7]~P1(a6,a3) % 1.55/1.64 [3]P1(x31,x31) % 1.55/1.64 [8]~P1(x82,x81)+P1(x81,x82) % 1.55/1.64 [9]P1(x91,a2)+~P2(x91,a3)+P1(x91,a3) % 1.55/1.64 [10]P2(x101,a3)+~P1(x101,a2)+P1(x101,a3) % 1.55/1.64 [11]P2(x111,a2)+~P1(x111,a1)+P1(x111,a2) % 1.55/1.64 [12]P2(x121,a2)+~P1(x121,a6)+P1(x121,a2) % 1.55/1.64 [13]P2(x131,a6)+P2(x131,f4(x131))+P1(x131,a6) % 1.55/1.64 [14]P2(x141,a6)+P2(f4(x141),x141)+P1(x141,a6) % 1.55/1.64 [15]P2(x151,f5(x151))+~P2(x151,a1)+P1(x151,a1) % 1.55/1.64 [16]P2(f5(x161),x161)+~P2(x161,a1)+P1(x161,a1) % 1.55/1.64 [17]P2(x171,a6)+P1(x171,a6)+~P1(f4(x171),a6) % 1.55/1.64 [18]P2(x181,a6)+~P1(f4(x181),x181)+P1(x181,a6) % 1.55/1.64 [23]~P2(x231,a1)+P1(x231,a1)+~P1(f5(x231),a1) % 1.55/1.64 [24]~P2(x241,a1)+~P1(f5(x241),x241)+P1(x241,a1) % 1.55/1.64 [20]~P1(x201,x203)+P1(x201,x202)+~P1(x203,x202) % 1.55/1.64 [21]~P2(x213,x212)+P2(x211,x212)+~P1(x213,x211) % 1.55/1.64 [22]~P2(x221,x223)+P2(x221,x222)+~P1(x223,x222) % 1.55/1.64 [19]P1(x191,a1)+P1(x191,a6)+~P2(x191,a2)+P1(x191,a2) % 1.55/1.64 [25]~P2(x252,x251)+~P2(x251,x252)+P1(x251,x252)+P1(x252,a1)+P1(x251,a1)+P2(x252,a1) % 1.55/1.64 [26]~P2(x262,x261)+~P2(x261,x262)+P1(x261,x262)+P1(x262,a6)+P1(x261,a6)+~P2(x262,a6) % 1.55/1.64 %EqnAxiom % 1.55/1.64 % 1.55/1.64 %------------------------------------------- % 1.55/1.64 cnf(27,plain, % 1.55/1.64 (~P1(a3,a2)), % 1.55/1.64 inference(scs_inference,[],[4,8])). % 1.55/1.64 cnf(33,plain, % 1.55/1.64 (~P2(x331,a1)+P2(x331,a2)), % 1.55/1.64 inference(scs_inference,[],[1,4,5,8,10,21,22])). % 1.55/1.64 cnf(38,plain, % 1.55/1.64 (~P1(a3,a6)), % 1.55/1.64 inference(scs_inference,[],[7,8])). % 1.55/1.64 cnf(42,plain, % 1.55/1.64 (~P2(x421,a6)+P2(x421,a2)), % 1.55/1.64 inference(scs_inference,[],[2,7,8,10,22])). % 1.55/1.64 cnf(51,plain, % 1.55/1.64 (~P2(a3,a2)), % 1.55/1.64 inference(scs_inference,[],[5,38,27,8,19])). % 1.55/1.64 cnf(55,plain, % 1.55/1.64 (~P2(a3,a6)), % 1.55/1.64 inference(scs_inference,[],[5,38,27,8,19,33,42])). % 1.55/1.64 cnf(587,plain, % 1.55/1.64 (P2(a3,f4(a3))), % 1.55/1.64 inference(scs_inference,[],[7,55,8,13])). % 1.55/1.64 cnf(682,plain, % 1.55/1.64 (P2(f4(a3),a3)), % 1.55/1.64 inference(scs_inference,[],[7,55,8,14])). % 1.55/1.64 cnf(683,plain, % 1.55/1.64 (P1(f4(a3),a3)+P1(f4(a3),a2)), % 1.55/1.64 inference(scs_inference,[],[682,9])). % 1.55/1.64 cnf(721,plain, % 1.55/1.64 (P1(f4(a3),a3)), % 1.55/1.64 inference(scs_inference,[],[587,51,683,22])). % 1.55/1.64 cnf(722,plain, % 1.55/1.64 ($false), % 1.55/1.64 inference(scs_inference,[],[38,721,55,18]), % 1.55/1.64 ['proof']). % 1.55/1.64 % SZS output end Proof % 1.55/1.64 % Total time :1.040000s %------------------------------------------------------------------------------