%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU376+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:46:08 AM UTC 2026
% Result : Theorem 0.22s 10.99s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 78 ( 15 unt; 0 def)
% Number of atoms : 474 ( 0 equ)
% Maximal formula atoms : 35 ( 6 avg)
% Number of connectives : 639 ( 243 ~; 304 |; 71 &)
% ( 3 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-4 aty)
% Number of variables : 200 ( 0 sgn 98 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d11_waybel_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( is_eventually_in(A,B,C)
<=> ? [D] :
( ! [E] :
( element(E,the_carrier(B))
=> ( related(B,D,E)
=> in(apply_netmap(A,B,E),C) ) )
& element(D,the_carrier(B)) ) ) ) ),
file('theBenchmark.p',d11_waybel_0) ).
fof(d12_waybel_0,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( is_often_in(A,B,C)
<=> ! [D] :
( element(D,the_carrier(B))
=> ? [E] :
( in(apply_netmap(A,B,E),C)
& related(B,D,E)
& element(E,the_carrier(B)) ) ) ) ) ),
file('theBenchmark.p',d12_waybel_0) ).
fof(d5_yellow_6,axiom,
! [A] :
( ( rel_str(A)
& ~ empty_carrier(A) )
=> ( directed_relstr(A)
<=> ! [B] :
( element(B,the_carrier(A))
=> ! [C] :
( element(C,the_carrier(A))
=> ? [D] :
( related(A,C,D)
& related(A,B,D)
& element(D,the_carrier(A)) ) ) ) ) ),
file('theBenchmark.p',d5_yellow_6) ).
fof(dt_l1_waybel_0,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('theBenchmark.p',dt_l1_waybel_0) ).
fof(t28_yellow_6,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( is_eventually_in(A,B,C)
=> is_often_in(A,B,C) ) ) ),
file('theBenchmark.p',t28_yellow_6) ).
fof(t28_yellow_6_neg,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
=> ! [C] :
( is_eventually_in(A,B,C)
=> is_often_in(A,B,C) ) ) ),
inference(assume_negation,[status(cth)],[t28_yellow_6]) ).
cnf(c_87,plain,
( rel_str(B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(clausify,[status(thm)],[dt_l1_waybel_0]) ).
fof(nnf_10,plain,
! [A] :
( ( ( ? [B] :
( ? [C] :
( ! [D] :
( ~ related(A,C,D)
| ~ related(A,B,D)
| ~ element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
& element(B,the_carrier(A)) )
| directed_relstr(A) )
& ( ! [X0] :
( ! [X1] :
( ? [X2] :
( related(A,X1,X2)
& related(A,X0,X2)
& element(X2,the_carrier(A)) )
| ~ element(X1,the_carrier(A)) )
| ~ element(X0,the_carrier(A)) )
| ~ directed_relstr(A) ) )
| ~ rel_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d5_yellow_6]) ).
fof(sk_d5_yellow_6_sk,plain,
! [A] :
( ( ( ( ! [D] :
( ~ related(A,sK7(A),D)
| ~ related(A,sK6(A),D)
| ~ element(D,the_carrier(A)) )
& element(sK7(A),the_carrier(A))
& element(sK6(A),the_carrier(A)) )
| directed_relstr(A) )
& ( ! [X0] :
( ! [X1] :
( ( related(A,X1,sK0(A,X0,X1))
& related(A,X0,sK0(A,X0,X1))
& element(sK0(A,X0,X1),the_carrier(A)) )
| ~ element(X1,the_carrier(A)) )
| ~ element(X0,the_carrier(A)) )
| ~ directed_relstr(A) ) )
| ~ rel_str(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK6,sK7]),skolemize(X2,sK0(A,X0,X1)),skolemize(B,sK6(A)),skolemize(C,sK7(A))],[nnf_10]) ).
fof(sk_d5_yellow_6,plain,
( ! [VAR_0,VAR_1] :
( ~ related(VAR_0,sK7(VAR_0),VAR_1)
| ~ related(VAR_0,sK6(VAR_0),VAR_1)
| ~ element(VAR_1,the_carrier(VAR_0))
| directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0] :
( element(sK7(VAR_0),the_carrier(VAR_0))
| directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0] :
( element(sK6(VAR_0),the_carrier(VAR_0))
| directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( related(VAR_0,VAR_2,sK0(VAR_0,VAR_1,VAR_2))
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( related(VAR_0,VAR_1,sK0(VAR_0,VAR_1,VAR_2))
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK0(VAR_0,VAR_1,VAR_2),the_carrier(VAR_0))
| ~ element(VAR_2,the_carrier(VAR_0))
| ~ element(VAR_1,the_carrier(VAR_0))
| ~ directed_relstr(VAR_0)
| ~ rel_str(VAR_0)
| empty_carrier(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d5_yellow_6_sk]) ).
cnf(c_92,plain,
( related(A,C,sK0(A,B,C))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ directed_relstr(A)
| ~ rel_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_yellow_6]) ).
cnf(c_93,plain,
( related(A,B,sK0(A,B,C))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ directed_relstr(A)
| ~ rel_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_yellow_6]) ).
cnf(c_94,plain,
( element(sK0(A,B,C),the_carrier(A))
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ directed_relstr(A)
| ~ rel_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d5_yellow_6]) ).
fof(nnf_61,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ is_often_in(A,B,C)
& is_eventually_in(A,B,C) )
& net_str(B,A)
& directed_relstr(B)
& transitive_relstr(B)
& ~ empty_carrier(B) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t28_yellow_6_neg]) ).
fof(sk_t28_yellow_6_neg,plain,
( ~ is_often_in(sK2,sK1,sK5)
& is_eventually_in(sK2,sK1,sK5)
& net_str(sK1,sK2)
& directed_relstr(sK1)
& transitive_relstr(sK1)
& ~ empty_carrier(sK1)
& one_sorted_str(sK2)
& ~ empty_carrier(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK1,sK5]),skolemize(A,sK2),skolemize(B,sK1),skolemize(C,sK5)],[nnf_61]) ).
cnf(c_98,negated_conjecture,
net_str(sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_106,plain,
( related(B,D,sK0(B,C,D))
| ~ element(D,the_carrier(B))
| ~ element(C,the_carrier(B))
| ~ directed_relstr(B)
| empty_carrier(B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(resolve,[status(thm)],[c_87,c_92]) ).
cnf(c_107,plain,
( related(B,C,sK0(B,C,D))
| ~ element(D,the_carrier(B))
| ~ element(C,the_carrier(B))
| ~ directed_relstr(B)
| empty_carrier(B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(resolve,[status(thm)],[c_87,c_93]) ).
cnf(c_108,plain,
( element(sK0(B,C,D),the_carrier(B))
| ~ element(D,the_carrier(B))
| ~ element(C,the_carrier(B))
| ~ directed_relstr(B)
| empty_carrier(B)
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(resolve,[status(thm)],[c_87,c_94]) ).
fof(nnf_9,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ? [D] :
( ! [E] :
( ~ in(apply_netmap(A,B,E),C)
| ~ related(B,D,E)
| ~ element(E,the_carrier(B)) )
& element(D,the_carrier(B)) )
| is_often_in(A,B,C) )
& ( ! [X0] :
( ? [X1] :
( in(apply_netmap(A,B,X1),C)
& related(B,X0,X1)
& element(X1,the_carrier(B)) )
| ~ element(X0,the_carrier(B)) )
| ~ is_often_in(A,B,C) ) )
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d12_waybel_0]) ).
fof(sk_d12_waybel_0_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ! [E] :
( ~ in(apply_netmap(A,B,E),C)
| ~ related(B,sK3(A,B,C),E)
| ~ element(E,the_carrier(B)) )
& element(sK3(A,B,C),the_carrier(B)) )
| is_often_in(A,B,C) )
& ( ! [X0] :
( ( in(apply_netmap(A,B,sK8(A,B,C,X0)),C)
& related(B,X0,sK8(A,B,C,X0))
& element(sK8(A,B,C,X0),the_carrier(B)) )
| ~ element(X0,the_carrier(B)) )
| ~ is_often_in(A,B,C) ) )
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK3]),skolemize(X1,sK8(A,B,C,X0)),skolemize(D,sK3(A,B,C))],[nnf_9]) ).
fof(sk_d12_waybel_0,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(apply_netmap(VAR_0,VAR_1,VAR_3),VAR_2)
| ~ related(VAR_1,sK3(VAR_0,VAR_1,VAR_2),VAR_3)
| ~ element(VAR_3,the_carrier(VAR_1))
| is_often_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK3(VAR_0,VAR_1,VAR_2),the_carrier(VAR_1))
| is_often_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( in(apply_netmap(VAR_0,VAR_1,sK8(VAR_0,VAR_1,VAR_2,VAR_3)),VAR_2)
| ~ element(VAR_3,the_carrier(VAR_1))
| ~ is_often_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_1,VAR_3,sK8(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ element(VAR_3,the_carrier(VAR_1))
| ~ is_often_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( element(sK8(VAR_0,VAR_1,VAR_2,VAR_3),the_carrier(VAR_1))
| ~ element(VAR_3,the_carrier(VAR_1))
| ~ is_often_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d12_waybel_0_sk]) ).
cnf(c_116,plain,
( ~ in(apply_netmap(A,B,D),C)
| ~ related(B,sK3(A,B,C),D)
| ~ element(D,the_carrier(B))
| is_often_in(A,B,C)
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d12_waybel_0]) ).
cnf(c_117,plain,
( element(sK3(A,B,C),the_carrier(B))
| is_often_in(A,B,C)
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d12_waybel_0]) ).
fof(nnf_8,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ! [D] :
( ? [E] :
( ~ in(apply_netmap(A,B,E),C)
& related(B,D,E)
& element(E,the_carrier(B)) )
| ~ element(D,the_carrier(B)) )
| is_eventually_in(A,B,C) )
& ( ? [X0] :
( ! [X1] :
( in(apply_netmap(A,B,X1),C)
| ~ related(B,X0,X1)
| ~ element(X1,the_carrier(B)) )
& element(X0,the_carrier(B)) )
| ~ is_eventually_in(A,B,C) ) )
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[d11_waybel_0]) ).
fof(sk_d11_waybel_0_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ! [D] :
( ( ~ in(apply_netmap(A,B,sK9(A,B,C,D)),C)
& related(B,D,sK9(A,B,C,D))
& element(sK9(A,B,C,D),the_carrier(B)) )
| ~ element(D,the_carrier(B)) )
| is_eventually_in(A,B,C) )
& ( ( ! [X1] :
( in(apply_netmap(A,B,X1),C)
| ~ related(B,sK4(A,B,C),X1)
| ~ element(X1,the_carrier(B)) )
& element(sK4(A,B,C),the_carrier(B)) )
| ~ is_eventually_in(A,B,C) ) )
| ~ net_str(B,A)
| empty_carrier(B) )
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK9]),skolemize(X0,sK4(A,B,C)),skolemize(E,sK9(A,B,C,D))],[nnf_8]) ).
fof(sk_d11_waybel_0,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ in(apply_netmap(VAR_0,VAR_1,sK9(VAR_0,VAR_1,VAR_2,VAR_3)),VAR_2)
| ~ element(VAR_3,the_carrier(VAR_1))
| is_eventually_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( related(VAR_1,VAR_3,sK9(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ element(VAR_3,the_carrier(VAR_1))
| is_eventually_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( element(sK9(VAR_0,VAR_1,VAR_2,VAR_3),the_carrier(VAR_1))
| ~ element(VAR_3,the_carrier(VAR_1))
| is_eventually_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( in(apply_netmap(VAR_0,VAR_1,VAR_3),VAR_2)
| ~ related(VAR_1,sK4(VAR_0,VAR_1,VAR_2),VAR_3)
| ~ element(VAR_3,the_carrier(VAR_1))
| ~ is_eventually_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( element(sK4(VAR_0,VAR_1,VAR_2),the_carrier(VAR_1))
| ~ is_eventually_in(VAR_0,VAR_1,VAR_2)
| ~ net_str(VAR_1,VAR_0)
| empty_carrier(VAR_1)
| ~ one_sorted_str(VAR_0)
| empty_carrier(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d11_waybel_0_sk]) ).
cnf(c_124,plain,
( in(apply_netmap(A,B,D),C)
| ~ related(B,sK4(A,B,C),D)
| ~ element(D,the_carrier(B))
| ~ is_eventually_in(A,B,C)
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d11_waybel_0]) ).
cnf(c_125,plain,
( element(sK4(A,B,C),the_carrier(B))
| ~ is_eventually_in(A,B,C)
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_d11_waybel_0]) ).
cnf(c_135,negated_conjecture,
( element(sK4(sK2,sK1,A),the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2)
| empty_carrier(sK2) ),
inference(resolve,[status(thm)],[c_125,c_98]) ).
cnf(c_138,negated_conjecture,
( in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK4(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2)
| empty_carrier(sK2) ),
inference(resolve,[status(thm)],[c_124,c_98]) ).
cnf(c_159,negated_conjecture,
( element(sK3(sK2,sK1,A),the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2)
| empty_carrier(sK2) ),
inference(resolve,[status(thm)],[c_117,c_98]) ).
cnf(c_162,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK3(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2)
| empty_carrier(sK2) ),
inference(resolve,[status(thm)],[c_116,c_98]) ).
cnf(c_197,negated_conjecture,
( element(sK0(sK1,A,B),the_carrier(sK1))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_98,c_108]) ).
cnf(c_198,negated_conjecture,
( related(sK1,A,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_98,c_107]) ).
cnf(c_199,negated_conjecture,
( related(sK1,B,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_98,c_106]) ).
cnf(c_231,negated_conjecture,
~ empty_carrier(sK2),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_232,negated_conjecture,
one_sorted_str(sK2),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_233,negated_conjecture,
~ empty_carrier(sK1),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_234,negated_conjecture,
directed_relstr(sK1),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_235,negated_conjecture,
is_eventually_in(sK2,sK1,sK5),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_236,negated_conjecture,
~ is_often_in(sK2,sK1,sK5),
inference(split_conjunct,[status(thm)],[sk_t28_yellow_6_neg]) ).
cnf(c_1953,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK3(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_231,c_162]) ).
cnf(c_1954,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK3(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_1953]) ).
cnf(c_295,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK3(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| is_often_in(sK2,sK1,A) ),
inference(resolve,[status(thm)],[c_233,c_1954]) ).
cnf(c_1955,negated_conjecture,
( element(sK3(sK2,sK1,A),the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_231,c_159]) ).
cnf(c_1956,negated_conjecture,
( element(sK3(sK2,sK1,A),the_carrier(sK1))
| is_often_in(sK2,sK1,A)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_1955]) ).
cnf(c_296,negated_conjecture,
( element(sK3(sK2,sK1,A),the_carrier(sK1))
| is_often_in(sK2,sK1,A) ),
inference(resolve,[status(thm)],[c_233,c_1956]) ).
cnf(c_1957,negated_conjecture,
( in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK4(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_231,c_138]) ).
cnf(c_1958,negated_conjecture,
( in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK4(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_1957]) ).
cnf(c_303,negated_conjecture,
( in(apply_netmap(sK2,sK1,B),A)
| ~ related(sK1,sK4(sK2,sK1,A),B)
| ~ element(B,the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A) ),
inference(resolve,[status(thm)],[c_233,c_1958]) ).
cnf(c_1959,negated_conjecture,
( element(sK4(sK2,sK1,A),the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1)
| ~ one_sorted_str(sK2) ),
inference(resolve,[status(thm)],[c_231,c_135]) ).
cnf(c_1960,negated_conjecture,
( element(sK4(sK2,sK1,A),the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_1959]) ).
cnf(c_304,negated_conjecture,
( element(sK4(sK2,sK1,A),the_carrier(sK1))
| ~ is_eventually_in(sK2,sK1,A) ),
inference(resolve,[status(thm)],[c_233,c_1960]) ).
cnf(c_1961,negated_conjecture,
( related(sK1,B,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_199]) ).
cnf(c_1962,negated_conjecture,
( related(sK1,B,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1) ),
inference(resolve,[status(thm)],[c_233,c_1961]) ).
cnf(c_308,negated_conjecture,
( related(sK1,B,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_234,c_1962]) ).
cnf(c_1963,negated_conjecture,
( related(sK1,A,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_198]) ).
cnf(c_1964,negated_conjecture,
( related(sK1,A,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1) ),
inference(resolve,[status(thm)],[c_233,c_1963]) ).
cnf(c_309,negated_conjecture,
( related(sK1,A,sK0(sK1,A,B))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_234,c_1964]) ).
cnf(c_1965,negated_conjecture,
( element(sK0(sK1,A,B),the_carrier(sK1))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_232,c_197]) ).
cnf(c_1966,negated_conjecture,
( element(sK0(sK1,A,B),the_carrier(sK1))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1))
| ~ directed_relstr(sK1) ),
inference(resolve,[status(thm)],[c_233,c_1965]) ).
cnf(c_310,negated_conjecture,
( element(sK0(sK1,A,B),the_carrier(sK1))
| ~ element(B,the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_234,c_1966]) ).
cnf(c_397,plain,
element(sK3(sK2,sK1,sK5),the_carrier(sK1)),
inference(resolve,[status(thm)],[c_296,c_236]) ).
cnf(c_403,plain,
( in(apply_netmap(sK2,sK1,A),sK5)
| ~ related(sK1,sK4(sK2,sK1,sK5),A)
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_303,c_235]) ).
cnf(c_404,plain,
element(sK4(sK2,sK1,sK5),the_carrier(sK1)),
inference(resolve,[status(thm)],[c_304,c_235]) ).
cnf(c_557,plain,
( element(sK0(sK1,sK3(sK2,sK1,sK5),A),the_carrier(sK1))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_397,c_310]) ).
cnf(c_561,plain,
( related(sK1,A,sK0(sK1,sK3(sK2,sK1,sK5),A))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_397,c_308]) ).
cnf(c_571,plain,
( related(sK1,A,sK0(sK1,A,sK4(sK2,sK1,sK5)))
| ~ element(A,the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_404,c_309]) ).
cnf(c_1139,plain,
element(sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5)),the_carrier(sK1)),
inference(resolve,[status(thm)],[c_557,c_404]) ).
cnf(c_1181,plain,
related(sK1,sK4(sK2,sK1,sK5),sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),
inference(resolve,[status(thm)],[c_561,c_404]) ).
cnf(c_1213,plain,
related(sK1,sK3(sK2,sK1,sK5),sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),
inference(resolve,[status(thm)],[c_571,c_397]) ).
cnf(c_1967,plain,
( in(apply_netmap(sK2,sK1,sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),sK5)
| ~ element(sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5)),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_1181,c_403]) ).
cnf(c_1951,plain,
in(apply_netmap(sK2,sK1,sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),sK5),
inference(resolve,[status(thm)],[c_1139,c_1967]) ).
cnf(c_1968,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),sK5)
| ~ element(sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5)),the_carrier(sK1))
| is_often_in(sK2,sK1,sK5) ),
inference(resolve,[status(thm)],[c_1213,c_295]) ).
cnf(c_1969,negated_conjecture,
( ~ in(apply_netmap(sK2,sK1,sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),sK5)
| ~ element(sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5)),the_carrier(sK1)) ),
inference(resolve,[status(thm)],[c_236,c_1968]) ).
cnf(c_1970,negated_conjecture,
~ in(apply_netmap(sK2,sK1,sK0(sK1,sK3(sK2,sK1,sK5),sK4(sK2,sK1,sK5))),sK5),
inference(resolve,[status(thm)],[c_1139,c_1969]) ).
cnf(c_1952,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1951,c_1970]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU376+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/10.44 % Computer : n002.cluster.edu
% 0.19/10.44 % Model : x86_64 x86_64
% 0.19/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/10.44 % Memory : 8046.5625MB
% 0.19/10.44 % OS : Linux 6.8.0-71-generic
% 0.19/10.44 % CPULimit : 300
% 0.19/10.44 % WCLimit : 300
% 0.19/10.44 % DateTime : Sat Sep 26 09:24:46 UTC 2026
% 0.19/10.45 % CPUTime :
% 0.19/10.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/10.45 % Process 1371172 was started by sandbox on n002,
% 0.19/10.45 % Sat Sep 26 09:24:46 2026
% 0.19/10.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/10.47
% 0.19/10.47 % From the command line: assign(max_seconds, 300).
% 0.22/10.99
% 0.22/10.99 % given #500 (W,wt=26): 1461 empty(f12(powerset(empty_set))) | in(f10(powerset(empty_set)),f12(powerset(empty_set))). [para(1392(a,1),352(b,1))].
% 0.22/10.99
% 0.22/10.99 % SZS status Theorem for theBenchmark
% 0.22/10.99
% 0.22/10.99 % Proof 1 at 0.39 (+ 0.09) seconds.
% 0.22/10.99 % Length of proof is 48.
% 0.22/10.99 % Level of proof is 8.
% 0.22/10.99 % Maximum clause weight is 37.000.
% 0.22/10.99 % Given clauses 721.
% 0.22/10.99
% 0.22/10.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------