%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU102+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:50:56 PM UTC 2026
% Result : Theorem 48.58s 12.81s
% Output : Proof 48.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 3
% Syntax : Number of formulae : 35 ( 7 unt; 0 def)
% Number of atoms : 110 ( 9 equ)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 110 ( 35 ~; 51 |; 18 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 39 ( 0 sgn 24 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f23,axiom,
! [A,B,C] :
( ( element(C,A)
& element(B,A)
& preboolean(A)
& ~ empty(A) )
=> prebool_difference(A,B,C) = set_difference(B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_finsub_1) ).
fof(f23_nnf,plain,
! [A,B,C] :
( prebool_difference(A,B,C) = set_difference(B,C)
| ~ element(C,A)
| ~ element(B,A)
| ~ preboolean(A)
| empty(A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A,B,C] :
( prebool_difference(A,B,C) = set_difference(B,C)
| ~ element(C,A)
| ~ element(B,A)
| ~ preboolean(A)
| empty(A) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c44,plain,
( prebool_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X2,X0)
| ~ element(X1,X0)
| ~ preboolean(X0)
| empty(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
fof(f25,conjecture,
! [A,B,C] :
( ( preboolean(C)
& ~ empty(C) )
=> ( ( element(B,C)
& element(A,C) )
=> element(set_intersection2(A,B),C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_finsub_1) ).
fof(f25_neg,negated_conjecture,
~ ! [A,B,C] :
( ( preboolean(C)
& ~ empty(C) )
=> ( ( element(B,C)
& element(A,C) )
=> element(set_intersection2(A,B),C) ) ),
inference(negated_conjecture,[status(cth)],[f25]) ).
fof(f25_nnf,plain,
? [A,B,C] :
( ~ element(set_intersection2(A,B),C)
& element(B,C)
& element(A,C)
& preboolean(C)
& ~ empty(C) ),
inference(nnf_transformation,[status(thm)],[f25_neg]) ).
fof(f25_sk,plain,
( ~ element(set_intersection2(sk10,sk11),sk12)
& element(sk11,sk12)
& element(sk10,sk12)
& preboolean(sk12)
& ~ empty(sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk10,sk11,sk12])],[f25_nnf]) ).
cnf(c47,plain,
preboolean(sk12),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p306,plain,
( prebool_difference(sk12,X0,X1) = set_difference(X0,X1)
| ~ element(X1,sk12)
| ~ element(X0,sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[c44,c47]) ).
cnf(c48,plain,
element(sk10,sk12),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p3112,plain,
( prebool_difference(sk12,sk10,X0) = set_difference(sk10,X0)
| ~ element(X0,sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[p306,c48]) ).
cnf(c49,plain,
element(sk11,sk12),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p3770,plain,
( prebool_difference(sk12,sk10,sk11) = set_difference(sk10,sk11)
| empty(sk12) ),
inference(resolution,[status(thm)],[p3112,c49]) ).
fof(f6,axiom,
! [A,B,C] :
( ( element(C,A)
& element(B,A)
& preboolean(A)
& ~ empty(A) )
=> element(prebool_difference(A,B,C),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_finsub_1) ).
fof(f6_nnf,plain,
! [A,B,C] :
( element(prebool_difference(A,B,C),A)
| ~ element(C,A)
| ~ element(B,A)
| ~ preboolean(A)
| empty(A) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] :
( element(prebool_difference(A,B,C),A)
| ~ element(C,A)
| ~ element(B,A)
| ~ preboolean(A)
| empty(A) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c7,plain,
( element(prebool_difference(X0,X1,X2),X0)
| ~ element(X2,X0)
| ~ element(X1,X0)
| ~ preboolean(X0)
| empty(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p75,plain,
( element(prebool_difference(sk12,X0,X1),sk12)
| ~ element(X1,sk12)
| ~ element(X0,sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[c7,c47]) ).
cnf(p78,plain,
( element(prebool_difference(sk12,sk10,X0),sk12)
| ~ element(X0,sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[p75,c48]) ).
cnf(p90,plain,
( element(prebool_difference(sk12,sk10,sk11),sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[p78,c49]) ).
cnf(p3942,plain,
( element(set_difference(sk10,sk11),sk12)
| empty(sk12)
| empty(sk12) ),
inference(superposition,[status(thm)],[p3770,p90]) ).
cnf(p4016,plain,
( element(set_difference(sk10,sk11),sk12)
| empty(sk12) ),
inference(factoring,[status(thm)],[p3942]) ).
cnf(p4030,plain,
( prebool_difference(sk12,sk10,set_difference(sk10,sk11)) = set_intersection2(sk10,sk11)
| empty(sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[p4016,p3112]) ).
cnf(p5023,plain,
( prebool_difference(sk12,sk10,set_difference(sk10,sk11)) = set_intersection2(sk10,sk11)
| empty(sk12) ),
inference(factoring,[status(thm)],[p4030]) ).
cnf(p97,plain,
( element(prebool_difference(sk12,sk10,prebool_difference(sk12,sk10,sk11)),sk12)
| empty(sk12)
| empty(sk12) ),
inference(resolution,[status(thm)],[p90,p78]) ).
cnf(p159,plain,
( element(prebool_difference(sk12,sk10,prebool_difference(sk12,sk10,sk11)),sk12)
| empty(sk12) ),
inference(factoring,[status(thm)],[p97]) ).
cnf(p3943,plain,
( element(prebool_difference(sk12,sk10,set_difference(sk10,sk11)),sk12)
| empty(sk12)
| empty(sk12) ),
inference(superposition,[status(thm)],[p3770,p159]) ).
cnf(p4087,plain,
( element(prebool_difference(sk12,sk10,set_difference(sk10,sk11)),sk12)
| empty(sk12) ),
inference(factoring,[status(thm)],[p3943]) ).
cnf(p5024,plain,
( element(set_intersection2(sk10,sk11),sk12)
| empty(sk12)
| empty(sk12) ),
inference(superposition,[status(thm)],[p5023,p4087]) ).
cnf(p5027,plain,
( element(set_intersection2(sk10,sk11),sk12)
| empty(sk12) ),
inference(factoring,[status(thm)],[p5024]) ).
cnf(c50,plain,
~ element(set_intersection2(sk10,sk11),sk12),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p5028,plain,
empty(sk12),
inference(resolution,[status(thm)],[p5027,c50]) ).
cnf(c46,plain,
~ empty(sk12),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p5032,plain,
$false,
inference(resolution,[status(thm)],[p5028,c46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU102+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.37 % Computer : n002.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Thu Sep 24 12:48:12 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 48.58/12.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 48.58/12.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------