%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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:22 PM UTC 2026
% Result : Theorem 128.61s 26.86s
% Output : Proof 128.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 21
% Syntax : Number of formulae : 217 ( 173 unt; 0 def)
% Number of atoms : 389 ( 164 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 319 ( 147 ~; 99 |; 63 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-4 aty)
% Number of variables : 211 ( 6 sgn 84 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f45,conjecture,
! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f45_neg,negated_conjecture,
~ ! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f45_nnf,plain,
? [X100,X101] :
( ! [X102,X103] :
( ~ leaf(X103,tptp0)
| ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(X100,X102,tptp0)
| ~ occurrence_of(X102,tptp3) )
& ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) ),
inference(nnf_transformation,[status(thm)],[f45_neg]) ).
fof(f45_sk,plain,
! [X102,X103] :
( ( ~ leaf(X103,tptp0)
| ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(sk17,X102,tptp0)
| ~ occurrence_of(X102,tptp3) )
& ~ leaf_occ(sk17,sk18)
& arboreal(sk17)
& subactivity_occurrence(sk17,sk18)
& occurrence_of(sk18,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17,sk18])],[f45_nnf]) ).
cnf(c87,plain,
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp1)
| ~ next_subocc(sk17,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t218,plain,
or(not(occurrence_of(X1,tptp3)),or(not(next_subocc(sk17,X1,tptp0)),or(not(occurrence_of(X2,tptp1)),or(not(min_precedes(X1,X2,tptp0)),not(leaf(X2,tptp0)))))) = true,
inference(equality_encoding,[status(esa)],[c87]) ).
cnf(t460,plain,
or(not(occurrence_of(X1,tptp3)),or(not(next_subocc(sk17,X1,tptp0)),or(not(occurrence_of(X2,tptp1)),or(not(min_precedes(X1,X2,tptp0)),not(leaf(X2,tptp0)))))) = true,
inference(orient,[status(thm)],[t218]) ).
fof(f0,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X1,X2,X3)
& min_precedes(X0,X1,X3) )
=> min_precedes(X0,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos) ).
fof(f0_nnf,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1,X3,X2] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( min_precedes(X0,X2,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t169,plain,
ifeq(min_precedes(X1,X2,X3),true,ifeq(min_precedes(X2,X4,X3),true,min_precedes(X1,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t318,plain,
ifeq(min_precedes(X1,X2,X3),true,ifeq(min_precedes(X2,X4,X3),true,min_precedes(X1,X4,X3),true),true) = true,
inference(orient,[status(thm)],[t169]) ).
fof(f4,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/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f4_nnf,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)],[f4]) ).
fof(f4_sk,plain,
! [X15,X16,X17,X18] :
( ( ( min_precedes(sk0(X15,X16,X17),X16,X17)
& min_precedes(X15,sk0(X15,X16,X17),X17) )
| ~ min_precedes(X15,X16,X17)
| next_subocc(X15,X16,X17) )
& ( ( ( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f4_nnf]) ).
cnf(c4,plain,
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t98,plain,
ifeq(next_subocc(X1,X2,X3),true,min_precedes(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t353,plain,
ifeq(next_subocc(X1,X2,X3),true,min_precedes(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t98]) ).
fof(f32,axiom,
! [X95,X96] :
( ( ~ leaf_occ(X95,X96)
& arboreal(X95)
& subactivity_occurrence(X95,X96)
& occurrence_of(X96,tptp0) )
=> ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f32_nnf,plain,
! [X95,X96] :
( ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) )
| leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X96,X95] :
( ( leaf(sk16(X95,X96),tptp0)
& next_subocc(sk15(X95,X96),sk16(X95,X96),tptp0)
& ( occurrence_of(sk16(X95,X96),tptp1)
| occurrence_of(sk16(X95,X96),tptp2) )
& next_subocc(sk14(X95,X96),sk15(X95,X96),tptp0)
& occurrence_of(sk15(X95,X96),tptp4)
& next_subocc(X95,sk14(X95,X96),tptp0)
& occurrence_of(sk14(X95,X96),tptp3) )
| leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14,sk15,sk16])],[f32_nnf]) ).
cnf(c66,plain,
( next_subocc(sk14(X0,X1),sk15(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t229,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk14(X2,X1),sk15(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c66]) ).
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(sk14(X2,X1),sk15(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t229]) ).
cnf(c85,plain,
~ leaf_occ(sk17,sk18),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t22,plain,
leaf_occ(sk17,sk18) = false,
inference(equality_encoding,[status(esa)],[c85]) ).
cnf(t617,plain,
leaf_occ(sk17,sk18) = false,
inference(orient,[status(thm)],[t22]) ).
cnf(t626,plain,
true = ifeq(occurrence_of(sk18,tptp0),true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),true),true),
inference(cp,[status(thm)],[t314,t617]) ).
cnf(c82,plain,
occurrence_of(sk18,tptp0),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t23,plain,
occurrence_of(sk18,tptp0) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(t416,plain,
occurrence_of(sk18,tptp0) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t14272,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),true),true),
inference(step,[status(thm)],[t626,t416]) ).
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(t14273,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14272,t256]) ).
cnf(c83,plain,
subactivity_occurrence(sk17,sk18),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t29,plain,
subactivity_occurrence(sk17,sk18) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t540,plain,
subactivity_occurrence(sk17,sk18) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(t14274,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14273,t540]) ).
cnf(t14275,plain,
true = ifeq(arboreal(sk17),true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14274,t256]) ).
cnf(c84,plain,
arboreal(sk17),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t3,plain,
arboreal(sk17) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(t573,plain,
arboreal(sk17) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t14276,plain,
true = ifeq(true,true,or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14275,t573]) ).
cnf(t14277,plain,
true = or(false,next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0)),
inference(step,[status(thm)],[t14276,t256]) ).
cnf(t26,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t263,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t26]) ).
cnf(t14278,plain,
true = next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0),
inference(step,[status(thm)],[t14277,t263]) ).
cnf(t1104,plain,
next_subocc(sk14(sk17,sk18),sk15(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14278]) ).
cnf(t1105,plain,
true = ifeq(true,true,min_precedes(sk14(sk17,sk18),sk15(sk17,sk18),tptp0),true),
inference(cp,[status(thm)],[t353,t1104]) ).
cnf(t14307,plain,
true = min_precedes(sk14(sk17,sk18),sk15(sk17,sk18),tptp0),
inference(step,[status(thm)],[t1105,t256]) ).
cnf(t1279,plain,
min_precedes(sk14(sk17,sk18),sk15(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14307]) ).
cnf(t1292,plain,
true = ifeq(true,true,ifeq(min_precedes(sk15(sk17,sk18),X1,tptp0),true,min_precedes(sk14(sk17,sk18),X1,tptp0),true),true),
inference(cp,[status(thm)],[t318,t1279]) ).
cnf(t16296,plain,
true = ifeq(min_precedes(sk15(sk17,sk18),X1,tptp0),true,min_precedes(sk14(sk17,sk18),X1,tptp0),true),
inference(step,[status(thm)],[t1292,t256]) ).
cnf(t13219,plain,
ifeq(min_precedes(sk15(sk17,sk18),X1,tptp0),true,min_precedes(sk14(sk17,sk18),X1,tptp0),true) = true,
inference(orient,[status(thm)],[t16296]) ).
cnf(c68,plain,
( next_subocc(sk15(X0,X1),sk16(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t230,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),next_subocc(sk15(X2,X1),sk16(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
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(sk15(X2,X1),sk16(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t230]) ).
cnf(t627,plain,
true = ifeq(occurrence_of(sk18,tptp0),true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),true),true),
inference(cp,[status(thm)],[t313,t617]) ).
cnf(t14279,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),true),true),
inference(step,[status(thm)],[t627,t416]) ).
cnf(t14280,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14279,t256]) ).
cnf(t14281,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14280,t540]) ).
cnf(t14282,plain,
true = ifeq(arboreal(sk17),true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14281,t256]) ).
cnf(t14283,plain,
true = ifeq(true,true,or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14282,t573]) ).
cnf(t14284,plain,
true = or(false,next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0)),
inference(step,[status(thm)],[t14283,t256]) ).
cnf(t14285,plain,
true = next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0),
inference(step,[status(thm)],[t14284,t263]) ).
cnf(t1110,plain,
next_subocc(sk15(sk17,sk18),sk16(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14285]) ).
cnf(t1112,plain,
true = ifeq(true,true,min_precedes(sk15(sk17,sk18),sk16(sk17,sk18),tptp0),true),
inference(cp,[status(thm)],[t353,t1110]) ).
cnf(t14317,plain,
true = min_precedes(sk15(sk17,sk18),sk16(sk17,sk18),tptp0),
inference(step,[status(thm)],[t1112,t256]) ).
cnf(t1349,plain,
min_precedes(sk15(sk17,sk18),sk16(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14317]) ).
cnf(t13223,plain,
true = ifeq(true,true,min_precedes(sk14(sk17,sk18),sk16(sk17,sk18),tptp0),true),
inference(cp,[status(thm)],[t13219,t1349]) ).
cnf(t16297,plain,
true = min_precedes(sk14(sk17,sk18),sk16(sk17,sk18),tptp0),
inference(step,[status(thm)],[t13223,t256]) ).
cnf(t13225,plain,
min_precedes(sk14(sk17,sk18),sk16(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t16297]) ).
cnf(t13242,plain,
true = or(not(occurrence_of(sk14(sk17,sk18),tptp3)),or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(cp,[status(thm)],[t460,t13225]) ).
cnf(c63,plain,
( occurrence_of(sk14(X0,X1),tptp3)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t215,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),occurrence_of(sk14(X2,X1),tptp3)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(t309,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),occurrence_of(sk14(X2,X1),tptp3)),true),true),true) = true,
inference(orient,[status(thm)],[t215]) ).
cnf(t630,plain,
true = ifeq(occurrence_of(sk18,tptp0),true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),true),true),
inference(cp,[status(thm)],[t309,t617]) ).
cnf(t14196,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),true),true),
inference(step,[status(thm)],[t630,t416]) ).
cnf(t14197,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),true),
inference(step,[status(thm)],[t14196,t256]) ).
cnf(t14198,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),true),
inference(step,[status(thm)],[t14197,t540]) ).
cnf(t14199,plain,
true = ifeq(arboreal(sk17),true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),
inference(step,[status(thm)],[t14198,t256]) ).
cnf(t14200,plain,
true = ifeq(true,true,or(false,occurrence_of(sk14(sk17,sk18),tptp3)),true),
inference(step,[status(thm)],[t14199,t573]) ).
cnf(t14201,plain,
true = or(false,occurrence_of(sk14(sk17,sk18),tptp3)),
inference(step,[status(thm)],[t14200,t256]) ).
cnf(t14202,plain,
true = occurrence_of(sk14(sk17,sk18),tptp3),
inference(step,[status(thm)],[t14201,t263]) ).
cnf(t777,plain,
occurrence_of(sk14(sk17,sk18),tptp3) = true,
inference(orient,[status(thm)],[t14202]) ).
cnf(t16329,plain,
true = or(not(true),or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(step,[status(thm)],[t13242,t777]) ).
cnf(t10,plain,
not(true) = false,
introduced(definition) ).
cnf(t615,plain,
not(true) = false,
inference(orient,[status(thm)],[t10]) ).
cnf(t16330,plain,
true = or(false,or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(step,[status(thm)],[t16329,t615]) ).
cnf(t16331,plain,
true = or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16330,t263]) ).
cnf(c64,plain,
( next_subocc(X0,sk14(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t222,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,sk14(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c64]) ).
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,sk14(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t222]) ).
cnf(t628,plain,
true = ifeq(occurrence_of(sk18,tptp0),true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),true),true),
inference(cp,[status(thm)],[t312,t617]) ).
cnf(t14212,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),true),true),
inference(step,[status(thm)],[t628,t416]) ).
cnf(t14213,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14212,t256]) ).
cnf(t14214,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14213,t540]) ).
cnf(t14215,plain,
true = ifeq(arboreal(sk17),true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14214,t256]) ).
cnf(t14216,plain,
true = ifeq(true,true,or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14215,t573]) ).
cnf(t14217,plain,
true = or(false,next_subocc(sk17,sk14(sk17,sk18),tptp0)),
inference(step,[status(thm)],[t14216,t256]) ).
cnf(t14218,plain,
true = next_subocc(sk17,sk14(sk17,sk18),tptp0),
inference(step,[status(thm)],[t14217,t263]) ).
cnf(t840,plain,
next_subocc(sk17,sk14(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14218]) ).
cnf(t16332,plain,
true = or(not(true),or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16331,t840]) ).
cnf(t16333,plain,
true = or(false,or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16332,t615]) ).
cnf(t16334,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp1)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))),
inference(step,[status(thm)],[t16333,t263]) ).
cnf(c67,plain,
( occurrence_of(sk16(X0,X1),tptp1)
| occurrence_of(sk16(X0,X1),tptp2)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t240,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),or(occurrence_of(sk16(X2,X1),tptp2),occurrence_of(sk16(X2,X1),tptp1))),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(t310,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),or(occurrence_of(sk16(X2,X1),tptp2),occurrence_of(sk16(X2,X1),tptp1))),true),true),true) = true,
inference(orient,[status(thm)],[t240]) ).
cnf(t438,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(X1,sk18),true,ifeq(arboreal(X1),true,or(leaf_occ(X1,sk18),or(occurrence_of(sk16(X1,sk18),tptp2),occurrence_of(sk16(X1,sk18),tptp1))),true),true),true),
inference(cp,[status(thm)],[t310,t416]) ).
cnf(t16083,plain,
true = ifeq(subactivity_occurrence(X1,sk18),true,ifeq(arboreal(X1),true,or(leaf_occ(X1,sk18),or(occurrence_of(sk16(X1,sk18),tptp2),occurrence_of(sk16(X1,sk18),tptp1))),true),true),
inference(step,[status(thm)],[t438,t256]) ).
cnf(t11921,plain,
ifeq(subactivity_occurrence(X1,sk18),true,ifeq(arboreal(X1),true,or(leaf_occ(X1,sk18),or(occurrence_of(sk16(X1,sk18),tptp2),occurrence_of(sk16(X1,sk18),tptp1))),true),true) = true,
inference(orient,[status(thm)],[t16083]) ).
cnf(t47,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t600,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t47]) ).
cnf(c86,plain,
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp2)
| ~ next_subocc(sk17,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(t219,plain,
or(not(occurrence_of(X1,tptp3)),or(not(next_subocc(sk17,X1,tptp0)),or(not(occurrence_of(X2,tptp2)),or(not(min_precedes(X1,X2,tptp0)),not(leaf(X2,tptp0)))))) = true,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(t461,plain,
or(not(occurrence_of(X1,tptp3)),or(not(next_subocc(sk17,X1,tptp0)),or(not(occurrence_of(X2,tptp2)),or(not(min_precedes(X1,X2,tptp0)),not(leaf(X2,tptp0)))))) = true,
inference(orient,[status(thm)],[t219]) ).
cnf(t13241,plain,
true = or(not(occurrence_of(sk14(sk17,sk18),tptp3)),or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(cp,[status(thm)],[t461,t13225]) ).
cnf(t16298,plain,
true = or(not(true),or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(step,[status(thm)],[t13241,t777]) ).
cnf(t16299,plain,
true = or(false,or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))))),
inference(step,[status(thm)],[t16298,t615]) ).
cnf(t16300,plain,
true = or(not(next_subocc(sk17,sk14(sk17,sk18),tptp0)),or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16299,t263]) ).
cnf(t16301,plain,
true = or(not(true),or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16300,t840]) ).
cnf(t16302,plain,
true = or(false,or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0))))),
inference(step,[status(thm)],[t16301,t615]) ).
cnf(t16303,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))),
inference(step,[status(thm)],[t16302,t263]) ).
cnf(t16304,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp2)),or(false,not(leaf(sk16(sk17,sk18),tptp0)))),
inference(step,[status(thm)],[t16303,t615]) ).
cnf(t16305,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp2)),not(leaf(sk16(sk17,sk18),tptp0))),
inference(step,[status(thm)],[t16304,t263]) ).
cnf(c69,plain,
( leaf(sk16(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t214,plain,
ifeq(occurrence_of(X1,tptp0),true,ifeq(subactivity_occurrence(X2,X1),true,ifeq(arboreal(X2),true,or(leaf_occ(X2,X1),leaf(sk16(X2,X1),tptp0)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c69]) ).
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(sk16(X2,X1),tptp0)),true),true),true) = true,
inference(orient,[status(thm)],[t214]) ).
cnf(t629,plain,
true = ifeq(occurrence_of(sk18,tptp0),true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),true),true),
inference(cp,[status(thm)],[t311,t617]) ).
cnf(t14189,plain,
true = ifeq(true,true,ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),true),true),
inference(step,[status(thm)],[t629,t416]) ).
cnf(t14190,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14189,t256]) ).
cnf(t14191,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),true),
inference(step,[status(thm)],[t14190,t540]) ).
cnf(t14192,plain,
true = ifeq(arboreal(sk17),true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14191,t256]) ).
cnf(t14193,plain,
true = ifeq(true,true,or(false,leaf(sk16(sk17,sk18),tptp0)),true),
inference(step,[status(thm)],[t14192,t573]) ).
cnf(t14194,plain,
true = or(false,leaf(sk16(sk17,sk18),tptp0)),
inference(step,[status(thm)],[t14193,t256]) ).
cnf(t14195,plain,
true = leaf(sk16(sk17,sk18),tptp0),
inference(step,[status(thm)],[t14194,t263]) ).
cnf(t762,plain,
leaf(sk16(sk17,sk18),tptp0) = true,
inference(orient,[status(thm)],[t14195]) ).
cnf(t16306,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp2)),not(true)),
inference(step,[status(thm)],[t16305,t762]) ).
cnf(t16307,plain,
true = or(not(occurrence_of(sk16(sk17,sk18),tptp2)),false),
inference(step,[status(thm)],[t16306,t615]) ).
cnf(t24,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t262,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t16308,plain,
true = not(occurrence_of(sk16(sk17,sk18),tptp2)),
inference(step,[status(thm)],[t16307,t262]) ).
cnf(t13247,plain,
not(occurrence_of(sk16(sk17,sk18),tptp2)) = true,
inference(orient,[status(thm)],[t16308]) ).
cnf(t13248,plain,
false = ifeq(true,true,occurrence_of(sk16(sk17,sk18),tptp2),false),
inference(cp,[status(thm)],[t600,t13247]) ).
cnf(t16310,plain,
false = occurrence_of(sk16(sk17,sk18),tptp2),
inference(step,[status(thm)],[t13248,t256]) ).
cnf(t13275,plain,
occurrence_of(sk16(sk17,sk18),tptp2) = false,
inference(orient,[status(thm)],[t16310]) ).
cnf(t13292,plain,
true = ifeq(subactivity_occurrence(sk17,sk18),true,ifeq(arboreal(sk17),true,or(leaf_occ(sk17,sk18),or(false,occurrence_of(sk16(sk17,sk18),tptp1))),true),true),
inference(cp,[status(thm)],[t11921,t13275]) ).
cnf(t16313,plain,
true = ifeq(true,true,ifeq(arboreal(sk17),true,or(leaf_occ(sk17,sk18),or(false,occurrence_of(sk16(sk17,sk18),tptp1))),true),true),
inference(step,[status(thm)],[t13292,t540]) ).
cnf(t16314,plain,
true = ifeq(arboreal(sk17),true,or(leaf_occ(sk17,sk18),or(false,occurrence_of(sk16(sk17,sk18),tptp1))),true),
inference(step,[status(thm)],[t16313,t256]) ).
cnf(t16315,plain,
true = ifeq(true,true,or(leaf_occ(sk17,sk18),or(false,occurrence_of(sk16(sk17,sk18),tptp1))),true),
inference(step,[status(thm)],[t16314,t573]) ).
cnf(t16316,plain,
true = or(leaf_occ(sk17,sk18),or(false,occurrence_of(sk16(sk17,sk18),tptp1))),
inference(step,[status(thm)],[t16315,t256]) ).
cnf(t16317,plain,
true = or(false,or(false,occurrence_of(sk16(sk17,sk18),tptp1))),
inference(step,[status(thm)],[t16316,t617]) ).
cnf(t16318,plain,
true = or(false,occurrence_of(sk16(sk17,sk18),tptp1)),
inference(step,[status(thm)],[t16317,t263]) ).
cnf(t16319,plain,
true = occurrence_of(sk16(sk17,sk18),tptp1),
inference(step,[status(thm)],[t16318,t263]) ).
cnf(t13296,plain,
occurrence_of(sk16(sk17,sk18),tptp1) = true,
inference(orient,[status(thm)],[t16319]) ).
cnf(t16335,plain,
true = or(not(true),or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))),
inference(step,[status(thm)],[t16334,t13296]) ).
cnf(t16336,plain,
true = or(false,or(not(true),not(leaf(sk16(sk17,sk18),tptp0)))),
inference(step,[status(thm)],[t16335,t615]) ).
cnf(t16337,plain,
true = or(not(true),not(leaf(sk16(sk17,sk18),tptp0))),
inference(step,[status(thm)],[t16336,t263]) ).
cnf(t16338,plain,
true = or(false,not(leaf(sk16(sk17,sk18),tptp0))),
inference(step,[status(thm)],[t16337,t615]) ).
cnf(t16339,plain,
true = not(leaf(sk16(sk17,sk18),tptp0)),
inference(step,[status(thm)],[t16338,t263]) ).
cnf(t16340,plain,
true = not(true),
inference(step,[status(thm)],[t16339,t762]) ).
cnf(t16341,plain,
true = false,
inference(step,[status(thm)],[t16340,t615]) ).
cnf(t13328,plain,
false = true,
inference(orient,[status(thm)],[t16341]) ).
cnf(c5,plain,
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f7,axiom,
! [X25,X26,X27] :
( min_precedes(X25,X26,X27)
=> ~ root(X26,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f7_nnf,plain,
! [X25,X26,X27] :
( ~ root(X26,X27)
| ~ min_precedes(X25,X26,X27) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X25,X26,X27] :
( ~ root(X26,X27)
| ~ min_precedes(X25,X26,X27) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c11,plain,
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f9,axiom,
! [X30,X31] :
( earlier(X30,X31)
=> ~ earlier(X31,X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f9_nnf,plain,
! [X30,X31] :
( ~ earlier(X31,X30)
| ~ earlier(X30,X31) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X30,X31] :
( ~ earlier(X31,X30)
| ~ earlier(X30,X31) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c15,plain,
( ~ earlier(X1,X0)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f14,axiom,
! [X42,X43] :
( leaf(X42,X43)
<=> ( ~ ? [X45] : min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f14_nnf,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)],[f14]) ).
fof(f14_sk,plain,
! [X42,X43,X45,X44] :
( ( min_precedes(X42,sk4(X42,X43),X43)
| ( ~ min_precedes(X44,X42,X43)
& ~ root(X42,X43) )
| leaf(X42,X43) )
& ( ( ~ min_precedes(X42,X45,X43)
& ( min_precedes(sk3(X42,X43),X42,X43)
| root(X42,X43) ) )
| ~ leaf(X42,X43) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4])],[f14_nnf]) ).
cnf(c28,plain,
( ~ min_precedes(X0,X3,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f20,axiom,
! [X56,X57,X58] :
( ( root_occ(X57,X56)
& occurrence_of(X56,X58) )
=> ~ ? [X59] : min_precedes(X59,X57,X58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_20) ).
fof(f20_nnf,plain,
! [X56,X57,X58] :
( ! [X59] : ~ min_precedes(X59,X57,X58)
| ~ root_occ(X57,X56)
| ~ occurrence_of(X56,X58) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X56,X58,X57,X59] :
( ~ min_precedes(X59,X57,X58)
| ~ root_occ(X57,X56)
| ~ occurrence_of(X56,X58) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c41,plain,
( ~ min_precedes(X3,X1,X2)
| ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
fof(f21,axiom,
! [X60,X61,X62] :
( ( leaf_occ(X61,X60)
& occurrence_of(X60,X62) )
=> ~ ? [X63] : min_precedes(X61,X63,X62) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f21_nnf,plain,
! [X60,X61,X62] :
( ! [X63] : ~ min_precedes(X61,X63,X62)
| ~ leaf_occ(X61,X60)
| ~ occurrence_of(X60,X62) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X60,X62,X61,X63] :
( ~ min_precedes(X61,X63,X62)
| ~ leaf_occ(X61,X60)
| ~ occurrence_of(X60,X62) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c42,plain,
( ~ min_precedes(X1,X3,X2)
| ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f34,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f34_nnf,plain,
~ atomic(tptp0),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
~ atomic(tptp0),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c71,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f39,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(f39_nnf,plain,
tptp4 != tptp3,
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
tptp4 != tptp3,
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c76,plain,
tptp4 != tptp3,
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
fof(f40,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_40) ).
fof(f40_nnf,plain,
tptp4 != tptp2,
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
tptp4 != tptp2,
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c77,plain,
tptp4 != tptp2,
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f41,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_41) ).
fof(f41_nnf,plain,
tptp4 != tptp1,
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
tptp4 != tptp1,
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c78,plain,
tptp4 != tptp1,
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f42,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f42_nnf,plain,
tptp3 != tptp2,
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
tptp3 != tptp2,
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c79,plain,
tptp3 != tptp2,
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
fof(f43,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f43_nnf,plain,
tptp3 != tptp1,
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
tptp3 != tptp1,
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c80,plain,
tptp3 != tptp1,
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
fof(f44,axiom,
tptp2 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_44) ).
fof(f44_nnf,plain,
tptp2 != tptp1,
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
tptp2 != tptp1,
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c81,plain,
tptp2 != tptp1,
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5,c11,c15,c28,c41,c42,c71,c76,c77,c78,c79,c80,c81,c85,c86,c87]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t13328]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/10.37 % Computer : n014.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Thu Sep 24 06:31:30 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 128.61/26.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 128.61/26.86 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------