%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SEU196+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 : n014.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:18 PM UTC 2026
% Result : Theorem 90.21s 12.62s
% Output : Proof 90.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 28
% Syntax : Number of formulae : 140 ( 69 unt; 0 def)
% Number of atoms : 290 ( 65 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 322 ( 172 ~; 88 |; 48 &)
% ( 5 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 7 con; 0-4 aty)
% Number of variables : 238 ( 26 sgn 152 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f183,conjecture,
! [A,B] :
( relation(B)
=> subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t99_relat_1) ).
fof(f183_neg,negated_conjecture,
~ ! [A,B] :
( relation(B)
=> subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ),
inference(negated_conjecture,[status(cth)],[f183]) ).
fof(f183_nnf,plain,
? [A,B] :
( ~ subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B))
& relation(B) ),
inference(nnf_transformation,[status(thm)],[f183_neg]) ).
fof(f183_sk,plain,
( ~ subset(relation_rng(relation_dom_restriction(sk58,sk57)),relation_rng(sk58))
& relation(sk58) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk57,sk58])],[f183_nnf]) ).
cnf(c371,plain,
~ subset(relation_rng(relation_dom_restriction(sk58,sk57)),relation_rng(sk58)),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(t157,plain,
subset(relation_rng(relation_dom_restriction(sk58,sk57)),relation_rng(sk58)) = false,
inference(equality_encoding,[status(esa)],[c371]) ).
cnf(t1761,plain,
subset(relation_rng(relation_dom_restriction(sk58,sk57)),relation_rng(sk58)) = false,
inference(orient,[status(thm)],[t157]) ).
fof(f145,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> subset(relation_rng(relation_composition(A,B)),relation_rng(B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_relat_1) ).
fof(f145_nnf,plain,
! [A] :
( ! [B] :
( subset(relation_rng(relation_composition(A,B)),relation_rng(B))
| ~ relation(B) )
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f145]) ).
fof(f145_sk,plain,
! [A,B] :
( subset(relation_rng(relation_composition(A,B)),relation_rng(B))
| ~ relation(B)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f145_nnf]) ).
cnf(c321,plain,
( subset(relation_rng(relation_composition(X0,X1)),relation_rng(X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(t220,plain,
ifeq(relation(X1),true,ifeq(relation(X2),true,subset(relation_rng(relation_composition(X1,X2)),relation_rng(X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c321]) ).
cnf(t324,plain,
ifeq(relation(X1),true,ifeq(relation(X2),true,subset(relation_rng(relation_composition(X1,X2)),relation_rng(X2)),true),true) = true,
inference(orient,[status(thm)],[t220]) ).
fof(f182,lemma,
! [A,B] :
( relation(B)
=> relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t94_relat_1) ).
fof(f182_nnf,plain,
! [A,B] :
( relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B)
| ~ relation(B) ),
inference(nnf_transformation,[status(thm)],[f182]) ).
fof(f182_sk,plain,
! [B,A] :
( relation_dom_restriction(B,A) = relation_composition(identity_relation(A),B)
| ~ relation(B) ),
inference(skolemisation,[status(esa)],[f182_nnf]) ).
cnf(c369,plain,
( relation_dom_restriction(X1,X0) = relation_composition(identity_relation(X0),X1)
| ~ relation(X1) ),
inference(cnf_transformation,[status(esa)],[f182_sk]) ).
cnf(hi297,axiom,
ifeq(relation(X0),true,relation_dom_restriction(X0,X1),relation_composition(identity_relation(X1),X0)) = relation_composition(identity_relation(X1),X0),
inference(equality_encoding,[status(esa)],[c369]) ).
cnf(c370,plain,
relation(sk58),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(hi298,negated_conjecture,
relation(sk58) = true,
inference(equality_encoding,[status(esa)],[c370]) ).
cnf(t133,plain,
relation_composition(identity_relation(X1),sk58) = relation_dom_restriction(sk58,X1),
inference(hyper_resolution,[status(thm)],[hi297,hi298]) ).
cnf(t1888,plain,
relation_composition(identity_relation(X1),sk58) = relation_dom_restriction(sk58,X1),
inference(orient,[status(thm)],[t133]) ).
cnf(t1898,plain,
true = ifeq(relation(identity_relation(X1)),true,ifeq(relation(sk58),true,subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)),true),true),
inference(cp,[status(thm)],[t324,t1888]) ).
fof(f54,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_relat_1) ).
fof(f54_nnf,plain,
! [A] : relation(identity_relation(A)),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [A] : relation(identity_relation(A)),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c190,plain,
relation(identity_relation(X0)),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(t40,plain,
relation(identity_relation(X1)) = true,
inference(equality_encoding,[status(esa)],[c190]) ).
cnf(t733,plain,
relation(identity_relation(X1)) = true,
inference(orient,[status(thm)],[t40]) ).
cnf(t4753,plain,
true = ifeq(true,true,ifeq(relation(sk58),true,subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)),true),true),
inference(step,[status(thm)],[t1898,t733]) ).
cnf(t106,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t245,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t106]) ).
cnf(t4754,plain,
true = ifeq(relation(sk58),true,subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)),true),
inference(step,[status(thm)],[t4753,t245]) ).
fof(f66,axiom,
! [A,B] :
( ( relation(B)
& relation(A) )
=> relation(set_union2(A,B)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_relat_1) ).
fof(f66_nnf,plain,
! [A,B] :
( relation(set_union2(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [A,B] :
( relation(set_union2(A,B))
| ~ relation(B)
| ~ relation(A) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c203,plain,
( relation(set_union2(X0,X1))
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(hi149,axiom,
ifeq(relation(X0),true,ifeq(relation(X1),true,relation(set_union2(X0,X1)),true),true) = true,
inference(equality_encoding,[status(esa)],[c203]) ).
cnf(t88,plain,
relation(set_union2(sk58,sk58)) = true,
inference(hyper_resolution,[status(thm)],[hi149,hi298,hi298]) ).
fof(f78,axiom,
! [A,B] : set_union2(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k2_xboole_0) ).
fof(f78_nnf,plain,
! [A,B] : set_union2(A,A) = A,
inference(nnf_transformation,[status(thm)],[f78]) ).
fof(f78_sk,plain,
! [A] : set_union2(A,A) = A,
inference(skolemisation,[status(esa)],[f78_nnf]) ).
cnf(c219,plain,
set_union2(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(t68,plain,
set_union2(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c219]) ).
cnf(t259,plain,
set_union2(X1,X1) = X1,
inference(orient,[status(thm)],[t68]) ).
cnf(t4424,plain,
relation(sk58) = true,
inference(step,[status(thm)],[t88,t259]) ).
cnf(t1073,plain,
relation(sk58) = true,
inference(orient,[status(thm)],[t4424]) ).
cnf(t4755,plain,
true = ifeq(true,true,subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)),true),
inference(step,[status(thm)],[t4754,t1073]) ).
cnf(t4756,plain,
true = subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)),
inference(step,[status(thm)],[t4755,t245]) ).
cnf(t4397,plain,
subset(relation_rng(relation_dom_restriction(sk58,X1)),relation_rng(sk58)) = true,
inference(orient,[status(thm)],[t4756]) ).
cnf(t4757,plain,
true = false,
inference(step,[status(thm)],[t1761,t4397]) ).
cnf(t4408,plain,
true = false,
inference(rw,[status(thm)],[t4757]) ).
cnf(t4409,plain,
false = true,
inference(orient,[status(thm)],[t4408]) ).
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(f12,axiom,
! [A] :
( A = empty_set
<=> ! [B] : ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f12_nnf,plain,
! [A] :
( ( ? [B] : in(B,A)
| A = empty_set )
& ( ! [B] : ~ in(B,A)
| A != empty_set ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] :
( ( in(sk11(A),A)
| A = empty_set )
& ( ~ in(B,A)
| A != empty_set ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f12_nnf]) ).
cnf(c47,plain,
( ~ in(X1,X0)
| X0 != empty_set ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f25,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(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_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)],[f25]) ).
fof(f25_sk,plain,
! [C,A,B,D] :
( ( ( ~ in(sk32(A,B,C),B)
& in(sk32(A,B,C),A)
& ~ in(sk32(A,B,C),C) )
| ( ( in(sk32(A,B,C),B)
| ~ in(sk32(A,B,C),A) )
& in(sk32(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,[sk32])],[f25_nnf]) ).
cnf(c127,plain,
( ~ in(X3,X1)
| ~ in(X3,X2)
| X2 != set_difference(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f34,axiom,
! [A,B] :
( proper_subset(A,B)
<=> ( A != B
& subset(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
fof(f34_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)],[f34]) ).
fof(f34_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)],[f34_nnf]) ).
cnf(c169,plain,
( X0 != X1
| ~ proper_subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f63,axiom,
! [A] : ~ empty(powerset(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f63_nnf,plain,
! [A] : ~ empty(powerset(A)),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [A] : ~ empty(powerset(A)),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c200,plain,
~ empty(powerset(X0)),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
fof(f65,axiom,
! [A,B] : ~ empty(ordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(f65_nnf,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [A,B] : ~ empty(ordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c202,plain,
~ empty(ordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
fof(f67,axiom,
! [A] : ~ empty(singleton(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(f67_nnf,plain,
! [A] : ~ empty(singleton(A)),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [A] : ~ empty(singleton(A)),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c204,plain,
~ empty(singleton(X0)),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
fof(f69,axiom,
! [A,B] : ~ empty(unordered_pair(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(f69_nnf,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [A,B] : ~ empty(unordered_pair(A,B)),
inference(skolemisation,[status(esa)],[f69_nnf]) ).
cnf(c206,plain,
~ empty(unordered_pair(X0,X1)),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
fof(f83,axiom,
! [A,B] : ~ proper_subset(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
fof(f83_nnf,plain,
! [A,B] : ~ proper_subset(A,A),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [A] : ~ proper_subset(A,A),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c224,plain,
~ proper_subset(X0,X0),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
fof(f84,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
fof(f84_nnf,plain,
! [A] : singleton(A) != empty_set,
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
! [A] : singleton(A) != empty_set,
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c225,plain,
singleton(X0) != empty_set,
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
fof(f86,lemma,
! [A,B] :
~ ( in(A,B)
& disjoint(singleton(A),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
fof(f86_nnf,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
! [A,B] :
( ~ in(A,B)
| ~ disjoint(singleton(A),B) ),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c227,plain,
( ~ in(X0,X1)
| ~ disjoint(singleton(X0),X1) ),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
fof(f99,axiom,
? [A] :
( relation(A)
& ~ empty(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(f99_nnf,plain,
? [A] :
( relation(A)
& ~ empty(A) ),
inference(nnf_transformation,[status(thm)],[f99]) ).
fof(f99_sk,plain,
( relation(sk48)
& ~ empty(sk48) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk48])],[f99_nnf]) ).
cnf(c249,plain,
~ empty(sk48),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
fof(f101,axiom,
? [A] : ~ empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f101_nnf,plain,
? [A] : ~ empty(A),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
~ empty(sk50),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk50])],[f101_nnf]) ).
cnf(c253,plain,
~ empty(sk50),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
fof(f140,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(f140_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)],[f140]) ).
fof(f140_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,B)
| ~ in(C,A) )
& ( ( in(sk53(A,B),B)
& in(sk53(A,B),A) )
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk53])],[f140_nnf]) ).
cnf(c315,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,X1)
| ~ in(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
fof(f156,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(f156_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)],[f156]) ).
fof(f156_sk,plain,
! [A,B,C] :
( ( ~ disjoint(A,B)
| ~ in(C,set_intersection2(A,B)) )
& ( in(sk54(A,B),set_intersection2(A,B))
| disjoint(A,B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk54])],[f156_nnf]) ).
cnf(c333,plain,
( ~ disjoint(X0,X1)
| ~ in(X2,set_intersection2(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
fof(f158,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(f158_nnf,plain,
! [A,B,C] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
! [C,A,B] :
( ~ in(B,C)
| ~ in(B,subset_complement(A,C))
| ~ element(C,powerset(A)) ),
inference(skolemisation,[status(esa)],[f158_nnf]) ).
cnf(c335,plain,
( ~ in(X1,X2)
| ~ in(X1,subset_complement(X0,X2))
| ~ element(X2,powerset(X0)) ),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
fof(f160,axiom,
! [A,B,C] :
~ ( empty(C)
& element(B,powerset(C))
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f160_nnf,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f160]) ).
fof(f160_sk,plain,
! [A,B,C] :
( ~ empty(C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f160_nnf]) ).
cnf(c337,plain,
( ~ empty(X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f160_sk]) ).
fof(f162,lemma,
! [A,B] :
~ ( proper_subset(B,A)
& subset(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
fof(f162_nnf,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
! [A,B] :
( ~ proper_subset(B,A)
| ~ subset(A,B) ),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c340,plain,
( ~ proper_subset(X1,X0)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
fof(f166,lemma,
! [A,B] :
( set_difference(A,singleton(B)) = A
<=> ~ in(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f166_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)],[f166]) ).
fof(f166_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)],[f166_nnf]) ).
cnf(c346,plain,
( ~ in(X1,X0)
| set_difference(X0,singleton(X1)) != X0 ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f172,axiom,
! [A,B] :
~ ( empty(B)
& in(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f172_nnf,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
! [A,B] :
( ~ empty(B)
| ~ in(A,B) ),
inference(skolemisation,[status(esa)],[f172_nnf]) ).
cnf(c356,plain,
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c47,c127,c169,c200,c202,c204,c206,c224,c225,c227,c249,c253,c315,c333,c335,c337,c340,c346,c356,c371]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4409]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU196+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n014.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:08:17 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 90.21/12.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.21/12.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------