%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : KRS098+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 : n010.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:09 AM UTC 2026
% Result : Unsatisfiable 19.33s 2.95s
% Output : CNFRefutation 19.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS098+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n010.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 19:39:44 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.33/2.95 % SZS status Unsatisfiable for theBenchmark.p
% 19.33/2.95 % SZS output start CNFRefutation for theBenchmark.p
% 19.33/2.95 fof(axiom_2, axiom, ! [X0] : ((cUnsatisfiable(X0) <=> (? [X1] : ((rr3(X0,X1) & (? [X2] : ((rt3(X1,X2) & ce(X2))) & ! [X3] : ! [X4] : (((rtt(X1,X3) & rtt(X1,X4)) => X3 = X4))))) & (? [X1] : ((rr2(X0,X1) & (! [X3] : ! [X4] : (((rtt(X1,X3) & rtt(X1,X4)) => X3 = X4)) & ? [X2] : ((rt2(X1,X2) & cd(X2)))))) & (~? [X5] : ? [X6] : ((rr(X0,X5) & (rr(X0,X6) & X5 != X6))) & ? [X1] : ((rr1(X0,X1) & (! [X3] : ! [X4] : (((rtt(X1,X3) & rtt(X1,X4)) => X3 = X4)) & ? [X2] : ((rt1(X1,X2) & cc(X2)))))))))))).
% 19.33/2.95 fof(axiom_4, axiom, cUnsatisfiable('i2003$u11$u14$u17$u20$u25524')).
% 19.33/2.95 fof(axiom_6, axiom, ! [X0] : ~((ce(X0) & cc(X0)))).
% 19.33/2.95 fof(axiom_8, axiom, ! [X0] : ! [X1] : ((rr1(X0,X1) => rr(X0,X1)))).
% 19.33/2.95 fof(axiom_10, axiom, ! [X0] : ! [X1] : ((rt1(X0,X1) => rtt(X0,X1)))).
% 19.33/2.95 fof(axiom_12, axiom, ! [X0] : ! [X1] : ((rr3(X0,X1) => rr(X0,X1)))).
% 19.33/2.95 fof(axiom_13, axiom, ! [X0] : ! [X1] : ((rt3(X0,X1) => rtt(X0,X1)))).
% 19.33/2.95 cnf(c29, plain, ~cUnsatisfiable(X0) | X1(X0), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c31, plain, ~X0(X1) | ~rr(X1,X2) | ~rr(X1,X3) | X2 = X3, inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c42, plain, ~X0(X1) | rr3(X1,sK85(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c43, plain, ~X0(X1) | rt3(sK85(X1),sK86(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c44, plain, ~X0(X1) | ce(sK86(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c45, plain, ~X0(X1) | ~rtt(sK85(X1),X2) | ~rtt(sK85(X1),X3) | X2 = X3, inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c49, plain, ~X0(X1) | X2(X1), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c51, plain, ~X0(X1) | X2(X1), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c52, plain, ~X0(X1) | rr1(X1,sK93(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c54, plain, ~X0(X1) | rt1(sK93(X1),sK96(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c55, plain, ~X0(X1) | cc(sK96(X1)), inference(clausification, [status(esa)], [axiom_2])).
% 19.33/2.95 cnf(c62, plain, cUnsatisfiable('i2003$u11$u14$u17$u20$u25524'), inference(clausification, [status(esa)], [axiom_4])).
% 19.33/2.95 cnf(c64, plain, ~ce(X0) | ~cc(X0), inference(clausification, [status(esa)], [axiom_6])).
% 19.33/2.95 cnf(c66, plain, ~rr1(X0,X1) | rr(X0,X1), inference(clausification, [status(esa)], [axiom_8])).
% 19.33/2.95 cnf(c68, plain, ~rt1(X0,X1) | rtt(X0,X1), inference(clausification, [status(esa)], [axiom_10])).
% 19.33/2.95 cnf(c70, plain, ~rr3(X0,X1) | rr(X0,X1), inference(clausification, [status(esa)], [axiom_12])).
% 19.33/2.95 cnf(c71, plain, ~rt3(X0,X1) | rtt(X0,X1), inference(clausification, [status(esa)], [axiom_13])).
% 19.33/2.95 cnf(d0, plain, ~'Ts70'(X0) | ~cc(sK86(X0)), inference(resolution, [status(thm)], [c44,c64])).
% 19.33/2.95 cnf(d1, plain, ~'Ts70'(X0) | rtt(sK85(X0),sK86(X0)), inference(resolution, [status(thm)], [c43,c71])).
% 19.33/2.95 cnf(d2, plain, ~'Ts70'(X0) | X1 = sK86(X0) | ~rtt(sK85(X0),X1) | ~'Ts70'(X0), inference(resolution, [status(thm)], [d1,c45])).
% 19.33/2.95 cnf(d3, plain, ~'Ts71'(X0) | rtt(sK93(X0),sK96(X0)), inference(resolution, [status(thm)], [c54,c68])).
% 19.33/2.95 cnf(d4, plain, 'Ts71'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [c29,c62])).
% 19.33/2.95 cnf(d5, plain, 'Ts70'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [c49,d4])).
% 19.33/2.95 cnf(d6, plain, rr(X0,sK85(X0)) | ~'Ts70'(X0), inference(resolution, [status(thm)], [c70,c42])).
% 19.33/2.95 cnf(d7, plain, rr(X0,sK93(X0)) | ~'Ts71'(X0), inference(resolution, [status(thm)], [c66,c52])).
% 19.33/2.95 cnf(d8, plain, ~'Ts71'(X0) | sK93(X0) = X1 | ~rr(X0,X1) | ~'Ts68'(X0), inference(resolution, [status(thm)], [d7,c31])).
% 19.33/2.95 cnf(d9, plain, sK93(X0) = sK85(X0) | ~'Ts71'(X0) | ~'Ts68'(X0) | ~'Ts70'(X0), inference(resolution, [status(thm)], [d8,d6])).
% 19.33/2.95 cnf(d10, plain, sK93('i2003$u11$u14$u17$u20$u25524') = sK85('i2003$u11$u14$u17$u20$u25524') | ~'Ts71'('i2003$u11$u14$u17$u20$u25524') | ~'Ts68'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d9,d5])).
% 19.33/2.95 cnf(d11, plain, sK93('i2003$u11$u14$u17$u20$u25524') = sK85('i2003$u11$u14$u17$u20$u25524') | ~'Ts68'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d4,d10])).
% 19.33/2.95 cnf(d12, plain, 'Ts68'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [c51,d4])).
% 19.33/2.95 cnf(d13, plain, sK93('i2003$u11$u14$u17$u20$u25524') = sK85('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d12,d11])).
% 19.33/2.95 cnf(d14, plain, rtt(sK85('i2003$u11$u14$u17$u20$u25524'),sK96('i2003$u11$u14$u17$u20$u25524')) | ~'Ts71'('i2003$u11$u14$u17$u20$u25524'), inference(superposition, [status(thm)], [d13,d3])).
% 19.33/2.95 cnf(d15, plain, rtt(sK85('i2003$u11$u14$u17$u20$u25524'),sK96('i2003$u11$u14$u17$u20$u25524')), inference(resolution, [status(thm)], [d4,d14])).
% 19.33/2.95 cnf(d16, plain, sK96('i2003$u11$u14$u17$u20$u25524') = sK86('i2003$u11$u14$u17$u20$u25524') | ~'Ts70'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d15,d2])).
% 19.33/2.95 cnf(d17, plain, sK96('i2003$u11$u14$u17$u20$u25524') = sK86('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d5,d16])).
% 19.33/2.95 cnf(d18, plain, cc(sK86('i2003$u11$u14$u17$u20$u25524')) | ~'Ts71'('i2003$u11$u14$u17$u20$u25524'), inference(superposition, [status(thm)], [d17,c55])).
% 19.33/2.95 cnf(d19, plain, cc(sK86('i2003$u11$u14$u17$u20$u25524')), inference(resolution, [status(thm)], [d4,d18])).
% 19.33/2.95 cnf(d20, plain, ~'Ts70'('i2003$u11$u14$u17$u20$u25524'), inference(resolution, [status(thm)], [d19,d0])).
% 19.33/2.95 cnf(d21, plain, $false, inference(resolution, [status(thm)], [d5,d20])).
% 19.33/2.95 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------