%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWX033+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:15:25 AM UTC 2026
% Result : Theorem 94.09s 51.57s
% Output : CNFRefutation 94.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX033+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 16:46:40 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 94.09/51.57 % SZS status Theorem for theBenchmark.p
% 94.09/51.57 % SZS output start CNFRefutation for theBenchmark.p
% 94.09/51.57 fof(id1, axiom, ! [X0] : '\'0\'' != s(X0)).
% 94.09/51.57 fof(id2, axiom, ! [X0] : ! [X1] : ((s(X0) = s(X1) => X0 = X1))).
% 94.09/51.57 fof(id7, axiom, ! [X0] : ! [X1] : ! [X2] : ~(('plus$usucceeds'(X0,X1,X2) & 'plus$ufails'(X0,X1,X2)))).
% 94.09/51.57 fof(id18, axiom, ! [X0] : ! [X1] : ! [X2] : (('plus$usucceeds'(X0,X1,X2) <=> (? [X3] : ? [X4] : ((X0 = s(X3) & (X2 = s(X4) & 'plus$usucceeds'(X3,X1,X4)))) | (X0 = '\'0\'' & X2 = X1))))).
% 94.09/51.57 fof(id19, axiom, ! [X0] : ! [X1] : ! [X2] : (('plus$ufails'(X0,X1,X2) <=> (! [X3] : ! [X4] : ((X0 != s(X3) | (X2 != s(X4) | 'plus$ufails'(X3,X1,X4)))) & (X0 != '\'0\'' | X2 != X1))))).
% 94.09/51.57 fof(id24, axiom, ! [X0] : ! [X1] : (('\'@<$usucceeds\''(X0,X1) <=> (? [X2] : ? [X3] : ((X0 = s(X2) & (X1 = s(X3) & '\'@<$usucceeds\''(X2,X3)))) | ? [X4] : ((X0 = '\'0\'' & X1 = s(X4))))))).
% 94.09/51.57 fof(id27, axiom, ! [X0] : (('nat$usucceeds'(X0) <=> (? [X1] : ((X0 = s(X1) & 'nat$usucceeds'(X1))) | X0 = '\'0\'')))).
% 94.09/51.57 fof((@+)/2, axiom, ! [X0] : ! [X1] : ! [X2] : (('nat$usucceeds'(X0) => ('\'@+\''(X0,X1) = X2 <=> 'plus$usucceeds'(X0,X1,X2))))).
% 94.09/51.57 fof(lemma-(plus:existence), axiom, ! [X0] : ! [X1] : (('nat$usucceeds'(X0) => ? [X2] : 'plus$usucceeds'(X0,X1,X2)))).
% 94.09/51.57 fof(corollary-(plus:zero), axiom, ! [X0] : '\'@+\''('\'0\'',X0) = X0).
% 94.09/51.57 fof(corollary-(plus:successor), axiom, ! [X0] : ! [X1] : (('nat$usucceeds'(X0) => '\'@+\''(s(X0),X1) = s('\'@+\''(X0,X1))))).
% 94.09/51.57 fof(induction, axiom, (! [X0] : (((? [X1] : ((X0 = s(X1) & ('nat$usucceeds'(X1) & ! [X2] : ! [X3] : (('\'@+\''(X1,X2) = '\'@+\''(X1,X3) => X2 = X3))))) | X0 = '\'0\'') => ! [X2] : ! [X3] : (('\'@+\''(X0,X2) = '\'@+\''(X0,X3) => X2 = X3)))) => ! [X0] : (('nat$usucceeds'(X0) => ! [X2] : ! [X3] : (('\'@+\''(X0,X2) = '\'@+\''(X0,X3) => X2 = X3)))))).
% 94.09/51.57 fof(lemma-(plus:injective:second), conjecture, ! [X0] : ! [X1] : ! [X2] : ((('nat$usucceeds'(X0) & '\'@+\''(X0,X1) = '\'@+\''(X0,X2)) => X1 = X2))).
% 94.09/51.57 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ((('nat$usucceeds'(X0) & '\'@+\''(X0,X1) = '\'@+\''(X0,X2)) => X1 = X2)), inference(negate_conjecture, [status(cth)], [lemma-(plus:injective:second)])).
% 94.09/51.57 cnf(c0, plain, '\'0\'' != s(X0), inference(clausification, [status(esa)], [id1])).
% 94.09/51.57 cnf(c1, plain, s(X0) != s(X1) | X0 = X1, inference(clausification, [status(esa)], [id2])).
% 94.09/51.57 cnf(c7, plain, ~'plus$usucceeds'(X0,X1,X2) | ~'plus$ufails'(X0,X1,X2), inference(clausification, [status(esa)], [id7])).
% 94.09/51.57 cnf(c38, plain, ~'plus$usucceeds'(X0,X1,X2) | X3(X0,X1,X2) | X0 = '\'0\'', inference(clausification, [status(esa)], [id18])).
% 94.09/51.57 cnf(c42, plain, ~X0(X1,X2,X3) | X1 = s(sK54(X1,X2,X3)), inference(clausification, [status(esa)], [id18])).
% 94.09/51.57 cnf(c43, plain, ~X0(X1,X2,X3) | X3 = s(sK55(X1,X2,X3)), inference(clausification, [status(esa)], [id18])).
% 94.09/51.57 cnf(c44, plain, ~X0(X1,X2,X3) | 'plus$usucceeds'(sK54(X1,X2,X3),X2,sK55(X1,X2,X3)), inference(clausification, [status(esa)], [id18])).
% 94.09/51.57 cnf(c49, plain, 'plus$ufails'(X0,X1,X2) | ~X3(X0,X1,X2) | X2 = X1, inference(clausification, [status(esa)], [id19])).
% 94.09/51.57 cnf(c51, plain, X0(X1,X2,X3) | X1 = s(sK64(X1,X2,X3)), inference(clausification, [status(esa)], [id19])).
% 94.09/51.57 cnf(c79, plain, ~'\'@<$usucceeds\''(X0,X1) | X2(X0,X1) | X1 = s(sK97(X0,X1)), inference(clausification, [status(esa)], [id24])).
% 94.09/51.57 cnf(c81, plain, '\'@<$usucceeds\''(X0,X1) | X0 != '\'0\'' | X1 != s(X2), inference(clausification, [status(esa)], [id24])).
% 94.09/51.57 cnf(c83, plain, ~X0(X1,X2) | X2 = s(sK100(X1,X2)), inference(clausification, [status(esa)], [id24])).
% 94.09/51.57 cnf(c102, plain, 'nat$usucceeds'(X0) | X0 != s(X1) | ~'nat$usucceeds'(X1), inference(clausification, [status(esa)], [id27])).
% 94.09/51.57 cnf(c103, plain, 'nat$usucceeds'(X0) | X0 != '\'0\'', inference(clausification, [status(esa)], [id27])).
% 94.09/51.57 cnf(c111, plain, ~'nat$usucceeds'(X0) | '\'@+\''(X0,X1) != X2 | 'plus$usucceeds'(X0,X1,X2), inference(clausification, [status(esa)], [(@+)/2])).
% 94.09/51.57 cnf(c112, plain, ~'nat$usucceeds'(X0) | '\'@+\''(X0,X1) = X2 | ~'plus$usucceeds'(X0,X1,X2), inference(clausification, [status(esa)], [(@+)/2])).
% 94.09/51.57 cnf(c126, plain, ~'nat$usucceeds'(X0) | 'plus$usucceeds'(X0,X1,sK167(X0,X1)), inference(clausification, [status(esa)], [lemma-(plus:existence)])).
% 94.09/51.57 cnf(c128, plain, '\'@+\''('\'0\'',X0) = X0, inference(clausification, [status(esa)], [corollary-(plus:zero)])).
% 94.09/51.57 cnf(c129, plain, ~'nat$usucceeds'(X0) | '\'@+\''(s(X0),X1) = s('\'@+\''(X0,X1)), inference(clausification, [status(esa)], [corollary-(plus:successor)])).
% 94.09/51.57 cnf(c135, plain, X0 | ~'nat$usucceeds'(X1) | '\'@+\''(X1,X2) != '\'@+\''(X1,X3) | X2 = X3, inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c136, plain, ~X0 | sK189 = s(sK190) | sK189 = '\'0\'', inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c137, plain, ~X0 | 'nat$usucceeds'(sK190) | sK189 = '\'0\'', inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c138, plain, ~X0 | '\'@+\''(sK190,X1) != '\'@+\''(sK190,X2) | X1 = X2 | sK189 = '\'0\'', inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c139, plain, ~X0 | '\'@+\''(sK189,sK193) = '\'@+\''(sK189,sK194), inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c140, plain, ~X0 | sK193 != sK194, inference(clausification, [status(esa)], [induction])).
% 94.09/51.57 cnf(c141, plain, 'nat$usucceeds'(sK195), inference(clausification, [status(esa)], [negated_conjecture])).
% 94.09/51.57 cnf(c142, plain, '\'@+\''(sK195,sK196) = '\'@+\''(sK195,sK197), inference(clausification, [status(esa)], [negated_conjecture])).
% 94.09/51.57 cnf(c143, plain, sK196 != sK197, inference(clausification, [status(esa)], [negated_conjecture])).
% 94.09/51.57 cnf(d0, plain, '\'@+\''(sK190,X2) != X1 | X2 = X0 | sK189 = '\'0\'' | ~'Ts185' | ~'plus$usucceeds'(sK190,X0,X1) | ~'nat$usucceeds'(sK190), inference(superposition, [status(thm)], [c112,c138])).
% 94.09/51.57 cnf(d1, plain, '\'@+\''(sK195,sK196) != '\'@+\''(sK195,X0) | sK197 = X0 | ~'nat$usucceeds'(sK195) | 'Ts185', inference(superposition, [status(thm)], [c142,c135])).
% 94.09/51.57 cnf(d2, plain, '\'@+\''(sK195,sK196) != '\'@+\''(sK195,X0) | sK197 = X0 | 'Ts185', inference(resolution, [status(thm)], [c141,d1])).
% 94.09/51.57 cnf(d3, plain, sK197 = sK196 | 'Ts185', inference(equality_resolution, [status(thm)], [d2])).
% 94.09/51.57 cnf(d4, plain, sK196 != sK196 | 'Ts185', inference(superposition, [status(thm)], [d3,c143])).
% 94.09/51.58 cnf(d5, plain, '\'0\'' != X0 | 'Ts58'(X0,X1,X2), inference(superposition, [status(thm)], [c51,c0])).
% 94.09/51.58 cnf(d6, plain, 'Ts58'('\'0\'',X0,X1), inference(equality_resolution, [status(thm)], [d5])).
% 94.09/51.58 cnf(d7, plain, X0 = X1 | 'plus$ufails'('\'0\'',X1,X0), inference(resolution, [status(thm)], [c49,d6])).
% 94.09/51.58 cnf(d8, plain, X0 = X1 | ~'plus$usucceeds'('\'0\'',X1,X0), inference(resolution, [status(thm)], [d7,c7])).
% 94.09/51.58 cnf(d9, plain, 'plus$usucceeds'(X0,X1,'\'@+\''(X0,X1)) | ~'nat$usucceeds'(X0), inference(equality_resolution, [status(thm)], [c111])).
% 94.09/51.58 cnf(d10, plain, ~'nat$usucceeds'('\'0\'') | '\'@+\''('\'0\'',X0) = X0, inference(resolution, [status(thm)], [d9,d8])).
% 94.09/51.58 cnf(d11, plain, X0 = X0 | ~'nat$usucceeds'('\'0\''), inference(demodulation, [status(thm)], [d10,c128])).
% 94.09/51.58 cnf(d12, plain, 'nat$usucceeds'('\'0\''), inference(equality_resolution, [status(thm)], [c103])).
% 94.09/51.58 cnf(d13, plain, X0 = X0, inference(resolution, [status(thm)], [d12,d11])).
% 94.09/51.58 cnf(d14, plain, 'Ts185', inference(resolution, [status(thm)], [d13,d4])).
% 94.09/51.58 cnf(d15, plain, X0 = X1 | '\'@+\''(sK190,X0) != X2 | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,X1,X2) | ~'nat$usucceeds'(sK190), inference(resolution, [status(thm)], [d14,d0])).
% 94.09/51.58 cnf(d16, plain, '\'@+\''(sK189,sK193) = '\'@+\''('\'0\'',sK194) | ~'Ts185' | 'nat$usucceeds'(sK190) | ~'Ts185', inference(superposition, [status(thm)], [c137,c139])).
% 94.09/51.58 cnf(d17, plain, '\'@+\''(sK189,sK193) = sK194 | 'nat$usucceeds'(sK190) | ~'Ts185', inference(demodulation, [status(thm)], [d16,c128])).
% 94.09/51.58 cnf(d18, plain, '\'@+\''('\'0\'',sK193) = sK194 | 'nat$usucceeds'(sK190) | ~'Ts185' | 'nat$usucceeds'(sK190) | ~'Ts185', inference(superposition, [status(thm)], [c137,d17])).
% 94.09/51.58 cnf(d19, plain, sK193 = sK194 | 'nat$usucceeds'(sK190) | ~'Ts185', inference(demodulation, [status(thm)], [d18,c128])).
% 94.09/51.58 cnf(d20, plain, sK193 != sK193 | ~'Ts185' | 'nat$usucceeds'(sK190) | ~'Ts185', inference(superposition, [status(thm)], [d19,c140])).
% 94.09/51.58 cnf(d21, plain, 'nat$usucceeds'(sK190) | ~'Ts185', inference(equality_resolution, [status(thm)], [d20])).
% 94.09/51.58 cnf(d22, plain, 'nat$usucceeds'(sK190), inference(resolution, [status(thm)], [d14,d21])).
% 94.09/51.58 cnf(d23, plain, X0 = X1 | '\'@+\''(sK190,X0) != X2 | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,X1,X2), inference(resolution, [status(thm)], [d22,d15])).
% 94.09/51.58 cnf(d24, plain, X0 = X1 | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,X1,'\'@+\''(sK190,X0)), inference(equality_resolution, [status(thm)], [d23])).
% 94.09/51.58 cnf(d25, plain, 'plus$usucceeds'(sK189,sK194,'\'@+\''(sK189,sK193)) | ~'nat$usucceeds'(sK189) | ~'Ts185', inference(superposition, [status(thm)], [c139,d9])).
% 94.09/51.58 cnf(d26, plain, 'plus$usucceeds'(sK189,sK194,'\'@+\''(sK189,sK193)) | ~'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d14,d25])).
% 94.09/51.58 cnf(d27, plain, 'nat$usucceeds'(s(X0)) | ~'nat$usucceeds'(X0), inference(equality_resolution, [status(thm)], [c102])).
% 94.09/51.58 cnf(d28, plain, 'nat$usucceeds'(sK189) | ~'nat$usucceeds'(sK190) | sK189 = '\'0\'' | ~'Ts185', inference(superposition, [status(thm)], [c136,d27])).
% 94.09/51.58 cnf(d29, plain, '\'@+\''(sK189,sK193) = '\'@+\''('\'0\'',sK194) | ~'Ts185' | 'nat$usucceeds'(sK189) | ~'nat$usucceeds'(sK190) | ~'Ts185', inference(superposition, [status(thm)], [d28,c139])).
% 94.09/51.58 cnf(d30, plain, '\'@+\''(sK189,sK193) = sK194 | 'nat$usucceeds'(sK189) | ~'nat$usucceeds'(sK190) | ~'Ts185', inference(demodulation, [status(thm)], [d29,c128])).
% 94.09/51.58 cnf(d31, plain, '\'@+\''(sK189,sK193) = sK194 | 'nat$usucceeds'(sK189) | ~'nat$usucceeds'(sK190), inference(resolution, [status(thm)], [d14,d30])).
% 94.09/51.58 cnf(d32, plain, '\'@+\''(sK189,sK193) = sK194 | 'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d22,d31])).
% 94.09/51.58 cnf(d33, plain, sK189 = '\'0\'' | 'nat$usucceeds'(sK189) | ~'nat$usucceeds'(sK190), inference(resolution, [status(thm)], [d14,d28])).
% 94.09/51.58 cnf(d34, plain, sK189 = '\'0\'' | 'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d22,d33])).
% 94.09/51.58 cnf(d35, plain, '\'@+\''('\'0\'',sK193) = sK194 | 'nat$usucceeds'(sK189) | 'nat$usucceeds'(sK189), inference(superposition, [status(thm)], [d34,d32])).
% 94.09/51.58 cnf(d36, plain, sK193 = sK194 | 'nat$usucceeds'(sK189), inference(demodulation, [status(thm)], [d35,c128])).
% 94.09/51.58 cnf(d37, plain, sK193 != sK194, inference(resolution, [status(thm)], [d14,c140])).
% 94.09/51.58 cnf(d38, plain, 'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d37,d36])).
% 94.09/51.58 cnf(d39, plain, 'plus$usucceeds'(sK189,sK194,'\'@+\''(sK189,sK193)), inference(resolution, [status(thm)], [d38,d26])).
% 94.09/51.58 cnf(d40, plain, sK189 = '\'0\'' | 'Ts50'(sK189,sK194,'\'@+\''(sK189,sK193)), inference(resolution, [status(thm)], [d39,c38])).
% 94.09/51.58 cnf(d41, plain, sK189 = '\'0\'' | sK189 = s(sK190), inference(resolution, [status(thm)], [d14,c136])).
% 94.09/51.58 cnf(d42, plain, '\'@+\''(sK189,X0) = s('\'@+\''(sK190,X0)) | ~'nat$usucceeds'(sK190) | sK189 = '\'0\'', inference(superposition, [status(thm)], [d41,c129])).
% 94.09/51.58 cnf(d43, plain, '\'@+\''(sK189,X0) = s('\'@+\''(sK190,X0)) | sK189 = '\'0\'', inference(resolution, [status(thm)], [d22,d42])).
% 94.09/51.58 cnf(d44, plain, '\'@+\''(sK189,X0) = s(X1) | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,X0,X1) | ~'nat$usucceeds'(sK190), inference(superposition, [status(thm)], [c112,d43])).
% 94.09/51.58 cnf(d45, plain, '\'@+\''(sK189,X0) = s(X1) | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,X0,X1), inference(resolution, [status(thm)], [d22,d44])).
% 94.09/51.58 cnf(d46, plain, 'Ts50'(sK189,sK194,s(X0)) | sK189 = '\'0\'' | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,sK193,X0), inference(superposition, [status(thm)], [d45,d40])).
% 94.09/51.58 cnf(d47, plain, sK189 != s(X0) | sK190 = X0 | sK189 = '\'0\'' | ~'Ts185', inference(superposition, [status(thm)], [c136,c1])).
% 94.09/51.58 cnf(d48, plain, sK189 != X0 | sK189 = '\'0\'' | sK190 = sK54(X0,X1,X2) | ~'Ts185' | ~'Ts50'(X0,X1,X2), inference(superposition, [status(thm)], [c42,d47])).
% 94.09/51.58 cnf(d49, plain, sK189 != X0 | sK189 = '\'0\'' | sK190 = sK54(X0,X1,X2) | ~'Ts50'(X0,X1,X2), inference(resolution, [status(thm)], [d14,d48])).
% 94.09/51.58 cnf(d50, plain, sK189 = '\'0\'' | sK190 = sK54(sK189,X0,X1) | ~'Ts50'(sK189,X0,X1), inference(equality_resolution, [status(thm)], [d49])).
% 94.09/51.58 cnf(d51, plain, 'plus$usucceeds'(sK190,X0,sK55(sK189,X0,X1)) | ~'Ts50'(sK189,X0,X1) | sK189 = '\'0\'' | ~'Ts50'(sK189,X0,X1), inference(superposition, [status(thm)], [d50,c44])).
% 94.09/51.58 cnf(d52, plain, X2 != s(X3) | sK55(X0,X1,X2) = X3 | ~'Ts50'(X0,X1,X2), inference(superposition, [status(thm)], [c43,c1])).
% 94.09/51.58 cnf(d53, plain, sK55(X0,X1,s(X2)) = X2 | ~'Ts50'(X0,X1,s(X2)), inference(equality_resolution, [status(thm)], [d52])).
% 94.09/51.58 cnf(d54, plain, 'plus$usucceeds'(sK190,X0,X1) | sK189 = '\'0\'' | ~'Ts50'(sK189,X0,s(X1)) | ~'Ts50'(sK189,X0,s(X1)), inference(superposition, [status(thm)], [d53,d51])).
% 94.09/51.58 cnf(d55, plain, sK189 = '\'0\'' | 'plus$usucceeds'(sK190,sK194,X0) | sK189 = '\'0\'' | ~'plus$usucceeds'(sK190,sK193,X0), inference(resolution, [status(thm)], [d54,d46])).
% 94.09/51.58 cnf(d56, plain, sK189 = '\'0\'' | 'plus$usucceeds'(sK190,sK194,'\'@+\''(sK190,sK193)) | ~'nat$usucceeds'(sK190), inference(resolution, [status(thm)], [d55,d9])).
% 94.09/51.58 cnf(d57, plain, sK189 = '\'0\'' | 'plus$usucceeds'(sK190,sK194,'\'@+\''(sK190,sK193)), inference(resolution, [status(thm)], [d22,d56])).
% 94.09/51.58 cnf(d58, plain, sK189 = '\'0\'' | sK193 = sK194 | sK189 = '\'0\'', inference(resolution, [status(thm)], [d57,d24])).
% 94.09/51.58 cnf(d59, plain, sK189 = '\'0\'', inference(resolution, [status(thm)], [d37,d58])).
% 94.09/51.58 cnf(d60, plain, X0 != '\'0\'' | '\'@<$usucceeds\''(X0,s(X1)), inference(equality_resolution, [status(thm)], [c81])).
% 94.09/51.58 cnf(d61, plain, '\'@<$usucceeds\''('\'0\'',s(X0)), inference(equality_resolution, [status(thm)], [d60])).
% 94.09/51.58 cnf(d62, plain, '\'@<$usucceeds\''('\'0\'',X0) | 'Ts58'(X0,X1,X2), inference(superposition, [status(thm)], [c51,d61])).
% 94.09/51.58 cnf(d63, plain, X0 = X1 | 'plus$ufails'(X2,X1,X0) | '\'@<$usucceeds\''('\'0\'',X2), inference(resolution, [status(thm)], [c49,d62])).
% 94.09/51.58 cnf(d64, plain, X0 = X1 | '\'@<$usucceeds\''('\'0\'',X2) | ~'plus$usucceeds'(X2,X1,X0), inference(resolution, [status(thm)], [d63,c7])).
% 94.09/51.58 cnf(d65, plain, 'plus$usucceeds'(sK189,sK194,X0) | ~'nat$usucceeds'(sK189) | ~'plus$usucceeds'(sK189,sK193,X0) | ~'nat$usucceeds'(sK189), inference(superposition, [status(thm)], [c112,d26])).
% 94.09/51.58 cnf(d66, plain, ~'plus$usucceeds'(sK189,sK193,X0) | 'plus$usucceeds'(sK189,sK194,X0), inference(resolution, [status(thm)], [d38,d65])).
% 94.09/51.58 cnf(d67, plain, 'plus$usucceeds'(sK189,sK194,sK167(sK189,sK193)) | ~'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d66,c126])).
% 94.09/51.58 cnf(d68, plain, 'plus$usucceeds'(sK189,sK194,sK167(sK189,sK193)), inference(resolution, [status(thm)], [d38,d67])).
% 94.09/51.58 cnf(d69, plain, sK167(sK189,sK193) = sK194 | '\'@<$usucceeds\''('\'0\'',sK189), inference(resolution, [status(thm)], [d68,d64])).
% 94.09/51.58 cnf(d70, plain, sK167(X0,X1) = X1 | '\'@<$usucceeds\''('\'0\'',X0) | ~'nat$usucceeds'(X0), inference(resolution, [status(thm)], [d64,c126])).
% 94.09/51.58 cnf(d71, plain, sK193 = sK194 | '\'@<$usucceeds\''('\'0\'',sK189) | '\'@<$usucceeds\''('\'0\'',sK189) | ~'nat$usucceeds'(sK189), inference(superposition, [status(thm)], [d70,d69])).
% 94.09/51.58 cnf(d72, plain, '\'@<$usucceeds\''('\'0\'',sK189) | ~'nat$usucceeds'(sK189), inference(resolution, [status(thm)], [d37,d71])).
% 94.09/51.58 cnf(d73, plain, '\'@<$usucceeds\''('\'0\'',sK189), inference(resolution, [status(thm)], [d38,d72])).
% 94.09/51.58 cnf(d74, plain, '\'@<$usucceeds\''('\'0\'','\'0\''), inference(demodulation, [status(thm)], [d73,d59])).
% 94.09/51.58 cnf(d75, plain, '\'0\'' != X1 | ~'\'@<$usucceeds\''(X0,X1) | 'Ts94'(X0,X1), inference(superposition, [status(thm)], [c79,c0])).
% 94.09/51.58 cnf(d76, plain, ~'\'@<$usucceeds\''(X0,'\'0\'') | 'Ts94'(X0,'\'0\''), inference(equality_resolution, [status(thm)], [d75])).
% 94.09/51.58 cnf(d77, plain, '\'0\'' != X1 | ~'Ts94'(X0,X1), inference(superposition, [status(thm)], [c83,c0])).
% 94.09/51.58 cnf(d78, plain, ~'Ts94'(X0,'\'0\''), inference(equality_resolution, [status(thm)], [d77])).
% 94.09/51.58 cnf(d79, plain, ~'\'@<$usucceeds\''(X0,'\'0\''), inference(resolution, [status(thm)], [d78,d76])).
% 94.09/51.58 cnf(d80, plain, $false, inference(resolution, [status(thm)], [d79,d74])).
% 94.09/51.58 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------