%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN075-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 : 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 19:04:28 EDT 2024 % Result : Unsatisfiable 7.37s 7.43s % Output : CNFRefutation 7.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN075-1 : TPTP v8.2.0. Released v1.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.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 22:53:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.52/0.59 start to proof:theBenchmark % 7.37/7.43 %------------------------------------------- % 7.37/7.43 % File :CSE---1.7 % 7.37/7.43 % Problem :theBenchmark % 7.37/7.43 % Transform :cnf % 7.37/7.43 % Format :tptp:raw % 7.37/7.43 % Command :java -jar mcs_scs.jar %d %s % 7.37/7.43 % 7.37/7.43 % Result :Theorem 6.790000s % 7.37/7.43 % Output :CNFRefutation 6.790000s % 7.37/7.43 %------------------------------------------- % 7.37/7.43 %-------------------------------------------------------------------------- % 7.37/7.43 % File : SYN075-1 : TPTP v8.2.0. Released v1.0.0. % 7.37/7.43 % Domain : Syntactic % 7.37/7.43 % Problem : Pelletier Problem 52 % 7.37/7.43 % Version : Especial. % 7.37/7.43 % English : % 7.37/7.43 % 7.37/7.43 % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 7.37/7.43 % Source : [Pel86] % 7.37/7.43 % Names : Pelletier 52 [Pel86] % 7.37/7.43 % 7.37/7.43 % Status : Unsatisfiable % 7.37/7.43 % 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.00 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.12 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.11 v2.2.1, 0.11 v2.2.0, 0.22 v2.1.0, 0.33 v2.0.0 % 7.37/7.43 % Syntax : Number of clauses : 10 ( 0 unt; 4 nHn; 8 RR) % 7.37/7.43 % Number of literals : 31 ( 17 equ; 17 neg) % 7.37/7.43 % Maximal clause size : 4 ( 3 avg) % 7.37/7.43 % Maximal term depth : 2 ( 1 avg) % 7.37/7.43 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty) % 7.37/7.43 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 7.37/7.43 % Number of variables : 23 ( 2 sgn) % 7.37/7.43 % SPC : CNF_UNS_RFO_SEQ_NHN % 7.37/7.43 % 7.37/7.43 % Comments : % 7.37/7.43 %-------------------------------------------------------------------------- % 7.37/7.43 cnf(clause_1,axiom, % 7.37/7.43 ( ~ big_f(X,Y) % 7.37/7.43 | X = a ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_2,axiom, % 7.37/7.43 ( ~ big_f(X,Y) % 7.37/7.43 | Y = b ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_3,axiom, % 7.37/7.43 ( X != a % 7.37/7.43 | Y != b % 7.37/7.43 | big_f(X,Y) ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_4,negated_conjecture, % 7.37/7.43 ( ~ big_f(Y,f(X)) % 7.37/7.43 | Y != g(X) % 7.37/7.43 | f(X) = X ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_5,negated_conjecture, % 7.37/7.43 ( ~ big_f(Y,f(X)) % 7.37/7.43 | Y = g(X) % 7.37/7.43 | big_f(h(X,Z),f(X)) % 7.37/7.43 | ~ big_f(h(X,Z),f(X)) ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_6,negated_conjecture, % 7.37/7.43 ( Y != g(X) % 7.37/7.43 | big_f(Y,f(X)) % 7.37/7.43 | f(X) = X ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_7,negated_conjecture, % 7.37/7.43 ( Y != g(X) % 7.37/7.43 | big_f(Y,f(X)) % 7.37/7.43 | big_f(h(X,Z),f(X)) % 7.37/7.43 | h(X,Z) = Z ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_8,negated_conjecture, % 7.37/7.43 ( Y != g(X) % 7.37/7.43 | big_f(Y,f(X)) % 7.37/7.43 | h(X,Z) != Z % 7.37/7.43 | ~ big_f(h(X,Z),f(X)) ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_9,negated_conjecture, % 7.37/7.43 ( f(X) != X % 7.37/7.43 | big_f(h(X,Z),f(X)) % 7.37/7.43 | h(X,Z) = Z ) ). % 7.37/7.43 % 7.37/7.43 cnf(clause_10,negated_conjecture, % 7.37/7.43 ( f(X) != X % 7.37/7.43 | h(X,Z) != Z % 7.37/7.43 | ~ big_f(h(X,Z),f(X)) ) ). % 7.37/7.43 % 7.37/7.43 %-------------------------------------------------------------------------- % 7.37/7.43 %------------------------------------------- % 7.37/7.43 % Proof found % 7.37/7.43 % SZS status Theorem for theBenchmark % 7.37/7.43 % SZS output start Proof % 7.37/7.44 %ClaNum:18(EqnAxiom:9) % 7.37/7.44 %VarNum:58(SingletonVarNum:20) % 7.37/7.44 %MaxLitNum:4 % 7.37/7.44 %MaxfuncDepth:1 % 7.37/7.44 %SharedTerms:2 % 7.37/7.44 %goalClause: 13 14 15 16 17 18 % 7.37/7.44 [11]~P1(x112,x111)+E(x111,a1) % 7.37/7.44 [12]~P1(x121,x122)+E(x121,a2) % 7.37/7.44 [10]P1(x101,x102)+~E(x102,a1)+~E(x101,a2) % 7.37/7.44 [13]~E(x132,f4(x131))+E(f3(x131),x131)+P1(x132,f3(x131)) % 7.37/7.44 [14]E(f3(x141),x141)+~P1(x142,f3(x141))+~E(x142,f4(x141)) % 7.37/7.44 [15]~E(f3(x151),x151)+E(f5(x151,x152),x152)+P1(f5(x151,x152),f3(x151)) % 7.37/7.44 [17]~E(f3(x171),x171)+~E(f5(x171,x172),x172)+~P1(f5(x171,x172),f3(x171)) % 7.37/7.44 [16]~E(x163,f4(x161))+E(f5(x161,x162),x162)+P1(f5(x161,x162),f3(x161))+P1(x163,f3(x161)) % 7.37/7.44 [18]~E(x181,f4(x182))+P1(x181,f3(x182))+~E(f5(x182,x183),x183)+~P1(f5(x182,x183),f3(x182)) % 7.37/7.44 %EqnAxiom % 7.37/7.44 [1]E(x11,x11) % 7.37/7.44 [2]E(x22,x21)+~E(x21,x22) % 7.37/7.44 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.37/7.44 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 7.37/7.44 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53)) % 7.37/7.44 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62)) % 7.37/7.44 [7]~E(x71,x72)+E(f4(x71),f4(x72)) % 7.37/7.44 [8]P1(x82,x83)+~E(x81,x82)+~P1(x81,x83) % 7.37/7.44 [9]P1(x93,x92)+~E(x91,x92)+~P1(x93,x91) % 7.37/7.44 % 7.37/7.44 %------------------------------------------- % 7.37/7.44 cnf(19,plain, % 7.37/7.44 (E(f3(x191),x191)+P1(f4(x191),f3(x191))), % 7.37/7.44 inference(equality_inference,[],[13])). % 7.37/7.44 cnf(24,plain, % 7.37/7.44 (E(f3(x241),x241)+E(f3(x241),a1)), % 7.37/7.44 inference(scs_inference,[],[11,19])). % 7.37/7.44 cnf(42,plain, % 7.37/7.44 (E(f5(a1,x421),x421)+P1(f5(a1,x421),f3(a1))), % 7.37/7.44 inference(scs_inference,[],[15,24])). % 7.37/7.44 cnf(43,plain, % 7.37/7.44 (E(x431,f5(a1,x431))+P1(f5(a1,x431),f3(a1))), % 7.37/7.44 inference(scs_inference,[],[42,2])). % 7.37/7.44 cnf(44,plain, % 7.37/7.44 (P1(f5(a1,x441),f3(a1))+E(f3(x441),f3(f5(a1,x441)))), % 7.37/7.44 inference(scs_inference,[],[43,4])). % 7.37/7.44 cnf(46,plain, % 7.37/7.44 (~E(f5(a1,x461),x461)+~P1(f5(a1,x461),f3(a1))), % 7.37/7.44 inference(scs_inference,[],[17,24])). % 7.37/7.44 cnf(58,plain, % 7.37/7.44 (~E(x581,x582)+E(f5(x582,x583),f5(x581,x583))), % 7.37/7.44 inference(scs_inference,[],[2,5])). % 7.37/7.44 cnf(60,plain, % 7.37/7.44 (E(f5(x601,x602),f5(x601,x603))+~E(x603,x602)), % 7.37/7.44 inference(scs_inference,[],[2,6])). % 7.37/7.44 cnf(62,plain, % 7.37/7.44 (~E(x621,x622)+E(f4(x622),f4(x621))), % 7.37/7.44 inference(scs_inference,[],[2,7])). % 7.37/7.44 cnf(64,plain, % 7.37/7.44 (E(a1,x641)+~P1(x642,x641)), % 7.37/7.44 inference(scs_inference,[],[2,11])). % 7.37/7.44 cnf(65,plain, % 7.37/7.44 (E(f3(x651),x651)+E(a1,f3(x651))), % 7.37/7.44 inference(scs_inference,[],[64,19])). % 7.37/7.44 cnf(66,plain, % 7.37/7.44 (E(f3(f3(x661)),f3(x661))+E(a1,f3(x661))), % 7.37/7.44 inference(scs_inference,[],[65,4])). % 7.37/7.44 cnf(74,plain, % 7.37/7.44 (~E(x741,x742)+~E(x741,x743)+E(x742,x743)), % 7.37/7.44 inference(scs_inference,[],[2,3])). % 7.37/7.44 cnf(77,plain, % 7.37/7.44 (P1(f4(x771),f3(x771))+E(x771,f3(x771))), % 7.37/7.44 inference(scs_inference,[],[2,19])). % 7.37/7.44 cnf(86,plain, % 7.37/7.44 (~E(x861,x862)+~P1(x862,x863)+P1(x861,x863)), % 7.37/7.44 inference(scs_inference,[],[2,8])). % 7.37/7.44 cnf(95,plain, % 7.37/7.44 (~E(a1,x951)+P1(x952,x951)+~E(x952,a2)), % 7.37/7.44 inference(scs_inference,[],[2,10])). % 7.37/7.44 cnf(99,plain, % 7.37/7.44 (~E(a2,x991)+P1(x991,x992)+~E(x992,a1)), % 7.37/7.44 inference(scs_inference,[],[2,10])). % 7.37/7.44 cnf(113,plain, % 7.37/7.44 (E(f3(f5(a1,x1131)),f3(x1131))+P1(f5(a1,x1131),f3(a1))), % 7.37/7.44 inference(scs_inference,[],[2,44])). % 7.37/7.44 cnf(128,plain, % 7.37/7.44 (E(x1281,f3(x1281))+E(a1,f3(x1281))), % 7.37/7.44 inference(scs_inference,[],[2,65])). % 7.37/7.44 cnf(131,plain, % 7.37/7.44 (~E(x1311,x1312)+E(x1313,x1311)+~E(x1312,x1313)), % 7.37/7.44 inference(scs_inference,[],[2,74])). % 7.37/7.44 cnf(184,plain, % 7.37/7.44 (E(x1841,f3(x1841))+P1(x1842,f3(x1841))+~E(x1842,f4(x1841))), % 7.37/7.44 inference(scs_inference,[],[2,13])). % 7.37/7.44 cnf(201,plain, % 7.37/7.44 (~E(f4(x2011),x2012)+E(x2011,f3(x2011))+P1(x2012,f3(x2011))), % 7.37/7.44 inference(scs_inference,[],[2,184])). % 7.37/7.44 cnf(308,plain, % 7.37/7.44 (~P1(x3081,x3082)+P1(x3083,x3082)+~E(a2,x3083)), % 7.37/7.44 inference(scs_inference,[],[11,99])). % 7.37/7.44 cnf(343,plain, % 7.37/7.44 (E(x3431,f3(x3431))+P1(a1,f3(x3431))+~P1(x3432,f4(x3431))), % 7.37/7.44 inference(scs_inference,[],[11,201])). % 7.37/7.44 cnf(358,plain, % 7.37/7.44 (~P1(x3581,a2)+~P1(x3582,x3583)+P1(a1,x3583)), % 7.37/7.44 inference(scs_inference,[],[11,308])). % 7.37/7.44 cnf(359,plain, % 7.37/7.44 (E(f3(x3591),x3591)+P1(a1,f3(x3591))+~P1(x3592,a2)), % 7.37/7.44 inference(scs_inference,[],[358,19])). % 7.37/7.44 cnf(360,plain, % 7.37/7.44 (E(x3601,f3(x3601))+P1(a1,f3(x3601))+~P1(x3602,a2)), % 7.37/7.44 inference(scs_inference,[],[359,2])). % 7.37/7.44 cnf(406,plain, % 7.37/7.44 (~P1(f5(a1,a2),x4061)+~P1(f5(a1,a2),f3(a1))), % 7.37/7.44 inference(scs_inference,[],[12,46])). % 7.37/7.44 cnf(407,plain, % 7.37/7.44 (~P1(f5(a1,a2),f3(a1))), % 7.37/7.44 inference(factoring_inference,[],[406])). % 7.37/7.44 cnf(438,plain, % 7.37/7.44 ($false), % 7.37/7.44 inference(scs_inference,[],[407,42,43,44,58,60,62,113,2,86,95,131,308,343,360,3,9,65,66,77,128]), % 7.37/7.44 ['proof']). % 7.37/7.44 % SZS output end Proof % 7.37/7.44 % Total time :6.790000s %------------------------------------------------------------------------------