%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GEO497+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:15:17 AM UTC 2026
% Result : Theorem 59.38s 10.63s
% Output : CNFRefutation 59.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO497+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n011.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 : Fri Sep 25 13:36:28 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 59.38/10.63 % SZS status Theorem for theBenchmark.p
% 59.38/10.63 % SZS output start CNFRefutation for theBenchmark.p
% 59.38/10.63 fof(aSatz2_2, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((~'s$ue'(X0,X1,X2,X3) | 's$ue'(X2,X3,X0,X1)))).
% 59.38/10.63 fof(aSatz2_13, axiom, ! [X0] : ! [X1] : ! [X2] : ((~'s$ue'(X0,X1,X2,X2) | X0 = X1))).
% 59.38/10.63 fof(aSatz3_2, axiom, ! [X0] : ! [X1] : ! [X2] : ((~'s$ut'(X0,X1,X2) | 's$ut'(X2,X1,X0)))).
% 59.38/10.63 fof(aSatz3_14a, axiom, ! [X0] : ! [X1] : 's$ut'(X0,X1,ext(X0,X1,alpha,gamma))).
% 59.38/10.63 fof(aSatz3_14b, axiom, ! [X0] : ! [X1] : X0 != ext(X1,X0,alpha,gamma)).
% 59.38/10.63 fof(aSatz5_5a, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((~le(X0,X1,X2,X3) | 's$ut'(X0,X1,ins(X2,X3,X0,X1))) & ((~le(X0,X1,X2,X3) | 's$ue'(X0,ins(X2,X3,X0,X1),X2,X3)) & (~le(X0,X1,X2,X3) | ins(X2,X3,X0,X1) = ext(X0,X1,insert(X0,X1,X2,X3),X3)))))).
% 59.38/10.63 fof(aSatz5_7, axiom, ! [X0] : ! [X1] : le(X0,X1,X0,X1)).
% 59.38/10.63 fof(aSatz5_11, axiom, ! [X0] : ! [X1] : ! [X2] : le(X0,X0,X1,X2)).
% 59.38/10.63 fof(aSatz6_2a, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ((X0 = X1 | (X2 = X1 | (X3 = X1 | (~'s$ut'(X0,X1,X3) | (~'s$ut'(X2,X1,X3) | sameside(X0,X1,X2)))))))).
% 59.38/10.63 fof(d_insert, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : insert(X0,X1,X2,X3) = ext(ext(X3,X2,alpha,gamma),X2,X0,X1)).
% 59.38/10.63 fof(aA4, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('s$ut'(X0,X1,ext(X0,X1,X2,X3)) & 's$ue'(X1,ext(X0,X1,X2,X3),X2,X3)))).
% 59.38/10.63 fof(aSatz6_11a, conjecture, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (((X0 = X1 | (X2 = X3 | sameside(insert(X2,X3,X1,X0),X1,X0))) & (X0 = X1 | (X2 = X3 | 's$ue'(X1,insert(X2,X3,X1,X0),X2,X3)))))).
% 59.38/10.63 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ! [X3] : (((X0 = X1 | (X2 = X3 | sameside(insert(X2,X3,X1,X0),X1,X0))) & (X0 = X1 | (X2 = X3 | 's$ue'(X1,insert(X2,X3,X1,X0),X2,X3))))), inference(negate_conjecture, [status(cth)], [aSatz6_11a])).
% 59.38/10.63 cnf(c1, plain, ~'s$ue'(X0,X1,X2,X3) | 's$ue'(X2,X3,X0,X1), inference(clausification, [status(esa)], [aSatz2_2])).
% 59.38/10.63 cnf(c8, plain, ~'s$ue'(X0,X1,X2,X2) | X0 = X1, inference(clausification, [status(esa)], [aSatz2_13])).
% 59.38/10.63 cnf(c12, plain, ~'s$ut'(X0,X1,X2) | 's$ut'(X2,X1,X0), inference(clausification, [status(esa)], [aSatz3_2])).
% 59.38/10.63 cnf(c24, plain, 's$ut'(X0,X1,ext(X0,X1,alpha,gamma)), inference(clausification, [status(esa)], [aSatz3_14a])).
% 59.38/10.63 cnf(c25, plain, X0 != ext(X1,X0,alpha,gamma), inference(clausification, [status(esa)], [aSatz3_14b])).
% 59.38/10.63 cnf(c50, plain, ~le(X0,X1,X2,X3) | 's$ue'(X0,ins(X2,X3,X0,X1),X2,X3), inference(clausification, [status(esa)], [aSatz5_5a])).
% 59.38/10.63 cnf(c54, plain, le(X0,X1,X0,X1), inference(clausification, [status(esa)], [aSatz5_7])).
% 59.38/10.63 cnf(c58, plain, le(X0,X0,X1,X2), inference(clausification, [status(esa)], [aSatz5_11])).
% 59.38/10.63 cnf(c63, plain, ~'s$ut'(X0,X1,X2) | X0 = X1 | sameside(X0,X1,X3) | ~'s$ut'(X3,X1,X2) | X3 = X1 | X2 = X1, inference(clausification, [status(esa)], [aSatz6_2a])).
% 59.38/10.63 cnf(c77, plain, insert(X0,X1,X2,X3) = ext(ext(X3,X2,alpha,gamma),X2,X0,X1), inference(clausification, [status(esa)], [d_insert])).
% 59.38/10.63 cnf(c116, plain, 's$ut'(X0,X1,ext(X0,X1,X2,X3)), inference(clausification, [status(esa)], [aA4])).
% 59.38/10.63 cnf(c117, plain, 's$ue'(X0,ext(X1,X0,X2,X3),X2,X3), inference(clausification, [status(esa)], [aA4])).
% 59.38/10.63 cnf(c127, plain, ~X0(sK333,sK334,sK335,sK332) | ~'s$ue'(sK333,insert(sK334,sK335,sK333,sK332),sK334,sK335), inference(clausification, [status(esa)], [negated_conjecture])).
% 59.38/10.63 cnf(c128, plain, X0(X1,X2,X3,X4) | X4 != X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 59.38/10.63 cnf(c129, plain, X0(X1,X2,X3,X4) | X2 != X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 59.38/10.63 cnf(c130, plain, X0(X1,X2,X3,X4) | ~sameside(insert(X2,X3,X1,X4),X1,X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 59.38/10.63 cnf(d0, plain, 's$ue'(X1,insert(X2,X3,X1,X0),X2,X3), inference(superposition, [status(thm)], [c77,c117])).
% 59.38/10.63 cnf(d1, plain, ~'Ts331'(sK333,sK334,sK335,sK332), inference(resolution, [status(thm)], [d0,c127])).
% 59.38/10.63 cnf(d2, plain, 's$ut'(ext(X0,X1,X2,X3),X1,X0), inference(resolution, [status(thm)], [c116,c12])).
% 59.38/10.63 cnf(d3, plain, X0 = X1 | ext(X2,X1,alpha,gamma) = X1 | X2 = X1 | ~'s$ut'(X0,X1,ext(X2,X1,alpha,gamma)) | sameside(X0,X1,X2), inference(resolution, [status(thm)], [c63,c24])).
% 59.38/10.63 cnf(d4, plain, X0 = X1 | ext(ext(X0,X1,alpha,gamma),X1,X2,X3) = X1 | ext(X0,X1,alpha,gamma) = X1 | sameside(ext(ext(X0,X1,alpha,gamma),X1,X2,X3),X1,X0), inference(resolution, [status(thm)], [d3,d2])).
% 59.38/10.63 cnf(d5, plain, X0 = X1 | ext(X0,X1,alpha,gamma) = X1 | insert(X2,X3,X1,X0) = X1 | sameside(ext(ext(X0,X1,alpha,gamma),X1,X2,X3),X1,X0), inference(demodulation, [status(thm)], [d4,c77])).
% 59.38/10.63 cnf(d6, plain, X0 = X1 | ext(X0,X1,alpha,gamma) = X1 | insert(X2,X3,X1,X0) = X1 | sameside(insert(X2,X3,X1,X0),X1,X0), inference(demodulation, [status(thm)], [d5,c77])).
% 59.38/10.63 cnf(d7, plain, X0 = X1 | ext(X0,X1,alpha,gamma) = X1 | insert(X2,X3,X1,X0) = X1 | 'Ts331'(X1,X2,X3,X0), inference(resolution, [status(thm)], [d6,c130])).
% 59.38/10.63 cnf(d8, plain, sK332 = sK333 | ext(sK332,sK333,alpha,gamma) = sK333 | insert(sK334,sK335,sK333,sK332) = sK333, inference(resolution, [status(thm)], [d7,d1])).
% 59.38/10.63 cnf(d9, plain, 's$ue'(sK333,sK333,sK334,sK335) | ext(sK332,sK333,alpha,gamma) = sK333 | sK332 = sK333, inference(superposition, [status(thm)], [d8,d0])).
% 59.38/10.63 cnf(d10, plain, ext(sK332,sK333,alpha,gamma) = sK333 | sK332 = sK333 | 's$ue'(sK334,sK335,sK333,sK333), inference(resolution, [status(thm)], [d9,c1])).
% 59.38/10.63 cnf(d11, plain, ext(sK332,sK333,alpha,gamma) = sK333 | sK332 = sK333 | sK334 = sK335, inference(resolution, [status(thm)], [d10,c8])).
% 59.38/10.63 cnf(d12, plain, sK333 != sK333 | sK334 = sK335 | sK332 = sK333, inference(superposition, [status(thm)], [d11,c25])).
% 59.38/10.63 cnf(d13, plain, ~le(X0,X1,X2,X2) | X0 = ins(X2,X2,X0,X1), inference(resolution, [status(thm)], [c50,c8])).
% 59.38/10.63 cnf(d14, plain, X0 = ins(X1,X1,X0,X0), inference(resolution, [status(thm)], [d13,c58])).
% 59.38/10.63 cnf(d15, plain, X0 = ins(X0,X0,X0,X0), inference(resolution, [status(thm)], [d13,c54])).
% 59.38/10.63 cnf(d16, plain, X0 = X0, inference(demodulation, [status(thm)], [d15,d14])).
% 59.38/10.63 cnf(d17, plain, sK334 = sK335 | sK332 = sK333, inference(resolution, [status(thm)], [d16,d12])).
% 59.38/10.63 cnf(d18, plain, ~'Ts331'(sK333,sK334,sK335,sK333) | sK334 = sK335, inference(superposition, [status(thm)], [d17,d1])).
% 59.38/10.63 cnf(d19, plain, 'Ts331'(X0,X1,X2,X0), inference(equality_resolution, [status(thm)], [c128])).
% 59.38/10.63 cnf(d20, plain, sK334 = sK335, inference(resolution, [status(thm)], [d19,d18])).
% 59.38/10.63 cnf(d21, plain, ~'Ts331'(sK333,sK334,sK334,sK332), inference(demodulation, [status(thm)], [d1,d20])).
% 59.38/10.63 cnf(d22, plain, 'Ts331'(X0,X1,X1,X2), inference(equality_resolution, [status(thm)], [c129])).
% 59.38/10.63 cnf(d23, plain, $false, inference(resolution, [status(thm)], [d22,d21])).
% 59.38/10.63 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------