%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ008-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 01:59:50 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.39s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 33
% Syntax : Number of formulae : 118 ( 27 unt; 21 def)
% Number of atoms : 275 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 286 ( 129 ~; 136 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 25 ( 24 usr; 22 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 69 ( 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : safe(n0,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( safe(X,Y)
| ~ greater_or_equal(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : greater_or_equal(X,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( ~ greater_or_equal(X,Y)
| greater_or_equal(s(X),s(Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z,W] :
( achievable(west(m(X),c(s(Y))),boatonwest,east(m(Z),c(W)))
| ~ safe(Z,W)
| ~ safe(X,s(Y))
| ~ achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(W)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z,W] :
( achievable(west(m(X),c(Y)),boatoneast,east(m(Z),c(s(s(W)))))
| ~ safe(Z,s(s(W)))
| ~ safe(X,Y)
| ~ achievable(west(m(X),c(s(s(Y)))),boatonwest,east(m(Z),c(W))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y,Z,W] :
( achievable(west(m(s(X)),c(Y)),boatonwest,east(m(Z),c(W)))
| ~ safe(Z,W)
| ~ safe(s(X),Y)
| ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(W))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,Z,W] :
( achievable(west(m(X),c(Y)),boatoneast,east(m(s(s(Z))),c(W)))
| ~ safe(s(s(Z)),W)
| ~ safe(X,Y)
| ~ achievable(west(m(s(s(X))),c(Y)),boatonwest,east(m(Z),c(W))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X,Y,Z,W] :
( achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W))))
| ~ safe(s(Z),s(W))
| ~ safe(X,Y)
| ~ achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y,Z,W] :
( achievable(west(m(s(X)),c(s(Y))),boatonwest,east(m(Z),c(W)))
| ~ safe(Z,W)
| ~ safe(s(X),s(Y))
| ~ achievable(west(m(X),c(Y)),boatoneast,east(m(s(Z)),c(s(W)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
achievable(west(m(s(s(s(n0)))),c(s(s(s(n0))))),boatonwest,east(m(n0),c(n0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [X] : ~ achievable(west(m(n0),c(n0)),X,east(m(s(s(s(n0)))),c(s(s(s(n0)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,plain,
! [X0] : safe(n0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f18,plain,
! [X0,X1] :
( safe(X0,X1)
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f19,plain,
! [X0] : greater_or_equal(X0,n0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f20,plain,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| greater_or_equal(s(X0),s(X1)) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f22,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(X0),c(s(X1))),boatonwest,east(m(X2),c(X3)))
| ~ safe(X2,X3)
| ~ safe(X0,s(X1))
| ~ achievable(west(m(X0),c(X1)),boatoneast,east(m(X2),c(s(X3)))) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(X0),c(X1)),boatoneast,east(m(X2),c(s(s(X3)))))
| ~ safe(X2,s(s(X3)))
| ~ safe(X0,X1)
| ~ achievable(west(m(X0),c(s(s(X1)))),boatonwest,east(m(X2),c(X3))) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(s(X0)),c(X1)),boatonwest,east(m(X2),c(X3)))
| ~ safe(X2,X3)
| ~ safe(s(X0),X1)
| ~ achievable(west(m(X0),c(X1)),boatoneast,east(m(s(X2)),c(X3))) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f27,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(X0),c(X1)),boatoneast,east(m(s(s(X2))),c(X3)))
| ~ safe(s(s(X2)),X3)
| ~ safe(X0,X1)
| ~ achievable(west(m(s(s(X0))),c(X1)),boatonwest,east(m(X2),c(X3))) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f29,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(X0),c(X1)),boatoneast,east(m(s(X2)),c(s(X3))))
| ~ safe(s(X2),s(X3))
| ~ safe(X0,X1)
| ~ achievable(west(m(s(X0)),c(s(X1))),boatonwest,east(m(X2),c(X3))) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( achievable(west(m(s(X0)),c(s(X1))),boatonwest,east(m(X2),c(X3)))
| ~ safe(X2,X3)
| ~ safe(s(X0),s(X1))
| ~ achievable(west(m(X0),c(X1)),boatoneast,east(m(s(X2)),c(s(X3)))) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f31,plain,
achievable(west(m(s(s(s(n0)))),c(s(s(s(n0))))),boatonwest,east(m(n0),c(n0))),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f32,plain,
! [X0] : ~ achievable(west(m(n0),c(n0)),X0,east(m(s(s(s(n0)))),c(s(s(s(n0)))))),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f33,plain,
! [X0] : safe(X0,n0),
inference(resolution,[status(thm)],[f18,f19]) ).
fof(f34,plain,
! [X0] : greater_or_equal(s(X0),s(n0)),
inference(resolution,[status(thm)],[f20,f19]) ).
fof(f35,plain,
! [X0] : greater_or_equal(s(s(X0)),s(s(n0))),
inference(resolution,[status(thm)],[f34,f20]) ).
fof(f36,plain,
! [X0] : safe(s(X0),s(n0)),
inference(resolution,[status(thm)],[f34,f18]) ).
fof(f37,plain,
! [X0] : greater_or_equal(s(s(s(X0))),s(s(s(n0)))),
inference(resolution,[status(thm)],[f35,f20]) ).
fof(f38,plain,
! [X0] : safe(s(s(X0)),s(s(n0))),
inference(resolution,[status(thm)],[f35,f18]) ).
fof(f40,plain,
! [X0] : safe(s(s(s(X0))),s(s(s(n0)))),
inference(resolution,[status(thm)],[f37,f18]) ).
fof(f50,plain,
( achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0)))))
| ~ safe(n0,s(s(n0)))
| ~ safe(s(s(s(n0))),s(n0)) ),
inference(resolution,[status(thm)],[f31,f23]) ).
fof(f62,definition,
( sQ3_spl
<=> safe(s(s(s(n0))),s(n0)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f64,plain,
( sQ3_spl
| ~ safe(s(s(s(n0))),s(n0)) ),
inference(component_clause,[status(thm)],[f62]) ).
fof(f65,definition,
( sQ4_spl
<=> safe(n0,s(s(n0))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f67,plain,
( sQ4_spl
| ~ safe(n0,s(s(n0))) ),
inference(component_clause,[status(thm)],[f65]) ).
fof(f68,definition,
( sQ5_spl
<=> achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f69,plain,
( ~ sQ5_spl
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatoneast,east(m(n0),c(s(s(n0))))) ),
inference(component_clause,[status(thm)],[f68]) ).
fof(f71,plain,
( sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f50,f62,f65,f68]) ).
fof(f72,definition,
( sQ6_spl
<=> safe(s(s(s(n0))),s(s(n0))) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f74,plain,
( sQ6_spl
| ~ safe(s(s(s(n0))),s(s(n0))) ),
inference(component_clause,[status(thm)],[f72]) ).
fof(f75,definition,
( sQ7_spl
<=> safe(n0,s(n0)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f77,plain,
( sQ7_spl
| ~ safe(n0,s(n0)) ),
inference(component_clause,[status(thm)],[f75]) ).
fof(f82,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f77,f17]) ).
fof(f83,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f82]) ).
fof(f84,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f74,f38]) ).
fof(f85,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f84]) ).
fof(f86,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f67,f17]) ).
fof(f87,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f86]) ).
fof(f88,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f64,f36]) ).
fof(f89,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f88]) ).
fof(f91,definition,
( sQ9_spl
<=> safe(s(s(s(n0))),s(s(s(n0)))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f93,plain,
( sQ9_spl
| ~ safe(s(s(s(n0))),s(s(s(n0)))) ),
inference(component_clause,[status(thm)],[f91]) ).
fof(f94,definition,
( sQ10_spl
<=> safe(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( sQ10_spl
| ~ safe(n0,n0) ),
inference(component_clause,[status(thm)],[f94]) ).
fof(f101,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f96,f17]) ).
fof(f102,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f101]) ).
fof(f103,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f93,f40]) ).
fof(f104,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f103]) ).
fof(f106,plain,
( ~ sQ5_spl
| achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0))))
| ~ safe(n0,s(n0))
| ~ safe(s(s(s(n0))),s(s(n0))) ),
inference(resolution,[status(thm)],[f69,f22]) ).
fof(f108,definition,
( sQ12_spl
<=> achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0)))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f109,plain,
( ~ sQ12_spl
| achievable(west(m(s(s(s(n0)))),c(s(s(n0)))),boatonwest,east(m(n0),c(s(n0)))) ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,plain,
( ~ sQ5_spl
| sQ12_spl
| ~ sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f106,f72,f75,f108,f68]) ).
fof(f129,plain,
( ~ sQ12_spl
| achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0))))))
| ~ safe(n0,s(s(s(n0))))
| ~ safe(s(s(s(n0))),n0) ),
inference(resolution,[status(thm)],[f109,f23]) ).
fof(f141,definition,
( sQ19_spl
<=> safe(s(s(n0)),s(s(n0))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f143,plain,
( sQ19_spl
| ~ safe(s(s(n0)),s(s(n0))) ),
inference(component_clause,[status(thm)],[f141]) ).
fof(f144,definition,
( sQ20_spl
<=> safe(s(n0),s(n0)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f146,plain,
( sQ20_spl
| ~ safe(s(n0),s(n0)) ),
inference(component_clause,[status(thm)],[f144]) ).
fof(f151,definition,
( sQ22_spl
<=> safe(s(s(s(n0))),n0) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f153,plain,
( sQ22_spl
| ~ safe(s(s(s(n0))),n0) ),
inference(component_clause,[status(thm)],[f151]) ).
fof(f154,definition,
( sQ23_spl
<=> safe(n0,s(s(s(n0)))) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f156,plain,
( sQ23_spl
| ~ safe(n0,s(s(s(n0)))) ),
inference(component_clause,[status(thm)],[f154]) ).
fof(f157,definition,
( sQ24_spl
<=> achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f158,plain,
( ~ sQ24_spl
| achievable(west(m(s(s(s(n0)))),c(n0)),boatoneast,east(m(n0),c(s(s(s(n0)))))) ),
inference(component_clause,[status(thm)],[f157]) ).
fof(f160,plain,
( ~ sQ12_spl
| sQ24_spl
| ~ sQ23_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f129,f151,f154,f157,f108]) ).
fof(f162,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f156,f17]) ).
fof(f163,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f162]) ).
fof(f164,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f153,f33]) ).
fof(f165,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f164]) ).
fof(f166,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f146,f36]) ).
fof(f167,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f166]) ).
fof(f168,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f143,f38]) ).
fof(f169,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f168]) ).
fof(f180,plain,
( ~ sQ24_spl
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0)))))
| ~ safe(n0,s(s(n0)))
| ~ safe(s(s(s(n0))),s(n0)) ),
inference(resolution,[status(thm)],[f158,f22]) ).
fof(f182,definition,
( sQ26_spl
<=> achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( ~ sQ26_spl
| achievable(west(m(s(s(s(n0)))),c(s(n0))),boatonwest,east(m(n0),c(s(s(n0))))) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( ~ sQ24_spl
| sQ26_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f180,f62,f65,f182,f157]) ).
fof(f197,plain,
( ~ sQ26_spl
| achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0)))))
| ~ safe(s(s(n0)),s(s(n0)))
| ~ safe(s(n0),s(n0)) ),
inference(resolution,[status(thm)],[f183,f27]) ).
fof(f201,definition,
( sQ28_spl
<=> achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f202,plain,
( ~ sQ28_spl
| achievable(west(m(s(n0)),c(s(n0))),boatoneast,east(m(s(s(n0))),c(s(s(n0))))) ),
inference(component_clause,[status(thm)],[f201]) ).
fof(f204,plain,
( ~ sQ26_spl
| sQ28_spl
| ~ sQ19_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f197,f144,f141,f201,f182]) ).
fof(f230,plain,
( ~ sQ28_spl
| achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0))))
| ~ safe(s(n0),s(n0))
| ~ safe(s(s(n0)),s(s(n0))) ),
inference(resolution,[status(thm)],[f30,f202]) ).
fof(f232,definition,
( sQ33_spl
<=> achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0)))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( ~ sQ33_spl
| achievable(west(m(s(s(n0))),c(s(s(n0)))),boatonwest,east(m(s(n0)),c(s(n0)))) ),
inference(component_clause,[status(thm)],[f232]) ).
fof(f235,plain,
( ~ sQ28_spl
| sQ33_spl
| ~ sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f230,f141,f144,f232,f201]) ).
fof(f237,plain,
( ~ sQ33_spl
| achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0))))
| ~ safe(s(s(s(n0))),s(n0))
| ~ safe(n0,s(s(n0))) ),
inference(resolution,[status(thm)],[f233,f27]) ).
fof(f242,definition,
( sQ34_spl
<=> achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0)))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f243,plain,
( ~ sQ34_spl
| achievable(west(m(n0),c(s(s(n0)))),boatoneast,east(m(s(s(s(n0)))),c(s(n0)))) ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,plain,
( ~ sQ33_spl
| sQ34_spl
| ~ sQ3_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f237,f65,f62,f242,f232]) ).
fof(f253,plain,
( ~ sQ34_spl
| achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0)))
| ~ safe(s(s(s(n0))),n0)
| ~ safe(n0,s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f243,f22]) ).
fof(f257,definition,
( sQ35_spl
<=> achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f258,plain,
( ~ sQ35_spl
| achievable(west(m(n0),c(s(s(s(n0))))),boatonwest,east(m(s(s(s(n0)))),c(n0))) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f260,plain,
( ~ sQ34_spl
| sQ35_spl
| ~ sQ22_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f253,f154,f151,f257,f242]) ).
fof(f261,plain,
( ~ sQ35_spl
| achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0)))))
| ~ safe(s(s(s(n0))),s(s(n0)))
| ~ safe(n0,s(n0)) ),
inference(resolution,[status(thm)],[f258,f23]) ).
fof(f263,definition,
( sQ36_spl
<=> achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f264,plain,
( ~ sQ36_spl
| achievable(west(m(n0),c(s(n0))),boatoneast,east(m(s(s(s(n0)))),c(s(s(n0))))) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,plain,
( ~ sQ35_spl
| sQ36_spl
| ~ sQ6_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f261,f75,f72,f263,f257]) ).
fof(f272,plain,
( ~ sQ36_spl
| achievable(west(m(s(n0)),c(s(n0))),boatonwest,east(m(s(s(n0))),c(s(s(n0)))))
| ~ safe(s(s(n0)),s(s(n0)))
| ~ safe(s(n0),s(n0)) ),
inference(resolution,[status(thm)],[f264,f26]) ).
fof(f277,definition,
( sQ37_spl
<=> achievable(west(m(s(n0)),c(s(n0))),boatonwest,east(m(s(s(n0))),c(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( ~ sQ37_spl
| achievable(west(m(s(n0)),c(s(n0))),boatonwest,east(m(s(s(n0))),c(s(s(n0))))) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f280,plain,
( ~ sQ36_spl
| sQ37_spl
| ~ sQ19_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f272,f144,f141,f277,f263]) ).
fof(f286,plain,
( ~ sQ37_spl
| achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0))))))
| ~ safe(s(s(s(n0))),s(s(s(n0))))
| ~ safe(n0,n0) ),
inference(resolution,[status(thm)],[f278,f29]) ).
fof(f289,definition,
( sQ39_spl
<=> achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f290,plain,
( ~ sQ39_spl
| achievable(west(m(n0),c(n0)),boatoneast,east(m(s(s(s(n0)))),c(s(s(s(n0)))))) ),
inference(component_clause,[status(thm)],[f289]) ).
fof(f292,plain,
( ~ sQ37_spl
| sQ39_spl
| ~ sQ9_spl
| ~ sQ10_spl ),
inference(split_clause,[status(thm)],[f286,f94,f91,f289,f277]) ).
fof(f298,plain,
( ~ sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f290,f32]) ).
fof(f299,plain,
~ sQ39_spl,
inference(contradiction_clause,[status(thm)],[f298]) ).
fof(f300,plain,
$false,
inference(sat_refutation,[status(thm)],[f71,f83,f85,f87,f89,f102,f104,f111,f160,f163,f165,f167,f169,f185,f204,f235,f245,f260,f266,f280,f292,f299]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ008-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:48:06 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.14/0.39 % Refutation found
% 0.14/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.41 % Elapsed time: 0.047424 seconds
% 0.14/0.41 % CPU time: 0.129435 seconds
% 0.14/0.41 % Total memory used: 32.990 MB
% 0.14/0.41 % Net memory used: 32.797 MB
%------------------------------------------------------------------------------