%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO002+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:13 PM UTC 2026
% Result : Theorem 12.56s 2.03s
% Output : CNFRefutation 12.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 18
% Syntax : Number of formulae : 150 ( 36 unt; 0 def)
% Number of atoms : 433 ( 49 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 458 ( 175 ~; 171 |; 94 &)
% ( 4 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-5 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-3 aty)
% Number of variables : 313 ( 273 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( ~ atomic(X0)
& occurrence_of(X1,X0) )
=> ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X8,X9,X10,X11] :
( ( ~ min_precedes(X10,X11,X8)
& arboreal(X10)
& leaf_occ(X11,X9)
& subactivity_occurrence(X10,X9)
& occurrence_of(X9,X8) )
=> X11 = X10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X39,X40] :
( subactivity_occurrence(X39,X40)
=> ( activity_occurrence(X40)
& activity_occurrence(X39) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X43] :
( legal(X43)
=> arboreal(X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X53,X54] :
( root(X53,X54)
=> legal(X53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X109,X110,X111,X112,X113] :
( send_message(X109,X110,X111,X112,X113)
=> ( X109 != tptp2
& X109 != tptp3
& X109 != tptp4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X114,X115,X116,X117,X118,X119] :
( ( occurrence_of(X119,X114)
& send_message(X114,X115,X116,X117,X118) )
=> min_precedes(X117,X119,X118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [X120,X121,X122] :
( tptp1(X120,X121,X122)
=> ( root(X122,X121)
& ~ atomic(X121)
& ~ atomic(X120)
& activity(X120) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
! [X123,X124,X125,X126] :
( ( occurrence_of(X126,X123)
& tptp1(X123,X124,X125) )
=> ? [X127,X128,X129,X130] :
( root_occ(X130,X126)
& occurrence_of(X130,X127)
& send_message(X127,X128,X129,X125,X124) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,conjecture,
~ ? [X133,X134,X135] :
( occurrence_of(X135,X133)
& tptp1(X133,tptp0,X134) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ ~ ? [X133,X134,X135] :
( occurrence_of(X135,X133)
& tptp1(X133,tptp0,X134) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f55,plain,
! [X0,X1] :
( ( subactivity_occurrence(sK0_skl(X1,X0),X1)
& root(sK0_skl(X1,X0),X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X2,sK0_skl(X1,X0))],[f54]) ).
fof(f56,plain,
! [X0,X1] :
( root(sK0_skl(X0,X1),X1)
| atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1] :
( subactivity_occurrence(sK0_skl(X0,X1),X0)
| atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f61,plain,
! [X8,X9,X10,X11] :
( X11 = X10
| min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f62,plain,
! [X10,X11] :
( X11 = X10
| ! [X8] :
( min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ! [X9] :
( ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ) ) ),
inference(miniscoping,[status(thm)],[f61]) ).
fof(f63,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| min_precedes(X2,X3,X1)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X0)
| ~ subactivity_occurrence(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f74,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f75,plain,
! [X21,X22,X23] :
( ( subactivity_occurrence(X23,sK2_skl(X23,X22,X21))
& subactivity_occurrence(X22,sK2_skl(X23,X22,X21))
& occurrence_of(sK2_skl(X23,X22,X21),X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X24,sK2_skl(X23,X22,X21))],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( occurrence_of(sK2_skl(X1,X0,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X0,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f78,plain,
! [X0,X1,X2] :
( subactivity_occurrence(X1,sK2_skl(X1,X0,X2))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f83,plain,
! [X28,X29,X30] :
( X29 = X30
| ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f84,plain,
! [X29,X30] :
( X29 = X30
| ! [X28] :
( ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ) ),
inference(miniscoping,[status(thm)],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f92,plain,
! [X39,X40] :
( ( activity_occurrence(X40)
& activity_occurrence(X39) )
| ~ subactivity_occurrence(X39,X40) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f93,plain,
! [X0,X1] :
( activity_occurrence(X0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f95,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f96,plain,
! [X41] :
( ( occurrence_of(X41,sK4_skl(X41))
& activity(sK4_skl(X41)) )
| ~ activity_occurrence(X41) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X42,sK4_skl(X41))],[f95]) ).
fof(f98,plain,
! [X0] :
( occurrence_of(X0,sK4_skl(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f99,plain,
! [X43] :
( arboreal(X43)
| ~ legal(X43) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f100,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f120,plain,
! [X53,X54] :
( legal(X53)
| ~ root(X53,X54) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f121,plain,
! [X53] :
( legal(X53)
| ! [X54] : ~ root(X53,X54) ),
inference(miniscoping,[status(thm)],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
! [X55,X56] :
( ( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f124,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
( ! [X55,X56] :
( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ! [X55,X56] :
( ( leaf(X55,sK8_skl(X56,X55))
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,sK8_skl(X56,X55)) )
| ~ leaf_occ(X55,X56) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X57,sK8_skl(X56,X55))],[f124]) ).
fof(f127,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f130,plain,
! [X58,X59] :
( ( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f131,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f132,plain,
( ! [X58,X59] :
( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ! [X58,X59] :
( ( root(X58,sK9_skl(X59,X58))
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,sK9_skl(X59,X58)) )
| ~ root_occ(X58,X59) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X60,sK9_skl(X59,X58))],[f131]) ).
fof(f136,plain,
! [X0,X1,X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f159,plain,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f160,plain,
! [X78,X79,X80] :
( ( ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(NNF_transformation,[status(thm)],[f159]) ).
fof(f161,plain,
( ! [X78,X79,X80] :
( ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ! [X78,X79,X80] :
( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f162,plain,
( ! [X78,X79,X80] :
( ( min_precedes(sK11_skl(X80,X79,X78),X79,X80)
& min_precedes(X78,sK11_skl(X80,X79,X78),X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ! [X78,X79,X80] :
( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(X81,sK11_skl(X80,X79,X78))],[f161]) ).
fof(f164,plain,
! [X0,X1,X2,X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f173,plain,
! [X90,X91,X92,X93] :
( X90 = X91
| ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ~ occurrence_of(X92,X93) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f174,plain,
! [X90,X91] :
( X90 = X91
| ! [X92] :
( ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ! [X93] : ~ occurrence_of(X92,X93) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| ~ root_occ(X3,X0)
| ~ root_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f182,plain,
! [X101] :
( ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f183,plain,
! [X101] :
( ( next_subocc(sK12_skl(X101),sK13_skl(X101),tptp0)
& leaf_occ(sK13_skl(X101),X101)
& ( occurrence_of(sK13_skl(X101),tptp2)
| occurrence_of(sK13_skl(X101),tptp3) )
& root_occ(sK12_skl(X101),X101)
& occurrence_of(sK12_skl(X101),tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(X102,sK12_skl(X101)),skolemize(X103,sK13_skl(X101))],[f182]) ).
fof(f185,plain,
! [X0] :
( root_occ(sK12_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f186,plain,
! [X0] :
( occurrence_of(sK13_skl(X0),tptp2)
| occurrence_of(sK13_skl(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f187,plain,
! [X0] :
( leaf_occ(sK13_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f188,plain,
! [X0] :
( next_subocc(sK12_skl(X0),sK13_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f206,plain,
! [X109,X110,X111,X112,X113] :
( ( X109 != tptp2
& X109 != tptp3
& X109 != tptp4 )
| ~ send_message(X109,X110,X111,X112,X113) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f207,plain,
! [X109] :
( ( X109 != tptp2
& X109 != tptp3
& X109 != tptp4 )
| ! [X110,X111,X112,X113] : ~ send_message(X109,X110,X111,X112,X113) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f209,plain,
! [X0,X1,X2,X3,X4] :
( X0 != tptp3
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4] :
( X0 != tptp2
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f211,plain,
! [X114,X115,X116,X117,X118,X119] :
( min_precedes(X117,X119,X118)
| ~ occurrence_of(X119,X114)
| ~ send_message(X114,X115,X116,X117,X118) ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f212,plain,
! [X117,X118,X119] :
( min_precedes(X117,X119,X118)
| ! [X114] :
( ~ occurrence_of(X119,X114)
| ! [X115,X116] : ~ send_message(X114,X115,X116,X117,X118) ) ),
inference(miniscoping,[status(thm)],[f211]) ).
fof(f213,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X3,X5,X4)
| ~ occurrence_of(X5,X0)
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
! [X120,X121,X122] :
( ( root(X122,X121)
& ~ atomic(X121)
& ~ atomic(X120)
& activity(X120) )
| ~ tptp1(X120,X121,X122) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f216,plain,
! [X0,X1,X2] :
( ~ atomic(X0)
| ~ tptp1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f218,plain,
! [X0,X1,X2] :
( root(X2,X1)
| ~ tptp1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f214]) ).
fof(f219,plain,
! [X123,X124,X125,X126] :
( ? [X127,X128,X129,X130] :
( root_occ(X130,X126)
& occurrence_of(X130,X127)
& send_message(X127,X128,X129,X125,X124) )
| ~ occurrence_of(X126,X123)
| ~ tptp1(X123,X124,X125) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f220,plain,
! [X124,X125,X126] :
( ? [X130] :
( root_occ(X130,X126)
& ? [X127] :
( occurrence_of(X130,X127)
& ? [X128,X129] : send_message(X127,X128,X129,X125,X124) ) )
| ! [X123] :
( ~ occurrence_of(X126,X123)
| ~ tptp1(X123,X124,X125) ) ),
inference(miniscoping,[status(thm)],[f219]) ).
fof(f221,plain,
! [X124,X125,X126] :
( ( root_occ(sK14_skl(X126,X125,X124),X126)
& occurrence_of(sK14_skl(X126,X125,X124),sK15_skl(X126,X125,X124))
& send_message(sK15_skl(X126,X125,X124),sK16_skl(X126,X125,X124),sK17_skl(X126,X125,X124),X125,X124) )
| ! [X123] :
( ~ occurrence_of(X126,X123)
| ~ tptp1(X123,X124,X125) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(X130,sK14_skl(X126,X125,X124)),skolemize(X127,sK15_skl(X126,X125,X124)),skolemize(X128,sK16_skl(X126,X125,X124)),skolemize(X129,sK17_skl(X126,X125,X124))],[f220]) ).
fof(f222,plain,
! [X0,X1,X2,X3] :
( send_message(sK15_skl(X3,X2,X1),sK16_skl(X3,X2,X1),sK17_skl(X3,X2,X1),X2,X1)
| ~ occurrence_of(X3,X0)
| ~ tptp1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
! [X0,X1,X2,X3] :
( occurrence_of(sK14_skl(X3,X2,X1),sK15_skl(X3,X2,X1))
| ~ occurrence_of(X3,X0)
| ~ tptp1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f224,plain,
! [X0,X1,X2,X3] :
( root_occ(sK14_skl(X3,X2,X1),X3)
| ~ occurrence_of(X3,X0)
| ~ tptp1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f226,plain,
? [X133] :
( ? [X135] : occurrence_of(X135,X133)
& ? [X134] : tptp1(X133,tptp0,X134) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f227,plain,
( occurrence_of(sK20_skl,sK18_skl)
& tptp1(sK18_skl,tptp0,sK19_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl]),skolemize(X133,sK18_skl),skolemize(X134,sK19_skl),skolemize(X135,sK20_skl)],[f226]) ).
fof(f228,plain,
tptp1(sK18_skl,tptp0,sK19_skl),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
occurrence_of(sK20_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f230,plain,
~ atomic(sK18_skl),
inference(resolution,[status(thm)],[f216,f228]) ).
fof(f234,plain,
root(sK19_skl,tptp0),
inference(resolution,[status(thm)],[f218,f228]) ).
fof(f235,plain,
( root(sK0_skl(sK20_skl,sK18_skl),sK18_skl)
| atomic(sK18_skl) ),
inference(resolution,[status(thm)],[f56,f229]) ).
fof(f236,plain,
root(sK0_skl(sK20_skl,sK18_skl),sK18_skl),
inference(forward_subsumption_resolution,[status(thm)],[f235,f230]) ).
fof(f239,plain,
legal(sK0_skl(sK20_skl,sK18_skl)),
inference(resolution,[status(thm)],[f122,f236]) ).
fof(f243,plain,
( subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl)
| atomic(sK18_skl) ),
inference(resolution,[status(thm)],[f57,f229]) ).
fof(f244,plain,
subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl),
inference(forward_subsumption_resolution,[status(thm)],[f243,f230]) ).
fof(f247,plain,
arboreal(sK0_skl(sK20_skl,sK18_skl)),
inference(resolution,[status(thm)],[f239,f100]) ).
fof(f249,plain,
activity_occurrence(sK0_skl(sK20_skl,sK18_skl)),
inference(resolution,[status(thm)],[f244,f93]) ).
fof(f254,plain,
occurrence_of(sK0_skl(sK20_skl,sK18_skl),sK4_skl(sK0_skl(sK20_skl,sK18_skl))),
inference(resolution,[status(thm)],[f98,f249]) ).
fof(f273,plain,
! [X0] :
( sK4_skl(sK0_skl(sK20_skl,sK18_skl)) = X0
| ~ occurrence_of(sK0_skl(sK20_skl,sK18_skl),X0) ),
inference(resolution,[status(thm)],[f254,f85]) ).
fof(f369,plain,
! [X0,X1] :
( X0 = X1
| ~ root_occ(X1,sK20_skl)
| ~ root_occ(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f175,f229]) ).
fof(f384,plain,
! [X0] :
( ~ root(X0,sK18_skl)
| ~ subactivity_occurrence(X0,sK20_skl)
| root_occ(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f136,f229]) ).
fof(f385,plain,
( ~ subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK20_skl)
| root_occ(sK0_skl(sK20_skl,sK18_skl),sK20_skl) ),
inference(resolution,[status(thm)],[f384,f236]) ).
fof(f386,plain,
root_occ(sK0_skl(sK20_skl,sK18_skl),sK20_skl),
inference(forward_subsumption_resolution,[status(thm)],[f385,f244]) ).
fof(f387,plain,
! [X0] :
( sK0_skl(sK20_skl,sK18_skl) = X0
| ~ root_occ(X0,sK20_skl) ),
inference(resolution,[status(thm)],[f386,f369]) ).
fof(f453,plain,
! [X0] :
( root_occ(sK14_skl(X0,sK19_skl,tptp0),X0)
| ~ occurrence_of(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f224,f228]) ).
fof(f454,plain,
root_occ(sK14_skl(sK20_skl,sK19_skl,tptp0),sK20_skl),
inference(resolution,[status(thm)],[f453,f229]) ).
fof(f455,plain,
sK0_skl(sK20_skl,sK18_skl) = sK14_skl(sK20_skl,sK19_skl,tptp0),
inference(resolution,[status(thm)],[f454,f387]) ).
fof(f483,plain,
! [X0] :
( send_message(sK15_skl(X0,sK19_skl,tptp0),sK16_skl(X0,sK19_skl,tptp0),sK17_skl(X0,sK19_skl,tptp0),sK19_skl,tptp0)
| ~ occurrence_of(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f222,f228]) ).
fof(f484,plain,
! [X0] :
( occurrence_of(sK14_skl(X0,sK19_skl,tptp0),sK15_skl(X0,sK19_skl,tptp0))
| ~ occurrence_of(X0,sK18_skl) ),
inference(resolution,[status(thm)],[f223,f228]) ).
fof(f485,plain,
send_message(sK15_skl(sK20_skl,sK19_skl,tptp0),sK16_skl(sK20_skl,sK19_skl,tptp0),sK17_skl(sK20_skl,sK19_skl,tptp0),sK19_skl,tptp0),
inference(resolution,[status(thm)],[f483,f229]) ).
fof(f489,plain,
occurrence_of(sK14_skl(sK20_skl,sK19_skl,tptp0),sK15_skl(sK20_skl,sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f484,f229]) ).
fof(f490,plain,
occurrence_of(sK0_skl(sK20_skl,sK18_skl),sK15_skl(sK20_skl,sK19_skl,tptp0)),
inference(forward_demodulation,[status(thm)],[f455,f489]) ).
fof(f491,plain,
! [X0] :
( min_precedes(sK19_skl,X0,tptp0)
| ~ occurrence_of(X0,sK15_skl(sK20_skl,sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f485,f213]) ).
fof(f494,plain,
sK15_skl(sK20_skl,sK19_skl,tptp0) != tptp2,
inference(resolution,[status(thm)],[f485,f210]) ).
fof(f495,plain,
sK15_skl(sK20_skl,sK19_skl,tptp0) != tptp3,
inference(resolution,[status(thm)],[f485,f209]) ).
fof(f499,plain,
sK4_skl(sK0_skl(sK20_skl,sK18_skl)) = sK15_skl(sK20_skl,sK19_skl,tptp0),
inference(resolution,[status(thm)],[f490,f273]) ).
fof(f515,plain,
! [X0] :
( sK15_skl(sK20_skl,sK19_skl,tptp0) = X0
| ~ occurrence_of(sK0_skl(sK20_skl,sK18_skl),X0) ),
inference(resolution,[status(thm)],[f490,f85]) ).
fof(f529,plain,
min_precedes(sK19_skl,sK0_skl(sK20_skl,sK18_skl),tptp0),
inference(resolution,[status(thm)],[f491,f490]) ).
fof(f536,plain,
subactivity_occurrence(sK0_skl(sK20_skl,sK18_skl),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f529,f78]) ).
fof(f538,plain,
subactivity_occurrence(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f529,f77]) ).
fof(f539,plain,
occurrence_of(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0),tptp0),
inference(resolution,[status(thm)],[f529,f76]) ).
fof(f655,plain,
( occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp2)
| occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp3) ),
inference(resolution,[status(thm)],[f539,f186]) ).
fof(f656,plain,
next_subocc(sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0),
inference(resolution,[status(thm)],[f539,f188]) ).
fof(f658,plain,
leaf_occ(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f539,f187]) ).
fof(f659,plain,
root_occ(sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f539,f185]) ).
fof(f661,plain,
! [X0] :
( ~ root(X0,tptp0)
| ~ subactivity_occurrence(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))
| root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f539,f136]) ).
fof(f663,plain,
! [X0,X1] :
( X0 = X1
| ~ root_occ(X1,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))
| ~ root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f539,f175]) ).
fof(f669,plain,
! [X0,X1] :
( X1 = X0
| min_precedes(X0,X1,tptp0)
| ~ arboreal(X0)
| ~ leaf_occ(X1,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))
| ~ subactivity_occurrence(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f539,f63]) ).
fof(f1104,plain,
subactivity_occurrence(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(resolution,[status(thm)],[f658,f127]) ).
fof(f1202,plain,
activity_occurrence(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))),
inference(resolution,[status(thm)],[f1104,f93]) ).
fof(f1203,plain,
occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)))),
inference(resolution,[status(thm)],[f1202,f98]) ).
fof(f1353,plain,
! [X0] :
( sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) = X0
| ~ root_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f663,f659]) ).
fof(f1482,plain,
! [X0] :
( sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))) = X0
| ~ occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),X0) ),
inference(resolution,[status(thm)],[f1203,f85]) ).
fof(f2053,plain,
( ~ root(sK19_skl,tptp0)
| root_occ(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f661,f538]) ).
fof(f2057,plain,
root_occ(sK19_skl,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f2053,f234]) ).
fof(f2059,plain,
sK12_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) = sK19_skl,
inference(resolution,[status(thm)],[f2057,f1353]) ).
fof(f2073,plain,
next_subocc(sK19_skl,sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f2059,f656]) ).
fof(f2165,plain,
! [X0] :
( ~ min_precedes(X0,sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0)
| ~ min_precedes(sK19_skl,X0,tptp0) ),
inference(resolution,[status(thm)],[f2073,f164]) ).
fof(f2998,plain,
( sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))) = tptp3
| occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp2) ),
inference(resolution,[status(thm)],[f655,f1482]) ).
fof(f3301,plain,
( sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))) = tptp2
| sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))) = tptp3 ),
inference(resolution,[status(thm)],[f2998,f1482]) ).
fof(f3352,plain,
( sK4_skl(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0))) = tptp2
| occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp3) ),
inference(paramodulation,[status(thm)],[f3301,f1203]) ).
fof(f4132,plain,
! [X0] :
( X0 = sK0_skl(sK20_skl,sK18_skl)
| min_precedes(sK0_skl(sK20_skl,sK18_skl),X0,tptp0)
| ~ arboreal(sK0_skl(sK20_skl,sK18_skl))
| ~ leaf_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(resolution,[status(thm)],[f669,f536]) ).
fof(f4134,plain,
! [X0] :
( X0 = sK0_skl(sK20_skl,sK18_skl)
| min_precedes(sK0_skl(sK20_skl,sK18_skl),X0,tptp0)
| ~ leaf_occ(X0,sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4132,f247]) ).
fof(f4136,plain,
( sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) = sK0_skl(sK20_skl,sK18_skl)
| min_precedes(sK0_skl(sK20_skl,sK18_skl),sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp0) ),
inference(resolution,[status(thm)],[f4134,f658]) ).
fof(f6412,plain,
( ~ min_precedes(sK19_skl,sK0_skl(sK20_skl,sK18_skl),tptp0)
| sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) = sK0_skl(sK20_skl,sK18_skl) ),
inference(resolution,[status(thm)],[f4136,f2165]) ).
fof(f6426,plain,
sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)) = sK0_skl(sK20_skl,sK18_skl),
inference(forward_subsumption_resolution,[status(thm)],[f6412,f529]) ).
fof(f6480,plain,
( sK4_skl(sK0_skl(sK20_skl,sK18_skl)) = tptp2
| occurrence_of(sK13_skl(sK2_skl(sK0_skl(sK20_skl,sK18_skl),sK19_skl,tptp0)),tptp3) ),
inference(backward_demodulation,[status(thm)],[f6426,f3352]) ).
fof(f6613,plain,
( sK4_skl(sK0_skl(sK20_skl,sK18_skl)) = tptp2
| occurrence_of(sK0_skl(sK20_skl,sK18_skl),tptp3) ),
inference(forward_demodulation,[status(thm)],[f6426,f6480]) ).
fof(f6614,plain,
( sK15_skl(sK20_skl,sK19_skl,tptp0) = tptp2
| occurrence_of(sK0_skl(sK20_skl,sK18_skl),tptp3) ),
inference(forward_demodulation,[status(thm)],[f499,f6613]) ).
fof(f6615,plain,
occurrence_of(sK0_skl(sK20_skl,sK18_skl),tptp3),
inference(forward_subsumption_resolution,[status(thm)],[f6614,f494]) ).
fof(f6653,plain,
sK15_skl(sK20_skl,sK19_skl,tptp0) = tptp3,
inference(resolution,[status(thm)],[f6615,f515]) ).
fof(f6670,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6653,f495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO002+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.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:40:53 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 12.56/2.03 % Refutation found
% 12.56/2.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.56/2.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.56/2.09 % Elapsed time: 1.698780 seconds
% 12.56/2.09 % CPU time: 13.033565 seconds
% 12.56/2.09 % Total memory used: 219.021 MB
% 12.56/2.09 % Net memory used: 209.356 MB
%------------------------------------------------------------------------------