%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM003+2 : TPTP v8.2.0. Bugfixed v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 04:52:42 EDT 2024 % Result : Theorem 71.90s 72.19s % Output : CNFRefutation 72.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM003+2 : TPTP v8.2.0. Bugfixed v2.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Jun 21 00:17:39 EDT 2024 % 0.13/0.33 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 71.90/72.17 %------------------------------------------- % 71.90/72.17 % File :CSE---1.7 % 71.90/72.17 % Problem :theBenchmark % 71.90/72.17 % Transform :cnf % 71.90/72.17 % Format :tptp:raw % 71.90/72.17 % Command :java -jar mcs_scs.jar %d %s % 71.90/72.17 % 71.90/72.17 % Result :Theorem 71.320000s % 71.90/72.17 % Output :CNFRefutation 71.320000s % 71.90/72.17 %------------------------------------------- % 71.90/72.18 %-------------------------------------------------------------------------- % 71.90/72.18 % File : COM003+2 : TPTP v8.2.0. Bugfixed v2.2.0. % 71.90/72.18 % Domain : Computing Theory % 71.90/72.18 % Problem : The halting problem is undecidable % 71.90/72.18 % Version : [Bru91] axioms. % 71.90/72.18 % English : % 71.90/72.18 % 71.90/72.18 % Refs : [Gan98] Ganzinger (1998), Email to Geoff Sutcliffe % 71.90/72.18 % : [Bur87b] Burkholder (1987), A 76th Automated Theorem Proving Pr % 71.90/72.18 % : [Bru91] Brushi (1991), The Halting Problem % 71.90/72.18 % Source : [Bru91] % 71.90/72.18 % Names : - [Bru91] % 71.90/72.18 % 71.90/72.18 % Status : Theorem % 71.90/72.18 % Rating : 0.06 v8.2.0, 0.07 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.12 v6.0.0, 0.50 v5.5.0, 0.21 v5.4.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.14 v5.0.0, 0.10 v4.1.0, 0.06 v4.0.1, 0.11 v4.0.0, 0.10 v3.7.0, 0.33 v3.5.0, 0.12 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1 % 71.90/72.18 % Syntax : Number of formulae : 16 ( 1 unt; 0 def) % 71.90/72.18 % Number of atoms : 52 ( 0 equ) % 71.90/72.18 % Maximal formula atoms : 7 ( 3 avg) % 71.90/72.18 % Number of connectives : 39 ( 3 ~; 0 |; 15 &) % 71.90/72.18 % ( 11 <=>; 10 =>; 0 <=; 0 <~>) % 71.90/72.18 % Maximal formula depth : 8 ( 6 avg) % 71.90/72.18 % Maximal term depth : 1 ( 1 avg) % 71.90/72.18 % Number of predicates : 17 ( 17 usr; 0 prp; 1-4 aty) % 71.90/72.18 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 71.90/72.18 % Number of variables : 44 ( 37 !; 7 ?) % 71.90/72.18 % SPC : FOF_THM_RFO_NEQ % 71.90/72.18 % 71.90/72.18 % Comments : % 71.90/72.18 % Bugfixes : v2.2.0 - Clauses program_halts2_halts3_outputs_def, program_ % 71.90/72.18 % not_halts2_halts3_outputs_def, program_halts2_halts2_outputs_ % 71.90/72.18 % def, program_not_halts2_halts2_outputs_def, p4 by [Gan98]. % 71.90/72.18 %-------------------------------------------------------------------------- % 71.90/72.18 fof(program_decides_def,axiom, % 71.90/72.18 ! [X] : % 71.90/72.18 ( program_decides(X) % 71.90/72.18 <=> ! [Y] : % 71.90/72.18 ( program(Y) % 71.90/72.18 => ! [Z] : decides(X,Y,Z) ) ) ). % 71.90/72.18 % 71.90/72.18 fof(program_program_decides_def,axiom, % 71.90/72.18 ! [X] : % 71.90/72.18 ( program_program_decides(X) % 71.90/72.18 <=> ( program(X) % 71.90/72.18 & program_decides(X) ) ) ). % 71.90/72.18 % 71.90/72.18 fof(algorithm_program_decides_def,axiom, % 71.90/72.18 ! [X] : % 71.90/72.18 ( algorithm_program_decides(X) % 71.90/72.18 <=> ( algorithm(X) % 71.90/72.18 & program_decides(X) ) ) ). % 71.90/72.18 % 71.90/72.18 fof(program_halts2_def,axiom, % 71.90/72.18 ! [X,Y] : % 71.90/72.18 ( program_halts2(X,Y) % 71.90/72.18 <=> ( program(X) % 71.90/72.18 & halts2(X,Y) ) ) ). % 71.90/72.18 % 71.90/72.18 fof(halts3_outputs_def,axiom, % 71.90/72.18 ! [X,Y,Z,W] : % 71.90/72.19 ( halts3_outputs(X,Y,Z,W) % 71.90/72.19 <=> ( halts3(X,Y,Z) % 71.90/72.19 & outputs(X,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(program_not_halts2_def,axiom, % 71.90/72.19 ! [X,Y] : % 71.90/72.19 ( program_not_halts2(X,Y) % 71.90/72.19 <=> ( program(X) % 71.90/72.19 & ~ halts2(X,Y) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(halts2_outputs_def,axiom, % 71.90/72.19 ! [X,Y,W] : % 71.90/72.19 ( halts2_outputs(X,Y,W) % 71.90/72.19 <=> ( halts2(X,Y) % 71.90/72.19 & outputs(X,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(program_halts2_halts3_outputs_def,axiom, % 71.90/72.19 ! [X,Y,Z,W] : % 71.90/72.19 ( program_halts2_halts3_outputs(X,Y,Z,W) % 71.90/72.19 <=> ( program_halts2(Y,Z) % 71.90/72.19 => halts3_outputs(X,Y,Z,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(program_not_halts2_halts3_outputs_def,axiom, % 71.90/72.19 ! [X,Y,Z,W] : % 71.90/72.19 ( program_not_halts2_halts3_outputs(X,Y,Z,W) % 71.90/72.19 <=> ( program_not_halts2(Y,Z) % 71.90/72.19 => halts3_outputs(X,Y,Z,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(program_halts2_halts2_outputs_def,axiom, % 71.90/72.19 ! [X,Y,W] : % 71.90/72.19 ( program_halts2_halts2_outputs(X,Y,W) % 71.90/72.19 <=> ( program_halts2(Y,Y) % 71.90/72.19 => halts2_outputs(X,Y,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(program_not_halts2_halts2_outputs_def,axiom, % 71.90/72.19 ! [X,Y,W] : % 71.90/72.19 ( program_not_halts2_halts2_outputs(X,Y,W) % 71.90/72.19 <=> ( program_not_halts2(Y,Y) % 71.90/72.19 => halts2_outputs(X,Y,W) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(p1,axiom, % 71.90/72.19 ( ? [X] : algorithm_program_decides(X) % 71.90/72.19 => ? [W] : program_program_decides(W) ) ). % 71.90/72.19 % 71.90/72.19 fof(p2,axiom, % 71.90/72.19 ! [W] : % 71.90/72.19 ( program_program_decides(W) % 71.90/72.19 => ! [Y,Z] : % 71.90/72.19 ( program_halts2_halts3_outputs(W,Y,Z,good) % 71.90/72.19 & program_not_halts2_halts3_outputs(W,Y,Z,bad) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(p3,axiom, % 71.90/72.19 ( ? [W] : % 71.90/72.19 ( program(W) % 71.90/72.19 & ! [Y] : % 71.90/72.19 ( program_halts2_halts3_outputs(W,Y,Y,good) % 71.90/72.19 & program_not_halts2_halts3_outputs(W,Y,Y,bad) ) ) % 71.90/72.19 => ? [V] : % 71.90/72.19 ( program(V) % 71.90/72.19 & ! [Y] : % 71.90/72.19 ( program_halts2_halts2_outputs(V,Y,good) % 71.90/72.19 & program_not_halts2_halts2_outputs(V,Y,bad) ) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(p4,axiom, % 71.90/72.19 ( ? [V] : % 71.90/72.19 ( program(V) % 71.90/72.19 & ! [Y] : % 71.90/72.19 ( program_halts2_halts2_outputs(V,Y,good) % 71.90/72.19 & program_not_halts2_halts2_outputs(V,Y,bad) ) ) % 71.90/72.19 => ? [U] : % 71.90/72.19 ( program(U) % 71.90/72.19 & ! [Y] : % 71.90/72.19 ( ( program_halts2(Y,Y) % 71.90/72.19 => ~ halts2(U,Y) ) % 71.90/72.19 & program_not_halts2_halts2_outputs(U,Y,good) ) ) ) ). % 71.90/72.19 % 71.90/72.19 fof(prove_this,conjecture, % 71.90/72.19 ~ ? [X] : algorithm_program_decides(X) ). % 71.90/72.19 % 71.90/72.19 %-------------------------------------------------------------------------- % 71.90/72.19 %------------------------------------------- % 71.90/72.19 % Proof found % 71.90/72.19 % SZS status Theorem for theBenchmark % 71.90/72.19 % SZS output start Proof % 71.90/72.19 %ClaNum:43(EqnAxiom:0) % 71.90/72.19 %VarNum:225(SingletonVarNum:103) % 71.90/72.19 %MaxLitNum:5 % 71.90/72.19 %MaxfuncDepth:1 % 71.90/72.19 %SharedTerms:10 % 71.90/72.19 %goalClause: 1 % 71.90/72.19 %singleGoalClaCount:1 % 71.90/72.19 [1]P1(a1) % 71.90/72.20 [2]~P1(x21)+P3(a3) % 71.90/72.20 [3]~P3(x31)+P4(x31) % 71.90/72.20 [4]~P1(x41)+P4(x41) % 71.90/72.20 [5]~P3(x51)+P5(x51) % 71.90/72.20 [6]~P1(x61)+P2(x61) % 71.90/72.20 [7]P4(x71)+P5(f4(x71)) % 71.90/72.20 [22]P4(x221)+~P7(x221,f4(x221),f5(x221)) % 71.90/72.20 [10]P5(x101)+~P12(x101,x102) % 71.90/72.20 [11]P5(x111)+~P13(x111,x112) % 71.90/72.20 [13]~P12(x131,x132)+P6(x131,x132) % 71.90/72.20 [15]~P13(x151,x152)+~P6(x151,x152) % 71.90/72.20 [17]P12(x171,x171)+P14(x172,x171,x173) % 71.90/72.20 [18]P13(x181,x181)+P16(x182,x181,x183) % 71.90/72.20 [20]P6(x201,x202)+~P8(x201,x202,x203) % 71.90/72.20 [21]P9(x211,x212)+~P8(x211,x213,x212) % 71.90/72.20 [23]~P8(x231,x232,x233)+P14(x231,x232,x233) % 71.90/72.20 [24]~P8(x241,x242,x243)+P16(x241,x242,x243) % 71.90/72.20 [30]~P3(x301)+P15(x301,x302,x303,a12) % 71.90/72.20 [31]~P3(x311)+P17(x311,x312,x313,a2) % 71.90/72.20 [32]P12(x321,x322)+P15(x323,x321,x322,x324) % 71.90/72.20 [33]P13(x331,x332)+P17(x333,x331,x332,x334) % 71.90/72.20 [35]P9(x351,x352)+~P10(x351,x353,x354,x352) % 71.90/72.20 [36]P11(x361,x362,x363)+~P10(x361,x362,x363,x364) % 71.90/72.20 [37]~P10(x371,x372,x373,x374)+P15(x371,x372,x373,x374) % 71.90/72.20 [38]~P10(x381,x382,x383,x384)+P17(x381,x382,x383,x384) % 71.90/72.20 [8]~P4(x81)+~P5(x81)+P3(x81) % 71.90/72.20 [9]~P4(x91)+~P2(x91)+P1(x91) % 71.90/72.20 [12]P13(x121,x122)+~P5(x121)+P6(x121,x122) % 71.90/72.20 [14]~P5(x141)+~P6(x141,x142)+P12(x141,x142) % 71.90/72.20 [16]~P4(x161)+~P5(x162)+P7(x161,x162,x163) % 71.90/72.20 [19]~P6(x191,x192)+~P9(x191,x193)+P8(x191,x192,x193) % 71.90/72.20 [25]~P12(x252,x252)+~P14(x251,x252,x253)+P8(x251,x252,x253) % 71.90/72.20 [26]~P13(x262,x262)+~P16(x261,x262,x263)+P8(x261,x262,x263) % 71.90/72.20 [34]~P9(x341,x344)+~P11(x341,x342,x343)+P10(x341,x342,x343,x344) % 71.90/72.20 [39]~P12(x392,x393)+~P15(x391,x392,x393,x394)+P10(x391,x392,x393,x394) % 71.90/72.20 [40]~P13(x402,x403)+~P17(x401,x402,x403,x404)+P10(x401,x402,x403,x404) % 71.90/72.20 [27]~P5(x271)+~P14(x271,f7(x271),a12)+~P16(x271,f11(x271),a2)+P5(a6) % 71.90/72.20 [41]~P5(x411)+~P15(x411,f9(x411),f9(x411),a12)+~P17(x411,f10(x411),f10(x411),a2)+P5(a8) % 71.90/72.20 [29]~P5(x292)+~P14(x292,f7(x292),a12)+~P16(x292,f11(x292),a2)+P16(a6,x291,a12) % 71.90/72.20 [42]~P5(x422)+~P15(x422,f9(x422),f9(x422),a12)+~P17(x422,f10(x422),f10(x422),a2)+P14(a8,x421,a12) % 71.90/72.20 [43]~P5(x432)+~P15(x432,f9(x432),f9(x432),a12)+~P17(x432,f10(x432),f10(x432),a2)+P16(a8,x431,a2) % 71.90/72.20 [28]~P5(x281)+~P12(x282,x282)+~P6(a6,x282)+~P14(x281,f7(x281),a12)+~P16(x281,f11(x281),a2) % 71.90/72.20 %EqnAxiom % 71.90/72.20 % 71.90/72.20 %------------------------------------------- % 72.01/72.30 cnf(44,plain, % 72.01/72.30 (P3(a3)), % 72.01/72.30 inference(scs_inference,[],[1,2])). % 72.01/72.30 cnf(54,plain, % 72.01/72.30 (~P12(x541,x542)+~P13(x541,x542)), % 72.01/72.30 inference(scs_inference,[],[13,15])). % 72.01/72.31 cnf(60,plain, % 72.01/72.31 (~P8(x601,x602,x603)+~P13(x601,x602)), % 72.01/72.31 inference(scs_inference,[],[20,15])). % 72.01/72.31 cnf(76,plain, % 72.01/72.31 (P7(a3,x761,x762)+~P5(x761)), % 72.01/72.31 inference(scs_inference,[],[44,16,3])). % 72.01/72.31 cnf(102,plain, % 72.01/72.31 (~P15(a3,f9(a3),f9(a3),a12)+~P17(a3,f10(a3),f10(a3),a2)+P5(a8)), % 72.01/72.31 inference(scs_inference,[],[44,41,5])). % 72.01/72.31 cnf(103,plain, % 72.01/72.31 (~P17(a3,f10(a3),f10(a3),a2)+P5(a8)), % 72.01/72.31 inference(scs_inference,[],[44,102,30])). % 72.01/72.31 cnf(104,plain, % 72.01/72.31 (P5(a8)), % 72.01/72.31 inference(scs_inference,[],[44,103,31])). % 72.01/72.31 cnf(125,plain, % 72.01/72.31 (~P15(a3,f9(a3),f9(a3),a12)+~P17(a3,f10(a3),f10(a3),a2)+P14(a8,x1251,a12)), % 72.01/72.31 inference(scs_inference,[],[44,42,5])). % 72.01/72.31 cnf(126,plain, % 72.01/72.31 (~P17(a3,f10(a3),f10(a3),a2)+P14(a8,x1261,a12)), % 72.01/72.31 inference(scs_inference,[],[44,125,30])). % 72.01/72.31 cnf(127,plain, % 72.01/72.31 (P14(a8,x1271,a12)), % 72.01/72.31 inference(scs_inference,[],[44,126,31])). % 72.01/72.31 cnf(128,plain, % 72.01/72.31 (~P16(a8,f11(a8),a2)+P16(a6,x1281,a12)), % 72.01/72.31 inference(scs_inference,[],[104,127,29])). % 72.01/72.31 cnf(392,plain, % 72.01/72.31 (~P15(a3,f9(a3),f9(a3),a12)+~P17(a3,f10(a3),f10(a3),a2)+P16(a8,x3921,a2)), % 72.01/72.31 inference(scs_inference,[],[44,43,5])). % 72.01/72.31 cnf(423,plain, % 72.01/72.31 (~P17(a3,f10(a3),f10(a3),a2)+P16(a8,x4231,a2)), % 72.01/72.31 inference(scs_inference,[],[44,392,30])). % 72.01/72.31 cnf(454,plain, % 72.01/72.31 (P16(a8,x4541,a2)), % 72.01/72.31 inference(scs_inference,[],[44,423,31])). % 72.01/72.31 cnf(455,plain, % 72.01/72.31 (P16(a6,x4551,a12)), % 72.01/72.31 inference(scs_inference,[],[454,128])). % 72.01/72.31 cnf(3537,plain, % 72.01/72.31 (P4(a3)), % 72.01/72.31 inference(scs_inference,[],[44,3])). % 72.01/72.31 cnf(3549,plain, % 72.01/72.31 (P5(a3)), % 72.01/72.31 inference(scs_inference,[],[44,3537,104,16,5])). % 72.01/72.31 cnf(3551,plain, % 72.01/72.31 (P8(a6,x35511,a12)+~P13(x35511,x35511)), % 72.01/72.31 inference(scs_inference,[],[455,44,3537,104,16,5,26])). % 72.01/72.31 cnf(3560,plain, % 72.01/72.31 (P8(a8,x35601,a2)+~P13(x35601,x35601)), % 72.01/72.31 inference(scs_inference,[],[3537,3549,454,16,26])). % 72.01/72.31 cnf(90082,plain, % 72.01/72.31 (P15(a3,x900821,x900822,a12)), % 72.01/72.31 inference(scs_inference,[],[104,44,76,30])). % 72.01/72.31 cnf(90084,plain, % 72.01/72.31 (P17(a3,x900841,x900842,a2)), % 72.01/72.31 inference(scs_inference,[],[104,44,76,30,31])). % 72.01/72.31 cnf(90088,plain, % 72.01/72.31 (P5(a6)), % 72.01/72.31 inference(scs_inference,[],[1,454,104,127,44,76,30,31,4,27])). % 72.01/72.31 cnf(90109,plain, % 72.01/72.31 (P10(a3,x901091,x901092,a2)+~P13(x901091,x901092)), % 72.01/72.31 inference(scs_inference,[],[90082,90084,90088,76,39,40])). % 72.01/72.31 cnf(90120,plain, % 72.01/72.31 (P12(a6,x901201)+~P6(a6,x901201)), % 72.01/72.31 inference(scs_inference,[],[90088,76,14])). % 72.01/72.31 cnf(90271,plain, % 72.01/72.31 (~P8(a6,x902711,x902712)+P12(a6,x902711)), % 72.01/72.31 inference(scs_inference,[],[90120,20])). % 72.01/72.31 cnf(90653,plain, % 72.01/72.31 (~P13(x906531,x906531)+P12(a6,x906531)), % 72.01/72.31 inference(scs_inference,[],[90271,3551])). % 72.01/72.31 cnf(97202,plain, % 72.01/72.31 (P14(a8,x972021,a12)), % 72.01/72.31 inference(rename_variables,[],[127])). % 72.01/72.31 cnf(97206,plain, % 72.01/72.31 (P13(a6,a6)), % 72.01/72.31 inference(scs_inference,[],[455,454,127,97202,104,90088,12,14,25,28])). % 72.01/72.31 cnf(97221,plain, % 72.01/72.31 ($false), % 72.01/72.31 inference(scs_inference,[],[97206,90109,3560,54,20,21,60,90653]), % 72.01/72.31 ['proof']). % 72.15/72.41 % SZS output end Proof % 72.15/72.41 % Total time :71.320000s %------------------------------------------------------------------------------