%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PRO003+2 : TPTP v9.3.1. Released v4.0.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 01:59:13 PM UTC 2026
% Result : Theorem 70.63s 9.42s
% Output : CNFRefutation 70.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 22
% Syntax : Number of formulae : 167 ( 44 unt; 0 def)
% Number of atoms : 541 ( 44 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 613 ( 239 ~; 260 |; 92 &)
% ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 320 ( 289 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X7,X8,X9,X10] :
( ( root_occ(X8,X9)
& root_occ(X7,X9)
& occurrence_of(X9,X10) )
=> X7 = X8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ~ ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X22,X23,X24] :
( min_precedes(X22,X23,X24)
=> precedes(X22,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X28,X29] :
( precedes(X28,X29)
<=> ( legal(X29)
& earlier(X28,X29) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X32,X33] :
( root_occ(X32,X33)
<=> ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X35,X36] :
( leaf_occ(X35,X36)
<=> ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X40,X41] :
( occurrence_of(X40,X41)
=> ( arboreal(X40)
<=> atomic(X41) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X42,X43] :
( leaf(X42,X43)
<=> ( ~ ? [X45] : min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [X51] :
( legal(X51)
=> arboreal(X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X52] :
( activity_occurrence(X52)
=> ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X54,X55] :
( subactivity_occurrence(X54,X55)
=> ( activity_occurrence(X55)
& activity_occurrence(X54) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X64,X65,X66] :
( ( occurrence_of(X64,X66)
& occurrence_of(X64,X65) )
=> X65 = X66 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X70,X71,X72] :
( min_precedes(X71,X72,X70)
=> ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X85,X86,X87,X88] :
( ( subactivity_occurrence(X88,X86)
& subactivity_occurrence(X87,X86)
& arboreal(X88)
& arboreal(X87)
& occurrence_of(X86,X85) )
=> ( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X89,X90] :
( occurrence_of(X90,X89)
=> ( activity_occurrence(X90)
& activity(X89) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X91,X92] :
( ( ~ atomic(X91)
& occurrence_of(X92,X91) )
=> ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X95] :
( occurrence_of(X95,tptp0)
=> ? [X96,X97] :
( next_subocc(X96,X97,tptp0)
& leaf_occ(X97,X95)
& occurrence_of(X97,tptp3)
& root_occ(X96,X95)
& occurrence_of(X96,tptp4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X98,X99] :
( ( root_occ(X98,X99)
& occurrence_of(X99,tptp0) )
=> ? [X100] :
( next_subocc(X98,X100,tptp0)
& occurrence_of(X100,tptp1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,conjecture,
~ ? [X101] : occurrence_of(X101,tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
~ ~ ? [X101] : occurrence_of(X101,tptp0),
inference(negated_conjecture,[status(cth)],[f47]) ).
fof(f55,plain,
! [X7,X8,X9,X10] :
( X7 = X8
| ~ root_occ(X8,X9)
| ~ root_occ(X7,X9)
| ~ occurrence_of(X9,X10) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f56,plain,
! [X7,X8] :
( X7 = X8
| ! [X9] :
( ~ root_occ(X8,X9)
| ~ root_occ(X7,X9)
| ! [X10] : ~ occurrence_of(X9,X10) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( ~ root_occ(X2,X1)
| ~ occurrence_of(X1,X3)
| X0 = X2
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f61,plain,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f62,plain,
! [X15,X16,X17] :
( ( ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(NNF_transformation,[status(thm)],[f61]) ).
fof(f63,plain,
( ! [X15,X16,X17] :
( ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ! [X15,X16,X17] :
( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(miniscoping,[status(thm)],[f62]) ).
fof(f64,plain,
( ! [X15,X16,X17] :
( ( min_precedes(sK0_skl(X17,X16,X15),X16,X17)
& min_precedes(X15,sK0_skl(X17,X16,X15),X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ! [X15,X16,X17] :
( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X18,sK0_skl(X17,X16,X15))],[f63]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ~ next_subocc(X3,X1,X2)
| ~ min_precedes(X3,X0,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f73,plain,
! [X22,X23,X24] :
( precedes(X22,X23)
| ~ min_precedes(X22,X23,X24) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f74,plain,
! [X22,X23] :
( precedes(X22,X23)
| ! [X24] : ~ min_precedes(X22,X23,X24) ),
inference(miniscoping,[status(thm)],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f79,plain,
! [X28,X29] :
( ( ~ legal(X29)
| ~ earlier(X28,X29)
| precedes(X28,X29) )
& ( ( legal(X29)
& earlier(X28,X29) )
| ~ precedes(X28,X29) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f80,plain,
( ! [X28,X29] :
( ~ legal(X29)
| ~ earlier(X28,X29)
| precedes(X28,X29) )
& ! [X28,X29] :
( ( legal(X29)
& earlier(X28,X29) )
| ~ precedes(X28,X29) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f82,plain,
! [X0,X1] :
( ~ precedes(X1,X0)
| legal(X0) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f86,plain,
! [X32,X33] :
( ( ! [X34] :
( ~ root(X32,X34)
| ~ subactivity_occurrence(X32,X33)
| ~ occurrence_of(X33,X34) )
| root_occ(X32,X33) )
& ( ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) )
| ~ root_occ(X32,X33) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f87,plain,
( ! [X32,X33] :
( ! [X34] :
( ~ root(X32,X34)
| ~ subactivity_occurrence(X32,X33)
| ~ occurrence_of(X33,X34) )
| root_occ(X32,X33) )
& ! [X32,X33] :
( ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) )
| ~ root_occ(X32,X33) ) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
( ! [X32,X33] :
( ! [X34] :
( ~ root(X32,X34)
| ~ subactivity_occurrence(X32,X33)
| ~ occurrence_of(X33,X34) )
| root_occ(X32,X33) )
& ! [X32,X33] :
( ( root(X32,sK1_skl(X33,X32))
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,sK1_skl(X33,X32)) )
| ~ root_occ(X32,X33) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(X34,sK1_skl(X33,X32))],[f87]) ).
fof(f92,plain,
! [X0,X1,X2] :
( ~ root(X2,X1)
| ~ subactivity_occurrence(X2,X0)
| root_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f93,plain,
! [X35,X36] :
( ( ! [X37] :
( ~ leaf(X35,X37)
| ~ subactivity_occurrence(X35,X36)
| ~ occurrence_of(X36,X37) )
| leaf_occ(X35,X36) )
& ( ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) )
| ~ leaf_occ(X35,X36) ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f94,plain,
( ! [X35,X36] :
( ! [X37] :
( ~ leaf(X35,X37)
| ~ subactivity_occurrence(X35,X36)
| ~ occurrence_of(X36,X37) )
| leaf_occ(X35,X36) )
& ! [X35,X36] :
( ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) )
| ~ leaf_occ(X35,X36) ) ),
inference(miniscoping,[status(thm)],[f93]) ).
fof(f95,plain,
( ! [X35,X36] :
( ! [X37] :
( ~ leaf(X35,X37)
| ~ subactivity_occurrence(X35,X36)
| ~ occurrence_of(X36,X37) )
| leaf_occ(X35,X36) )
& ! [X35,X36] :
( ( leaf(X35,sK2_skl(X36,X35))
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,sK2_skl(X36,X35)) )
| ~ leaf_occ(X35,X36) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X37,sK2_skl(X36,X35))],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( occurrence_of(X1,sK2_skl(X1,X0))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f98,plain,
! [X0,X1] :
( leaf(X0,sK2_skl(X1,X0))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f103,plain,
! [X40,X41] :
( ( arboreal(X40)
<=> atomic(X41) )
| ~ occurrence_of(X40,X41) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f104,plain,
! [X40,X41] :
( ( ( ~ atomic(X41)
| arboreal(X40) )
& ( atomic(X41)
| ~ arboreal(X40) ) )
| ~ occurrence_of(X40,X41) ),
inference(NNF_transformation,[status(thm)],[f103]) ).
fof(f106,plain,
! [X0,X1] :
( arboreal(X1)
| ~ occurrence_of(X1,X0)
| ~ atomic(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f107,plain,
! [X42,X43] :
( leaf(X42,X43)
<=> ( ! [X45] : ~ min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f108,plain,
! [X42,X43] :
( ( ? [X45] : min_precedes(X42,X45,X43)
| ( ! [X44] : ~ min_precedes(X44,X42,X43)
& ~ root(X42,X43) )
| leaf(X42,X43) )
& ( ( ! [X45] : ~ min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) )
| ~ leaf(X42,X43) ) ),
inference(NNF_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
( ! [X42,X43] :
( ? [X45] : min_precedes(X42,X45,X43)
| ( ! [X44] : ~ min_precedes(X44,X42,X43)
& ~ root(X42,X43) )
| leaf(X42,X43) )
& ! [X42,X43] :
( ( ! [X45] : ~ min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) )
| ~ leaf(X42,X43) ) ),
inference(miniscoping,[status(thm)],[f108]) ).
fof(f110,plain,
( ! [X42,X43] :
( min_precedes(X42,sK4_skl(X43,X42),X43)
| ( ! [X44] : ~ min_precedes(X44,X42,X43)
& ~ root(X42,X43) )
| leaf(X42,X43) )
& ! [X42,X43] :
( ( ! [X45] : ~ min_precedes(X42,X45,X43)
& ( min_precedes(sK3_skl(X43,X42),X42,X43)
| root(X42,X43) ) )
| ~ leaf(X42,X43) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(X44,sK3_skl(X43,X42)),skolemize(X45,sK4_skl(X43,X42))],[f109]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ leaf(X0,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f124,plain,
! [X51] :
( arboreal(X51)
| ~ legal(X51) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f125,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [X52] :
( ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) )
| ~ activity_occurrence(X52) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f127,plain,
! [X52] :
( ( occurrence_of(X52,sK6_skl(X52))
& activity(sK6_skl(X52)) )
| ~ activity_occurrence(X52) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(X53,sK6_skl(X52))],[f126]) ).
fof(f129,plain,
! [X0] :
( ~ activity_occurrence(X0)
| occurrence_of(X0,sK6_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f130,plain,
! [X54,X55] :
( ( activity_occurrence(X55)
& activity_occurrence(X54) )
| ~ subactivity_occurrence(X54,X55) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f132,plain,
! [X0,X1] :
( activity_occurrence(X1)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f139,plain,
! [X64,X65,X66] :
( X65 = X66
| ~ occurrence_of(X64,X66)
| ~ occurrence_of(X64,X65) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f140,plain,
! [X65,X66] :
( X65 = X66
| ! [X64] :
( ~ occurrence_of(X64,X66)
| ~ occurrence_of(X64,X65) ) ),
inference(miniscoping,[status(thm)],[f139]) ).
fof(f141,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f146,plain,
! [X70,X71,X72] :
( ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) )
| ~ min_precedes(X71,X72,X70) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f147,plain,
! [X70,X71,X72] :
( ( subactivity_occurrence(X72,sK8_skl(X72,X71,X70))
& subactivity_occurrence(X71,sK8_skl(X72,X71,X70))
& occurrence_of(sK8_skl(X72,X71,X70),X70) )
| ~ min_precedes(X71,X72,X70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(X73,sK8_skl(X72,X71,X70))],[f146]) ).
fof(f148,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X0,X2)
| occurrence_of(sK8_skl(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,sK8_skl(X1,X0,X2)) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f150,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X0,X2)
| subactivity_occurrence(X0,sK8_skl(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f166,plain,
! [X85,X86,X87,X88] :
( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85)
| ~ subactivity_occurrence(X88,X86)
| ~ subactivity_occurrence(X87,X86)
| ~ arboreal(X88)
| ~ arboreal(X87)
| ~ occurrence_of(X86,X85) ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f167,plain,
! [X85,X87,X88] :
( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85)
| ! [X86] :
( ~ subactivity_occurrence(X88,X86)
| ~ subactivity_occurrence(X87,X86)
| ~ arboreal(X88)
| ~ arboreal(X87)
| ~ occurrence_of(X86,X85) ) ),
inference(miniscoping,[status(thm)],[f166]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X0,X3)
| ~ occurrence_of(X1,X3)
| ~ arboreal(X2)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X0,X2,X3)
| X2 = X0
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [X89,X90] :
( ( activity_occurrence(X90)
& activity(X89) )
| ~ occurrence_of(X90,X89) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f171,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f172,plain,
! [X91,X92] :
( ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) )
| atomic(X91)
| ~ occurrence_of(X92,X91) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f173,plain,
! [X91,X92] :
( ( subactivity_occurrence(sK13_skl(X92,X91),X92)
& root(sK13_skl(X92,X91),X91) )
| atomic(X91)
| ~ occurrence_of(X92,X91) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X93,sK13_skl(X92,X91))],[f172]) ).
fof(f174,plain,
! [X0,X1] :
( atomic(X1)
| root(sK13_skl(X0,X1),X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f175,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| atomic(X1)
| subactivity_occurrence(sK13_skl(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f178,plain,
! [X95] :
( ? [X96,X97] :
( next_subocc(X96,X97,tptp0)
& leaf_occ(X97,X95)
& occurrence_of(X97,tptp3)
& root_occ(X96,X95)
& occurrence_of(X96,tptp4) )
| ~ occurrence_of(X95,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f179,plain,
! [X95] :
( ( next_subocc(sK14_skl(X95),sK15_skl(X95),tptp0)
& leaf_occ(sK15_skl(X95),X95)
& occurrence_of(sK15_skl(X95),tptp3)
& root_occ(sK14_skl(X95),X95)
& occurrence_of(sK14_skl(X95),tptp4) )
| ~ occurrence_of(X95,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl]),skolemize(X96,sK14_skl(X95)),skolemize(X97,sK15_skl(X95))],[f178]) ).
fof(f181,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root_occ(sK14_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f182,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK15_skl(X0),tptp3) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f183,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK15_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f184,plain,
! [X0] :
( next_subocc(sK14_skl(X0),sK15_skl(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f186,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f188,plain,
atomic(tptp3),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f194,plain,
tptp1 != tptp3,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f197,plain,
! [X98,X99] :
( ? [X100] :
( next_subocc(X98,X100,tptp0)
& occurrence_of(X100,tptp1) )
| ~ root_occ(X98,X99)
| ~ occurrence_of(X99,tptp0) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f198,plain,
! [X98] :
( ? [X100] :
( next_subocc(X98,X100,tptp0)
& occurrence_of(X100,tptp1) )
| ! [X99] :
( ~ root_occ(X98,X99)
| ~ occurrence_of(X99,tptp0) ) ),
inference(miniscoping,[status(thm)],[f197]) ).
fof(f199,plain,
! [X98] :
( ( next_subocc(X98,sK16_skl(X98),tptp0)
& occurrence_of(sK16_skl(X98),tptp1) )
| ! [X99] :
( ~ root_occ(X98,X99)
| ~ occurrence_of(X99,tptp0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(X100,sK16_skl(X98))],[f198]) ).
fof(f200,plain,
! [X0,X1] :
( ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16_skl(X0),tptp1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f201,plain,
! [X0,X1] :
( next_subocc(X0,sK16_skl(X0),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f202,plain,
occurrence_of(sK17_skl,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(X101,sK17_skl)],[f48]) ).
fof(f203,plain,
occurrence_of(sK17_skl,tptp0),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f209,plain,
! [X0,X1] :
( X1 = sK6_skl(X0)
| ~ occurrence_of(X0,X1)
| ~ activity_occurrence(X0) ),
inference(resolution,[status(thm)],[f129,f141]) ).
fof(f210,plain,
! [X0,X1] :
( sK6_skl(X0) = X1
| ~ occurrence_of(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f209,f171]) ).
fof(f219,plain,
! [X0] :
( subactivity_occurrence(sK15_skl(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f183,f97]) ).
fof(f225,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(X0,sK2_skl(X0,sK15_skl(X0))) ),
inference(resolution,[status(thm)],[f96,f183]) ).
fof(f226,plain,
! [X0] :
( leaf(sK15_skl(X0),sK2_skl(X0,sK15_skl(X0)))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f98,f183]) ).
fof(f227,plain,
root_occ(sK14_skl(sK17_skl),sK17_skl),
inference(resolution,[status(thm)],[f181,f203]) ).
fof(f230,plain,
( ~ occurrence_of(sK17_skl,tptp0)
| occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1) ),
inference(resolution,[status(thm)],[f227,f200]) ).
fof(f232,plain,
occurrence_of(sK16_skl(sK14_skl(sK17_skl)),tptp1),
inference(forward_subsumption_resolution,[status(thm)],[f230,f203]) ).
fof(f233,plain,
tptp1 = sK6_skl(sK16_skl(sK14_skl(sK17_skl))),
inference(resolution,[status(thm)],[f232,f210]) ).
fof(f313,plain,
! [X0,X1,X2,X3,X4] :
( min_precedes(X0,X2,X4)
| ~ atomic(X3)
| min_precedes(X2,X0,X4)
| ~ arboreal(X2)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X4)
| ~ occurrence_of(X0,X3)
| X0 = X2
| ~ subactivity_occurrence(X0,X1) ),
inference(resolution,[status(thm)],[f168,f106]) ).
fof(f320,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root(sK13_skl(X0,tptp0),tptp0) ),
inference(resolution,[status(thm)],[f174,f186]) ).
fof(f325,plain,
! [X0,X1] :
( ~ occurrence_of(sK17_skl,X1)
| X0 = sK14_skl(sK17_skl)
| ~ root_occ(X0,sK17_skl) ),
inference(resolution,[status(thm)],[f57,f227]) ).
fof(f344,plain,
root(sK13_skl(sK17_skl,tptp0),tptp0),
inference(resolution,[status(thm)],[f320,f203]) ).
fof(f345,plain,
! [X0] :
( ~ subactivity_occurrence(sK13_skl(sK17_skl,tptp0),X0)
| root_occ(sK13_skl(sK17_skl,tptp0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[status(thm)],[f344,f92]) ).
fof(f383,plain,
! [X0] :
( ~ root_occ(X0,sK17_skl)
| next_subocc(X0,sK16_skl(X0),tptp0) ),
inference(resolution,[status(thm)],[f201,f203]) ).
fof(f384,plain,
next_subocc(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0),
inference(resolution,[status(thm)],[f383,f227]) ).
fof(f419,plain,
min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0),
inference(resolution,[status(thm)],[f384,f65]) ).
fof(f506,plain,
occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0),
inference(resolution,[status(thm)],[f419,f148]) ).
fof(f508,plain,
precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl))),
inference(resolution,[status(thm)],[f419,f75]) ).
fof(f510,plain,
legal(sK16_skl(sK14_skl(sK17_skl))),
inference(resolution,[status(thm)],[f508,f82]) ).
fof(f513,plain,
arboreal(sK16_skl(sK14_skl(sK17_skl))),
inference(resolution,[status(thm)],[f510,f125]) ).
fof(f593,plain,
( ~ occurrence_of(sK17_skl,tptp0)
| atomic(tptp0)
| root_occ(sK13_skl(sK17_skl,tptp0),sK17_skl)
| ~ occurrence_of(sK17_skl,tptp0) ),
inference(resolution,[status(thm)],[f345,f175]) ).
fof(f595,plain,
! [X0,X1] :
( ~ min_precedes(sK13_skl(sK17_skl,tptp0),X0,X1)
| ~ occurrence_of(sK8_skl(X0,sK13_skl(sK17_skl,tptp0),X1),tptp0)
| root_occ(sK13_skl(sK17_skl,tptp0),sK8_skl(X0,sK13_skl(sK17_skl,tptp0),X1)) ),
inference(resolution,[status(thm)],[f345,f149]) ).
fof(f596,plain,
( atomic(tptp0)
| root_occ(sK13_skl(sK17_skl,tptp0),sK17_skl)
| ~ occurrence_of(sK17_skl,tptp0) ),
inference(duplicate_literals_removal,[status(thm)],[f593]) ).
fof(f597,plain,
( root_occ(sK13_skl(sK17_skl,tptp0),sK17_skl)
| atomic(tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f596,f203]) ).
fof(f598,plain,
root_occ(sK13_skl(sK17_skl,tptp0),sK17_skl),
inference(forward_subsumption_resolution,[status(thm)],[f597,f186]) ).
fof(f600,plain,
! [X0] :
( ~ occurrence_of(sK17_skl,X0)
| sK13_skl(sK17_skl,tptp0) = sK14_skl(sK17_skl) ),
inference(resolution,[status(thm)],[f598,f325]) ).
fof(f637,plain,
sK14_skl(sK17_skl) = sK13_skl(sK17_skl,tptp0),
inference(resolution,[status(thm)],[f600,f203]) ).
fof(f692,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X1,X0,X2)
| ~ occurrence_of(sK8_skl(X1,X4,X5),X2)
| X1 = X0
| ~ atomic(X3)
| ~ min_precedes(X4,X1,X5)
| ~ subactivity_occurrence(X0,sK8_skl(X1,X4,X5))
| ~ arboreal(X1)
| ~ occurrence_of(X0,X3)
| min_precedes(X0,X1,X2) ),
inference(resolution,[status(thm)],[f313,f150]) ).
fof(f785,plain,
leaf(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK2_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)))),
inference(resolution,[status(thm)],[f506,f226]) ).
fof(f788,plain,
occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),sK2_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)))),
inference(resolution,[status(thm)],[f506,f225]) ).
fof(f790,plain,
next_subocc(sK14_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0),
inference(resolution,[status(thm)],[f506,f184]) ).
fof(f792,plain,
occurrence_of(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp3),
inference(resolution,[status(thm)],[f506,f182]) ).
fof(f794,plain,
root_occ(sK14_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),
inference(resolution,[status(thm)],[f506,f181]) ).
fof(f797,plain,
tptp0 = sK6_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),
inference(resolution,[status(thm)],[f506,f210]) ).
fof(f798,plain,
! [X0] :
( ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),X0)
| X0 = tptp0 ),
inference(resolution,[status(thm)],[f506,f141]) ).
fof(f1210,plain,
! [X0,X1,X2,X3,X4] :
( ~ activity_occurrence(sK8_skl(X1,X2,X3))
| min_precedes(X1,X0,sK6_skl(sK8_skl(X1,X2,X3)))
| X1 = X0
| ~ atomic(X4)
| ~ min_precedes(X2,X1,X3)
| ~ subactivity_occurrence(X0,sK8_skl(X1,X2,X3))
| ~ arboreal(X1)
| ~ occurrence_of(X0,X4)
| min_precedes(X0,X1,sK6_skl(sK8_skl(X1,X2,X3))) ),
inference(resolution,[status(thm)],[f692,f129]) ).
fof(f1213,plain,
! [X0,X1,X2,X3,X4] :
( ~ occurrence_of(X0,X4)
| min_precedes(X1,X0,sK6_skl(sK8_skl(X1,X2,X3)))
| ~ atomic(X4)
| ~ arboreal(X1)
| ~ min_precedes(X2,X1,X3)
| ~ subactivity_occurrence(X0,sK8_skl(X1,X2,X3))
| X0 = X1
| min_precedes(X0,X1,sK6_skl(sK8_skl(X1,X2,X3))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1210,f132]) ).
fof(f1834,plain,
! [X0,X1,X2,X3] :
( ~ arboreal(X0)
| X0 = sK15_skl(sK8_skl(X0,X1,X2))
| min_precedes(sK15_skl(sK8_skl(X0,X1,X2)),X0,sK6_skl(sK8_skl(X0,X1,X2)))
| ~ atomic(X3)
| ~ min_precedes(X1,X0,X2)
| min_precedes(X0,sK15_skl(sK8_skl(X0,X1,X2)),sK6_skl(sK8_skl(X0,X1,X2)))
| ~ occurrence_of(sK15_skl(sK8_skl(X0,X1,X2)),X3)
| ~ occurrence_of(sK8_skl(X0,X1,X2),tptp0) ),
inference(resolution,[status(thm)],[f1213,f219]) ).
fof(f2111,plain,
! [X0,X1] :
( ~ min_precedes(sK13_skl(sK17_skl,tptp0),X0,X1)
| ~ occurrence_of(sK8_skl(X0,sK13_skl(sK17_skl,tptp0),X1),tptp0)
| root_occ(sK14_skl(sK17_skl),sK8_skl(X0,sK13_skl(sK17_skl,tptp0),X1)) ),
inference(forward_demodulation,[status(thm)],[f637,f595]) ).
fof(f2112,plain,
! [X0,X1] :
( ~ min_precedes(sK13_skl(sK17_skl,tptp0),X0,X1)
| ~ occurrence_of(sK8_skl(X0,sK13_skl(sK17_skl,tptp0),X1),tptp0)
| root_occ(sK14_skl(sK17_skl),sK8_skl(X0,sK14_skl(sK17_skl),X1)) ),
inference(forward_demodulation,[status(thm)],[f637,f2111]) ).
fof(f2113,plain,
! [X0,X1] :
( ~ min_precedes(sK13_skl(sK17_skl,tptp0),X0,X1)
| ~ occurrence_of(sK8_skl(X0,sK14_skl(sK17_skl),X1),tptp0)
| root_occ(sK14_skl(sK17_skl),sK8_skl(X0,sK14_skl(sK17_skl),X1)) ),
inference(forward_demodulation,[status(thm)],[f637,f2112]) ).
fof(f2114,plain,
! [X0,X1] :
( ~ occurrence_of(sK8_skl(X0,sK14_skl(sK17_skl),X1),tptp0)
| ~ min_precedes(sK14_skl(sK17_skl),X0,X1)
| root_occ(sK14_skl(sK17_skl),sK8_skl(X0,sK14_skl(sK17_skl),X1)) ),
inference(forward_demodulation,[status(thm)],[f637,f2113]) ).
fof(f2116,plain,
( ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| root_occ(sK14_skl(sK17_skl),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) ),
inference(resolution,[status(thm)],[f2114,f506]) ).
fof(f2119,plain,
root_occ(sK14_skl(sK17_skl),sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),
inference(forward_subsumption_resolution,[status(thm)],[f2116,f419]) ).
fof(f2122,plain,
! [X0,X1] :
( ~ root_occ(X1,sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))
| sK14_skl(sK17_skl) = X1
| ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),X0) ),
inference(resolution,[status(thm)],[f2119,f57]) ).
fof(f3577,plain,
( ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),sK6_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)))
| ~ atomic(tptp3)
| ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| min_precedes(sK16_skl(sK14_skl(sK17_skl)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK6_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)))
| ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0) ),
inference(resolution,[status(thm)],[f1834,f792]) ).
fof(f3594,plain,
( ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),sK6_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)))
| ~ atomic(tptp3)
| ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| min_precedes(sK16_skl(sK14_skl(sK17_skl)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0)
| ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0) ),
inference(forward_demodulation,[status(thm)],[f797,f3577]) ).
fof(f3595,plain,
( ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| ~ atomic(tptp3)
| ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| min_precedes(sK16_skl(sK14_skl(sK17_skl)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0)
| ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),tptp0) ),
inference(forward_demodulation,[status(thm)],[f797,f3594]) ).
fof(f3596,plain,
( sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) = sK16_skl(sK14_skl(sK17_skl))
| ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| ~ atomic(tptp3)
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| min_precedes(sK16_skl(sK14_skl(sK17_skl)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3595,f148]) ).
fof(f3933,plain,
min_precedes(sK14_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0),
inference(resolution,[status(thm)],[f790,f65]) ).
fof(f3984,plain,
sK2_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))) = tptp0,
inference(resolution,[status(thm)],[f788,f798]) ).
fof(f4747,plain,
leaf(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f3984,f785]) ).
fof(f4755,plain,
! [X0] : ~ min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),X0,tptp0),
inference(resolution,[status(thm)],[f4747,f112]) ).
fof(f7831,plain,
! [X0] :
( ~ occurrence_of(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0),X0)
| sK14_skl(sK17_skl) = sK14_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) ),
inference(resolution,[status(thm)],[f2122,f794]) ).
fof(f7838,plain,
sK14_skl(sK17_skl) = sK14_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),
inference(resolution,[status(thm)],[f7831,f506]) ).
fof(f7856,plain,
min_precedes(sK14_skl(sK17_skl),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f7838,f3933]) ).
fof(f7858,plain,
next_subocc(sK14_skl(sK17_skl),sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0),
inference(backward_demodulation,[status(thm)],[f7838,f790]) ).
fof(f7880,plain,
! [X0] :
( ~ min_precedes(X0,sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),tptp0)
| ~ min_precedes(sK14_skl(sK17_skl),X0,tptp0) ),
inference(resolution,[status(thm)],[f7858,f66]) ).
fof(f7925,plain,
occurrence_of(sK8_skl(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK14_skl(sK17_skl),tptp0),tptp0),
inference(resolution,[status(thm)],[f7856,f148]) ).
fof(f7964,plain,
occurrence_of(sK15_skl(sK8_skl(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK14_skl(sK17_skl),tptp0)),tptp3),
inference(resolution,[status(thm)],[f7925,f182]) ).
fof(f8007,plain,
sK6_skl(sK15_skl(sK8_skl(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK14_skl(sK17_skl),tptp0))) = tptp3,
inference(resolution,[status(thm)],[f7964,f210]) ).
fof(f9395,plain,
( ~ atomic(tptp3)
| ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| ~ min_precedes(sK14_skl(sK17_skl),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3596,f7880]) ).
fof(f9396,plain,
( ~ atomic(tptp3)
| ~ arboreal(sK16_skl(sK14_skl(sK17_skl)))
| min_precedes(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)),sK16_skl(sK14_skl(sK17_skl)),tptp0)
| sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) ),
inference(resolution,[status(thm)],[f9395,f419]) ).
fof(f9397,plain,
( sK16_skl(sK14_skl(sK17_skl)) = sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))
| ~ atomic(tptp3)
| ~ arboreal(sK16_skl(sK14_skl(sK17_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f9396,f4755]) ).
fof(f9398,plain,
( sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) = sK16_skl(sK14_skl(sK17_skl))
| ~ atomic(tptp3) ),
inference(forward_subsumption_resolution,[status(thm)],[f9397,f513]) ).
fof(f9399,plain,
sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0)) = sK16_skl(sK14_skl(sK17_skl)),
inference(resolution,[status(thm)],[f9398,f188]) ).
fof(f9438,plain,
sK6_skl(sK15_skl(sK8_skl(sK16_skl(sK14_skl(sK17_skl)),sK14_skl(sK17_skl),tptp0))) = tptp3,
inference(backward_demodulation,[status(thm)],[f9399,f8007]) ).
fof(f9552,plain,
sK6_skl(sK16_skl(sK14_skl(sK17_skl))) = tptp3,
inference(forward_demodulation,[status(thm)],[f9399,f9438]) ).
fof(f9553,plain,
tptp1 = tptp3,
inference(forward_demodulation,[status(thm)],[f233,f9552]) ).
fof(f9554,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f9553,f194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO003+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:40:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 70.63/9.42 % Refutation found
% 70.63/9.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 70.63/9.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.73/9.52 % Elapsed time: 9.139082 seconds
% 4.73/9.52 % CPU time: 71.948052 seconds
% 4.73/9.52 % Total memory used: 414.408 MB
% 4.73/9.52 % Net memory used: 389.285 MB
%------------------------------------------------------------------------------