%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV849-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 02:49:40 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.34s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 23
% Syntax : Number of formulae : 79 ( 16 unt; 10 def)
% Number of atoms : 218 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 260 ( 121 ~; 129 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 11 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 13 con; 0-2 aty)
% Number of variables : 61 ( 61 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f459,negated_conjecture,
hBOOL(hAPP(v_ba,v_s0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f460,negated_conjecture,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f462,negated_conjecture,
v_ba = v_b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f463,negated_conjecture,
v_ca = v_c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f464,negated_conjecture,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f465,negated_conjecture,
! [V_x] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_x),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,V_x,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f466,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f471,negated_conjecture,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Z),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f472,negated_conjecture,
! [V_Z] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f473,negated_conjecture,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Za),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f474,negated_conjecture,
! [V_Za] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f475,negated_conjecture,
! [V_Z,V_s_H,V_s,V_na] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ hBOOL(hAPP(v_b,V_s))
| ~ c_Natural_Oevaln(v_c,V_s,V_na,V_s_H)
| hBOOL(hAPP(hAPP(v_P,V_Z),V_s_H)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f476,negated_conjecture,
! [V_Za,V_s_Ha,V_sa,V_na] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ hBOOL(hAPP(v_b,V_sa))
| ~ c_Natural_Oevaln(v_c,V_sa,V_na,V_s_Ha)
| hBOOL(hAPP(hAPP(v_P,V_Za),V_s_Ha)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1207,plain,
hBOOL(hAPP(v_ba,v_s0)),
inference(cnf_transformation,[status(thm)],[f459]) ).
fof(f1208,plain,
c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f1210,plain,
v_ba = v_b,
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f1211,plain,
v_ca = v_c,
inference(cnf_transformation,[status(thm)],[f463]) ).
fof(f1212,plain,
hBOOL(hAPP(hAPP(v_P,v_xb),v_s0)),
inference(cnf_transformation,[status(thm)],[f464]) ).
fof(f1213,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))
| c_Hoare__Mirabelle_Otriple__valid(v_na,X0,t_a) ),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f1214,plain,
( ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2))
| hBOOL(hAPP(v_b,v_s2)) ),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f1223,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ! [V_Z] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Z),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ) ),
inference(miniscoping,[status(thm)],[f471]) ).
fof(f1224,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(thm)],[f1223]) ).
fof(f1225,plain,
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ! [V_Z] : ~ hBOOL(hAPP(hAPP(v_P,V_Z),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(miniscoping,[status(thm)],[f472]) ).
fof(f1226,plain,
! [X0] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(thm)],[f1225]) ).
fof(f1227,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ! [V_Za] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| hBOOL(hAPP(hAPP(v_P,V_Za),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ) ),
inference(miniscoping,[status(thm)],[f473]) ).
fof(f1228,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(thm)],[f1227]) ).
fof(f1229,plain,
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ! [V_Za] : ~ hBOOL(hAPP(hAPP(v_P,V_Za),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(miniscoping,[status(thm)],[f474]) ).
fof(f1230,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| ~ hBOOL(hAPP(v_b,v_s2))
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(cnf_transformation,[status(thm)],[f1229]) ).
fof(f1231,plain,
! [V_na] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(V_na)),v_G))
| ! [V_Z,V_s] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ hBOOL(hAPP(v_b,V_s))
| ! [V_s_H] :
( ~ c_Natural_Oevaln(v_c,V_s,V_na,V_s_H)
| hBOOL(hAPP(hAPP(v_P,V_Z),V_s_H)) ) ) ),
inference(miniscoping,[status(thm)],[f475]) ).
fof(f1232,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_n(X3)),v_G))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1231]) ).
fof(f1233,plain,
! [V_na] :
( ~ c_Hoare__Mirabelle_Otriple__valid(V_na,v_n(V_na),t_a)
| ! [V_Za,V_sa] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ hBOOL(hAPP(v_b,V_sa))
| ! [V_s_Ha] :
( ~ c_Natural_Oevaln(v_c,V_sa,V_na,V_s_Ha)
| hBOOL(hAPP(hAPP(v_P,V_Za),V_s_Ha)) ) ) ),
inference(miniscoping,[status(thm)],[f476]) ).
fof(f1234,plain,
! [X0,X1,X2,X3] :
( ~ c_Hoare__Mirabelle_Otriple__valid(X3,v_n(X3),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1233]) ).
fof(f1277,definition,
( sQ0_spl
<=> hBOOL(hAPP(v_b,v_s2)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1280,definition,
( sQ1_spl
<=> hBOOL(hAPP(hAPP(v_P,v_xb),v_s2)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1282,plain,
( sQ1_spl
| ~ hBOOL(hAPP(hAPP(v_P,v_xb),v_s2)) ),
inference(component_clause,[status(thm)],[f1280]) ).
fof(f1283,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1214,f1277,f1280]) ).
fof(f1306,definition,
( sQ8_spl
<=> c_Com_Ocom_OWhile(v_ba,v_ca) = c_Com_Ocom_OWhile(v_b,v_c) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1308,plain,
( sQ8_spl
| c_Com_Ocom_OWhile(v_ba,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(component_clause,[status(thm)],[f1306]) ).
fof(f1309,definition,
! [X0] :
( sQ9_spl
<=> ( ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2)) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
! [X0] :
( ~ sQ9_spl
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1))
| hBOOL(hAPP(hAPP(v_P,X0),v_s2)) ),
inference(component_clause,[status(thm)],[f1309]) ).
fof(f1312,definition,
( sQ10_spl
<=> hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1313,plain,
( ~ sQ10_spl
| hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_G)) ),
inference(component_clause,[status(thm)],[f1312]) ).
fof(f1315,plain,
( sQ10_spl
| sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1224,f1306,f1309,f1312]) ).
fof(f1316,definition,
! [X0] :
( sQ11_spl
<=> ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
! [X0] :
( ~ sQ11_spl
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_s1)) ),
inference(component_clause,[status(thm)],[f1316]) ).
fof(f1319,plain,
( sQ10_spl
| sQ11_spl
| ~ sQ0_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1226,f1306,f1277,f1316,f1312]) ).
fof(f1320,definition,
( sQ12_spl
<=> c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( sQ12_spl
| ~ c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(component_clause,[status(thm)],[f1320]) ).
fof(f1323,plain,
( ~ sQ12_spl
| sQ9_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1228,f1306,f1309,f1320]) ).
fof(f1324,plain,
( ~ sQ12_spl
| sQ11_spl
| ~ sQ0_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f1230,f1306,f1277,f1316,f1320]) ).
fof(f1325,plain,
hBOOL(hAPP(v_b,v_s0)),
inference(forward_demodulation,[status(thm)],[f1210,f1207]) ).
fof(f1327,plain,
c_Natural_Oevaln(v_c,v_s0,v_na,v_s1),
inference(forward_demodulation,[status(thm)],[f1211,f1208]) ).
fof(f1330,plain,
( sQ8_spl
| c_Com_Ocom_OWhile(v_b,v_ca) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(forward_demodulation,[status(thm)],[f1210,f1308]) ).
fof(f1331,plain,
( sQ8_spl
| c_Com_Ocom_OWhile(v_b,v_c) != c_Com_Ocom_OWhile(v_b,v_c) ),
inference(forward_demodulation,[status(thm)],[f1211,f1330]) ).
fof(f1332,plain,
( sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1331]) ).
fof(f1333,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1332]) ).
fof(f1344,plain,
! [X0,X1,X2,X3] :
( c_Hoare__Mirabelle_Otriple__valid(v_na,v_n(X3),t_a)
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,X3,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(resolution,[status(thm)],[f1232,f1213]) ).
fof(f1357,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(hAPP(hAPP(v_P,X3),X5))
| ~ hBOOL(hAPP(v_b,X5))
| ~ c_Natural_Oevaln(v_c,X5,v_na,X4)
| hBOOL(hAPP(hAPP(v_P,X3),X4))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,v_na,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(resolution,[status(thm)],[f1344,f1234]) ).
fof(f1358,definition,
! [X0,X1,X2] :
( sQ15_spl
<=> ( ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,v_na,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1359,plain,
! [X0,X1,X2] :
( ~ sQ15_spl
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ hBOOL(hAPP(v_b,X2))
| ~ c_Natural_Oevaln(v_c,X2,v_na,X1)
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(component_clause,[status(thm)],[f1358]) ).
fof(f1361,plain,
sQ15_spl,
inference(split_clause,[status(thm)],[f1357,f1358]) ).
fof(f1362,plain,
! [X0] :
( ~ sQ15_spl
| ~ hBOOL(hAPP(v_b,v_s0))
| ~ c_Natural_Oevaln(v_c,v_s0,v_na,X0)
| hBOOL(hAPP(hAPP(v_P,v_xb),X0)) ),
inference(resolution,[status(thm)],[f1359,f1212]) ).
fof(f1363,definition,
! [X0] :
( sQ16_spl
<=> ( ~ c_Natural_Oevaln(v_c,v_s0,v_na,X0)
| hBOOL(hAPP(hAPP(v_P,v_xb),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1364,plain,
! [X0] :
( ~ sQ16_spl
| ~ c_Natural_Oevaln(v_c,v_s0,v_na,X0)
| hBOOL(hAPP(hAPP(v_P,v_xb),X0)) ),
inference(component_clause,[status(thm)],[f1363]) ).
fof(f1366,definition,
( sQ17_spl
<=> hBOOL(hAPP(v_b,v_s0)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f1368,plain,
( sQ17_spl
| ~ hBOOL(hAPP(v_b,v_s0)) ),
inference(component_clause,[status(thm)],[f1366]) ).
fof(f1369,plain,
( ~ sQ15_spl
| ~ sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1362,f1363,f1366,f1358]) ).
fof(f1370,plain,
( ~ sQ16_spl
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s1)) ),
inference(resolution,[status(thm)],[f1364,f1327]) ).
fof(f1371,plain,
( ~ sQ16_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1370,f1317]) ).
fof(f1372,plain,
( ~ sQ16_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1371]) ).
fof(f1373,plain,
( sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1368,f1325]) ).
fof(f1374,plain,
sQ17_spl,
inference(contradiction_clause,[status(thm)],[f1373]) ).
fof(f1375,plain,
( ~ sQ10_spl
| c_Hoare__Mirabelle_Otriple__valid(v_na,v_xa,t_a) ),
inference(resolution,[status(thm)],[f1313,f1213]) ).
fof(f1383,plain,
( ~ sQ10_spl
| sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f1322]) ).
fof(f1384,plain,
( ~ sQ10_spl
| sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f1383]) ).
fof(f1390,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| hBOOL(hAPP(hAPP(v_P,v_xb),v_s2)) ),
inference(resolution,[status(thm)],[f1310,f1370]) ).
fof(f1396,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1390,f1282]) ).
fof(f1397,plain,
( ~ sQ16_spl
| ~ sQ9_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1396]) ).
fof(f1398,plain,
$false,
inference(sat_refutation,[status(thm)],[f1283,f1315,f1319,f1323,f1324,f1333,f1361,f1369,f1372,f1374,f1384,f1397]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV849-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 09:27:52 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.09/0.34 % Refutation found
% 0.09/0.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.35 % Elapsed time: 0.051292 seconds
% 0.09/0.35 % CPU time: 0.139516 seconds
% 0.09/0.35 % Total memory used: 122.107 MB
% 0.09/0.35 % Net memory used: 121.849 MB
%------------------------------------------------------------------------------