%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : PRO011+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 17:50:17 EDT 2022
% Result : Theorem 3.48s 3.72s
% Output : CNFRefutation 3.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 8
% Syntax : Number of formulae : 85 ( 15 unt; 1 def)
% Number of atoms : 318 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 347 ( 114 ~; 120 |; 92 &)
% ( 8 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 146 ( 4 sgn 81 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_07,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ) ).
fof(sos_34,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( occurrence_of(X103,X104)
& subactivity_occurrence(X102,X103)
& leaf(X102,X104) ) ) ).
fof(sos_45,axiom,
! [X145,X146] :
( ( leaf(X145,X146)
& ~ atomic(X146) )
=> ? [X147] :
( occurrence_of(X147,X146)
& leaf_occ(X145,X147) ) ) ).
fof(sos_46,axiom,
! [X148,X149,X150] :
( min_precedes(X148,X149,X150)
=> arboreal(X148) ) ).
fof(sos_49,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163,X164] :
( occurrence_of(X162,tptp3)
& root_occ(X162,X161)
& occurrence_of(X163,tptp4)
& next_subocc(X162,X163,tptp0)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) )
& next_subocc(X163,X164,tptp0)
& leaf_occ(X164,X161) ) ) ).
fof(sos_51,axiom,
~ atomic(tptp0) ).
fof(goals,conjecture,
! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( leaf_occ(X167,X165)
& ( occurrence_of(X167,tptp1)
=> ~ ? [X168] :
( occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,X165)
& min_precedes(X166,X168,tptp0) ) )
& ( occurrence_of(X167,tptp2)
=> ~ ? [X169] :
( occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,X165)
& min_precedes(X166,X169,tptp0) ) ) ) ) ).
fof(definition_0,definition,
! [X166,X167] :
( definitionFOFtoCNF_0(X166,X167)
<=> ( occurrence_of(X167,tptp1)
& ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,skolemFOFtoCNF_X165) ) ) ) ).
fof(subgoal_0,plain,
! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( leaf_occ(X167,X165)
& ( occurrence_of(X167,tptp1)
=> ~ ? [X168] :
( occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,X165)
& min_precedes(X166,X168,tptp0) ) )
& ( occurrence_of(X167,tptp2)
=> ~ ? [X169] :
( occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,X165)
& min_precedes(X166,X169,tptp0) ) ) ) ),
inference(strip,[],[goals]) ).
fof(negate_0_0,plain,
~ ! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( leaf_occ(X167,X165)
& ( occurrence_of(X167,tptp1)
=> ~ ? [X168] :
( occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,X165)
& min_precedes(X166,X168,tptp0) ) )
& ( occurrence_of(X167,tptp2)
=> ~ ? [X169] :
( occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,X165)
& min_precedes(X166,X169,tptp0) ) ) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [X16,X17] :
( ~ occurrence_of(X16,X17)
| ( ~ arboreal(X16)
<=> ~ atomic(X17) ) ),
inference(canonicalize,[],[sos_07]) ).
fof(normalize_0_1,plain,
! [X16,X17] :
( ~ occurrence_of(X16,X17)
| ( ~ arboreal(X16)
<=> ~ atomic(X17) ) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [X16,X17] :
( ( ~ arboreal(X16)
| ~ occurrence_of(X16,X17)
| atomic(X17) )
& ( ~ atomic(X17)
| ~ occurrence_of(X16,X17)
| arboreal(X16) ) ),
inference(clausify,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [X16,X17] :
( ~ arboreal(X16)
| ~ occurrence_of(X16,X17)
| atomic(X17) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
? [X165] :
( occurrence_of(X165,tptp0)
& ! [X166,X167] :
( ~ leaf_occ(X167,X165)
| ( occurrence_of(X167,tptp1)
& ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,X165) ) )
| ( occurrence_of(X167,tptp2)
& ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,X165) ) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_5,plain,
( occurrence_of(skolemFOFtoCNF_X165,tptp0)
& ! [X166,X167] :
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| ( occurrence_of(X167,tptp1)
& ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,skolemFOFtoCNF_X165) ) )
| ( occurrence_of(X167,tptp2)
& ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,skolemFOFtoCNF_X165) ) ) ) ),
inference(skolemize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
occurrence_of(skolemFOFtoCNF_X165,tptp0),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
! [X161] :
( ~ occurrence_of(X161,tptp0)
| ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X162,X163,tptp0)
& next_subocc(X163,X164,tptp0)
& occurrence_of(X162,tptp3)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) ) ) ),
inference(canonicalize,[],[sos_49]) ).
fof(normalize_0_8,plain,
! [X161] :
( ~ occurrence_of(X161,tptp0)
| ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X162,X163,tptp0)
& next_subocc(X163,X164,tptp0)
& occurrence_of(X162,tptp3)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) ) ) ),
inference(specialize,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [X161] :
( ( ~ occurrence_of(X161,tptp0)
| leaf_occ(skolemFOFtoCNF_X164(X161),X161) )
& ( ~ occurrence_of(X161,tptp0)
| next_subocc(skolemFOFtoCNF_X162(X161),skolemFOFtoCNF_X163(X161),tptp0) )
& ( ~ occurrence_of(X161,tptp0)
| next_subocc(skolemFOFtoCNF_X163(X161),skolemFOFtoCNF_X164(X161),tptp0) )
& ( ~ occurrence_of(X161,tptp0)
| occurrence_of(skolemFOFtoCNF_X162(X161),tptp3) )
& ( ~ occurrence_of(X161,tptp0)
| occurrence_of(skolemFOFtoCNF_X163(X161),tptp4) )
& ( ~ occurrence_of(X161,tptp0)
| root_occ(skolemFOFtoCNF_X162(X161),X161) )
& ( ~ occurrence_of(X161,tptp0)
| occurrence_of(skolemFOFtoCNF_X164(X161),tptp1)
| occurrence_of(skolemFOFtoCNF_X164(X161),tptp2) ) ),
inference(clausify,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [X161] :
( ~ occurrence_of(X161,tptp0)
| leaf_occ(skolemFOFtoCNF_X164(X161),X161) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [X102,X103] :
( ~ leaf_occ(X102,X103)
<=> ! [X104] :
( ~ leaf(X102,X104)
| ~ occurrence_of(X103,X104)
| ~ subactivity_occurrence(X102,X103) ) ),
inference(canonicalize,[],[sos_34]) ).
fof(normalize_0_12,plain,
! [X102,X103] :
( ~ leaf_occ(X102,X103)
<=> ! [X104] :
( ~ leaf(X102,X104)
| ~ occurrence_of(X103,X104)
| ~ subactivity_occurrence(X102,X103) ) ),
inference(specialize,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [X102,X103,X104] :
( ( ~ leaf_occ(X102,X103)
| leaf(X102,skolemFOFtoCNF_X104(X102,X103)) )
& ( ~ leaf_occ(X102,X103)
| occurrence_of(X103,skolemFOFtoCNF_X104(X102,X103)) )
& ( ~ leaf_occ(X102,X103)
| subactivity_occurrence(X102,X103) )
& ( ~ leaf(X102,X104)
| ~ occurrence_of(X103,X104)
| ~ subactivity_occurrence(X102,X103)
| leaf_occ(X102,X103) ) ),
inference(clausify,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [X102,X103] :
( ~ leaf_occ(X102,X103)
| leaf(X102,skolemFOFtoCNF_X104(X102,X103)) ),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [X145,X146] :
( ~ leaf(X145,X146)
| atomic(X146)
| ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) ) ),
inference(canonicalize,[],[sos_45]) ).
fof(normalize_0_16,plain,
! [X145,X146] :
( ~ leaf(X145,X146)
| atomic(X146)
| ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) ) ),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [X145,X146] :
( ( ~ leaf(X145,X146)
| atomic(X146)
| leaf_occ(X145,skolemFOFtoCNF_X147(X145,X146)) )
& ( ~ leaf(X145,X146)
| atomic(X146)
| occurrence_of(skolemFOFtoCNF_X147(X145,X146),X146) ) ),
inference(clausify,[],[normalize_0_16]) ).
fof(normalize_0_18,plain,
! [X145,X146] :
( ~ leaf(X145,X146)
| atomic(X146)
| occurrence_of(skolemFOFtoCNF_X147(X145,X146),X146) ),
inference(conjunct,[],[normalize_0_17]) ).
fof(normalize_0_19,plain,
! [X102,X103] :
( ~ leaf_occ(X102,X103)
| occurrence_of(X103,skolemFOFtoCNF_X104(X102,X103)) ),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_20,plain,
! [X16,X17] :
( ~ atomic(X17)
| ~ occurrence_of(X16,X17)
| arboreal(X16) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_21,plain,
~ atomic(tptp0),
inference(canonicalize,[],[sos_51]) ).
fof(normalize_0_22,plain,
! [X148] :
( arboreal(X148)
| ! [X149,X150] : ~ min_precedes(X148,X149,X150) ),
inference(canonicalize,[],[sos_46]) ).
fof(normalize_0_23,plain,
! [X148] :
( arboreal(X148)
| ! [X149,X150] : ~ min_precedes(X148,X149,X150) ),
inference(specialize,[],[normalize_0_22]) ).
fof(normalize_0_24,plain,
! [X148,X149,X150] :
( ~ min_precedes(X148,X149,X150)
| arboreal(X148) ),
inference(clausify,[],[normalize_0_23]) ).
fof(normalize_0_25,plain,
! [X166,X167] :
( ~ definitionFOFtoCNF_0(X166,X167)
<=> ( ~ occurrence_of(X167,tptp1)
| ! [X168] :
( ~ min_precedes(X166,X168,tptp0)
| ~ occurrence_of(X168,tptp2)
| ~ subactivity_occurrence(X168,skolemFOFtoCNF_X165) ) ) ),
inference(canonicalize,[],[definition_0]) ).
fof(normalize_0_26,plain,
! [X166,X167,X168] :
( ( ~ definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X168(X166),tptp0) )
& ( ~ definitionFOFtoCNF_0(X166,X167)
| occurrence_of(X167,tptp1) )
& ( ~ definitionFOFtoCNF_0(X166,X167)
| occurrence_of(skolemFOFtoCNF_X168(X166),tptp2) )
& ( ~ definitionFOFtoCNF_0(X166,X167)
| subactivity_occurrence(skolemFOFtoCNF_X168(X166),skolemFOFtoCNF_X165) )
& ( ~ min_precedes(X166,X168,tptp0)
| ~ occurrence_of(X167,tptp1)
| ~ occurrence_of(X168,tptp2)
| ~ subactivity_occurrence(X168,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167) ) ),
inference(clausify,[],[normalize_0_25]) ).
fof(normalize_0_27,plain,
! [X166,X167] :
( ~ definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X168(X166),tptp0) ),
inference(conjunct,[],[normalize_0_26]) ).
fof(normalize_0_28,plain,
! [X166,X167] :
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| ( occurrence_of(X167,tptp1)
& ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,skolemFOFtoCNF_X165) ) )
| ( occurrence_of(X167,tptp2)
& ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,skolemFOFtoCNF_X165) ) ) ),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_29,plain,
! [X166,X167] :
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| ( occurrence_of(X167,tptp1)
& ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2)
& subactivity_occurrence(X168,skolemFOFtoCNF_X165) ) )
| ( occurrence_of(X167,tptp2)
& ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,skolemFOFtoCNF_X165) ) ) ),
inference(specialize,[],[normalize_0_28]) ).
fof(normalize_0_30,plain,
! [X166,X167] :
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| ( occurrence_of(X167,tptp2)
& ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1)
& subactivity_occurrence(X169,skolemFOFtoCNF_X165) ) ) ),
inference(simplify,[],[normalize_0_29,normalize_0_25]) ).
fof(normalize_0_31,plain,
! [X166,X167] :
( ( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X169(X166),tptp0) )
& ( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| occurrence_of(X167,tptp2) )
& ( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| occurrence_of(skolemFOFtoCNF_X169(X166),tptp1) )
& ( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| subactivity_occurrence(skolemFOFtoCNF_X169(X166),skolemFOFtoCNF_X165) ) ),
inference(clausify,[],[normalize_0_30]) ).
fof(normalize_0_32,plain,
! [X166,X167] :
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X169(X166),tptp0) ),
inference(conjunct,[],[normalize_0_31]) ).
cnf(refute_0_0,plain,
( ~ arboreal(X16)
| ~ occurrence_of(X16,X17)
| atomic(X17) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_1,plain,
( ~ arboreal(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))
| ~ occurrence_of(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(subst,[],[refute_0_0:[bind(X16,$fot(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))),bind(X17,$fot(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))]]) ).
cnf(refute_0_2,plain,
occurrence_of(skolemFOFtoCNF_X165,tptp0),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_3,plain,
( ~ occurrence_of(X161,tptp0)
| leaf_occ(skolemFOFtoCNF_X164(X161),X161) ),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_4,plain,
( ~ occurrence_of(skolemFOFtoCNF_X165,tptp0)
| leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165) ),
inference(subst,[],[refute_0_3:[bind(X161,$fot(skolemFOFtoCNF_X165))]]) ).
cnf(refute_0_5,plain,
leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165),
inference(resolve,[$cnf( occurrence_of(skolemFOFtoCNF_X165,tptp0) )],[refute_0_2,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ leaf_occ(X102,X103)
| leaf(X102,skolemFOFtoCNF_X104(X102,X103)) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_7,plain,
( ~ leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)
| leaf(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(subst,[],[refute_0_6:[bind(X102,$fot(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))),bind(X103,$fot(skolemFOFtoCNF_X165))]]) ).
cnf(refute_0_8,plain,
leaf(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),
inference(resolve,[$cnf( leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165) )],[refute_0_5,refute_0_7]) ).
cnf(refute_0_9,plain,
( ~ leaf(X145,X146)
| atomic(X146)
| occurrence_of(skolemFOFtoCNF_X147(X145,X146),X146) ),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_10,plain,
( ~ leaf(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| occurrence_of(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(subst,[],[refute_0_9:[bind(X145,$fot(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))),bind(X146,$fot(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))]]) ).
cnf(refute_0_11,plain,
( atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| occurrence_of(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(resolve,[$cnf( leaf(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) )],[refute_0_8,refute_0_10]) ).
cnf(refute_0_12,plain,
( ~ leaf_occ(X102,X103)
| occurrence_of(X103,skolemFOFtoCNF_X104(X102,X103)) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_13,plain,
( ~ leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)
| occurrence_of(skolemFOFtoCNF_X165,skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(subst,[],[refute_0_12:[bind(X102,$fot(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))),bind(X103,$fot(skolemFOFtoCNF_X165))]]) ).
cnf(refute_0_14,plain,
occurrence_of(skolemFOFtoCNF_X165,skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),
inference(resolve,[$cnf( leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165) )],[refute_0_5,refute_0_13]) ).
cnf(refute_0_15,plain,
( ~ atomic(X17)
| ~ occurrence_of(X16,X17)
| arboreal(X16) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_16,plain,
( ~ atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| ~ occurrence_of(skolemFOFtoCNF_X165,skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| arboreal(skolemFOFtoCNF_X165) ),
inference(subst,[],[refute_0_15:[bind(X16,$fot(skolemFOFtoCNF_X165)),bind(X17,$fot(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))]]) ).
cnf(refute_0_17,plain,
( ~ atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))
| arboreal(skolemFOFtoCNF_X165) ),
inference(resolve,[$cnf( occurrence_of(skolemFOFtoCNF_X165,skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) )],[refute_0_14,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ arboreal(skolemFOFtoCNF_X165)
| ~ occurrence_of(skolemFOFtoCNF_X165,tptp0)
| atomic(tptp0) ),
inference(subst,[],[refute_0_0:[bind(X16,$fot(skolemFOFtoCNF_X165)),bind(X17,$fot(tptp0))]]) ).
cnf(refute_0_19,plain,
( ~ arboreal(skolemFOFtoCNF_X165)
| atomic(tptp0) ),
inference(resolve,[$cnf( occurrence_of(skolemFOFtoCNF_X165,tptp0) )],[refute_0_2,refute_0_18]) ).
cnf(refute_0_20,plain,
~ atomic(tptp0),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_21,plain,
~ arboreal(skolemFOFtoCNF_X165),
inference(resolve,[$cnf( atomic(tptp0) )],[refute_0_19,refute_0_20]) ).
cnf(refute_0_22,plain,
~ atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),
inference(resolve,[$cnf( arboreal(skolemFOFtoCNF_X165) )],[refute_0_17,refute_0_21]) ).
cnf(refute_0_23,plain,
occurrence_of(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),
inference(resolve,[$cnf( atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) )],[refute_0_11,refute_0_22]) ).
cnf(refute_0_24,plain,
( ~ arboreal(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)))
| atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) ),
inference(resolve,[$cnf( occurrence_of(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) )],[refute_0_23,refute_0_1]) ).
cnf(refute_0_25,plain,
~ arboreal(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))),
inference(resolve,[$cnf( atomic(skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)) )],[refute_0_24,refute_0_22]) ).
cnf(refute_0_26,plain,
( ~ min_precedes(X148,X149,X150)
| arboreal(X148) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_27,plain,
( ~ min_precedes(X_250,skolemFOFtoCNF_X168(X_250),tptp0)
| arboreal(X_250) ),
inference(subst,[],[refute_0_26:[bind(X148,$fot(X_250)),bind(X149,$fot(skolemFOFtoCNF_X168(X_250))),bind(X150,$fot(tptp0))]]) ).
cnf(refute_0_28,plain,
( ~ definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X168(X166),tptp0) ),
inference(canonicalize,[],[normalize_0_27]) ).
cnf(refute_0_29,plain,
( ~ definitionFOFtoCNF_0(X_239,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))
| min_precedes(X_239,skolemFOFtoCNF_X168(X_239),tptp0) ),
inference(subst,[],[refute_0_28:[bind(X166,$fot(X_239)),bind(X167,$fot(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165)))]]) ).
cnf(refute_0_30,plain,
( ~ min_precedes(X_238,skolemFOFtoCNF_X169(X_238),tptp0)
| arboreal(X_238) ),
inference(subst,[],[refute_0_26:[bind(X148,$fot(X_238)),bind(X149,$fot(skolemFOFtoCNF_X169(X_238))),bind(X150,$fot(tptp0))]]) ).
cnf(refute_0_31,plain,
( ~ leaf_occ(X167,skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X166,X167)
| min_precedes(X166,skolemFOFtoCNF_X169(X166),tptp0) ),
inference(canonicalize,[],[normalize_0_32]) ).
cnf(refute_0_32,plain,
( ~ leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165)
| definitionFOFtoCNF_0(X_236,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))
| min_precedes(X_236,skolemFOFtoCNF_X169(X_236),tptp0) ),
inference(subst,[],[refute_0_31:[bind(X166,$fot(X_236)),bind(X167,$fot(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165)))]]) ).
cnf(refute_0_33,plain,
( definitionFOFtoCNF_0(X_236,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))
| min_precedes(X_236,skolemFOFtoCNF_X169(X_236),tptp0) ),
inference(resolve,[$cnf( leaf_occ(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165) )],[refute_0_5,refute_0_32]) ).
cnf(refute_0_34,plain,
( definitionFOFtoCNF_0(X_238,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165))
| min_precedes(X_238,skolemFOFtoCNF_X169(X_238),tptp0) ),
inference(subst,[],[refute_0_33:[bind(X_236,$fot(X_238))]]) ).
cnf(refute_0_35,plain,
( arboreal(X_238)
| definitionFOFtoCNF_0(X_238,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165)) ),
inference(resolve,[$cnf( min_precedes(X_238,skolemFOFtoCNF_X169(X_238),tptp0) )],[refute_0_34,refute_0_30]) ).
cnf(refute_0_36,plain,
( arboreal(X_239)
| definitionFOFtoCNF_0(X_239,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165)) ),
inference(subst,[],[refute_0_35:[bind(X_238,$fot(X_239))]]) ).
cnf(refute_0_37,plain,
( arboreal(X_239)
| min_precedes(X_239,skolemFOFtoCNF_X168(X_239),tptp0) ),
inference(resolve,[$cnf( definitionFOFtoCNF_0(X_239,skolemFOFtoCNF_X164(skolemFOFtoCNF_X165)) )],[refute_0_36,refute_0_29]) ).
cnf(refute_0_38,plain,
( arboreal(X_250)
| min_precedes(X_250,skolemFOFtoCNF_X168(X_250),tptp0) ),
inference(subst,[],[refute_0_37:[bind(X_239,$fot(X_250))]]) ).
cnf(refute_0_39,plain,
arboreal(X_250),
inference(resolve,[$cnf( min_precedes(X_250,skolemFOFtoCNF_X168(X_250),tptp0) )],[refute_0_38,refute_0_27]) ).
cnf(refute_0_40,plain,
arboreal(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))),
inference(subst,[],[refute_0_39:[bind(X_250,$fot(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))))]]) ).
cnf(refute_0_41,plain,
$false,
inference(resolve,[$cnf( arboreal(skolemFOFtoCNF_X147(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X104(skolemFOFtoCNF_X164(skolemFOFtoCNF_X165),skolemFOFtoCNF_X165))) )],[refute_0_40,refute_0_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : PRO011+3 : TPTP v8.1.0. Released v4.0.0.
% 0.13/0.14 % Command : metis --show proof --show saturation %s
% 0.13/0.35 % Computer : n025.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Mon Jun 13 02:20:23 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 3.48/3.72 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/3.72
% 3.48/3.72 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 3.48/3.72
%------------------------------------------------------------------------------