%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:02:13 AM UTC 2026
% Result : Theorem 14.12s 2.22s
% Output : CNFRefutation 14.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n014.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 13:40:03 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.12/2.22 % SZS status Theorem for theBenchmark.p
% 14.12/2.22 % SZS output start CNFRefutation for theBenchmark.p
% 14.12/2.22 fof(l20_induction, axiom, (! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (('succ$ucpq'(triple(X0,X1,X2),triple(X3,X4,X5)) => ((~'check$ucpq'(triple(X3,X4,X5)) | ~ok(triple(X3,X4,X5))) => (~'check$ucpq'('im$usucc$ucpq'(triple(X3,X4,X5))) | ~ok('im$usucc$ucpq'(triple(X3,X4,X5))))))) => ! [X6] : ! [X7] : ! [X8] : (((~'check$ucpq'(triple(X6,X7,X8)) | ~ok(triple(X6,X7,X8))) => ! [X9] : ! [X10] : ! [X11] : (('succ$ucpq'(triple(X6,X7,X8),triple(X9,X10,X11)) => (~ok(triple(X9,X10,X11)) | ~'check$ucpq'(triple(X9,X10,X11))))))))).
% 14.12/2.22 fof(l12_l13, lemma, ! [X0] : ! [X1] : ! [X2] : (((~'check$ucpq'(triple(X0,X1,X2)) | ~ok(triple(X0,X1,X2))) => (~'check$ucpq'('im$usucc$ucpq'(triple(X0,X1,X2))) | ~ok('im$usucc$ucpq'(triple(X0,X1,X2))))))).
% 14.12/2.22 fof(l20_co, conjecture, ! [X0] : ! [X1] : ! [X2] : (((~'check$ucpq'(triple(X0,X1,X2)) | ~ok(triple(X0,X1,X2))) => ! [X3] : ! [X4] : ! [X5] : (('succ$ucpq'(triple(X0,X1,X2),triple(X3,X4,X5)) => (~ok(triple(X3,X4,X5)) | ~'check$ucpq'(triple(X3,X4,X5)))))))).
% 14.12/2.22 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : (((~'check$ucpq'(triple(X0,X1,X2)) | ~ok(triple(X0,X1,X2))) => ! [X3] : ! [X4] : ! [X5] : (('succ$ucpq'(triple(X0,X1,X2),triple(X3,X4,X5)) => (~ok(triple(X3,X4,X5)) | ~'check$ucpq'(triple(X3,X4,X5))))))), inference(negate_conjecture, [status(cth)], [l20_co])).
% 14.12/2.22 cnf(c0, plain, 'check$ucpq'(triple(X0,X1,X2)) | X3 | ~'check$ucpq'(triple(X4,X5,X6)) | ~ok(triple(X4,X5,X6)) | ~'succ$ucpq'(triple(X0,X1,X2),triple(X4,X5,X6)), inference(clausification, [status(esa)], [l20_induction])).
% 14.12/2.22 cnf(c1, plain, X0 | ~'check$ucpq'(triple(X1,X2,X3)) | ~ok(triple(X1,X2,X3)) | ~'succ$ucpq'(triple(X4,X5,X6),triple(X1,X2,X3)) | ok(triple(X4,X5,X6)), inference(clausification, [status(esa)], [l20_induction])).
% 14.12/2.22 cnf(c3, plain, ~X0 | ~'check$ucpq'(triple(sK10,sK11,sK12)) | ~ok(triple(sK10,sK11,sK12)), inference(clausification, [status(esa)], [l20_induction])).
% 14.12/2.22 cnf(c4, plain, ~X0 | 'check$ucpq'('im$usucc$ucpq'(triple(sK10,sK11,sK12))), inference(clausification, [status(esa)], [l20_induction])).
% 14.12/2.22 cnf(c5, plain, ~X0 | ok('im$usucc$ucpq'(triple(sK10,sK11,sK12))), inference(clausification, [status(esa)], [l20_induction])).
% 14.12/2.22 cnf(c6, plain, 'check$ucpq'(triple(X0,X1,X2)) | ~'check$ucpq'('im$usucc$ucpq'(triple(X0,X1,X2))) | ~ok('im$usucc$ucpq'(triple(X0,X1,X2))), inference(clausification, [status(esa)], [l12_l13])).
% 14.12/2.22 cnf(c7, plain, ok(triple(X0,X1,X2)) | ~'check$ucpq'('im$usucc$ucpq'(triple(X0,X1,X2))) | ~ok('im$usucc$ucpq'(triple(X0,X1,X2))), inference(clausification, [status(esa)], [l12_l13])).
% 14.12/2.22 cnf(c58, plain, ~'check$ucpq'(triple(sK133,sK134,sK135)) | ~ok(triple(sK133,sK134,sK135)), inference(clausification, [status(esa)], [negated_conjecture])).
% 14.12/2.22 cnf(c59, plain, 'succ$ucpq'(triple(sK133,sK134,sK135),triple(sK136,sK137,sK138)), inference(clausification, [status(esa)], [negated_conjecture])).
% 14.12/2.22 cnf(c60, plain, ok(triple(sK136,sK137,sK138)), inference(clausification, [status(esa)], [negated_conjecture])).
% 14.12/2.22 cnf(c61, plain, 'check$ucpq'(triple(sK136,sK137,sK138)), inference(clausification, [status(esa)], [negated_conjecture])).
% 14.12/2.22 cnf(d0, plain, ~'check$ucpq'(triple(sK136,sK137,sK138)) | ~ok(triple(sK136,sK137,sK138)) | ok(triple(sK133,sK134,sK135)) | 'Ts0', inference(resolution, [status(thm)], [c59,c1])).
% 14.12/2.22 cnf(d1, plain, ~'check$ucpq'(triple(sK136,sK137,sK138)) | ok(triple(sK133,sK134,sK135)) | 'Ts0', inference(resolution, [status(thm)], [c60,d0])).
% 14.12/2.22 cnf(d2, plain, ok(triple(sK133,sK134,sK135)) | 'Ts0', inference(resolution, [status(thm)], [c61,d1])).
% 14.12/2.22 cnf(d3, plain, 'Ts0' | ~'check$ucpq'(triple(sK133,sK134,sK135)), inference(resolution, [status(thm)], [d2,c58])).
% 14.12/2.22 cnf(d4, plain, ~'check$ucpq'(triple(sK136,sK137,sK138)) | 'check$ucpq'(triple(sK133,sK134,sK135)) | ~ok(triple(sK136,sK137,sK138)) | 'Ts0', inference(resolution, [status(thm)], [c59,c0])).
% 14.12/2.22 cnf(d5, plain, 'check$ucpq'(triple(sK133,sK134,sK135)) | ~'check$ucpq'(triple(sK136,sK137,sK138)) | 'Ts0', inference(resolution, [status(thm)], [c60,d4])).
% 14.12/2.22 cnf(d6, plain, 'check$ucpq'(triple(sK133,sK134,sK135)) | 'Ts0', inference(resolution, [status(thm)], [c61,d5])).
% 14.12/2.22 cnf(d7, plain, 'Ts0' | 'Ts0', inference(resolution, [status(thm)], [d6,d3])).
% 14.12/2.22 cnf(d8, plain, ok('im$usucc$ucpq'(triple(sK10,sK11,sK12))), inference(resolution, [status(thm)], [d7,c5])).
% 14.12/2.22 cnf(d9, plain, ~'check$ucpq'('im$usucc$ucpq'(triple(sK10,sK11,sK12))) | ok(triple(sK10,sK11,sK12)), inference(resolution, [status(thm)], [d8,c7])).
% 14.12/2.22 cnf(d10, plain, 'check$ucpq'('im$usucc$ucpq'(triple(sK10,sK11,sK12))), inference(resolution, [status(thm)], [d7,c4])).
% 14.12/2.22 cnf(d11, plain, ok(triple(sK10,sK11,sK12)), inference(resolution, [status(thm)], [d10,d9])).
% 14.12/2.22 cnf(d12, plain, ~'check$ucpq'(triple(sK10,sK11,sK12)) | ~ok(triple(sK10,sK11,sK12)), inference(resolution, [status(thm)], [d7,c3])).
% 14.12/2.22 cnf(d13, plain, 'check$ucpq'(triple(sK10,sK11,sK12)) | ~'check$ucpq'('im$usucc$ucpq'(triple(sK10,sK11,sK12))), inference(resolution, [status(thm)], [d8,c6])).
% 14.12/2.22 cnf(d14, plain, 'check$ucpq'(triple(sK10,sK11,sK12)), inference(resolution, [status(thm)], [d10,d13])).
% 14.12/2.22 cnf(d15, plain, ~ok(triple(sK10,sK11,sK12)), inference(resolution, [status(thm)], [d14,d12])).
% 14.12/2.22 cnf(d16, plain, $false, inference(resolution, [status(thm)], [d15,d11])).
% 14.12/2.22 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------