%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS081+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 07:45:07 AM UTC 2026
% Result : Unsatisfiable 29.12s 6.97s
% Output : CNFRefutation 29.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KRS081+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n019.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Fri Sep 25 19:38:49 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.12/6.97 % SZS status Unsatisfiable for theBenchmark.p
% 29.12/6.97 % SZS output start CNFRefutation for theBenchmark.p
% 29.12/6.97 fof(axiom_2, axiom, ! [X0] : ((cUnsatisfiable(X0) <=> (? [X1] : ((rr(X0,X1) & cp3(X1))) & (? [X1] : ((rr(X0,X1) & (cp4(X1) & cp(X1)))) & (? [X1] : ((rr(X0,X1) & cp4(X1))) & (? [X1] : ((rr(X0,X1) & (cp2(X1) & cp(X1)))) & (? [X1] : ((rr(X0,X1) & cp5(X1))) & (? [X1] : ((rr(X0,X1) & (cp(X1) & cp3(X1)))) & (? [X1] : ((rr(X0,X1) & cp1(X1))) & (! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : (((rr(X0,X2) & (rr(X0,X3) & (rr(X0,X4) & (rr(X0,X5) & rr(X0,X6))))) => (X2 = X3 | (X2 = X4 | (X2 = X5 | (X2 = X6 | (X3 = X4 | (X3 = X5 | (X3 = X6 | (X4 = X5 | (X4 = X6 | X5 = X6))))))))))) & (? [X1] : ((rr(X0,X1) & (cp1(X1) & cp(X1)))) & ? [X1] : ((rr(X0,X1) & cp2(X1))))))))))))))).
% 29.12/6.97 fof(axiom_3, axiom, ! [X0] : ((cp1(X0) => ~((cp2(X0) | (cp4(X0) | (cp5(X0) | cp3(X0)))))))).
% 29.12/6.97 fof(axiom_4, axiom, ! [X0] : ((cp2(X0) => ~((cp4(X0) | (cp5(X0) | cp3(X0))))))).
% 29.12/6.97 fof(axiom_5, axiom, ! [X0] : ((cp3(X0) => ~((cp4(X0) | cp5(X0)))))).
% 29.12/6.97 fof(axiom_6, axiom, ! [X0] : ((cp4(X0) => ~cp5(X0)))).
% 29.12/6.97 fof(axiom_7, axiom, cUnsatisfiable('i2003$u11$u14$u17$u19$u24236')).
% 29.12/6.97 cnf(c17, plain, ~cUnsatisfiable(X0) | X1(X0), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c19, plain, ~X0(X1) | rr(X1,sK38(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c20, plain, ~X0(X1) | cp5(sK38(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c21, plain, ~X0(X1) | rr(X1,sK39(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c23, plain, ~X0(X1) | cp1(sK39(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c24, plain, ~rr(X0,X1) | ~rr(X0,X2) | X2 = X3 | X3 = X1 | X2 = X1 | ~rr(X0,X4) | ~rr(X0,X5) | X2 = X4 | X2 = X5 | X5 = X4 | X3 = X5 | ~rr(X0,X3) | X3 = X4 | X1 = X4 | X5 = X1 | ~X6(X0), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c25, plain, ~X0(X1) | rr(X1,sK45(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c26, plain, ~X0(X1) | cp3(sK45(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c28, plain, ~X0(X1) | rr(X1,sK46(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c30, plain, ~X0(X1) | cp2(sK46(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c31, plain, ~X0(X1) | rr(X1,sK47(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c33, plain, ~X0(X1) | cp4(sK47(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 29.12/6.97 cnf(c49, plain, ~cp1(X0) | ~cp2(X0), inference(clausification, [status(esa)], [axiom_3])).
% 29.12/6.97 cnf(c50, plain, ~cp1(X0) | ~cp5(X0), inference(clausification, [status(esa)], [axiom_3])).
% 29.12/6.97 cnf(c51, plain, ~cp1(X0) | ~cp3(X0), inference(clausification, [status(esa)], [axiom_3])).
% 29.12/6.97 cnf(c52, plain, ~cp1(X0) | ~cp4(X0), inference(clausification, [status(esa)], [axiom_3])).
% 29.12/6.97 cnf(c53, plain, ~cp2(X0) | ~cp4(X0), inference(clausification, [status(esa)], [axiom_4])).
% 29.12/6.97 cnf(c54, plain, ~cp2(X0) | ~cp3(X0), inference(clausification, [status(esa)], [axiom_4])).
% 29.12/6.97 cnf(c55, plain, ~cp2(X0) | ~cp5(X0), inference(clausification, [status(esa)], [axiom_4])).
% 29.12/6.97 cnf(c56, plain, ~cp3(X0) | ~cp4(X0), inference(clausification, [status(esa)], [axiom_5])).
% 29.12/6.97 cnf(c57, plain, ~cp3(X0) | ~cp5(X0), inference(clausification, [status(esa)], [axiom_5])).
% 29.12/6.97 cnf(c58, plain, ~cp4(X0) | ~cp5(X0), inference(clausification, [status(esa)], [axiom_6])).
% 29.12/6.97 cnf(c59, plain, cUnsatisfiable('i2003$u11$u14$u17$u19$u24236'), inference(clausification, [status(esa)], [axiom_7])).
% 29.12/6.97 cnf(d0, plain, 'Ts30'('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [c17,c59])).
% 29.12/6.97 cnf(d1, plain, cp4(sK47('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c33,d0])).
% 29.12/6.97 cnf(d2, plain, cp2(sK46('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c30,d0])).
% 29.12/6.97 cnf(d3, plain, cp3(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c26,d0])).
% 29.12/6.97 cnf(d4, plain, cp5(sK38('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c20,d0])).
% 29.12/6.97 cnf(d5, plain, rr('i2003$u11$u14$u17$u19$u24236',sK46('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c28,d0])).
% 29.12/6.97 cnf(d6, plain, rr('i2003$u11$u14$u17$u19$u24236',sK47('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c31,d0])).
% 29.12/6.97 cnf(d7, plain, rr('i2003$u11$u14$u17$u19$u24236',sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c25,d0])).
% 29.12/6.97 cnf(d8, plain, rr('i2003$u11$u14$u17$u19$u24236',sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c21,d0])).
% 29.12/6.97 cnf(d9, plain, rr('i2003$u11$u14$u17$u19$u24236',sK38('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c19,d0])).
% 29.12/6.97 cnf(d10, plain, sK38('i2003$u11$u14$u17$u19$u24236') = X0 | sK38('i2003$u11$u14$u17$u19$u24236') = X1 | sK38('i2003$u11$u14$u17$u19$u24236') = X2 | sK38('i2003$u11$u14$u17$u19$u24236') = X3 | X0 = X1 | X2 = X0 | X2 = X1 | X3 = X0 | X3 = X1 | X3 = X2 | ~rr('i2003$u11$u14$u17$u19$u24236',X0) | ~rr('i2003$u11$u14$u17$u19$u24236',X1) | ~rr('i2003$u11$u14$u17$u19$u24236',X2) | ~rr('i2003$u11$u14$u17$u19$u24236',X3) | ~'Ts30'('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d9,c24])).
% 29.12/6.97 cnf(d11, plain, X0 = X1 | X0 = X2 | X0 = X3 | X1 = X2 | X1 = X3 | X3 = X2 | sK38('i2003$u11$u14$u17$u19$u24236') = X0 | sK38('i2003$u11$u14$u17$u19$u24236') = X1 | sK38('i2003$u11$u14$u17$u19$u24236') = X2 | sK38('i2003$u11$u14$u17$u19$u24236') = X3 | ~rr('i2003$u11$u14$u17$u19$u24236',X0) | ~rr('i2003$u11$u14$u17$u19$u24236',X1) | ~rr('i2003$u11$u14$u17$u19$u24236',X2) | ~rr('i2003$u11$u14$u17$u19$u24236',X3), inference(resolution, [status(thm)], [d0,d10])).
% 29.12/6.97 cnf(d12, plain, sK39('i2003$u11$u14$u17$u19$u24236') = X0 | X1 = sK39('i2003$u11$u14$u17$u19$u24236') | X1 = X0 | X2 = sK39('i2003$u11$u14$u17$u19$u24236') | X2 = X0 | X2 = X1 | sK38('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = X0 | sK38('i2003$u11$u14$u17$u19$u24236') = X1 | sK38('i2003$u11$u14$u17$u19$u24236') = X2 | ~rr('i2003$u11$u14$u17$u19$u24236',X0) | ~rr('i2003$u11$u14$u17$u19$u24236',X1) | ~rr('i2003$u11$u14$u17$u19$u24236',X2), inference(resolution, [status(thm)], [d11,d8])).
% 29.12/6.97 cnf(d13, plain, sK45('i2003$u11$u14$u17$u19$u24236') = X0 | sK45('i2003$u11$u14$u17$u19$u24236') = X1 | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | X0 = X1 | X0 = sK39('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK45('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = X0 | sK38('i2003$u11$u14$u17$u19$u24236') = X1 | sK38('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = X1 | ~rr('i2003$u11$u14$u17$u19$u24236',X0) | ~rr('i2003$u11$u14$u17$u19$u24236',X1), inference(resolution, [status(thm)], [d12,d7])).
% 29.12/6.97 cnf(d14, plain, X0 = sK47('i2003$u11$u14$u17$u19$u24236') | X0 = sK39('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = X0 | sK38('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK45('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = X0 | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | ~rr('i2003$u11$u14$u17$u19$u24236',X0), inference(resolution, [status(thm)], [d13,d6])).
% 29.12/6.97 cnf(d15, plain, sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK45('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d14,d5])).
% 29.12/6.97 cnf(d16, plain, cp5(sK39('i2003$u11$u14$u17$u19$u24236')) | sK38('i2003$u11$u14$u17$u19$u24236') = sK45('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d15,d4])).
% 29.12/6.97 cnf(d17, plain, cp1(sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [c23,d0])).
% 29.12/6.97 cnf(d18, plain, ~cp5(sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d17,c50])).
% 29.12/6.97 cnf(d19, plain, sK38('i2003$u11$u14$u17$u19$u24236') = sK45('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d18,d16])).
% 29.12/6.97 cnf(d20, plain, cp5(sK45('i2003$u11$u14$u17$u19$u24236')) | sK38('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d19,d4])).
% 29.12/6.97 cnf(d21, plain, ~cp5(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d3,c57])).
% 29.12/6.97 cnf(d22, plain, sK38('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d21,d20])).
% 29.12/6.97 cnf(d23, plain, cp5(sK46('i2003$u11$u14$u17$u19$u24236')) | sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d22,d4])).
% 29.12/6.97 cnf(d24, plain, ~cp5(sK46('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d2,c55])).
% 29.12/6.97 cnf(d25, plain, sK38('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d24,d23])).
% 29.12/6.97 cnf(d26, plain, cp5(sK47('i2003$u11$u14$u17$u19$u24236')) | sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d25,d4])).
% 29.12/6.97 cnf(d27, plain, ~cp5(sK47('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d1,c58])).
% 29.12/6.97 cnf(d28, plain, sK39('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d27,d26])).
% 29.12/6.97 cnf(d29, plain, cp4(sK39('i2003$u11$u14$u17$u19$u24236')) | sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d28,d1])).
% 29.12/6.97 cnf(d30, plain, ~cp4(sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d17,c52])).
% 29.12/6.97 cnf(d31, plain, sK45('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d30,d29])).
% 29.12/6.97 cnf(d32, plain, cp3(sK39('i2003$u11$u14$u17$u19$u24236')) | sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d31,d3])).
% 29.12/6.97 cnf(d33, plain, ~cp3(sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d17,c51])).
% 29.12/6.97 cnf(d34, plain, sK45('i2003$u11$u14$u17$u19$u24236') = sK46('i2003$u11$u14$u17$u19$u24236') | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(resolution, [status(thm)], [d33,d32])).
% 29.12/6.97 cnf(d35, plain, cp2(sK45('i2003$u11$u14$u17$u19$u24236')) | sK45('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236'), inference(superposition, [status(thm)], [d34,d2])).
% 29.12/6.97 cnf(d36, plain, cp4(sK45('i2003$u11$u14$u17$u19$u24236')) | sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(superposition, [status(thm)], [d35,d1])).
% 29.12/6.97 cnf(d37, plain, ~cp4(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d3,c56])).
% 29.12/6.97 cnf(d38, plain, sK46('i2003$u11$u14$u17$u19$u24236') = sK39('i2003$u11$u14$u17$u19$u24236') | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d37,d36])).
% 29.12/6.97 cnf(d39, plain, cp2(sK39('i2003$u11$u14$u17$u19$u24236')) | sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(superposition, [status(thm)], [d38,d2])).
% 29.12/6.97 cnf(d40, plain, ~cp2(sK39('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d17,c49])).
% 29.12/6.97 cnf(d41, plain, sK46('i2003$u11$u14$u17$u19$u24236') = sK47('i2003$u11$u14$u17$u19$u24236') | cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d40,d39])).
% 29.12/6.97 cnf(d42, plain, cp4(sK46('i2003$u11$u14$u17$u19$u24236')) | cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(superposition, [status(thm)], [d41,d1])).
% 29.12/6.97 cnf(d43, plain, ~cp4(sK46('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d2,c53])).
% 29.12/6.97 cnf(d44, plain, cp2(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d43,d42])).
% 29.12/6.97 cnf(d45, plain, ~cp3(sK45('i2003$u11$u14$u17$u19$u24236')), inference(resolution, [status(thm)], [d44,c54])).
% 29.12/6.97 cnf(d46, plain, $false, inference(resolution, [status(thm)], [d3,d45])).
% 29.12/6.97 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------