%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN328-1 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n024.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:05:10 EDT 2024 % Result : Unsatisfiable 0.57s 0.87s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN328-1 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.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:41:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.56/0.58 start to proof:theBenchmark % 0.57/0.86 %------------------------------------------- % 0.57/0.86 % File :CSE---1.7 % 0.57/0.86 % Problem :theBenchmark % 0.57/0.86 % Transform :cnf % 0.57/0.86 % Format :tptp:raw % 0.57/0.86 % Command :java -jar mcs_scs.jar %d %s % 0.57/0.86 % 0.57/0.86 % Result :Theorem 0.250000s % 0.57/0.86 % Output :CNFRefutation 0.250000s % 0.57/0.86 %------------------------------------------- % 0.57/0.86 %-------------------------------------------------------------------------- % 0.57/0.86 % File : SYN328-1 : TPTP v8.2.0. Released v1.2.0. % 0.57/0.86 % Domain : Syntactic % 0.57/0.86 % Problem : Church problem 46.12 (3) % 0.57/0.86 % Version : Especial. % 0.57/0.86 % English : % 0.57/0.86 % 0.57/0.86 % Refs : [Chu56] Church (1956), Introduction to Mathematical Logic I % 0.57/0.86 % : [FL+93] Fermuller et al. (1993), Resolution Methods for the De % 0.57/0.86 % : [Tam94] Tammet (1994), Email to Geoff Sutcliffe. % 0.57/0.86 % Source : [Tam94] % 0.57/0.86 % Names : Ch12N3 [Tam94] % 0.57/0.86 % 0.57/0.86 % Status : Unsatisfiable % 0.57/0.87 % Rating : 0.08 v8.2.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.00 v2.0.0 % 0.57/0.87 % Syntax : Number of clauses : 11 ( 0 unt; 4 nHn; 9 RR) % 0.57/0.87 % Number of literals : 28 ( 0 equ; 14 neg) % 0.57/0.87 % Maximal clause size : 3 ( 2 avg) % 0.57/0.87 % Maximal term depth : 2 ( 1 avg) % 0.57/0.87 % Number of predicates : 3 ( 3 usr; 0 prp; 1-1 aty) % 0.57/0.87 % Number of functors : 2 ( 2 usr; 0 con; 1-1 aty) % 0.57/0.87 % Number of variables : 11 ( 0 sgn) % 0.57/0.87 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.57/0.87 % 0.57/0.87 % Comments : All the problems here can be decided by using a certain % 0.57/0.87 % completeness-preserving term ordering strategies. See [FL+93]. % 0.57/0.87 % : The conversion from the full 1st order form in [Chu56] % 0.57/0.87 % to clause form was done by hand by Tanel Tammet. % 0.57/0.87 %-------------------------------------------------------------------------- % 0.57/0.87 cnf(clause1,negated_conjecture, % 0.57/0.87 ( ~ f(y(X)) % 0.57/0.87 | g(y(X)) % 0.57/0.87 | ~ f(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause2,negated_conjecture, % 0.57/0.87 ( f(y(X)) % 0.57/0.87 | f(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause3,negated_conjecture, % 0.57/0.87 ( ~ g(y(X)) % 0.57/0.87 | f(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause4,negated_conjecture, % 0.57/0.87 ( ~ f(y(X)) % 0.57/0.87 | h(y(X)) % 0.57/0.87 | ~ g(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause5,negated_conjecture, % 0.57/0.87 ( f(y(X)) % 0.57/0.87 | g(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause6,negated_conjecture, % 0.57/0.87 ( ~ h(y(X)) % 0.57/0.87 | g(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause7,negated_conjecture, % 0.57/0.87 ( f(y(X)) % 0.57/0.87 | h(y(X)) % 0.57/0.87 | ~ h(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause8,negated_conjecture, % 0.57/0.87 ( ~ g(y(X)) % 0.57/0.87 | h(y(X)) % 0.57/0.87 | ~ h(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause9,negated_conjecture, % 0.57/0.87 ( ~ f(y(X)) % 0.57/0.87 | g(y(X)) % 0.57/0.87 | h(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause10,negated_conjecture, % 0.57/0.87 ( ~ h(y(X)) % 0.57/0.87 | h(X) ) ). % 0.57/0.87 % 0.57/0.87 cnf(clause11,negated_conjecture, % 0.57/0.87 ( ~ f(z(X)) % 0.57/0.87 | ~ g(z(X)) % 0.57/0.87 | ~ h(z(X)) ) ). % 0.57/0.87 % 0.57/0.87 %-------------------------------------------------------------------------- % 0.57/0.87 %------------------------------------------- % 0.57/0.87 % Proof found % 0.57/0.87 % SZS status Theorem for theBenchmark % 0.57/0.87 % SZS output start Proof % 0.57/0.87 %ClaNum:11(EqnAxiom:0) % 0.57/0.87 %VarNum:28(SingletonVarNum:11) % 0.57/0.87 %MaxLitNum:3 % 0.57/0.87 %MaxfuncDepth:1 % 0.57/0.87 %SharedTerms:0 % 0.57/0.87 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 % 0.57/0.87 [1]P1(x11)+P1(f1(x11)) % 0.57/0.87 [2]P2(x21)+P1(f1(x21)) % 0.57/0.87 [3]P1(x31)+~P2(f1(x31)) % 0.57/0.87 [4]P2(x41)+~P3(f1(x41)) % 0.57/0.87 [5]P3(x51)+~P3(f1(x51)) % 0.57/0.87 [6]~P3(x61)+P1(f1(x61))+P3(f1(x61)) % 0.57/0.87 [7]P3(x71)+P2(f1(x71))+~P1(f1(x71)) % 0.57/0.87 [8]~P1(x81)+P2(f1(x81))+~P1(f1(x81)) % 0.57/0.87 [9]~P2(x91)+P3(f1(x91))+~P1(f1(x91)) % 0.57/0.87 [10]~P3(x101)+P3(f1(x101))+~P2(f1(x101)) % 0.58/0.87 [11]~P1(f2(x111))+~P2(f2(x111))+~P3(f2(x111)) % 0.58/0.87 %EqnAxiom % 0.58/0.87 % 0.58/0.87 %------------------------------------------- % 0.58/0.87 cnf(18,plain, % 0.58/0.87 (P2(x181)+P2(f1(f1(x181)))+~P1(f1(f1(x181)))), % 0.58/0.87 inference(scs_inference,[],[7,4])). % 0.58/0.87 cnf(21,plain, % 0.58/0.87 (P1(f1(f2(x211)))+~P2(f2(x211))+~P3(f2(x211))), % 0.58/0.87 inference(scs_inference,[],[11,1])). % 0.58/0.87 cnf(26,plain, % 0.58/0.87 (P2(f1(f1(x261)))+P2(f1(x261))+P2(x261)), % 0.58/0.87 inference(scs_inference,[],[2,18])). % 0.58/0.87 cnf(28,plain, % 0.58/0.87 (~P3(x281)+P1(f1(f1(x281)))+P3(f1(x281))), % 0.58/0.87 inference(scs_inference,[],[2,10])). % 0.58/0.87 cnf(29,plain, % 0.58/0.87 (~P3(x291)+P3(f1(x291))+P2(f1(f1(x291)))), % 0.58/0.87 inference(scs_inference,[],[28,7])). % 0.58/0.87 cnf(35,plain, % 0.58/0.87 (~P3(f2(x351))+P1(f1(f2(x351)))), % 0.58/0.87 inference(scs_inference,[],[2,21])). % 0.58/0.87 cnf(36,plain, % 0.58/0.87 (P1(f1(f2(x361)))+~P3(f1(f2(x361)))), % 0.58/0.87 inference(scs_inference,[],[35,5])). % 0.58/0.87 cnf(46,plain, % 0.58/0.87 (P3(x461)+~P2(f1(f1(x461)))+P2(f1(x461))), % 0.58/0.87 inference(scs_inference,[],[3,7])). % 0.58/0.87 cnf(47,plain, % 0.58/0.87 (P2(x471)+P3(x471)+P2(f1(x471))), % 0.58/0.87 inference(scs_inference,[],[46,26])). % 0.58/0.87 cnf(54,plain, % 0.58/0.87 (~P1(x541)+~P2(f1(f1(x541)))+P2(f1(x541))), % 0.58/0.87 inference(scs_inference,[],[3,8])). % 0.58/0.87 cnf(55,plain, % 0.58/0.87 (P2(x551)+~P1(x551)+P2(f1(x551))), % 0.58/0.87 inference(scs_inference,[],[54,26])). % 0.58/0.87 cnf(58,plain, % 0.58/0.87 (~P1(f1(x581))+P2(f1(f1(x581)))+P1(x581)), % 0.58/0.87 inference(scs_inference,[],[3,55])). % 0.58/0.87 cnf(59,plain, % 0.58/0.87 (P2(f1(f1(x591)))+P1(x591)), % 0.58/0.87 inference(scs_inference,[],[58,1])). % 0.58/0.87 cnf(61,plain, % 0.58/0.87 (~P2(x611)+~P2(f1(f1(x611)))+P3(f1(x611))), % 0.58/0.87 inference(scs_inference,[],[3,9])). % 0.58/0.87 cnf(73,plain, % 0.58/0.87 (~P3(f1(f2(x731)))+~P1(f2(x731))+~P3(f2(x731))), % 0.58/0.87 inference(scs_inference,[],[4,11])). % 0.58/0.87 cnf(74,plain, % 0.58/0.87 (~P1(f2(x741))+~P3(f2(x741))+~P2(f1(f2(x741)))), % 0.58/0.87 inference(scs_inference,[],[73,10])). % 0.58/0.87 cnf(75,plain, % 0.58/0.87 (~P3(f2(x751))+~P2(f1(f2(x751)))), % 0.58/0.87 inference(scs_inference,[],[74,3])). % 0.58/0.87 cnf(76,plain, % 0.58/0.87 (~P2(f1(f2(x761)))+~P3(f1(f2(x761)))), % 0.58/0.87 inference(scs_inference,[],[75,5])). % 0.58/0.87 cnf(88,plain, % 0.58/0.87 (P3(x881)+~P1(f1(f1(x881)))+P2(f1(f1(x881)))), % 0.58/0.87 inference(scs_inference,[],[5,7])). % 0.58/0.87 cnf(89,plain, % 0.58/0.87 (P2(f1(f1(x891)))+P3(x891)+P1(f1(x891))), % 0.58/0.87 inference(scs_inference,[],[88,1])). % 0.58/0.87 cnf(90,plain, % 0.58/0.87 (P2(f1(f1(x901)))+P3(f1(x901))+P1(f1(x901))), % 0.58/0.87 inference(scs_inference,[],[89,29])). % 0.58/0.87 cnf(91,plain, % 0.58/0.87 (P3(f1(x911))+P1(f1(x911))+~P2(x911)), % 0.58/0.87 inference(scs_inference,[],[90,61])). % 0.58/0.87 cnf(92,plain, % 0.58/0.87 (P3(f1(x921))+P1(f1(x921))), % 0.58/0.87 inference(scs_inference,[],[91,2])). % 0.58/0.87 cnf(93,plain, % 0.58/0.87 (P1(f1(f2(x931)))), % 0.58/0.87 inference(scs_inference,[],[92,36])). % 0.58/0.87 cnf(101,plain, % 0.58/0.87 (~P1(f2(x1011))+P2(f1(f2(x1011)))), % 0.58/0.87 inference(scs_inference,[],[93,8])). % 0.58/0.87 cnf(103,plain, % 0.58/0.87 (~P3(f1(f2(x1031)))+~P1(f2(x1031))), % 0.58/0.87 inference(scs_inference,[],[93,8,76])). % 0.58/0.87 cnf(112,plain, % 0.58/0.87 (~P1(f2(x1121))+~P2(f2(x1121))), % 0.58/0.87 inference(scs_inference,[],[93,9,5,103])). % 0.58/0.87 cnf(130,plain, % 0.58/0.87 (P2(f1(f1(x1301)))+P3(x1301)+P2(f1(x1301))), % 0.58/0.87 inference(scs_inference,[],[5,47])). % 0.58/0.87 cnf(131,plain, % 0.58/0.88 (P2(f1(x1311))+P3(x1311)), % 0.58/0.88 inference(scs_inference,[],[130,46])). % 0.58/0.88 cnf(134,plain, % 0.58/0.88 (P3(x1341)+P2(f1(f1(x1341)))), % 0.58/0.88 inference(scs_inference,[],[5,131])). % 0.58/0.88 cnf(135,plain, % 0.58/0.88 (P3(f1(x1351))+P3(x1351)+~P2(x1351)), % 0.58/0.88 inference(scs_inference,[],[134,61])). % 0.58/0.88 cnf(138,plain, % 0.58/0.88 (P3(x1381)+~P2(x1381)), % 0.58/0.88 inference(scs_inference,[],[5,135])). % 0.58/0.88 cnf(139,plain, % 0.58/0.88 (P1(x1391)+P3(f1(f1(x1391)))), % 0.58/0.88 inference(scs_inference,[],[138,59])). % 0.58/0.88 cnf(140,plain, % 0.58/0.88 (P1(x1401)+P2(f1(x1401))), % 0.58/0.88 inference(scs_inference,[],[139,4])). % 0.58/0.88 cnf(141,plain, % 0.58/0.88 (P1(x1411)), % 0.58/0.88 inference(scs_inference,[],[140,3])). % 0.58/0.88 cnf(143,plain, % 0.58/0.88 (P1(x1431)), % 0.58/0.88 inference(rename_variables,[],[141])). % 0.58/0.88 cnf(145,plain, % 0.58/0.88 (P1(x1451)), % 0.58/0.88 inference(rename_variables,[],[141])). % 0.58/0.88 cnf(148,plain, % 0.58/0.88 ($false), % 0.58/0.88 inference(scs_inference,[],[141,143,145,101,112,138,103]), % 0.58/0.88 ['proof']). % 0.58/0.88 % SZS output end Proof % 0.58/0.88 % Total time :0.250000s %------------------------------------------------------------------------------