%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ056-2.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:00 PM UTC 2026
% Result : Unsatisfiable 2.26s 0.85s
% Output : CNFRefutation 2.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 35
% Syntax : Number of formulae : 175 ( 27 unt; 22 def)
% Number of atoms : 526 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 710 ( 359 ~; 329 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 23 prp; 0-5 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 192 ( 192 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [I,T1,T2,T3,T4,J] :
( p(J,T1,T2,T3,T4)
| ~ p(I,T1,T2,T3,T4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [T0,I,T2,T3,T4,J] :
( p(T0,J,T2,T3,T4)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,I,T2,T3,T4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [T0,T1,I,T3,T4,J] :
( p(T0,T1,J,T3,T4)
| ~ neq(T1,J)
| ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,I,T3,T4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [T0,T1,T2,I,T4,J] :
( p(T0,T1,T2,J,T4)
| ~ neq(T2,J)
| ~ neq(T2,I)
| ~ neq(T1,J)
| ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,T2,I,T4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [T0,T1,T2,T3,I,J] :
( p(T0,T1,T2,T3,J)
| ~ neq(T3,J)
| ~ neq(T3,I)
| ~ neq(T2,J)
| ~ neq(T2,I)
| ~ neq(T1,J)
| ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,T2,T3,I) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
neq(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
neq(s0,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
neq(s1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
neq(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
neq(s2,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
neq(s2,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
p(s0,s0,s0,s0,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
~ p(s2,s2,s2,s2,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,plain,
! [T1,T2,T3,T4] :
( ! [J] : p(J,T1,T2,T3,T4)
| ! [I] : ~ p(I,T1,T2,T3,T4) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f18,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X5,X1,X2,X3,X4)
| ~ p(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f19,plain,
! [T0,T2,T3,T4,J] :
( p(T0,J,T2,T3,T4)
| ~ neq(T0,J)
| ! [I] :
( ~ neq(T0,I)
| ~ p(T0,I,T2,T3,T4) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X5,X2,X3,X4)
| ~ neq(X0,X5)
| ~ neq(X0,X1)
| ~ p(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [T0,T1,T3,T4,J] :
( p(T0,T1,J,T3,T4)
| ~ neq(T1,J)
| ! [I] :
( ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,I,T3,T4) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f22,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X1,X5,X3,X4)
| ~ neq(X1,X5)
| ~ neq(X1,X2)
| ~ neq(X0,X5)
| ~ neq(X0,X2)
| ~ p(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f23,plain,
! [T0,T1,T2,T4,J] :
( p(T0,T1,T2,J,T4)
| ~ neq(T2,J)
| ! [I] :
( ~ neq(T2,I)
| ~ neq(T1,J)
| ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,T2,I,T4) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X1,X2,X5,X4)
| ~ neq(X2,X5)
| ~ neq(X2,X3)
| ~ neq(X1,X5)
| ~ neq(X1,X3)
| ~ neq(X0,X5)
| ~ neq(X0,X3)
| ~ p(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f25,plain,
! [T0,T1,T2,T3,J] :
( p(T0,T1,T2,T3,J)
| ~ neq(T3,J)
| ! [I] :
( ~ neq(T3,I)
| ~ neq(T2,J)
| ~ neq(T2,I)
| ~ neq(T1,J)
| ~ neq(T1,I)
| ~ neq(T0,J)
| ~ neq(T0,I)
| ~ p(T0,T1,T2,T3,I) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f26,plain,
! [X0,X1,X2,X3,X4,X5] :
( p(X0,X1,X2,X3,X5)
| ~ neq(X3,X5)
| ~ neq(X3,X4)
| ~ neq(X2,X5)
| ~ neq(X2,X4)
| ~ neq(X1,X5)
| ~ neq(X1,X4)
| ~ neq(X0,X5)
| ~ neq(X0,X4)
| ~ p(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f28,plain,
neq(s0,s1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f29,plain,
neq(s0,s2),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f30,plain,
neq(s1,s0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f32,plain,
neq(s1,s2),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f33,plain,
neq(s2,s0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f34,plain,
neq(s2,s1),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f36,plain,
p(s0,s0,s0,s0,s0),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f37,plain,
~ p(s2,s2,s2,s2,s2),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f38,plain,
! [X0,X1,X2,X3] :
( p(s0,s1,X1,X2,X3)
| ~ neq(s0,X0)
| ~ p(s0,X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f28,f20]) ).
fof(f39,plain,
! [X0,X1,X2,X3] :
( p(s0,s2,X1,X2,X3)
| ~ neq(s0,X0)
| ~ p(s0,X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f29,f20]) ).
fof(f40,plain,
! [X0,X1,X2,X3] :
( p(s1,s0,X1,X2,X3)
| ~ neq(s1,X0)
| ~ p(s1,X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f30,f20]) ).
fof(f42,plain,
! [X0,X1,X2,X3] :
( p(s2,s0,X1,X2,X3)
| ~ neq(s2,X0)
| ~ p(s2,X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f33,f20]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( p(s2,s1,X1,X2,X3)
| ~ neq(s2,X0)
| ~ p(s2,X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f34,f20]) ).
fof(f47,plain,
! [X0] : ~ p(X0,s2,s2,s2,s2),
inference(resolution,[status(thm)],[f37,f18]) ).
fof(f63,plain,
! [X0] :
( ~ neq(s0,X0)
| ~ p(s0,X0,s2,s2,s2) ),
inference(resolution,[status(thm)],[f47,f39]) ).
fof(f82,plain,
~ p(s0,s1,s2,s2,s2),
inference(resolution,[status(thm)],[f63,f28]) ).
fof(f87,plain,
! [X0] : ~ p(X0,s1,s2,s2,s2),
inference(resolution,[status(thm)],[f82,f18]) ).
fof(f91,definition,
( sQ8_spl
<=> neq(s0,s2) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f93,plain,
( sQ8_spl
| ~ neq(s0,s2) ),
inference(component_clause,[status(thm)],[f91]) ).
fof(f94,definition,
( sQ9_spl
<=> neq(s1,s2) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f96,plain,
( sQ9_spl
| ~ neq(s1,s2) ),
inference(component_clause,[status(thm)],[f94]) ).
fof(f106,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f96,f32]) ).
fof(f107,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f106]) ).
fof(f108,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f93,f29]) ).
fof(f109,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f108]) ).
fof(f133,plain,
! [X0,X1] :
( ~ neq(s1,s2)
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s2,s2) ),
inference(resolution,[status(thm)],[f87,f22]) ).
fof(f143,definition,
! [X0,X1] :
( sQ17_spl
<=> ( ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s2,s2) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f144,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s2,s2) ),
inference(component_clause,[status(thm)],[f143]) ).
fof(f146,plain,
( ~ sQ9_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f133,f143,f94]) ).
fof(f153,definition,
( sQ19_spl
<=> p(s0,s1,s0,s2,s2) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f154,plain,
( ~ sQ19_spl
| p(s0,s1,s0,s2,s2) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f155,plain,
( sQ19_spl
| ~ p(s0,s1,s0,s2,s2) ),
inference(component_clause,[status(thm)],[f153]) ).
fof(f182,plain,
! [X0] :
( sQ19_spl
| ~ p(X0,s1,s0,s2,s2) ),
inference(resolution,[status(thm)],[f155,f18]) ).
fof(f191,definition,
( sQ26_spl
<=> neq(s1,s0) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f193,plain,
( sQ26_spl
| ~ neq(s1,s0) ),
inference(component_clause,[status(thm)],[f191]) ).
fof(f209,plain,
! [X0] :
( ~ sQ17_spl
| ~ neq(X0,s2)
| ~ neq(X0,s0)
| ~ p(X0,s1,s0,s2,s2) ),
inference(resolution,[status(thm)],[f144,f30]) ).
fof(f214,plain,
( ~ sQ17_spl
| ~ neq(s1,s0)
| ~ p(s1,s1,s0,s2,s2) ),
inference(resolution,[status(thm)],[f209,f32]) ).
fof(f216,definition,
( sQ29_spl
<=> p(s1,s1,s0,s2,s2) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f218,plain,
( sQ29_spl
| ~ p(s1,s1,s0,s2,s2) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f219,plain,
( ~ sQ17_spl
| ~ sQ26_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f214,f216,f191,f143]) ).
fof(f221,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f193,f30]) ).
fof(f222,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f221]) ).
fof(f240,plain,
! [X0] :
( sQ19_spl
| ~ neq(s2,X0)
| ~ p(s2,X0,s0,s2,s2) ),
inference(resolution,[status(thm)],[f182,f43]) ).
fof(f277,definition,
( sQ39_spl
<=> neq(s0,s1) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f279,plain,
( sQ39_spl
| ~ neq(s0,s1) ),
inference(component_clause,[status(thm)],[f277]) ).
fof(f286,plain,
! [X0] :
( sQ29_spl
| ~ p(X0,s1,s0,s2,s2) ),
inference(resolution,[status(thm)],[f218,f18]) ).
fof(f299,plain,
( ~ sQ19_spl
| sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f154,f286]) ).
fof(f300,plain,
( ~ sQ19_spl
| sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f299]) ).
fof(f323,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f279,f28]) ).
fof(f324,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f323]) ).
fof(f363,plain,
( sQ19_spl
| ~ p(s2,s0,s0,s2,s2) ),
inference(resolution,[status(thm)],[f240,f33]) ).
fof(f380,definition,
( sQ53_spl
<=> neq(s2,s0) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ53_spl
| ~ neq(s2,s0) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f416,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f33]) ).
fof(f417,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f416]) ).
fof(f426,plain,
! [X0] :
( sQ19_spl
| ~ p(X0,s0,s0,s2,s2) ),
inference(resolution,[status(thm)],[f363,f18]) ).
fof(f445,definition,
( sQ63_spl
<=> p(s0,s1,s0,s1,s2) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( ~ sQ63_spl
| p(s0,s1,s0,s1,s2) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f447,plain,
( sQ63_spl
| ~ p(s0,s1,s0,s1,s2) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f454,plain,
! [X0,X1] :
( sQ19_spl
| ~ neq(s0,s2)
| ~ neq(s0,X1)
| ~ neq(s0,s2)
| ~ neq(s0,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s0,s0,X1,s2) ),
inference(resolution,[status(thm)],[f426,f24]) ).
fof(f461,definition,
! [X0,X1] :
( sQ65_spl
<=> ( ~ neq(s0,X1)
| ~ neq(s0,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s0,s0,X1,s2) ) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f462,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ neq(s0,X1)
| ~ neq(s0,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s0,s0,X1,s2) ),
inference(component_clause,[status(thm)],[f461]) ).
fof(f464,plain,
( sQ19_spl
| ~ sQ8_spl
| sQ65_spl ),
inference(split_clause,[status(thm)],[f454,f461,f91,f153]) ).
fof(f469,plain,
! [X0,X1] :
( ~ sQ65_spl
| ~ neq(s0,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s0,s0,X1,s2) ),
inference(duplicate_literals_removal,[status(thm)],[f462]) ).
fof(f490,plain,
! [X0] :
( sQ63_spl
| ~ neq(s0,X0)
| ~ p(s0,X0,s0,s1,s2) ),
inference(resolution,[status(thm)],[f447,f38]) ).
fof(f525,definition,
( sQ75_spl
<=> neq(s2,s1) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f527,plain,
( sQ75_spl
| ~ neq(s2,s1) ),
inference(component_clause,[status(thm)],[f525]) ).
fof(f552,plain,
! [X0] :
( ~ sQ65_spl
| ~ neq(X0,s2)
| ~ neq(X0,s1)
| ~ p(X0,s0,s0,s1,s2) ),
inference(resolution,[status(thm)],[f469,f28]) ).
fof(f589,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f34]) ).
fof(f590,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f589]) ).
fof(f592,plain,
( ~ sQ65_spl
| ~ neq(s0,s2)
| ~ p(s0,s0,s0,s1,s2) ),
inference(resolution,[status(thm)],[f552,f28]) ).
fof(f597,definition,
( sQ86_spl
<=> p(s0,s0,s0,s1,s2) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( sQ86_spl
| ~ p(s0,s0,s0,s1,s2) ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f600,plain,
( ~ sQ65_spl
| ~ sQ8_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f592,f597,f91,f461]) ).
fof(f606,plain,
! [X0] :
( sQ86_spl
| ~ p(X0,s0,s0,s1,s2) ),
inference(resolution,[status(thm)],[f599,f18]) ).
fof(f627,plain,
! [X0] :
( sQ86_spl
| ~ neq(s2,X0)
| ~ p(s2,X0,s0,s1,s2) ),
inference(resolution,[status(thm)],[f606,f42]) ).
fof(f656,plain,
( sQ86_spl
| ~ p(s2,s1,s0,s1,s2) ),
inference(resolution,[status(thm)],[f627,f34]) ).
fof(f674,plain,
! [X0] :
( sQ86_spl
| ~ p(X0,s1,s0,s1,s2) ),
inference(resolution,[status(thm)],[f656,f18]) ).
fof(f687,plain,
( ~ sQ63_spl
| sQ86_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f446,f674]) ).
fof(f688,plain,
( ~ sQ63_spl
| sQ86_spl ),
inference(contradiction_clause,[status(thm)],[f687]) ).
fof(f697,plain,
( sQ63_spl
| ~ p(s0,s2,s0,s1,s2) ),
inference(resolution,[status(thm)],[f490,f29]) ).
fof(f722,plain,
! [X0] :
( sQ63_spl
| ~ p(X0,s2,s0,s1,s2) ),
inference(resolution,[status(thm)],[f697,f18]) ).
fof(f747,plain,
! [X0,X1] :
( sQ63_spl
| ~ neq(s2,s0)
| ~ neq(s2,X1)
| ~ neq(X0,s0)
| ~ neq(X0,X1)
| ~ p(X0,s2,X1,s1,s2) ),
inference(resolution,[status(thm)],[f722,f22]) ).
fof(f757,definition,
! [X0,X1] :
( sQ109_spl
<=> ( ~ neq(s2,X1)
| ~ neq(X0,s0)
| ~ neq(X0,X1)
| ~ p(X0,s2,X1,s1,s2) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f758,plain,
! [X0,X1] :
( ~ sQ109_spl
| ~ neq(s2,X1)
| ~ neq(X0,s0)
| ~ neq(X0,X1)
| ~ p(X0,s2,X1,s1,s2) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f760,plain,
( sQ63_spl
| ~ sQ53_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f747,f757,f380,f445]) ).
fof(f779,plain,
! [X0] :
( ~ sQ109_spl
| ~ neq(X0,s0)
| ~ neq(X0,s1)
| ~ p(X0,s2,s1,s1,s2) ),
inference(resolution,[status(thm)],[f758,f34]) ).
fof(f841,plain,
( ~ sQ109_spl
| ~ neq(s2,s0)
| ~ p(s2,s2,s1,s1,s2) ),
inference(resolution,[status(thm)],[f779,f34]) ).
fof(f843,definition,
( sQ122_spl
<=> p(s2,s2,s1,s1,s2) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( sQ122_spl
| ~ p(s2,s2,s1,s1,s2) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,plain,
( ~ sQ109_spl
| ~ sQ53_spl
| ~ sQ122_spl ),
inference(split_clause,[status(thm)],[f841,f843,f380,f757]) ).
fof(f861,plain,
! [X0] :
( sQ122_spl
| ~ p(X0,s2,s1,s1,s2) ),
inference(resolution,[status(thm)],[f845,f18]) ).
fof(f885,plain,
! [X0] :
( sQ122_spl
| ~ neq(s0,X0)
| ~ p(s0,X0,s1,s1,s2) ),
inference(resolution,[status(thm)],[f861,f39]) ).
fof(f1024,plain,
( sQ122_spl
| ~ p(s0,s1,s1,s1,s2) ),
inference(resolution,[status(thm)],[f885,f28]) ).
fof(f1096,plain,
! [X0] :
( sQ122_spl
| ~ p(X0,s1,s1,s1,s2) ),
inference(resolution,[status(thm)],[f1024,f18]) ).
fof(f1109,plain,
! [X0,X1] :
( sQ122_spl
| ~ neq(s1,s2)
| ~ neq(s1,X1)
| ~ neq(s1,s2)
| ~ neq(s1,X1)
| ~ neq(s1,s2)
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,s1,s1,X1) ),
inference(resolution,[status(thm)],[f1096,f26]) ).
fof(f1113,definition,
! [X0,X1] :
( sQ163_spl
<=> ( ~ neq(s1,X1)
| ~ neq(s1,X1)
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,s1,s1,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f1114,plain,
! [X0,X1] :
( ~ sQ163_spl
| ~ neq(s1,X1)
| ~ neq(s1,X1)
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,s1,s1,X1) ),
inference(component_clause,[status(thm)],[f1113]) ).
fof(f1116,plain,
( sQ122_spl
| ~ sQ9_spl
| sQ163_spl ),
inference(split_clause,[status(thm)],[f1109,f1113,f94,f843]) ).
fof(f1125,plain,
! [X0,X1] :
( ~ sQ163_spl
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,s1,s1,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1114]) ).
fof(f1251,plain,
! [X0] :
( ~ sQ163_spl
| ~ neq(X0,s2)
| ~ neq(X0,s0)
| ~ p(X0,s1,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1125,f30]) ).
fof(f1313,plain,
( ~ sQ163_spl
| ~ neq(s1,s0)
| ~ p(s1,s1,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1251,f32]) ).
fof(f1315,definition,
( sQ194_spl
<=> p(s1,s1,s1,s1,s0) ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
( sQ194_spl
| ~ p(s1,s1,s1,s1,s0) ),
inference(component_clause,[status(thm)],[f1315]) ).
fof(f1318,plain,
( ~ sQ163_spl
| ~ sQ26_spl
| ~ sQ194_spl ),
inference(split_clause,[status(thm)],[f1313,f1315,f191,f1113]) ).
fof(f1408,plain,
! [X0] :
( sQ194_spl
| ~ p(X0,s1,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1317,f18]) ).
fof(f1452,plain,
! [X0] :
( sQ194_spl
| ~ neq(s2,X0)
| ~ p(s2,X0,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1408,f43]) ).
fof(f1634,plain,
( sQ194_spl
| ~ p(s2,s0,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1452,f33]) ).
fof(f1708,plain,
! [X0] :
( sQ194_spl
| ~ p(X0,s0,s1,s1,s0) ),
inference(resolution,[status(thm)],[f1634,f18]) ).
fof(f1749,plain,
! [X0,X1] :
( sQ194_spl
| ~ neq(s0,s1)
| ~ neq(s0,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s0,X1,s1,s0) ),
inference(resolution,[status(thm)],[f1708,f22]) ).
fof(f1759,definition,
! [X0,X1] :
( sQ262_spl
<=> ( ~ neq(s0,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s0,X1,s1,s0) ) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f1760,plain,
! [X0,X1] :
( ~ sQ262_spl
| ~ neq(s0,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s0,X1,s1,s0) ),
inference(component_clause,[status(thm)],[f1759]) ).
fof(f1762,plain,
( sQ194_spl
| ~ sQ39_spl
| sQ262_spl ),
inference(split_clause,[status(thm)],[f1749,f1759,f277,f1315]) ).
fof(f1856,plain,
! [X0] :
( ~ sQ262_spl
| ~ neq(X0,s1)
| ~ neq(X0,s2)
| ~ p(X0,s0,s2,s1,s0) ),
inference(resolution,[status(thm)],[f1760,f29]) ).
fof(f1891,plain,
( ~ sQ262_spl
| ~ neq(s0,s2)
| ~ p(s0,s0,s2,s1,s0) ),
inference(resolution,[status(thm)],[f1856,f28]) ).
fof(f1896,definition,
( sQ282_spl
<=> p(s0,s0,s2,s1,s0) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f1898,plain,
( sQ282_spl
| ~ p(s0,s0,s2,s1,s0) ),
inference(component_clause,[status(thm)],[f1896]) ).
fof(f1899,plain,
( ~ sQ262_spl
| ~ sQ8_spl
| ~ sQ282_spl ),
inference(split_clause,[status(thm)],[f1891,f1896,f91,f1759]) ).
fof(f1927,plain,
! [X0] :
( sQ282_spl
| ~ p(X0,s0,s2,s1,s0) ),
inference(resolution,[status(thm)],[f1898,f18]) ).
fof(f1982,plain,
! [X0] :
( sQ282_spl
| ~ neq(s1,X0)
| ~ p(s1,X0,s2,s1,s0) ),
inference(resolution,[status(thm)],[f1927,f40]) ).
fof(f2096,plain,
( sQ282_spl
| ~ p(s1,s2,s2,s1,s0) ),
inference(resolution,[status(thm)],[f1982,f32]) ).
fof(f2214,plain,
! [X0] :
( sQ282_spl
| ~ p(X0,s2,s2,s1,s0) ),
inference(resolution,[status(thm)],[f2096,f18]) ).
fof(f2258,plain,
! [X0,X1] :
( sQ282_spl
| ~ neq(s2,s1)
| ~ neq(s2,X1)
| ~ neq(s2,s1)
| ~ neq(s2,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s2,s2,X1,s0) ),
inference(resolution,[status(thm)],[f2214,f24]) ).
fof(f2265,definition,
! [X0,X1] :
( sQ339_spl
<=> ( ~ neq(s2,X1)
| ~ neq(s2,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s2,s2,X1,s0) ) ),
introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition]) ).
fof(f2266,plain,
! [X0,X1] :
( ~ sQ339_spl
| ~ neq(s2,X1)
| ~ neq(s2,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s2,s2,X1,s0) ),
inference(component_clause,[status(thm)],[f2265]) ).
fof(f2268,plain,
( sQ282_spl
| ~ sQ75_spl
| sQ339_spl ),
inference(split_clause,[status(thm)],[f2258,f2265,f525,f1896]) ).
fof(f2274,plain,
! [X0,X1] :
( ~ sQ339_spl
| ~ neq(s2,X1)
| ~ neq(X0,s1)
| ~ neq(X0,X1)
| ~ p(X0,s2,s2,X1,s0) ),
inference(duplicate_literals_removal,[status(thm)],[f2266]) ).
fof(f2420,plain,
! [X0] :
( ~ sQ339_spl
| ~ neq(X0,s1)
| ~ neq(X0,s0)
| ~ p(X0,s2,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2274,f33]) ).
fof(f2474,plain,
( ~ sQ339_spl
| ~ neq(s2,s0)
| ~ p(s2,s2,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2420,f34]) ).
fof(f2476,definition,
( sQ370_spl
<=> p(s2,s2,s2,s0,s0) ),
introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition]) ).
fof(f2478,plain,
( sQ370_spl
| ~ p(s2,s2,s2,s0,s0) ),
inference(component_clause,[status(thm)],[f2476]) ).
fof(f2479,plain,
( ~ sQ339_spl
| ~ sQ53_spl
| ~ sQ370_spl ),
inference(split_clause,[status(thm)],[f2474,f2476,f380,f2265]) ).
fof(f2542,plain,
! [X0] :
( sQ370_spl
| ~ p(X0,s2,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2478,f18]) ).
fof(f2574,plain,
! [X0] :
( sQ370_spl
| ~ neq(s0,X0)
| ~ p(s0,X0,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2542,f39]) ).
fof(f2763,plain,
( sQ370_spl
| ~ p(s0,s1,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2574,f28]) ).
fof(f2866,plain,
! [X0] :
( sQ370_spl
| ~ p(X0,s1,s2,s0,s0) ),
inference(resolution,[status(thm)],[f2763,f18]) ).
fof(f2937,plain,
! [X0,X1] :
( sQ370_spl
| ~ neq(s1,s2)
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s0,s0) ),
inference(resolution,[status(thm)],[f2866,f22]) ).
fof(f2947,definition,
! [X0,X1] :
( sQ442_spl
<=> ( ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s0,s0) ) ),
introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition]) ).
fof(f2948,plain,
! [X0,X1] :
( ~ sQ442_spl
| ~ neq(s1,X1)
| ~ neq(X0,s2)
| ~ neq(X0,X1)
| ~ p(X0,s1,X1,s0,s0) ),
inference(component_clause,[status(thm)],[f2947]) ).
fof(f2950,plain,
( sQ370_spl
| ~ sQ9_spl
| sQ442_spl ),
inference(split_clause,[status(thm)],[f2937,f2947,f94,f2476]) ).
fof(f3104,plain,
! [X0] :
( ~ sQ442_spl
| ~ neq(X0,s2)
| ~ neq(X0,s0)
| ~ p(X0,s1,s0,s0,s0) ),
inference(resolution,[status(thm)],[f2948,f30]) ).
fof(f3200,plain,
( ~ sQ442_spl
| ~ neq(s1,s0)
| ~ p(s1,s1,s0,s0,s0) ),
inference(resolution,[status(thm)],[f3104,f32]) ).
fof(f3202,definition,
( sQ480_spl
<=> p(s1,s1,s0,s0,s0) ),
introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition]) ).
fof(f3204,plain,
( sQ480_spl
| ~ p(s1,s1,s0,s0,s0) ),
inference(component_clause,[status(thm)],[f3202]) ).
fof(f3205,plain,
( ~ sQ442_spl
| ~ sQ26_spl
| ~ sQ480_spl ),
inference(split_clause,[status(thm)],[f3200,f3202,f191,f2947]) ).
fof(f3270,plain,
! [X0] :
( sQ480_spl
| ~ p(X0,s1,s0,s0,s0) ),
inference(resolution,[status(thm)],[f3204,f18]) ).
fof(f3338,plain,
! [X0] :
( sQ480_spl
| ~ neq(s2,X0)
| ~ p(s2,X0,s0,s0,s0) ),
inference(resolution,[status(thm)],[f3270,f43]) ).
fof(f3525,plain,
( sQ480_spl
| ~ p(s2,s0,s0,s0,s0) ),
inference(resolution,[status(thm)],[f3338,f33]) ).
fof(f3735,plain,
! [X0] :
( sQ480_spl
| ~ p(X0,s0,s0,s0,s0) ),
inference(resolution,[status(thm)],[f3525,f18]) ).
fof(f3748,plain,
( sQ480_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f36,f3735]) ).
fof(f3749,plain,
sQ480_spl,
inference(contradiction_clause,[status(thm)],[f3748]) ).
fof(f3750,plain,
$false,
inference(sat_refutation,[status(thm)],[f107,f109,f146,f219,f222,f300,f324,f417,f464,f590,f600,f688,f760,f846,f1116,f1318,f1762,f1899,f2268,f2479,f2950,f3205,f3749]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ056-2.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 03:48:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 2.26/0.85 % Refutation found
% 2.26/0.85 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.26/0.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.26/0.86 % Elapsed time: 0.480832 seconds
% 2.26/0.86 % CPU time: 3.488031 seconds
% 2.26/0.86 % Total memory used: 79.677 MB
% 2.26/0.86 % Net memory used: 74.820 MB
%------------------------------------------------------------------------------