%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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:11:39 AM UTC 2026
% Result : Theorem 69.08s 17.70s
% Output : CNFRefutation 69.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW295+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 15:36:16 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.08/17.70 % SZS status Theorem for theBenchmark.p
% 69.08/17.70 % SZS output start CNFRefutation for theBenchmark.p
% 69.08/17.70 fof(fact_evaln_OBody, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody',X3)),X2,X1,X0) => 'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'(X3),X2,hAPP('c$uNat$uOSuc',X1),X0)))).
% 69.08/17.70 fof(fact_evaln_Oequations_I9_J, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : (('c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'(X3),X2,hAPP('c$uNat$uOSuc',X1),X0) <=> 'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody',X3)),X2,X1,X0)))).
% 69.08/17.70 fof(conj_0, conjecture, (! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody','v$upn')),X1,'v$un',X2) => 'v$uQ'(X0,X2))))) <=> ! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),X1,hAPP('c$uNat$uOSuc','v$un'),X2) => 'v$uQ'(X0,X2))))))).
% 69.08/17.70 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody','v$upn')),X1,'v$un',X2) => 'v$uQ'(X0,X2))))) <=> ! [X0] : ! [X1] : (('v$uP'(X0,X1) => ! [X2] : (('c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),X1,hAPP('c$uNat$uOSuc','v$un'),X2) => 'v$uQ'(X0,X2))))))), inference(negate_conjecture, [status(cth)], [conj_0])).
% 69.08/17.70 cnf(c1, plain, ~'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody',X0)),X1,X2,X3) | 'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'(X0),X1,hAPP('c$uNat$uOSuc',X2),X3), inference(clausification, [status(esa)], [fact_evaln_OBody])).
% 69.08/17.70 cnf(c2, plain, ~'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'(X0),X1,hAPP('c$uNat$uOSuc',X2),X3) | 'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody',X0)),X1,X2,X3), inference(clausification, [status(esa)], [fact_evaln_Oequations_I9_J])).
% 69.08/17.70 cnf(c7482, plain, X0 | ~'v$uP'(X1,X2) | ~'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),X2,hAPP('c$uNat$uOSuc','v$un'),X3) | 'v$uQ'(X1,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7483, plain, 'v$uP'(sK17009,sK17010) | ~X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7485, plain, 'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),sK17010,hAPP('c$uNat$uOSuc','v$un'),sK17011) | ~X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7487, plain, ~'v$uQ'(sK17009,sK17011) | ~X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7489, plain, ~X0 | ~'v$uP'(X1,X2) | ~'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody','v$upn')),X2,'v$un',X3) | 'v$uQ'(X1,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7490, plain, X0 | 'v$uP'(sK17018,sK17019), inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7491, plain, X0 | 'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody','v$upn')),sK17019,'v$un',sK17020), inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(c7492, plain, X0 | ~'v$uQ'(sK17018,sK17020), inference(clausification, [status(esa)], [negated_conjecture])).
% 69.08/17.70 cnf(d0, plain, 'Ts17008' | 'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),sK17019,hAPP('c$uNat$uOSuc','v$un'),sK17020), inference(resolution, [status(thm)], [c7491,c1])).
% 69.08/17.70 cnf(d1, plain, 'Ts17008' | ~'v$uP'(X0,sK17019) | 'v$uQ'(X0,sK17020) | 'Ts17008', inference(resolution, [status(thm)], [c7482,d0])).
% 69.08/17.70 cnf(d2, plain, 'Ts17008' | 'v$uQ'(sK17018,sK17020) | 'Ts17008', inference(resolution, [status(thm)], [d1,c7490])).
% 69.08/17.70 cnf(d3, plain, 'Ts17008' | 'Ts17008', inference(resolution, [status(thm)], [d2,c7492])).
% 69.08/17.70 cnf(d4, plain, 'v$uP'(sK17009,sK17010), inference(resolution, [status(thm)], [d3,c7483])).
% 69.08/17.70 cnf(d5, plain, 'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),sK17010,hAPP('c$uNat$uOSuc','v$un'),sK17011), inference(resolution, [status(thm)], [d3,c7485])).
% 69.08/17.70 cnf(d6, plain, ~'c$uNatural$uOevaln'(hAPP('c$uOption$uOthe'('tc$uCom$uOcom'),hAPP('c$uCom$uObody','v$upn')),X0,'v$un',X1) | ~'v$uP'(X2,X0) | 'v$uQ'(X2,X1), inference(resolution, [status(thm)], [d3,c7489])).
% 69.08/17.70 cnf(d7, plain, ~'v$uP'(X0,X1) | 'v$uQ'(X0,X2) | ~'c$uNatural$uOevaln'('c$uCom$uOcom$uOBODY'('v$upn'),X1,hAPP('c$uNat$uOSuc','v$un'),X2), inference(resolution, [status(thm)], [d6,c2])).
% 69.08/17.70 cnf(d8, plain, ~'v$uP'(X0,sK17010) | 'v$uQ'(X0,sK17011), inference(resolution, [status(thm)], [d7,d5])).
% 69.08/17.70 cnf(d9, plain, 'v$uQ'(sK17009,sK17011), inference(resolution, [status(thm)], [d8,d4])).
% 69.08/17.70 cnf(d10, plain, ~'v$uQ'(sK17009,sK17011), inference(resolution, [status(thm)], [d3,c7487])).
% 69.08/17.70 cnf(d11, plain, $false, inference(resolution, [status(thm)], [d10,d9])).
% 69.08/17.70 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------