%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU245+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:51:29 PM UTC 2026
% Result : Theorem 6.03s 1.29s
% Output : Proof 6.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 9
% Syntax : Number of formulae : 69 ( 19 unt; 0 def)
% Number of atoms : 168 ( 24 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 161 ( 62 ~; 65 |; 24 &)
% ( 4 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 90 ( 5 sgn 51 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f25,axiom,
! [A,B,C] :
( C = set_intersection2(A,B)
<=> ! [D] :
( in(D,C)
<=> ( in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_xboole_0) ).
fof(f25_nnf,plain,
! [A,B,C] :
( ( ? [D] :
( ( in(D,B)
& in(D,A)
& ~ in(D,C) )
| ( ( ~ in(D,B)
| ~ in(D,A) )
& in(D,C) ) )
| C = set_intersection2(A,B) )
& ( ! [D] :
( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [C,A,B,D] :
( ( ( in(sk9(A,B,C),B)
& in(sk9(A,B,C),A)
& ~ in(sk9(A,B,C),C) )
| ( ( ~ in(sk9(A,B,C),B)
| ~ in(sk9(A,B,C),A) )
& in(sk9(A,B,C),C) )
| C = set_intersection2(A,B) )
& ( ( ( ~ in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_intersection2(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f25_nnf]) ).
cnf(c40,plain,
( ~ in(X3,X1)
| ~ in(X3,X0)
| in(X3,X2)
| X2 != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p149,plain,
( ~ in(X0,X2)
| ~ in(X0,X1)
| in(X0,set_intersection2(X1,X2)) ),
inference(equality_resolution,[status(thm)],[c40]) ).
fof(f23,axiom,
! [A] :
( relation(A)
=> ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_wellord1) ).
fof(f23_nnf,plain,
! [A] :
( ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B))
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A,B] :
( relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B))
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c30,plain,
( relation_restriction(X0,X1) = set_intersection2(X0,cartesian_product2(X1,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
fof(f24,conjecture,
! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_wellord1) ).
fof(f24_neg,negated_conjecture,
~ ! [A,B,C] :
( relation(C)
=> ( in(A,relation_restriction(C,B))
<=> ( in(A,cartesian_product2(B,B))
& in(A,C) ) ) ),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f24_nnf,plain,
? [A,B,C] :
( ( ( in(A,cartesian_product2(B,B))
& in(A,C)
& ~ in(A,relation_restriction(C,B)) )
| ( ( ~ in(A,cartesian_product2(B,B))
| ~ in(A,C) )
& in(A,relation_restriction(C,B)) ) )
& relation(C) ),
inference(nnf_transformation,[status(thm)],[f24_neg]) ).
fof(f24_sk,plain,
( ( ( in(sk6,cartesian_product2(sk7,sk7))
& in(sk6,sk8)
& ~ in(sk6,relation_restriction(sk8,sk7)) )
| ( ( ~ in(sk6,cartesian_product2(sk7,sk7))
| ~ in(sk6,sk8) )
& in(sk6,relation_restriction(sk8,sk7)) ) )
& relation(sk8) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk6,sk7,sk8])],[f24_nnf]) ).
cnf(c31,plain,
relation(sk8),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p75,plain,
relation_restriction(sk8,X0) = set_intersection2(sk8,cartesian_product2(X0,X0)),
inference(resolution,[status(thm)],[c30,c31]) ).
fof(f15,axiom,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(f15_nnf,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A,B] : set_intersection2(A,B) = set_intersection2(B,A),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c22,plain,
set_intersection2(X0,X1) = set_intersection2(X1,X0),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p113,plain,
set_intersection2(sk8,cartesian_product2(X0,X0)) = relation_restriction(sk8,X0),
inference(superposition,[status(thm)],[p75,c22]) ).
cnf(c38,plain,
( in(X3,X0)
| ~ in(X3,X2)
| X2 != set_intersection2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p120,plain,
( in(X0,X1)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(equality_resolution,[status(thm)],[c38]) ).
cnf(p131,plain,
( in(X0,sk8)
| ~ in(X0,relation_restriction(sk8,X1)) ),
inference(superposition,[status(thm)],[p113,p120]) ).
cnf(c33,plain,
( in(sk6,sk8)
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p142,plain,
( in(sk6,sk8)
| in(sk6,sk8) ),
inference(resolution,[status(thm)],[p131,c33]) ).
cnf(p143,plain,
in(sk6,sk8),
inference(factoring,[status(thm)],[p142]) ).
cnf(p424,plain,
( ~ in(sk6,X0)
| in(sk6,set_intersection2(sk8,X0)) ),
inference(resolution,[status(thm)],[p149,p143]) ).
cnf(p123,plain,
( in(X0,X2)
| ~ in(X0,set_intersection2(X1,X2)) ),
inference(resolution,[status(thm)],[c38,c22]) ).
cnf(p135,plain,
( in(X0,cartesian_product2(X1,X1))
| ~ in(X0,relation_restriction(sk8,X1)) ),
inference(superposition,[status(thm)],[p113,p123]) ).
cnf(c34,plain,
( in(sk6,cartesian_product2(sk7,sk7))
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f21,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f21_nnf,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A,B] :
( element(A,B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c28,plain,
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p101,plain,
( element(sk6,cartesian_product2(sk7,sk7))
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(resolution,[status(thm)],[c34,c28]) ).
cnf(p231,plain,
( element(sk6,cartesian_product2(sk7,sk7))
| in(sk6,cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p135,p101]) ).
cnf(p287,plain,
( element(sk6,cartesian_product2(sk7,sk7))
| element(sk6,cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p231,c28]) ).
cnf(p337,plain,
element(sk6,cartesian_product2(sk7,sk7)),
inference(factoring,[status(thm)],[p287]) ).
fof(f12,axiom,
! [A,B] :
( element(A,B)
=> ( in(A,B)
| empty(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f12_nnf,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] :
( in(A,B)
| empty(B)
| ~ element(A,B) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c19,plain,
( in(X0,X1)
| empty(X1)
| ~ element(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p338,plain,
( in(sk6,cartesian_product2(sk7,sk7))
| empty(cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p337,c19]) ).
cnf(p440,plain,
( empty(cartesian_product2(sk7,sk7))
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(resolution,[status(thm)],[p424,p338]) ).
cnf(c35,plain,
( ~ in(sk6,relation_restriction(sk8,sk7))
| ~ in(sk6,cartesian_product2(sk7,sk7))
| ~ in(sk6,sk8) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p147,plain,
( ~ in(sk6,relation_restriction(sk8,sk7))
| ~ in(sk6,cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p143,c35]) ).
cnf(p340,plain,
( ~ in(sk6,relation_restriction(sk8,sk7))
| empty(cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p338,p147]) ).
cnf(p444,plain,
( empty(cartesian_product2(sk7,sk7))
| empty(cartesian_product2(sk7,sk7)) ),
inference(resolution,[status(thm)],[p440,p340]) ).
cnf(p447,plain,
empty(cartesian_product2(sk7,sk7)),
inference(factoring,[status(thm)],[p444]) ).
fof(f13,axiom,
! [A] :
( empty(A)
=> A = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f13_nnf,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A] :
( A = empty_set
| ~ empty(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c20,plain,
( X0 = empty_set
| ~ empty(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p449,plain,
cartesian_product2(sk7,sk7) = empty_set,
inference(resolution,[status(thm)],[p447,c20]) ).
cnf(p458,plain,
empty_set = relation_restriction(sk8,sk7),
inference(superposition,[status(thm)],[p449,p113]) ).
cnf(p490,plain,
relation_restriction(sk8,sk7) = empty_set,
inference(superposition,[status(thm)],[p458,p113]) ).
fof(f22,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f22_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c29,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p99,plain,
( ~ empty(cartesian_product2(sk7,sk7))
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(resolution,[status(thm)],[c34,c29]) ).
cnf(p451,plain,
( ~ empty(empty_set)
| in(sk6,relation_restriction(sk8,sk7)) ),
inference(demodulation,[status(thm)],[p449,p99]) ).
cnf(p492,plain,
( ~ empty(empty_set)
| in(sk6,empty_set) ),
inference(demodulation,[status(thm)],[p490,p451]) ).
fof(f5,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f5_nnf,plain,
empty(empty_set),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c12,plain,
empty(empty_set),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p496,plain,
in(sk6,empty_set),
inference(resolution,[status(thm)],[p492,c12]) ).
cnf(p497,plain,
~ empty(empty_set),
inference(resolution,[status(thm)],[p496,c29]) ).
cnf(p525,plain,
$false,
inference(resolution,[status(thm)],[p497,c12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU245+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 13:18:31 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.03/1.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.03/1.29 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------