%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU309+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:20:07 PM UTC 2026
% Result : Theorem 42.82s 11.07s
% Output : CNFRefutation 17.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 73
% Syntax : Number of formulae : 298 ( 93 unt; 42 def)
% Number of atoms : 627 ( 57 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 507 ( 178 ~; 174 |; 93 &)
% ( 44 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 66 ( 64 usr; 43 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-3 aty)
% Number of variables : 112 ( 96 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f77,axiom,
! [A] :
( one_sorted_str(A)
=> cast_as_carrier_subset(A) = the_carrier(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A] :
( A = omega
<=> ( ! [B] :
( ordinal(B)
=> ( ( being_limit_ordinal(B)
& in(empty_set,B) )
=> subset(A,B) ) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,B) = set_difference(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f130,axiom,
! [A] :
( one_sorted_str(A)
=> element(cast_as_carrier_subset(A),powerset(the_carrier(A))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [A,B] :
( element(B,powerset(A))
=> element(subset_complement(A,B),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [A] : relation(identity_relation(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f154,axiom,
! [A,B,C] :
( ( element(C,powerset(A))
& element(B,powerset(A)) )
=> element(subset_difference(A,B,C),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,axiom,
! [A] :
( meet_semilatt_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,axiom,
! [A] :
( join_semilatt_str(A)
=> one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,axiom,
! [A] :
( latt_str(A)
=> ( join_semilatt_str(A)
& meet_semilatt_str(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f169,axiom,
? [A] : meet_semilatt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f171,axiom,
? [A] : join_semilatt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,axiom,
? [A] : latt_str(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,axiom,
( relation_empty_yielding(empty_set)
& relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,axiom,
( ~ empty(omega)
& ordinal(omega)
& epsilon_connected(omega)
& epsilon_transitive(omega) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,axiom,
( ordinal(empty_set)
& epsilon_connected(empty_set)
& epsilon_transitive(empty_set)
& empty(empty_set)
& one_to_one(empty_set)
& function(empty_set)
& relation_empty_yielding(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f226,axiom,
( v5_membered(empty_set)
& v4_membered(empty_set)
& v3_membered(empty_set)
& v2_membered(empty_set)
& v1_membered(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f235,axiom,
! [A,B] :
( element(B,powerset(A))
=> subset_complement(A,subset_complement(A,B)) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,lemma,
! [A] : singleton(A) != empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f260,axiom,
? [A] :
( function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f264,axiom,
? [A] :
( being_limit_ordinal(A)
& ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f265,axiom,
? [A] :
( empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,axiom,
? [A] :
( function(A)
& empty(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f271,axiom,
? [A] :
( ordinal(A)
& epsilon_connected(A)
& epsilon_transitive(A)
& empty(A)
& one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f277,axiom,
? [A] :
( one_to_one(A)
& function(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,axiom,
? [A] :
( ~ empty_carrier(A)
& one_sorted_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f281,axiom,
? [A] :
( function(A)
& relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,axiom,
! [A,B,C] :
( ( element(C,powerset(A))
& element(B,powerset(A)) )
=> subset_difference(A,B,C) = set_difference(B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f361,lemma,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_difference(the_carrier(A),cast_as_carrier_subset(A),subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f381,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> subset_difference(the_carrier(A),cast_as_carrier_subset(A),subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)) = B ) ),
inference(negated_conjecture,[status(cth)],[f380]) ).
fof(f891,plain,
! [A] :
( cast_as_carrier_subset(A) = the_carrier(A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f892,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f891]) ).
fof(f1000,plain,
! [A] :
( A = omega
<=> ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f1001,plain,
! [A] :
( ( ? [B] :
( ~ subset(A,B)
& being_limit_ordinal(B)
& in(empty_set,B)
& ordinal(B) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(NNF_transformation,[status(thm)],[f1000]) ).
fof(f1002,plain,
( ! [A] :
( ? [B] :
( ~ subset(A,B)
& being_limit_ordinal(B)
& in(empty_set,B)
& ordinal(B) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ! [A] :
( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(miniscoping,[status(thm)],[f1001]) ).
fof(f1003,plain,
( ! [A] :
( ( ~ subset(A,sK71_skl(A))
& being_limit_ordinal(sK71_skl(A))
& in(empty_set,sK71_skl(A))
& ordinal(sK71_skl(A)) )
| ~ ordinal(A)
| ~ being_limit_ordinal(A)
| ~ in(empty_set,A)
| A = omega )
& ! [A] :
( ( ! [B] :
( subset(A,B)
| ~ being_limit_ordinal(B)
| ~ in(empty_set,B)
| ~ ordinal(B) )
& ordinal(A)
& being_limit_ordinal(A)
& in(empty_set,A) )
| A != omega ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71_skl]),skolemize(B,sK71_skl(A))],[f1002]) ).
fof(f1006,plain,
! [X0] :
( ordinal(X0)
| X0 != omega ),
inference(cnf_transformation,[status(thm)],[f1003]) ).
fof(f1020,plain,
! [A,B] :
( subset_complement(A,B) = set_difference(A,B)
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f1021,plain,
! [X0,X1] :
( subset_complement(X1,X0) = set_difference(X1,X0)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1020]) ).
fof(f1140,plain,
! [A] :
( element(cast_as_carrier_subset(A),powerset(the_carrier(A)))
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f130]) ).
fof(f1141,plain,
! [X0] :
( element(cast_as_carrier_subset(X0),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1140]) ).
fof(f1148,plain,
! [A,B] :
( element(subset_complement(A,B),powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f139]) ).
fof(f1149,plain,
! [X0,X1] :
( element(subset_complement(X1,X0),powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1148]) ).
fof(f1164,plain,
! [X0] : relation(identity_relation(X0)),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f1167,plain,
! [A,B,C] :
( element(subset_difference(A,B,C),powerset(A))
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f154]) ).
fof(f1168,plain,
! [X0,X1,X2] :
( element(subset_difference(X1,X0,X2),powerset(X1))
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1167]) ).
fof(f1177,plain,
! [A] :
( one_sorted_str(A)
| ~ meet_semilatt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f159]) ).
fof(f1178,plain,
! [X0] :
( one_sorted_str(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1177]) ).
fof(f1179,plain,
! [A] :
( one_sorted_str(A)
| ~ join_semilatt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f161]) ).
fof(f1180,plain,
! [X0] :
( one_sorted_str(X0)
| ~ join_semilatt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1179]) ).
fof(f1181,plain,
! [A] :
( ( join_semilatt_str(A)
& meet_semilatt_str(A) )
| ~ latt_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f162]) ).
fof(f1182,plain,
! [X0] :
( meet_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1181]) ).
fof(f1183,plain,
! [X0] :
( join_semilatt_str(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1181]) ).
fof(f1194,plain,
meet_semilatt_str(sK93_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(A,sK93_skl)],[f169]) ).
fof(f1195,plain,
meet_semilatt_str(sK93_skl),
inference(cnf_transformation,[status(thm)],[f1194]) ).
fof(f1198,plain,
join_semilatt_str(sK95_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95_skl]),skolemize(A,sK95_skl)],[f171]) ).
fof(f1199,plain,
join_semilatt_str(sK95_skl),
inference(cnf_transformation,[status(thm)],[f1198]) ).
fof(f1200,plain,
latt_str(sK96_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK96_skl]),skolemize(A,sK96_skl)],[f172]) ).
fof(f1201,plain,
latt_str(sK96_skl),
inference(cnf_transformation,[status(thm)],[f1200]) ).
fof(f1204,plain,
! [A] : element(sK98_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK98_skl]),skolemize(B,sK98_skl(A))],[f174]) ).
fof(f1205,plain,
! [X0] : element(sK98_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f1204]) ).
fof(f1223,plain,
empty(empty_set),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f1224,plain,
relation(empty_set),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f1244,plain,
epsilon_transitive(omega),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f1279,plain,
epsilon_transitive(empty_set),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f1386,plain,
v1_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1387,plain,
v2_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1388,plain,
v3_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1389,plain,
v4_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1390,plain,
v5_membered(empty_set),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f1411,plain,
! [A,B] :
( subset_complement(A,subset_complement(A,B)) = B
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f235]) ).
fof(f1412,plain,
! [X0,X1] :
( subset_complement(X1,subset_complement(X1,X0)) = X0
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1411]) ).
fof(f1425,plain,
! [X0] : singleton(X0) != empty_set,
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f1508,plain,
( function(sK112_skl)
& relation(sK112_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK112_skl]),skolemize(A,sK112_skl)],[f260]) ).
fof(f1509,plain,
relation(sK112_skl),
inference(cnf_transformation,[status(thm)],[f1508]) ).
fof(f1527,plain,
( being_limit_ordinal(sK116_skl)
& ordinal(sK116_skl)
& epsilon_connected(sK116_skl)
& epsilon_transitive(sK116_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK116_skl]),skolemize(A,sK116_skl)],[f264]) ).
fof(f1528,plain,
epsilon_transitive(sK116_skl),
inference(cnf_transformation,[status(thm)],[f1527]) ).
fof(f1530,plain,
ordinal(sK116_skl),
inference(cnf_transformation,[status(thm)],[f1527]) ).
fof(f1532,plain,
( empty(sK117_skl)
& one_to_one(sK117_skl)
& function(sK117_skl)
& relation(sK117_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK117_skl]),skolemize(A,sK117_skl)],[f265]) ).
fof(f1533,plain,
relation(sK117_skl),
inference(cnf_transformation,[status(thm)],[f1532]) ).
fof(f1557,plain,
( function(sK122_skl)
& empty(sK122_skl)
& relation(sK122_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK122_skl]),skolemize(A,sK122_skl)],[f270]) ).
fof(f1558,plain,
relation(sK122_skl),
inference(cnf_transformation,[status(thm)],[f1557]) ).
fof(f1561,plain,
( ordinal(sK123_skl)
& epsilon_connected(sK123_skl)
& epsilon_transitive(sK123_skl)
& empty(sK123_skl)
& one_to_one(sK123_skl)
& function(sK123_skl)
& relation(sK123_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123_skl]),skolemize(A,sK123_skl)],[f271]) ).
fof(f1562,plain,
relation(sK123_skl),
inference(cnf_transformation,[status(thm)],[f1561]) ).
fof(f1586,plain,
( one_to_one(sK129_skl)
& function(sK129_skl)
& relation(sK129_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK129_skl]),skolemize(A,sK129_skl)],[f277]) ).
fof(f1587,plain,
relation(sK129_skl),
inference(cnf_transformation,[status(thm)],[f1586]) ).
fof(f1598,plain,
( ~ empty_carrier(sK132_skl)
& one_sorted_str(sK132_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK132_skl]),skolemize(A,sK132_skl)],[f280]) ).
fof(f1599,plain,
one_sorted_str(sK132_skl),
inference(cnf_transformation,[status(thm)],[f1598]) ).
fof(f1600,plain,
~ empty_carrier(sK132_skl),
inference(cnf_transformation,[status(thm)],[f1598]) ).
fof(f1601,plain,
( function(sK133_skl)
& relation_empty_yielding(sK133_skl)
& relation(sK133_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK133_skl]),skolemize(A,sK133_skl)],[f281]) ).
fof(f1602,plain,
relation(sK133_skl),
inference(cnf_transformation,[status(thm)],[f1601]) ).
fof(f1625,plain,
! [A,B,C] :
( subset_difference(A,B,C) = set_difference(B,C)
| ~ element(C,powerset(A))
| ~ element(B,powerset(A)) ),
inference(pre_NNF_transformation,[status(thm)],[f291]) ).
fof(f1626,plain,
! [X0,X1,X2] :
( subset_difference(X1,X0,X2) = set_difference(X0,X2)
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f1625]) ).
fof(f2066,plain,
! [A] :
( ! [B] :
( subset_complement(the_carrier(A),B) = subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)
| ~ element(B,powerset(the_carrier(A))) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f361]) ).
fof(f2067,plain,
! [X0,X1] :
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f2066]) ).
fof(f2119,plain,
? [A] :
( ? [B] :
( subset_difference(the_carrier(A),cast_as_carrier_subset(A),subset_difference(the_carrier(A),cast_as_carrier_subset(A),B)) != B
& element(B,powerset(the_carrier(A))) )
& one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f381]) ).
fof(f2120,plain,
( subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),sK254_skl)) != sK254_skl
& element(sK254_skl,powerset(the_carrier(sK253_skl)))
& one_sorted_str(sK253_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK253_skl,sK254_skl]),skolemize(A,sK253_skl),skolemize(B,sK254_skl)],[f2119]) ).
fof(f2121,plain,
one_sorted_str(sK253_skl),
inference(cnf_transformation,[status(thm)],[f2120]) ).
fof(f2122,plain,
element(sK254_skl,powerset(the_carrier(sK253_skl))),
inference(cnf_transformation,[status(thm)],[f2120]) ).
fof(f2123,plain,
subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),sK254_skl)) != sK254_skl,
inference(cnf_transformation,[status(thm)],[f2120]) ).
fof(f3173,plain,
ordinal(omega),
inference(destructive_equality_resolution,[status(thm)],[f1006]) ).
fof(f3290,plain,
cast_as_carrier_subset(sK253_skl) = the_carrier(sK253_skl),
inference(resolution,[status(thm)],[f892,f2121]) ).
fof(f3293,plain,
subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),sK254_skl)) != sK254_skl,
inference(backward_demodulation,[status(thm)],[f3290,f2123]) ).
fof(f3294,plain,
( element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl)))
| ~ one_sorted_str(sK253_skl) ),
inference(paramodulation,[status(thm)],[f3290,f1141]) ).
fof(f3295,plain,
subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),sK254_skl)) != sK254_skl,
inference(forward_demodulation,[status(thm)],[f3290,f3293]) ).
fof(f3296,definition,
( sQ57_spl
<=> one_sorted_str(sK253_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f3298,plain,
( sQ57_spl
| ~ one_sorted_str(sK253_skl) ),
inference(component_clause,[status(thm)],[f3296]) ).
fof(f3299,definition,
( sQ58_spl
<=> element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f3302,plain,
( sQ58_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f3294,f3296,f3299]) ).
fof(f3303,plain,
( sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3298,f2121]) ).
fof(f3304,plain,
sQ57_spl,
inference(contradiction_clause,[status(thm)],[f3303]) ).
fof(f3316,plain,
! [X0] :
( subset_complement(the_carrier(sK253_skl),X0) = subset_difference(the_carrier(sK253_skl),cast_as_carrier_subset(sK253_skl),X0)
| ~ element(X0,powerset(the_carrier(sK253_skl))) ),
inference(resolution,[status(thm)],[f2067,f2121]) ).
fof(f3319,plain,
! [X0] :
( subset_complement(the_carrier(sK253_skl),X0) = subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),X0)
| ~ element(X0,powerset(the_carrier(sK253_skl))) ),
inference(forward_demodulation,[status(thm)],[f3290,f3316]) ).
fof(f3323,plain,
subset_complement(the_carrier(sK253_skl),sK254_skl) = subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),sK254_skl),
inference(resolution,[status(thm)],[f3319,f2122]) ).
fof(f3342,plain,
subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),subset_complement(the_carrier(sK253_skl),sK254_skl)) != sK254_skl,
inference(backward_demodulation,[status(thm)],[f3323,f3295]) ).
fof(f3343,plain,
( subset_complement(the_carrier(sK253_skl),sK254_skl) = set_difference(the_carrier(sK253_skl),sK254_skl)
| ~ element(sK254_skl,powerset(the_carrier(sK253_skl)))
| ~ element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl))) ),
inference(paramodulation,[status(thm)],[f3323,f1626]) ).
fof(f3344,plain,
( element(subset_complement(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl)))
| ~ element(sK254_skl,powerset(the_carrier(sK253_skl)))
| ~ element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl))) ),
inference(paramodulation,[status(thm)],[f3323,f1168]) ).
fof(f3345,definition,
( sQ63_spl
<=> element(sK254_skl,powerset(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f3347,plain,
( sQ63_spl
| ~ element(sK254_skl,powerset(the_carrier(sK253_skl))) ),
inference(component_clause,[status(thm)],[f3345]) ).
fof(f3348,definition,
( sQ64_spl
<=> subset_complement(the_carrier(sK253_skl),sK254_skl) = set_difference(the_carrier(sK253_skl),sK254_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3349,plain,
( ~ sQ64_spl
| subset_complement(the_carrier(sK253_skl),sK254_skl) = set_difference(the_carrier(sK253_skl),sK254_skl) ),
inference(component_clause,[status(thm)],[f3348]) ).
fof(f3351,plain,
( sQ64_spl
| ~ sQ63_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f3343,f3299,f3345,f3348]) ).
fof(f3352,definition,
( sQ65_spl
<=> element(subset_complement(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f3353,plain,
( ~ sQ65_spl
| element(subset_complement(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))) ),
inference(component_clause,[status(thm)],[f3352]) ).
fof(f3355,plain,
( sQ65_spl
| ~ sQ63_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f3344,f3299,f3345,f3352]) ).
fof(f3356,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3347,f2122]) ).
fof(f3357,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f3356]) ).
fof(f3360,definition,
( sQ66_spl
<=> one_sorted_str(sK95_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f3362,plain,
( sQ66_spl
| ~ one_sorted_str(sK95_skl) ),
inference(component_clause,[status(thm)],[f3360]) ).
fof(f3378,plain,
( ~ sQ64_spl
| subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) != sK254_skl ),
inference(backward_demodulation,[status(thm)],[f3349,f3342]) ).
fof(f3379,plain,
( ~ sQ64_spl
| set_difference(the_carrier(sK253_skl),sK254_skl) = subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),sK254_skl) ),
inference(backward_demodulation,[status(thm)],[f3349,f3323]) ).
fof(f3380,plain,
( sQ66_spl
| ~ join_semilatt_str(sK95_skl) ),
inference(resolution,[status(thm)],[f3362,f1180]) ).
fof(f3381,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3380,f1199]) ).
fof(f3382,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f3381]) ).
fof(f3407,plain,
( ~ sQ65_spl
| ~ sQ64_spl
| element(set_difference(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))) ),
inference(forward_demodulation,[status(thm)],[f3349,f3353]) ).
fof(f3409,plain,
( ~ sQ65_spl
| ~ sQ64_spl
| subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) ),
inference(resolution,[status(thm)],[f3407,f3319]) ).
fof(f3411,plain,
( ~ sQ64_spl
| element(set_difference(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl)))
| ~ element(sK254_skl,powerset(the_carrier(sK253_skl)))
| ~ element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl))) ),
inference(paramodulation,[status(thm)],[f3379,f1168]) ).
fof(f3416,definition,
( sQ73_spl
<=> element(set_difference(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f3419,plain,
( ~ sQ64_spl
| sQ73_spl
| ~ sQ63_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f3411,f3299,f3345,f3416,f3348]) ).
fof(f3547,plain,
( ~ sQ64_spl
| ~ sQ65_spl
| subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) != sK254_skl ),
inference(backward_demodulation,[status(thm)],[f3409,f3378]) ).
fof(f3555,definition,
( sQ85_spl
<=> subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f3556,plain,
( ~ sQ85_spl
| subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) ),
inference(component_clause,[status(thm)],[f3555]) ).
fof(f4004,plain,
( ~ sQ64_spl
| ~ sQ65_spl
| ~ sQ85_spl
| set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) != sK254_skl ),
inference(backward_demodulation,[status(thm)],[f3556,f3547]) ).
fof(f4007,definition,
( sQ116_spl
<=> one_sorted_str(sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f4009,plain,
( sQ116_spl
| ~ one_sorted_str(sK132_skl) ),
inference(component_clause,[status(thm)],[f4007]) ).
fof(f4014,plain,
( sQ116_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4009,f1599]) ).
fof(f4015,plain,
sQ116_spl,
inference(contradiction_clause,[status(thm)],[f4014]) ).
fof(f5253,definition,
( sQ161_spl
<=> relation(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f5255,plain,
( sQ161_spl
| ~ relation(empty_set) ),
inference(component_clause,[status(thm)],[f5253]) ).
fof(f5268,plain,
( sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5255,f1224]) ).
fof(f5269,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f5268]) ).
fof(f6060,definition,
( sQ175_spl
<=> relation(sK112_skl) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f6062,plain,
( sQ175_spl
| ~ relation(sK112_skl) ),
inference(component_clause,[status(thm)],[f6060]) ).
fof(f6075,plain,
( sQ175_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6062,f1509]) ).
fof(f6076,plain,
sQ175_spl,
inference(contradiction_clause,[status(thm)],[f6075]) ).
fof(f6813,definition,
( sQ210_spl
<=> relation(sK117_skl) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f6815,plain,
( sQ210_spl
| ~ relation(sK117_skl) ),
inference(component_clause,[status(thm)],[f6813]) ).
fof(f6828,plain,
( sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6815,f1533]) ).
fof(f6829,plain,
sQ210_spl,
inference(contradiction_clause,[status(thm)],[f6828]) ).
fof(f6876,definition,
( sQ219_spl
<=> relation(identity_relation(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f6878,plain,
( sQ219_spl
| ~ relation(identity_relation(the_carrier(sK253_skl))) ),
inference(component_clause,[status(thm)],[f6876]) ).
fof(f6993,definition,
( sQ220_spl
<=> relation(sK122_skl) ),
introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition]) ).
fof(f6995,plain,
( sQ220_spl
| ~ relation(sK122_skl) ),
inference(component_clause,[status(thm)],[f6993]) ).
fof(f7008,plain,
( sQ220_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6995,f1558]) ).
fof(f7009,plain,
sQ220_spl,
inference(contradiction_clause,[status(thm)],[f7008]) ).
fof(f7051,definition,
( sQ224_spl
<=> relation(sK123_skl) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f7053,plain,
( sQ224_spl
| ~ relation(sK123_skl) ),
inference(component_clause,[status(thm)],[f7051]) ).
fof(f7066,plain,
( sQ224_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7053,f1562]) ).
fof(f7067,plain,
sQ224_spl,
inference(contradiction_clause,[status(thm)],[f7066]) ).
fof(f8173,definition,
( sQ279_spl
<=> empty_carrier(sK132_skl) ),
introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition]) ).
fof(f8174,plain,
( ~ sQ279_spl
| empty_carrier(sK132_skl) ),
inference(component_clause,[status(thm)],[f8173]) ).
fof(f8260,definition,
( sQ297_spl
<=> join_semilatt_str(sK95_skl) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f8262,plain,
( sQ297_spl
| ~ join_semilatt_str(sK95_skl) ),
inference(component_clause,[status(thm)],[f8260]) ).
fof(f8275,definition,
( sQ301_spl
<=> empty(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ301_spl])],[split_symbol_definition]) ).
fof(f8277,plain,
( sQ301_spl
| ~ empty(empty_set) ),
inference(component_clause,[status(thm)],[f8275]) ).
fof(f8699,plain,
( ~ sQ279_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8174,f1600]) ).
fof(f8700,plain,
~ sQ279_spl,
inference(contradiction_clause,[status(thm)],[f8699]) ).
fof(f8701,plain,
( sQ301_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8277,f1223]) ).
fof(f8702,plain,
sQ301_spl,
inference(contradiction_clause,[status(thm)],[f8701]) ).
fof(f9650,plain,
subset_complement(the_carrier(sK253_skl),sK254_skl) = set_difference(the_carrier(sK253_skl),sK254_skl),
inference(resolution,[status(thm)],[f2122,f1021]) ).
fof(f10417,definition,
( sQ363_spl
<=> relation(sK129_skl) ),
introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition]) ).
fof(f10419,plain,
( sQ363_spl
| ~ relation(sK129_skl) ),
inference(component_clause,[status(thm)],[f10417]) ).
fof(f10432,plain,
( sQ363_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10419,f1587]) ).
fof(f10433,plain,
sQ363_spl,
inference(contradiction_clause,[status(thm)],[f10432]) ).
fof(f10878,plain,
( sQ297_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8262,f1199]) ).
fof(f10879,plain,
sQ297_spl,
inference(contradiction_clause,[status(thm)],[f10878]) ).
fof(f11245,definition,
( sQ387_spl
<=> epsilon_transitive(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ387_spl])],[split_symbol_definition]) ).
fof(f11247,plain,
( sQ387_spl
| ~ epsilon_transitive(empty_set) ),
inference(component_clause,[status(thm)],[f11245]) ).
fof(f11256,definition,
( sQ390_spl
<=> relation(identity_relation(empty_set)) ),
introduced(definition,[new_symbols(definition,[sQ390_spl])],[split_symbol_definition]) ).
fof(f11258,plain,
( sQ390_spl
| ~ relation(identity_relation(empty_set)) ),
inference(component_clause,[status(thm)],[f11256]) ).
fof(f12144,definition,
( sQ417_spl
<=> relation(sK133_skl) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f12146,plain,
( sQ417_spl
| ~ relation(sK133_skl) ),
inference(component_clause,[status(thm)],[f12144]) ).
fof(f12171,plain,
( sQ417_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12146,f1602]) ).
fof(f12172,plain,
sQ417_spl,
inference(contradiction_clause,[status(thm)],[f12171]) ).
fof(f12229,definition,
( sQ430_spl
<=> epsilon_transitive(omega) ),
introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition]) ).
fof(f12231,plain,
( sQ430_spl
| ~ epsilon_transitive(omega) ),
inference(component_clause,[status(thm)],[f12229]) ).
fof(f12250,plain,
( sQ430_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12231,f1244]) ).
fof(f12251,plain,
sQ430_spl,
inference(contradiction_clause,[status(thm)],[f12250]) ).
fof(f12254,definition,
( sQ436_spl
<=> ordinal(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f12256,plain,
( sQ436_spl
| ~ ordinal(sK116_skl) ),
inference(component_clause,[status(thm)],[f12254]) ).
fof(f12264,definition,
( sQ439_spl
<=> ordinal(omega) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f12266,plain,
( sQ439_spl
| ~ ordinal(omega) ),
inference(component_clause,[status(thm)],[f12264]) ).
fof(f12271,plain,
( sQ439_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12266,f3173]) ).
fof(f12272,plain,
sQ439_spl,
inference(contradiction_clause,[status(thm)],[f12271]) ).
fof(f12273,plain,
( sQ436_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12256,f1530]) ).
fof(f12274,plain,
sQ436_spl,
inference(contradiction_clause,[status(thm)],[f12273]) ).
fof(f12665,definition,
( sQ468_spl
<=> relation(identity_relation(powerset(empty_set))) ),
introduced(definition,[new_symbols(definition,[sQ468_spl])],[split_symbol_definition]) ).
fof(f12667,plain,
( sQ468_spl
| ~ relation(identity_relation(powerset(empty_set))) ),
inference(component_clause,[status(thm)],[f12665]) ).
fof(f13233,plain,
( sQ219_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6878,f1164]) ).
fof(f13251,plain,
sQ219_spl,
inference(contradiction_clause,[status(thm)],[f13233]) ).
fof(f13314,plain,
( sQ387_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11247,f1279]) ).
fof(f13315,plain,
sQ387_spl,
inference(contradiction_clause,[status(thm)],[f13314]) ).
fof(f13323,definition,
( sQ497_spl
<=> latt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ497_spl])],[split_symbol_definition]) ).
fof(f13325,plain,
( sQ497_spl
| ~ latt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f13323]) ).
fof(f13330,plain,
( sQ497_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13325,f1201]) ).
fof(f13331,plain,
sQ497_spl,
inference(contradiction_clause,[status(thm)],[f13330]) ).
fof(f13587,plain,
( sQ468_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12667,f1164]) ).
fof(f13588,plain,
sQ468_spl,
inference(contradiction_clause,[status(thm)],[f13587]) ).
fof(f14291,plain,
element(subset_complement(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))),
inference(resolution,[status(thm)],[f1149,f2122]) ).
fof(f14303,plain,
element(set_difference(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl))),
inference(forward_demodulation,[status(thm)],[f9650,f14291]) ).
fof(f14349,plain,
subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = subset_difference(the_carrier(sK253_skl),the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)),
inference(resolution,[status(thm)],[f14303,f3319]) ).
fof(f14396,plain,
subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)),
inference(resolution,[status(thm)],[f14303,f1021]) ).
fof(f14408,plain,
( subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl))
| ~ element(set_difference(the_carrier(sK253_skl),sK254_skl),powerset(the_carrier(sK253_skl)))
| ~ element(the_carrier(sK253_skl),powerset(the_carrier(sK253_skl))) ),
inference(paramodulation,[status(thm)],[f14349,f1626]) ).
fof(f14410,plain,
( sQ85_spl
| ~ sQ73_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f14408,f3299,f3416,f3555]) ).
fof(f14422,definition,
( sQ523_spl
<=> epsilon_transitive(sK116_skl) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f14424,plain,
( sQ523_spl
| ~ epsilon_transitive(sK116_skl) ),
inference(component_clause,[status(thm)],[f14422]) ).
fof(f14436,plain,
( sQ523_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14424,f1528]) ).
fof(f14437,plain,
sQ523_spl,
inference(contradiction_clause,[status(thm)],[f14436]) ).
fof(f14562,plain,
one_sorted_str(sK93_skl),
inference(resolution,[status(thm)],[f1178,f1195]) ).
fof(f14827,plain,
meet_semilatt_str(sK96_skl),
inference(resolution,[status(thm)],[f1182,f1201]) ).
fof(f14828,plain,
join_semilatt_str(sK96_skl),
inference(resolution,[status(thm)],[f1183,f1201]) ).
fof(f15173,definition,
( sQ554_spl
<=> one_sorted_str(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ554_spl])],[split_symbol_definition]) ).
fof(f15175,plain,
( sQ554_spl
| ~ one_sorted_str(sK93_skl) ),
inference(component_clause,[status(thm)],[f15173]) ).
fof(f15181,plain,
( sQ554_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15175,f14562]) ).
fof(f15182,plain,
sQ554_spl,
inference(contradiction_clause,[status(thm)],[f15181]) ).
fof(f15222,definition,
( sQ557_spl
<=> one_sorted_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition]) ).
fof(f15224,plain,
( sQ557_spl
| ~ one_sorted_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f15222]) ).
fof(f15281,plain,
( sQ557_spl
| ~ join_semilatt_str(sK96_skl) ),
inference(resolution,[status(thm)],[f15224,f1180]) ).
fof(f15282,plain,
( sQ557_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15281,f14828]) ).
fof(f15283,plain,
sQ557_spl,
inference(contradiction_clause,[status(thm)],[f15282]) ).
fof(f15524,definition,
( sQ575_spl
<=> meet_semilatt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ575_spl])],[split_symbol_definition]) ).
fof(f15526,plain,
( sQ575_spl
| ~ meet_semilatt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f15524]) ).
fof(f15567,definition,
( sQ586_spl
<=> join_semilatt_str(sK96_skl) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f15569,plain,
( sQ586_spl
| ~ join_semilatt_str(sK96_skl) ),
inference(component_clause,[status(thm)],[f15567]) ).
fof(f15587,plain,
( sQ586_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15569,f14828]) ).
fof(f15588,plain,
sQ586_spl,
inference(contradiction_clause,[status(thm)],[f15587]) ).
fof(f15604,definition,
( sQ591_spl
<=> meet_semilatt_str(sK93_skl) ),
introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition]) ).
fof(f15606,plain,
( sQ591_spl
| ~ meet_semilatt_str(sK93_skl) ),
inference(component_clause,[status(thm)],[f15604]) ).
fof(f15667,plain,
( sQ591_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15606,f1195]) ).
fof(f15668,plain,
sQ591_spl,
inference(contradiction_clause,[status(thm)],[f15667]) ).
fof(f16134,plain,
( sQ390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11258,f1164]) ).
fof(f16135,plain,
sQ390_spl,
inference(contradiction_clause,[status(thm)],[f16134]) ).
fof(f17293,plain,
( sQ575_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14827,f15526]) ).
fof(f17294,plain,
sQ575_spl,
inference(contradiction_clause,[status(thm)],[f17293]) ).
fof(f17296,definition,
( sQ648_spl
<=> v4_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ648_spl])],[split_symbol_definition]) ).
fof(f17298,plain,
( sQ648_spl
| ~ v4_membered(empty_set) ),
inference(component_clause,[status(thm)],[f17296]) ).
fof(f17300,plain,
( sQ648_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17298,f1389]) ).
fof(f17301,plain,
sQ648_spl,
inference(contradiction_clause,[status(thm)],[f17300]) ).
fof(f17309,definition,
( sQ649_spl
<=> v5_membered(empty_set) ),
introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition]) ).
fof(f17311,plain,
( sQ649_spl
| ~ v5_membered(empty_set) ),
inference(component_clause,[status(thm)],[f17309]) ).
fof(f17313,plain,
( sQ649_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f17311,f1390]) ).
fof(f17314,plain,
sQ649_spl,
inference(contradiction_clause,[status(thm)],[f17313]) ).
fof(f18352,plain,
subset_complement(the_carrier(sK253_skl),subset_complement(the_carrier(sK253_skl),sK254_skl)) = sK254_skl,
inference(resolution,[status(thm)],[f1412,f2122]) ).
fof(f18362,plain,
subset_complement(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)) = sK254_skl,
inference(forward_demodulation,[status(thm)],[f9650,f18352]) ).
fof(f19055,definition,
! [X0] :
( sQ685_spl
<=> ~ v5_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition]) ).
fof(f19056,plain,
! [X0] :
( ~ sQ685_spl
| ~ v5_membered(X0) ),
inference(component_clause,[status(thm)],[f19055]) ).
fof(f19063,definition,
! [X0] :
( sQ686_spl
<=> ~ v4_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition]) ).
fof(f19064,plain,
! [X0] :
( ~ sQ686_spl
| ~ v4_membered(X0) ),
inference(component_clause,[status(thm)],[f19063]) ).
fof(f19070,definition,
! [X0] :
( sQ687_spl
<=> ~ v3_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition]) ).
fof(f19071,plain,
! [X0] :
( ~ sQ687_spl
| ~ v3_membered(X0) ),
inference(component_clause,[status(thm)],[f19070]) ).
fof(f19076,definition,
! [X0] :
( sQ688_spl
<=> ~ v2_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition]) ).
fof(f19077,plain,
! [X0] :
( ~ sQ688_spl
| ~ v2_membered(X0) ),
inference(component_clause,[status(thm)],[f19076]) ).
fof(f19081,definition,
! [X0] :
( sQ689_spl
<=> ~ v1_membered(X0) ),
introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition]) ).
fof(f19082,plain,
! [X0] :
( ~ sQ689_spl
| ~ v1_membered(X0) ),
inference(component_clause,[status(thm)],[f19081]) ).
fof(f19085,plain,
( ~ sQ685_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1390,f19056]) ).
fof(f19088,plain,
~ sQ685_spl,
inference(contradiction_clause,[status(thm)],[f19085]) ).
fof(f19348,plain,
( ~ sQ686_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1389,f19064]) ).
fof(f19351,plain,
~ sQ686_spl,
inference(contradiction_clause,[status(thm)],[f19348]) ).
fof(f19352,plain,
( ~ sQ687_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1388,f19071]) ).
fof(f19355,plain,
~ sQ687_spl,
inference(contradiction_clause,[status(thm)],[f19352]) ).
fof(f19356,plain,
( ~ sQ688_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1387,f19077]) ).
fof(f19359,plain,
~ sQ688_spl,
inference(contradiction_clause,[status(thm)],[f19356]) ).
fof(f19371,definition,
! [X0] :
( sQ694_spl
<=> empty_set = singleton(X0) ),
introduced(definition,[new_symbols(definition,[sQ694_spl])],[split_symbol_definition]) ).
fof(f19372,plain,
! [X0] :
( ~ sQ694_spl
| empty_set = singleton(X0) ),
inference(component_clause,[status(thm)],[f19371]) ).
fof(f19376,plain,
( ~ sQ694_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19372,f1425]) ).
fof(f19377,plain,
~ sQ694_spl,
inference(contradiction_clause,[status(thm)],[f19376]) ).
fof(f19385,definition,
( sQ695_spl
<=> element(sK98_skl(powerset(the_carrier(sK253_skl))),powerset(the_carrier(sK253_skl))) ),
introduced(definition,[new_symbols(definition,[sQ695_spl])],[split_symbol_definition]) ).
fof(f19387,plain,
( sQ695_spl
| ~ element(sK98_skl(powerset(the_carrier(sK253_skl))),powerset(the_carrier(sK253_skl))) ),
inference(component_clause,[status(thm)],[f19385]) ).
fof(f19396,plain,
( sQ695_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19387,f1205]) ).
fof(f19397,plain,
sQ695_spl,
inference(contradiction_clause,[status(thm)],[f19396]) ).
fof(f19543,plain,
( ~ sQ689_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1386,f19082]) ).
fof(f19546,plain,
~ sQ689_spl,
inference(contradiction_clause,[status(thm)],[f19543]) ).
fof(f19673,plain,
sK254_skl = set_difference(the_carrier(sK253_skl),set_difference(the_carrier(sK253_skl),sK254_skl)),
inference(forward_demodulation,[status(thm)],[f18362,f14396]) ).
fof(f19674,plain,
( ~ sQ64_spl
| ~ sQ65_spl
| ~ sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19673,f4004]) ).
fof(f19675,plain,
( ~ sQ64_spl
| ~ sQ65_spl
| ~ sQ85_spl ),
inference(contradiction_clause,[status(thm)],[f19674]) ).
fof(f19676,plain,
$false,
inference(sat_refutation,[status(thm)],[f3302,f3304,f3351,f3355,f3357,f3382,f3419,f4015,f5269,f6076,f6829,f7009,f7067,f8700,f8702,f10433,f10879,f12172,f12251,f12272,f12274,f13251,f13315,f13331,f13588,f14410,f14437,f15182,f15283,f15588,f15668,f16135,f17294,f17301,f17314,f19088,f19351,f19355,f19359,f19377,f19397,f19546,f19675]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU309+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/5.53 % Computer : n014.cluster.edu
% 0.08/5.53 % Model : x86_64 x86_64
% 0.08/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.53 % Memory : 8046.5625MB
% 0.08/5.53 % OS : Linux 6.8.0-71-generic
% 0.08/5.53 % CPULimit : 300
% 0.08/5.53 % WCLimit : 300
% 0.08/5.53 % DateTime : Mon Sep 21 06:10:10 UTC 2026
% 0.08/5.53 % CPUTime :
% 0.08/5.59 % Drodi V4.1.1
% 42.82/11.07 % Refutation found
% 42.82/11.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 42.82/11.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.09/11.30 % Elapsed time: 5.766287 seconds
% 3.09/11.30 % CPU time: 44.078512 seconds
% 3.09/11.30 % Total memory used: 471.587 MB
% 3.09/11.30 % Net memory used: 424.139 MB
%------------------------------------------------------------------------------