%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV631+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 08:48:59 AM UTC 2026
% Result : Theorem 10.39s 9.40s
% Output : CNFRefutation 10.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV631+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n016.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sat Sep 26 11:30:00 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.39/9.40 % SZS status Theorem for theBenchmark.p
% 10.39/9.40 % SZS output start CNFRefutation for theBenchmark.p
% 10.39/9.40 fof($_inj_HList.hlist.Hcons, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : ! [X6] : ! [X7] : (('cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X2,X4,X6) = 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X1,X3,X5,X7) => (X6 = X7 & (X4 = X5 & (X2 = X3 & X0 = X1)))))).
% 10.39/9.40 fof(_HAMMER_GOAL, conjecture, ! [X0] : (('ciT$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2elist$u$u$u24t'(ciT,X1) => ! [X2] : (('cF$u$u$u24t'(X0,X2) => ! [X3] : (('cHList$u2ehlist$u2ehlist$u$u$u24t'(X1,X3) => ! [X4] : (('cF$u$u$u24t'(X0,X4) => ! [X5] : (('cHList$u2ehlist$u2ehlist$u$u$u24t'(X1,X5) => ('cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) = 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X4,X5) => (X2 = X4 & X3 = X5))))))))))))))).
% 10.39/9.40 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('ciT$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2elist$u$u$u24t'(ciT,X1) => ! [X2] : (('cF$u$u$u24t'(X0,X2) => ! [X3] : (('cHList$u2ehlist$u2ehlist$u$u$u24t'(X1,X3) => ! [X4] : (('cF$u$u$u24t'(X0,X4) => ! [X5] : (('cHList$u2ehlist$u2ehlist$u$u$u24t'(X1,X5) => ('cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) = 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X4,X5) => (X2 = X4 & X3 = X5)))))))))))))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 10.39/9.40 cnf(c6, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) != 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X4,X5,X6,X7) | X3 = X7, inference(clausification, [status(esa)], [$_inj_HList.hlist.Hcons])).
% 10.39/9.40 cnf(c7, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) != 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X4,X5,X6,X7) | X2 = X6, inference(clausification, [status(esa)], [$_inj_HList.hlist.Hcons])).
% 10.39/9.40 cnf(c41, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK67,sK68) = 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK69,sK70), inference(clausification, [status(esa)], [negated_conjecture])).
% 10.39/9.40 cnf(c42, plain, sK67 != sK69 | sK68 != sK70, inference(clausification, [status(esa)], [negated_conjecture])).
% 10.39/9.40 cnf(d0, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK67,sK68) != 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) | sK70 = X3, inference(superposition, [status(thm)], [c41,c6])).
% 10.39/9.40 cnf(d1, plain, sK70 = sK68, inference(equality_resolution, [status(thm)], [d0])).
% 10.39/9.40 cnf(d2, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK67,sK68) = 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK69,sK68), inference(demodulation, [status(thm)], [c41,d1])).
% 10.39/9.40 cnf(d3, plain, 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(sK65,sK66,sK67,sK68) != 'cHList$u2ehlist$u2eHcons$u$u$u24a4'(X0,X1,X2,X3) | sK69 = X2, inference(superposition, [status(thm)], [d2,c7])).
% 10.39/9.40 cnf(d4, plain, sK69 = sK67, inference(equality_resolution, [status(thm)], [d3])).
% 10.39/9.40 cnf(d5, plain, sK67 != sK69 | sK68 != sK68, inference(demodulation, [status(thm)], [c42,d1])).
% 10.39/9.40 cnf(d6, plain, sK67 != sK69, inference(equality_resolution, [status(thm)], [d5])).
% 10.39/9.40 cnf(d7, plain, sK67 != sK67, inference(demodulation, [status(thm)], [d6,d4])).
% 10.39/9.40 cnf(d8, plain, $false, inference(equality_resolution, [status(thm)], [d7])).
% 10.39/9.40 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------