%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COM003-2 : TPTP v8.2.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 : Unsatisfiable 0.53s 0.66s % Output : CNFRefutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : COM003-2 : TPTP v8.2.0. Released v1.1.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n022.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Thu Jun 20 23:36:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.47/0.56 start to proof:theBenchmark % 0.53/0.65 %------------------------------------------- % 0.53/0.65 % File :CSE---1.7 % 0.53/0.65 % Problem :theBenchmark % 0.53/0.65 % Transform :cnf % 0.53/0.65 % Format :tptp:raw % 0.53/0.65 % Command :java -jar mcs_scs.jar %d %s % 0.53/0.65 % 0.53/0.65 % Result :Theorem 0.050000s % 0.53/0.65 % Output :CNFRefutation 0.050000s % 0.53/0.65 %------------------------------------------- % 0.53/0.66 %-------------------------------------------------------------------------- % 0.53/0.66 % File : COM003-2 : TPTP v8.2.0. Released v1.1.0. % 0.53/0.66 % Domain : Computing Theory % 0.53/0.66 % Problem : The halting problem is undecidable % 0.53/0.66 % Version : [Bru91] axioms. % 0.53/0.66 % English : % 0.53/0.66 % 0.53/0.66 % Refs : [Bur87b] Burkholder (1987), A 76th Automated Theorem Proving Pr % 0.53/0.66 % : [Bru91] Brushi (1991), The Halting Problem % 0.53/0.66 % Source : [Bru91] % 0.53/0.66 % Names : - [Bru91] % 0.53/0.66 % 0.53/0.66 % Status : Unsatisfiable % 0.53/0.66 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v2.0.0 % 0.53/0.66 % Syntax : Number of clauses : 43 ( 1 unt; 2 nHn; 35 RR) % 0.53/0.66 % Number of literals : 109 ( 0 equ; 65 neg) % 0.53/0.66 % Maximal clause size : 5 ( 2 avg) % 0.53/0.66 % Maximal term depth : 2 ( 1 avg) % 0.53/0.66 % Number of predicates : 17 ( 17 usr; 0 prp; 1-4 aty) % 0.53/0.66 % Number of functors : 10 ( 10 usr; 6 con; 0-1 aty) % 0.53/0.66 % Number of variables : 103 ( 24 sgn) % 0.53/0.66 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.53/0.66 % 0.53/0.66 % Comments : % 0.53/0.66 %-------------------------------------------------------------------------- % 0.53/0.66 %----Definitions of the new predicates. % 0.53/0.66 % (all X (program_decides(X) <-> % 0.53/0.66 % (all Y (program(Y) -> (all Z decides(X,Y,Z)))))). % 0.53/0.66 cnf(program_decides1,axiom, % 0.53/0.66 ( ~ program_decides(X) % 0.53/0.66 | ~ program(Y) % 0.53/0.66 | decides(X,Y,Z) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_decides2,axiom, % 0.53/0.66 ( program_decides(X) % 0.53/0.66 | program(f2(X)) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_decides3,axiom, % 0.53/0.66 ( program_decides(X) % 0.53/0.66 | ~ decides(X,f2(X),f1(X)) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (program_program_decides(X) <-> % 0.53/0.66 % (program(X) & program_decides(X)))). % 0.53/0.66 cnf(program_program_decides1,axiom, % 0.53/0.66 ( ~ program_program_decides(X) % 0.53/0.66 | program(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_program_decides2,axiom, % 0.53/0.66 ( ~ program_program_decides(X) % 0.53/0.66 | program_decides(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_program_decides3,axiom, % 0.53/0.66 ( program_program_decides(X) % 0.53/0.66 | ~ program(X) % 0.53/0.66 | ~ program_decides(X) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (algorithm_program_decides(X) <-> % 0.53/0.66 % (algorithm(X) & program_decides(X)))). % 0.53/0.66 cnf(algorithm_program_decides1,axiom, % 0.53/0.66 ( ~ algorithm_program_decides(X) % 0.53/0.66 | algorithm(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(algorithm_program_decides2,axiom, % 0.53/0.66 ( ~ algorithm_program_decides(X) % 0.53/0.66 | program_decides(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(algorithm_program_decides3,axiom, % 0.53/0.66 ( algorithm_program_decides(X) % 0.53/0.66 | ~ algorithm(X) % 0.53/0.66 | ~ program_decides(X) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (program_halts2(X,Y) <-> % 0.53/0.66 % (program(X) & halts2(X,Y))))). % 0.53/0.66 cnf(program_halts1,axiom, % 0.53/0.66 ( ~ program_halts2(X,Y) % 0.53/0.66 | program(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts3a,axiom, % 0.53/0.66 ( ~ program_halts2(X,Y) % 0.53/0.66 | halts2(X,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts3b,axiom, % 0.53/0.66 ( program_halts2(X,Y) % 0.53/0.66 | ~ program(X) % 0.53/0.66 | ~ halts2(X,Y) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all Z (all W (halts3_outputs(X,Y,Z,W) <-> % 0.53/0.66 % (halts3(X,Y,Z) & outputs(X,W))))))). % 0.53/0.66 cnf(halts3_outputs1,axiom, % 0.53/0.66 ( ~ halts3_outputs(X,Y,Z,W) % 0.53/0.66 | halts3(X,Y,Z) ) ). % 0.53/0.66 % 0.53/0.66 cnf(halts3_outputs2,axiom, % 0.53/0.66 ( ~ halts3_outputs(X,Y,Z,W) % 0.53/0.66 | outputs(X,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(halts3_outputs3,axiom, % 0.53/0.66 ( halts3_outputs(X,Y,Z,W) % 0.53/0.66 | ~ halts3(X,Y,Z) % 0.53/0.66 | ~ outputs(X,W) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (program_not_halts2(X,Y) <-> % 0.53/0.66 % (program(X) & -halts2(X,Y))))). % 0.53/0.66 cnf(program_not_halts1,axiom, % 0.53/0.66 ( ~ program_not_halts2(X,Y) % 0.53/0.66 | program(X) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts3a,axiom, % 0.53/0.66 ( ~ program_not_halts2(X,Y) % 0.53/0.66 | ~ halts2(X,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts3b,axiom, % 0.53/0.66 ( program_not_halts2(X,Y) % 0.53/0.66 | ~ program(X) % 0.53/0.66 | halts2(X,Y) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all W (halts2_outputs(X,Y,W) <-> % 0.53/0.66 % (halts2(X,Y) & outputs(X,W)))))). % 0.53/0.66 cnf(halts2_outputs1,axiom, % 0.53/0.66 ( ~ halts2_outputs(X,Y,W) % 0.53/0.66 | halts2(X,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(halts2_outputs2,axiom, % 0.53/0.66 ( ~ halts2_outputs(X,Y,W) % 0.53/0.66 | outputs(X,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(halts2_outputs3,axiom, % 0.53/0.66 ( halts2_outputs(X,Y,W) % 0.53/0.66 | ~ halts2(X,Y) % 0.53/0.66 | ~ outputs(X,W) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all Z (all W (program_halts2_halts3_outputs(X,Y,Z,W) <-> % 0.53/0.66 % (program_halts2(Y,Z) & % 0.53/0.66 % halts3_outputs(X,Y,Z,W))))))). % 0.53/0.66 cnf(program_halts2_halts3_outputs1,axiom, % 0.53/0.66 ( ~ program_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | program_halts2(Y,Z) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts2_halts3_outputs2,axiom, % 0.53/0.66 ( ~ program_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | halts3_outputs(X,Y,Z,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts2_halts3_outputs3,axiom, % 0.53/0.66 ( program_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | ~ program_halts2(Y,Z) % 0.53/0.66 | ~ halts3_outputs(X,Y,Z,W) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all Z (all W (program_not_halts2_halts3_outputs(X,Y,Z,W) <-> % 0.53/0.66 % (program_not_halts2(Y,Z) & % 0.53/0.66 % halts3_outputs(X,Y,Z,W))))))). % 0.53/0.66 cnf(program_not_halts2_halts3_outputs1,axiom, % 0.53/0.66 ( ~ program_not_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | program_not_halts2(Y,Z) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts2_halts3_outputs2,axiom, % 0.53/0.66 ( ~ program_not_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | halts3_outputs(X,Y,Z,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts2_halts3_outputs3,axiom, % 0.53/0.66 ( program_not_halts2_halts3_outputs(X,Y,Z,W) % 0.53/0.66 | ~ program_not_halts2(Y,Z) % 0.53/0.66 | ~ halts3_outputs(X,Y,Z,W) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all W (program_halts2_halts2_outputs(X,Y,W) <-> % 0.53/0.66 % (program_halts2(Y,Y) & halts2_outputs(X,Y,W)))))). % 0.53/0.66 cnf(program_halts2_halts2_outputs1,axiom, % 0.53/0.66 ( ~ program_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | program_halts2(Y,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts2_halts2_outputs2,axiom, % 0.53/0.66 ( ~ program_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | halts2_outputs(X,Y,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_halts2_halts2_outputs3,axiom, % 0.53/0.66 ( program_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | ~ program_halts2(Y,Y) % 0.53/0.66 | ~ halts2_outputs(X,Y,W) ) ). % 0.53/0.66 % 0.53/0.66 % (all X (all Y (all W (program_not_halts2_halts2_outputs(X,Y,W) <-> % 0.53/0.66 % (program_not_halts2(Y,Y) & halts2_outputs(X,Y,W)))))). % 0.53/0.66 cnf(program_not_halts2_halts2_outputs1,axiom, % 0.53/0.66 ( ~ program_not_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | program_not_halts2(Y,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts2_halts2_outputs2,axiom, % 0.53/0.66 ( ~ program_not_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | halts2_outputs(X,Y,W) ) ). % 0.53/0.66 % 0.53/0.66 cnf(program_not_halts2_halts2_outputs3,axiom, % 0.53/0.66 ( program_not_halts2_halts2_outputs(X,Y,W) % 0.53/0.66 | ~ program_not_halts2(Y,Y) % 0.53/0.66 | ~ halts2_outputs(X,Y,W) ) ). % 0.53/0.66 % 0.53/0.66 % New verions of the original axioms % 0.53/0.66 % ((exists X algorithm_program_decides(X)) -> % 0.53/0.66 % (exists W program_program_decides(W))). % 0.53/0.66 cnf(axiom1_1,hypothesis, % 0.53/0.66 ( ~ algorithm_program_decides(X) % 0.53/0.66 | program_program_decides(c1) ) ). % 0.53/0.66 % 0.53/0.66 % (all W (program_program_decides(W) -> % 0.53/0.66 % (all Y (all Z (program_halts2_halts3_outputs(W,Y,Z,good) & % 0.53/0.66 % program_not_halts2_halts3_outputs(W,Y,Z,bad)))))). % 0.53/0.66 cnf(axiom2_1,hypothesis, % 0.53/0.66 ( ~ program_program_decides(W) % 0.53/0.66 | program_halts2_halts3_outputs(W,Y,Z,good) ) ). % 0.53/0.66 % 0.53/0.66 cnf(axiom2_2,hypothesis, % 0.53/0.66 ( ~ program_program_decides(W) % 0.53/0.66 | program_not_halts2_halts3_outputs(W,Y,Z,bad) ) ). % 0.53/0.66 % 0.53/0.66 % ((exists W (program(W) & % 0.53/0.66 % (all Y (program_halts2_halts3_outputs(W,Y,Y,good) & % 0.53/0.66 % program_not_halts2_halts3_outputs(W,Y,Y,bad))))) -> % 0.53/0.66 % (exists V (program(V) & % 0.53/0.66 % (all Y (program_halts2_halts2_outputs(V,Y,good) & % 0.53/0.66 % program_not_halts2_halts2_outputs(V,Y,bad)))))). % 0.53/0.66 cnf(axiom3_1,hypothesis, % 0.53/0.66 ( ~ program(W) % 0.53/0.66 | ~ program_halts2_halts3_outputs(W,f3(W),f3(W),good) % 0.53/0.66 | ~ program_not_halts2_halts3_outputs(W,f3(W),f3(W),bad) % 0.53/0.66 | program(c2) ) ). % 0.53/0.66 % 0.53/0.66 cnf(axiom3_2,hypothesis, % 0.53/0.66 ( ~ program(W) % 0.53/0.66 | ~ program_halts2_halts3_outputs(W,f3(W),f3(W),good) % 0.53/0.66 | ~ program_not_halts2_halts3_outputs(W,f3(W),f3(W),bad) % 0.53/0.66 | program_halts2_halts2_outputs(c2,Y,good) ) ). % 0.53/0.66 % 0.53/0.66 cnf(axiom3_3,hypothesis, % 0.53/0.66 ( ~ program(W) % 0.53/0.66 | ~ program_halts2_halts3_outputs(W,f3(W),f3(W),good) % 0.53/0.66 | ~ program_not_halts2_halts3_outputs(W,f3(W),f3(W),bad) % 0.53/0.66 | program_not_halts2_halts2_outputs(c2,Y,bad) ) ). % 0.53/0.66 % 0.53/0.66 % ((exists V (program(V) & % 0.53/0.66 % (all Y (program_halts2_halts2_outputs(V,Y,good) & % 0.53/0.66 % program_not_halts2_halts2_outputs(V,Y,bad))))) -> % 0.53/0.66 % (exists U (program(U) & % 0.53/0.66 % (all Y ((program_halts2(Y,Y) -> halts2(U,Y)) & % 0.53/0.66 % program_not_halts2_halts2_outputs(U,Y,bad)))))). % 0.53/0.66 cnf(axiom4_1,hypothesis, % 0.53/0.66 ( ~ program(V) % 0.53/0.66 | ~ program_halts2_halts2_outputs(V,f4(V),good) % 0.53/0.66 | ~ program_not_halts2_halts2_outputs(V,f4(V),bad) % 0.53/0.66 | program(c3) ) ). % 0.53/0.66 % 0.53/0.66 cnf(axiom4_2,hypothesis, % 0.53/0.66 ( ~ program(V) % 0.53/0.66 | ~ program_halts2_halts2_outputs(V,f4(V),good) % 0.53/0.66 | ~ program_not_halts2_halts2_outputs(V,f4(V),bad) % 0.53/0.66 | ~ program_halts2(Y,Y) % 0.53/0.66 | halts2(c3,Y) ) ). % 0.53/0.66 % 0.53/0.66 cnf(axiom4_3,hypothesis, % 0.53/0.66 ( ~ program(V) % 0.53/0.66 | ~ program_halts2_halts2_outputs(V,f4(V),good) % 0.53/0.66 | ~ program_not_halts2_halts2_outputs(V,f4(V),bad) % 0.53/0.66 | program_not_halts2_halts2_outputs(c3,Y,bad) ) ). % 0.53/0.66 % 0.53/0.66 %--- Prove -(exists X algorithm_program_decides(X)). % 0.53/0.66 cnf(prove_algorithm_does_not_exist,negated_conjecture, % 0.53/0.66 algorithm_program_decides(c4) ). % 0.53/0.66 % 0.53/0.66 %-------------------------------------------------------------------------- % 0.53/0.66 %------------------------------------------- % 0.53/0.66 % Proof found % 0.53/0.66 % SZS status Theorem for theBenchmark % 0.53/0.66 % SZS output start Proof % 0.53/0.66 %ClaNum:43(EqnAxiom:0) % 0.53/0.66 %VarNum:225(SingletonVarNum:103) % 0.53/0.66 %MaxLitNum:5 % 0.53/0.66 %MaxfuncDepth:1 % 0.53/0.66 %SharedTerms:10 % 0.53/0.66 %goalClause: 1 % 0.53/0.66 %singleGoalClaCount:1 % 0.53/0.66 [1]P1(a1) % 0.53/0.66 [2]~P1(x21)+P3(a2) % 0.53/0.66 [3]~P3(x31)+P4(x31) % 0.53/0.67 [4]~P1(x41)+P4(x41) % 0.53/0.67 [5]~P3(x51)+P5(x51) % 0.53/0.67 [6]~P1(x61)+P2(x61) % 0.53/0.67 [7]P4(x71)+P5(f6(x71)) % 0.53/0.67 [22]P4(x221)+~P7(x221,f6(x221),f7(x221)) % 0.53/0.67 [10]P5(x101)+~P12(x101,x102) % 0.53/0.67 [11]P5(x111)+~P13(x111,x112) % 0.53/0.67 [13]~P12(x131,x132)+P6(x131,x132) % 0.53/0.67 [15]~P13(x151,x152)+~P6(x151,x152) % 0.53/0.67 [18]P12(x181,x181)+~P14(x182,x181,x183) % 0.53/0.67 [19]P6(x191,x192)+~P8(x191,x192,x193) % 0.53/0.67 [20]P9(x201,x202)+~P8(x201,x203,x202) % 0.53/0.67 [21]P13(x211,x211)+~P16(x212,x211,x213) % 0.53/0.67 [23]~P14(x231,x232,x233)+P8(x231,x232,x233) % 0.53/0.67 [24]~P16(x241,x242,x243)+P8(x241,x242,x243) % 0.53/0.67 [30]~P3(x301)+P15(x301,x302,x303,a10) % 0.53/0.67 [31]~P3(x311)+P17(x311,x312,x313,a3) % 0.53/0.67 [33]P12(x331,x332)+~P15(x333,x331,x332,x334) % 0.53/0.67 [34]P9(x341,x342)+~P10(x341,x343,x344,x342) % 0.53/0.67 [35]P13(x351,x352)+~P17(x353,x351,x352,x354) % 0.53/0.67 [36]P11(x361,x362,x363)+~P10(x361,x362,x363,x364) % 0.53/0.67 [37]~P15(x371,x372,x373,x374)+P10(x371,x372,x373,x374) % 0.53/0.67 [38]~P17(x381,x382,x383,x384)+P10(x381,x382,x383,x384) % 0.53/0.67 [8]~P4(x81)+~P5(x81)+P3(x81) % 0.53/0.67 [9]~P4(x91)+~P2(x91)+P1(x91) % 0.53/0.67 [12]P13(x121,x122)+~P5(x121)+P6(x121,x122) % 0.53/0.67 [14]~P5(x141)+~P6(x141,x142)+P12(x141,x142) % 0.53/0.67 [16]~P4(x161)+~P5(x162)+P7(x161,x162,x163) % 0.53/0.67 [17]~P6(x171,x172)+~P9(x171,x173)+P8(x171,x172,x173) % 0.53/0.67 [25]~P12(x252,x252)+~P8(x251,x252,x253)+P14(x251,x252,x253) % 0.53/0.67 [26]~P13(x262,x262)+~P8(x261,x262,x263)+P16(x261,x262,x263) % 0.53/0.67 [32]~P9(x321,x324)+~P11(x321,x322,x323)+P10(x321,x322,x323,x324) % 0.53/0.67 [39]~P12(x392,x393)+~P10(x391,x392,x393,x394)+P15(x391,x392,x393,x394) % 0.53/0.67 [40]~P13(x402,x403)+~P10(x401,x402,x403,x404)+P17(x401,x402,x403,x404) % 0.53/0.67 [27]~P5(x271)+~P14(x271,f8(x271),a10)+~P16(x271,f8(x271),a3)+P5(a4) % 0.53/0.67 [41]~P5(x411)+~P15(x411,f9(x411),f9(x411),a10)+~P17(x411,f9(x411),f9(x411),a3)+P5(a5) % 0.53/0.67 [29]~P5(x292)+~P14(x292,f8(x292),a10)+~P16(x292,f8(x292),a3)+P16(a4,x291,a3) % 0.53/0.67 [42]~P5(x422)+~P15(x422,f9(x422),f9(x422),a10)+~P17(x422,f9(x422),f9(x422),a3)+P14(a5,x421,a10) % 0.53/0.67 [43]~P5(x432)+~P15(x432,f9(x432),f9(x432),a10)+~P17(x432,f9(x432),f9(x432),a3)+P16(a5,x431,a3) % 0.53/0.67 [28]~P12(x281,x281)+~P5(x282)+P6(a4,x281)+~P14(x282,f8(x282),a10)+~P16(x282,f8(x282),a3) % 0.53/0.67 %EqnAxiom % 0.53/0.67 % 0.53/0.67 %------------------------------------------- % 0.53/0.67 cnf(44,plain, % 0.53/0.67 (P3(a2)), % 0.53/0.67 inference(scs_inference,[],[1,2])). % 0.53/0.67 cnf(54,plain, % 0.53/0.67 (~P12(x541,x542)+~P13(x541,x542)), % 0.53/0.67 inference(scs_inference,[],[13,15])). % 0.53/0.67 cnf(57,plain, % 0.53/0.67 (~P12(x571,x572)+~P17(x573,x571,x572,x574)), % 0.53/0.67 inference(scs_inference,[],[54,35])). % 0.53/0.67 cnf(70,plain, % 0.53/0.67 (~P15(x701,x702,x703,x704)+~P17(x705,x702,x703,x706)), % 0.53/0.67 inference(scs_inference,[],[33,57])). % 0.53/0.67 cnf(80,plain, % 0.53/0.67 (~P17(x801,x802,x803,x804)), % 0.53/0.67 inference(scs_inference,[],[44,70,30])). % 0.53/0.67 cnf(82,plain, % 0.53/0.67 ($false), % 0.53/0.67 inference(scs_inference,[],[44,80,31]), % 0.53/0.67 ['proof']). % 0.53/0.67 % SZS output end Proof % 0.53/0.67 % Total time :0.050000s %------------------------------------------------------------------------------