%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO003+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:14 PM UTC 2026
% Result : Theorem 36.46s 15.21s
% Output : CNFRefutation 37.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 15
% Syntax : Number of formulae : 115 ( 37 unt; 0 def)
% Number of atoms : 337 ( 31 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 362 ( 140 ~; 136 |; 73 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 207 ( 183 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity_occurrence(X1)
& activity(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X69,X70,X71] :
( min_precedes(X70,X71,X69)
=> ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X76,X77] :
( ( ~ atomic(X76)
& occurrence_of(X77,X76) )
=> ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X105,X106,X107,X108] :
( ( root_occ(X106,X107)
& root_occ(X105,X107)
& occurrence_of(X107,X108) )
=> X105 = X106 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [X121,X122,X123,X124,X125] :
( ( subactivity_occurrence(X122,X125)
& subactivity_occurrence(X123,X125)
& occurrence_of(X125,X124)
& next_subocc(X121,X123,X124)
& next_subocc(X121,X122,X124) )
=> X122 = X123 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& occurrence_of(X163,tptp3)
& root_occ(X162,X161)
& occurrence_of(X162,tptp4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X164,X165] :
( ( root_occ(X164,X165)
& occurrence_of(X165,tptp0) )
=> ? [X166] :
( next_subocc(X164,X166,tptp0)
& occurrence_of(X166,tptp1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,conjecture,
~ ? [X167] : occurrence_of(X167,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,negated_conjecture,
~ ~ ? [X167] : occurrence_of(X167,tptp0),
inference(negated_conjecture,[status(cth)],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( ( activity_occurrence(X1)
& activity(X0) )
| ~ occurrence_of(X1,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f68,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f69,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f70,plain,
! [X2] :
( ( occurrence_of(X2,sK0_skl(X2))
& activity(sK0_skl(X2)) )
| ~ activity_occurrence(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X3,sK0_skl(X2))],[f69]) ).
fof(f72,plain,
! [X0] :
( occurrence_of(X0,sK0_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f73,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f74,plain,
! [X5,X6] :
( X5 = X6
| ! [X4] :
( ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X2,X0)
| ~ occurrence_of(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f144,plain,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f145,plain,
! [X60,X61,X62] :
( ( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(NNF_transformation,[status(thm)],[f144]) ).
fof(f146,plain,
( ! [X60,X61,X62] :
( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ! [X60,X61,X62] :
( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f147,plain,
( ! [X60,X61,X62] :
( ( min_precedes(sK7_skl(X62,X61,X60),X61,X62)
& min_precedes(X60,sK7_skl(X62,X61,X60),X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ! [X60,X61,X62] :
( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f162,plain,
! [X69,X70,X71] :
( ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f163,plain,
! [X69,X70,X71] :
( ( subactivity_occurrence(X71,sK9_skl(X71,X70,X69))
& subactivity_occurrence(X70,sK9_skl(X71,X70,X69))
& occurrence_of(sK9_skl(X71,X70,X69),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X72,sK9_skl(X71,X70,X69))],[f162]) ).
fof(f164,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X0,X2)
| occurrence_of(sK9_skl(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X0,sK9_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X0,X2)
| subactivity_occurrence(X0,sK9_skl(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f171,plain,
! [X76,X77] :
( ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f172,plain,
! [X76,X77] :
( ( subactivity_occurrence(sK11_skl(X77,X76),X77)
& root(sK11_skl(X77,X76),X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X78,sK11_skl(X77,X76))],[f171]) ).
fof(f173,plain,
! [X0,X1] :
( root(sK11_skl(X1,X0),X0)
| ~ occurrence_of(X1,X0)
| atomic(X0) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
! [X0,X1] :
( subactivity_occurrence(sK11_skl(X0,X1),X0)
| atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f192,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(NNF_transformation,[status(thm)],[f34]) ).
fof(f193,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(miniscoping,[status(thm)],[f192]) ).
fof(f194,plain,
( ! [X99,X100] :
( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ! [X99,X100] :
( ( root(X99,sK13_skl(X100,X99))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK13_skl(X100,X99)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f193]) ).
fof(f198,plain,
! [X0,X1,X2] :
( root_occ(X0,X2)
| ~ subactivity_occurrence(X0,X2)
| ~ occurrence_of(X2,X1)
| ~ root(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f199,plain,
! [X102,X103] :
( ( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(NNF_transformation,[status(thm)],[f35]) ).
fof(f200,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
( ! [X102,X103] :
( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ! [X102,X103] :
( ( leaf(X102,sK14_skl(X103,X102))
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,sK14_skl(X103,X102)) )
| ~ leaf_occ(X102,X103) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f200]) ).
fof(f203,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f206,plain,
! [X105,X106,X107,X108] :
( X105 = X106
| ~ root_occ(X106,X107)
| ~ root_occ(X105,X107)
| ~ occurrence_of(X107,X108) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f207,plain,
! [X105,X106] :
( X105 = X106
| ! [X107] :
( ~ root_occ(X106,X107)
| ~ root_occ(X105,X107)
| ! [X108] : ~ occurrence_of(X107,X108) ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ~ root_occ(X3,X0)
| X3 = X2
| ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f218,plain,
! [X121,X122,X123,X124,X125] :
( X122 = X123
| ~ subactivity_occurrence(X122,X125)
| ~ subactivity_occurrence(X123,X125)
| ~ occurrence_of(X125,X124)
| ~ next_subocc(X121,X123,X124)
| ~ next_subocc(X121,X122,X124) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f219,plain,
! [X122,X123] :
( X122 = X123
| ! [X125] :
( ~ subactivity_occurrence(X122,X125)
| ~ subactivity_occurrence(X123,X125)
| ! [X124] :
( ~ occurrence_of(X125,X124)
| ! [X121] :
( ~ next_subocc(X121,X123,X124)
| ~ next_subocc(X121,X122,X124) ) ) ) ),
inference(miniscoping,[status(thm)],[f218]) ).
fof(f220,plain,
! [X0,X1,X2,X3,X4] :
( ~ next_subocc(X2,X4,X1)
| ~ subactivity_occurrence(X4,X0)
| ~ subactivity_occurrence(X3,X0)
| X3 = X4
| ~ next_subocc(X2,X3,X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f219]) ).
fof(f250,plain,
! [X161] :
( ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& occurrence_of(X163,tptp3)
& root_occ(X162,X161)
& occurrence_of(X162,tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f251,plain,
! [X161] :
( ( next_subocc(sK16_skl(X161),sK17_skl(X161),tptp0)
& leaf_occ(sK17_skl(X161),X161)
& occurrence_of(sK17_skl(X161),tptp3)
& root_occ(sK16_skl(X161),X161)
& occurrence_of(sK16_skl(X161),tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl]),skolemize(X162,sK16_skl(X161)),skolemize(X163,sK17_skl(X161))],[f250]) ).
fof(f253,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root_occ(sK16_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f254,plain,
! [X0] :
( occurrence_of(sK17_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f255,plain,
! [X0] :
( leaf_occ(sK17_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f256,plain,
! [X0] :
( next_subocc(sK16_skl(X0),sK17_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f258,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f266,plain,
tptp1 != tptp3,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f269,plain,
! [X164,X165] :
( ? [X166] :
( next_subocc(X164,X166,tptp0)
& occurrence_of(X166,tptp1) )
| ~ root_occ(X164,X165)
| ~ occurrence_of(X165,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f63]) ).
fof(f270,plain,
! [X164] :
( ? [X166] :
( next_subocc(X164,X166,tptp0)
& occurrence_of(X166,tptp1) )
| ! [X165] :
( ~ root_occ(X164,X165)
| ~ occurrence_of(X165,tptp0) ) ),
inference(miniscoping,[status(thm)],[f269]) ).
fof(f271,plain,
! [X164] :
( ( next_subocc(X164,sK18_skl(X164),tptp0)
& occurrence_of(sK18_skl(X164),tptp1) )
| ! [X165] :
( ~ root_occ(X164,X165)
| ~ occurrence_of(X165,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X166,sK18_skl(X164))],[f270]) ).
fof(f272,plain,
! [X0,X1] :
( occurrence_of(sK18_skl(X0),tptp1)
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f273,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK18_skl(X0),tptp0)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f274,plain,
occurrence_of(sK19_skl,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(X167,sK19_skl)],[f65]) ).
fof(f275,plain,
occurrence_of(sK19_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f290,plain,
( root(sK11_skl(sK19_skl,tptp0),tptp0)
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f173,f275]) ).
fof(f291,plain,
root(sK11_skl(sK19_skl,tptp0),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f290,f258]) ).
fof(f329,plain,
( subactivity_occurrence(sK11_skl(sK19_skl,tptp0),sK19_skl)
| atomic(tptp0) ),
inference(resolution,[status(thm)],[f174,f275]) ).
fof(f330,plain,
subactivity_occurrence(sK11_skl(sK19_skl,tptp0),sK19_skl),
inference(forward_subsumption_resolution,[status(thm)],[f329,f258]) ).
fof(f341,plain,
root_occ(sK16_skl(sK19_skl),sK19_skl),
inference(resolution,[status(thm)],[f253,f275]) ).
fof(f344,plain,
( ~ occurrence_of(sK19_skl,tptp0)
| next_subocc(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0) ),
inference(resolution,[status(thm)],[f341,f273]) ).
fof(f345,plain,
next_subocc(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0),
inference(forward_subsumption_resolution,[status(thm)],[f344,f275]) ).
fof(f364,plain,
min_precedes(sK16_skl(sK19_skl),sK18_skl(sK16_skl(sK19_skl)),tptp0),
inference(resolution,[status(thm)],[f345,f148]) ).
fof(f384,plain,
! [X0,X1] :
( ~ root_occ(X1,sK19_skl)
| sK16_skl(sK19_skl) = X1
| ~ occurrence_of(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f208,f341]) ).
fof(f490,plain,
subactivity_occurrence(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(resolution,[status(thm)],[f364,f165]) ).
fof(f493,plain,
subactivity_occurrence(sK18_skl(sK16_skl(sK19_skl)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(resolution,[status(thm)],[f364,f166]) ).
fof(f495,plain,
occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0),
inference(resolution,[status(thm)],[f364,f164]) ).
fof(f597,plain,
! [X0,X1] :
( ~ subactivity_occurrence(sK18_skl(sK16_skl(sK19_skl)),X0)
| ~ subactivity_occurrence(X1,X0)
| X1 = sK18_skl(sK16_skl(sK19_skl))
| ~ next_subocc(sK16_skl(sK19_skl),X1,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f220,f345]) ).
fof(f619,plain,
! [X0] :
( ~ subactivity_occurrence(sK11_skl(sK19_skl,tptp0),X0)
| root_occ(sK11_skl(sK19_skl,tptp0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f198,f291]) ).
fof(f667,plain,
( root_occ(sK11_skl(sK19_skl,tptp0),sK19_skl)
| ~ occurrence_of(sK19_skl,tptp0) ),
inference(resolution,[status(thm)],[f619,f330]) ).
fof(f669,plain,
root_occ(sK11_skl(sK19_skl,tptp0),sK19_skl),
inference(forward_subsumption_resolution,[status(thm)],[f667,f275]) ).
fof(f684,plain,
! [X0] :
( sK16_skl(sK19_skl) = sK11_skl(sK19_skl,tptp0)
| ~ occurrence_of(sK19_skl,X0) ),
inference(resolution,[status(thm)],[f669,f384]) ).
fof(f768,plain,
sK16_skl(sK19_skl) = sK11_skl(sK19_skl,tptp0),
inference(resolution,[status(thm)],[f684,f275]) ).
fof(f774,plain,
! [X0] :
( ~ subactivity_occurrence(sK16_skl(sK19_skl),X0)
| root_occ(sK11_skl(sK19_skl,tptp0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(backward_demodulation,[status(thm)],[f768,f619]) ).
fof(f822,plain,
! [X0] :
( root_occ(sK16_skl(sK19_skl),X0)
| ~ subactivity_occurrence(sK16_skl(sK19_skl),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_demodulation,[status(thm)],[f768,f774]) ).
fof(f828,plain,
( occurrence_of(sK18_skl(sK16_skl(sK19_skl)),tptp1)
| ~ occurrence_of(sK19_skl,tptp0) ),
inference(resolution,[status(thm)],[f272,f341]) ).
fof(f829,plain,
occurrence_of(sK18_skl(sK16_skl(sK19_skl)),tptp1),
inference(forward_subsumption_resolution,[status(thm)],[f828,f275]) ).
fof(f835,plain,
activity_occurrence(sK18_skl(sK16_skl(sK19_skl))),
inference(resolution,[status(thm)],[f829,f68]) ).
fof(f836,plain,
! [X0] :
( ~ occurrence_of(sK18_skl(sK16_skl(sK19_skl)),X0)
| X0 = tptp1 ),
inference(resolution,[status(thm)],[f829,f75]) ).
fof(f843,plain,
occurrence_of(sK18_skl(sK16_skl(sK19_skl)),sK0_skl(sK18_skl(sK16_skl(sK19_skl)))),
inference(resolution,[status(thm)],[f835,f72]) ).
fof(f985,plain,
tptp1 = sK0_skl(sK18_skl(sK16_skl(sK19_skl))),
inference(resolution,[status(thm)],[f843,f836]) ).
fof(f1032,plain,
next_subocc(sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0),
inference(resolution,[status(thm)],[f495,f256]) ).
fof(f1034,plain,
occurrence_of(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp3),
inference(resolution,[status(thm)],[f495,f254]) ).
fof(f1035,plain,
leaf_occ(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(resolution,[status(thm)],[f495,f255]) ).
fof(f1036,plain,
root_occ(sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(resolution,[status(thm)],[f495,f253]) ).
fof(f1589,plain,
( root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))
| ~ occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0) ),
inference(resolution,[status(thm)],[f490,f822]) ).
fof(f1597,plain,
root_occ(sK16_skl(sK19_skl),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f1589,f495]) ).
fof(f1896,plain,
activity_occurrence(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))),
inference(resolution,[status(thm)],[f1034,f68]) ).
fof(f1897,plain,
! [X0] :
( tptp3 = X0
| ~ occurrence_of(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),X0) ),
inference(resolution,[status(thm)],[f1034,f75]) ).
fof(f1900,plain,
occurrence_of(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK0_skl(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)))),
inference(resolution,[status(thm)],[f1896,f72]) ).
fof(f2062,plain,
! [X0,X1] :
( ~ root_occ(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))
| ~ occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),X1)
| sK16_skl(sK19_skl) = X0 ),
inference(resolution,[status(thm)],[f1597,f208]) ).
fof(f2173,plain,
! [X0] :
( ~ subactivity_occurrence(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))
| X0 = sK18_skl(sK16_skl(sK19_skl))
| ~ next_subocc(sK16_skl(sK19_skl),X0,tptp0)
| ~ occurrence_of(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0),tptp0) ),
inference(resolution,[status(thm)],[f493,f597]) ).
fof(f2180,plain,
! [X0] :
( sK18_skl(sK16_skl(sK19_skl)) = X0
| ~ next_subocc(sK16_skl(sK19_skl),X0,tptp0)
| ~ subactivity_occurrence(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2173,f495]) ).
fof(f6752,plain,
subactivity_occurrence(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(resolution,[status(thm)],[f1035,f203]) ).
fof(f10464,plain,
sK0_skl(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))) = tptp3,
inference(resolution,[status(thm)],[f1900,f1897]) ).
fof(f14601,plain,
! [X0] :
( sK16_skl(sK19_skl) = X0
| ~ root_occ(X0,sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)) ),
inference(resolution,[status(thm)],[f2062,f495]) ).
fof(f14602,plain,
sK16_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)) = sK16_skl(sK19_skl),
inference(resolution,[status(thm)],[f14601,f1036]) ).
fof(f14661,plain,
next_subocc(sK16_skl(sK19_skl),sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f14602,f1032]) ).
fof(f14767,plain,
( sK18_skl(sK16_skl(sK19_skl)) = sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0))
| ~ subactivity_occurrence(sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)) ),
inference(resolution,[status(thm)],[f14661,f2180]) ).
fof(f14778,plain,
sK18_skl(sK16_skl(sK19_skl)) = sK17_skl(sK9_skl(sK18_skl(sK16_skl(sK19_skl)),sK16_skl(sK19_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f14767,f6752]) ).
fof(f14827,plain,
sK0_skl(sK18_skl(sK16_skl(sK19_skl))) = tptp3,
inference(backward_demodulation,[status(thm)],[f14778,f10464]) ).
fof(f14878,plain,
tptp1 = tptp3,
inference(forward_demodulation,[status(thm)],[f985,f14827]) ).
fof(f14879,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f14878,f266]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO003+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/10.43 % Computer : n008.cluster.edu
% 0.14/10.43 % Model : x86_64 x86_64
% 0.14/10.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/10.43 % Memory : 8046.5625MB
% 0.14/10.43 % OS : Linux 6.8.0-71-generic
% 0.14/10.43 % CPULimit : 300
% 0.14/10.43 % WCLimit : 300
% 0.14/10.43 % DateTime : Mon Sep 21 03:41:37 UTC 2026
% 0.14/10.44 % CPUTime :
% 0.14/10.45 % Drodi V4.1.1
% 36.46/15.21 % Refutation found
% 36.46/15.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.46/15.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.08/15.32 % Elapsed time: 4.869459 seconds
% 2.08/15.32 % CPU time: 37.767172 seconds
% 2.08/15.32 % Total memory used: 264.951 MB
% 2.08/15.32 % Net memory used: 252.368 MB
%------------------------------------------------------------------------------