%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SYN917+1 : TPTP v9.3.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Sun Sep 27 09:34:19 AM UTC 2026 % Result : Theorem 15.41s 3.01s % Output : CNFRefutation 15.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SYN917+1 : TPTP v9.3.1. Released v3.1.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.37 % Computer : n006.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Sat Sep 26 18:49:40 UTC 2026 % 0.09/0.37 % CPUTime : % 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 15.41/3.01 % SZS status Theorem for theBenchmark.p % 15.41/3.01 % SZS output start CNFRefutation for theBenchmark.p % 15.41/3.01 fof(prove_this, conjecture, (((! [X0] : ((((f(X0) & g(X0)) => h(X0)) => ? [X1] : ((f(X1) & ~g(X1))))) & (! [X2] : ((f(X2) => g(X2))) | ! [X3] : ((f(X3) => h(X3))))) => (! [X4] : (((f(X4) & h(X4)) => g(X4))) => ? [X5] : ((f(X5) & (g(X5) & ~h(X5)))))) & (((! [X0] : ! [X1] : ((r(X0,X1) => r(X1,X0))) & ! [X0] : ! [X1] : ! [X3] : (((r(X0,X1) & r(X1,X3)) => r(X0,X3)))) => ! [X0] : ! [X1] : ((r(X0,X1) => r(X0,X0)))) & ((((! [X0] : (((f(X0) & g(X0)) => h(X0))) => ? [X0] : ((f(X0) & ~g(X0)))) & (! [X2] : ((f(X2) => g(X2))) | ! [X3] : ((f(X3) => h(X3))))) => (! [X4] : (((f(X4) & h(X4)) => g(X4))) => ? [X5] : ((f(X5) & (g(X5) & ~h(X5)))))) & (? [X0] : ! [X1] : (((p(X1) => q(X0)) => (p(X0) => q(X0)))) & ((! [X0] : ((p(X0) & q(X0))) <=> (! [X0] : p(X0) & ! [X0] : q(X0))) & (((! [X0] : p(X0) | ! [X0] : q(X0)) => ! [X0] : ((p(X0) | q(X0)))) & ((? [X0] : ((p(X0) | q(X0))) <=> (? [X0] : p(X0) | ? [X0] : q(X0))) & (? [X1] : ((p(X1) => ! [X0] : p(X0))) & ((? [X0] : ((p(X0) & q(X0))) => (? [X0] : p(X0) & ? [X0] : q(X0))) & (! [X1] : ((! [X0] : p(X0) => p(X1))) & ((! [X0] : p(X0) => ? [X0] : p(X0)) & ((~? [X1] : p(X1) => ! [X1] : ((? [X0] : p(X0) => p(X1)))) & ((! [X0] : ((p(X0) | c)) <=> (! [X0] : p(X0) | c)) & ((? [X0] : ((p(X0) & c)) <=> (? [X0] : p(X0) & c)) & ((? [X0] : c <=> c) & ((! [X0] : c <=> c) & ((? [X0] : ((c => p(X0))) <=> (c => ? [X0] : p(X0))) & ((? [X0] : ((p(X0) => c)) <=> (! [X0] : p(X0) => c)) & ((! [X0] : ((c => p(X0))) <=> (c => ! [X0] : p(X0))) & (! [X0] : ((p(X0) => c)) <=> (? [X0] : p(X0) => c)))))))))))))))))))))). % 15.41/3.01 fof(negated_conjecture, negated_conjecture, ~((((! [X0] : ((((f(X0) & g(X0)) => h(X0)) => ? [X1] : ((f(X1) & ~g(X1))))) & (! [X2] : ((f(X2) => g(X2))) | ! [X3] : ((f(X3) => h(X3))))) => (! [X4] : (((f(X4) & h(X4)) => g(X4))) => ? [X5] : ((f(X5) & (g(X5) & ~h(X5)))))) & (((! [X0] : ! [X1] : ((r(X0,X1) => r(X1,X0))) & ! [X0] : ! [X1] : ! [X3] : (((r(X0,X1) & r(X1,X3)) => r(X0,X3)))) => ! [X0] : ! [X1] : ((r(X0,X1) => r(X0,X0)))) & ((((! [X0] : (((f(X0) & g(X0)) => h(X0))) => ? [X0] : ((f(X0) & ~g(X0)))) & (! [X2] : ((f(X2) => g(X2))) | ! [X3] : ((f(X3) => h(X3))))) => (! [X4] : (((f(X4) & h(X4)) => g(X4))) => ? [X5] : ((f(X5) & (g(X5) & ~h(X5)))))) & (? [X0] : ! [X1] : (((p(X1) => q(X0)) => (p(X0) => q(X0)))) & ((! [X0] : ((p(X0) & q(X0))) <=> (! [X0] : p(X0) & ! [X0] : q(X0))) & (((! [X0] : p(X0) | ! [X0] : q(X0)) => ! [X0] : ((p(X0) | q(X0)))) & ((? [X0] : ((p(X0) | q(X0))) <=> (? [X0] : p(X0) | ? [X0] : q(X0))) & (? [X1] : ((p(X1) => ! [X0] : p(X0))) & ((? [X0] : ((p(X0) & q(X0))) => (? [X0] : p(X0) & ? [X0] : q(X0))) & (! [X1] : ((! [X0] : p(X0) => p(X1))) & ((! [X0] : p(X0) => ? [X0] : p(X0)) & ((~? [X1] : p(X1) => ! [X1] : ((? [X0] : p(X0) => p(X1)))) & ((! [X0] : ((p(X0) | c)) <=> (! [X0] : p(X0) | c)) & ((? [X0] : ((p(X0) & c)) <=> (? [X0] : p(X0) & c)) & ((? [X0] : c <=> c) & ((! [X0] : c <=> c) & ((? [X0] : ((c => p(X0))) <=> (c => ? [X0] : p(X0))) & ((? [X0] : ((p(X0) => c)) <=> (! [X0] : p(X0) => c)) & ((! [X0] : ((c => p(X0))) <=> (c => ! [X0] : p(X0))) & (! [X0] : ((p(X0) => c)) <=> (? [X0] : p(X0) => c)))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [prove_this])). % 15.41/3.01 cnf(c0, plain, ~X0 | ~X1 | ~X2 | ~X3 | ~X4 | ~X5 | p(X6) | ~X7 | ~X8, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c1, plain, ~X0 | ~X1 | ~X2 | ~X3 | ~X4 | ~X5 | ~X6 | ~X7 | ~p(sK28), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c2, plain, ~X0(X1) | f(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c4, plain, ~X0(X1) | ~h(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c5, plain, ~X0 | f(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c6, plain, ~X0 | g(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c7, plain, ~X0 | ~h(sK29), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c8, plain, ~X0 | p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c9, plain, ~X0 | q(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c10, plain, X0 | ~p(sK31) | ~q(sK31), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c11, plain, ~X0 | p(sK32) | q(sK32), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c12, plain, X0 | ~p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c13, plain, X0 | ~q(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c14, plain, ~X0 | p(X1) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c15, plain, X0 | ~p(sK35), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c16, plain, X0 | ~c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c17, plain, ~X0 | p(sK36), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c18, plain, ~X0 | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c19, plain, X0 | ~p(X1) | ~c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c20, plain, ~X0 | ~c | p(sK38), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c21, plain, X0 | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c22, plain, X0 | ~p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c23, plain, ~X0 | ~p(sK40) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c24, plain, X0 | p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c25, plain, X0 | ~c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c26, plain, ~X0 | ~c | p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c27, plain, X0 | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c28, plain, X0 | ~p(sK43), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c29, plain, ~X0 | ~p(X1) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c30, plain, X0 | p(sK45), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c31, plain, X0 | ~c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c33, plain, X0 | X1 | ~c | p(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c34, plain, X0 | c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c36, plain, X0 | ~p(sK46) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c39, plain, X0 | X1 | ~p(sK49) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c40, plain, X0 | p(X1) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c42, plain, X0 | ~c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c45, plain, X0 | X1 | ~c | p(sK51), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c46, plain, X0 | c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c48, plain, X0 | ~p(X1) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c51, plain, X0 | X1 | ~X2 | ~X3 | ~X4 | ~p(X5) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c52, plain, X0 | ~X1 | ~X2 | ~X3 | p(sK52) | ~X4, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c54, plain, ~c | X0 | ~X1 | ~X2 | ~X3 | ~X4, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c61, plain, X0 | c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c66, plain, X0 | ~c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c73, plain, X0 | X1 | p(X2) | c, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c74, plain, X0 | ~p(sK58) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c76, plain, X0 | ~c | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c78, plain, X0 | ~p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c79, plain, X0 | p(sK62), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c82, plain, ~X0 | ~X1 | X2 | p(sK64) | ~X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c83, plain, ~X0 | ~X1 | X2 | c | ~X3 | X4, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c84, plain, ~c | ~X0 | ~X1 | ~X2 | ~X3 | X4 | ~p(X5), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c87, plain, X0 | p(X1) | p(X2) | ~X3, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c90, plain, X0 | ~p(sK65) | ~p(X1) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c91, plain, X0 | p(sK69) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c92, plain, X0 | q(sK69) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c93, plain, X0 | ~p(X1) | ~q(X2) | ~X3, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c95, plain, X0 | X1 | p(sK74) | q(sK75), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c96, plain, X0 | ~p(X1) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c98, plain, X0 | ~q(X1) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c100, plain, X0 | p(X1) | q(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c101, plain, X0 | ~p(sK78), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c102, plain, X0 | ~q(sK78), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c104, plain, X0 | X1 | p(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c105, plain, X0 | X1 | q(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c106, plain, X0 | ~p(sK79) | ~q(sK80) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c109, plain, X0 | ~p(sK84(X1)) | q(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c110, plain, X0 | p(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c111, plain, X0 | ~q(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c112, plain, X0 | X1 | f(sK85), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c113, plain, X0 | X1 | ~g(sK85), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c114, plain, ~f(X0) | g(X1) | h(X0) | ~f(X1) | X2, inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c115, plain, X0 | ~f(X1) | ~h(X1) | g(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c116, plain, X0 | ~f(X1) | ~g(X1) | h(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c117, plain, X0 | ~r(X1,X2) | r(X2,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c118, plain, X0 | ~r(X1,X2) | ~r(X2,X3) | r(X1,X3), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c119, plain, X0 | r(sK95,sK96), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c120, plain, X0 | ~r(sK95,sK95), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c121, plain, X0 | X1(X2) | f(sK98), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c122, plain, X0 | X1(X2) | ~g(sK98), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c123, plain, ~f(X0) | h(X1) | X2 | ~f(X1) | g(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c124, plain, X0 | ~f(X1) | ~h(X1) | g(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(c125, plain, X0 | ~f(X1) | ~g(X1) | h(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 15.41/3.01 cnf(d0, plain, 'Ts16' | 'Ts16', inference(resolution, [status(thm)], [c79,c78])). % 15.41/3.01 cnf(d1, plain, ~p(X0) | ~c | ~'Ts5' | ~'Ts14' | ~'Ts15' | 'Ts17', inference(resolution, [status(thm)], [d0,c84])). % 15.41/3.01 cnf(d2, plain, ~c | ~'Ts5' | ~'Ts14' | ~'Ts15' | 'Ts17' | ~'Ts5', inference(resolution, [status(thm)], [d1,c17])). % 15.41/3.01 cnf(d3, plain, 'Ts19' | ~p(X0) | ~'Ts18' | 'Ts19' | ~'Ts18', inference(resolution, [status(thm)], [c93,c92])). % 15.41/3.01 cnf(d4, plain, 'Ts19' | ~'Ts18' | 'Ts19' | ~'Ts18', inference(resolution, [status(thm)], [d3,c91])). % 15.41/3.01 cnf(d5, plain, p(X0) | ~'Ts17' | 'Ts18', inference(factoring, [status(thm)], [c87])). % 15.41/3.01 cnf(d6, plain, ~'Ts17' | 'Ts18' | ~p(X0) | ~'Ts17' | 'Ts18', inference(resolution, [status(thm)], [d5,c90])). % 15.41/3.01 cnf(d7, plain, ~'Ts17' | 'Ts18' | ~'Ts17' | 'Ts18', inference(resolution, [status(thm)], [d6,d5])). % 15.41/3.01 cnf(d8, plain, c | 'Ts5' | ~'Ts14' | ~'Ts15' | 'Ts17', inference(resolution, [status(thm)], [d0,c83])). % 15.41/3.01 cnf(d9, plain, 'Ts4' | c | 'Ts15' | 'Ts4', inference(resolution, [status(thm)], [c73,c15])). % 15.41/3.01 cnf(d10, plain, ~'Ts4' | 'Ts15' | ~'Ts4' | c, inference(resolution, [status(thm)], [c74,c14])). % 15.41/3.01 cnf(d11, plain, c | 'Ts15' | c | 'Ts15', inference(resolution, [status(thm)], [d10,d9])). % 15.41/3.01 cnf(d12, plain, c | c | 'Ts5' | ~'Ts14' | 'Ts17', inference(resolution, [status(thm)], [d11,d8])). % 15.41/3.01 cnf(d13, plain, c | 'Ts10' | c, inference(resolution, [status(thm)], [c34,c27])). % 15.41/3.01 cnf(d14, plain, c | 'Ts7' | 'Ts11' | 'Ts7', inference(resolution, [status(thm)], [c39,c24])). % 15.41/3.01 cnf(d15, plain, ~'Ts7' | 'Ts11' | c | ~'Ts7', inference(resolution, [status(thm)], [c40,c23])). % 15.41/3.01 cnf(d16, plain, c | 'Ts11' | c | 'Ts11', inference(resolution, [status(thm)], [d15,d14])). % 15.41/3.01 cnf(d17, plain, c | 'Ts12' | c, inference(resolution, [status(thm)], [c46,c21])). % 15.41/3.01 cnf(d18, plain, c | 'Ts9' | ~'Ts10' | ~'Ts11' | ~'Ts12' | 'Ts13' | 'Ts9', inference(resolution, [status(thm)], [c51,c30])). % 15.41/3.01 cnf(d19, plain, c | 'Ts9' | ~'Ts10' | ~'Ts11' | 'Ts13' | c, inference(resolution, [status(thm)], [d18,d17])). % 15.41/3.01 cnf(d20, plain, c | 'Ts9' | ~'Ts10' | 'Ts13' | c, inference(resolution, [status(thm)], [d19,d16])). % 15.41/3.01 cnf(d21, plain, c | 'Ts9' | 'Ts13' | c, inference(resolution, [status(thm)], [d20,d13])). % 15.41/3.01 cnf(d22, plain, ~'Ts9' | ~'Ts10' | ~'Ts11' | ~'Ts12' | 'Ts13' | c | ~'Ts9', inference(resolution, [status(thm)], [c52,c29])). % 15.41/3.01 cnf(d23, plain, c | ~'Ts9' | ~'Ts10' | ~'Ts11' | 'Ts13' | c, inference(resolution, [status(thm)], [d22,d17])). % 15.41/3.01 cnf(d24, plain, c | ~'Ts9' | ~'Ts10' | 'Ts13' | c, inference(resolution, [status(thm)], [d23,d16])). % 15.41/3.01 cnf(d25, plain, c | ~'Ts9' | 'Ts13' | c, inference(resolution, [status(thm)], [d24,d13])). % 15.41/3.01 cnf(d26, plain, c | 'Ts13' | c | 'Ts13', inference(resolution, [status(thm)], [d25,d21])). % 15.41/3.01 cnf(d27, plain, c | c | 'Ts14', inference(resolution, [status(thm)], [d26,c61])). % 15.41/3.01 cnf(d28, plain, c | c | 'Ts5' | 'Ts17', inference(resolution, [status(thm)], [d27,d12])). % 15.41/3.01 cnf(d29, plain, c | 'Ts17' | c, inference(resolution, [status(thm)], [d28,c18])). % 15.41/3.01 cnf(d30, plain, c | 'Ts18', inference(resolution, [status(thm)], [d29,d7])). % 15.41/3.01 cnf(d31, plain, c | 'Ts19', inference(resolution, [status(thm)], [d30,d4])). % 15.41/3.01 cnf(d32, plain, ~'Ts20' | ~'Ts19' | ~'Ts22' | ~'Ts23' | ~'Ts24' | ~'Ts25' | ~'Ts26' | ~'Ts21' | ~'Ts20' | ~'Ts19' | ~'Ts22' | ~'Ts23' | ~'Ts24' | ~'Ts25' | ~'Ts26' | ~'Ts21', inference(resolution, [status(thm)], [c1,c0])). % 15.41/3.01 cnf(d33, plain, 'Ts21' | q(X0) | 'Ts21', inference(resolution, [status(thm)], [c100,c101])). % 15.41/3.01 cnf(d34, plain, 'Ts21' | 'Ts21', inference(resolution, [status(thm)], [d33,c102])). % 15.41/3.01 cnf(d35, plain, ~'Ts20' | ~'Ts19' | ~'Ts22' | ~'Ts23' | ~'Ts24' | ~'Ts25' | ~'Ts26', inference(resolution, [status(thm)], [d34,d32])). % 15.41/3.01 cnf(d36, plain, 'Ts23' | q(X0) | 'Ts23', inference(resolution, [status(thm)], [c109,c110])). % 15.41/3.01 cnf(d37, plain, 'Ts23' | 'Ts23', inference(resolution, [status(thm)], [d36,c111])). % 15.41/3.01 cnf(d38, plain, ~'Ts20' | ~'Ts19' | ~'Ts22' | ~'Ts24' | ~'Ts25' | ~'Ts26', inference(resolution, [status(thm)], [d37,d35])). % 15.41/3.01 cnf(d39, plain, 'Ts20' | p(sK74) | 'Ts3' | 'Ts3', inference(resolution, [status(thm)], [c95,c13])). % 15.41/3.01 cnf(d40, plain, 'Ts20' | 'Ts3' | 'Ts3', inference(resolution, [status(thm)], [d39,c12])). % 15.41/3.01 cnf(d41, plain, 'Ts20' | ~'Ts3' | p(sK32) | ~'Ts3', inference(resolution, [status(thm)], [c98,c11])). % 15.41/3.01 cnf(d42, plain, 'Ts20' | ~'Ts3' | 'Ts20' | ~'Ts3', inference(resolution, [status(thm)], [d41,c96])). % 15.41/3.01 cnf(d43, plain, 'Ts20' | 'Ts20', inference(resolution, [status(thm)], [d42,d40])). % 15.41/3.01 cnf(d44, plain, ~'Ts19' | ~'Ts22' | ~'Ts24' | ~'Ts25' | ~'Ts26', inference(resolution, [status(thm)], [d43,d38])). % 15.41/3.01 cnf(d45, plain, 'Ts22' | 'Ts2' | ~p(sK31) | 'Ts2', inference(resolution, [status(thm)], [c105,c10])). % 15.41/3.01 cnf(d46, plain, 'Ts22' | 'Ts2' | 'Ts22' | 'Ts2', inference(resolution, [status(thm)], [d45,c104])). % 15.41/3.01 cnf(d47, plain, 'Ts22' | ~p(sK79) | ~'Ts2' | ~'Ts2', inference(resolution, [status(thm)], [c106,c9])). % 15.41/3.01 cnf(d48, plain, 'Ts22' | ~'Ts2' | ~'Ts2', inference(resolution, [status(thm)], [d47,c8])). % 15.41/3.01 cnf(d49, plain, 'Ts22' | 'Ts22', inference(resolution, [status(thm)], [d48,d46])). % 15.41/3.01 cnf(d50, plain, ~'Ts19' | ~'Ts24' | ~'Ts25' | ~'Ts26', inference(resolution, [status(thm)], [d49,d44])). % 15.41/3.01 cnf(d51, plain, 'Ts25' | 'Ts25' | r(sK96,sK95), inference(resolution, [status(thm)], [c119,c117])). % 15.41/3.01 cnf(d52, plain, 'Ts25' | 'Ts25' | r(X0,sK95) | ~r(X0,sK96), inference(resolution, [status(thm)], [d51,c118])). % 15.41/3.01 cnf(d53, plain, 'Ts25' | r(sK95,sK95) | 'Ts25', inference(resolution, [status(thm)], [d52,c119])). % 15.41/3.01 cnf(d54, plain, 'Ts25' | 'Ts25', inference(resolution, [status(thm)], [d53,c120])). % 15.41/3.01 cnf(d55, plain, ~'Ts19' | ~'Ts24' | ~'Ts26', inference(resolution, [status(thm)], [d54,d50])). % 15.41/3.01 cnf(d56, plain, 'Ts24' | ~f(sK29) | h(sK29) | ~'Ts1', inference(resolution, [status(thm)], [c116,c6])). % 15.41/3.01 cnf(d57, plain, 'Ts24' | h(sK29) | ~'Ts1' | ~'Ts1', inference(resolution, [status(thm)], [d56,c5])). % 15.41/3.01 cnf(d58, plain, 'Ts24' | ~'Ts1' | ~'Ts1', inference(resolution, [status(thm)], [d57,c7])). % 15.41/3.01 cnf(d59, plain, 'Ts24' | ~f(X0) | g(sK85) | h(X0) | 'Ts24' | 'Ts1', inference(resolution, [status(thm)], [c114,c112])). % 15.41/3.01 cnf(d60, plain, 'Ts24' | g(sK85) | h(sK85) | 'Ts1' | 'Ts24' | 'Ts1', inference(resolution, [status(thm)], [d59,c112])). % 15.41/3.01 cnf(d61, plain, 'Ts24' | g(sK85) | 'Ts1' | 'Ts24' | ~f(sK85) | g(sK85), inference(resolution, [status(thm)], [d60,c115])). % 15.41/3.01 cnf(d62, plain, 'Ts24' | g(sK85) | 'Ts1' | 'Ts24' | 'Ts1', inference(resolution, [status(thm)], [d61,c112])). % 15.41/3.01 cnf(d63, plain, 'Ts24' | 'Ts1' | 'Ts24' | 'Ts1', inference(resolution, [status(thm)], [d62,c113])). % 15.41/3.01 cnf(d64, plain, 'Ts24' | 'Ts24', inference(resolution, [status(thm)], [d63,d58])). % 15.41/3.01 cnf(d65, plain, ~'Ts19' | ~'Ts26', inference(resolution, [status(thm)], [d64,d55])). % 15.41/3.01 cnf(d66, plain, 'Ts26' | f(sK98) | f(X0), inference(resolution, [status(thm)], [c121,c2])). % 15.41/3.01 cnf(d67, plain, 'Ts26' | f(sK98), inference(factoring, [status(thm)], [d66])). % 15.41/3.01 cnf(d68, plain, 'Ts26' | 'Ts26' | ~f(X0) | g(X0) | h(sK98), inference(resolution, [status(thm)], [d67,c123])). % 15.41/3.01 cnf(d69, plain, 'Ts26' | g(sK98) | h(sK98) | 'Ts26', inference(resolution, [status(thm)], [d68,d67])). % 15.41/3.01 cnf(d70, plain, 'Ts26' | g(sK98) | 'Ts26' | ~f(sK98) | g(sK98), inference(resolution, [status(thm)], [d69,c124])). % 15.41/3.01 cnf(d71, plain, 'Ts26' | g(sK98) | 'Ts26', inference(resolution, [status(thm)], [d70,d67])). % 15.41/3.01 cnf(d72, plain, 'Ts26' | 'Ts26' | 'Ts0'(X0), inference(resolution, [status(thm)], [d71,c122])). % 15.41/3.01 cnf(d73, plain, 'Ts26' | f(X0), inference(resolution, [status(thm)], [d72,c2])). % 15.41/3.01 cnf(d74, plain, 'Ts26' | 'Ts26' | ~f(sK98) | h(sK98), inference(resolution, [status(thm)], [d71,c125])). % 15.41/3.01 cnf(d75, plain, 'Ts26' | h(sK98) | 'Ts26', inference(resolution, [status(thm)], [d74,d73])). % 15.41/3.01 cnf(d76, plain, 'Ts26' | ~'Ts0'(sK98), inference(resolution, [status(thm)], [d75,c4])). % 15.41/3.01 cnf(d77, plain, 'Ts26' | 'Ts26', inference(resolution, [status(thm)], [d76,d72])). % 15.41/3.01 cnf(d78, plain, ~'Ts19', inference(resolution, [status(thm)], [d77,d65])). % 15.41/3.01 cnf(d79, plain, c, inference(resolution, [status(thm)], [d78,d31])). % 15.41/3.01 cnf(d80, plain, ~'Ts5' | ~'Ts14' | ~'Ts15' | 'Ts17', inference(resolution, [status(thm)], [d79,d2])). % 15.41/3.01 cnf(d81, plain, ~'Ts18', inference(resolution, [status(thm)], [d78,d4])). % 15.41/3.01 cnf(d82, plain, ~'Ts17', inference(resolution, [status(thm)], [d81,d7])). % 15.41/3.01 cnf(d83, plain, ~'Ts5' | ~'Ts14' | ~'Ts15', inference(resolution, [status(thm)], [d82,d80])). % 15.41/3.01 cnf(d84, plain, ~'Ts4' | 'Ts15', inference(resolution, [status(thm)], [d79,c76])). % 15.41/3.01 cnf(d85, plain, 'Ts4', inference(resolution, [status(thm)], [d79,c16])). % 15.41/3.01 cnf(d86, plain, 'Ts15', inference(resolution, [status(thm)], [d85,d84])). % 15.41/3.01 cnf(d87, plain, ~'Ts5' | ~'Ts14', inference(resolution, [status(thm)], [d86,d83])). % 15.41/3.01 cnf(d88, plain, ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d79,c66])). % 15.41/3.01 cnf(d89, plain, ~'Ts9' | ~'Ts10' | ~'Ts11' | ~'Ts12' | 'Ts13', inference(resolution, [status(thm)], [d79,c54])). % 15.41/3.01 cnf(d90, plain, 'Ts9', inference(resolution, [status(thm)], [d79,c31])). % 15.41/3.01 cnf(d91, plain, ~'Ts10' | ~'Ts11' | ~'Ts12' | 'Ts13', inference(resolution, [status(thm)], [d90,d89])). % 15.41/3.01 cnf(d92, plain, ~c | 'Ts8' | 'Ts10' | 'Ts8', inference(resolution, [status(thm)], [c33,c28])). % 15.41/3.01 cnf(d93, plain, 'Ts8' | 'Ts10', inference(resolution, [status(thm)], [d79,d92])). % 15.41/3.01 cnf(d94, plain, ~'Ts8' | 'Ts10' | ~c | ~'Ts8', inference(resolution, [status(thm)], [c36,c26])). % 15.41/3.01 cnf(d95, plain, ~'Ts8' | 'Ts10', inference(resolution, [status(thm)], [d79,d94])). % 15.41/3.01 cnf(d96, plain, 'Ts10' | 'Ts10', inference(resolution, [status(thm)], [d95,d93])). % 15.41/3.01 cnf(d97, plain, ~'Ts11' | ~'Ts12' | 'Ts13', inference(resolution, [status(thm)], [d96,d91])). % 15.41/3.01 cnf(d98, plain, ~'Ts6' | 'Ts12' | ~c | ~'Ts6', inference(resolution, [status(thm)], [c48,c20])). % 15.41/3.01 cnf(d99, plain, ~'Ts6' | 'Ts12', inference(resolution, [status(thm)], [d79,d98])). % 15.41/3.01 cnf(d100, plain, ~c | 'Ts6' | 'Ts12' | 'Ts6', inference(resolution, [status(thm)], [c45,c22])). % 15.41/3.01 cnf(d101, plain, 'Ts6' | 'Ts12', inference(resolution, [status(thm)], [d79,d100])). % 15.41/3.01 cnf(d102, plain, 'Ts12' | 'Ts12', inference(resolution, [status(thm)], [d101,d99])). % 15.41/3.01 cnf(d103, plain, ~'Ts11' | 'Ts13', inference(resolution, [status(thm)], [d102,d97])). % 15.41/3.01 cnf(d104, plain, ~'Ts7' | 'Ts11', inference(resolution, [status(thm)], [d79,c42])). % 15.41/3.01 cnf(d105, plain, 'Ts7', inference(resolution, [status(thm)], [d79,c25])). % 15.41/3.01 cnf(d106, plain, 'Ts11', inference(resolution, [status(thm)], [d105,d104])). % 15.41/3.01 cnf(d107, plain, 'Ts13', inference(resolution, [status(thm)], [d106,d103])). % 15.41/3.01 cnf(d108, plain, 'Ts14', inference(resolution, [status(thm)], [d107,d88])). % 15.41/3.01 cnf(d109, plain, ~'Ts5', inference(resolution, [status(thm)], [d108,d87])). % 15.41/3.01 cnf(d110, plain, ~p(X0) | 'Ts5', inference(resolution, [status(thm)], [d79,c19])). % 15.41/3.01 cnf(d111, plain, p(sK64) | 'Ts5' | ~'Ts14' | ~'Ts15' | 'Ts17', inference(resolution, [status(thm)], [d0,c82])). % 15.41/3.01 cnf(d112, plain, p(sK64) | 'Ts5' | ~'Ts14' | ~'Ts15', inference(resolution, [status(thm)], [d82,d111])). % 15.41/3.01 cnf(d113, plain, p(sK64) | 'Ts5' | ~'Ts14', inference(resolution, [status(thm)], [d86,d112])). % 15.41/3.01 cnf(d114, plain, p(sK64) | 'Ts5', inference(resolution, [status(thm)], [d108,d113])). % 15.41/3.01 cnf(d115, plain, 'Ts5' | 'Ts5', inference(resolution, [status(thm)], [d114,d110])). % 15.41/3.01 cnf(d116, plain, $false, inference(resolution, [status(thm)], [d115,d109])). % 15.41/3.01 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------