%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU381+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:20:21 PM UTC 2026
% Result : Theorem 106.07s 13.94s
% Output : CNFRefutation 13.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 9
% Syntax : Number of formulae : 119 ( 18 unt; 0 def)
% Number of atoms : 492 ( 2 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 619 ( 246 ~; 282 |; 68 &)
% ( 9 <=>; 13 =>; 0 <=; 1 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 219 ( 207 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f36,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( element(B,powerset(the_carrier(A)))
=> ( upper_relstr_subset(B,A)
<=> ! [C] :
( element(C,the_carrier(A))
=> ! [D] :
( element(D,the_carrier(A))
=> ( ( related(A,C,D)
& in(C,B) )
=> in(D,B) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] :
( rel_str(boole_POSet(A))
& strict_rel_str(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A] :
( distributive_relstr(boole_POSet(A))
& join_complete_relstr(boole_POSet(A))
& up_complete_relstr(boole_POSet(A))
& bounded_relstr(boole_POSet(A))
& upper_bounded_relstr(boole_POSet(A))
& lower_bounded_relstr(boole_POSet(A))
& complete_relstr(boole_POSet(A))
& with_infima_relstr(boole_POSet(A))
& with_suprema_relstr(boole_POSet(A))
& antisymmetric_relstr(boole_POSet(A))
& transitive_relstr(boole_POSet(A))
& reflexive_relstr(boole_POSet(A))
& strict_rel_str(boole_POSet(A))
& ~ empty_carrier(boole_POSet(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [A,B,C] :
( ( element(C,the_carrier(A))
& element(B,the_carrier(A))
& rel_str(A)
& reflexive_relstr(A)
& ~ empty_carrier(A) )
=> ( related_reflexive(A,B,C)
<=> related(A,B,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,conjecture,
! [A,B] :
( element(B,powerset(the_carrier(boole_POSet(A))))
=> ( upper_relstr_subset(B,boole_POSet(A))
<=> ! [C,D] :
( ( in(C,B)
& subset(D,A)
& subset(C,D) )
=> in(D,B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,negated_conjecture,
~ ! [A,B] :
( element(B,powerset(the_carrier(boole_POSet(A))))
=> ( upper_relstr_subset(B,boole_POSet(A))
<=> ! [C,D] :
( ( in(C,B)
& subset(D,A)
& subset(C,D) )
=> in(D,B) ) ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
fof(f102,axiom,
! [A,B] :
( element(B,the_carrier(boole_POSet(A)))
=> ! [C] :
( element(C,the_carrier(boole_POSet(A)))
=> ( related_reflexive(boole_POSet(A),B,C)
<=> subset(B,C) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [A,B] :
( element(A,powerset(B))
<=> subset(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,axiom,
! [A,B,C] :
( ( element(B,powerset(C))
& in(A,B) )
=> element(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [A] : the_carrier(boole_POSet(A)) = powerset(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,plain,
! [A] :
( ! [B] :
( ( upper_relstr_subset(B,A)
<=> ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f306,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ~ in(D,B)
& related(A,C,D)
& in(C,B)
& element(D,the_carrier(A)) )
& element(C,the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f305]) ).
fof(f307,plain,
! [A] :
( ! [B] :
( ( ( ( ~ in(sK1_skl(B,A),B)
& related(A,sK0_skl(B,A),sK1_skl(B,A))
& in(sK0_skl(B,A),B)
& element(sK1_skl(B,A),the_carrier(A))
& element(sK0_skl(B,A),the_carrier(A)) )
| upper_relstr_subset(B,A) )
& ( ! [C] :
( ! [D] :
( in(D,B)
| ~ related(A,C,D)
| ~ in(C,B)
| ~ element(D,the_carrier(A)) )
| ~ element(C,the_carrier(A)) )
| ~ upper_relstr_subset(B,A) ) )
| ~ element(B,powerset(the_carrier(A))) )
| ~ rel_str(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(C,sK0_skl(B,A)),skolemize(D,sK1_skl(B,A))],[f306]) ).
fof(f308,plain,
! [X0,X1,X2,X3] :
( in(X3,X1)
| ~ related(X0,X2,X3)
| ~ in(X2,X1)
| ~ element(X3,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f309,plain,
! [X0,X1] :
( element(sK0_skl(X1,X0),the_carrier(X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f310,plain,
! [X0,X1] :
( element(sK1_skl(X1,X0),the_carrier(X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f311,plain,
! [X0,X1] :
( in(sK0_skl(X1,X0),X1)
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f312,plain,
! [X0,X1] :
( related(X0,sK0_skl(X1,X0),sK1_skl(X1,X0))
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f313,plain,
! [X0,X1] :
( ~ in(sK1_skl(X1,X0),X1)
| upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f317,plain,
( ! [A] : rel_str(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f319,plain,
! [X0] : rel_str(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f317]) ).
fof(f344,plain,
( ! [A] : distributive_relstr(boole_POSet(A))
& ! [A] : join_complete_relstr(boole_POSet(A))
& ! [A] : up_complete_relstr(boole_POSet(A))
& ! [A] : bounded_relstr(boole_POSet(A))
& ! [A] : upper_bounded_relstr(boole_POSet(A))
& ! [A] : lower_bounded_relstr(boole_POSet(A))
& ! [A] : complete_relstr(boole_POSet(A))
& ! [A] : with_infima_relstr(boole_POSet(A))
& ! [A] : with_suprema_relstr(boole_POSet(A))
& ! [A] : antisymmetric_relstr(boole_POSet(A))
& ! [A] : transitive_relstr(boole_POSet(A))
& ! [A] : reflexive_relstr(boole_POSet(A))
& ! [A] : strict_rel_str(boole_POSet(A))
& ! [A] : ~ empty_carrier(boole_POSet(A)) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f345,plain,
! [X0] : ~ empty_carrier(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f347,plain,
! [X0] : reflexive_relstr(boole_POSet(X0)),
inference(cnf_transformation,[status(thm)],[f344]) ).
fof(f667,plain,
! [A,B,C] :
( ( related_reflexive(A,B,C)
<=> related(A,B,C) )
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f668,plain,
! [A,B,C] :
( ( ( ~ related(A,B,C)
| related_reflexive(A,B,C) )
& ( related(A,B,C)
| ~ related_reflexive(A,B,C) ) )
| ~ element(C,the_carrier(A))
| ~ element(B,the_carrier(A))
| ~ rel_str(A)
| ~ reflexive_relstr(A)
| empty_carrier(A) ),
inference(NNF_transformation,[status(thm)],[f667]) ).
fof(f669,plain,
! [X0,X1,X2] :
( related(X0,X1,X2)
| ~ related_reflexive(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f668]) ).
fof(f670,plain,
! [X0,X1,X2] :
( ~ related(X0,X1,X2)
| related_reflexive(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ rel_str(X0)
| ~ reflexive_relstr(X0)
| empty_carrier(X0) ),
inference(cnf_transformation,[status(thm)],[f668]) ).
fof(f676,plain,
? [A,B] :
( ( upper_relstr_subset(B,boole_POSet(A))
<~> ! [C,D] :
( in(D,B)
| ~ in(C,B)
| ~ subset(D,A)
| ~ subset(C,D) ) )
& element(B,powerset(the_carrier(boole_POSet(A)))) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f677,plain,
? [A,B] :
( ( ? [C,D] :
( ~ in(D,B)
& in(C,B)
& subset(D,A)
& subset(C,D) )
| ~ upper_relstr_subset(B,boole_POSet(A)) )
& ( ! [C,D] :
( in(D,B)
| ~ in(C,B)
| ~ subset(D,A)
| ~ subset(C,D) )
| upper_relstr_subset(B,boole_POSet(A)) )
& element(B,powerset(the_carrier(boole_POSet(A)))) ),
inference(NNF_transformation,[status(thm)],[f676]) ).
fof(f678,plain,
? [A,B] :
( ( ? [D] :
( ~ in(D,B)
& ? [C] :
( in(C,B)
& subset(D,A)
& subset(C,D) ) )
| ~ upper_relstr_subset(B,boole_POSet(A)) )
& ( ! [D] :
( in(D,B)
| ! [C] :
( ~ in(C,B)
| ~ subset(D,A)
| ~ subset(C,D) ) )
| upper_relstr_subset(B,boole_POSet(A)) )
& element(B,powerset(the_carrier(boole_POSet(A)))) ),
inference(miniscoping,[status(thm)],[f677]) ).
fof(f679,plain,
( ( ( ~ in(sK36_skl,sK35_skl)
& in(sK37_skl,sK35_skl)
& subset(sK36_skl,sK34_skl)
& subset(sK37_skl,sK36_skl) )
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) )
& ( ! [D] :
( in(D,sK35_skl)
| ! [C] :
( ~ in(C,sK35_skl)
| ~ subset(D,sK34_skl)
| ~ subset(C,D) ) )
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) )
& element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl,sK35_skl,sK36_skl,sK37_skl]),skolemize(A,sK34_skl),skolemize(B,sK35_skl),skolemize(D,sK36_skl),skolemize(C,sK37_skl)],[f678]) ).
fof(f680,plain,
element(sK35_skl,powerset(the_carrier(boole_POSet(sK34_skl)))),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f681,plain,
! [X0,X1] :
( in(X1,sK35_skl)
| ~ in(X0,sK35_skl)
| ~ subset(X1,sK34_skl)
| ~ subset(X0,X1)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f682,plain,
( subset(sK37_skl,sK36_skl)
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f683,plain,
( subset(sK36_skl,sK34_skl)
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f684,plain,
( in(sK37_skl,sK35_skl)
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f685,plain,
( ~ in(sK36_skl,sK35_skl)
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f690,plain,
! [A,B] :
( ! [C] :
( ( related_reflexive(boole_POSet(A),B,C)
<=> subset(B,C) )
| ~ element(C,the_carrier(boole_POSet(A))) )
| ~ element(B,the_carrier(boole_POSet(A))) ),
inference(pre_NNF_transformation,[status(thm)],[f102]) ).
fof(f691,plain,
! [A,B] :
( ! [C] :
( ( ( ~ subset(B,C)
| related_reflexive(boole_POSet(A),B,C) )
& ( subset(B,C)
| ~ related_reflexive(boole_POSet(A),B,C) ) )
| ~ element(C,the_carrier(boole_POSet(A))) )
| ~ element(B,the_carrier(boole_POSet(A))) ),
inference(NNF_transformation,[status(thm)],[f690]) ).
fof(f692,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(cnf_transformation,[status(thm)],[f691]) ).
fof(f693,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,the_carrier(boole_POSet(X1))) ),
inference(cnf_transformation,[status(thm)],[f691]) ).
fof(f694,plain,
! [A,B] :
( ( ~ subset(A,B)
| element(A,powerset(B)) )
& ( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(NNF_transformation,[status(thm)],[f103]) ).
fof(f695,plain,
( ! [A,B] :
( ~ subset(A,B)
| element(A,powerset(B)) )
& ! [A,B] :
( subset(A,B)
| ~ element(A,powerset(B)) ) ),
inference(miniscoping,[status(thm)],[f694]) ).
fof(f696,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f697,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f698,plain,
! [A,B,C] :
( element(A,C)
| ~ element(B,powerset(C))
| ~ in(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f104]) ).
fof(f699,plain,
! [A,C] :
( element(A,C)
| ! [B] :
( ~ element(B,powerset(C))
| ~ in(A,B) ) ),
inference(miniscoping,[status(thm)],[f698]) ).
fof(f700,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ element(X1,powerset(X2))
| ~ in(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f701,plain,
! [X0] : the_carrier(boole_POSet(X0)) = powerset(X0),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f720,plain,
element(sK35_skl,powerset(powerset(sK34_skl))),
inference(backward_demodulation,[status(thm)],[f701,f680]) ).
fof(f1085,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ related(X0,X3,X2)
| ~ in(X3,X1)
| ~ element(X2,the_carrier(X0))
| ~ upper_relstr_subset(X1,X0)
| ~ element(X1,powerset(the_carrier(X0)))
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f700]) ).
fof(f1087,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ related(boole_POSet(X0),X3,X2)
| ~ in(X3,X1)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f1085]) ).
fof(f1088,plain,
! [X0,X1,X2,X3] :
( in(X2,X1)
| ~ related(boole_POSet(X0),X3,X2)
| ~ in(X3,X1)
| ~ element(X2,powerset(X0))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f701,f1087]) ).
fof(f1089,plain,
! [X0,X1,X2,X3] :
( in(X2,X0)
| ~ related(boole_POSet(X1),X3,X2)
| ~ in(X3,X0)
| ~ element(X2,powerset(X1))
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f319]) ).
fof(f1090,plain,
! [X0,X1] :
( in(X0,sK35_skl)
| ~ related(boole_POSet(sK34_skl),X1,X0)
| ~ in(X1,sK35_skl)
| ~ element(X0,powerset(sK34_skl))
| ~ upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1089,f720]) ).
fof(f1108,plain,
! [X0,X1] :
( element(sK0_skl(X1,boole_POSet(X0)),the_carrier(boole_POSet(X0)))
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f309]) ).
fof(f1109,plain,
! [X0,X1] :
( element(sK0_skl(X1,boole_POSet(X0)),powerset(X0))
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f701,f1108]) ).
fof(f1110,plain,
! [X0,X1] :
( element(sK0_skl(X0,boole_POSet(X1)),powerset(X1))
| upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1109,f319]) ).
fof(f1112,plain,
! [X0,X1] :
( element(sK1_skl(X1,boole_POSet(X0)),the_carrier(boole_POSet(X0)))
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f310]) ).
fof(f1113,plain,
! [X0,X1] :
( element(sK1_skl(X1,boole_POSet(X0)),powerset(X0))
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f701,f1112]) ).
fof(f1114,plain,
! [X0,X1] :
( element(sK1_skl(X0,boole_POSet(X1)),powerset(X1))
| upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1113,f319]) ).
fof(f1116,plain,
! [X0,X1] :
( in(sK0_skl(X1,boole_POSet(X0)),X1)
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f311]) ).
fof(f1117,plain,
! [X0,X1] :
( in(sK0_skl(X0,boole_POSet(X1)),X0)
| upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f319]) ).
fof(f1131,plain,
( element(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1110,f720]) ).
fof(f1135,plain,
! [X0,X1] :
( related(boole_POSet(X0),sK0_skl(X1,boole_POSet(X0)),sK1_skl(X1,boole_POSet(X0)))
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f312]) ).
fof(f1136,plain,
! [X0,X1] :
( related(boole_POSet(X1),sK0_skl(X0,boole_POSet(X1)),sK1_skl(X0,boole_POSet(X1)))
| upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1135,f319]) ).
fof(f1138,plain,
! [X0,X1] :
( ~ in(sK1_skl(X1,boole_POSet(X0)),X1)
| upper_relstr_subset(X1,boole_POSet(X0))
| ~ element(X1,powerset(powerset(X0)))
| ~ rel_str(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f313]) ).
fof(f1139,plain,
! [X0,X1] :
( ~ in(sK1_skl(X0,boole_POSet(X1)),X0)
| upper_relstr_subset(X0,boole_POSet(X1))
| ~ element(X0,powerset(powerset(X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1138,f319]) ).
fof(f1184,plain,
( element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1114,f720]) ).
fof(f1186,plain,
( in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1117,f720]) ).
fof(f1209,plain,
( subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1184,f696]) ).
fof(f1240,plain,
( related(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f1136,f720]) ).
fof(f2280,plain,
! [X0,X1,X2] :
( related(boole_POSet(X0),X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0))
| empty_carrier(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f669]) ).
fof(f2281,plain,
! [X0,X1,X2] :
( related(boole_POSet(X0),X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0))
| empty_carrier(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f701,f2280]) ).
fof(f2282,plain,
! [X0,X1,X2] :
( related(boole_POSet(X0),X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2281,f345]) ).
fof(f2284,plain,
! [X0,X1,X2] :
( ~ related(boole_POSet(X0),X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,the_carrier(boole_POSet(X0)))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0))
| empty_carrier(boole_POSet(X0)) ),
inference(paramodulation,[status(thm)],[f701,f670]) ).
fof(f2285,plain,
! [X0,X1,X2] :
( ~ related(boole_POSet(X0),X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0))
| empty_carrier(boole_POSet(X0)) ),
inference(forward_demodulation,[status(thm)],[f701,f2284]) ).
fof(f2286,plain,
! [X0,X1,X2] :
( ~ related(boole_POSet(X0),X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0))
| ~ reflexive_relstr(boole_POSet(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2285,f345]) ).
fof(f2308,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,powerset(X1)) ),
inference(forward_demodulation,[status(thm)],[f701,f692]) ).
fof(f2309,plain,
! [X0,X1,X2] :
( subset(X0,X2)
| ~ related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(forward_demodulation,[status(thm)],[f701,f2308]) ).
fof(f2310,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,the_carrier(boole_POSet(X1)))
| ~ element(X0,powerset(X1)) ),
inference(forward_demodulation,[status(thm)],[f701,f693]) ).
fof(f2311,plain,
! [X0,X1,X2] :
( ~ subset(X0,X2)
| related_reflexive(boole_POSet(X1),X0,X2)
| ~ element(X2,powerset(X1))
| ~ element(X0,powerset(X1)) ),
inference(forward_demodulation,[status(thm)],[f701,f2310]) ).
fof(f2360,plain,
! [X0,X1,X2] :
( related(boole_POSet(X0),X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2282,f347]) ).
fof(f2364,plain,
! [X0,X1,X2] :
( ~ related(boole_POSet(X0),X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2)
| ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| ~ rel_str(boole_POSet(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2286,f347]) ).
fof(f2365,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| related_reflexive(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| ~ element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| ~ element(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| ~ rel_str(boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f2364,f1240]) ).
fof(f2368,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| related_reflexive(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| ~ element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| ~ element(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2365,f319]) ).
fof(f3331,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| related_reflexive(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| ~ element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2368,f1131]) ).
fof(f3332,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| related_reflexive(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl))) ),
inference(resolution,[status(thm)],[f3331,f1184]) ).
fof(f3333,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| related_reflexive(boole_POSet(sK34_skl),sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f3332]) ).
fof(f34695,plain,
( subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| ~ element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| ~ element(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f3333,f2309]) ).
fof(f34696,plain,
( subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| ~ element(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),powerset(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f34695,f1131]) ).
fof(f62071,plain,
( subset(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK1_skl(sK35_skl,boole_POSet(sK34_skl)))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f34696,f1184]) ).
fof(f62074,plain,
( in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| ~ in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| ~ subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f62071,f681]) ).
fof(f62076,plain,
( in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| ~ in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| ~ subset(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK34_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f62074]) ).
fof(f62077,plain,
( in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| ~ in(sK0_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f62076,f1209]) ).
fof(f63514,plain,
( in(sK1_skl(sK35_skl,boole_POSet(sK34_skl)),sK35_skl)
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f62077,f1186]) ).
fof(f63515,plain,
( upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl))
| ~ element(sK35_skl,powerset(powerset(sK34_skl)))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f63514,f1139]) ).
fof(f63521,plain,
( ~ element(sK35_skl,powerset(powerset(sK34_skl)))
| upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f63515]) ).
fof(f63522,plain,
upper_relstr_subset(sK35_skl,boole_POSet(sK34_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f63521,f720]) ).
fof(f63537,plain,
! [X0,X1] :
( in(X0,sK35_skl)
| ~ related(boole_POSet(sK34_skl),X1,X0)
| ~ in(X1,sK35_skl)
| ~ element(X0,powerset(sK34_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1090,f63522]) ).
fof(f63538,plain,
~ in(sK36_skl,sK35_skl),
inference(backward_subsumption_resolution,[status(thm)],[f685,f63522]) ).
fof(f63539,plain,
in(sK37_skl,sK35_skl),
inference(backward_subsumption_resolution,[status(thm)],[f684,f63522]) ).
fof(f63540,plain,
subset(sK36_skl,sK34_skl),
inference(backward_subsumption_resolution,[status(thm)],[f683,f63522]) ).
fof(f63541,plain,
subset(sK37_skl,sK36_skl),
inference(backward_subsumption_resolution,[status(thm)],[f682,f63522]) ).
fof(f63543,plain,
! [X0] :
( element(sK37_skl,X0)
| ~ element(sK35_skl,powerset(X0)) ),
inference(resolution,[status(thm)],[f63539,f700]) ).
fof(f63547,plain,
element(sK36_skl,powerset(sK34_skl)),
inference(resolution,[status(thm)],[f63540,f697]) ).
fof(f63549,plain,
element(sK37_skl,powerset(sK34_skl)),
inference(resolution,[status(thm)],[f63543,f720]) ).
fof(f63578,plain,
! [X0] :
( ~ subset(sK37_skl,X0)
| related_reflexive(boole_POSet(sK34_skl),sK37_skl,X0)
| ~ element(X0,powerset(sK34_skl)) ),
inference(resolution,[status(thm)],[f63549,f2311]) ).
fof(f68358,plain,
( ~ subset(sK37_skl,sK36_skl)
| related_reflexive(boole_POSet(sK34_skl),sK37_skl,sK36_skl) ),
inference(resolution,[status(thm)],[f63578,f63547]) ).
fof(f68394,plain,
related_reflexive(boole_POSet(sK34_skl),sK37_skl,sK36_skl),
inference(forward_subsumption_resolution,[status(thm)],[f68358,f63541]) ).
fof(f68399,plain,
( related(boole_POSet(sK34_skl),sK37_skl,sK36_skl)
| ~ element(sK36_skl,powerset(sK34_skl))
| ~ element(sK37_skl,powerset(sK34_skl))
| ~ rel_str(boole_POSet(sK34_skl)) ),
inference(resolution,[status(thm)],[f68394,f2360]) ).
fof(f68401,plain,
( related(boole_POSet(sK34_skl),sK37_skl,sK36_skl)
| ~ element(sK36_skl,powerset(sK34_skl))
| ~ element(sK37_skl,powerset(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f68399,f319]) ).
fof(f92797,plain,
( related(boole_POSet(sK34_skl),sK37_skl,sK36_skl)
| ~ element(sK36_skl,powerset(sK34_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f68401,f63549]) ).
fof(f92798,plain,
related(boole_POSet(sK34_skl),sK37_skl,sK36_skl),
inference(resolution,[status(thm)],[f92797,f63547]) ).
fof(f92799,plain,
( in(sK36_skl,sK35_skl)
| ~ in(sK37_skl,sK35_skl)
| ~ element(sK36_skl,powerset(sK34_skl)) ),
inference(resolution,[status(thm)],[f92798,f63537]) ).
fof(f92803,plain,
( in(sK36_skl,sK35_skl)
| ~ in(sK37_skl,sK35_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f92799,f63547]) ).
fof(f92805,plain,
in(sK36_skl,sK35_skl),
inference(forward_subsumption_resolution,[status(thm)],[f92803,f63539]) ).
fof(f92806,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f63538,f92805]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU381+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n009.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 06:17:42 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 106.07/13.94 % Refutation found
% 106.07/13.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 106.07/13.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.65/14.07 % Elapsed time: 13.608874 seconds
% 13.65/14.07 % CPU time: 106.980085 seconds
% 13.65/14.07 % Total memory used: 453.818 MB
% 13.65/14.07 % Net memory used: 424.955 MB
%------------------------------------------------------------------------------