%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU391+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 : n012.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:10 AM UTC 2026
% Result : Theorem 35.91s 4.99s
% Output : CNFRefutation 35.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 3
% Syntax : Number of formulae : 59 ( 13 unt; 0 def)
% Number of atoms : 258 ( 29 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 316 ( 117 ~; 149 |; 40 &)
% ( 3 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 75 ( 0 sgn 32 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d3_yellow19,axiom,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> filter_of_net_str(A,B) = a_2_1_yellow19(A,B) ) ),
file('theBenchmark.p',d3_yellow19) ).
fof(fraenkel_a_2_1_yellow19,axiom,
! [A,B,C] :
( ( net_str(C,B)
& ~ empty_carrier(C)
& one_sorted_str(B)
& ~ empty_carrier(B) )
=> ( in(A,a_2_1_yellow19(B,C))
<=> ? [D] :
( is_eventually_in(B,C,D)
& A = D
& element(D,powerset(the_carrier(B))) ) ) ),
file('theBenchmark.p',fraenkel_a_2_1_yellow19) ).
fof(t11_yellow19,conjecture,
! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( in(C,filter_of_net_str(A,B))
<=> ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) ) ) ) ),
file('theBenchmark.p',t11_yellow19) ).
fof(t11_yellow19_neg,negated_conjecture,
~ ! [A] :
( ( one_sorted_str(A)
& ~ empty_carrier(A) )
=> ! [B] :
( ( net_str(B,A)
& ~ empty_carrier(B) )
=> ! [C] :
( in(C,filter_of_net_str(A,B))
<=> ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) ) ) ) ),
inference(assume_negation,[status(cth)],[t11_yellow19]) ).
fof(nnf_101,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ element(C,powerset(the_carrier(A)))
| ~ is_eventually_in(A,B,C)
| ~ in(C,filter_of_net_str(A,B)) )
& ( ( element(C,powerset(the_carrier(A)))
& is_eventually_in(A,B,C) )
| in(C,filter_of_net_str(A,B)) ) )
& net_str(B,A)
& ~ empty_carrier(B) )
& one_sorted_str(A)
& ~ empty_carrier(A) ),
inference(fof_nnf,[status(thm)],[t11_yellow19_neg]) ).
fof(sk_t11_yellow19_neg_sk,plain,
( ( ~ element(sK3,powerset(the_carrier(sK1)))
| ~ is_eventually_in(sK1,sK0,sK3)
| ~ in(sK3,filter_of_net_str(sK1,sK0)) )
& ( ( element(sK3,powerset(the_carrier(sK1)))
& is_eventually_in(sK1,sK0,sK3) )
| in(sK3,filter_of_net_str(sK1,sK0)) )
& net_str(sK0,sK1)
& ~ empty_carrier(sK0)
& one_sorted_str(sK1)
& ~ empty_carrier(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK3]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK3)],[nnf_101]) ).
fof(sk_t11_yellow19_neg,plain,
( ( ~ element(sK3,powerset(the_carrier(sK1)))
| ~ is_eventually_in(sK1,sK0,sK3)
| ~ in(sK3,filter_of_net_str(sK1,sK0)) )
& ( element(sK3,powerset(the_carrier(sK1)))
| in(sK3,filter_of_net_str(sK1,sK0)) )
& ( is_eventually_in(sK1,sK0,sK3)
| in(sK3,filter_of_net_str(sK1,sK0)) )
& net_str(sK0,sK1)
& ~ empty_carrier(sK0)
& one_sorted_str(sK1)
& ~ empty_carrier(sK1) ),
inference(cnf_transformation,[status(thm)],[sk_t11_yellow19_neg_sk]) ).
cnf(c_181,negated_conjecture,
net_str(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
fof(nnf_61,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ is_eventually_in(B,C,D)
| D != A
| ~ element(D,powerset(the_carrier(B))) )
| in(A,a_2_1_yellow19(B,C)) )
& ( ? [X0] :
( is_eventually_in(B,C,X0)
& X0 = A
& element(X0,powerset(the_carrier(B))) )
| ~ in(A,a_2_1_yellow19(B,C)) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(fof_nnf,[status(thm)],[fraenkel_a_2_1_yellow19]) ).
fof(sk_fraenkel_a_2_1_yellow19_sk,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ is_eventually_in(B,C,D)
| D != A
| ~ element(D,powerset(the_carrier(B))) )
| in(A,a_2_1_yellow19(B,C)) )
& ( ( is_eventually_in(B,C,sK2(A,B,C))
& sK2(A,B,C) = A
& element(sK2(A,B,C),powerset(the_carrier(B))) )
| ~ in(A,a_2_1_yellow19(B,C)) ) )
| ~ net_str(C,B)
| empty_carrier(C)
| ~ one_sorted_str(B)
| empty_carrier(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2(A,B,C))],[nnf_61]) ).
fof(sk_fraenkel_a_2_1_yellow19,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ is_eventually_in(VAR_0,VAR_1,VAR_3)
| VAR_3 != VAR_2
| ~ element(VAR_3,powerset(the_carrier(VAR_0)))
| in(VAR_2,a_2_1_yellow19(VAR_0,VAR_1))
| ~ 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] :
( is_eventually_in(VAR_0,VAR_1,sK2(VAR_2,VAR_0,VAR_1))
| ~ in(VAR_2,a_2_1_yellow19(VAR_0,VAR_1))
| ~ 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] :
( sK2(VAR_2,VAR_0,VAR_1) = VAR_2
| ~ in(VAR_2,a_2_1_yellow19(VAR_0,VAR_1))
| ~ 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(sK2(VAR_2,VAR_0,VAR_1),powerset(the_carrier(VAR_0)))
| ~ in(VAR_2,a_2_1_yellow19(VAR_0,VAR_1))
| ~ 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_fraenkel_a_2_1_yellow19_sk]) ).
cnf(c_244,plain,
( ~ is_eventually_in(A,B,D)
| D != C
| ~ element(D,powerset(the_carrier(A)))
| in(C,a_2_1_yellow19(A,B))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_1_yellow19]) ).
cnf(c_245,plain,
( is_eventually_in(A,B,sK2(C,A,B))
| ~ in(C,a_2_1_yellow19(A,B))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_1_yellow19]) ).
cnf(c_246,plain,
( sK2(C,A,B) = C
| ~ in(C,a_2_1_yellow19(A,B))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_1_yellow19]) ).
cnf(c_247,plain,
( element(sK2(C,A,B),powerset(the_carrier(A)))
| ~ in(C,a_2_1_yellow19(A,B))
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(split_conjunct,[status(thm)],[sk_fraenkel_a_2_1_yellow19]) ).
cnf(c_250,plain,
( a_2_1_yellow19(A,B) = filter_of_net_str(A,B)
| ~ net_str(B,A)
| empty_carrier(B)
| ~ one_sorted_str(A)
| empty_carrier(A) ),
inference(clausify,[status(thm)],[d3_yellow19]) ).
cnf(c_272,negated_conjecture,
( a_2_1_yellow19(sK1,sK0) = filter_of_net_str(sK1,sK0)
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_250,c_181]) ).
cnf(c_273,negated_conjecture,
( filter_of_net_str(sK1,sK0) = a_2_1_yellow19(sK1,sK0)
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(copy,[status(thm)],[c_272]) ).
cnf(c_364,negated_conjecture,
( element(sK2(A,sK1,sK0),powerset(the_carrier(sK1)))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_247,c_181]) ).
cnf(c_365,negated_conjecture,
( sK2(A,sK1,sK0) = A
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_246,c_181]) ).
cnf(c_366,negated_conjecture,
( is_eventually_in(sK1,sK0,sK2(A,sK1,sK0))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_245,c_181]) ).
cnf(c_367,negated_conjecture,
( ~ is_eventually_in(sK1,sK0,B)
| B != A
| ~ element(B,powerset(the_carrier(sK1)))
| in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1)
| empty_carrier(sK1) ),
inference(resolve,[status(thm)],[c_244,c_181]) ).
cnf(c_533,negated_conjecture,
~ empty_carrier(sK1),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_534,negated_conjecture,
one_sorted_str(sK1),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_535,negated_conjecture,
~ empty_carrier(sK0),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_536,negated_conjecture,
( is_eventually_in(sK1,sK0,sK3)
| in(sK3,filter_of_net_str(sK1,sK0)) ),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_537,negated_conjecture,
( element(sK3,powerset(the_carrier(sK1)))
| in(sK3,filter_of_net_str(sK1,sK0)) ),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_538,negated_conjecture,
( ~ element(sK3,powerset(the_carrier(sK1)))
| ~ is_eventually_in(sK1,sK0,sK3)
| ~ in(sK3,filter_of_net_str(sK1,sK0)) ),
inference(split_conjunct,[status(thm)],[sk_t11_yellow19_neg]) ).
cnf(c_23408,negated_conjecture,
( ~ is_eventually_in(sK1,sK0,B)
| B != A
| ~ element(B,powerset(the_carrier(sK1)))
| in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1) ),
inference(resolve,[status(thm)],[c_533,c_367]) ).
cnf(c_23409,negated_conjecture,
( ~ is_eventually_in(sK1,sK0,B)
| B != A
| ~ element(B,powerset(the_carrier(sK1)))
| in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_534,c_23408]) ).
cnf(c_1069,negated_conjecture,
( ~ is_eventually_in(sK1,sK0,B)
| B != A
| ~ element(B,powerset(the_carrier(sK1)))
| in(A,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_535,c_23409]) ).
cnf(c_23410,negated_conjecture,
( is_eventually_in(sK1,sK0,sK2(A,sK1,sK0))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1) ),
inference(resolve,[status(thm)],[c_533,c_366]) ).
cnf(c_23411,negated_conjecture,
( is_eventually_in(sK1,sK0,sK2(A,sK1,sK0))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_534,c_23410]) ).
cnf(c_1070,negated_conjecture,
( is_eventually_in(sK1,sK0,sK2(A,sK1,sK0))
| ~ in(A,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_535,c_23411]) ).
cnf(c_23412,negated_conjecture,
( sK2(A,sK1,sK0) = A
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1) ),
inference(resolve,[status(thm)],[c_533,c_365]) ).
cnf(c_23413,negated_conjecture,
( sK2(A,sK1,sK0) = A
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_534,c_23412]) ).
cnf(c_1071,negated_conjecture,
( sK2(A,sK1,sK0) = A
| ~ in(A,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_535,c_23413]) ).
cnf(c_23414,negated_conjecture,
( element(sK2(A,sK1,sK0),powerset(the_carrier(sK1)))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0)
| ~ one_sorted_str(sK1) ),
inference(resolve,[status(thm)],[c_533,c_364]) ).
cnf(c_23415,negated_conjecture,
( element(sK2(A,sK1,sK0),powerset(the_carrier(sK1)))
| ~ in(A,a_2_1_yellow19(sK1,sK0))
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_534,c_23414]) ).
cnf(c_1072,negated_conjecture,
( element(sK2(A,sK1,sK0),powerset(the_carrier(sK1)))
| ~ in(A,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_535,c_23415]) ).
cnf(c_23416,negated_conjecture,
( filter_of_net_str(sK1,sK0) = a_2_1_yellow19(sK1,sK0)
| empty_carrier(sK0)
| ~ one_sorted_str(sK1) ),
inference(resolve,[status(thm)],[c_533,c_273]) ).
cnf(c_23417,negated_conjecture,
( filter_of_net_str(sK1,sK0) = a_2_1_yellow19(sK1,sK0)
| empty_carrier(sK0) ),
inference(resolve,[status(thm)],[c_534,c_23416]) ).
cnf(c_1074,negated_conjecture,
filter_of_net_str(sK1,sK0) = a_2_1_yellow19(sK1,sK0),
inference(resolve,[status(thm)],[c_535,c_23417]) ).
cnf(c_1118,negated_conjecture,
( ~ element(sK3,powerset(the_carrier(sK1)))
| ~ is_eventually_in(sK1,sK0,sK3)
| ~ in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(paramod,[status(thm)],[c_1074,c_538]) ).
cnf(c_1119,negated_conjecture,
( element(sK3,powerset(the_carrier(sK1)))
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(paramod,[status(thm)],[c_1074,c_537]) ).
cnf(c_1120,negated_conjecture,
( is_eventually_in(sK1,sK0,sK3)
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(paramod,[status(thm)],[c_1074,c_536]) ).
cnf(c_2225,plain,
( sK3 != A
| ~ element(sK3,powerset(the_carrier(sK1)))
| in(A,a_2_1_yellow19(sK1,sK0))
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_1120,c_1069]) ).
cnf(c_23418,negated_conjecture,
( in(sK3,a_2_1_yellow19(sK1,sK0))
| sK3 != A
| in(A,a_2_1_yellow19(sK1,sK0))
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(resolve,[status(thm)],[c_2225,c_1119]) ).
cnf(c_23393,negated_conjecture,
( sK3 != A
| in(A,a_2_1_yellow19(sK1,sK0))
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(copy,[status(thm)],[c_23418]) ).
cnf(c_23419,plain,
( sK3 != sK3
| in(sK3,a_2_1_yellow19(sK1,sK0)) ),
inference(factor,[status(thm)],[c_23393]) ).
cnf(c_23394,plain,
in(sK3,a_2_1_yellow19(sK1,sK0)),
inference(copy,[status(thm)],[c_23419]) ).
cnf(c_23395,negated_conjecture,
( ~ element(sK3,powerset(the_carrier(sK1)))
| ~ is_eventually_in(sK1,sK0,sK3) ),
inference(resolve,[status(thm)],[c_23394,c_1118]) ).
cnf(c_23398,plain,
element(sK2(sK3,sK1,sK0),powerset(the_carrier(sK1))),
inference(resolve,[status(thm)],[c_23394,c_1072]) ).
cnf(c_23399,plain,
sK2(sK3,sK1,sK0) = sK3,
inference(resolve,[status(thm)],[c_23394,c_1071]) ).
cnf(c_23420,negated_conjecture,
is_eventually_in(sK1,sK0,sK2(sK3,sK1,sK0)),
inference(resolve,[status(thm)],[c_23394,c_1070]) ).
cnf(c_23400,negated_conjecture,
is_eventually_in(sK1,sK0,sK3),
inference(paramod,[status(thm)],[c_23399,c_23420]) ).
cnf(c_23406,plain,
element(sK3,powerset(the_carrier(sK1))),
inference(paramod,[status(thm)],[c_23399,c_23398]) ).
cnf(c_23421,negated_conjecture,
~ element(sK3,powerset(the_carrier(sK1))),
inference(resolve,[status(thm)],[c_23400,c_23395]) ).
cnf(c_23407,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_23406,c_23421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 09:24:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 250858 was started by sandbox on n012,
% 0.10/0.36 % Sat Sep 26 09:24:34 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 35.91/4.99
% 35.91/4.99 % given #500 (I,wt=11): 1093 -reflexive_relstr(c17) | -complete_relstr(c17) | up_complete_relstr(c17). [back_unit_del(385),unit_del(a,534),unit_del(b,535)].
% 35.91/4.99
% 35.91/4.99 % given #1000 (A,wt=27): 1303 -bounded_relstr(rel_str_of(A,f2(A,A))) | upper_bounded_relstr(rel_str_of(A,f2(A,A))). [resolve(542,a,411,a)].
% 35.91/4.99
% 35.91/4.99 % given #1500 (W,wt=19): 16049 finite(f4(A,c5)) | -in(powerset(A),f8(A)). [resolve(9775,b,404,b)].
% 35.91/4.99
% 35.91/4.99 % given #2000 (W,wt=21): 2148 finite(cartesian_product2(f11(c6),f11(c6))). [resolve(1067,a,851,a)].
% 35.91/4.99
% 35.91/4.99 % given #2500 (T,wt=21): 10725 in(f20(A,B),B) | B = A | finite(f15(A)). [resolve(1278,a,518,a)].
% 35.91/4.99
% 35.91/4.99 % given #3000 (A,wt=39): 2127 empty_carrier(rel_str_of(the_carrier(c12),the_InternalRel(c12))) | -reflexive_relstr(rel_str_of(the_carrier(c12),the_InternalRel(c12))) | -trivial_carrier(rel_str_of(the_carrier(c12),the_InternalRel(c12))) | antisymmetric_relstr(rel_str_of(the_carrier(c12),the_InternalRel(c12))). [resolve(1062,a,546,a)].
% 35.91/4.99
% 35.91/4.99 % SZS status Theorem for theBenchmark
% 35.91/4.99
% 35.91/4.99 % Proof 1 at 3.29 (+ 1.24) seconds.
% 35.91/4.99 % Length of proof is 38.
% 35.91/4.99 % Level of proof is 11.
% 35.91/4.99 % Maximum clause weight is 38.000.
% 35.91/4.99 % Given clauses 3191.
% 35.91/4.99
% 35.91/4.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------