%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO010+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:16 PM UTC 2026
% Result : Theorem 0.19s 0.54s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 24
% Syntax : Number of formulae : 122 ( 12 unt; 11 def)
% Number of atoms : 407 ( 8 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 436 ( 151 ~; 144 |; 111 &)
% ( 16 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 11 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-3 aty)
% Number of variables : 222 ( 178 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity_occurrence(X1)
& activity(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X23,X24,X25] :
( min_precedes(X24,X25,X23)
=> ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X28,X29] :
( root(X29,X28)
=> ? [X30] :
( atocc(X29,X30)
& subactivity(X30,X28) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X64,X65] :
( atocc(X64,X65)
<=> ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X68)
& activity_occurrence(X67) ) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,conjecture,
! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( ( activity_occurrence(X1)
& activity(X0) )
| ~ occurrence_of(X1,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f53,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f54,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f55,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))],[f54]) ).
fof(f57,plain,
! [X0] :
( occurrence_of(X0,sK0_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f58,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f59,plain,
! [X5,X6] :
( X5 = X6
| ! [X4] :
( ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f71,plain,
! [X16,X17] :
( ( arboreal(X16)
<=> atomic(X17) )
| ~ occurrence_of(X16,X17) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f72,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(NNF_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1] :
( atomic(X1)
| ~ arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
! [X0,X1] :
( ~ atomic(X1)
| arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f85,plain,
! [X23,X24,X25] :
( ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) )
| ~ min_precedes(X24,X25,X23) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f86,plain,
! [X23,X24,X25] :
( ? [X27] :
( atocc(X25,X27)
& ? [X26] :
( atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) ) )
| ~ min_precedes(X24,X25,X23) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f87,plain,
! [X23,X24,X25] :
( ( atocc(X25,sK1_skl(X25,X24,X23))
& atocc(X24,sK2_skl(X25,X24,X23))
& subactivity(sK1_skl(X25,X24,X23),X23)
& subactivity(sK2_skl(X25,X24,X23),X23) )
| ~ min_precedes(X24,X25,X23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(X27,sK1_skl(X25,X24,X23)),skolemize(X26,sK2_skl(X25,X24,X23))],[f86]) ).
fof(f90,plain,
! [X0,X1,X2] :
( atocc(X0,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f92,plain,
! [X28,X29] :
( ? [X30] :
( atocc(X29,X30)
& subactivity(X30,X28) )
| ~ root(X29,X28) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f93,plain,
! [X28,X29] :
( ( atocc(X29,sK3_skl(X29,X28))
& subactivity(sK3_skl(X29,X28),X28) )
| ~ root(X29,X28) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(X30,sK3_skl(X29,X28))],[f92]) ).
fof(f95,plain,
! [X0,X1] :
( atocc(X0,sK3_skl(X0,X1))
| ~ root(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f137,plain,
! [X64,X65] :
( ( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ( ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) )
| ~ atocc(X64,X65) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f138,plain,
( ! [X64,X65] :
( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ! [X64,X65] :
( ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) )
| ~ atocc(X64,X65) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
( ! [X64,X65] :
( ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) )
| atocc(X64,X65) )
& ! [X64,X65] :
( ( occurrence_of(X64,sK8_skl(X65,X64))
& atomic(sK8_skl(X65,X64))
& subactivity(X65,sK8_skl(X65,X64)) )
| ~ atocc(X64,X65) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X66,sK8_skl(X65,X64))],[f138]) ).
fof(f141,plain,
! [X0,X1] :
( atomic(sK8_skl(X1,X0))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f142,plain,
! [X0,X1] :
( occurrence_of(X0,sK8_skl(X1,X0))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f144,plain,
! [X67,X68] :
( ( activity_occurrence(X68)
& activity_occurrence(X67) )
| ~ subactivity_occurrence(X67,X68) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f145,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f177,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(f178,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)],[f177]) ).
fof(f179,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))],[f178]) ).
fof(f182,plain,
! [X0,X1] :
( root(X0,sK13_skl(X1,X0))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,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(f185,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)],[f184]) ).
fof(f186,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))],[f185]) ).
fof(f188,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f191,plain,
! [X105] :
( ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f192,plain,
! [X105] :
( ? [X108] :
( leaf_occ(X108,X105)
& ? [X107] :
( next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& ? [X106] :
( next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ) )
| ~ occurrence_of(X105,tptp0) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f193,plain,
! [X105] :
( ( leaf_occ(sK15_skl(X105),X105)
& next_subocc(sK16_skl(X105),sK15_skl(X105),tptp0)
& ( occurrence_of(sK15_skl(X105),tptp2)
| occurrence_of(sK15_skl(X105),tptp1) )
& next_subocc(sK17_skl(X105),sK16_skl(X105),tptp0)
& occurrence_of(sK16_skl(X105),tptp4)
& root_occ(sK17_skl(X105),X105)
& occurrence_of(sK17_skl(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X108,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X106,sK17_skl(X105))],[f192]) ).
fof(f195,plain,
! [X0] :
( root_occ(sK17_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f200,plain,
! [X0] :
( leaf_occ(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f202,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f213,plain,
? [X109] :
( ! [X110,X111] :
( ( ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) )
& occurrence_of(X111,tptp2) )
| ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ leaf_occ(X111,X109) )
& occurrence_of(X109,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f214,definition,
! [X110,X111] :
( sP0_prd(X111,X110)
<=> ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f215,plain,
? [X109] :
( ! [X110,X111] :
( ( ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) )
& occurrence_of(X111,tptp2) )
| sP0_prd(X111,X110)
| ~ leaf_occ(X111,X109) )
& occurrence_of(X109,tptp0) ),
inference(formula_renaming,[status(thm)],[f213,f214]) ).
fof(f216,plain,
( ! [X110,X111] :
( ( min_precedes(X110,sK19_skl(X111,X110),tptp0)
& occurrence_of(sK19_skl(X111,X110),tptp1)
& occurrence_of(X111,tptp2) )
| sP0_prd(X111,X110)
| ~ leaf_occ(X111,sK18_skl) )
& occurrence_of(sK18_skl,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl]),skolemize(X109,sK18_skl),skolemize(X113,sK19_skl(X111,X110))],[f215]) ).
fof(f217,plain,
occurrence_of(sK18_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f220,plain,
! [X0,X1] :
( min_precedes(X1,sK19_skl(X0,X1),tptp0)
| sP0_prd(X0,X1)
| ~ leaf_occ(X0,sK18_skl) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f221,plain,
! [X110,X111] :
( ( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110) )
& ( ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110) ) ),
inference(NNF_transformation,[status(thm)],[f214]) ).
fof(f222,plain,
( ! [X110,X111] :
( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110) )
& ! [X110,X111] :
( ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110) ) ),
inference(miniscoping,[status(thm)],[f221]) ).
fof(f223,plain,
( ! [X110,X111] :
( ! [X112] :
( ~ min_precedes(X110,X112,tptp0)
| ~ occurrence_of(X112,tptp2) )
| ~ occurrence_of(X111,tptp1)
| sP0_prd(X111,X110) )
& ! [X110,X111] :
( ( min_precedes(X110,sK20_skl(X111,X110),tptp0)
& occurrence_of(sK20_skl(X111,X110),tptp2)
& occurrence_of(X111,tptp1) )
| ~ sP0_prd(X111,X110) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(X112,sK20_skl(X111,X110))],[f222]) ).
fof(f226,plain,
! [X0,X1] :
( min_precedes(X1,sK20_skl(X0,X1),tptp0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f230,plain,
! [X0] :
( X0 = tptp0
| ~ occurrence_of(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f60,f217]) ).
fof(f279,plain,
activity_occurrence(sK18_skl),
inference(resolution,[status(thm)],[f53,f217]) ).
fof(f280,plain,
( sK0_skl(sK18_skl) = tptp0
| ~ activity_occurrence(sK18_skl) ),
inference(resolution,[status(thm)],[f57,f230]) ).
fof(f284,definition,
( sQ9_spl
<=> activity_occurrence(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( sQ9_spl
| ~ activity_occurrence(sK18_skl) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,definition,
( sQ10_spl
<=> sK0_skl(sK18_skl) = tptp0 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ10_spl
| sK0_skl(sK18_skl) = tptp0 ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f290,plain,
( sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f280,f284,f287]) ).
fof(f292,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f286,f279]) ).
fof(f293,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f292]) ).
fof(f294,plain,
( ~ sQ10_spl
| occurrence_of(sK18_skl,tptp0)
| ~ activity_occurrence(sK18_skl) ),
inference(paramodulation,[status(thm)],[f288,f57]) ).
fof(f296,definition,
( sQ11_spl
<=> occurrence_of(sK18_skl,tptp0) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f299,plain,
( ~ sQ10_spl
| sQ11_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f294,f284,f296,f287]) ).
fof(f307,plain,
( atomic(tptp0)
| ~ arboreal(sK18_skl) ),
inference(resolution,[status(thm)],[f73,f217]) ).
fof(f309,definition,
( sQ13_spl
<=> arboreal(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f311,plain,
( sQ13_spl
| ~ arboreal(sK18_skl) ),
inference(component_clause,[status(thm)],[f309]) ).
fof(f312,definition,
( sQ14_spl
<=> atomic(tptp0) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f313,plain,
( ~ sQ14_spl
| atomic(tptp0) ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f315,plain,
( sQ14_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f307,f309,f312]) ).
fof(f319,plain,
( ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f313,f202]) ).
fof(f320,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f319]) ).
fof(f324,plain,
! [X0,X1] :
( ~ atomic(sK8_skl(X1,X0))
| arboreal(X0)
| ~ atocc(X0,X1) ),
inference(resolution,[status(thm)],[f142,f74]) ).
fof(f330,plain,
! [X0,X1] :
( arboreal(X0)
| ~ atocc(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f324,f141]) ).
fof(f331,plain,
! [X0,X1] :
( ~ root(X0,X1)
| arboreal(X0) ),
inference(resolution,[status(thm)],[f330,f95]) ).
fof(f341,plain,
! [X0,X1] :
( arboreal(X0)
| ~ root_occ(X0,X1) ),
inference(resolution,[status(thm)],[f182,f331]) ).
fof(f344,plain,
! [X0,X1,X2] :
( arboreal(X0)
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[status(thm)],[f90,f330]) ).
fof(f357,plain,
! [X0] :
( arboreal(sK17_skl(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f195,f341]) ).
fof(f367,plain,
! [X0] :
( subactivity_occurrence(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f200,f188]) ).
fof(f386,plain,
! [X0] :
( activity_occurrence(sK15_skl(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f367,f145]) ).
fof(f387,plain,
activity_occurrence(sK15_skl(sK18_skl)),
inference(resolution,[status(thm)],[f386,f217]) ).
fof(f444,definition,
( sQ21_spl
<=> activity_occurrence(sK15_skl(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f446,plain,
( sQ21_spl
| ~ activity_occurrence(sK15_skl(sK18_skl)) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f460,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f387]) ).
fof(f461,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f460]) ).
fof(f480,definition,
! [X0] :
( sQ23_spl
<=> ~ leaf_occ(X0,sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f481,plain,
! [X0] :
( ~ sQ23_spl
| ~ leaf_occ(X0,sK18_skl) ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f483,definition,
! [X1] :
( sQ24_spl
<=> arboreal(X1) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0] :
( ~ sQ24_spl
| arboreal(X0) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f512,definition,
! [X0] :
( sQ29_spl
<=> ( ~ arboreal(sK17_skl(X0))
| ~ occurrence_of(X0,tptp0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f513,plain,
! [X0] :
( ~ sQ29_spl
| ~ arboreal(sK17_skl(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f516,definition,
! [X0] :
( sQ30_spl
<=> ~ occurrence_of(X0,tptp0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f517,plain,
! [X0] :
( ~ sQ30_spl
| ~ occurrence_of(X0,tptp0) ),
inference(component_clause,[status(thm)],[f516]) ).
fof(f523,plain,
! [X0] :
( ~ sQ29_spl
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f357]) ).
fof(f524,plain,
( ~ sQ30_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f217,f517]) ).
fof(f525,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f524]) ).
fof(f526,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f523]) ).
fof(f527,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f605,plain,
! [X0,X1] :
( arboreal(X1)
| ~ sP0_prd(X0,X1) ),
inference(resolution,[status(thm)],[f226,f344]) ).
fof(f723,plain,
( ~ sQ23_spl
| ~ occurrence_of(sK18_skl,tptp0) ),
inference(resolution,[status(thm)],[f481,f200]) ).
fof(f724,plain,
( ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f217]) ).
fof(f725,plain,
~ sQ23_spl,
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f819,plain,
! [X0,X1] :
( sP0_prd(X1,X0)
| ~ leaf_occ(X1,sK18_skl)
| arboreal(X0) ),
inference(resolution,[status(thm)],[f344,f220]) ).
fof(f824,plain,
! [X0,X1] :
( ~ leaf_occ(X1,sK18_skl)
| arboreal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f819,f605]) ).
fof(f856,plain,
! [X0] :
( ~ occurrence_of(sK18_skl,tptp0)
| arboreal(X0) ),
inference(resolution,[status(thm)],[f824,f200]) ).
fof(f857,plain,
( ~ sQ11_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f856,f483,f296]) ).
fof(f858,plain,
( sQ13_spl
| ~ sQ24_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f311,f484]) ).
fof(f859,plain,
( sQ13_spl
| ~ sQ24_spl ),
inference(contradiction_clause,[status(thm)],[f858]) ).
fof(f860,plain,
$false,
inference(sat_refutation,[status(thm)],[f290,f293,f299,f315,f320,f461,f525,f527,f725,f857,f859]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO010+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n009.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 03:42:12 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 0.19/0.54 % Refutation found
% 0.19/0.54 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/0.60 % Elapsed time: 0.121796 seconds
% 0.19/0.60 % CPU time: 0.226368 seconds
% 0.19/0.60 % Total memory used: 33.323 MB
% 0.19/0.60 % Net memory used: 33.199 MB
%------------------------------------------------------------------------------