%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ001-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:00:12 PM UTC 2026
% Result : Satisfiable 0.02s 0.32s
% Output : Saturation 0.02s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
lives(agatha),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
lives(butler),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
lives(charles),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( ~ richer(X,Y)
| ~ killed(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] :
( ~ hates(charles,X)
| ~ hates(agatha,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( ~ hates(X,charles)
| ~ hates(X,butler)
| ~ hates(X,agatha) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
hates(agatha,agatha),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
hates(agatha,charles),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( hates(X,Y)
| ~ killed(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] :
( hates(butler,X)
| ~ hates(agatha,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] :
( hates(butler,X)
| richer(X,agatha)
| ~ lives(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
( killed(charles,agatha)
| killed(butler,agatha)
| killed(agatha,agatha) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,plain,
lives(agatha),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f14,plain,
lives(butler),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f15,plain,
lives(charles),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f16,plain,
! [X0,X1] :
( ~ richer(X0,X1)
| ~ killed(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
! [X0] :
( ~ hates(charles,X0)
| ~ hates(agatha,X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f18,plain,
! [X0] :
( ~ hates(X0,charles)
| ~ hates(X0,butler)
| ~ hates(X0,agatha) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f19,plain,
hates(agatha,agatha),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f20,plain,
hates(agatha,charles),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0,X1] :
( hates(X0,X1)
| ~ killed(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
! [X0] :
( hates(butler,X0)
| ~ hates(agatha,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f23,plain,
! [X0] :
( hates(butler,X0)
| richer(X0,agatha)
| ~ lives(X0) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f24,plain,
( killed(charles,agatha)
| killed(butler,agatha)
| killed(agatha,agatha) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f25,definition,
( sQ0_spl
<=> killed(agatha,agatha) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f26,plain,
( ~ sQ0_spl
| killed(agatha,agatha) ),
inference(component_clause,[status(thm)],[f25]) ).
fof(f28,definition,
( sQ1_spl
<=> killed(butler,agatha) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f31,definition,
( sQ2_spl
<=> killed(charles,agatha) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f32,plain,
( ~ sQ2_spl
| killed(charles,agatha) ),
inference(component_clause,[status(thm)],[f31]) ).
fof(f33,plain,
( sQ2_spl
| ~ killed(charles,agatha) ),
inference(component_clause,[status(thm)],[f31]) ).
fof(f34,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f24,f25,f28,f31]) ).
fof(f35,plain,
( ~ hates(agatha,butler)
| ~ hates(agatha,agatha) ),
inference(resolution,[status(thm)],[f20,f18]) ).
fof(f36,definition,
( sQ3_spl
<=> hates(agatha,agatha) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f38,plain,
( sQ3_spl
| ~ hates(agatha,agatha) ),
inference(component_clause,[status(thm)],[f36]) ).
fof(f39,definition,
( sQ4_spl
<=> hates(agatha,butler) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f41,plain,
( sQ4_spl
| ~ hates(agatha,butler) ),
inference(component_clause,[status(thm)],[f39]) ).
fof(f42,plain,
( ~ sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f35,f36,f39]) ).
fof(f43,plain,
( ~ sQ2_spl
| hates(charles,agatha) ),
inference(resolution,[status(thm)],[f21,f32]) ).
fof(f44,plain,
hates(butler,charles),
inference(resolution,[status(thm)],[f22,f20]) ).
fof(f45,plain,
( ~ sQ2_spl
| ~ hates(agatha,agatha) ),
inference(resolution,[status(thm)],[f43,f17]) ).
fof(f46,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19,f38]) ).
fof(f47,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f46]) ).
fof(f48,plain,
( ~ sQ2_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f45,f36,f31]) ).
fof(f49,plain,
hates(butler,agatha),
inference(resolution,[status(thm)],[f19,f22]) ).
fof(f51,plain,
( ~ hates(butler,butler)
| ~ hates(butler,agatha) ),
inference(resolution,[status(thm)],[f44,f18]) ).
fof(f52,definition,
( sQ5_spl
<=> hates(butler,agatha) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f54,plain,
( sQ5_spl
| ~ hates(butler,agatha) ),
inference(component_clause,[status(thm)],[f52]) ).
fof(f55,definition,
( sQ6_spl
<=> hates(butler,butler) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f57,plain,
( sQ6_spl
| ~ hates(butler,butler) ),
inference(component_clause,[status(thm)],[f55]) ).
fof(f58,plain,
( ~ sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f51,f52,f55]) ).
fof(f59,plain,
( hates(butler,charles)
| richer(charles,agatha) ),
inference(resolution,[status(thm)],[f23,f15]) ).
fof(f60,plain,
( hates(butler,butler)
| richer(butler,agatha) ),
inference(resolution,[status(thm)],[f23,f14]) ).
fof(f62,definition,
( sQ7_spl
<=> richer(charles,agatha) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f63,plain,
( ~ sQ7_spl
| richer(charles,agatha) ),
inference(component_clause,[status(thm)],[f62]) ).
fof(f65,definition,
( sQ8_spl
<=> hates(butler,charles) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f68,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f59,f62,f65]) ).
fof(f69,definition,
( sQ9_spl
<=> richer(butler,agatha) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f70,plain,
( ~ sQ9_spl
| richer(butler,agatha) ),
inference(component_clause,[status(thm)],[f69]) ).
fof(f72,plain,
( sQ6_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f60,f69,f55]) ).
fof(f73,definition,
( sQ10_spl
<=> richer(agatha,agatha) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f74,plain,
( ~ sQ10_spl
| richer(agatha,agatha) ),
inference(component_clause,[status(thm)],[f73]) ).
fof(f77,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f54,f49]) ).
fof(f78,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f77]) ).
fof(f79,plain,
( ~ sQ9_spl
| ~ killed(butler,agatha) ),
inference(resolution,[status(thm)],[f70,f16]) ).
fof(f80,plain,
( ~ sQ7_spl
| ~ killed(charles,agatha) ),
inference(resolution,[status(thm)],[f63,f16]) ).
fof(model,axiom,
( sQ0_spl
| ~ sQ2_spl
| sQ3_spl
| ~ sQ4_spl
| sQ5_spl
| ~ sQ6_spl
| sQ7_spl
| sQ9_spl ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PUZ001-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Mon Sep 21 03:44:22 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Drodi V4.1.1
% 0.02/0.32 % SZS status Satisfiable for theBenchmark: Theory is satisfiable
% 0.02/0.32 % SZS output start Saturation for theBenchmark
% See solution above
% 0.02/0.33 % Elapsed time: 0.030901 seconds
% 0.02/0.33 % CPU time: 0.068211 seconds
% 0.02/0.33 % Total memory used: 16.711 MB
% 0.02/0.33 % Net memory used: 16.273 MB
%------------------------------------------------------------------------------