%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU170+2 : 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 : n005.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:45:18 AM UTC 2026
% Result : Theorem 248.94s 33.05s
% Output : CNFRefutation 248.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 23
% Syntax : Number of formulae : 100 ( 55 unt; 0 def)
% Number of atoms : 177 ( 47 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 126 ( 49 ~; 40 |; 19 &)
% ( 5 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 150 ( 14 sgn 58 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_xboole_0,axiom,
! [A,B] : set_union2(A,B) = set_union2(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(commutativity_k3_xboole_0,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('theBenchmark.p',commutativity_k3_xboole_0) ).
fof(d2_subset_1,axiom,
! [A,B] :
( ( empty(A)
=> ( element(B,A)
<=> empty(B) ) )
& ( ~ empty(A)
=> ( element(B,A)
<=> in(B,A) ) ) ),
file('theBenchmark.p',d2_subset_1) ).
fof(d5_subset_1,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('theBenchmark.p',d5_subset_1) ).
fof(fc1_subset_1,axiom,
! [A] : ~ empty(powerset(A)),
file('theBenchmark.p',fc1_subset_1) ).
fof(rc1_xboole_0,axiom,
? [A] : empty(A),
file('theBenchmark.p',rc1_xboole_0) ).
fof(symmetry_r1_xboole_0,axiom,
! [A,B] :
( disjoint(A,B)
=> disjoint(B,A) ),
file('theBenchmark.p',symmetry_r1_xboole_0) ).
fof(t28_xboole_1,axiom,
! [A,B] :
( subset(A,B)
=> set_intersection2(A,B) = A ),
file('theBenchmark.p',t28_xboole_1) ).
fof(t2_boole,axiom,
! [A] : set_intersection2(A,empty_set) = empty_set,
file('theBenchmark.p',t2_boole) ).
fof(t33_xboole_1,axiom,
! [A,B,C] :
( subset(A,B)
=> subset(set_difference(A,C),set_difference(B,C)) ),
file('theBenchmark.p',t33_xboole_1) ).
fof(t39_xboole_1,axiom,
! [A,B] : set_union2(A,set_difference(B,A)) = set_union2(A,B),
file('theBenchmark.p',t39_xboole_1) ).
fof(t3_boole,axiom,
! [A] : set_difference(A,empty_set) = A,
file('theBenchmark.p',t3_boole) ).
fof(t3_xboole_0,axiom,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('theBenchmark.p',t3_xboole_0) ).
fof(t40_xboole_1,axiom,
! [A,B] : set_difference(set_union2(A,B),B) = set_difference(A,B),
file('theBenchmark.p',t40_xboole_1) ).
fof(t48_xboole_1,axiom,
! [A,B] : set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
file('theBenchmark.p',t48_xboole_1) ).
fof(t4_xboole_0,axiom,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('theBenchmark.p',t4_xboole_0) ).
fof(t63_xboole_1,axiom,
! [A,B,C] :
( ( disjoint(B,C)
& subset(A,B) )
=> disjoint(A,C) ),
file('theBenchmark.p',t63_xboole_1) ).
fof(t6_boole,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('theBenchmark.p',t6_boole) ).
fof(t7_xboole_1,axiom,
! [A,B] : subset(A,set_union2(A,B)),
file('theBenchmark.p',t7_xboole_1) ).
fof(t83_xboole_1,axiom,
! [A,B] :
( disjoint(A,B)
<=> set_difference(A,B) = A ),
file('theBenchmark.p',t83_xboole_1) ).
fof(t92_zfmisc_1,axiom,
! [A,B] :
( in(A,B)
=> subset(A,union(B)) ),
file('theBenchmark.p',t92_zfmisc_1) ).
fof(t99_zfmisc_1,axiom,
! [A] : union(powerset(A)) = A,
file('theBenchmark.p',t99_zfmisc_1) ).
fof(t43_subset_1,conjecture,
! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,powerset(A))
=> ( disjoint(B,C)
<=> subset(B,subset_complement(A,C)) ) ) ),
file('theBenchmark.p',t43_subset_1) ).
fof(t43_subset_1_neg,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(A))
=> ! [C] :
( element(C,powerset(A))
=> ( disjoint(B,C)
<=> subset(B,subset_complement(A,C)) ) ) ),
inference(assume_negation,[status(cth)],[t43_subset_1]) ).
fof(nnf_108,plain,
? [A,B] :
( ? [C] :
( ( ~ subset(B,subset_complement(A,C))
| ~ disjoint(B,C) )
& ( subset(B,subset_complement(A,C))
| disjoint(B,C) )
& element(C,powerset(A)) )
& element(B,powerset(A)) ),
inference(fof_nnf,[status(thm)],[t43_subset_1_neg]) ).
fof(sk_t43_subset_1_neg,plain,
( ( ~ subset(sK0,subset_complement(sK2,sK1))
| ~ disjoint(sK0,sK1) )
& ( subset(sK0,subset_complement(sK2,sK1))
| disjoint(sK0,sK1) )
& element(sK1,powerset(sK2))
& element(sK0,powerset(sK2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2,sK1]),skolemize(A,sK2),skolemize(B,sK0),skolemize(C,sK1)],[nnf_108]) ).
cnf(c_109,negated_conjecture,
( ~ subset(sK0,subset_complement(sK2,sK1))
| ~ disjoint(sK0,sK1) ),
inference(split_conjunct,[status(thm)],[sk_t43_subset_1_neg]) ).
cnf(c_110,negated_conjecture,
( subset(sK0,subset_complement(sK2,sK1))
| disjoint(sK0,sK1) ),
inference(split_conjunct,[status(thm)],[sk_t43_subset_1_neg]) ).
cnf(c_111,negated_conjecture,
element(sK1,powerset(sK2)),
inference(split_conjunct,[status(thm)],[sk_t43_subset_1_neg]) ).
cnf(c_112,negated_conjecture,
element(sK0,powerset(sK2)),
inference(split_conjunct,[status(thm)],[sk_t43_subset_1_neg]) ).
cnf(c_118,plain,
union(powerset(A)) = A,
inference(clausify,[status(thm)],[t99_zfmisc_1]) ).
cnf(c_119,plain,
( subset(A,union(B))
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t92_zfmisc_1]) ).
cnf(c_123,plain,
( set_difference(A,B) != A
| disjoint(A,B) ),
inference(clausify,[status(thm)],[t83_xboole_1]) ).
cnf(c_124,plain,
( set_difference(A,B) = A
| ~ disjoint(A,B) ),
inference(clausify,[status(thm)],[t83_xboole_1]) ).
cnf(c_125,plain,
subset(A,set_union2(A,B)),
inference(clausify,[status(thm)],[t7_xboole_1]) ).
cnf(c_128,plain,
( empty_set = A
| ~ empty(A) ),
inference(clausify,[status(thm)],[t6_boole]) ).
cnf(c_134,plain,
( disjoint(A,C)
| ~ disjoint(B,C)
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t63_xboole_1]) ).
fof(nnf_91,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [X0] : in(X0,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(fof_nnf,[status(thm)],[t4_xboole_0]) ).
fof(sk_t4_xboole_0_sk,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( in(sK3(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3(A,B))],[nnf_91]) ).
fof(sk_t4_xboole_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ disjoint(VAR_1,VAR_2)
| ~ in(VAR_0,set_intersection2(VAR_1,VAR_2)) )
& ! [VAR_0,VAR_1] :
( in(sK3(VAR_0,VAR_1),set_intersection2(VAR_0,VAR_1))
| disjoint(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_t4_xboole_0_sk]) ).
cnf(c_137,plain,
( in(sK3(A,B),set_intersection2(A,B))
| disjoint(A,B) ),
inference(split_conjunct,[status(thm)],[sk_t4_xboole_0]) ).
cnf(c_139,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(A,B),
inference(clausify,[status(thm)],[t48_xboole_1]) ).
cnf(c_140,plain,
set_intersection2(A,B) = set_difference(A,set_difference(A,B)),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_144,plain,
set_difference(set_union2(A,B),B) = set_difference(A,B),
inference(clausify,[status(thm)],[t40_xboole_1]) ).
cnf(c_146,plain,
( ~ disjoint(B,C)
| ~ in(A,C)
| ~ in(A,B) ),
inference(clausify,[status(thm)],[t3_xboole_0]) ).
cnf(c_149,plain,
set_difference(A,empty_set) = A,
inference(clausify,[status(thm)],[t3_boole]) ).
cnf(c_156,plain,
set_union2(A,set_difference(B,A)) = set_union2(A,B),
inference(clausify,[status(thm)],[t39_xboole_1]) ).
cnf(c_168,plain,
( subset(set_difference(A,C),set_difference(B,C))
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t33_xboole_1]) ).
cnf(c_172,plain,
set_intersection2(A,empty_set) = empty_set,
inference(clausify,[status(thm)],[t2_boole]) ).
cnf(c_39873,plain,
set_difference(A,set_difference(A,empty_set)) = empty_set,
inference(paramod,[status(thm)],[c_140,c_172]) ).
cnf(c_173,plain,
set_difference(A,A) = empty_set,
inference(paramod,[status(thm)],[c_149,c_39873]) ).
cnf(c_174,plain,
( set_intersection2(A,B) = A
| ~ subset(A,B) ),
inference(clausify,[status(thm)],[t28_xboole_1]) ).
cnf(c_175,plain,
( set_difference(A,set_difference(A,B)) = A
| ~ subset(A,B) ),
inference(paramod,[status(thm)],[c_140,c_174]) ).
cnf(c_196,plain,
( disjoint(B,A)
| ~ disjoint(A,B) ),
inference(clausify,[status(thm)],[symmetry_r1_xboole_0]) ).
fof(nnf_55,plain,
? [A] : empty(A),
inference(fof_nnf,[status(thm)],[rc1_xboole_0]) ).
fof(sk_rc1_xboole_0,plain,
empty(sK4),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(A,sK4)],[nnf_55]) ).
cnf(c_201,plain,
empty(sK4),
inference(split_conjunct,[status(thm)],[sk_rc1_xboole_0]) ).
cnf(c_227,plain,
~ empty(powerset(A)),
inference(clausify,[status(thm)],[fc1_subset_1]) ).
cnf(c_239,plain,
( subset_complement(B,A) = set_difference(B,A)
| ~ element(A,powerset(B)) ),
inference(clausify,[status(thm)],[d5_subset_1]) ).
cnf(c_293,plain,
( in(B,A)
| ~ element(B,A)
| empty(A) ),
inference(clausify,[status(thm)],[d2_subset_1]) ).
cnf(c_310,plain,
set_intersection2(A,B) = set_intersection2(B,A),
inference(clausify,[status(thm)],[commutativity_k3_xboole_0]) ).
cnf(c_39874,plain,
set_difference(A,set_difference(A,B)) = set_intersection2(B,A),
inference(paramod,[status(thm)],[c_140,c_310]) ).
cnf(c_311,plain,
set_difference(A,set_difference(A,B)) = set_difference(B,set_difference(B,A)),
inference(paramod,[status(thm)],[c_140,c_39874]) ).
cnf(c_312,plain,
set_union2(A,B) = set_union2(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_319,plain,
( in(sK3(A,B),set_difference(A,set_difference(A,B)))
| disjoint(A,B) ),
inference(paramod,[status(thm)],[c_140,c_137]) ).
cnf(c_321,plain,
( ~ disjoint(B,B)
| ~ in(A,B) ),
inference(factor,[status(thm)],[c_146]) ).
cnf(c_363,plain,
( subset(sK0,subset_complement(sK2,sK1))
| set_difference(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_124,c_110]) ).
cnf(c_389,plain,
disjoint(A,empty_set),
inference(resolve,[status(thm)],[c_149,c_123]) ).
cnf(c_390,plain,
set_difference(set_union2(A,B),set_difference(B,A)) = set_difference(A,set_difference(B,A)),
inference(paramod,[status(thm)],[c_156,c_144]) ).
cnf(c_489,plain,
empty_set = sK4,
inference(resolve,[status(thm)],[c_201,c_128]) ).
cnf(c_510,plain,
disjoint(A,sK4),
inference(paramod,[status(thm)],[c_489,c_389]) ).
cnf(c_519,plain,
set_difference(A,A) = sK4,
inference(paramod,[status(thm)],[c_489,c_173]) ).
cnf(c_555,plain,
subset_complement(sK2,sK1) = set_difference(sK2,sK1),
inference(resolve,[status(thm)],[c_239,c_111]) ).
cnf(c_567,plain,
( subset(sK0,set_difference(sK2,sK1))
| set_difference(sK0,sK1) = sK0 ),
inference(paramod,[status(thm)],[c_555,c_363]) ).
cnf(c_569,negated_conjecture,
( ~ subset(sK0,set_difference(sK2,sK1))
| ~ disjoint(sK0,sK1) ),
inference(paramod,[status(thm)],[c_555,c_109]) ).
cnf(c_39875,negated_conjecture,
( in(sK0,powerset(sK2))
| empty(powerset(sK2)) ),
inference(resolve,[status(thm)],[c_293,c_112]) ).
cnf(c_1770,negated_conjecture,
in(sK0,powerset(sK2)),
inference(resolve,[status(thm)],[c_227,c_39875]) ).
cnf(c_1877,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = set_difference(B,set_difference(B,set_union2(A,B))),
inference(paramod,[status(thm)],[c_144,c_311]) ).
cnf(c_1885,plain,
subset(A,set_union2(B,A)),
inference(paramod,[status(thm)],[c_312,c_125]) ).
cnf(c_2502,plain,
~ in(A,sK4),
inference(resolve,[status(thm)],[c_510,c_321]) ).
cnf(c_39876,plain,
subset(sK0,union(powerset(sK2))),
inference(resolve,[status(thm)],[c_1770,c_119]) ).
cnf(c_2631,plain,
subset(sK0,sK2),
inference(paramod,[status(thm)],[c_118,c_39876]) ).
cnf(c_2649,plain,
subset(set_difference(sK0,A),set_difference(sK2,A)),
inference(resolve,[status(thm)],[c_2631,c_168]) ).
cnf(c_2802,plain,
( in(sK3(sK0,sK1),set_difference(sK0,set_difference(sK0,sK1)))
| ~ subset(sK0,set_difference(sK2,sK1)) ),
inference(resolve,[status(thm)],[c_569,c_319]) ).
cnf(c_3096,plain,
set_difference(A,set_difference(A,set_union2(B,A))) = A,
inference(resolve,[status(thm)],[c_1885,c_175]) ).
cnf(c_3104,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = B,
inference(paramod,[status(thm)],[c_3096,c_1877]) ).
cnf(c_39877,plain,
set_difference(set_union2(A,B),set_difference(A,B)) = set_difference(B,set_difference(A,B)),
inference(paramod,[status(thm)],[c_312,c_390]) ).
cnf(c_39878,plain,
B = set_difference(B,set_difference(A,B)),
inference(paramod,[status(thm)],[c_3104,c_39877]) ).
cnf(c_4044,plain,
set_difference(A,set_difference(B,A)) = A,
inference(copy,[status(thm)],[c_39878]) ).
cnf(c_8563,plain,
disjoint(A,set_difference(B,A)),
inference(resolve,[status(thm)],[c_4044,c_123]) ).
cnf(c_8657,plain,
disjoint(set_difference(A,B),B),
inference(resolve,[status(thm)],[c_8563,c_196]) ).
cnf(c_8661,plain,
( disjoint(A,C)
| ~ subset(A,set_difference(B,C)) ),
inference(resolve,[status(thm)],[c_8657,c_134]) ).
cnf(c_24663,plain,
( set_difference(sK0,sK1) = sK0
| disjoint(sK0,sK1) ),
inference(resolve,[status(thm)],[c_8661,c_567]) ).
cnf(c_39879,plain,
( set_difference(sK0,sK1) = sK0
| set_difference(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_24663,c_124]) ).
cnf(c_39842,plain,
set_difference(sK0,sK1) = sK0,
inference(copy,[status(thm)],[c_39879]) ).
cnf(c_39880,plain,
( in(sK3(sK0,sK1),set_difference(sK0,sK0))
| ~ subset(sK0,set_difference(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_39842,c_2802]) ).
cnf(c_39881,plain,
( in(sK3(sK0,sK1),sK4)
| ~ subset(sK0,set_difference(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_519,c_39880]) ).
cnf(c_39845,plain,
~ subset(sK0,set_difference(sK2,sK1)),
inference(resolve,[status(thm)],[c_2502,c_39881]) ).
cnf(c_39882,plain,
subset(sK0,set_difference(sK2,sK1)),
inference(paramod,[status(thm)],[c_39842,c_2649]) ).
cnf(c_39872,plain,
$false,
inference(resolve,[status(thm)],[c_39845,c_39882]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU170+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n005.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sat Sep 26 08:43:46 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.42 % Process 1728937 was started by sandbox on n005,
% 0.15/0.42 % Sat Sep 26 08:43:46 2026
% 0.15/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.46
% 0.15/0.46 % From the command line: assign(max_seconds, 300).
% 248.94/33.05
% 248.94/33.05 % given #500 (T,wt=6): 5821 element(f25(c3,c5),f24(c3)). [resolve(5163,a,292,c),unit_del(a,368)].
% 248.94/33.05
% 248.94/33.05 % given #1000 (F,wt=8): 10645 f24(A) != set_difference(B,union(f20(C))). [resolve(10615,a,4383,b)].
% 248.94/33.05
% 248.94/33.05 % given #1500 (A,wt=18): 590 set_difference(A,B) = C | in(f16(A,B,C),C) | subset(f16(A,B,C),union(A)). [resolve(242,c,119,a)].
% 248.94/33.05
% 248.94/33.05 % given #2000 (T,wt=6): 18516 in(c5,union(f24(powerset(c3)))). [resolve(2510,a,1771,a)].
% 248.94/33.05
% 248.94/33.05 % given #2500 (F,wt=9): 15473 f25(c3,f17(powerset(c5))) != cartesian_product2(A,B). [resolve(12771,a,357,b),flip(a),unit_del(b,2872)].
% 248.94/33.05
% 248.94/33.05 % given #3000 (T,wt=7): 23142 in(f18(c2),set_union2(A,f20(c2))). [resolve(23082,a,3083,a)].
% 248.94/33.05
% 248.94/33.05 % given #3500 (F,wt=9): 18297 -in(f25(union(f20(c3)),union(f20(c3))),c4). [para(13381(a,1),11645(a,2,2)),rewrite([525(10)])].
% 248.94/33.05
% 248.94/33.05 % given #4000 (T,wt=7): 25718 in(c4,f20(union(f25(c3,c3)))). [para(13304(a,1),10029(a,1,2)),rewrite([525(3)])].
% 248.94/33.05
% 248.94/33.05 % given #4500 (F,wt=8): 27666 set_union2(A,set_union2(B,powerset(c1))) != c1. [para(312(a,1),27476(a,1,2))].
% 248.94/33.05
% 248.94/33.05 % given #5000 (T,wt=7): 29418 in(c1,union(set_union2(f20(A),B))). [resolve(17817,a,501,a)].
% 248.94/33.05
% 248.94/33.05 % given #5500 (F,wt=9): 21952 set_difference(A,f24(c3)) != f24(union(f20(c3))). [resolve(21901,a,5156,b)].
% 248.94/33.05
% 248.94/33.05 % given #6000 (A,wt=36): 1099 cartesian_product2(A,B) != C | in(f12(D,C,B),C) | -in(E,A) | unordered_pair(unordered_pair(E,f12(D,C,B)),unordered_pair(E,E)) != f12(D,C,B) | set_difference(D,set_difference(D,C)) = B. [factor(1072,b,f)].
% 248.94/33.05
% 248.94/33.05 % given #6500 (T,wt=8): 21396 subset(f18(powerset(c1)),set_union2(f24(A),B)). [resolve(21382,a,442,a)].
% 248.94/33.05
% 248.94/33.05 % given #7000 (F,wt=8): 36204 -in(f20(set_union2(c2,A)),powerset(f18(c2))). [para(23192(a,1),14519(a,2,1,2)),rewrite([525(7)])].
% 248.94/33.05
% 248.94/33.05 % SZS status Theorem for theBenchmark
% 248.94/33.05
% 248.94/33.05 % Proof 1 at 24.17 (+ 7.95) seconds.
% 248.94/33.05 % Length of proof is 82.
% 248.94/33.05 % Level of proof is 13.
% 248.94/33.05 % Maximum clause weight is 15.000.
% 248.94/33.05 % Given clauses 7490.
% 248.94/33.05
% 248.94/33.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------