%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW350+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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 : Thu Sep 24 03:07:42 PM UTC 2026
% Result : Theorem 58.07s 8.34s
% Output : CNFRefutation 42.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 55 ( 8 unt; 6 def)
% Number of atoms : 125 ( 42 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 112 ( 42 ~; 56 |; 2 &)
% ( 6 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 7 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 96 ( 95 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V_u,V_t,V_s,V_c] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t))
=> ( hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_u))
=> V_u = V_t ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [V_n_2,V_ca_2,V_s_2,V_b_2] :
( ~ hBOOL(hAPP(V_b_2,V_s_2))
=> hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,c_Com_Ocom_OWhile(V_b_2,V_ca_2)),V_s_2),V_n_2),V_s_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [V_t,V_n,V_s,V_c] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,V_c),V_s),V_n),V_t))
=> hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5227,hypothesis,
! [B_Z_H] :
( ! [B_s1] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),B_s1))
=> B_Z_H = B_s1 )
=> B_Z_H = v_s_H ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5229,conjecture,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5230,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)),
inference(negated_conjecture,[status(cth)],[f5229]) ).
fof(f5234,plain,
! [V_u,V_t,V_s,V_c] :
( V_u = V_t
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_u))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t)) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f5235,plain,
! [V_t,V_s,V_c] :
( ! [V_u] :
( V_u = V_t
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_u)) )
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t)) ),
inference(miniscoping,[status(thm)],[f5234]) ).
fof(f5236,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X2),X3),X0))
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(X2),X3),X1))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f5235]) ).
fof(f5411,plain,
! [V_n_2,V_ca_2,V_s_2,V_b_2] :
( hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,c_Com_Ocom_OWhile(V_b_2,V_ca_2)),V_s_2),V_n_2),V_s_2))
| hBOOL(hAPP(V_b_2,V_s_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f5412,plain,
! [V_s_2,V_b_2] :
( ! [V_n_2,V_ca_2] : hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,c_Com_Ocom_OWhile(V_b_2,V_ca_2)),V_s_2),V_n_2),V_s_2))
| hBOOL(hAPP(V_b_2,V_s_2)) ),
inference(miniscoping,[status(thm)],[f5411]) ).
fof(f5413,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(X0,X2))
| hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,c_Com_Ocom_OWhile(X0,X1)),X2),X3),X2)) ),
inference(cnf_transformation,[status(thm)],[f5412]) ).
fof(f5473,plain,
! [V_t,V_n,V_s,V_c] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t))
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,V_c),V_s),V_n),V_t)) ),
inference(pre_NNF_transformation,[status(thm)],[f91]) ).
fof(f5474,plain,
! [V_t,V_s,V_c] :
( hBOOL(hAPP(hAPP(c_Natural_Oevalc(V_c),V_s),V_t))
| ! [V_n] : ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,V_c),V_s),V_n),V_t)) ),
inference(miniscoping,[status(thm)],[f5473]) ).
fof(f5475,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,X0),X1),X3),X2))
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f5474]) ).
fof(f19865,plain,
! [B_Z_H] :
( B_Z_H = v_s_H
| ? [B_s1] :
( B_Z_H != B_s1
& hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),B_s1)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5227]) ).
fof(f19866,plain,
! [B_Z_H] :
( B_Z_H = v_s_H
| ( B_Z_H != sK523_skl(B_Z_H)
& hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),sK523_skl(B_Z_H))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK523_skl]),skolemize(B_s1,sK523_skl(B_Z_H))],[f19865]) ).
fof(f19867,plain,
! [X0] :
( v_s_H = X0
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),sK523_skl(X0))) ),
inference(cnf_transformation,[status(thm)],[f19866]) ).
fof(f19868,plain,
! [X0] :
( X0 != sK523_skl(X0)
| v_s_H = X0 ),
inference(cnf_transformation,[status(thm)],[f19866]) ).
fof(f19871,plain,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)),
inference(cnf_transformation,[status(thm)],[f5230]) ).
fof(f20174,definition,
! [X0,X1] :
( sQ2_spl
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f20175,plain,
! [X0,X1] :
( ~ sQ2_spl
| X0 = X1 ),
inference(component_clause,[status(thm)],[f20174]) ).
fof(f20731,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,v_c),v_Z),X0),v_s_H)),
inference(resolution,[status(thm)],[f5475,f19871]) ).
fof(f20733,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ2_spl
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,X1),X2),X3),X4))
| hBOOL(X0) ),
inference(paramodulation,[status(thm)],[f20175,f5475]) ).
fof(f20738,definition,
! [X0] :
( sQ17_spl
<=> hBOOL(X0) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f20739,plain,
! [X0] :
( ~ sQ17_spl
| hBOOL(X0) ),
inference(component_clause,[status(thm)],[f20738]) ).
fof(f20741,definition,
! [X1,X2,X3,X4] :
( sQ18_spl
<=> ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,X1),X2),X3),X4)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f20742,plain,
! [X0,X1,X2,X3] :
( ~ sQ18_spl
| ~ hBOOL(hAPP(hAPP(hAPP(hAPP(c_Natural_Oevaln,X0),X1),X2),X3)) ),
inference(component_clause,[status(thm)],[f20741]) ).
fof(f20744,plain,
( ~ sQ2_spl
| sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f20733,f20738,f20741,f20174]) ).
fof(f20762,plain,
( ~ sQ17_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f20731,f20739]) ).
fof(f20764,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f20762]) ).
fof(f21060,plain,
( ~ sQ18_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19871,f21061]) ).
fof(f21061,plain,
! [X0,X1] :
( ~ sQ18_spl
| hBOOL(hAPP(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5413,f20742]) ).
fof(f21084,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f21060]) ).
fof(f23954,plain,
! [X0,X1] :
( v_s_H = X1
| ~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),X0))
| X0 = sK523_skl(X1) ),
inference(resolution,[status(thm)],[f19867,f5236]) ).
fof(f23955,plain,
! [X0,X1] :
( v_s_H = X1
| X0 = v_s_H
| sK523_skl(X0) = sK523_skl(X1) ),
inference(resolution,[status(thm)],[f23954,f19867]) ).
fof(f23964,plain,
! [X0,X1] :
( v_s_H = X1
| v_s_H = X0
| v_s_H = X1
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),sK523_skl(X0))) ),
inference(paramodulation,[status(thm)],[f23955,f19867]) ).
fof(f23965,plain,
! [X0,X1] :
( v_s_H = X0
| v_s_H = X1
| sK523_skl(X1) != X0
| X0 = v_s_H ),
inference(paramodulation,[status(thm)],[f23955,f19868]) ).
fof(f23966,plain,
! [X0,X1] :
( v_s_H = X1
| sK523_skl(X1) != X0
| X0 = v_s_H ),
inference(duplicate_literals_removal,[status(thm)],[f23965]) ).
fof(f23967,plain,
! [X0] :
( sK523_skl(X0) = v_s_H
| v_s_H = X0 ),
inference(destructive_equality_resolution,[status(thm)],[f23966]) ).
fof(f23968,definition,
! [X0] :
( sQ91_spl
<=> ( v_s_H = X0
| v_s_H = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f23969,plain,
! [X0] :
( ~ sQ91_spl
| v_s_H = X0
| v_s_H = X0 ),
inference(component_clause,[status(thm)],[f23968]) ).
fof(f23978,definition,
! [X0] :
( sQ93_spl
<=> ( v_s_H = X0
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),sK523_skl(X0))) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f23979,plain,
! [X0] :
( ~ sQ93_spl
| v_s_H = X0
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),sK523_skl(X0))) ),
inference(component_clause,[status(thm)],[f23978]) ).
fof(f23981,plain,
( sQ91_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f23964,f23978,f23968]) ).
fof(f23987,plain,
! [X0] :
( ~ sQ91_spl
| X0 = v_s_H ),
inference(duplicate_literals_removal,[status(thm)],[f23969]) ).
fof(f23994,plain,
! [X0,X1] :
( ~ sQ91_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f23987,f23987]) ).
fof(f23999,plain,
( ~ sQ91_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f23994,f20174,f23968]) ).
fof(f24052,plain,
! [X0] :
( ~ sQ93_spl
| v_s_H = X0
| v_s_H = X0
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)) ),
inference(paramodulation,[status(thm)],[f23967,f23979]) ).
fof(f24053,definition,
( sQ96_spl
<=> hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f24054,plain,
( ~ sQ96_spl
| hBOOL(hAPP(hAPP(c_Natural_Oevalc(v_c),v_Z),v_s_H)) ),
inference(component_clause,[status(thm)],[f24053]) ).
fof(f24056,plain,
( ~ sQ93_spl
| sQ91_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f24052,f24053,f23968,f23978]) ).
fof(f24059,plain,
( ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24054,f19871]) ).
fof(f24060,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f24059]) ).
fof(f24061,plain,
$false,
inference(sat_refutation,[status(thm)],[f20744,f20764,f21084,f23981,f23999,f24056,f24060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW350+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/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 : Mon Sep 21 09:48:40 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.77/1.07 % Drodi V4.1.1
% 58.07/8.34 % Refutation found
% 58.07/8.34 % SZS status Theorem for theBenchmark: Theorem is valid
% 58.07/8.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.16/8.51 % Elapsed time: 8.115764 seconds
% 8.16/8.51 % CPU time: 59.120557 seconds
% 8.16/8.51 % Total memory used: 1.157 GB
% 8.16/8.51 % Net memory used: 1.132 GB
%------------------------------------------------------------------------------