%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU223+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:24 PM UTC 2026
% Result : Theorem 101.51s 13.24s
% Output : Proof 101.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 30
% Syntax : Number of formulae : 180 ( 97 unt; 0 def)
% Number of atoms : 405 ( 118 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 434 ( 209 ~; 126 |; 75 &)
% ( 9 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 8 con; 0-4 aty)
% Number of variables : 301 ( 39 sgn 173 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f219,conjecture,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_dom_restriction(C,A)))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_funct_1) ).
fof(f219_neg,negated_conjecture,
~ ! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(B,relation_dom(relation_dom_restriction(C,A)))
=> apply(relation_dom_restriction(C,A),B) = apply(C,B) ) ),
inference(negated_conjecture,[status(cth)],[f219]) ).
fof(f219_nnf,plain,
? [A,B,C] :
( apply(relation_dom_restriction(C,A),B) != apply(C,B)
& in(B,relation_dom(relation_dom_restriction(C,A)))
& function(C)
& relation(C) ),
inference(nnf_transformation,[status(thm)],[f219_neg]) ).
fof(f219_sk,plain,
( apply(relation_dom_restriction(sk79,sk77),sk78) != apply(sk79,sk78)
& in(sk78,relation_dom(relation_dom_restriction(sk79,sk77)))
& function(sk79)
& relation(sk79) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk77,sk78,sk79])],[f219_nnf]) ).
cnf(c482,plain,
apply(relation_dom_restriction(sk79,sk77),sk78) != apply(sk79,sk78),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(t130,plain,
eq(apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)) = false,
inference(equality_encoding,[status(esa)],[c482]) ).
cnf(t1131,plain,
eq(apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)) = false,
inference(orient,[status(thm)],[t130]) ).
fof(f228,lemma,
! [A,B,C] :
( ( function(C)
& relation(C) )
=> ( in(ordered_pair(A,B),C)
<=> ( B = apply(C,A)
& in(A,relation_dom(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_funct_1) ).
fof(f228_nnf,plain,
! [A,B,C] :
( ( ( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
! [C,A,B] :
( ( ( B != apply(C,A)
| ~ in(A,relation_dom(C))
| in(ordered_pair(A,B),C) )
& ( ( B = apply(C,A)
& in(A,relation_dom(C)) )
| ~ in(ordered_pair(A,B),C) ) )
| ~ function(C)
| ~ relation(C) ),
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c498,plain,
( X1 = apply(X2,X0)
| ~ in(ordered_pair(X0,X1),X2)
| ~ function(X2)
| ~ relation(X2) ),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(t206,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(ordered_pair(X2,X3),X1),true,X3,apply(X1,X2)),apply(X1,X2)),apply(X1,X2)) = apply(X1,X2),
inference(equality_encoding,[status(esa)],[c498]) ).
cnf(t961,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(ordered_pair(X2,X3),X1),true,X3,apply(X1,X2)),apply(X1,X2)),apply(X1,X2)) = apply(X1,X2),
inference(orient,[status(thm)],[t206]) ).
fof(f25,axiom,
! [A,B] :
( subset(A,B)
<=> ! [C] :
( in(C,A)
=> in(C,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f25_nnf,plain,
! [A,B] :
( ( ? [C] :
( ~ in(C,B)
& in(C,A) )
| subset(A,B) )
& ( ! [C] :
( in(C,B)
| ~ in(C,A) )
| ~ subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [A,B,C] :
( ( ( ~ in(sk32(A,B),B)
& in(sk32(A,B),A) )
| subset(A,B) )
& ( in(C,B)
| ~ in(C,A)
| ~ subset(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk32])],[f25_nnf]) ).
cnf(c129,plain,
( in(X2,X1)
| ~ in(X2,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t176,plain,
ifeq(subset(X1,X2),true,ifeq(in(X3,X1),true,in(X3,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c129]) ).
cnf(t336,plain,
ifeq(subset(X1,X2),true,ifeq(in(X3,X1),true,in(X3,X2),true),true) = true,
inference(orient,[status(thm)],[t176]) ).
fof(f226,lemma,
! [A,B] :
( relation(B)
=> subset(relation_dom_restriction(B,A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t88_relat_1) ).
fof(f226_nnf,plain,
! [A,B] :
( subset(relation_dom_restriction(B,A),B)
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f226]) ).
fof(f226_sk,plain,
! [B,A] :
( subset(relation_dom_restriction(B,A),B)
| ~ relation(B) ),
inference(skolemisation,[status(esa)],[f226_nnf]) ).
cnf(c495,plain,
( subset(relation_dom_restriction(X1,X0),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(t148,plain,
ifeq(relation(X1),true,subset(relation_dom_restriction(X1,X2),X1),true) = true,
inference(equality_encoding,[status(esa)],[c495]) ).
cnf(t334,plain,
ifeq(relation(X1),true,subset(relation_dom_restriction(X1,X2),X1),true) = true,
inference(orient,[status(thm)],[t148]) ).
cnf(c479,plain,
relation(sk79),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(t6,plain,
relation(sk79) = true,
inference(equality_encoding,[status(esa)],[c479]) ).
cnf(t672,plain,
relation(sk79) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t673,plain,
true = ifeq(true,true,subset(relation_dom_restriction(sk79,X1),sk79),true),
inference(cp,[status(thm)],[t334,t672]) ).
cnf(t69,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t222,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t69]) ).
cnf(t27781,plain,
true = subset(relation_dom_restriction(sk79,X1),sk79),
inference(step,[status(thm)],[t673,t222]) ).
cnf(t1872,plain,
subset(relation_dom_restriction(sk79,X1),sk79) = true,
inference(orient,[status(thm)],[t27781]) ).
cnf(t1878,plain,
true = ifeq(true,true,ifeq(in(X1,relation_dom_restriction(sk79,X2)),true,in(X1,sk79),true),true),
inference(cp,[status(thm)],[t336,t1872]) ).
cnf(t28281,plain,
true = ifeq(in(X1,relation_dom_restriction(sk79,X2)),true,in(X1,sk79),true),
inference(step,[status(thm)],[t1878,t222]) ).
cnf(t12176,plain,
ifeq(in(X1,relation_dom_restriction(sk79,X2)),true,in(X1,sk79),true) = true,
inference(orient,[status(thm)],[t28281]) ).
fof(f27,axiom,
! [A] :
( ( function(A)
& relation(A) )
=> ! [B,C] :
( ( ~ in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> C = empty_set ) )
& ( in(B,relation_dom(A))
=> ( C = apply(A,B)
<=> in(ordered_pair(B,C),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f27_nnf,plain,
! [A] :
( ! [B,C] :
( ( ( ( C != empty_set
| C = apply(A,B) )
& ( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ( ( ( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [A,B,C] :
( ( ( ( ( C != empty_set
| C = apply(A,B) )
& ( C = empty_set
| C != apply(A,B) ) )
| in(B,relation_dom(A)) )
& ( ( ( ~ in(ordered_pair(B,C),A)
| C = apply(A,B) )
& ( in(ordered_pair(B,C),A)
| C != apply(A,B) ) )
| ~ in(B,relation_dom(A)) ) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c141,plain,
( in(ordered_pair(X1,X2),X0)
| X2 != apply(X0,X1)
| ~ in(X1,relation_dom(X0))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(t211,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,ifeq(X3,apply(X1,X2),in(ordered_pair(X2,X3),X1),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c141]) ).
cnf(t319,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,ifeq(X3,apply(X1,X2),in(ordered_pair(X2,X3),X1),true),true),true),true) = true,
inference(orient,[status(thm)],[t211]) ).
cnf(t321,plain,
true = ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,in(ordered_pair(X2,apply(X1,X2)),X1),true),true),true),
inference(cp,[status(thm)],[t319,t222]) ).
cnf(t27420,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,ifeq(in(X2,relation_dom(X1)),true,in(ordered_pair(X2,apply(X1,X2)),X1),true),true),true) = true,
inference(orient,[status(thm)],[t321]) ).
cnf(c481,plain,
in(sk78,relation_dom(relation_dom_restriction(sk79,sk77))),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(t86,plain,
in(sk78,relation_dom(relation_dom_restriction(sk79,sk77))) = true,
inference(equality_encoding,[status(esa)],[c481]) ).
cnf(t412,plain,
in(sk78,relation_dom(relation_dom_restriction(sk79,sk77))) = true,
inference(orient,[status(thm)],[t86]) ).
cnf(t27435,plain,
true = ifeq(relation(relation_dom_restriction(sk79,sk77)),true,ifeq(function(relation_dom_restriction(sk79,sk77)),true,ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),true),true),true),
inference(cp,[status(thm)],[t27420,t412]) ).
fof(f68,axiom,
! [A,B] :
( relation(A)
=> relation(relation_dom_restriction(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f68_nnf,plain,
! [A,B] :
( relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f68]) ).
fof(f68_sk,plain,
! [A,B] :
( relation(relation_dom_restriction(A,B))
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f68_nnf]) ).
cnf(c238,plain,
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f68_sk]) ).
cnf(t135,plain,
ifeq(relation(X1),true,relation(relation_dom_restriction(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c238]) ).
cnf(t331,plain,
ifeq(relation(X1),true,relation(relation_dom_restriction(X1,X2)),true) = true,
inference(orient,[status(thm)],[t135]) ).
cnf(t674,plain,
true = ifeq(true,true,relation(relation_dom_restriction(sk79,X1)),true),
inference(cp,[status(thm)],[t331,t672]) ).
cnf(t27747,plain,
true = relation(relation_dom_restriction(sk79,X1)),
inference(step,[status(thm)],[t674,t222]) ).
cnf(t1617,plain,
relation(relation_dom_restriction(sk79,X1)) = true,
inference(orient,[status(thm)],[t27747]) ).
cnf(t28515,plain,
true = ifeq(true,true,ifeq(function(relation_dom_restriction(sk79,sk77)),true,ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),true),true),true),
inference(step,[status(thm)],[t27435,t1617]) ).
cnf(t28516,plain,
true = ifeq(function(relation_dom_restriction(sk79,sk77)),true,ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),true),true),
inference(step,[status(thm)],[t28515,t222]) ).
fof(f90,axiom,
! [A,B] :
( ( function(A)
& relation(A) )
=> ( function(relation_dom_restriction(A,B))
& relation(relation_dom_restriction(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_funct_1) ).
fof(f90_nnf,plain,
! [A,B] :
( ( function(relation_dom_restriction(A,B))
& relation(relation_dom_restriction(A,B)) )
| ~ function(A)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
! [A,B] :
( ( function(relation_dom_restriction(A,B))
& relation(relation_dom_restriction(A,B)) )
| ~ function(A)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c269,plain,
( function(relation_dom_restriction(X0,X1))
| ~ function(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(t169,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,function(relation_dom_restriction(X1,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c269]) ).
cnf(t330,plain,
ifeq(relation(X1),true,ifeq(function(X1),true,function(relation_dom_restriction(X1,X2)),true),true) = true,
inference(orient,[status(thm)],[t169]) ).
cnf(c480,plain,
function(sk79),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(t2,plain,
function(sk79) = true,
inference(equality_encoding,[status(esa)],[c480]) ).
cnf(t804,plain,
function(sk79) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t805,plain,
true = ifeq(relation(sk79),true,ifeq(true,true,function(relation_dom_restriction(sk79,X1)),true),true),
inference(cp,[status(thm)],[t330,t804]) ).
cnf(t27749,plain,
true = ifeq(true,true,ifeq(true,true,function(relation_dom_restriction(sk79,X1)),true),true),
inference(step,[status(thm)],[t805,t672]) ).
cnf(t27750,plain,
true = ifeq(true,true,function(relation_dom_restriction(sk79,X1)),true),
inference(step,[status(thm)],[t27749,t222]) ).
cnf(t27751,plain,
true = function(relation_dom_restriction(sk79,X1)),
inference(step,[status(thm)],[t27750,t222]) ).
cnf(t1716,plain,
function(relation_dom_restriction(sk79,X1)) = true,
inference(orient,[status(thm)],[t27751]) ).
cnf(t28517,plain,
true = ifeq(true,true,ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),true),true),
inference(step,[status(thm)],[t28516,t1716]) ).
cnf(t28518,plain,
true = ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),true),
inference(step,[status(thm)],[t28517,t222]) ).
cnf(t28519,plain,
true = in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)),
inference(step,[status(thm)],[t28518,t222]) ).
cnf(t27477,plain,
in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),relation_dom_restriction(sk79,sk77)) = true,
inference(orient,[status(thm)],[t28519]) ).
cnf(t27479,plain,
true = ifeq(true,true,in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),sk79),true),
inference(cp,[status(thm)],[t12176,t27477]) ).
cnf(t28522,plain,
true = in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),sk79),
inference(step,[status(thm)],[t27479,t222]) ).
cnf(t27517,plain,
in(ordered_pair(sk78,apply(relation_dom_restriction(sk79,sk77),sk78)),sk79) = true,
inference(orient,[status(thm)],[t28522]) ).
cnf(t27534,plain,
apply(sk79,sk78) = ifeq(relation(sk79),true,ifeq(function(sk79),true,ifeq(true,true,apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)),apply(sk79,sk78)),apply(sk79,sk78)),
inference(cp,[status(thm)],[t961,t27517]) ).
cnf(t28523,plain,
apply(sk79,sk78) = ifeq(true,true,ifeq(function(sk79),true,ifeq(true,true,apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)),apply(sk79,sk78)),apply(sk79,sk78)),
inference(step,[status(thm)],[t27534,t672]) ).
cnf(t28524,plain,
apply(sk79,sk78) = ifeq(function(sk79),true,ifeq(true,true,apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)),apply(sk79,sk78)),
inference(step,[status(thm)],[t28523,t222]) ).
cnf(t28525,plain,
apply(sk79,sk78) = ifeq(true,true,ifeq(true,true,apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)),apply(sk79,sk78)),
inference(step,[status(thm)],[t28524,t804]) ).
cnf(t28526,plain,
apply(sk79,sk78) = ifeq(true,true,apply(relation_dom_restriction(sk79,sk77),sk78),apply(sk79,sk78)),
inference(step,[status(thm)],[t28525,t222]) ).
cnf(t28527,plain,
apply(sk79,sk78) = apply(relation_dom_restriction(sk79,sk77),sk78),
inference(step,[status(thm)],[t28526,t222]) ).
cnf(t27551,plain,
apply(relation_dom_restriction(sk79,sk77),sk78) = apply(sk79,sk78),
inference(orient,[status(thm)],[t28527]) ).
cnf(t28528,plain,
eq(apply(sk79,sk78),apply(sk79,sk78)) = false,
inference(step,[status(thm)],[t1131,t27551]) ).
cnf(t24,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t854,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t28529,plain,
true = false,
inference(step,[status(thm)],[t28528,t854]) ).
cnf(t27581,plain,
true = false,
inference(rw,[status(thm)],[t28529]) ).
cnf(t27584,plain,
false = true,
inference(orient,[status(thm)],[t27581]) ).
fof(f0,axiom,
! [A,B] :
( in(A,B)
=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f0_nnf,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( ~ in(B,A)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ~ in(X1,X0)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f1,axiom,
! [A,B] :
( proper_subset(A,B)
=> ~ proper_subset(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_xboole_0) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ proper_subset(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ proper_subset(X1,X0)
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f17,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f17_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B] :
( ( in(sk19(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19])],[f17_nnf]) ).
cnf(c78,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f31,axiom,
! [A,B,C] :
( C = set_difference(A,B)
<=> ! [D] :
( in(D,C)
<=> ( ~ in(D,B)
& in(D,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(f31_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_difference(A,B) )
& ( ! [D] :
( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk40(A,B,C),B)
& in(sk40(A,B,C),A)
& ~ in(sk40(A,B,C),C) )
| ( ( in(sk40(A,B,C),B)
| ~ in(sk40(A,B,C),A) )
& in(sk40(A,B,C),C) )
| C = set_difference(A,B) )
& ( ( ( in(D,B)
| ~ in(D,A)
| in(D,C) )
& ( ( ~ in(D,B)
& in(D,A) )
| ~ in(D,C) ) )
| C != set_difference(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk40])],[f31_nnf]) ).
cnf(c162,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f41,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f41_nnf,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [A,B] :
( ( A = B
| ~ subset(A,B)
| proper_subset(A,B) )
& ( ( A != B
& subset(A,B) )
| ~ proper_subset(A,B) ) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c209,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f80,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f80_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c256,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
fof(f82,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f82_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c258,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
fof(f85,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f85_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c262,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
fof(f88,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f88_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c266,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
fof(f103,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f103_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f103_nnf]) ).
cnf(c286,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
fof(f104,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f104_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f104_nnf]) ).
cnf(c287,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
fof(f106,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f106_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c289,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
fof(f121,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f121_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
( relation(sk60)
& ~ empty(sk60) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk60])],[f121_nnf]) ).
cnf(c316,plain,
~ empty(sk60),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
fof(f123,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f123_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
~ empty(sk62),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk62])],[f123_nnf]) ).
cnf(c320,plain,
~ empty(sk62),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
fof(f184,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] :
( in(C,B)
& in(C,A) ) )
& ~ ( ! [C] :
~ ( in(C,B)
& in(C,A) )
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(f184_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] :
( ~ in(C,B)
| ~ in(C,A) ) )
& ( ? [C] :
( in(C,B)
& in(C,A) )
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk70(A,B),B)
& in(sk70(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk70])],[f184_nnf]) ).
cnf(c420,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
fof(f200,lemma,
! [A,B] :
( ~ ( disjoint(A,B)
& ? [C] : in(C,set_intersection2(A,B)) )
& ~ ( ! [C] : ~ in(C,set_intersection2(A,B))
& ~ disjoint(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(f200_nnf,plain,
! [A,B] :
( ( ~ disjoint(A,B)
| ! [C] : ~ in(C,set_intersection2(A,B)) )
& ( ? [C] : in(C,set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk71(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk71])],[f200_nnf]) ).
cnf(c438,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f203,lemma,
! [A,B,C] :
( element(C,powerset(A))
=> ~ ( in(B,C)
& in(B,subset_complement(A,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_subset_1) ).
fof(f203_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f203]) ).
fof(f203_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f203_nnf]) ).
cnf(c454,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
fof(f207,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f207_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f207]) ).
fof(f207_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f207_nnf]) ).
cnf(c460,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
fof(f209,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f209_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f209]) ).
fof(f209_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f209_nnf]) ).
cnf(c463,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
fof(f214,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f214_nnf,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
! [A,B] :
( ( in(B,A)
| set_difference(A,singleton(B)) = A )
& ( ~ in(B,A)
| set_difference(A,singleton(B)) != A ) ),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c470,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
fof(f222,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f222_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c488,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c78,c162,c209,c256,c258,c262,c266,c286,c287,c289,c316,c320,c420,c438,c454,c460,c463,c470,c482,c488]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t27584]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU223+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.33 % Computer : n009.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Thu Sep 24 13:15:58 UTC 2026
% 0.07/0.33 % CPUTime :
% 0.07/0.33 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 101.51/13.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 101.51/13.24 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------