%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW345+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:09:00 PM UTC 2026
% Result : Theorem 177.52s 24.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW345+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n019.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Mon Sep 21 09:48:20 UTC 2026
% 0.20/0.46 % CPUTime :
% 1.21/1.57 % Drodi V4.1.1
% 177.52/24.60 % Refutation found
% 177.52/24.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 177.52/24.60 % SZS output start CNFRefutation for theBenchmark
% 177.52/24.60 fof(f5206,hypothesis,(
% 177.52/24.60 (! [B_Z,B_s] :( v_P(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(v_c,B_s,v_n,B_s_H)=> v_Q(B_Z,B_s_H) ) )) )),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5207,hypothesis,(
% 177.52/24.60 (! [B_Z,B_s] :( v_Q(B_Z,B_s)=> (! [B_s_H] :( c_Natural_Oevaln(v_d,B_s,v_n,B_s_H)=> v_R(B_Z,B_s_H) ) )) )),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5208,hypothesis,(
% 177.52/24.60 v_P(v_Z,v_s) ),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5209,hypothesis,(
% 177.52/24.60 c_Natural_Oevaln(v_c,v_s,v_n,v_s1) ),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5210,hypothesis,(
% 177.52/24.60 c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H) ),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5211,conjecture,(
% 177.52/24.60 v_R(v_Z,v_s_H) ),
% 177.52/24.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 177.52/24.60 fof(f5212,negated_conjecture,(
% 177.52/24.60 ~(v_R(v_Z,v_s_H) )),
% 177.52/24.60 inference(negated_conjecture,[status(cth)],[f5211])).
% 177.52/24.60 fof(f19795,plain,(
% 177.52/24.60 ![B_Z,B_s]: (~v_P(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(v_c,B_s,v_n,B_s_H)|v_Q(B_Z,B_s_H))))),
% 177.52/24.60 inference(pre_NNF_transformation,[status(thm)],[f5206])).
% 177.52/24.60 fof(f19796,plain,(
% 177.52/24.60 ![X0,X1,X2]: (~v_P(X0,X1)|~c_Natural_Oevaln(v_c,X1,v_n,X2)|v_Q(X0,X2))),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f19795])).
% 177.52/24.60 fof(f19797,plain,(
% 177.52/24.60 ![B_Z,B_s]: (~v_Q(B_Z,B_s)|(![B_s_H]: (~c_Natural_Oevaln(v_d,B_s,v_n,B_s_H)|v_R(B_Z,B_s_H))))),
% 177.52/24.60 inference(pre_NNF_transformation,[status(thm)],[f5207])).
% 177.52/24.60 fof(f19798,plain,(
% 177.52/24.60 ![X0,X1,X2]: (~v_Q(X0,X1)|~c_Natural_Oevaln(v_d,X1,v_n,X2)|v_R(X0,X2))),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f19797])).
% 177.52/24.60 fof(f19799,plain,(
% 177.52/24.60 v_P(v_Z,v_s)),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f5208])).
% 177.52/24.60 fof(f19800,plain,(
% 177.52/24.60 c_Natural_Oevaln(v_c,v_s,v_n,v_s1)),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f5209])).
% 177.52/24.60 fof(f19801,plain,(
% 177.52/24.60 c_Natural_Oevaln(v_d,v_s1,v_n,v_s_H)),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f5210])).
% 177.52/24.60 fof(f19802,plain,(
% 177.52/24.60 ~v_R(v_Z,v_s_H)),
% 177.52/24.60 inference(cnf_transformation,[status(thm)],[f5212])).
% 177.52/24.60 fof(f70695,plain,(
% 177.52/24.60 ![X0,X1,X2,X3]: (~v_P(X0,X1)|~c_Natural_Oevaln(v_c,X1,v_n,X2)|~c_Natural_Oevaln(v_d,X2,v_n,X3)|v_R(X0,X3))),
% 177.52/24.60 inference(resolution,[status(thm)],[f19796,f19798])).
% 177.52/24.60 fof(f71106,plain,(
% 177.52/24.60 ![X0,X1]: (~v_P(v_Z,X0)|~c_Natural_Oevaln(v_c,X0,v_n,X1)|~c_Natural_Oevaln(v_d,X1,v_n,v_s_H))),
% 177.52/24.60 inference(resolution,[status(thm)],[f70695,f19802])).
% 177.52/24.60 fof(f71107,plain,(
% 177.52/24.60 ![X0]: (~v_P(v_Z,X0)|~c_Natural_Oevaln(v_c,X0,v_n,v_s1))),
% 177.52/24.60 inference(resolution,[status(thm)],[f71106,f19801])).
% 177.52/24.60 fof(f71108,plain,(
% 177.52/24.60 ~v_P(v_Z,v_s)),
% 177.52/24.60 inference(resolution,[status(thm)],[f71107,f19800])).
% 177.52/24.60 fof(f71109,plain,(
% 177.52/24.60 $false),
% 177.52/24.60 inference(forward_subsumption_resolution,[status(thm)],[f71108,f19799])).
% 177.52/24.60 % SZS output end CNFRefutation for theBenchmark.p
% 110.04/24.69 % Elapsed time: 24.197365 seconds
% 110.04/24.69 % CPU time: 183.503389 seconds
% 110.04/24.69 % Total memory used: 1.865 GB
% 110.04/24.69 % Net memory used: 1.789 GB
%------------------------------------------------------------------------------