%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET611+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:36:36 AM UTC 2026
% Result : Theorem 108.12s 14.95s
% Output : CNFRefutation 108.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 7
% Syntax : Number of formulae : 56 ( 10 unt; 0 def)
% Number of atoms : 151 ( 56 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 151 ( 56 ~; 72 |; 16 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 97 ( 6 sgn 41 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(intersection_defn,axiom,
! [B,C,D] :
( member(D,intersection(B,C))
<=> ( member(D,C)
& member(D,B) ) ),
file('theBenchmark.p',intersection_defn) ).
fof(difference_defn,axiom,
! [B,C,D] :
( member(D,difference(B,C))
<=> ( ~ member(D,C)
& member(D,B) ) ),
file('theBenchmark.p',difference_defn) ).
fof(empty_set_defn,axiom,
! [B] : ~ member(B,empty_set),
file('theBenchmark.p',empty_set_defn) ).
fof(commutativity_of_intersection,axiom,
! [B,C] : intersection(B,C) = intersection(C,B),
file('theBenchmark.p',commutativity_of_intersection) ).
fof(equal_member_defn,axiom,
! [B,C] :
( B = C
<=> ! [D] :
( member(D,B)
<=> member(D,C) ) ),
file('theBenchmark.p',equal_member_defn) ).
fof(empty_defn,axiom,
! [B] :
( empty(B)
<=> ! [C] : ~ member(C,B) ),
file('theBenchmark.p',empty_defn) ).
fof(prove_th84,conjecture,
! [B,C] :
( intersection(B,C) = empty_set
<=> difference(B,C) = B ),
file('theBenchmark.p',prove_th84) ).
fof(prove_th84_neg,negated_conjecture,
~ ! [B,C] :
( intersection(B,C) = empty_set
<=> difference(B,C) = B ),
inference(assume_negation,[status(cth)],[prove_th84]) ).
fof(nnf_10,plain,
! [B] :
( ( ? [C] : member(C,B)
| empty(B) )
& ( ! [X0] : ~ member(X0,B)
| ~ empty(B) ) ),
inference(fof_nnf,[status(thm)],[empty_defn]) ).
fof(sk_empty_defn_sk,plain,
! [B] :
( ( member(sK0(B),B)
| empty(B) )
& ( ! [X0] : ~ member(X0,B)
| ~ empty(B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(C,sK0(B))],[nnf_10]) ).
fof(sk_empty_defn,plain,
( ! [VAR_0] :
( member(sK0(VAR_0),VAR_0)
| empty(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ member(VAR_1,VAR_0)
| ~ empty(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_empty_defn_sk]) ).
cnf(c_12,plain,
( member(sK0(A),A)
| empty(A) ),
inference(split_conjunct,[status(thm)],[sk_empty_defn]) ).
cnf(c_13,plain,
( ~ member(B,A)
| ~ empty(A) ),
inference(split_conjunct,[status(thm)],[sk_empty_defn]) ).
cnf(c_14,plain,
( ~ member(B,A)
| member(sK0(A),A) ),
inference(resolve,[status(thm)],[c_12,c_13]) ).
fof(nnf_11,plain,
? [B,C] :
( ( difference(B,C) != B
| intersection(B,C) != empty_set )
& ( difference(B,C) = B
| intersection(B,C) = empty_set ) ),
inference(fof_nnf,[status(thm)],[prove_th84_neg]) ).
fof(sk_prove_th84_neg,plain,
( ( difference(sK1,sK2) != sK1
| intersection(sK1,sK2) != empty_set )
& ( difference(sK1,sK2) = sK1
| intersection(sK1,sK2) = empty_set ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(B,sK1),skolemize(C,sK2)],[nnf_11]) ).
cnf(c_15,negated_conjecture,
( difference(sK1,sK2) != sK1
| intersection(sK1,sK2) != empty_set ),
inference(split_conjunct,[status(thm)],[sk_prove_th84_neg]) ).
cnf(c_16,negated_conjecture,
( difference(sK1,sK2) = sK1
| intersection(sK1,sK2) = empty_set ),
inference(split_conjunct,[status(thm)],[sk_prove_th84_neg]) ).
fof(nnf_7,plain,
! [B,C] :
( ( ? [D] :
( ( ~ member(D,C)
| ~ member(D,B) )
& ( member(D,C)
| member(D,B) ) )
| C = B )
& ( ! [X0] :
( ( ~ member(X0,C)
| member(X0,B) )
& ( member(X0,C)
| ~ member(X0,B) ) )
| C != B ) ),
inference(fof_nnf,[status(thm)],[equal_member_defn]) ).
fof(sk_equal_member_defn_sk,plain,
! [B,C] :
( ( ( ( ~ member(sK3(B,C),C)
| ~ member(sK3(B,C),B) )
& ( member(sK3(B,C),C)
| member(sK3(B,C),B) ) )
| C = B )
& ( ! [X0] :
( ( ~ member(X0,C)
| member(X0,B) )
& ( member(X0,C)
| ~ member(X0,B) ) )
| C != B ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(D,sK3(B,C))],[nnf_7]) ).
fof(sk_equal_member_defn,plain,
( ! [VAR_0,VAR_1] :
( ~ member(sK3(VAR_1,VAR_0),VAR_0)
| ~ member(sK3(VAR_1,VAR_0),VAR_1)
| VAR_0 = VAR_1 )
& ! [VAR_0,VAR_1] :
( member(sK3(VAR_1,VAR_0),VAR_0)
| member(sK3(VAR_1,VAR_0),VAR_1)
| VAR_0 = VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ member(VAR_2,VAR_0)
| member(VAR_2,VAR_1)
| VAR_0 != VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( member(VAR_2,VAR_0)
| ~ member(VAR_2,VAR_1)
| VAR_0 != VAR_1 ) ),
inference(cnf_transformation,[status(thm)],[sk_equal_member_defn_sk]) ).
cnf(c_21,plain,
( ~ member(sK3(B,A),A)
| ~ member(sK3(B,A),B)
| A = B ),
inference(split_conjunct,[status(thm)],[sk_equal_member_defn]) ).
cnf(c_22,plain,
( member(sK3(B,A),A)
| member(sK3(B,A),B)
| A = B ),
inference(split_conjunct,[status(thm)],[sk_equal_member_defn]) ).
cnf(c_25,plain,
intersection(A,B) = intersection(B,A),
inference(clausify,[status(thm)],[commutativity_of_intersection]) ).
cnf(c_29,plain,
~ member(A,empty_set),
inference(clausify,[status(thm)],[empty_set_defn]) ).
cnf(c_30,plain,
( member(A,C)
| ~ member(A,B)
| member(A,difference(B,C)) ),
inference(clausify,[status(thm)],[difference_defn]) ).
cnf(c_31,plain,
( ~ member(A,C)
| ~ member(A,difference(B,C)) ),
inference(clausify,[status(thm)],[difference_defn]) ).
cnf(c_32,plain,
( member(A,B)
| ~ member(A,difference(B,C)) ),
inference(clausify,[status(thm)],[difference_defn]) ).
cnf(c_33,plain,
( ~ member(A,C)
| ~ member(A,B)
| member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection_defn]) ).
cnf(c_34,plain,
( member(A,C)
| ~ member(A,intersection(B,C)) ),
inference(clausify,[status(thm)],[intersection_defn]) ).
cnf(c_53,plain,
( member(sK3(A,empty_set),A)
| empty_set = A ),
inference(resolve,[status(thm)],[c_29,c_22]) ).
cnf(c_63,plain,
( ~ member(A,sK2)
| ~ member(A,sK1)
| intersection(sK1,sK2) = empty_set ),
inference(paramod,[status(thm)],[c_16,c_31]) ).
cnf(c_64,plain,
( member(sK3(A,difference(B,C)),A)
| difference(B,C) = A
| member(sK3(A,difference(B,C)),B) ),
inference(resolve,[status(thm)],[c_32,c_22]) ).
cnf(c_67,plain,
( difference(A,B) = A
| member(sK3(A,difference(A,B)),A) ),
inference(factor,[status(thm)],[c_64]) ).
cnf(c_185,plain,
( member(sK0(A),A)
| empty_set = A ),
inference(resolve,[status(thm)],[c_53,c_14]) ).
cnf(c_23047,plain,
( member(sK0(intersection(A,B)),B)
| empty_set = intersection(A,B) ),
inference(resolve,[status(thm)],[c_185,c_34]) ).
cnf(c_212,plain,
( member(sK0(intersection(A,B)),B)
| intersection(A,B) = empty_set ),
inference(copy,[status(thm)],[c_23047]) ).
cnf(c_446,plain,
( ~ member(sK0(intersection(A,sK2)),sK1)
| intersection(sK1,sK2) = empty_set
| intersection(A,sK2) = empty_set ),
inference(resolve,[status(thm)],[c_212,c_63]) ).
cnf(c_459,plain,
( member(sK0(intersection(B,A)),B)
| intersection(A,B) = empty_set ),
inference(paramod,[status(thm)],[c_25,c_212]) ).
cnf(c_460,plain,
( ~ member(sK0(intersection(sK1,sK2)),sK1)
| intersection(sK1,sK2) = empty_set ),
inference(factor,[status(thm)],[c_446]) ).
cnf(c_23048,plain,
( intersection(sK2,sK1) = empty_set
| intersection(sK1,sK2) = empty_set ),
inference(resolve,[status(thm)],[c_460,c_459]) ).
cnf(c_23049,plain,
( intersection(sK1,sK2) = empty_set
| intersection(sK1,sK2) = empty_set ),
inference(paramod,[status(thm)],[c_25,c_23048]) ).
cnf(c_637,plain,
intersection(sK1,sK2) = empty_set,
inference(copy,[status(thm)],[c_23049]) ).
cnf(c_23050,negated_conjecture,
( difference(sK1,sK2) != sK1
| empty_set != empty_set ),
inference(paramod,[status(thm)],[c_637,c_15]) ).
cnf(c_638,negated_conjecture,
difference(sK1,sK2) != sK1,
inference(copy,[status(thm)],[c_23050]) ).
cnf(c_659,plain,
( ~ member(sK3(A,difference(A,B)),C)
| member(sK3(A,difference(A,B)),intersection(A,C))
| difference(A,B) = A ),
inference(resolve,[status(thm)],[c_67,c_33]) ).
cnf(c_662,plain,
( member(sK3(A,difference(A,B)),C)
| member(sK3(A,difference(A,B)),difference(A,C))
| difference(A,B) = A ),
inference(resolve,[status(thm)],[c_67,c_30]) ).
cnf(c_23051,plain,
( ~ member(sK3(A,difference(A,B)),difference(A,B))
| difference(A,B) = A
| difference(A,B) = A ),
inference(resolve,[status(thm)],[c_67,c_21]) ).
cnf(c_665,plain,
( ~ member(sK3(A,difference(A,B)),difference(A,B))
| difference(A,B) = A ),
inference(copy,[status(thm)],[c_23051]) ).
cnf(c_23003,negated_conjecture,
~ member(sK3(sK1,difference(sK1,sK2)),difference(sK1,sK2)),
inference(resolve,[status(thm)],[c_665,c_638]) ).
cnf(c_23052,plain,
( member(sK3(sK1,difference(sK1,sK2)),sK2)
| difference(sK1,sK2) = sK1 ),
inference(resolve,[status(thm)],[c_23003,c_662]) ).
cnf(c_23022,negated_conjecture,
member(sK3(sK1,difference(sK1,sK2)),sK2),
inference(resolve,[status(thm)],[c_638,c_23052]) ).
cnf(c_23053,plain,
( member(sK3(sK1,difference(sK1,sK2)),intersection(sK1,sK2))
| difference(sK1,sK2) = sK1 ),
inference(resolve,[status(thm)],[c_23022,c_659]) ).
cnf(c_23054,plain,
( member(sK3(sK1,difference(sK1,sK2)),empty_set)
| difference(sK1,sK2) = sK1 ),
inference(paramod,[status(thm)],[c_637,c_23053]) ).
cnf(c_23055,negated_conjecture,
member(sK3(sK1,difference(sK1,sK2)),empty_set),
inference(resolve,[status(thm)],[c_638,c_23054]) ).
cnf(c_23046,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_29,c_23055]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET611+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n017.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 07:54:33 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 214754 was started by sandbox2 on n017,
% 0.18/0.45 % Sat Sep 26 07:54:33 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 108.12/14.95
% 108.12/14.95 % given #500 (T,wt=12): 790 intersection(A,B) = B | C != B | member(f4(B),C). [resolve(718,b,24,b)].
% 108.12/14.95
% 108.12/14.95 % given #1000 (F,wt=5): 7311 -subset(c1,intersection(A,c2)). [para(25(a,1),7308(a,2))].
% 108.12/14.95
% 108.12/14.95 % given #1500 (T,wt=13): 3125 member(f3(difference(c1,empty_set),difference(A,intersection(c1,c1))),difference(c1,empty_set)). [resolve(2764,a,19,a)].
% 108.12/14.95
% 108.12/14.95 % given #2000 (F,wt=11): 7735 -member(f3(intersection(c1,c1),c2),intersection(A,difference(B,c1))). [ur(34,b,7235,a)].
% 108.12/14.95
% 108.12/14.95 % given #2500 (T,wt=13): 10193 member(f3(intersection(c1,c1),intersection(A,intersection(B,c2))),intersection(c1,c1)). [resolve(8487,a,19,a)].
% 108.12/14.95
% 108.12/14.95 % given #3000 (F,wt=7): 18984 -member(f1(empty_set,c1),difference(c2,A)). [back_rewrite(18844),rewrite([18951(4)])].
% 108.12/14.95
% 108.12/14.95 % given #3500 (A,wt=17): 641 intersection(A,B) = empty_set | member(f4(B),intersection(C,intersection(B,B))) | -member(f4(B),C). [resolve(520,b,33,c)].
% 108.12/14.95
% 108.12/14.95 % SZS status Theorem for theBenchmark
% 108.12/14.95
% 108.12/14.95 % Proof 1 at 11.66 (+ 2.75) seconds.
% 108.12/14.95 % Length of proof is 38.
% 108.12/14.95 % Level of proof is 11.
% 108.12/14.95 % Maximum clause weight is 21.000.
% 108.12/14.95 % Given clauses 3712.
% 108.12/14.95
% 108.12/14.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------