%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO002+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Sun Sep 27 08:20:52 AM UTC 2026
% Result : Theorem 6.45s 1.27s
% Output : CNFRefutation 6.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 24
% Syntax : Number of formulae : 181 ( 43 unt; 0 def)
% Number of atoms : 509 ( 53 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 537 ( 209 ~; 221 |; 84 &)
% ( 4 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-4 aty)
% Number of variables : 352 ( 35 sgn 141 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_02,axiom,
! [X7,X8,X9,X10] :
( ( root_occ(X8,X9)
& root_occ(X7,X9)
& occurrence_of(X9,X10) )
=> X7 = X8 ),
file('theBenchmark.p',sos_02) ).
fof(sos_04,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('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [X19,X20,X21] :
( next_subocc(X19,X20,X21)
=> ( arboreal(X20)
& arboreal(X19) ) ),
file('theBenchmark.p',sos_05) ).
fof(sos_07,axiom,
! [X25,X26,X27] :
( min_precedes(X25,X26,X27)
=> ~ root(X26,X27) ),
file('theBenchmark.p',sos_07) ).
fof(sos_10,axiom,
! [X32,X33] :
( root_occ(X32,X33)
<=> ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) ) ),
file('theBenchmark.p',sos_10) ).
fof(sos_11,axiom,
! [X35,X36] :
( leaf_occ(X35,X36)
<=> ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) ) ),
file('theBenchmark.p',sos_11) ).
fof(sos_12,axiom,
! [X38,X39] :
( root(X38,X39)
=> legal(X38) ),
file('theBenchmark.p',sos_12) ).
fof(sos_15,axiom,
! [X46,X47] :
( atocc(X46,X47)
<=> ? [X48] :
( occurrence_of(X46,X48)
& atomic(X48)
& subactivity(X47,X48) ) ),
file('theBenchmark.p',sos_15) ).
fof(sos_17,axiom,
! [X51] :
( legal(X51)
=> arboreal(X51) ),
file('theBenchmark.p',sos_17) ).
fof(sos_18,axiom,
! [X52] :
( activity_occurrence(X52)
=> ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) ) ),
file('theBenchmark.p',sos_18) ).
fof(sos_19,axiom,
! [X54,X55] :
( subactivity_occurrence(X54,X55)
=> ( activity_occurrence(X55)
& activity_occurrence(X54) ) ),
file('theBenchmark.p',sos_19) ).
fof(sos_20,axiom,
! [X56,X57,X58] :
( ( root_occ(X57,X56)
& occurrence_of(X56,X58) )
=> ~ ? [X59] : min_precedes(X59,X57,X58) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X60,X61,X62] :
( ( leaf_occ(X61,X60)
& occurrence_of(X60,X62) )
=> ~ ? [X63] : min_precedes(X61,X63,X62) ),
file('theBenchmark.p',sos_21) ).
fof(sos_22,axiom,
! [X64,X65,X66] :
( ( occurrence_of(X64,X66)
& occurrence_of(X64,X65) )
=> X65 = X66 ),
file('theBenchmark.p',sos_22) ).
fof(sos_24,axiom,
! [X70,X71,X72] :
( min_precedes(X71,X72,X70)
=> ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) ) ),
file('theBenchmark.p',sos_24) ).
fof(sos_27,axiom,
! [X82,X83] :
( root(X83,X82)
=> ? [X84] :
( atocc(X83,X84)
& subactivity(X84,X82) ) ),
file('theBenchmark.p',sos_27) ).
fof(sos_28,axiom,
! [X85,X86,X87,X88] :
( ( subactivity_occurrence(X88,X86)
& subactivity_occurrence(X87,X86)
& arboreal(X88)
& arboreal(X87)
& occurrence_of(X86,X85) )
=> ( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85) ) ),
file('theBenchmark.p',sos_28) ).
fof(sos_30,axiom,
! [X91,X92] :
( ( ~ atomic(X91)
& occurrence_of(X92,X91) )
=> ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) ) ),
file('theBenchmark.p',sos_30) ).
fof(sos_32,axiom,
! [X95] :
( occurrence_of(X95,tptp0)
=> ? [X96,X97] :
( next_subocc(X96,X97,tptp0)
& leaf_occ(X97,X95)
& ( occurrence_of(X97,tptp2)
| occurrence_of(X97,tptp3) )
& root_occ(X96,X95)
& occurrence_of(X96,tptp4) ) ),
file('theBenchmark.p',sos_32) ).
fof(sos_46,axiom,
! [X103,X104,X105,X106,X107] :
( send_message(X103,X104,X105,X106,X107)
=> ( X103 != tptp2
& X103 != tptp3
& X103 != tptp4 ) ),
file('theBenchmark.p',sos_46) ).
fof(sos_47,axiom,
! [X108,X109,X110,X111,X112,X113] :
( ( occurrence_of(X113,X108)
& send_message(X108,X109,X110,X111,X112) )
=> min_precedes(X111,X113,X112) ),
file('theBenchmark.p',sos_47) ).
fof(sos_48,axiom,
! [X114,X115,X116] :
( tptp1(X114,X115,X116)
=> ( root(X116,X115)
& ~ atomic(X115)
& ~ atomic(X114)
& activity(X114) ) ),
file('theBenchmark.p',sos_48) ).
fof(sos_49,axiom,
! [X117,X118,X119,X120] :
( ( occurrence_of(X120,X117)
& tptp1(X117,X118,X119) )
=> ? [X121,X122,X123,X124] :
( root_occ(X124,X120)
& occurrence_of(X124,X121)
& send_message(X121,X122,X123,X119,X118) ) ),
file('theBenchmark.p',sos_49) ).
fof(goals,conjecture,
~ ? [X127,X128,X129] :
( occurrence_of(X129,X127)
& tptp1(X127,tptp0,X128) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ~ ? [X127,X128,X129] :
( occurrence_of(X129,X127)
& tptp1(X127,tptp0,X128) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_42,plain,
( ~ min_precedes(D,B,C)
| ~ min_precedes(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_04]) ).
cnf(c_45,plain,
( arboreal(A)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_05]) ).
cnf(c_46,plain,
( arboreal(B)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_05]) ).
fof(nnf_33,plain,
! [X95] :
( ? [X96,X97] :
( next_subocc(X96,X97,tptp0)
& leaf_occ(X97,X95)
& ( occurrence_of(X97,tptp2)
| occurrence_of(X97,tptp3) )
& root_occ(X96,X95)
& occurrence_of(X96,tptp4) )
| ~ occurrence_of(X95,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(sk_sos_32_sk,plain,
! [X95] :
( ( next_subocc(sK0(X95),sK1(X95),tptp0)
& leaf_occ(sK1(X95),X95)
& ( occurrence_of(sK1(X95),tptp2)
| occurrence_of(sK1(X95),tptp3) )
& root_occ(sK0(X95),X95)
& occurrence_of(sK0(X95),tptp4) )
| ~ occurrence_of(X95,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X96,sK0(X95)),skolemize(X97,sK1(X95))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0] :
( next_subocc(sK0(VAR_0),sK1(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK1(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK1(VAR_0),tptp2)
| occurrence_of(sK1(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK0(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK0(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_32_sk]) ).
cnf(c_47,plain,
( next_subocc(sK0(A),sK1(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_53,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_07]) ).
cnf(c_54,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_55,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_12]) ).
fof(nnf_28,plain,
! [X82,X83] :
( ? [X84] :
( atocc(X83,X84)
& subactivity(X84,X82) )
| ~ root(X83,X82) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(sk_sos_27_sk,plain,
! [X82,X83] :
( ( atocc(X83,sK2(X82,X83))
& subactivity(sK2(X82,X83),X82) )
| ~ root(X83,X82) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X84,sK2(X82,X83))],[nnf_28]) ).
fof(sk_sos_27,plain,
( ! [VAR_0,VAR_1] :
( atocc(VAR_0,sK2(VAR_1,VAR_0))
| ~ root(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity(sK2(VAR_1,VAR_0),VAR_1)
| ~ root(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_27_sk]) ).
cnf(c_60,plain,
( atocc(A,sK2(B,A))
| ~ root(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
fof(nnf_31,plain,
! [X91,X92] :
( ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) )
| atomic(X91)
| ~ occurrence_of(X92,X91) ),
inference(fof_nnf,[status(thm)],[sos_30]) ).
fof(sk_sos_30_sk,plain,
! [X91,X92] :
( ( subactivity_occurrence(sK3(X91,X92),X92)
& root(sK3(X91,X92),X91) )
| atomic(X91)
| ~ occurrence_of(X92,X91) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X93,sK3(X91,X92))],[nnf_31]) ).
fof(sk_sos_30,plain,
( ! [VAR_0,VAR_1] :
( subactivity_occurrence(sK3(VAR_1,VAR_0),VAR_0)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(sK3(VAR_1,VAR_0),VAR_1)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_30_sk]) ).
cnf(c_61,plain,
( root(sK3(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_30]) ).
cnf(c_64,plain,
( root(C,B)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_48]) ).
cnf(c_66,plain,
( legal(sK3(B,A))
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_61,c_55]) ).
cnf(c_69,plain,
( legal(C)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_64,c_55]) ).
cnf(c_76,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_17]) ).
fof(nnf_19,plain,
! [X52] :
( ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) )
| ~ activity_occurrence(X52) ),
inference(fof_nnf,[status(thm)],[sos_18]) ).
fof(sk_sos_18_sk,plain,
! [X52] :
( ( occurrence_of(X52,sK4(X52))
& activity(sK4(X52)) )
| ~ activity_occurrence(X52) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X53,sK4(X52))],[nnf_19]) ).
fof(sk_sos_18,plain,
( ! [VAR_0] :
( occurrence_of(VAR_0,sK4(VAR_0))
| ~ activity_occurrence(VAR_0) )
& ! [VAR_0] :
( activity(sK4(VAR_0))
| ~ activity_occurrence(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_18_sk]) ).
cnf(c_96,plain,
( occurrence_of(A,sK4(A))
| ~ activity_occurrence(A) ),
inference(split_conjunct,[status(thm)],[sk_sos_18]) ).
cnf(c_97,plain,
( activity_occurrence(A)
| ~ subactivity_occurrence(A,B) ),
inference(clausify,[status(thm)],[sos_19]) ).
fof(nnf_38,plain,
! [X117,X118,X119,X120] :
( ? [X121,X122,X123,X124] :
( root_occ(X124,X120)
& occurrence_of(X124,X121)
& send_message(X121,X122,X123,X119,X118) )
| ~ occurrence_of(X120,X117)
| ~ tptp1(X117,X118,X119) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(sk_sos_49_sk,plain,
! [X117,X118,X119,X120] :
( ( root_occ(sK10(X117,X118,X119,X120),X120)
& occurrence_of(sK10(X117,X118,X119,X120),sK5(X117,X118,X119,X120))
& send_message(sK5(X117,X118,X119,X120),sK6(X117,X118,X119,X120),sK7(X117,X118,X119,X120),X119,X118) )
| ~ occurrence_of(X120,X117)
| ~ tptp1(X117,X118,X119) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK10]),skolemize(X121,sK5(X117,X118,X119,X120)),skolemize(X122,sK6(X117,X118,X119,X120)),skolemize(X123,sK7(X117,X118,X119,X120)),skolemize(X124,sK10(X117,X118,X119,X120))],[nnf_38]) ).
fof(sk_sos_49,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( root_occ(sK10(VAR_0,VAR_1,VAR_2,VAR_3),VAR_3)
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( occurrence_of(sK10(VAR_0,VAR_1,VAR_2,VAR_3),sK5(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( send_message(sK5(VAR_0,VAR_1,VAR_2,VAR_3),sK6(VAR_0,VAR_1,VAR_2,VAR_3),sK7(VAR_0,VAR_1,VAR_2,VAR_3),VAR_2,VAR_1)
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_109,plain,
( send_message(sK5(A,B,C,D),sK6(A,B,C,D),sK7(A,B,C,D),C,B)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_123,plain,
( min_precedes(D,F,E)
| ~ occurrence_of(F,A)
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_47]) ).
cnf(c_124,plain,
( A != tptp2
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_46]) ).
cnf(c_125,plain,
( A != tptp3
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_46]) ).
cnf(c_144,plain,
( ~ occurrence_of(D,A)
| ~ tptp1(A,B,C)
| sK5(A,B,C,D) != tptp3 ),
inference(resolve,[status(thm)],[c_125,c_109]) ).
cnf(c_145,plain,
( ~ occurrence_of(D,A)
| ~ tptp1(A,B,C)
| sK5(A,B,C,D) != tptp2 ),
inference(resolve,[status(thm)],[c_124,c_109]) ).
cnf(c_146,plain,
( ~ occurrence_of(E,B)
| ~ tptp1(B,C,D)
| min_precedes(D,A,C)
| ~ occurrence_of(A,sK5(B,C,D,E)) ),
inference(resolve,[status(thm)],[c_123,c_109]) ).
cnf(c_161,plain,
( ~ subactivity_occurrence(A,B)
| occurrence_of(A,sK4(A)) ),
inference(resolve,[status(thm)],[c_96,c_97]) ).
cnf(c_167,plain,
( ~ tptp1(B,C,A)
| arboreal(A) ),
inference(resolve,[status(thm)],[c_76,c_69]) ).
cnf(c_168,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| arboreal(sK3(A,B)) ),
inference(resolve,[status(thm)],[c_76,c_66]) ).
cnf(c_190,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_194,plain,
( subactivity_occurrence(A,B)
| ~ root_occ(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_196,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_11]) ).
fof(nnf_16,plain,
! [X46,X47] :
( ( ! [X48] :
( ~ occurrence_of(X46,X48)
| ~ atomic(X48)
| ~ subactivity(X47,X48) )
| atocc(X46,X47) )
& ( ? [X130] :
( occurrence_of(X46,X130)
& atomic(X130)
& subactivity(X47,X130) )
| ~ atocc(X46,X47) ) ),
inference(fof_nnf,[status(thm)],[sos_15]) ).
fof(sk_sos_15_sk,plain,
! [X46,X47] :
( ( ! [X48] :
( ~ occurrence_of(X46,X48)
| ~ atomic(X48)
| ~ subactivity(X47,X48) )
| atocc(X46,X47) )
& ( ( occurrence_of(X46,sK8(X46,X47))
& atomic(sK8(X46,X47))
& subactivity(X47,sK8(X46,X47)) )
| ~ atocc(X46,X47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X130,sK8(X46,X47))],[nnf_16]) ).
fof(sk_sos_15,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ occurrence_of(VAR_0,VAR_2)
| ~ atomic(VAR_2)
| ~ subactivity(VAR_1,VAR_2)
| atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_0,sK8(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( atomic(sK8(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity(VAR_1,sK8(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_15_sk]) ).
cnf(c_204,plain,
( occurrence_of(A,sK8(A,B))
| ~ atocc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_15]) ).
cnf(c_205,plain,
( ~ min_precedes(D,C,B)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_20]) ).
cnf(c_206,plain,
( ~ min_precedes(C,D,B)
| ~ leaf_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_207,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_22]) ).
fof(nnf_25,plain,
! [X70,X71,X72] :
( ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) )
| ~ min_precedes(X71,X72,X70) ),
inference(fof_nnf,[status(thm)],[sos_24]) ).
fof(sk_sos_24_sk,plain,
! [X70,X71,X72] :
( ( subactivity_occurrence(X72,sK9(X70,X71,X72))
& subactivity_occurrence(X71,sK9(X70,X71,X72))
& occurrence_of(sK9(X70,X71,X72),X70) )
| ~ min_precedes(X71,X72,X70) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X73,sK9(X70,X71,X72))],[nnf_25]) ).
fof(sk_sos_24,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK9(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK9(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK9(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ min_precedes(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_24_sk]) ).
cnf(c_210,plain,
( occurrence_of(sK9(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_24]) ).
cnf(c_211,plain,
( subactivity_occurrence(A,sK9(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_24]) ).
cnf(c_212,plain,
( subactivity_occurrence(B,sK9(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_24]) ).
cnf(c_217,plain,
( D = C
| min_precedes(D,C,B)
| min_precedes(C,D,B)
| ~ subactivity_occurrence(D,A)
| ~ subactivity_occurrence(C,A)
| ~ arboreal(D)
| ~ arboreal(C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_28]) ).
cnf(c_218,plain,
( subactivity_occurrence(sK3(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_30]) ).
cnf(c_220,plain,
( root_occ(sK0(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_221,plain,
( occurrence_of(sK1(A),tptp2)
| occurrence_of(sK1(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_222,plain,
( leaf_occ(sK1(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_235,plain,
( ~ atomic(A)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_48]) ).
cnf(c_237,plain,
( occurrence_of(sK10(A,B,C,D),sK5(A,B,C,D))
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_238,plain,
( root_occ(sK10(A,B,C,D),D)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
fof(nnf_40,plain,
? [X127,X128,X129] :
( occurrence_of(X129,X127)
& tptp1(X127,tptp0,X128) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( occurrence_of(sK13,sK11)
& tptp1(sK11,tptp0,sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X127,sK11),skolemize(X128,sK12),skolemize(X129,sK13)],[nnf_40]) ).
cnf(c_240,negated_conjecture,
tptp1(sK11,tptp0,sK12),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_241,negated_conjecture,
occurrence_of(sK13,sK11),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_246,plain,
( arboreal(sK1(A))
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_47,c_46]) ).
cnf(c_247,plain,
( arboreal(sK0(A))
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_248,plain,
( ~ min_precedes(B,sK1(A),tptp0)
| ~ min_precedes(sK0(A),B,tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_47,c_42]) ).
cnf(c_257,plain,
( atocc(sK3(B,A),sK2(B,sK3(B,A)))
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_61,c_60]) ).
cnf(c_259,plain,
( ~ subactivity_occurrence(sK3(B,A),C)
| ~ occurrence_of(C,B)
| root_occ(sK3(B,A),C)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_61,c_54]) ).
cnf(c_264,plain,
( ~ min_precedes(D,C,B)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_64,c_53]) ).
cnf(c_286,plain,
( ~ subactivity_occurrence(sK3(B,A),A)
| root_occ(sK3(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(factor,[status(thm)],[c_259]) ).
cnf(c_308,plain,
( root_occ(sK10(sK11,tptp0,sK12,A),A)
| ~ occurrence_of(A,sK11) ),
inference(resolve,[status(thm)],[c_240,c_238]) ).
cnf(c_309,plain,
( occurrence_of(sK10(sK11,tptp0,sK12,A),sK5(sK11,tptp0,sK12,A))
| ~ occurrence_of(A,sK11) ),
inference(resolve,[status(thm)],[c_240,c_237]) ).
cnf(c_310,plain,
~ atomic(sK11),
inference(resolve,[status(thm)],[c_240,c_235]) ).
cnf(c_314,plain,
arboreal(sK12),
inference(resolve,[status(thm)],[c_240,c_167]) ).
cnf(c_321,plain,
( ~ occurrence_of(B,sK11)
| min_precedes(sK12,A,tptp0)
| ~ occurrence_of(A,sK5(sK11,tptp0,sK12,B)) ),
inference(resolve,[status(thm)],[c_240,c_146]) ).
cnf(c_322,plain,
( ~ occurrence_of(A,sK11)
| sK5(sK11,tptp0,sK12,A) != tptp2 ),
inference(resolve,[status(thm)],[c_240,c_145]) ).
cnf(c_323,plain,
( ~ occurrence_of(A,sK11)
| sK5(sK11,tptp0,sK12,A) != tptp3 ),
inference(resolve,[status(thm)],[c_240,c_144]) ).
cnf(c_5382,negated_conjecture,
( subactivity_occurrence(sK3(sK11,sK13),sK13)
| atomic(sK11) ),
inference(resolve,[status(thm)],[c_241,c_218]) ).
cnf(c_333,negated_conjecture,
subactivity_occurrence(sK3(sK11,sK13),sK13),
inference(resolve,[status(thm)],[c_310,c_5382]) ).
cnf(c_341,plain,
( B = A
| ~ root_occ(B,sK13)
| ~ root_occ(A,sK13) ),
inference(resolve,[status(thm)],[c_241,c_190]) ).
cnf(c_5383,negated_conjecture,
( atomic(sK11)
| arboreal(sK3(sK11,sK13)) ),
inference(resolve,[status(thm)],[c_241,c_168]) ).
cnf(c_349,negated_conjecture,
arboreal(sK3(sK11,sK13)),
inference(resolve,[status(thm)],[c_310,c_5383]) ).
cnf(c_5384,negated_conjecture,
( atocc(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13)))
| atomic(sK11) ),
inference(resolve,[status(thm)],[c_257,c_241]) ).
cnf(c_369,negated_conjecture,
atocc(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_310,c_5384]) ).
cnf(c_378,plain,
~ min_precedes(A,sK12,tptp0),
inference(resolve,[status(thm)],[c_264,c_240]) ).
cnf(c_5385,negated_conjecture,
( ~ subactivity_occurrence(sK3(sK11,sK13),sK13)
| root_occ(sK3(sK11,sK13),sK13)
| atomic(sK11) ),
inference(resolve,[status(thm)],[c_286,c_241]) ).
cnf(c_5386,negated_conjecture,
( ~ subactivity_occurrence(sK3(sK11,sK13),sK13)
| root_occ(sK3(sK11,sK13),sK13) ),
inference(resolve,[status(thm)],[c_310,c_5385]) ).
cnf(c_414,negated_conjecture,
root_occ(sK3(sK11,sK13),sK13),
inference(resolve,[status(thm)],[c_333,c_5386]) ).
cnf(c_421,plain,
( sK12 = C
| min_precedes(sK12,C,B)
| min_precedes(C,sK12,B)
| ~ subactivity_occurrence(sK12,A)
| ~ subactivity_occurrence(C,A)
| ~ arboreal(C)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_314,c_217]) ).
cnf(c_429,plain,
root_occ(sK10(sK11,tptp0,sK12,sK13),sK13),
inference(resolve,[status(thm)],[c_308,c_241]) ).
cnf(c_430,plain,
occurrence_of(sK10(sK11,tptp0,sK12,sK13),sK5(sK11,tptp0,sK12,sK13)),
inference(resolve,[status(thm)],[c_309,c_241]) ).
cnf(c_431,plain,
sK5(sK11,tptp0,sK12,sK13) != tptp2,
inference(resolve,[status(thm)],[c_322,c_241]) ).
cnf(c_432,plain,
( sK3(sK11,sK13) = C
| min_precedes(sK3(sK11,sK13),C,B)
| min_precedes(C,sK3(sK11,sK13),B)
| ~ subactivity_occurrence(sK3(sK11,sK13),A)
| ~ subactivity_occurrence(C,A)
| ~ arboreal(C)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_349,c_217]) ).
cnf(c_437,plain,
sK5(sK11,tptp0,sK12,sK13) != tptp3,
inference(resolve,[status(thm)],[c_323,c_241]) ).
cnf(c_442,plain,
occurrence_of(sK3(sK11,sK13),sK4(sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_333,c_161]) ).
cnf(c_455,plain,
( sK3(sK11,sK13) = A
| ~ root_occ(A,sK13) ),
inference(resolve,[status(thm)],[c_414,c_341]) ).
cnf(c_5387,plain,
sK3(sK11,sK13) = sK10(sK11,tptp0,sK12,sK13),
inference(resolve,[status(thm)],[c_455,c_429]) ).
cnf(c_490,plain,
sK10(sK11,tptp0,sK12,sK13) = sK3(sK11,sK13),
inference(copy,[status(thm)],[c_5387]) ).
cnf(c_491,plain,
occurrence_of(sK3(sK11,sK13),sK5(sK11,tptp0,sK12,sK13)),
inference(paramod,[status(thm)],[c_490,c_430]) ).
cnf(c_5388,plain,
( ~ occurrence_of(sK13,sK11)
| min_precedes(sK12,sK3(sK11,sK13),tptp0) ),
inference(resolve,[status(thm)],[c_491,c_321]) ).
cnf(c_550,negated_conjecture,
min_precedes(sK12,sK3(sK11,sK13),tptp0),
inference(resolve,[status(thm)],[c_241,c_5388]) ).
cnf(c_564,plain,
( sK5(sK11,tptp0,sK12,sK13) = A
| ~ occurrence_of(sK3(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_491,c_207]) ).
cnf(c_589,plain,
subactivity_occurrence(sK3(sK11,sK13),sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_550,c_212]) ).
cnf(c_590,plain,
subactivity_occurrence(sK12,sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_550,c_211]) ).
cnf(c_591,plain,
occurrence_of(sK9(tptp0,sK12,sK3(sK11,sK13)),tptp0),
inference(resolve,[status(thm)],[c_550,c_210]) ).
cnf(c_786,plain,
occurrence_of(sK3(sK11,sK13),sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13)))),
inference(resolve,[status(thm)],[c_369,c_204]) ).
cnf(c_847,plain,
sK5(sK11,tptp0,sK12,sK13) = sK4(sK3(sK11,sK13)),
inference(resolve,[status(thm)],[c_442,c_564]) ).
cnf(c_875,plain,
( sK4(sK3(sK11,sK13)) = A
| ~ occurrence_of(sK3(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_442,c_207]) ).
cnf(c_927,plain,
sK4(sK3(sK11,sK13)) != tptp3,
inference(paramod,[status(thm)],[c_847,c_437]) ).
cnf(c_928,plain,
sK4(sK3(sK11,sK13)) != tptp2,
inference(paramod,[status(thm)],[c_847,c_431]) ).
cnf(c_963,plain,
( ~ min_precedes(A,sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| ~ min_precedes(sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),A,tptp0) ),
inference(resolve,[status(thm)],[c_591,c_248]) ).
cnf(c_964,plain,
arboreal(sK0(sK9(tptp0,sK12,sK3(sK11,sK13)))),
inference(resolve,[status(thm)],[c_591,c_247]) ).
cnf(c_965,plain,
arboreal(sK1(sK9(tptp0,sK12,sK3(sK11,sK13)))),
inference(resolve,[status(thm)],[c_591,c_246]) ).
cnf(c_966,plain,
leaf_occ(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_591,c_222]) ).
cnf(c_967,plain,
( occurrence_of(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp2)
| occurrence_of(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp3) ),
inference(resolve,[status(thm)],[c_591,c_221]) ).
cnf(c_968,plain,
root_occ(sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_591,c_220]) ).
cnf(c_973,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_591,c_206]) ).
cnf(c_974,plain,
( ~ min_precedes(B,A,tptp0)
| ~ root_occ(A,sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_591,c_205]) ).
cnf(c_5389,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| min_precedes(A,sK12,tptp0)
| ~ subactivity_occurrence(sK12,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ subactivity_occurrence(A,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_421,c_591]) ).
cnf(c_5390,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| min_precedes(A,sK12,tptp0)
| ~ subactivity_occurrence(A,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_590,c_5389]) ).
cnf(c_1222,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| ~ subactivity_occurrence(A,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_378,c_5390]) ).
cnf(c_5391,plain,
( sK3(sK11,sK13) = A
| min_precedes(sK3(sK11,sK13),A,tptp0)
| min_precedes(A,sK3(sK11,sK13),tptp0)
| ~ subactivity_occurrence(sK3(sK11,sK13),sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ subactivity_occurrence(A,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_432,c_591]) ).
cnf(c_1263,plain,
( sK3(sK11,sK13) = A
| min_precedes(sK3(sK11,sK13),A,tptp0)
| min_precedes(A,sK3(sK11,sK13),tptp0)
| ~ subactivity_occurrence(A,sK9(tptp0,sK12,sK3(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_589,c_5391]) ).
cnf(c_2477,plain,
sK4(sK3(sK11,sK13)) = sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_786,c_875]) ).
cnf(c_2533,plain,
sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))) != tptp2,
inference(paramod,[status(thm)],[c_2477,c_928]) ).
cnf(c_2534,plain,
sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))) != tptp3,
inference(paramod,[status(thm)],[c_2477,c_927]) ).
cnf(c_5392,plain,
( sK12 = sK0(sK9(tptp0,sK12,sK3(sK11,sK13)))
| min_precedes(sK12,sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| ~ subactivity_occurrence(sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_1222,c_964]) ).
cnf(c_2560,plain,
( sK0(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK12
| min_precedes(sK12,sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| ~ subactivity_occurrence(sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(copy,[status(thm)],[c_5392]) ).
cnf(c_3106,plain,
~ min_precedes(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),A,tptp0),
inference(resolve,[status(thm)],[c_966,c_973]) ).
cnf(c_3109,plain,
subactivity_occurrence(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_966,c_196]) ).
cnf(c_3121,plain,
~ min_precedes(A,sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0),
inference(resolve,[status(thm)],[c_968,c_974]) ).
cnf(c_3137,plain,
subactivity_occurrence(sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_968,c_194]) ).
cnf(c_5393,plain,
( sK0(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK12
| min_precedes(sK12,sK0(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0) ),
inference(resolve,[status(thm)],[c_3137,c_2560]) ).
cnf(c_3143,plain,
sK0(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK12,
inference(resolve,[status(thm)],[c_3121,c_5393]) ).
cnf(c_3207,plain,
( ~ min_precedes(A,sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| ~ min_precedes(sK12,A,tptp0) ),
inference(paramod,[status(thm)],[c_3143,c_963]) ).
cnf(c_3344,plain,
( tptp3 = A
| ~ occurrence_of(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),A)
| occurrence_of(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp2) ),
inference(resolve,[status(thm)],[c_967,c_207]) ).
cnf(c_3378,plain,
~ min_precedes(sK3(sK11,sK13),sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0),
inference(resolve,[status(thm)],[c_3207,c_550]) ).
cnf(c_5394,plain,
( sK3(sK11,sK13) = sK1(sK9(tptp0,sK12,sK3(sK11,sK13)))
| min_precedes(sK3(sK11,sK13),sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| min_precedes(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK3(sK11,sK13),tptp0)
| ~ subactivity_occurrence(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_1263,c_965]) ).
cnf(c_5395,plain,
( sK1(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK3(sK11,sK13)
| min_precedes(sK3(sK11,sK13),sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| min_precedes(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK3(sK11,sK13),tptp0)
| ~ subactivity_occurrence(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK9(tptp0,sK12,sK3(sK11,sK13))) ),
inference(copy,[status(thm)],[c_5394]) ).
cnf(c_5396,plain,
( sK1(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK3(sK11,sK13)
| min_precedes(sK3(sK11,sK13),sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0)
| min_precedes(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),sK3(sK11,sK13),tptp0) ),
inference(resolve,[status(thm)],[c_3109,c_5395]) ).
cnf(c_5397,plain,
( sK1(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK3(sK11,sK13)
| min_precedes(sK3(sK11,sK13),sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),tptp0) ),
inference(resolve,[status(thm)],[c_3106,c_5396]) ).
cnf(c_4995,plain,
sK1(sK9(tptp0,sK12,sK3(sK11,sK13))) = sK3(sK11,sK13),
inference(resolve,[status(thm)],[c_3378,c_5397]) ).
cnf(c_5398,plain,
( tptp3 = A
| ~ occurrence_of(sK1(sK9(tptp0,sK12,sK3(sK11,sK13))),A)
| occurrence_of(sK3(sK11,sK13),tptp2) ),
inference(paramod,[status(thm)],[c_4995,c_3344]) ).
cnf(c_5020,plain,
( tptp3 = A
| ~ occurrence_of(sK3(sK11,sK13),A)
| occurrence_of(sK3(sK11,sK13),tptp2) ),
inference(paramod,[status(thm)],[c_4995,c_5398]) ).
cnf(c_5399,plain,
( tptp3 = sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13)))
| occurrence_of(sK3(sK11,sK13),tptp2) ),
inference(resolve,[status(thm)],[c_5020,c_786]) ).
cnf(c_5400,plain,
( sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))) = tptp3
| occurrence_of(sK3(sK11,sK13),tptp2) ),
inference(copy,[status(thm)],[c_5399]) ).
cnf(c_5320,plain,
occurrence_of(sK3(sK11,sK13),tptp2),
inference(resolve,[status(thm)],[c_2534,c_5400]) ).
cnf(c_5357,plain,
( tptp2 = A
| ~ occurrence_of(sK3(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_5320,c_207]) ).
cnf(c_5401,plain,
tptp2 = sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))),
inference(resolve,[status(thm)],[c_5357,c_786]) ).
cnf(c_5402,plain,
sK8(sK3(sK11,sK13),sK2(sK11,sK3(sK11,sK13))) = tptp2,
inference(copy,[status(thm)],[c_5401]) ).
cnf(c_5381,plain,
$false,
inference(resolve,[status(thm)],[c_2533,c_5402]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO002+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n007.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sat Sep 26 04:52:23 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.36 % Process 2820735 was started by sandbox2 on n007,
% 0.11/0.36 % Sat Sep 26 04:52:23 2026
% 0.11/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 6.45/1.27
% 6.45/1.27 % given #500 (T,wt=28): 1248 arboreal(f5(f14(c1,c3),c1)) | occurrence_of(c3,f3(f14(c1,c3),c3)). [resolve(1234,b,195,a)].
% 6.45/1.27
% 6.45/1.27 % given #1000 (A,wt=47): 1078 atocc(A,f13(f12(tptp0,c2,f14(c1,c3)),f14(c1,c3))) | -atomic(f12(tptp0,c2,f14(c1,c3))) | -occurrence_of(A,f12(tptp0,c2,f14(c1,c3))). [resolve(587,a,383,d)].
% 6.45/1.27
% 6.45/1.27 % SZS status Theorem for theBenchmark
% 6.45/1.27
% 6.45/1.27 % Proof 1 at 0.71 (+ 0.14) seconds.
% 6.45/1.27 % Length of proof is 136.
% 6.45/1.27 % Level of proof is 19.
% 6.45/1.27 % Maximum clause weight is 53.000.
% 6.45/1.27 % Given clauses 1226.
% 6.45/1.27
% 6.45/1.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------