%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SYN938+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 : n017.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:22 AM UTC 2026
% Result : Theorem 15.85s 2.52s
% Output : CNFRefutation 15.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN938+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.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 18:46:33 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.85/2.52 % SZS status Theorem for theBenchmark.p
% 15.85/2.52 % SZS output start CNFRefutation for theBenchmark.p
% 15.85/2.52 fof(prove_this, conjecture, (! [X0] : ! [X1] : ((! [X2] : q1(f(X2)) => ? [X3] : ? [X4] : (((p1(f(X4)) => p1(X3)) & ((r1(X4) => (r1(X1) & r1(X0))) & q1(X3)))))) & (! [X1] : ! [X0] : ((! [X2] : q1(f(X2)) => ? [X3] : ? [X4] : (((p1(f(X4)) => (p1(X3) & (r1(X4) => (r1(X1) & r1(X0))))) & q1(X3))))) & (! [X1] : ! [X0] : ((q1(f(X1)) => ? [X3] : ? [X4] : (((p1(f(X4)) => (p1(X3) & (r1(X4) => (r1(X1) & r1(X0))))) & q1(X3))))) & (((! [X3] : ((a1(X3) => (b(X3) | c(X3)))) & ~! [X3] : ((a1(X3) => b(X3)))) => ? [X3] : ((a1(X3) & c(X3)))) & (! [X5] : ? [X3] : ? [X6] : ? [X7] : ? [X8] : ? [X4] : (((p1(X5) & (e(X5) & ((e(X3) => (g(X3) | s(X3,f(X3)))) & ((e(X6) => (g(X6) | c(f(X6)))) & (s(X5,X4) => p1(X4)))))) => ((p1(X7) & g(X7)) | (p1(X8) & c(X8))))) & (! [X5] : ! [X1] : ! [X0] : (((s1(X5) & (s1(X1) & (r(X1,X0) & (! [X3] : ((s1(X3) => p1(X3))) & ! [X3] : ! [X4] : ((r(X3,X4) => q(X3,X4))))))) => ? [X3] : ? [X4] : ((p1(X3) & q(X3,X4))))) & ((! [X3] : p1(X3) => ! [X5] : ! [X1] : ((p1(X5) & p1(X1)))) & (((! [X3] : p1(X3) & ? [X4] : q1(X4)) => ? [X2] : ! [X4] : ((p1(X4) | r1(X2)))) & ((! [X3] : ? [X4] : ((p1(X3) & q1(X4))) => ? [X2] : ! [X4] : ((p1(X4) | r1(X2)))) & ((! [X3] : ? [X4] : ((a(X3,X4) & a(X4,X4))) => ? [X2] : a(X2,X2)) & (! [X5] : ! [X1] : ! [X0] : (((s1(X5) & (s1(X1) & (r(X1,X0) & (! [X3] : ((s1(X3) => p1(X3))) & ! [X3] : ! [X4] : ((r(X3,X4) => q(X3,X4))))))) => ? [X3] : ? [X4] : ((p1(X3) & q(X3,X4))))) & (! [X5] : ! [X1] : ((! [X4] : ((q1(X4) => p1(X4))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & ((? [X3] : p1(X3) => (? [X3] : p1(X3) & (a0 => ((b0 | ~b0) & (q0 => q0))))) & ((! [X3] : p1(X3) => ? [X4] : p1(X4)) & ((! [X3] : ((p1(X3) => q1(X3))) => (! [X3] : p1(X3) => ! [X3] : q1(X3))) & (! [X5] : ! [X1] : ((! [X2] : ((q1(X2) => p1(X2))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & ((! [X3] : ((a1(X3) => b(X3))) => (? [X3] : a1(X3) => ? [X3] : b(X3))) & ((? [X3] : ((a1(X3) => b(X3))) => (! [X3] : a1(X3) => ? [X3] : b(X3))) & (~? [X4] : ! [X3] : ((a(X3,X4) <=> ~a(X3,X3))) & (((? [X3] : a1(X3) & ! [X3] : b(X3)) => ? [X3] : ((a1(X3) & b(X3)))) & ((? [X3] : b(X3) => ? [X3] : ((a1(X3) | b(X3)))) & ((? [X3] : ? [X4] : a(X3,X4) <=> ? [X4] : ? [X3] : a(X3,X4)) & (! [X5] : ! [X1] : ((! [X3] : p1(X3) => (p1(X5) & p1(X1)))) & ((! [X3] : p1(X3) => (! [X3] : p1(X3) & ! [X4] : p1(X4))) & ((? [X3] : p1(X3) <=> ? [X4] : p1(X4)) & ((? [X3] : p1(X3) => ? [X2] : p1(X2)) & (? [X2] : ! [X3] : ? [X4] : (((p(X4,X3) => ? [X9] : p(X9,X4)) & ((p(X2,X4) & p(X4,X2)) => p(X4,X3)))) & ((! [X3] : ! [X4] : ((eq(X3,X4) <=> ! [X2] : (('a$umember$uof'(X2,X3) <=> 'a$umember$uof'(X2,X4))))) => ! [X5] : ! [X1] : ((eq(X5,X1) => eq(X1,X5)))) & (! [X5] : ! [X1] : ((! [X4] : ((q1(X4) => p1(X4))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & (? [X3] : ! [X4] : ((p1(X3) => p1(X4))) & (! [X1] : (((! [X3] : ((p1(X3) => q1(X3))) & r1(X1)) => (! [X4] : ((r1(X4) => p1(X4))) => q1(X1)))) & (! [X5] : ! [X1] : ? [X3] : ? [X4] : (((p1(X3) => r1(X4)) => (p1(X5) => r1(X1)))) & (? [X4] : ((? [X3] : p1(X3) => p1(X4))) & ((? [X3] : ! [X4] : p(X3,X4) => ! [X4] : ? [X3] : p(X3,X4)) & ((p1(z) => p1(z)) & ((? [X3] : p1(X3) => ? [X4] : p1(X4)) & ((! [X3] : ! [X4] : p(X3,X4) => ! [X3] : p(X3,X3)) & (! [X5] : ((((f0 | g0) & ! [X3] : ((p1(X3) & q1(X3)))) => q1(X5))) & (((a0 <=> b0) | (a0 | b0)) & (((a0 & b0) => (a0 <=> b0)) & (! [X5] : ! [X1] : ? [X3] : ? [X4] : ((((q1(X3) => p(X3,X5)) & (q1(X5) & (q1(X1) & ((r1(X4) => p(X1,X4)) & (r1(X5) & (r1(X1) & ((s1(X5) => p(X3,X4)) & s1(X5)))))))) => p(X5,X1))) & (! [X1] : ((! [X4] : (((r1(X1) => r1(X4)) => p(f(X4),X4))) => ? [X3] : ? [X4] : ((p(X3,X4) & (q(f(X1),X1) => q(X3,X4)))))) & ((! [X3] : ((p1(X3) => q1(X3))) & ? [X4] : ((q1(X4) => r1(X4)))) => ? [X2] : ((p1(X2) => r1(X2))))))))))))))))))))))))))))))))))))))))))))))).
% 15.85/2.52 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : ((! [X2] : q1(f(X2)) => ? [X3] : ? [X4] : (((p1(f(X4)) => p1(X3)) & ((r1(X4) => (r1(X1) & r1(X0))) & q1(X3)))))) & (! [X1] : ! [X0] : ((! [X2] : q1(f(X2)) => ? [X3] : ? [X4] : (((p1(f(X4)) => (p1(X3) & (r1(X4) => (r1(X1) & r1(X0))))) & q1(X3))))) & (! [X1] : ! [X0] : ((q1(f(X1)) => ? [X3] : ? [X4] : (((p1(f(X4)) => (p1(X3) & (r1(X4) => (r1(X1) & r1(X0))))) & q1(X3))))) & (((! [X3] : ((a1(X3) => (b(X3) | c(X3)))) & ~! [X3] : ((a1(X3) => b(X3)))) => ? [X3] : ((a1(X3) & c(X3)))) & (! [X5] : ? [X3] : ? [X6] : ? [X7] : ? [X8] : ? [X4] : (((p1(X5) & (e(X5) & ((e(X3) => (g(X3) | s(X3,f(X3)))) & ((e(X6) => (g(X6) | c(f(X6)))) & (s(X5,X4) => p1(X4)))))) => ((p1(X7) & g(X7)) | (p1(X8) & c(X8))))) & (! [X5] : ! [X1] : ! [X0] : (((s1(X5) & (s1(X1) & (r(X1,X0) & (! [X3] : ((s1(X3) => p1(X3))) & ! [X3] : ! [X4] : ((r(X3,X4) => q(X3,X4))))))) => ? [X3] : ? [X4] : ((p1(X3) & q(X3,X4))))) & ((! [X3] : p1(X3) => ! [X5] : ! [X1] : ((p1(X5) & p1(X1)))) & (((! [X3] : p1(X3) & ? [X4] : q1(X4)) => ? [X2] : ! [X4] : ((p1(X4) | r1(X2)))) & ((! [X3] : ? [X4] : ((p1(X3) & q1(X4))) => ? [X2] : ! [X4] : ((p1(X4) | r1(X2)))) & ((! [X3] : ? [X4] : ((a(X3,X4) & a(X4,X4))) => ? [X2] : a(X2,X2)) & (! [X5] : ! [X1] : ! [X0] : (((s1(X5) & (s1(X1) & (r(X1,X0) & (! [X3] : ((s1(X3) => p1(X3))) & ! [X3] : ! [X4] : ((r(X3,X4) => q(X3,X4))))))) => ? [X3] : ? [X4] : ((p1(X3) & q(X3,X4))))) & (! [X5] : ! [X1] : ((! [X4] : ((q1(X4) => p1(X4))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & ((? [X3] : p1(X3) => (? [X3] : p1(X3) & (a0 => ((b0 | ~b0) & (q0 => q0))))) & ((! [X3] : p1(X3) => ? [X4] : p1(X4)) & ((! [X3] : ((p1(X3) => q1(X3))) => (! [X3] : p1(X3) => ! [X3] : q1(X3))) & (! [X5] : ! [X1] : ((! [X2] : ((q1(X2) => p1(X2))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & ((! [X3] : ((a1(X3) => b(X3))) => (? [X3] : a1(X3) => ? [X3] : b(X3))) & ((? [X3] : ((a1(X3) => b(X3))) => (! [X3] : a1(X3) => ? [X3] : b(X3))) & (~? [X4] : ! [X3] : ((a(X3,X4) <=> ~a(X3,X3))) & (((? [X3] : a1(X3) & ! [X3] : b(X3)) => ? [X3] : ((a1(X3) & b(X3)))) & ((? [X3] : b(X3) => ? [X3] : ((a1(X3) | b(X3)))) & ((? [X3] : ? [X4] : a(X3,X4) <=> ? [X4] : ? [X3] : a(X3,X4)) & (! [X5] : ! [X1] : ((! [X3] : p1(X3) => (p1(X5) & p1(X1)))) & ((! [X3] : p1(X3) => (! [X3] : p1(X3) & ! [X4] : p1(X4))) & ((? [X3] : p1(X3) <=> ? [X4] : p1(X4)) & ((? [X3] : p1(X3) => ? [X2] : p1(X2)) & (? [X2] : ! [X3] : ? [X4] : (((p(X4,X3) => ? [X9] : p(X9,X4)) & ((p(X2,X4) & p(X4,X2)) => p(X4,X3)))) & ((! [X3] : ! [X4] : ((eq(X3,X4) <=> ! [X2] : (('a$umember$uof'(X2,X3) <=> 'a$umember$uof'(X2,X4))))) => ! [X5] : ! [X1] : ((eq(X5,X1) => eq(X1,X5)))) & (! [X5] : ! [X1] : ((! [X4] : ((q1(X4) => p1(X4))) => ? [X3] : (((p1(X3) => p1(X5)) & (q1(X3) => p1(X1)))))) & (? [X3] : ! [X4] : ((p1(X3) => p1(X4))) & (! [X1] : (((! [X3] : ((p1(X3) => q1(X3))) & r1(X1)) => (! [X4] : ((r1(X4) => p1(X4))) => q1(X1)))) & (! [X5] : ! [X1] : ? [X3] : ? [X4] : (((p1(X3) => r1(X4)) => (p1(X5) => r1(X1)))) & (? [X4] : ((? [X3] : p1(X3) => p1(X4))) & ((? [X3] : ! [X4] : p(X3,X4) => ! [X4] : ? [X3] : p(X3,X4)) & ((p1(z) => p1(z)) & ((? [X3] : p1(X3) => ? [X4] : p1(X4)) & ((! [X3] : ! [X4] : p(X3,X4) => ! [X3] : p(X3,X3)) & (! [X5] : ((((f0 | g0) & ! [X3] : ((p1(X3) & q1(X3)))) => q1(X5))) & (((a0 <=> b0) | (a0 | b0)) & (((a0 & b0) => (a0 <=> b0)) & (! [X5] : ! [X1] : ? [X3] : ? [X4] : ((((q1(X3) => p(X3,X5)) & (q1(X5) & (q1(X1) & ((r1(X4) => p(X1,X4)) & (r1(X5) & (r1(X1) & ((s1(X5) => p(X3,X4)) & s1(X5)))))))) => p(X5,X1))) & (! [X1] : ((! [X4] : (((r1(X1) => r1(X4)) => p(f(X4),X4))) => ? [X3] : ? [X4] : ((p(X3,X4) & (q(f(X1),X1) => q(X3,X4)))))) & ((! [X3] : ((p1(X3) => q1(X3))) & ? [X4] : ((q1(X4) => r1(X4)))) => ? [X2] : ((p1(X2) => r1(X2))))))))))))))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [prove_this])).
% 15.85/2.52 cnf(c0, plain, ~X0 | ~X1 | p1(sK39) | ~X2 | ~X3 | ~X4 | ~X5 | ~X6 | ~X7 | ~X8 | p1(X9) | ~X10 | ~X11 | ~X12, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c1, plain, ~X0 | ~X1 | ~X2 | ~X3 | ~X4 | ~X5 | ~X6 | ~X7 | ~X8 | p1(X9) | ~X10 | ~X11 | ~X12 | ~p1(X13) | ~X14, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c3, plain, ~X0 | ~X1 | ~X2 | ~X3 | ~X4 | ~X5 | ~X6 | ~X7 | ~X8 | ~X9 | ~X10 | ~p1(sK37) | ~p1(X11) | ~X12 | ~X13 | ~p1(sK38), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c5, plain, X0 | ~b0 | q0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c6, plain, X0 | ~b0 | ~q0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c7, plain, X0 | b0 | q0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c8, plain, X0 | b0 | ~q0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c9, plain, X0(X1,X2,X3) | p(X3,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c10, plain, X0(X1,X2,X3) | p(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c11, plain, X0(X1,X2,X3) | ~p(X2,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c12, plain, X0 | r1(sK41) | p(f(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c13, plain, X0 | ~r1(X1) | p(f(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c14, plain, X0 | ~p(X1,X2) | q(f(sK41),sK41), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c15, plain, X0 | ~p(X1,X2) | ~q(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c22, plain, X0 | ~s1(sK45) | p(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c23, plain, X0 | s1(sK45), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c24, plain, X0 | ~p(sK45,sK46), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c25, plain, X0 | a0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c26, plain, X0 | b0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c29, plain, X0 | ~b0 | ~a0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c32, plain, X0 | a0 | b0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c35, plain, X0 | ~a0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c36, plain, X0 | ~b0, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c39, plain, X0 | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c40, plain, X0 | ~q1(sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c41, plain, ~X0 | ~X1 | X2 | q1(X3) | ~X4 | ~X5 | ~X6 | ~p1(X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c42, plain, ~X0 | X1 | ~X2 | ~X3 | ~X4 | ~X5 | r1(sK52) | ~q1(sK52), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c43, plain, ~X0 | ~X1 | X2 | p1(X3) | ~X4 | ~X5 | ~X6, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c44, plain, ~X0 | ~X1 | X2 | ~r1(X3) | ~X4 | ~X5 | ~X6, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c45, plain, X0 | p1(sK54) | p(X1,X2) | ~X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c46, plain, X0 | p1(sK54) | ~p(sK58,sK58) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c47, plain, X0 | ~p1(X1) | p(X2,X3) | ~X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c48, plain, X0 | ~p1(X1) | ~p(sK58,sK58) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c49, plain, X0 | p(sK59,X1) | p1(z) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c50, plain, X0 | p(sK59,X1) | ~p1(z) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c51, plain, X0 | ~p(X1,sK61) | p1(z) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c52, plain, X0 | ~p(X1,sK61) | ~p1(z) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c53, plain, X0 | ~p1(X1) | r1(X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c54, plain, X0 | p1(sK63), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c55, plain, X0 | ~r1(sK64), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c56, plain, X0 | ~p1(X1) | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c57, plain, X0 | r1(sK67), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c58, plain, X0 | ~r1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c59, plain, X0 | ~q1(sK67), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c60, plain, X0 | ~q1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c61, plain, X0 | p1(X1) | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c64, plain, X0 | ~p1(sK70) | ~p1(sK71), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c65, plain, X0 | ~eq(X1,X2) | ~'a$umember$uof'(X3,X1) | 'a$umember$uof'(X3,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c66, plain, X0 | ~eq(X1,X2) | 'a$umember$uof'(X3,X1) | ~'a$umember$uof'(X3,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c68, plain, X0 | eq(X1,X2) | 'a$umember$uof'(sK77(X1,X2),X1) | 'a$umember$uof'(sK77(X1,X2),X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c69, plain, X0 | eq(X1,X2) | ~'a$umember$uof'(sK77(X1,X2),X2) | ~'a$umember$uof'(sK77(X1,X2),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c71, plain, X0 | eq(sK78,sK79), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c72, plain, X0 | ~eq(sK79,sK78), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c73, plain, p1(X0) | ~X1 | p1(sK83) | ~X2 | ~X3 | ~X4 | X5 | ~X6, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c74, plain, p1(X0) | ~X1 | ~X2 | ~X3 | ~X4 | ~p1(X5) | X6 | ~X7, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c76, plain, ~X0 | ~X1 | ~X2 | ~X3 | ~p1(sK81(X4)) | ~p1(X5) | X6 | ~X7, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c77, plain, p(X0,sK87(X1)) | p1(sK84) | X2 | ~X3(sK87(X1),X0,X1) | ~X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c78, plain, X0 | ~X1(sK87(X2),X3,X2) | ~X4 | p1(sK84) | ~p(X5,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c79, plain, p(X0,sK87(X1)) | X2 | ~X3(sK87(X1),X0,X1) | ~p1(X4) | ~X5, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c80, plain, ~p(X0,X1) | X2 | ~X3(sK87(X4),X1,X4) | ~p1(X5) | ~X6, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c81, plain, X0 | p1(X1) | ~p1(X2) | ~X3 | p1(sK93), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c82, plain, X0 | p1(sK96) | p1(X1) | ~X2 | p1(sK93), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c83, plain, X0 | p1(X1) | ~p1(X2) | ~p1(X3) | ~X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c87, plain, X0 | ~p1(sK92) | ~p1(X1) | ~p1(X2) | ~p1(sK91) | ~X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c89, plain, ~X0 | a(sK97,sK98) | p1(X1) | ~a(X2,X3) | X4, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c90, plain, ~X0 | a(sK97,sK98) | ~p1(sK105) | ~a(X1,X2) | ~p1(sK106) | X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c91, plain, ~X0 | a(sK97,sK98) | p1(X1) | a(sK104,sK103) | X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c92, plain, ~X0 | a(sK97,sK98) | ~p1(sK105) | a(sK104,sK103) | ~p1(sK106) | X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c93, plain, ~a(X0,X1) | ~X2 | p1(X3) | ~a(X4,X5) | X6, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c94, plain, ~a(X0,X1) | ~X2 | ~p1(sK105) | ~a(X3,X4) | ~p1(sK106) | X5, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c97, plain, X0 | a1(sK108), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c98, plain, X0 | b(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c99, plain, X0 | ~a1(X1) | ~b(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c100, plain, X0 | ~X1 | b(sK111) | ~X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c102, plain, X0 | ~X1 | ~b(X2) | ~X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c103, plain, X0 | ~a1(sK113) | b(sK113), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c104, plain, X0 | a1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c105, plain, X0 | ~b(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c106, plain, X0 | ~a1(X1) | b(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c107, plain, X0 | a1(sK117), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c108, plain, X0 | ~b(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c109, plain, X0 | ~q1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c110, plain, X0 | p1(X1) | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c113, plain, X0 | ~p1(sK119) | ~p1(sK120), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c114, plain, X0 | ~p1(X1) | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c115, plain, X0 | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c116, plain, X0 | ~q1(sK125), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c117, plain, ~X0 | ~X1 | ~a(X2,X2) | ~X3 | ~X4 | ~X5 | X6 | ~a(X2,sK128) | p1(X7), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c118, plain, ~X0 | ~X1 | a(X2,X2) | ~X3 | ~X4 | p1(X5) | a(X2,sK128) | ~X6 | X7, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c119, plain, ~X0 | ~X1 | ~a(X2,X2) | ~X3 | ~X4 | ~a(X2,sK128) | ~X5 | X6 | ~p1(X7), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c120, plain, ~X0 | ~X1 | a(X2,X2) | ~X3 | ~X4 | a(X2,sK128) | ~X5 | X6 | ~p1(X7), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c121, plain, X0 | ~q1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c122, plain, X0 | p1(X1) | q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c125, plain, X0 | ~p1(sK130) | ~p1(sK131), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c127, plain, X0 | s1(sK135), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c128, plain, X0 | r(sK135,sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c129, plain, X0 | ~s1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c130, plain, X0 | ~r(X1,X2) | q(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c131, plain, X0 | ~p1(X1) | ~q(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c133, plain, X0 | a(sK143(X1),sK143(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.52 cnf(c134, plain, X0 | ~a(X1,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c135, plain, X0 | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c137, plain, X0 | ~p1(sK148(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c139, plain, X0 | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c141, plain, X0 | ~p1(sK152(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c144, plain, X0 | s1(sK154), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c145, plain, X0 | r(sK154,sK155), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c146, plain, X0 | ~s1(X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c147, plain, X0 | ~r(X1,X2) | q(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c148, plain, X0 | ~p1(X1) | ~q(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c149, plain, X0 | p1(sK161), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c150, plain, X0 | e(sK161), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c151, plain, X0 | ~e(X1) | g(X1) | s(X1,f(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c152, plain, X0 | ~e(X1) | g(X1) | c(f(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c153, plain, X0 | ~s(sK161,X1) | p1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c154, plain, X0 | ~p1(X1) | ~g(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c155, plain, X0 | ~p1(X1) | ~c(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c156, plain, X0 | ~a1(X1) | b(X1) | c(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c157, plain, X0 | a1(sK168), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c158, plain, X0 | ~b(sK168), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c159, plain, X0 | ~a1(X1) | ~c(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c160, plain, X0 | q1(f(sK170)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c161, plain, X0 | p1(f(X1)) | ~q1(X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c162, plain, X0 | ~p1(X1) | r1(X2) | ~q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c163, plain, ~r1(sK171) | ~p1(X0) | X1 | ~q1(X0) | ~r1(sK170), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c164, plain, X0 | q1(f(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c165, plain, X0 | p1(f(X1)) | ~q1(X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c166, plain, X0 | ~p1(X1) | r1(X2) | ~q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c167, plain, X0 | ~p1(X1) | ~r1(sK174) | ~q1(X1) | ~r1(sK175), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c168, plain, X0 | q1(f(X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c169, plain, X0 | p1(f(X1)) | r1(X1) | ~q1(X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c170, plain, ~r1(sK179) | ~r1(sK180) | X0 | ~q1(X1) | p1(f(X2)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c171, plain, X0 | ~p1(X1) | r1(X2) | ~q1(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(c172, plain, ~r1(sK179) | ~p1(X0) | ~r1(sK180) | ~q1(X0) | X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 15.85/2.53 cnf(d0, plain, 'Ts0' | b0 | 'Ts0' | b0, inference(resolution, [status(thm)], [c8,c7])).
% 15.85/2.53 cnf(d1, plain, ~'Ts34' | ~'Ts32' | ~'Ts29' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts28' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | p1(X0) | ~'Ts0' | ~'Ts34' | ~'Ts32' | ~'Ts29' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts28' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | p1(X1), inference(resolution, [status(thm)], [c1,c0])).
% 15.85/2.53 cnf(d2, plain, 'Ts28' | 'Ts28', inference(resolution, [status(thm)], [c137,c135])).
% 15.85/2.53 cnf(d3, plain, ~'Ts34' | ~'Ts32' | ~'Ts29' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | p1(X0) | p1(X1) | ~'Ts0', inference(resolution, [status(thm)], [d2,d1])).
% 15.85/2.53 cnf(d4, plain, 'Ts29' | 'Ts29', inference(resolution, [status(thm)], [c141,c139])).
% 15.85/2.53 cnf(d5, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | p1(X0) | p1(X1) | ~'Ts0', inference(resolution, [status(thm)], [d4,d3])).
% 15.85/2.53 cnf(d6, plain, 'Ts25' | p1(X0) | 'Ts25' | p1(X0), inference(resolution, [status(thm)], [c122,c121])).
% 15.85/2.53 cnf(d7, plain, 'Ts25' | 'Ts25' | ~p1(sK131), inference(resolution, [status(thm)], [d6,c125])).
% 15.85/2.53 cnf(d8, plain, 'Ts25' | 'Ts25', inference(resolution, [status(thm)], [d7,d6])).
% 15.85/2.53 cnf(d9, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts27' | ~'Ts31' | p1(X0) | p1(X1) | ~'Ts0', inference(resolution, [status(thm)], [d8,d5])).
% 15.85/2.53 cnf(d10, plain, 'Ts27' | 'Ts27', inference(resolution, [status(thm)], [c133,c134])).
% 15.85/2.53 cnf(d11, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | p1(X0) | p1(X1) | ~'Ts0', inference(resolution, [status(thm)], [d10,d9])).
% 15.85/2.53 cnf(d12, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | p1(X0) | ~'Ts0', inference(factoring, [status(thm)], [d11])).
% 15.85/2.53 cnf(d13, plain, 'Ts26' | p1(sK135) | 'Ts26', inference(resolution, [status(thm)], [c129,c127])).
% 15.85/2.53 cnf(d14, plain, 'Ts26' | q(sK135,sK136) | 'Ts26', inference(resolution, [status(thm)], [c130,c128])).
% 15.85/2.53 cnf(d15, plain, 'Ts26' | 'Ts26' | ~p1(sK135), inference(resolution, [status(thm)], [d14,c131])).
% 15.85/2.53 cnf(d16, plain, 'Ts26' | 'Ts26', inference(resolution, [status(thm)], [d15,d13])).
% 15.85/2.53 cnf(d17, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d16,d12])).
% 15.85/2.53 cnf(d18, plain, 'Ts30' | p1(sK154) | 'Ts30', inference(resolution, [status(thm)], [c146,c144])).
% 15.85/2.53 cnf(d19, plain, 'Ts30' | q(sK154,sK155) | 'Ts30', inference(resolution, [status(thm)], [c147,c145])).
% 15.85/2.53 cnf(d20, plain, 'Ts30' | 'Ts30' | ~p1(sK154), inference(resolution, [status(thm)], [d19,c148])).
% 15.85/2.53 cnf(d21, plain, 'Ts30' | 'Ts30', inference(resolution, [status(thm)], [d20,d18])).
% 15.85/2.53 cnf(d22, plain, ~'Ts34' | ~'Ts32' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d21,d17])).
% 15.85/2.53 cnf(d23, plain, 'Ts32' | b(sK168) | c(sK168) | 'Ts32', inference(resolution, [status(thm)], [c156,c157])).
% 15.85/2.53 cnf(d24, plain, 'Ts32' | b(sK168) | 'Ts32' | ~a1(sK168), inference(resolution, [status(thm)], [d23,c159])).
% 15.85/2.53 cnf(d25, plain, 'Ts32' | b(sK168) | 'Ts32', inference(resolution, [status(thm)], [d24,c157])).
% 15.85/2.53 cnf(d26, plain, 'Ts32' | 'Ts32', inference(resolution, [status(thm)], [d25,c158])).
% 15.85/2.53 cnf(d27, plain, ~'Ts34' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d26,d22])).
% 15.85/2.53 cnf(d28, plain, 'Ts31' | p1(f(sK161)) | 'Ts31' | ~e(sK161) | g(sK161), inference(resolution, [status(thm)], [c153,c151])).
% 15.85/2.53 cnf(d29, plain, 'Ts31' | ~p1(f(X0)) | 'Ts31' | ~e(X0) | g(X0), inference(resolution, [status(thm)], [c155,c152])).
% 15.85/2.53 cnf(d30, plain, 'Ts31' | ~e(sK161) | g(sK161) | 'Ts31' | ~e(sK161) | g(sK161), inference(resolution, [status(thm)], [d29,d28])).
% 15.85/2.53 cnf(d31, plain, 'Ts31' | g(sK161) | 'Ts31', inference(resolution, [status(thm)], [d30,c150])).
% 15.85/2.53 cnf(d32, plain, 'Ts31' | 'Ts31' | ~p1(sK161), inference(resolution, [status(thm)], [d31,c154])).
% 15.85/2.53 cnf(d33, plain, 'Ts31' | 'Ts31', inference(resolution, [status(thm)], [d32,c149])).
% 15.85/2.53 cnf(d34, plain, ~'Ts34' | ~'Ts33' | ~'Ts24' | ~'Ts35' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d33,d27])).
% 15.85/2.53 cnf(d35, plain, 'Ts33' | p1(f(X0)) | 'Ts33', inference(resolution, [status(thm)], [c161,c160])).
% 15.85/2.53 cnf(d36, plain, 'Ts33' | ~p1(f(sK170)) | r1(X0) | 'Ts33', inference(resolution, [status(thm)], [c162,c160])).
% 15.85/2.53 cnf(d37, plain, 'Ts33' | r1(X0) | 'Ts33', inference(resolution, [status(thm)], [d36,d35])).
% 15.85/2.53 cnf(d38, plain, 'Ts33' | ~p1(f(sK170)) | ~r1(sK170) | ~r1(sK171) | 'Ts33', inference(resolution, [status(thm)], [c163,c160])).
% 15.85/2.53 cnf(d39, plain, 'Ts33' | ~r1(sK170) | ~r1(sK171) | 'Ts33', inference(resolution, [status(thm)], [d38,d35])).
% 15.85/2.53 cnf(d40, plain, 'Ts33' | ~r1(sK170) | 'Ts33', inference(resolution, [status(thm)], [d39,d37])).
% 15.85/2.53 cnf(d41, plain, 'Ts33' | 'Ts33', inference(resolution, [status(thm)], [d40,d37])).
% 15.85/2.53 cnf(d42, plain, ~'Ts34' | ~'Ts24' | ~'Ts35' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d41,d34])).
% 15.85/2.53 cnf(d43, plain, 'Ts34' | p1(f(X0)) | 'Ts34', inference(resolution, [status(thm)], [c165,c164])).
% 15.85/2.53 cnf(d44, plain, 'Ts34' | ~p1(f(X0)) | r1(X1) | 'Ts34', inference(resolution, [status(thm)], [c166,c164])).
% 15.85/2.53 cnf(d45, plain, 'Ts34' | r1(X0) | 'Ts34', inference(resolution, [status(thm)], [d44,d43])).
% 15.85/2.53 cnf(d46, plain, 'Ts34' | ~p1(f(X0)) | ~r1(sK175) | ~r1(sK174) | 'Ts34', inference(resolution, [status(thm)], [c167,c164])).
% 15.85/2.53 cnf(d47, plain, 'Ts34' | ~r1(sK175) | ~r1(sK174) | 'Ts34', inference(resolution, [status(thm)], [d46,d43])).
% 15.85/2.53 cnf(d48, plain, 'Ts34' | ~r1(sK175) | 'Ts34', inference(resolution, [status(thm)], [d47,d45])).
% 15.85/2.53 cnf(d49, plain, 'Ts34' | 'Ts34', inference(resolution, [status(thm)], [d48,d45])).
% 15.85/2.53 cnf(d50, plain, ~'Ts24' | ~'Ts35' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d49,d42])).
% 15.85/2.53 cnf(d51, plain, 'Ts35' | p1(f(X0)) | r1(X0) | 'Ts35', inference(resolution, [status(thm)], [c169,c168])).
% 15.85/2.53 cnf(d52, plain, 'Ts35' | ~p1(f(X0)) | r1(X1) | 'Ts35', inference(resolution, [status(thm)], [c171,c168])).
% 15.85/2.53 cnf(d53, plain, 'Ts35' | r1(X0) | 'Ts35' | r1(X1), inference(resolution, [status(thm)], [d52,d51])).
% 15.85/2.53 cnf(d54, plain, 'Ts35' | r1(X0), inference(factoring, [status(thm)], [d53])).
% 15.85/2.53 cnf(d55, plain, 'Ts35' | p1(f(X0)) | ~r1(sK180) | ~r1(sK179) | 'Ts35', inference(resolution, [status(thm)], [c170,c168])).
% 15.85/2.53 cnf(d56, plain, 'Ts35' | ~p1(f(X0)) | ~r1(sK180) | ~r1(sK179) | 'Ts35', inference(resolution, [status(thm)], [c172,c168])).
% 15.85/2.53 cnf(d57, plain, 'Ts35' | ~r1(sK180) | ~r1(sK179) | 'Ts35' | ~r1(sK180) | ~r1(sK179), inference(resolution, [status(thm)], [d56,d55])).
% 15.85/2.53 cnf(d58, plain, 'Ts35' | ~r1(sK180) | 'Ts35', inference(resolution, [status(thm)], [d57,d54])).
% 15.85/2.53 cnf(d59, plain, 'Ts35' | 'Ts35', inference(resolution, [status(thm)], [d58,d54])).
% 15.85/2.53 cnf(d60, plain, ~'Ts24' | p1(X0) | ~'Ts0', inference(resolution, [status(thm)], [d59,d50])).
% 15.85/2.53 cnf(d61, plain, ~'Ts34' | ~'Ts32' | ~'Ts29' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d2,c3])).
% 15.85/2.53 cnf(d62, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts25' | ~'Ts35' | ~'Ts27' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d4,d61])).
% 15.85/2.53 cnf(d63, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts27' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d8,d62])).
% 15.85/2.53 cnf(d64, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts26' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d10,d63])).
% 15.85/2.53 cnf(d65, plain, ~'Ts34' | ~'Ts32' | ~'Ts30' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d16,d64])).
% 15.85/2.53 cnf(d66, plain, ~'Ts34' | ~'Ts32' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d21,d65])).
% 15.85/2.53 cnf(d67, plain, ~'Ts34' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~'Ts31' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d26,d66])).
% 15.85/2.53 cnf(d68, plain, ~'Ts34' | ~'Ts33' | ~'Ts24' | ~'Ts35' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d33,d67])).
% 15.85/2.53 cnf(d69, plain, ~'Ts34' | ~'Ts24' | ~'Ts35' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d41,d68])).
% 15.85/2.53 cnf(d70, plain, ~'Ts24' | ~'Ts35' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d49,d69])).
% 15.85/2.53 cnf(d71, plain, ~'Ts24' | ~p1(X0) | ~p1(sK37) | ~p1(sK38) | ~'Ts0', inference(resolution, [status(thm)], [d59,d70])).
% 15.85/2.53 cnf(d72, plain, ~'Ts24' | ~p1(X0) | ~p1(sK37) | ~'Ts0' | ~'Ts24' | ~'Ts0', inference(resolution, [status(thm)], [d71,d60])).
% 15.85/2.53 cnf(d73, plain, ~'Ts24' | ~p1(X0) | ~'Ts0' | ~'Ts24' | ~'Ts0', inference(resolution, [status(thm)], [d72,d60])).
% 15.85/2.53 cnf(d74, plain, ~'Ts24' | ~'Ts0' | ~'Ts24' | ~'Ts0', inference(resolution, [status(thm)], [d73,d60])).
% 15.85/2.53 cnf(d75, plain, ~'Ts24' | b0, inference(resolution, [status(thm)], [d74,d0])).
% 15.85/2.53 cnf(d76, plain, b(sK113) | 'Ts20' | 'Ts20', inference(resolution, [status(thm)], [c103,c104])).
% 15.85/2.53 cnf(d77, plain, 'Ts20' | 'Ts20', inference(resolution, [status(thm)], [d76,c105])).
% 15.85/2.53 cnf(d78, plain, 'Ts24' | p1(X0) | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts21' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d77,c118])).
% 15.85/2.53 cnf(d79, plain, b(sK117) | 'Ts21' | 'Ts21', inference(resolution, [status(thm)], [c106,c107])).
% 15.85/2.53 cnf(d80, plain, 'Ts21' | 'Ts21', inference(resolution, [status(thm)], [d79,c108])).
% 15.85/2.53 cnf(d81, plain, 'Ts24' | p1(X0) | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d80,d78])).
% 15.85/2.53 cnf(d82, plain, 'Ts24' | ~p1(X0) | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts21' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d77,c120])).
% 15.85/2.53 cnf(d83, plain, 'Ts24' | ~p1(X0) | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d80,d82])).
% 15.85/2.53 cnf(d84, plain, 'Ts24' | a(X0,X0) | a(X0,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23' | 'Ts24' | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d83,d81])).
% 15.85/2.53 cnf(d85, plain, q1(X0) | 'Ts23' | 'Ts23', inference(resolution, [status(thm)], [c114,c115])).
% 15.85/2.53 cnf(d86, plain, 'Ts23' | 'Ts23', inference(resolution, [status(thm)], [d85,c116])).
% 15.85/2.53 cnf(d87, plain, 'Ts24' | a(X0,X0) | a(X0,sK128) | a(X1,X1) | a(X1,sK128) | ~'Ts19' | ~'Ts22', inference(resolution, [status(thm)], [d86,d84])).
% 15.85/2.53 cnf(d88, plain, p1(X0) | 'Ts22' | p1(X0) | 'Ts22', inference(resolution, [status(thm)], [c110,c109])).
% 15.85/2.53 cnf(d89, plain, 'Ts22' | ~p1(sK120) | 'Ts22', inference(resolution, [status(thm)], [d88,c113])).
% 15.85/2.53 cnf(d90, plain, 'Ts22' | 'Ts22', inference(resolution, [status(thm)], [d89,d88])).
% 15.85/2.53 cnf(d91, plain, 'Ts24' | a(X0,X0) | a(X0,sK128) | a(X1,X1) | a(X1,sK128) | ~'Ts19', inference(resolution, [status(thm)], [d90,d87])).
% 15.85/2.53 cnf(d92, plain, 'Ts24' | a(sK128,sK128) | a(sK128,sK128) | a(sK128,sK128) | ~'Ts19', inference(factoring, [status(thm)], [d91])).
% 15.85/2.53 cnf(d93, plain, 'Ts24' | p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts21' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d77,c117])).
% 15.85/2.53 cnf(d94, plain, 'Ts24' | p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d80,d93])).
% 15.85/2.53 cnf(d95, plain, 'Ts24' | p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts22', inference(resolution, [status(thm)], [d86,d94])).
% 15.85/2.53 cnf(d96, plain, 'Ts24' | p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19', inference(resolution, [status(thm)], [d90,d95])).
% 15.85/2.53 cnf(d97, plain, 'Ts24' | ~'Ts19' | 'Ts24' | p1(X0) | ~a(sK128,sK128) | ~'Ts19', inference(resolution, [status(thm)], [d92,d96])).
% 15.85/2.53 cnf(d98, plain, 'Ts24' | p1(X0) | ~'Ts19' | 'Ts24' | ~'Ts19', inference(resolution, [status(thm)], [d97,d92])).
% 15.85/2.53 cnf(d99, plain, 'Ts24' | ~p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts21' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d77,c119])).
% 15.85/2.53 cnf(d100, plain, 'Ts24' | ~p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts22' | ~'Ts23', inference(resolution, [status(thm)], [d80,d99])).
% 15.85/2.53 cnf(d101, plain, 'Ts24' | ~p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19' | ~'Ts22', inference(resolution, [status(thm)], [d86,d100])).
% 15.85/2.53 cnf(d102, plain, 'Ts24' | ~p1(X0) | ~a(X1,X1) | ~a(X1,sK128) | ~'Ts19', inference(resolution, [status(thm)], [d90,d101])).
% 15.85/2.53 cnf(d103, plain, 'Ts24' | ~p1(X0) | ~a(sK128,sK128) | ~'Ts19' | 'Ts24' | ~'Ts19', inference(resolution, [status(thm)], [d102,d92])).
% 15.85/2.53 cnf(d104, plain, 'Ts24' | ~p1(X0) | ~'Ts19' | 'Ts24' | ~'Ts19', inference(resolution, [status(thm)], [d103,d92])).
% 15.85/2.53 cnf(d105, plain, 'Ts24' | ~'Ts19' | 'Ts24' | ~'Ts19', inference(resolution, [status(thm)], [d104,d98])).
% 15.85/2.53 cnf(d106, plain, ~a1(X0) | 'Ts18' | 'Ts18', inference(resolution, [status(thm)], [c99,c98])).
% 15.85/2.53 cnf(d107, plain, 'Ts18' | 'Ts18', inference(resolution, [status(thm)], [d106,c97])).
% 15.85/2.53 cnf(d108, plain, ~'Ts17' | ~b(X0) | 'Ts19', inference(resolution, [status(thm)], [d107,c102])).
% 15.85/2.53 cnf(d109, plain, ~'Ts17' | b(sK111) | 'Ts19', inference(resolution, [status(thm)], [d107,c100])).
% 15.85/2.53 cnf(d110, plain, ~'Ts17' | 'Ts19' | ~'Ts17' | 'Ts19', inference(resolution, [status(thm)], [d109,d108])).
% 15.85/2.53 cnf(d111, plain, p1(X0) | ~'Ts16' | a(sK97,sK98) | 'Ts17' | p1(X1) | ~'Ts16' | a(sK97,sK98) | 'Ts17', inference(resolution, [status(thm)], [c91,c89])).
% 15.85/2.53 cnf(d112, plain, p1(X0) | ~'Ts16' | a(sK97,sK98) | 'Ts17', inference(factoring, [status(thm)], [d111])).
% 15.85/2.53 cnf(d113, plain, p1(X0) | ~'Ts16' | 'Ts17' | p1(X1) | ~'Ts16' | ~a(X2,X3) | 'Ts17', inference(resolution, [status(thm)], [d112,c93])).
% 15.85/2.53 cnf(d114, plain, p1(X0) | p1(X1) | ~'Ts16' | 'Ts17' | p1(X2) | ~'Ts16' | 'Ts17', inference(resolution, [status(thm)], [d113,d112])).
% 15.85/2.53 cnf(d115, plain, p1(X0) | p1(X1) | ~'Ts16' | 'Ts17', inference(factoring, [status(thm)], [d114])).
% 15.85/2.53 cnf(d116, plain, p1(X0) | ~'Ts16' | 'Ts17', inference(factoring, [status(thm)], [d115])).
% 15.85/2.53 cnf(d117, plain, ~p1(sK106) | ~p1(sK105) | ~'Ts16' | a(sK97,sK98) | 'Ts17' | ~p1(sK106) | ~p1(sK105) | ~'Ts16' | a(sK97,sK98) | 'Ts17', inference(resolution, [status(thm)], [c92,c90])).
% 15.85/2.53 cnf(d118, plain, ~p1(sK106) | ~p1(sK105) | ~'Ts16' | 'Ts17' | ~p1(sK106) | ~p1(sK105) | ~'Ts16' | ~a(X0,X1) | 'Ts17', inference(resolution, [status(thm)], [d117,c94])).
% 15.85/2.53 cnf(d119, plain, ~p1(sK106) | ~p1(sK105) | ~'Ts16' | 'Ts17' | ~p1(sK106) | ~p1(sK105) | ~'Ts16' | 'Ts17', inference(resolution, [status(thm)], [d118,d117])).
% 15.85/2.53 cnf(d120, plain, ~'Ts16' | 'Ts17' | ~p1(sK106) | ~'Ts16' | 'Ts17', inference(resolution, [status(thm)], [d116,d119])).
% 15.85/2.53 cnf(d121, plain, ~'Ts16' | 'Ts17' | ~'Ts16' | 'Ts17', inference(resolution, [status(thm)], [d120,d116])).
% 15.85/2.53 cnf(d122, plain, p1(sK96) | p1(sK93) | ~'Ts15' | 'Ts16', inference(factoring, [status(thm)], [c82])).
% 15.85/2.53 cnf(d123, plain, p1(sK93) | ~'Ts15' | 'Ts16' | p1(X0) | p1(sK93) | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d122,c81])).
% 15.85/2.53 cnf(d124, plain, p1(sK93) | ~'Ts15' | 'Ts16', inference(factoring, [status(thm)], [d123])).
% 15.85/2.53 cnf(d125, plain, ~'Ts15' | 'Ts16' | p1(X0) | ~p1(X1) | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d124,c83])).
% 15.85/2.53 cnf(d126, plain, p1(X0) | ~'Ts15' | 'Ts16' | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d125,d124])).
% 15.85/2.53 cnf(d127, plain, ~'Ts15' | 'Ts16' | ~p1(X0) | ~p1(X1) | ~p1(sK92) | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d126,c87])).
% 15.85/2.53 cnf(d128, plain, ~p1(X0) | ~p1(X1) | ~'Ts15' | 'Ts16' | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d127,d126])).
% 15.85/2.53 cnf(d129, plain, ~p1(X0) | ~'Ts15' | 'Ts16' | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d128,d126])).
% 15.85/2.53 cnf(d130, plain, ~'Ts15' | 'Ts16' | ~'Ts15' | 'Ts16', inference(resolution, [status(thm)], [d129,d126])).
% 15.85/2.53 cnf(d131, plain, p1(sK84) | ~p(X0,X1) | ~'Ts14' | 'Ts15' | p(X2,X1), inference(resolution, [status(thm)], [c78,c9])).
% 15.85/2.53 cnf(d132, plain, p1(sK84) | p(X0,sK87(X1)) | ~'Ts14' | 'Ts15' | p(X1,X0), inference(resolution, [status(thm)], [c77,c9])).
% 15.85/2.53 cnf(d133, plain, p1(sK84) | ~p(X0,X1) | ~'Ts14' | 'Ts15' | p(X1,X2), inference(resolution, [status(thm)], [c78,c10])).
% 15.85/2.53 cnf(d134, plain, p1(sK84) | p(sK87(X0),X1) | ~'Ts14' | 'Ts15' | p1(sK84) | p(X0,X2) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d133,d132])).
% 15.85/2.53 cnf(d135, plain, p1(sK84) | p(X0,X1) | ~'Ts14' | 'Ts15' | p1(sK84) | p(X2,X3) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d134,d131])).
% 15.85/2.53 cnf(d136, plain, p1(sK84) | p(X0,X1) | ~'Ts14' | 'Ts15', inference(factoring, [status(thm)], [d135])).
% 15.85/2.53 cnf(d137, plain, p1(sK84) | ~p(X0,X1) | ~'Ts14' | 'Ts15' | ~p(X1,sK87(X2)), inference(resolution, [status(thm)], [c78,c11])).
% 15.85/2.53 cnf(d138, plain, p1(sK84) | ~'Ts14' | 'Ts15' | p1(sK84) | ~p(X0,X1) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d136,d137])).
% 15.85/2.53 cnf(d139, plain, p1(sK84) | ~'Ts14' | 'Ts15' | p1(sK84) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d138,d136])).
% 15.85/2.53 cnf(d140, plain, ~p1(X0) | ~p(X1,X2) | ~'Ts14' | 'Ts15' | p(X3,X2), inference(resolution, [status(thm)], [c80,c9])).
% 15.85/2.53 cnf(d141, plain, ~p1(X0) | p(X1,sK87(X2)) | ~'Ts14' | 'Ts15' | p(X2,X1), inference(resolution, [status(thm)], [c79,c9])).
% 15.85/2.53 cnf(d142, plain, ~'Ts14' | 'Ts15' | p(X0,X1) | p(X1,sK87(X0)) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d139,d141])).
% 15.85/2.53 cnf(d143, plain, p(X0,X1) | ~'Ts14' | 'Ts15' | ~p1(X2) | p(X3,sK87(X0)) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d142,d140])).
% 15.85/2.53 cnf(d144, plain, p(X0,sK87(X1)) | p(X1,X2) | ~'Ts14' | 'Ts15' | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d143,d139])).
% 15.85/2.53 cnf(d145, plain, p(X0,sK87(X0)) | ~'Ts14' | 'Ts15', inference(factoring, [status(thm)], [d144])).
% 15.85/2.53 cnf(d146, plain, ~p1(X0) | ~p(X1,X2) | ~'Ts14' | 'Ts15' | ~p(X2,sK87(X3)), inference(resolution, [status(thm)], [c80,c11])).
% 15.85/2.53 cnf(d147, plain, ~'Ts14' | 'Ts15' | ~p1(X0) | ~p(X1,X2) | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d145,d146])).
% 15.85/2.53 cnf(d148, plain, ~p1(X0) | ~'Ts14' | 'Ts15' | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d147,d145])).
% 15.85/2.53 cnf(d149, plain, ~'Ts14' | 'Ts15' | ~'Ts14' | 'Ts15', inference(resolution, [status(thm)], [d148,d139])).
% 15.85/2.53 cnf(d150, plain, r1(X0) | 'Ts10' | 'Ts10', inference(resolution, [status(thm)], [c53,c54])).
% 15.85/2.53 cnf(d151, plain, 'Ts10' | 'Ts10', inference(resolution, [status(thm)], [d150,c55])).
% 15.85/2.53 cnf(d152, plain, p1(X0) | p1(sK83) | ~'Ts9' | ~'Ts11' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d151,c73])).
% 15.85/2.53 cnf(d153, plain, p1(X0) | ~p1(X1) | ~'Ts9' | ~'Ts11' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d151,c74])).
% 15.85/2.53 cnf(d154, plain, p1(X0) | ~'Ts9' | ~'Ts11' | ~'Ts12' | ~'Ts13' | 'Ts14' | p1(X1) | ~'Ts9' | ~'Ts11' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d153,d152])).
% 15.85/2.53 cnf(d155, plain, p1(sK67) | 'Ts11' | 'Ts11', inference(resolution, [status(thm)], [c58,c57])).
% 15.85/2.53 cnf(d156, plain, 'Ts11' | q1(sK67) | 'Ts11', inference(resolution, [status(thm)], [d155,c56])).
% 15.85/2.53 cnf(d157, plain, 'Ts11' | 'Ts11', inference(resolution, [status(thm)], [d156,c59])).
% 15.85/2.53 cnf(d158, plain, p1(X0) | p1(X1) | ~'Ts9' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d157,d154])).
% 15.85/2.53 cnf(d159, plain, p1(X0) | 'Ts12' | p1(X0) | 'Ts12', inference(resolution, [status(thm)], [c61,c60])).
% 15.85/2.53 cnf(d160, plain, 'Ts12' | ~p1(sK71) | 'Ts12', inference(resolution, [status(thm)], [d159,c64])).
% 15.85/2.53 cnf(d161, plain, 'Ts12' | 'Ts12', inference(resolution, [status(thm)], [d160,d159])).
% 15.85/2.53 cnf(d162, plain, p1(X0) | p1(X1) | ~'Ts9' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d161,d158])).
% 15.85/2.53 cnf(d163, plain, p1(X0) | ~'Ts9' | ~'Ts13' | 'Ts14', inference(factoring, [status(thm)], [d162])).
% 15.85/2.53 cnf(d164, plain, ~p1(X0) | ~p1(sK81(X1)) | ~'Ts9' | ~'Ts11' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d151,c76])).
% 15.85/2.53 cnf(d165, plain, ~p1(X0) | ~p1(sK81(X1)) | ~'Ts9' | ~'Ts12' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d157,d164])).
% 15.85/2.53 cnf(d166, plain, ~p1(X0) | ~p1(sK81(X1)) | ~'Ts9' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d161,d165])).
% 15.85/2.53 cnf(d167, plain, ~p1(X0) | ~'Ts9' | ~'Ts13' | 'Ts14' | ~'Ts9' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d166,d163])).
% 15.85/2.53 cnf(d168, plain, ~'Ts9' | ~'Ts13' | 'Ts14' | ~'Ts9' | ~'Ts13' | 'Ts14', inference(resolution, [status(thm)], [d167,d163])).
% 15.85/2.53 cnf(d169, plain, eq(X0,X1) | 'a$umember$uof'(sK77(X0,X1),X1) | 'Ts13' | ~eq(X2,X0) | 'a$umember$uof'(sK77(X0,X1),X2) | 'Ts13', inference(resolution, [status(thm)], [c68,c66])).
% 15.85/2.53 cnf(d170, plain, ~eq(X0,X1) | eq(X1,X0) | 'a$umember$uof'(sK77(X1,X0),X0) | 'Ts13', inference(factoring, [status(thm)], [d169])).
% 15.85/2.53 cnf(d171, plain, eq(X0,X1) | 'a$umember$uof'(sK77(X0,X1),X0) | 'Ts13' | ~eq(X1,X2) | 'a$umember$uof'(sK77(X0,X1),X2) | 'Ts13', inference(resolution, [status(thm)], [c68,c65])).
% 15.85/2.53 cnf(d172, plain, ~eq(X0,X1) | eq(X1,X0) | 'a$umember$uof'(sK77(X1,X0),X1) | 'Ts13', inference(factoring, [status(thm)], [d171])).
% 15.85/2.53 cnf(d173, plain, eq(X0,X1) | ~eq(X1,X0) | 'Ts13' | eq(X0,X1) | ~'a$umember$uof'(sK77(X0,X1),X1) | 'Ts13', inference(resolution, [status(thm)], [d172,c69])).
% 15.85/2.53 cnf(d174, plain, ~eq(X0,X1) | eq(X1,X0) | 'Ts13' | eq(X1,X0) | ~eq(X0,X1) | 'Ts13', inference(resolution, [status(thm)], [d173,d170])).
% 15.85/2.53 cnf(d175, plain, eq(sK79,sK78) | 'Ts13' | 'Ts13', inference(resolution, [status(thm)], [d174,c71])).
% 15.85/2.53 cnf(d176, plain, 'Ts13' | 'Ts13', inference(resolution, [status(thm)], [d175,c72])).
% 15.85/2.53 cnf(d177, plain, ~'Ts9' | 'Ts14', inference(resolution, [status(thm)], [d176,d168])).
% 15.85/2.53 cnf(d178, plain, p1(z) | ~'Ts8' | 'Ts9' | p1(z) | ~'Ts8' | 'Ts9', inference(resolution, [status(thm)], [c51,c49])).
% 15.85/2.53 cnf(d179, plain, ~p1(z) | ~'Ts8' | 'Ts9' | ~p1(z) | ~'Ts8' | 'Ts9', inference(resolution, [status(thm)], [c52,c50])).
% 15.85/2.53 cnf(d180, plain, ~'Ts8' | 'Ts9' | ~'Ts8' | 'Ts9', inference(resolution, [status(thm)], [d179,d178])).
% 15.85/2.53 cnf(d181, plain, p1(sK54) | ~'Ts7' | 'Ts8' | p1(sK54) | ~'Ts7' | 'Ts8', inference(resolution, [status(thm)], [c46,c45])).
% 15.85/2.53 cnf(d182, plain, ~'Ts7' | 'Ts8' | p(X0,X1) | ~'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d181,c47])).
% 15.85/2.53 cnf(d183, plain, ~'Ts7' | 'Ts8' | ~p1(X0) | ~'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d182,c48])).
% 15.85/2.53 cnf(d184, plain, ~'Ts7' | 'Ts8' | ~'Ts7' | 'Ts8', inference(resolution, [status(thm)], [d183,d181])).
% 15.85/2.53 cnf(d185, plain, 'Ts6' | 'Ts6', inference(resolution, [status(thm)], [c40,c39])).
% 15.85/2.53 cnf(d186, plain, ~'Ts2' | ~r1(X0) | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d185,c44])).
% 15.85/2.53 cnf(d187, plain, 'Ts3' | 'Ts3' | ~s1(sK45), inference(resolution, [status(thm)], [c24,c22])).
% 15.85/2.53 cnf(d188, plain, 'Ts3' | 'Ts3', inference(resolution, [status(thm)], [d187,c23])).
% 15.85/2.53 cnf(d189, plain, ~'Ts2' | ~r1(X0) | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d188,d186])).
% 15.85/2.53 cnf(d190, plain, ~p1(X0) | ~'Ts2' | q1(X0) | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d185,c41])).
% 15.85/2.53 cnf(d191, plain, p1(X0) | ~'Ts2' | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d185,c43])).
% 15.85/2.53 cnf(d192, plain, ~'Ts2' | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7' | ~'Ts2' | q1(X0) | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d191,d190])).
% 15.85/2.53 cnf(d193, plain, ~'Ts2' | q1(X0) | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d188,d192])).
% 15.85/2.53 cnf(d194, plain, ~'Ts2' | r1(sK52) | ~q1(sK52) | ~'Ts3' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d185,c42])).
% 15.85/2.53 cnf(d195, plain, ~'Ts2' | r1(sK52) | ~q1(sK52) | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d188,d194])).
% 15.85/2.53 cnf(d196, plain, ~'Ts2' | r1(sK52) | ~'Ts4' | ~'Ts5' | 'Ts7' | ~'Ts2' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d195,d193])).
% 15.85/2.53 cnf(d197, plain, ~'Ts2' | ~'Ts4' | ~'Ts5' | 'Ts7' | ~'Ts2' | ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d196,d189])).
% 15.85/2.53 cnf(d198, plain, 'Ts2' | q(f(sK41),sK41) | 'Ts2' | r1(sK41), inference(resolution, [status(thm)], [c14,c12])).
% 15.85/2.53 cnf(d199, plain, 'Ts2' | r1(sK41) | ~p(f(sK41),sK41) | 'Ts2', inference(resolution, [status(thm)], [d198,c15])).
% 15.85/2.53 cnf(d200, plain, 'Ts2' | r1(sK41) | 'Ts2' | r1(sK41), inference(resolution, [status(thm)], [d199,c12])).
% 15.85/2.53 cnf(d201, plain, 'Ts2' | q(f(sK41),sK41) | 'Ts2' | ~r1(X0), inference(resolution, [status(thm)], [c14,c13])).
% 15.85/2.53 cnf(d202, plain, 'Ts2' | 'Ts2' | q(f(sK41),sK41), inference(resolution, [status(thm)], [d200,d201])).
% 15.85/2.53 cnf(d203, plain, 'Ts2' | ~p(f(sK41),sK41) | 'Ts2', inference(resolution, [status(thm)], [d202,c15])).
% 15.85/2.53 cnf(d204, plain, 'Ts2' | 'Ts2' | ~r1(sK41), inference(resolution, [status(thm)], [d203,c13])).
% 15.85/2.53 cnf(d205, plain, 'Ts2' | 'Ts2', inference(resolution, [status(thm)], [d204,d200])).
% 15.85/2.53 cnf(d206, plain, ~'Ts4' | ~'Ts5' | 'Ts7', inference(resolution, [status(thm)], [d205,d197])).
% 15.85/2.53 cnf(d207, plain, ~'Ts2' | ~'Ts4' | 'Ts7' | a0 | b0, inference(resolution, [status(thm)], [d197,c32])).
% 15.85/2.53 cnf(d208, plain, a0 | b0 | ~'Ts2' | 'Ts7' | b0, inference(resolution, [status(thm)], [d207,c26])).
% 15.85/2.53 cnf(d209, plain, a0 | b0 | 'Ts7', inference(resolution, [status(thm)], [d205,d208])).
% 15.85/2.53 cnf(d210, plain, a0 | b0 | 'Ts8', inference(resolution, [status(thm)], [d209,d184])).
% 15.85/2.53 cnf(d211, plain, a0 | b0 | 'Ts9', inference(resolution, [status(thm)], [d210,d180])).
% 15.85/2.53 cnf(d212, plain, 'Ts14' | a0 | b0, inference(resolution, [status(thm)], [d177,d211])).
% 15.85/2.53 cnf(d213, plain, a0 | b0 | 'Ts15', inference(resolution, [status(thm)], [d212,d149])).
% 15.85/2.53 cnf(d214, plain, b0 | 'Ts15' | 'Ts5', inference(resolution, [status(thm)], [d213,c35])).
% 15.85/2.53 cnf(d215, plain, b0 | 'Ts15' | ~'Ts4' | 'Ts7', inference(resolution, [status(thm)], [d214,d206])).
% 15.85/2.53 cnf(d216, plain, b0 | 'Ts7' | 'Ts15' | b0, inference(resolution, [status(thm)], [d215,c26])).
% 15.85/2.53 cnf(d217, plain, b0 | 'Ts15' | 'Ts8', inference(resolution, [status(thm)], [d216,d184])).
% 15.85/2.53 cnf(d218, plain, b0 | 'Ts15' | 'Ts9', inference(resolution, [status(thm)], [d217,d180])).
% 15.85/2.53 cnf(d219, plain, b0 | 'Ts15' | 'Ts14', inference(resolution, [status(thm)], [d218,d177])).
% 15.85/2.53 cnf(d220, plain, b0 | 'Ts15' | 'Ts15', inference(resolution, [status(thm)], [d219,d149])).
% 15.85/2.53 cnf(d221, plain, b0 | 'Ts16', inference(resolution, [status(thm)], [d220,d130])).
% 15.85/2.53 cnf(d222, plain, 'Ts16' | 'Ts5', inference(resolution, [status(thm)], [d221,c36])).
% 15.85/2.53 cnf(d223, plain, 'Ts16' | ~'Ts4' | 'Ts7', inference(resolution, [status(thm)], [d222,d206])).
% 15.85/2.53 cnf(d224, plain, 'Ts16' | ~a0 | 'Ts4', inference(resolution, [status(thm)], [d221,c29])).
% 15.85/2.53 cnf(d225, plain, 'Ts7' | 'Ts16' | a0, inference(resolution, [status(thm)], [d223,c25])).
% 15.85/2.53 cnf(d226, plain, a0 | 'Ts16' | 'Ts8', inference(resolution, [status(thm)], [d225,d184])).
% 15.85/2.53 cnf(d227, plain, a0 | 'Ts16' | 'Ts9', inference(resolution, [status(thm)], [d226,d180])).
% 15.85/2.53 cnf(d228, plain, a0 | 'Ts16' | 'Ts14', inference(resolution, [status(thm)], [d227,d177])).
% 15.85/2.53 cnf(d229, plain, a0 | 'Ts16' | 'Ts15', inference(resolution, [status(thm)], [d228,d149])).
% 15.85/2.53 cnf(d230, plain, 'Ts15' | 'Ts16' | 'Ts4' | 'Ts16', inference(resolution, [status(thm)], [d229,d224])).
% 15.85/2.53 cnf(d231, plain, 'Ts15' | 'Ts16' | 'Ts7' | 'Ts16', inference(resolution, [status(thm)], [d230,d223])).
% 15.85/2.53 cnf(d232, plain, 'Ts15' | 'Ts16' | 'Ts8', inference(resolution, [status(thm)], [d231,d184])).
% 15.85/2.53 cnf(d233, plain, 'Ts15' | 'Ts16' | 'Ts9', inference(resolution, [status(thm)], [d232,d180])).
% 15.85/2.53 cnf(d234, plain, 'Ts15' | 'Ts16' | 'Ts14', inference(resolution, [status(thm)], [d233,d177])).
% 15.85/2.53 cnf(d235, plain, 'Ts15' | 'Ts16' | 'Ts15', inference(resolution, [status(thm)], [d234,d149])).
% 15.85/2.53 cnf(d236, plain, 'Ts16' | 'Ts16', inference(resolution, [status(thm)], [d235,d130])).
% 15.85/2.53 cnf(d237, plain, 'Ts17', inference(resolution, [status(thm)], [d236,d121])).
% 15.85/2.53 cnf(d238, plain, 'Ts19', inference(resolution, [status(thm)], [d237,d110])).
% 15.85/2.53 cnf(d239, plain, 'Ts24', inference(resolution, [status(thm)], [d238,d105])).
% 15.85/2.53 cnf(d240, plain, b0, inference(resolution, [status(thm)], [d239,d75])).
% 15.85/2.53 cnf(d241, plain, 'Ts0' | ~q0, inference(resolution, [status(thm)], [d240,c6])).
% 15.85/2.53 cnf(d242, plain, ~'Ts0', inference(resolution, [status(thm)], [d239,d74])).
% 15.85/2.53 cnf(d243, plain, ~q0, inference(resolution, [status(thm)], [d242,d241])).
% 15.85/2.53 cnf(d244, plain, 'Ts0' | q0, inference(resolution, [status(thm)], [d240,c5])).
% 15.85/2.53 cnf(d245, plain, q0, inference(resolution, [status(thm)], [d242,d244])).
% 15.85/2.53 cnf(d246, plain, $false, inference(resolution, [status(thm)], [d245,d243])).
% 15.85/2.53 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------