%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN013-1 : 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 : n028.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:14 EDT 2024 % Result : Unsatisfiable 7.20s 7.27s % Output : CNFRefutation 7.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN013-1 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 19:53:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.57 start to proof:theBenchmark % 7.20/7.26 %------------------------------------------- % 7.20/7.26 % File :CSE---1.7 % 7.20/7.26 % Problem :theBenchmark % 7.20/7.26 % Transform :cnf % 7.20/7.26 % Format :tptp:raw % 7.20/7.26 % Command :java -jar mcs_scs.jar %d %s % 7.20/7.26 % 7.20/7.26 % Result :Theorem 6.650000s % 7.20/7.26 % Output :CNFRefutation 6.650000s % 7.20/7.26 %------------------------------------------- % 7.20/7.27 %-------------------------------------------------------------------------- % 7.20/7.27 % File : SYN013-1 : TPTP v8.2.0. Released v1.0.0. % 7.20/7.27 % Domain : Syntactic % 7.20/7.27 % Problem : A problem in quantification theory % 7.20/7.27 % Version : Especial. % 7.20/7.27 % English : % 7.20/7.27 % 7.20/7.27 % Refs : [Wan65] Wang (1965), Formalization and Automatic Theorem-Provi % 7.20/7.27 % : [Wos65] Wos (1965), Unpublished Note % 7.20/7.27 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a % 7.20/7.27 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 7.20/7.27 % Source : [MOW76] % 7.20/7.27 % Names : ExQ1 [Wan65] % 7.20/7.27 % : EXQ1 [MOW76] % 7.20/7.27 % : wos31 [WM76] % 7.20/7.27 % : exq1.ver1.in [ANL] % 7.20/7.27 % : exq1.ver2.in [ANL] % 7.20/7.27 % : wang1.in [OTTER] % 7.20/7.27 % 7.20/7.27 % Status : Unsatisfiable % 7.20/7.27 % Rating : 0.10 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.00 v3.4.0, 0.08 v3.3.0, 0.21 v3.2.0, 0.31 v3.1.0, 0.18 v2.7.0, 0.17 v2.6.0, 0.20 v2.5.0, 0.42 v2.4.0, 0.22 v2.3.0, 0.33 v2.2.0, 0.44 v2.1.0, 0.00 v2.0.0 % 7.20/7.27 % Syntax : Number of clauses : 16 ( 3 unt; 11 nHn; 14 RR) % 7.20/7.27 % Number of literals : 49 ( 28 equ; 19 neg) % 7.20/7.27 % Maximal clause size : 6 ( 3 avg) % 7.20/7.27 % Maximal term depth : 2 ( 1 avg) % 7.20/7.27 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty) % 7.20/7.27 % Number of functors : 5 ( 5 usr; 3 con; 0-1 aty) % 7.20/7.27 % Number of variables : 15 ( 0 sgn) % 7.20/7.27 % SPC : CNF_UNS_RFO_SEQ_NHN % 7.20/7.27 % 7.20/7.27 % Comments : % 7.20/7.27 %-------------------------------------------------------------------------- % 7.20/7.27 cnf(c_1,negated_conjecture, % 7.20/7.27 m != n ). % 7.20/7.27 % 7.20/7.27 cnf(c_2,negated_conjecture, % 7.20/7.27 n != k ). % 7.20/7.27 % 7.20/7.27 cnf(c_3,negated_conjecture, % 7.20/7.27 k != m ). % 7.20/7.27 % 7.20/7.27 cnf(c_4,negated_conjecture, % 7.20/7.27 ( Y = m % 7.20/7.27 | ~ element(Y,m) % 7.20/7.27 | f(Y) != m ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_5,negated_conjecture, % 7.20/7.27 ( Y = m % 7.20/7.27 | ~ element(Y,m) % 7.20/7.27 | f(Y) != Y ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_6,negated_conjecture, % 7.20/7.27 ( Y = m % 7.20/7.27 | ~ element(Y,m) % 7.20/7.27 | element(Y,f(Y)) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_7,negated_conjecture, % 7.20/7.27 ( Y = m % 7.20/7.27 | ~ element(Y,m) % 7.20/7.27 | element(f(Y),Y) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_8,negated_conjecture, % 7.20/7.27 ( Y = m % 7.20/7.27 | element(Y,m) % 7.20/7.27 | V = m % 7.20/7.27 | V = Y % 7.20/7.27 | ~ element(Y,V) % 7.20/7.27 | ~ element(V,Y) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_9,negated_conjecture, % 7.20/7.27 ( Y = n % 7.20/7.27 | element(Y,n) % 7.20/7.27 | g(Y) != n ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_10,negated_conjecture, % 7.20/7.27 ( Y = n % 7.20/7.27 | element(Y,n) % 7.20/7.27 | g(Y) != Y ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_11,negated_conjecture, % 7.20/7.27 ( Y = n % 7.20/7.27 | element(Y,n) % 7.20/7.27 | element(Y,g(Y)) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_12,negated_conjecture, % 7.20/7.27 ( Y = n % 7.20/7.27 | element(Y,n) % 7.20/7.27 | element(g(Y),Y) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_13,negated_conjecture, % 7.20/7.27 ( Y = n % 7.20/7.27 | ~ element(Y,n) % 7.20/7.27 | V = n % 7.20/7.27 | V = Y % 7.20/7.27 | ~ element(Y,V) % 7.20/7.27 | ~ element(V,Y) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_14,negated_conjecture, % 7.20/7.27 ( Y = k % 7.20/7.27 | Y != m % 7.20/7.27 | element(Y,k) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_15,negated_conjecture, % 7.20/7.27 ( Y = k % 7.20/7.27 | Y != n % 7.20/7.27 | element(Y,k) ) ). % 7.20/7.27 % 7.20/7.27 cnf(c_16,negated_conjecture, % 7.20/7.27 ( Y = k % 7.20/7.27 | Y = m % 7.20/7.27 | Y = n % 7.20/7.27 | ~ element(Y,k) ) ). % 7.20/7.27 % 7.20/7.27 %-------------------------------------------------------------------------- % 7.20/7.27 %------------------------------------------- % 7.20/7.27 % Proof found % 7.20/7.27 % SZS status Theorem for theBenchmark % 7.20/7.27 % SZS output start Proof % 7.20/7.27 %ClaNum:23(EqnAxiom:7) % 7.20/7.27 %VarNum:58(SingletonVarNum:15) % 7.20/7.27 %MaxLitNum:6 % 7.20/7.27 %MaxfuncDepth:1 % 7.20/7.27 %SharedTerms:6 % 7.20/7.27 %goalClause: 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 % 7.20/7.27 %singleGoalClaCount:3 % 7.20/7.27 [8]~E(a1,a5) % 7.20/7.27 [9]~E(a1,a2) % 7.20/7.27 [10]~E(a2,a5) % 7.20/7.27 [11]P1(x111,a2)+~E(x111,a1)+E(x111,a2) % 7.20/7.27 [12]P1(x121,a2)+~E(x121,a5)+E(x121,a2) % 7.20/7.27 [13]P1(x131,a5)+E(x131,a5)+~E(f3(x131),a5) % 7.20/7.27 [14]P1(x141,a5)+~E(f3(x141),x141)+E(x141,a5) % 7.20/7.27 [16]~P1(x161,a1)+E(x161,a1)+~E(f4(x161),a1) % 7.20/7.27 [17]~E(f4(x171),x171)+~P1(x171,a1)+E(x171,a1) % 7.20/7.27 [18]P1(x181,a5)+P1(x181,f3(x181))+E(x181,a5) % 7.20/7.27 [19]P1(x191,a5)+P1(f3(x191),x191)+E(x191,a5) % 7.20/7.27 [20]P1(x201,f4(x201))+~P1(x201,a1)+E(x201,a1) % 7.20/7.27 [21]P1(f4(x211),x211)+~P1(x211,a1)+E(x211,a1) % 7.20/7.27 [15]E(x151,a5)+E(x151,a2)+~P1(x151,a2)+E(x151,a1) % 7.20/7.27 [22]~P1(x222,x221)+~P1(x221,x222)+E(x221,x222)+E(x222,a1)+E(x221,a1)+P1(x221,a1) % 7.20/7.27 [23]~P1(x232,x231)+~P1(x231,x232)+E(x231,x232)+E(x232,a5)+E(x231,a5)+~P1(x231,a5) % 7.20/7.27 %EqnAxiom % 7.20/7.27 [1]E(x11,x11) % 7.20/7.27 [2]E(x22,x21)+~E(x21,x22) % 7.20/7.27 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.20/7.27 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 7.20/7.27 [5]~E(x51,x52)+E(f4(x51),f4(x52)) % 7.20/7.27 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63) % 7.20/7.27 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71) % 7.20/7.27 % 7.20/7.27 %------------------------------------------- % 7.20/7.27 cnf(24,plain, % 7.20/7.27 (E(a1,a2)+P1(a1,a2)), % 7.20/7.27 inference(equality_inference,[],[11])). % 7.20/7.27 cnf(25,plain, % 7.20/7.27 (E(a5,a2)+P1(a5,a2)), % 7.20/7.27 inference(equality_inference,[],[12])). % 7.20/7.27 cnf(26,plain, % 7.20/7.27 (P1(a1,a2)), % 7.20/7.27 inference(scs_inference,[],[9,24])). % 7.20/7.27 cnf(31,plain, % 7.20/7.27 (P1(a5,a2)), % 7.20/7.27 inference(scs_inference,[],[10,2,25])). % 7.20/7.27 cnf(38,plain, % 7.20/7.27 (P1(x381,a2)+~E(a5,x381)), % 7.20/7.27 inference(scs_inference,[],[31,6])). % 7.20/7.27 cnf(46,plain, % 7.20/7.27 (P1(x461,f3(a2))+~E(a2,x461)+P1(a2,a5)), % 7.20/7.27 inference(scs_inference,[],[10,18,6])). % 7.20/7.27 cnf(47,plain, % 7.20/7.27 (P1(a2,f3(a2))+P1(a2,a5)), % 7.20/7.27 inference(equality_inference,[],[46])). % 7.20/7.27 cnf(48,plain, % 7.20/7.27 (P1(a2,x481)+~E(f3(a2),x481)+P1(a2,a5)), % 7.20/7.27 inference(scs_inference,[],[47,7])). % 7.20/7.27 cnf(71,plain, % 7.20/7.27 (E(f4(x711),f4(x712))+~E(x712,x711)), % 7.20/7.27 inference(scs_inference,[],[2,5])). % 7.20/7.27 cnf(75,plain, % 7.20/7.27 (~E(x751,a1)+~E(a2,x751)), % 7.20/7.27 inference(scs_inference,[],[9,2,3])). % 7.20/7.27 cnf(76,plain, % 7.20/7.28 (~E(x761,a2)+~E(x761,a1)), % 7.20/7.28 inference(scs_inference,[],[75,2])). % 7.20/7.28 cnf(77,plain, % 7.20/7.28 (~P1(a2,a1)+~P1(a2,a5)), % 7.20/7.28 inference(scs_inference,[],[8,10,26,76,23])). % 7.20/7.28 cnf(82,plain, % 7.20/7.28 (~P1(a2,a1)+~E(f4(a2),a1)), % 7.20/7.28 inference(scs_inference,[],[9,2,16])). % 7.20/7.28 cnf(83,plain, % 7.20/7.28 (~P1(a2,x831)+~E(x831,a1)+~E(f4(a2),a1)), % 7.20/7.28 inference(scs_inference,[],[82,7])). % 7.20/7.28 cnf(92,plain, % 7.20/7.28 (~P1(a2,a1)+~E(f4(a2),a2)), % 7.20/7.28 inference(scs_inference,[],[9,2,17])). % 7.20/7.28 cnf(99,plain, % 7.20/7.28 (~E(x991,a5)+P1(x991,a2)), % 7.20/7.28 inference(scs_inference,[],[2,38])). % 7.20/7.28 cnf(101,plain, % 7.20/7.28 (~E(x1011,a1)+E(a1,a5)+~E(a5,x1011)), % 7.20/7.28 inference(scs_inference,[],[8,2,3])). % 7.20/7.28 cnf(102,plain, % 7.20/7.28 (~E(a5,x1021)+~E(x1021,a1)), % 7.20/7.28 inference(scs_inference,[],[8,101])). % 7.20/7.28 cnf(103,plain, % 7.20/7.28 (~E(a5,a1)), % 7.20/7.28 inference(scs_inference,[],[9,26,8,102,15])). % 7.20/7.28 cnf(111,plain, % 7.20/7.28 (~E(x1111,a2)+~E(a5,x1111)), % 7.20/7.28 inference(scs_inference,[],[10,2,3])). % 7.20/7.28 cnf(112,plain, % 7.20/7.28 (~E(x1121,a5)+~E(x1121,a2)), % 7.20/7.28 inference(scs_inference,[],[111,2])). % 7.20/7.28 cnf(170,plain, % 7.20/7.28 (~P1(a2,a1)+P1(a2,f4(a2))), % 7.20/7.28 inference(scs_inference,[],[9,2,20])). % 7.20/7.28 cnf(189,plain, % 7.20/7.28 (~P1(a2,a1)+P1(f4(a2),a2)), % 7.20/7.28 inference(scs_inference,[],[9,2,21])). % 7.20/7.28 cnf(314,plain, % 7.20/7.28 (~E(a2,a1)), % 7.20/7.28 inference(scs_inference,[],[9,26,8,75,15])). % 7.20/7.28 cnf(316,plain, % 7.20/7.28 (~P1(a2,a5)), % 7.20/7.28 inference(scs_inference,[],[103,314,10,31,77,22])). % 7.20/7.28 cnf(318,plain, % 7.20/7.28 (P1(a2,f3(a2))), % 7.20/7.28 inference(scs_inference,[],[316,47])). % 7.20/7.28 cnf(319,plain, % 7.20/7.28 (~E(f3(a2),x3191)+P1(a2,x3191)), % 7.20/7.28 inference(scs_inference,[],[316,48])). % 7.20/7.28 cnf(324,plain, % 7.20/7.28 (~E(f3(a2),a5)), % 7.20/7.28 inference(scs_inference,[],[316,319])). % 7.20/7.28 cnf(349,plain, % 7.20/7.28 (~E(f3(a2),a2)), % 7.20/7.28 inference(scs_inference,[],[316,112,14])). % 7.20/7.28 cnf(350,plain, % 7.20/7.28 (E(f3(a2),a1)+~P1(f3(a2),a2)), % 7.20/7.28 inference(scs_inference,[],[349,324,15])). % 7.20/7.28 cnf(365,plain, % 7.20/7.28 (E(f3(a2),a1)), % 7.20/7.28 inference(scs_inference,[],[10,316,350,19])). % 7.20/7.28 cnf(374,plain, % 7.20/7.28 (~E(f4(a2),a1)), % 7.20/7.28 inference(scs_inference,[],[318,365,71,2,83])). % 7.20/7.28 cnf(688,plain, % 7.20/7.28 (~E(f4(a2),a2)), % 7.20/7.28 inference(scs_inference,[],[365,92,319])). % 7.20/7.28 cnf(692,plain, % 7.20/7.28 (~P1(a2,a1)+E(f4(a2),a5)), % 7.20/7.28 inference(scs_inference,[],[688,374,15,99,189])). % 7.20/7.28 cnf(699,plain, % 7.20/7.28 (E(f4(a2),a5)), % 7.20/7.28 inference(scs_inference,[],[365,692,319])). % 7.20/7.28 cnf(792,plain, % 7.20/7.28 (~P1(a2,a1)), % 7.20/7.28 inference(scs_inference,[],[316,699,170,7])). % 7.20/7.28 cnf(793,plain, % 7.20/7.28 ($false), % 7.20/7.28 inference(scs_inference,[],[792,365,319]), % 7.20/7.28 ['proof']). % 7.20/7.28 % SZS output end Proof % 7.20/7.28 % Total time :6.650000s %------------------------------------------------------------------------------