%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PRO016+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 : Fri Sep 25 02:31:23 PM UTC 2026
% Result : Theorem 104.41s 18.80s
% Output : Proof 104.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 30
% Syntax : Number of formulae : 320 ( 251 unt; 0 def)
% Number of atoms : 582 ( 247 equ)
% Maximal formula atoms : 16 ( 1 avg)
% Number of connectives : 453 ( 191 ~; 141 |; 99 &)
% ( 5 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 2 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-4 aty)
% Number of variables : 356 ( 13 sgn 146 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t47,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1462,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t47]) ).
fof(f4,axiom,
! [X8,X9] :
( earlier(X8,X9)
=> ~ earlier(X9,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(f4_nnf,plain,
! [X8,X9] :
( ~ earlier(X9,X8)
| ~ earlier(X8,X9) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X8,X9] :
( ~ earlier(X9,X8)
| ~ earlier(X8,X9) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c6,plain,
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t82,plain,
or(not(earlier(X1,X2)),not(earlier(X2,X1))) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t932,plain,
or(not(earlier(X1,X2)),not(earlier(X2,X1))) = true,
inference(orient,[status(thm)],[t82]) ).
fof(f10,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
fof(f10_nnf,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c13,plain,
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t76,plain,
ifeq(precedes(X1,X2),true,earlier(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t400,plain,
ifeq(precedes(X1,X2),true,earlier(X1,X2),true) = true,
inference(orient,[status(thm)],[t76]) ).
fof(f15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_15) ).
fof(f15_nnf,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c25,plain,
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t89,plain,
ifeq(min_precedes(X1,X2,X3),true,precedes(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t345,plain,
ifeq(min_precedes(X1,X2,X3),true,precedes(X1,X2),true) = true,
inference(orient,[status(thm)],[t89]) ).
fof(f22,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f22_nnf,plain,
! [X60,X61,X62] :
( ( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X60,X61,X62,X63] :
( ( ( min_precedes(sk7(X60,X61,X62),X61,X62)
& min_precedes(X60,sk7(X60,X61,X62),X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f22_nnf]) ).
cnf(c35,plain,
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t102,plain,
ifeq(next_subocc(X1,X2,X3),true,min_precedes(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t358,plain,
ifeq(next_subocc(X1,X2,X3),true,min_precedes(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t102]) ).
fof(f49,axiom,
! [X161,X162] :
( ( ~ leaf_occ(X161,X162)
& arboreal(X161)
& subactivity_occurrence(X161,X162)
& occurrence_of(X162,tptp0) )
=> ? [X163,X164,X165] :
( leaf_occ(X165,X162)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp2)
| occurrence_of(X165,tptp1) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f49_nnf,plain,
! [X161,X162] :
( ? [X163,X164,X165] :
( leaf_occ(X165,X162)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp2)
| occurrence_of(X165,tptp1) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X162,X161] :
( ( leaf_occ(sk18(X161,X162),X162)
& next_subocc(sk17(X161,X162),sk18(X161,X162),tptp0)
& ( occurrence_of(sk18(X161,X162),tptp2)
| occurrence_of(sk18(X161,X162),tptp1) )
& next_subocc(sk16(X161,X162),sk17(X161,X162),tptp0)
& occurrence_of(sk17(X161,X162),tptp4)
& next_subocc(X161,sk16(X161,X162),tptp0)
& occurrence_of(sk16(X161,X162),tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16,sk17,sk18])],[f49_nnf]) ).
cnf(c83,plain,
( next_subocc(X0,sk16(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t225,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(X2,sk16(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t312,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(X2,sk16(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t225]) ).
fof(f29,axiom,
! [X83,X84,X85,X86] :
( ( subactivity_occurrence(X84,X86)
& occurrence_of(X86,X85)
& min_precedes(X83,X84,X85) )
=> subactivity_occurrence(X83,X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(f29_nnf,plain,
! [X83,X84,X85,X86] :
( subactivity_occurrence(X83,X86)
| ~ subactivity_occurrence(X84,X86)
| ~ occurrence_of(X86,X85)
| ~ min_precedes(X83,X84,X85) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X83,X84,X85,X86] :
( subactivity_occurrence(X83,X86)
| ~ subactivity_occurrence(X84,X86)
| ~ occurrence_of(X86,X85)
| ~ min_precedes(X83,X84,X85) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c53,plain,
( subactivity_occurrence(X0,X3)
| ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(t199,plain,
ifeq(min_precedes(X1,X2,X3),true,ifeq(occurrence_of(X4,X3),true,ifeq(subactivity_occurrence(X2,X4),true,subactivity_occurrence(X1,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(t327,plain,
ifeq(min_precedes(X1,X2,X3),true,ifeq(occurrence_of(X4,X3),true,ifeq(subactivity_occurrence(X2,X4),true,subactivity_occurrence(X1,X4),true),true),true) = true,
inference(orient,[status(thm)],[t199]) ).
fof(f62,conjecture,
! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( ( occurrence_of(X169,tptp2)
=> ~ ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) ) )
& ( occurrence_of(X169,tptp1)
=> ~ ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) ) )
& leaf_occ(X169,X167)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp2)
| occurrence_of(X169,tptp1) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f62_neg,negated_conjecture,
~ ! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( ( occurrence_of(X169,tptp2)
=> ~ ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) ) )
& ( occurrence_of(X169,tptp1)
=> ~ ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) ) )
& leaf_occ(X169,X167)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp2)
| occurrence_of(X169,tptp1) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f62_nnf,plain,
? [X166,X167] :
( ! [X168,X169] :
( ( ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) )
& occurrence_of(X169,tptp2) )
| ( ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) )
& occurrence_of(X169,tptp1) )
| ~ leaf_occ(X169,X167)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp2)
& ~ occurrence_of(X169,tptp1) )
| ~ next_subocc(X166,X168,tptp0)
| ~ occurrence_of(X168,tptp3) )
& ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) ),
inference(nnf_transformation,[status(thm)],[f62_neg]) ).
fof(f62_sk,plain,
! [X168,X169] :
( ( ( min_precedes(X168,sk22(X168,X169),tptp0)
& occurrence_of(sk22(X168,X169),tptp1)
& occurrence_of(X169,tptp2) )
| ( min_precedes(X168,sk21(X168,X169),tptp0)
& occurrence_of(sk21(X168,X169),tptp2)
& occurrence_of(X169,tptp1) )
| ~ leaf_occ(X169,sk20)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp2)
& ~ occurrence_of(X169,tptp1) )
| ~ next_subocc(sk19,X168,tptp0)
| ~ occurrence_of(X168,tptp3) )
& ~ leaf_occ(sk19,sk20)
& arboreal(sk19)
& subactivity_occurrence(sk19,sk20)
& occurrence_of(sk20,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19,sk20,sk21,sk22])],[f62_nnf]) ).
cnf(c101,plain,
occurrence_of(sk20,tptp0),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(t23,plain,
occurrence_of(sk20,tptp0) = true,
inference(equality_encoding,[status(esa)],[c101]) ).
cnf(t836,plain,
occurrence_of(sk20,tptp0) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t845,plain,
true = ifeq(min_precedes(X1,X2,tptp0),true,ifeq(true,true,ifeq(subactivity_occurrence(X2,sk20),true,subactivity_occurrence(X1,sk20),true),true),true),
inference(cp,[status(thm)],[t327,t836]) ).
cnf(t35,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t35]) ).
cnf(t21631,plain,
true = ifeq(min_precedes(X1,X2,tptp0),true,ifeq(subactivity_occurrence(X2,sk20),true,subactivity_occurrence(X1,sk20),true),true),
inference(step,[status(thm)],[t845,t256]) ).
cnf(t14030,plain,
ifeq(min_precedes(X1,X2,tptp0),true,ifeq(subactivity_occurrence(X2,sk20),true,subactivity_occurrence(X1,sk20),true),true) = true,
inference(orient,[status(thm)],[t21631]) ).
cnf(c87,plain,
( next_subocc(sk17(X0,X1),sk18(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t233,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk17(X2,X1),sk18(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c87]) ).
cnf(t313,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk17(X2,X1),sk18(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t233]) ).
cnf(c104,plain,
~ leaf_occ(sk19,sk20),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(t22,plain,
leaf_occ(sk19,sk20) = false,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(t1480,plain,
leaf_occ(sk19,sk20) = false,
inference(orient,[status(thm)],[t22]) ).
cnf(t1490,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),true),true),
inference(cp,[status(thm)],[t313,t1480]) ).
cnf(t20070,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),true),true),
inference(step,[status(thm)],[t1490,t836]) ).
cnf(t20071,plain,
true = ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t20070,t256]) ).
cnf(c102,plain,
subactivity_occurrence(sk19,sk20),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(t29,plain,
subactivity_occurrence(sk19,sk20) = true,
inference(equality_encoding,[status(esa)],[c102]) ).
cnf(t1199,plain,
subactivity_occurrence(sk19,sk20) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t20072,plain,
true = ifeq(true,true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t20071,t1199]) ).
cnf(t20073,plain,
true = ifeq(arboreal(sk19),true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t20072,t256]) ).
cnf(c103,plain,
arboreal(sk19),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(t3,plain,
arboreal(sk19) = true,
inference(equality_encoding,[status(esa)],[c103]) ).
cnf(t1406,plain,
arboreal(sk19) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t20074,plain,
true = ifeq(true,true,or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t20073,t1406]) ).
cnf(t20075,plain,
true = or(false,next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t20074,t256]) ).
cnf(t26,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t267,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t26]) ).
cnf(t20076,plain,
true = next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0),
inference(step,[status(thm)],[t20075,t267]) ).
cnf(t2511,plain,
next_subocc(sk17(sk19,sk20),sk18(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t20076]) ).
cnf(t2513,plain,
true = ifeq(true,true,min_precedes(sk17(sk19,sk20),sk18(sk19,sk20),tptp0),true),
inference(cp,[status(thm)],[t358,t2511]) ).
cnf(t20134,plain,
true = min_precedes(sk17(sk19,sk20),sk18(sk19,sk20),tptp0),
inference(step,[status(thm)],[t2513,t256]) ).
cnf(t2988,plain,
min_precedes(sk17(sk19,sk20),sk18(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t20134]) ).
cnf(t14049,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk18(sk19,sk20),sk20),true,subactivity_occurrence(sk17(sk19,sk20),sk20),true),true),
inference(cp,[status(thm)],[t14030,t2988]) ).
cnf(t21632,plain,
true = ifeq(subactivity_occurrence(sk18(sk19,sk20),sk20),true,subactivity_occurrence(sk17(sk19,sk20),sk20),true),
inference(step,[status(thm)],[t14049,t256]) ).
fof(f34,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',sos_34) ).
fof(f34_nnf,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)],[f34]) ).
fof(f34_sk,plain,
! [X102,X103,X104] :
( ( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104)
| leaf_occ(X102,X103) )
& ( ( leaf(X102,sk14(X102,X103))
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,sk14(X102,X103)) )
| ~ leaf_occ(X102,X103) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f34_nnf]) ).
cnf(c63,plain,
( subactivity_occurrence(X0,X1)
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t72,plain,
ifeq(leaf_occ(X1,X2),true,subactivity_occurrence(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(t349,plain,
ifeq(leaf_occ(X1,X2),true,subactivity_occurrence(X1,X2),true) = true,
inference(orient,[status(thm)],[t72]) ).
cnf(c88,plain,
( leaf_occ(sk18(X0,X1),X1)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t219,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),leaf_occ(sk18(X2,X1),X1)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
cnf(t311,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),leaf_occ(sk18(X2,X1),X1)),true),true),true) = true,
inference(orient,[status(thm)],[t219]) ).
cnf(t1492,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),true),true),
inference(cp,[status(thm)],[t311,t1480]) ).
cnf(t19932,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),true),true),
inference(step,[status(thm)],[t1492,t836]) ).
cnf(t19933,plain,
true = ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),true),
inference(step,[status(thm)],[t19932,t256]) ).
cnf(t19934,plain,
true = ifeq(true,true,ifeq(arboreal(sk19),true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),true),
inference(step,[status(thm)],[t19933,t1199]) ).
cnf(t19935,plain,
true = ifeq(arboreal(sk19),true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),
inference(step,[status(thm)],[t19934,t256]) ).
cnf(t19936,plain,
true = ifeq(true,true,or(false,leaf_occ(sk18(sk19,sk20),sk20)),true),
inference(step,[status(thm)],[t19935,t1406]) ).
cnf(t19937,plain,
true = or(false,leaf_occ(sk18(sk19,sk20),sk20)),
inference(step,[status(thm)],[t19936,t256]) ).
cnf(t19938,plain,
true = leaf_occ(sk18(sk19,sk20),sk20),
inference(step,[status(thm)],[t19937,t267]) ).
cnf(t1653,plain,
leaf_occ(sk18(sk19,sk20),sk20) = true,
inference(orient,[status(thm)],[t19938]) ).
cnf(t1654,plain,
true = ifeq(true,true,subactivity_occurrence(sk18(sk19,sk20),sk20),true),
inference(cp,[status(thm)],[t349,t1653]) ).
cnf(t19966,plain,
true = subactivity_occurrence(sk18(sk19,sk20),sk20),
inference(step,[status(thm)],[t1654,t256]) ).
cnf(t1832,plain,
subactivity_occurrence(sk18(sk19,sk20),sk20) = true,
inference(orient,[status(thm)],[t19966]) ).
cnf(t21633,plain,
true = ifeq(true,true,subactivity_occurrence(sk17(sk19,sk20),sk20),true),
inference(step,[status(thm)],[t21632,t1832]) ).
cnf(t21634,plain,
true = subactivity_occurrence(sk17(sk19,sk20),sk20),
inference(step,[status(thm)],[t21633,t256]) ).
cnf(t14058,plain,
subactivity_occurrence(sk17(sk19,sk20),sk20) = true,
inference(orient,[status(thm)],[t21634]) ).
cnf(t14070,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),true),true),true),
inference(cp,[status(thm)],[t312,t14058]) ).
cnf(t21727,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),true),true),true),
inference(step,[status(thm)],[t14070,t836]) ).
cnf(t21728,plain,
true = ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),true),true),
inference(step,[status(thm)],[t21727,t256]) ).
cnf(t21729,plain,
true = ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),true),
inference(step,[status(thm)],[t21728,t256]) ).
fof(f7,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f7_nnf,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c10,plain,
( ~ atomic(X1)
| arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t130,plain,
ifeq(occurrence_of(X1,X2),true,ifeq(atomic(X2),true,arboreal(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t274,plain,
ifeq(occurrence_of(X1,X2),true,ifeq(atomic(X2),true,arboreal(X1),true),true) = true,
inference(orient,[status(thm)],[t130]) ).
cnf(c84,plain,
( occurrence_of(sk17(X0,X1),tptp4)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t221,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),occurrence_of(sk17(X2,X1),tptp4)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(t308,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),occurrence_of(sk17(X2,X1),tptp4)),true),true),true) = true,
inference(orient,[status(thm)],[t221]) ).
cnf(t1494,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),true),true),
inference(cp,[status(thm)],[t308,t1480]) ).
cnf(t19952,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),true),true),
inference(step,[status(thm)],[t1494,t836]) ).
cnf(t19953,plain,
true = ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),true),
inference(step,[status(thm)],[t19952,t256]) ).
cnf(t19954,plain,
true = ifeq(true,true,ifeq(arboreal(sk19),true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),true),
inference(step,[status(thm)],[t19953,t1199]) ).
cnf(t19955,plain,
true = ifeq(arboreal(sk19),true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),
inference(step,[status(thm)],[t19954,t256]) ).
cnf(t19956,plain,
true = ifeq(true,true,or(false,occurrence_of(sk17(sk19,sk20),tptp4)),true),
inference(step,[status(thm)],[t19955,t1406]) ).
cnf(t19957,plain,
true = or(false,occurrence_of(sk17(sk19,sk20),tptp4)),
inference(step,[status(thm)],[t19956,t256]) ).
cnf(t19958,plain,
true = occurrence_of(sk17(sk19,sk20),tptp4),
inference(step,[status(thm)],[t19957,t267]) ).
cnf(t1759,plain,
occurrence_of(sk17(sk19,sk20),tptp4) = true,
inference(orient,[status(thm)],[t19958]) ).
cnf(t1765,plain,
true = ifeq(true,true,ifeq(atomic(tptp4),true,arboreal(sk17(sk19,sk20)),true),true),
inference(cp,[status(thm)],[t274,t1759]) ).
cnf(t19962,plain,
true = ifeq(atomic(tptp4),true,arboreal(sk17(sk19,sk20)),true),
inference(step,[status(thm)],[t1765,t256]) ).
fof(f52,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_52) ).
fof(f52_nnf,plain,
atomic(tptp4),
inference(nnf_transformation,[status(thm)],[f52]) ).
cnf(c91,plain,
atomic(tptp4),
inference(cnf_transformation,[status(esa)],[f52_nnf]) ).
cnf(t8,plain,
atomic(tptp4) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t1185,plain,
atomic(tptp4) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t19963,plain,
true = ifeq(true,true,arboreal(sk17(sk19,sk20)),true),
inference(step,[status(thm)],[t19962,t1185]) ).
cnf(t19964,plain,
true = arboreal(sk17(sk19,sk20)),
inference(step,[status(thm)],[t19963,t256]) ).
cnf(t1803,plain,
arboreal(sk17(sk19,sk20)) = true,
inference(orient,[status(thm)],[t19964]) ).
cnf(t21730,plain,
true = ifeq(true,true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),true),
inference(step,[status(thm)],[t21729,t1803]) ).
cnf(t21731,plain,
true = or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),
inference(step,[status(thm)],[t21730,t256]) ).
fof(f37,axiom,
! [X113,X114,X115] :
( ( leaf_occ(X114,X113)
& occurrence_of(X113,X115) )
=> ~ ? [X116] : min_precedes(X114,X116,X115) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f37_nnf,plain,
! [X113,X114,X115] :
( ! [X116] : ~ min_precedes(X114,X116,X115)
| ~ leaf_occ(X114,X113)
| ~ occurrence_of(X113,X115) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X113,X115,X114,X116] :
( ~ min_precedes(X114,X116,X115)
| ~ leaf_occ(X114,X113)
| ~ occurrence_of(X113,X115) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c68,plain,
( ~ min_precedes(X1,X3,X2)
| ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(t154,plain,
or(not(occurrence_of(X1,X2)),or(not(leaf_occ(X3,X1)),not(min_precedes(X3,X4,X2)))) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(t897,plain,
or(not(occurrence_of(X1,X2)),or(not(leaf_occ(X3,X1)),not(min_precedes(X3,X4,X2)))) = true,
inference(orient,[status(thm)],[t154]) ).
cnf(t3005,plain,
true = or(not(occurrence_of(X1,tptp0)),or(not(leaf_occ(sk17(sk19,sk20),X1)),not(true))),
inference(cp,[status(thm)],[t897,t2988]) ).
cnf(t10,plain,
not(true) = false,
introduced(definition) ).
cnf(t1517,plain,
not(true) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t20546,plain,
true = or(not(occurrence_of(X1,tptp0)),or(not(leaf_occ(sk17(sk19,sk20),X1)),false)),
inference(step,[status(thm)],[t3005,t1517]) ).
cnf(t24,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t266,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t20547,plain,
true = or(not(occurrence_of(X1,tptp0)),not(leaf_occ(sk17(sk19,sk20),X1))),
inference(step,[status(thm)],[t20546,t266]) ).
cnf(t5664,plain,
or(not(occurrence_of(X1,tptp0)),not(leaf_occ(sk17(sk19,sk20),X1))) = true,
inference(orient,[status(thm)],[t20547]) ).
cnf(t5671,plain,
true = or(not(true),not(leaf_occ(sk17(sk19,sk20),sk20))),
inference(cp,[status(thm)],[t5664,t836]) ).
cnf(t20548,plain,
true = or(false,not(leaf_occ(sk17(sk19,sk20),sk20))),
inference(step,[status(thm)],[t5671,t1517]) ).
cnf(t20549,plain,
true = not(leaf_occ(sk17(sk19,sk20),sk20)),
inference(step,[status(thm)],[t20548,t267]) ).
cnf(t5672,plain,
not(leaf_occ(sk17(sk19,sk20),sk20)) = true,
inference(orient,[status(thm)],[t20549]) ).
cnf(t5673,plain,
false = ifeq(true,true,leaf_occ(sk17(sk19,sk20),sk20),false),
inference(cp,[status(thm)],[t1462,t5672]) ).
cnf(t20550,plain,
false = leaf_occ(sk17(sk19,sk20),sk20),
inference(step,[status(thm)],[t5673,t256]) ).
cnf(t5674,plain,
leaf_occ(sk17(sk19,sk20),sk20) = false,
inference(orient,[status(thm)],[t20550]) ).
cnf(t21732,plain,
true = or(false,next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0)),
inference(step,[status(thm)],[t21731,t5674]) ).
cnf(t21733,plain,
true = next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0),
inference(step,[status(thm)],[t21732,t267]) ).
cnf(t14874,plain,
next_subocc(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0) = true,
inference(orient,[status(thm)],[t21733]) ).
cnf(t14875,plain,
true = ifeq(true,true,min_precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0),true),
inference(cp,[status(thm)],[t358,t14874]) ).
cnf(t21813,plain,
true = min_precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0),
inference(step,[status(thm)],[t14875,t256]) ).
cnf(t15560,plain,
min_precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20),tptp0) = true,
inference(orient,[status(thm)],[t21813]) ).
cnf(t15561,plain,
true = ifeq(true,true,precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)),true),
inference(cp,[status(thm)],[t345,t15560]) ).
cnf(t21820,plain,
true = precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)),
inference(step,[status(thm)],[t15561,t256]) ).
cnf(t15649,plain,
precedes(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)) = true,
inference(orient,[status(thm)],[t21820]) ).
cnf(t15651,plain,
true = ifeq(true,true,earlier(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)),true),
inference(cp,[status(thm)],[t400,t15649]) ).
cnf(t21822,plain,
true = earlier(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)),
inference(step,[status(thm)],[t15651,t256]) ).
cnf(t15678,plain,
earlier(sk17(sk19,sk20),sk16(sk17(sk19,sk20),sk20)) = true,
inference(orient,[status(thm)],[t21822]) ).
cnf(t15682,plain,
true = or(not(true),not(earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20)))),
inference(cp,[status(thm)],[t932,t15678]) ).
cnf(t21876,plain,
true = or(false,not(earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20)))),
inference(step,[status(thm)],[t15682,t1517]) ).
cnf(t21877,plain,
true = not(earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20))),
inference(step,[status(thm)],[t21876,t267]) ).
cnf(t16130,plain,
not(earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20))) = true,
inference(orient,[status(thm)],[t21877]) ).
cnf(t16131,plain,
false = ifeq(true,true,earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20)),false),
inference(cp,[status(thm)],[t1462,t16130]) ).
cnf(t21878,plain,
false = earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20)),
inference(step,[status(thm)],[t16131,t256]) ).
cnf(t16132,plain,
earlier(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20)) = false,
inference(orient,[status(thm)],[t21878]) ).
fof(f40,axiom,
! [X126,X127,X128,X129] :
( ( next_subocc(X128,X126,X129)
& next_subocc(X127,X126,X129) )
=> X127 = X128 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(f40_nnf,plain,
! [X126,X127,X128,X129] :
( X127 = X128
| ~ next_subocc(X128,X126,X129)
| ~ next_subocc(X127,X126,X129) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X127,X126,X129,X128] :
( X127 = X128
| ~ next_subocc(X128,X126,X129)
| ~ next_subocc(X127,X126,X129) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c71,plain,
( X1 = X2
| ~ next_subocc(X2,X0,X3)
| ~ next_subocc(X1,X0,X3) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(t152,plain,
ifeq(next_subocc(X1,X2,X3),true,ifeq(next_subocc(X4,X2,X3),true,X1,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c71]) ).
cnf(t262,plain,
ifeq(next_subocc(X1,X2,X3),true,ifeq(next_subocc(X4,X2,X3),true,X1,X4),X4) = X4,
inference(orient,[status(thm)],[t152]) ).
cnf(c85,plain,
( next_subocc(sk16(X0,X1),sk17(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(t232,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk16(X2,X1),sk17(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c85]) ).
cnf(t314,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk16(X2,X1),sk17(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t232]) ).
cnf(t1489,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),true),true),
inference(cp,[status(thm)],[t314,t1480]) ).
cnf(t20063,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),true),true),
inference(step,[status(thm)],[t1489,t836]) ).
cnf(t20064,plain,
true = ifeq(subactivity_occurrence(sk19,sk20),true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t20063,t256]) ).
cnf(t20065,plain,
true = ifeq(true,true,ifeq(arboreal(sk19),true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t20064,t1199]) ).
cnf(t20066,plain,
true = ifeq(arboreal(sk19),true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t20065,t256]) ).
cnf(t20067,plain,
true = ifeq(true,true,or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t20066,t1406]) ).
cnf(t20068,plain,
true = or(false,next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t20067,t256]) ).
cnf(t20069,plain,
true = next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0),
inference(step,[status(thm)],[t20068,t267]) ).
cnf(t2501,plain,
next_subocc(sk16(sk19,sk20),sk17(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t20069]) ).
cnf(t2504,plain,
sk16(sk19,sk20) = ifeq(next_subocc(X1,sk17(sk19,sk20),tptp0),true,ifeq(true,true,X1,sk16(sk19,sk20)),sk16(sk19,sk20)),
inference(cp,[status(thm)],[t262,t2501]) ).
cnf(t20857,plain,
sk16(sk19,sk20) = ifeq(next_subocc(X1,sk17(sk19,sk20),tptp0),true,X1,sk16(sk19,sk20)),
inference(step,[status(thm)],[t2504,t256]) ).
cnf(t8164,plain,
ifeq(next_subocc(X1,sk17(sk19,sk20),tptp0),true,X1,sk16(sk19,sk20)) = sk16(sk19,sk20),
inference(orient,[status(thm)],[t20857]) ).
cnf(t2515,plain,
sk17(sk19,sk20) = ifeq(next_subocc(X1,sk18(sk19,sk20),tptp0),true,ifeq(true,true,X1,sk17(sk19,sk20)),sk17(sk19,sk20)),
inference(cp,[status(thm)],[t262,t2511]) ).
cnf(t20858,plain,
sk17(sk19,sk20) = ifeq(next_subocc(X1,sk18(sk19,sk20),tptp0),true,X1,sk17(sk19,sk20)),
inference(step,[status(thm)],[t2515,t256]) ).
cnf(t8165,plain,
ifeq(next_subocc(X1,sk18(sk19,sk20),tptp0),true,X1,sk17(sk19,sk20)) = sk17(sk19,sk20),
inference(orient,[status(thm)],[t20858]) ).
cnf(t51,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t265,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t51]) ).
fof(f36,axiom,
! [X109,X110,X111,X112] :
( ( leaf_occ(X110,X111)
& leaf_occ(X109,X111)
& ~ atomic(X112)
& occurrence_of(X111,X112) )
=> X109 = X110 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_36) ).
fof(f36_nnf,plain,
! [X109,X110,X111,X112] :
( X109 = X110
| ~ leaf_occ(X110,X111)
| ~ leaf_occ(X109,X111)
| atomic(X112)
| ~ occurrence_of(X111,X112) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X111,X112,X109,X110] :
( X109 = X110
| ~ leaf_occ(X110,X111)
| ~ leaf_occ(X109,X111)
| atomic(X112)
| ~ occurrence_of(X111,X112) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c67,plain,
( X0 = X1
| ~ leaf_occ(X1,X2)
| ~ leaf_occ(X0,X2)
| atomic(X3)
| ~ occurrence_of(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t210,plain,
ifeq(occurrence_of(X1,X2),true,ifeq(leaf_occ(X3,X1),true,ifeq(leaf_occ(X4,X1),true,or(atomic(X2),eq(X3,X4)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(t278,plain,
ifeq(occurrence_of(X1,X2),true,ifeq(leaf_occ(X3,X1),true,ifeq(leaf_occ(X4,X1),true,or(atomic(X2),eq(X3,X4)),true),true),true) = true,
inference(orient,[status(thm)],[t210]) ).
cnf(t855,plain,
true = ifeq(true,true,ifeq(leaf_occ(X1,sk20),true,ifeq(leaf_occ(X2,sk20),true,or(atomic(tptp0),eq(X1,X2)),true),true),true),
inference(cp,[status(thm)],[t278,t836]) ).
cnf(t21943,plain,
true = ifeq(leaf_occ(X1,sk20),true,ifeq(leaf_occ(X2,sk20),true,or(atomic(tptp0),eq(X1,X2)),true),true),
inference(step,[status(thm)],[t855,t256]) ).
fof(f51,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_51) ).
fof(f51_nnf,plain,
~ atomic(tptp0),
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
~ atomic(tptp0),
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c90,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(t4,plain,
atomic(tptp0) = false,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t1464,plain,
atomic(tptp0) = false,
inference(orient,[status(thm)],[t4]) ).
cnf(t21944,plain,
true = ifeq(leaf_occ(X1,sk20),true,ifeq(leaf_occ(X2,sk20),true,or(false,eq(X1,X2)),true),true),
inference(step,[status(thm)],[t21943,t1464]) ).
cnf(t21945,plain,
true = ifeq(leaf_occ(X1,sk20),true,ifeq(leaf_occ(X2,sk20),true,eq(X1,X2),true),true),
inference(step,[status(thm)],[t21944,t267]) ).
cnf(t16695,plain,
ifeq(leaf_occ(X1,sk20),true,ifeq(leaf_occ(X2,sk20),true,eq(X1,X2),true),true) = true,
inference(orient,[status(thm)],[t21945]) ).
cnf(t16706,plain,
true = ifeq(true,true,ifeq(leaf_occ(X1,sk20),true,eq(sk18(sk19,sk20),X1),true),true),
inference(cp,[status(thm)],[t16695,t1653]) ).
cnf(t21997,plain,
true = ifeq(leaf_occ(X1,sk20),true,eq(sk18(sk19,sk20),X1),true),
inference(step,[status(thm)],[t16706,t256]) ).
cnf(t17205,plain,
ifeq(leaf_occ(X1,sk20),true,eq(sk18(sk19,sk20),X1),true) = true,
inference(orient,[status(thm)],[t21997]) ).
cnf(t14071,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),true),true),true),
inference(cp,[status(thm)],[t311,t14058]) ).
cnf(t21641,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),true),true),true),
inference(step,[status(thm)],[t14071,t836]) ).
cnf(t21642,plain,
true = ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),true),true),
inference(step,[status(thm)],[t21641,t256]) ).
cnf(t21643,plain,
true = ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),true),
inference(step,[status(thm)],[t21642,t256]) ).
cnf(t21644,plain,
true = ifeq(true,true,or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),true),
inference(step,[status(thm)],[t21643,t1803]) ).
cnf(t21645,plain,
true = or(leaf_occ(sk17(sk19,sk20),sk20),leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),
inference(step,[status(thm)],[t21644,t256]) ).
cnf(t21646,plain,
true = or(false,leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20)),
inference(step,[status(thm)],[t21645,t5674]) ).
cnf(t21647,plain,
true = leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20),
inference(step,[status(thm)],[t21646,t267]) ).
cnf(t14122,plain,
leaf_occ(sk18(sk17(sk19,sk20),sk20),sk20) = true,
inference(orient,[status(thm)],[t21647]) ).
cnf(t17209,plain,
true = ifeq(true,true,eq(sk18(sk19,sk20),sk18(sk17(sk19,sk20),sk20)),true),
inference(cp,[status(thm)],[t17205,t14122]) ).
cnf(t22000,plain,
true = eq(sk18(sk19,sk20),sk18(sk17(sk19,sk20),sk20)),
inference(step,[status(thm)],[t17209,t256]) ).
cnf(t17228,plain,
eq(sk18(sk19,sk20),sk18(sk17(sk19,sk20),sk20)) = true,
inference(orient,[status(thm)],[t22000]) ).
cnf(t17229,plain,
sk18(sk17(sk19,sk20),sk20) = ifeq(true,true,sk18(sk19,sk20),sk18(sk17(sk19,sk20),sk20)),
inference(cp,[status(thm)],[t265,t17228]) ).
cnf(t22001,plain,
sk18(sk17(sk19,sk20),sk20) = sk18(sk19,sk20),
inference(step,[status(thm)],[t17229,t256]) ).
cnf(t17238,plain,
sk18(sk17(sk19,sk20),sk20) = sk18(sk19,sk20),
inference(orient,[status(thm)],[t22001]) ).
cnf(t17239,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),true),true),
inference(cp,[status(thm)],[t313,t17238]) ).
cnf(t22012,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),true),true),
inference(step,[status(thm)],[t17239,t836]) ).
cnf(t22013,plain,
true = ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t22012,t256]) ).
cnf(t22014,plain,
true = ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t22013,t14058]) ).
cnf(t22015,plain,
true = ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t22014,t256]) ).
cnf(t22016,plain,
true = ifeq(true,true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t22015,t1803]) ).
cnf(t22017,plain,
true = or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t22016,t256]) ).
cnf(t22018,plain,
true = or(false,next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t22017,t5674]) ).
cnf(t22019,plain,
true = next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0),
inference(step,[status(thm)],[t22018,t267]) ).
cnf(t17285,plain,
next_subocc(sk17(sk17(sk19,sk20),sk20),sk18(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t22019]) ).
cnf(t17287,plain,
sk17(sk19,sk20) = ifeq(true,true,sk17(sk17(sk19,sk20),sk20),sk17(sk19,sk20)),
inference(cp,[status(thm)],[t8165,t17285]) ).
cnf(t22020,plain,
sk17(sk19,sk20) = sk17(sk17(sk19,sk20),sk20),
inference(step,[status(thm)],[t17287,t256]) ).
cnf(t17297,plain,
sk17(sk17(sk19,sk20),sk20) = sk17(sk19,sk20),
inference(orient,[status(thm)],[t22020]) ).
cnf(t17298,plain,
true = ifeq(occurrence_of(sk20,tptp0),true,ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),true),true),
inference(cp,[status(thm)],[t314,t17297]) ).
cnf(t22271,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),true),true),
inference(step,[status(thm)],[t17298,t836]) ).
cnf(t22272,plain,
true = ifeq(subactivity_occurrence(sk17(sk19,sk20),sk20),true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t22271,t256]) ).
cnf(t22273,plain,
true = ifeq(true,true,ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),true),
inference(step,[status(thm)],[t22272,t14058]) ).
cnf(t22274,plain,
true = ifeq(arboreal(sk17(sk19,sk20)),true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t22273,t256]) ).
cnf(t22275,plain,
true = ifeq(true,true,or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),true),
inference(step,[status(thm)],[t22274,t1803]) ).
cnf(t22276,plain,
true = or(leaf_occ(sk17(sk19,sk20),sk20),next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t22275,t256]) ).
cnf(t22277,plain,
true = or(false,next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0)),
inference(step,[status(thm)],[t22276,t5674]) ).
cnf(t22278,plain,
true = next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0),
inference(step,[status(thm)],[t22277,t267]) ).
cnf(t19321,plain,
next_subocc(sk16(sk17(sk19,sk20),sk20),sk17(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t22278]) ).
cnf(t19323,plain,
sk16(sk19,sk20) = ifeq(true,true,sk16(sk17(sk19,sk20),sk20),sk16(sk19,sk20)),
inference(cp,[status(thm)],[t8164,t19321]) ).
cnf(t22279,plain,
sk16(sk19,sk20) = sk16(sk17(sk19,sk20),sk20),
inference(step,[status(thm)],[t19323,t256]) ).
cnf(t19334,plain,
sk16(sk17(sk19,sk20),sk20) = sk16(sk19,sk20),
inference(orient,[status(thm)],[t22279]) ).
cnf(t22281,plain,
earlier(sk16(sk19,sk20),sk17(sk19,sk20)) = false,
inference(step,[status(thm)],[t16132,t19334]) ).
cnf(t2502,plain,
true = ifeq(true,true,min_precedes(sk16(sk19,sk20),sk17(sk19,sk20),tptp0),true),
inference(cp,[status(thm)],[t358,t2501]) ).
cnf(t20124,plain,
true = min_precedes(sk16(sk19,sk20),sk17(sk19,sk20),tptp0),
inference(step,[status(thm)],[t2502,t256]) ).
cnf(t2886,plain,
min_precedes(sk16(sk19,sk20),sk17(sk19,sk20),tptp0) = true,
inference(orient,[status(thm)],[t20124]) ).
cnf(t2887,plain,
true = ifeq(true,true,precedes(sk16(sk19,sk20),sk17(sk19,sk20)),true),
inference(cp,[status(thm)],[t345,t2886]) ).
cnf(t20131,plain,
true = precedes(sk16(sk19,sk20),sk17(sk19,sk20)),
inference(step,[status(thm)],[t2887,t256]) ).
cnf(t2961,plain,
precedes(sk16(sk19,sk20),sk17(sk19,sk20)) = true,
inference(orient,[status(thm)],[t20131]) ).
cnf(t2963,plain,
true = ifeq(true,true,earlier(sk16(sk19,sk20),sk17(sk19,sk20)),true),
inference(cp,[status(thm)],[t400,t2961]) ).
cnf(t20133,plain,
true = earlier(sk16(sk19,sk20),sk17(sk19,sk20)),
inference(step,[status(thm)],[t2963,t256]) ).
cnf(t2976,plain,
earlier(sk16(sk19,sk20),sk17(sk19,sk20)) = true,
inference(orient,[status(thm)],[t20133]) ).
cnf(t22282,plain,
true = false,
inference(step,[status(thm)],[t22281,t2976]) ).
cnf(t19337,plain,
true = false,
inference(rw,[status(thm)],[t22282]) ).
cnf(t19344,plain,
false = true,
inference(orient,[status(thm)],[t19337]) ).
fof(f14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f14_nnf,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c24,plain,
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f19,axiom,
! [X49,X50,X51] :
( min_precedes(X49,X50,X51)
=> ~ atomic(X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_19) ).
fof(f19_nnf,plain,
! [X49,X50,X51] :
( ~ atomic(X51)
| ~ min_precedes(X49,X50,X51) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X49,X50,X51] :
( ~ atomic(X51)
| ~ min_precedes(X49,X50,X51) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c29,plain,
( ~ atomic(X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
fof(f21,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ~ ? [X59] : min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(f21_nnf,plain,
! [X56,X57] :
( ( ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X56,X57,X59,X58] :
( ( min_precedes(X56,sk6(X56,X57),X57)
| ( ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ~ min_precedes(X56,X59,X57)
& ( min_precedes(sk5(X56,X57),X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5,sk6])],[f21_nnf]) ).
cnf(c32,plain,
( ~ min_precedes(X0,X3,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(c36,plain,
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f38,axiom,
! [X117,X118,X119] :
( ( root_occ(X118,X117)
& occurrence_of(X117,X119) )
=> ~ ? [X120] : min_precedes(X120,X118,X119) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_38) ).
fof(f38_nnf,plain,
! [X117,X118,X119] :
( ! [X120] : ~ min_precedes(X120,X118,X119)
| ~ root_occ(X118,X117)
| ~ occurrence_of(X117,X119) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X117,X119,X118,X120] :
( ~ min_precedes(X120,X118,X119)
| ~ root_occ(X118,X117)
| ~ occurrence_of(X117,X119) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c69,plain,
( ~ min_precedes(X3,X1,X2)
| ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
fof(f56,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_56) ).
fof(f56_nnf,plain,
tptp4 != tptp3,
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
tptp4 != tptp3,
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c95,plain,
tptp4 != tptp3,
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
fof(f57,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_57) ).
fof(f57_nnf,plain,
tptp4 != tptp1,
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
tptp4 != tptp1,
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c96,plain,
tptp4 != tptp1,
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f58,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_58) ).
fof(f58_nnf,plain,
tptp4 != tptp2,
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
tptp4 != tptp2,
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c97,plain,
tptp4 != tptp2,
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
fof(f59,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_59) ).
fof(f59_nnf,plain,
tptp3 != tptp1,
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
tptp3 != tptp1,
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c98,plain,
tptp3 != tptp1,
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f60,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_60) ).
fof(f60_nnf,plain,
tptp3 != tptp2,
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
tptp3 != tptp2,
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c99,plain,
tptp3 != tptp2,
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
fof(f61,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_61) ).
fof(f61_nnf,plain,
tptp1 != tptp2,
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
tptp1 != tptp2,
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c100,plain,
tptp1 != tptp2,
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c6,c24,c29,c32,c36,c68,c69,c90,c95,c96,c97,c98,c99,c100,c104]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t19344]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO016+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/5.41 % Computer : n017.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Thu Sep 24 06:28:07 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 104.41/18.80 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 104.41/18.80 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------