%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU373+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 : 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:20 PM UTC 2026
% Result : Theorem 0.58s 0.63s
% Output : CNFRefutation 0.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 15
% Syntax : Number of formulae : 68 ( 14 unt; 7 def)
% Number of atoms : 212 ( 4 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 225 ( 81 ~; 77 |; 41 &)
% ( 11 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 8 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-4 aty)
% Number of variables : 61 ( 55 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f80,axiom,
! [A] :
( rel_str(A)
=> ! [B] :
( rel_str(B)
=> ( subrelstr(B,A)
<=> ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( net_str(C,A)
=> ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f269,axiom,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> rel_str(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f276,axiom,
! [A,B] :
( ( net_str(B,A)
& one_sorted_str(A) )
=> ! [C] :
( subnetstr(C,A,B)
=> net_str(C,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f459,axiom,
? [A] :
( function(A)
& relation_empty_yielding(A)
& relation(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f461,axiom,
? [A] :
( strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f464,axiom,
? [A] :
( lattice(A)
& join_absorbing(A)
& meet_absorbing(A)
& meet_associative(A)
& meet_commutative(A)
& join_associative(A)
& join_commutative(A)
& strict_latt_str(A)
& ~ empty_carrier(A)
& latt_str(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f595,conjecture,
! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> subset(the_carrier(C),the_carrier(B)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f596,negated_conjecture,
~ ! [A] :
( one_sorted_str(A)
=> ! [B] :
( net_str(B,A)
=> ! [C] :
( subnetstr(C,A,B)
=> subset(the_carrier(C),the_carrier(B)) ) ) ),
inference(negated_conjecture,[status(cth)],[f595]) ).
fof(f1109,plain,
! [A] :
( ! [B] :
( ( subrelstr(B,A)
<=> ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) ) )
| ~ rel_str(B) )
| ~ rel_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f80]) ).
fof(f1110,plain,
! [A] :
( ! [B] :
( ( ( ~ subset(the_InternalRel(B),the_InternalRel(A))
| ~ subset(the_carrier(B),the_carrier(A))
| subrelstr(B,A) )
& ( ( subset(the_InternalRel(B),the_InternalRel(A))
& subset(the_carrier(B),the_carrier(A)) )
| ~ subrelstr(B,A) ) )
| ~ rel_str(B) )
| ~ rel_str(A) ),
inference(NNF_transformation,[status(thm)],[f1109]) ).
fof(f1111,plain,
! [X0,X1] :
( subset(the_carrier(X1),the_carrier(X0))
| ~ subrelstr(X1,X0)
| ~ rel_str(X1)
| ~ rel_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1110]) ).
fof(f1783,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( subnetstr(C,A,B)
<=> ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f179]) ).
fof(f1784,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( the_mapping(A,C) != relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
| ~ subrelstr(C,B)
| subnetstr(C,A,B) )
& ( ( the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C))
& subrelstr(C,B) )
| ~ subnetstr(C,A,B) ) )
| ~ net_str(C,A) )
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(NNF_transformation,[status(thm)],[f1783]) ).
fof(f1785,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X2,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1784]) ).
fof(f1960,plain,
! [A] :
( ! [B] :
( rel_str(B)
| ~ net_str(B,A) )
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f269]) ).
fof(f1961,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1960]) ).
fof(f1971,plain,
! [A,B] :
( ! [C] :
( net_str(C,A)
| ~ subnetstr(C,A,B) )
| ~ net_str(B,A)
| ~ one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f276]) ).
fof(f1972,plain,
! [X0,X1,X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[status(thm)],[f1971]) ).
fof(f2802,plain,
( function(sK200_skl)
& relation_empty_yielding(sK200_skl)
& relation(sK200_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK200_skl]),skolemize(A,sK200_skl)],[f459]) ).
fof(f2803,plain,
relation(sK200_skl),
inference(cnf_transformation,[status(thm)],[f2802]) ).
fof(f2810,plain,
( strict_latt_str(sK202_skl)
& ~ empty_carrier(sK202_skl)
& latt_str(sK202_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK202_skl]),skolemize(A,sK202_skl)],[f461]) ).
fof(f2811,plain,
latt_str(sK202_skl),
inference(cnf_transformation,[status(thm)],[f2810]) ).
fof(f2823,plain,
( lattice(sK205_skl)
& join_absorbing(sK205_skl)
& meet_absorbing(sK205_skl)
& meet_associative(sK205_skl)
& meet_commutative(sK205_skl)
& join_associative(sK205_skl)
& join_commutative(sK205_skl)
& strict_latt_str(sK205_skl)
& ~ empty_carrier(sK205_skl)
& latt_str(sK205_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK205_skl]),skolemize(A,sK205_skl)],[f464]) ).
fof(f2824,plain,
latt_str(sK205_skl),
inference(cnf_transformation,[status(thm)],[f2823]) ).
fof(f3599,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ subset(the_carrier(C),the_carrier(B))
& subnetstr(C,A,B) )
& net_str(B,A) )
& one_sorted_str(A) ),
inference(pre_NNF_transformation,[status(thm)],[f596]) ).
fof(f3600,plain,
( ~ subset(the_carrier(sK409_skl),the_carrier(sK408_skl))
& subnetstr(sK409_skl,sK407_skl,sK408_skl)
& net_str(sK408_skl,sK407_skl)
& one_sorted_str(sK407_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK407_skl,sK408_skl,sK409_skl]),skolemize(A,sK407_skl),skolemize(B,sK408_skl),skolemize(C,sK409_skl)],[f3599]) ).
fof(f3601,plain,
one_sorted_str(sK407_skl),
inference(cnf_transformation,[status(thm)],[f3600]) ).
fof(f3602,plain,
net_str(sK408_skl,sK407_skl),
inference(cnf_transformation,[status(thm)],[f3600]) ).
fof(f3603,plain,
subnetstr(sK409_skl,sK407_skl,sK408_skl),
inference(cnf_transformation,[status(thm)],[f3600]) ).
fof(f3604,plain,
~ subset(the_carrier(sK409_skl),the_carrier(sK408_skl)),
inference(cnf_transformation,[status(thm)],[f3600]) ).
fof(f5362,plain,
! [X0,X1,X2] :
( subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1785,f1972]) ).
fof(f6752,plain,
! [X0,X1,X2] :
( ~ subnetstr(X1,X2,X0)
| ~ net_str(X0,X2)
| ~ one_sorted_str(X2)
| subset(the_carrier(X1),the_carrier(X0))
| ~ rel_str(X1)
| ~ rel_str(X0) ),
inference(resolution,[status(thm)],[f1111,f5362]) ).
fof(f6753,plain,
! [X0,X1,X2] :
( ~ subnetstr(X0,X2,X1)
| ~ net_str(X1,X2)
| ~ one_sorted_str(X2)
| subset(the_carrier(X0),the_carrier(X1))
| ~ rel_str(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6752,f1961]) ).
fof(f6778,plain,
( ~ net_str(sK408_skl,sK407_skl)
| ~ one_sorted_str(sK407_skl)
| subset(the_carrier(sK409_skl),the_carrier(sK408_skl))
| ~ rel_str(sK409_skl) ),
inference(resolution,[status(thm)],[f6753,f3603]) ).
fof(f6779,definition,
( sQ231_spl
<=> rel_str(sK409_skl) ),
introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition]) ).
fof(f6781,plain,
( sQ231_spl
| ~ rel_str(sK409_skl) ),
inference(component_clause,[status(thm)],[f6779]) ).
fof(f6782,definition,
( sQ232_spl
<=> subset(the_carrier(sK409_skl),the_carrier(sK408_skl)) ),
introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition]) ).
fof(f6783,plain,
( ~ sQ232_spl
| subset(the_carrier(sK409_skl),the_carrier(sK408_skl)) ),
inference(component_clause,[status(thm)],[f6782]) ).
fof(f6785,definition,
( sQ233_spl
<=> one_sorted_str(sK407_skl) ),
introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition]) ).
fof(f6787,plain,
( sQ233_spl
| ~ one_sorted_str(sK407_skl) ),
inference(component_clause,[status(thm)],[f6785]) ).
fof(f6788,definition,
( sQ234_spl
<=> net_str(sK408_skl,sK407_skl) ),
introduced(definition,[new_symbols(definition,[sQ234_spl])],[split_symbol_definition]) ).
fof(f6790,plain,
( sQ234_spl
| ~ net_str(sK408_skl,sK407_skl) ),
inference(component_clause,[status(thm)],[f6788]) ).
fof(f6791,plain,
( ~ sQ234_spl
| ~ sQ233_spl
| sQ232_spl
| ~ sQ231_spl ),
inference(split_clause,[status(thm)],[f6778,f6779,f6782,f6785,f6788]) ).
fof(f6792,plain,
( sQ234_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6790,f3602]) ).
fof(f6793,plain,
sQ234_spl,
inference(contradiction_clause,[status(thm)],[f6792]) ).
fof(f6794,plain,
( sQ233_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6787,f3601]) ).
fof(f6795,plain,
sQ233_spl,
inference(contradiction_clause,[status(thm)],[f6794]) ).
fof(f6796,plain,
( ~ sQ232_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6783,f3604]) ).
fof(f6797,plain,
~ sQ232_spl,
inference(contradiction_clause,[status(thm)],[f6796]) ).
fof(f6800,definition,
( sQ235_spl
<=> relation(sK200_skl) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f6802,plain,
( sQ235_spl
| ~ relation(sK200_skl) ),
inference(component_clause,[status(thm)],[f6800]) ).
fof(f6811,plain,
( sQ235_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6802,f2803]) ).
fof(f6812,plain,
sQ235_spl,
inference(contradiction_clause,[status(thm)],[f6811]) ).
fof(f6831,plain,
! [X0] :
( sQ231_spl
| ~ net_str(sK409_skl,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f6781,f1961]) ).
fof(f6832,plain,
! [X0,X1] :
( sQ231_spl
| ~ subnetstr(sK409_skl,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[status(thm)],[f6831,f1972]) ).
fof(f6833,plain,
! [X0,X1] :
( sQ231_spl
| ~ subnetstr(sK409_skl,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f6832]) ).
fof(f6860,definition,
( sQ241_spl
<=> latt_str(sK202_skl) ),
introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition]) ).
fof(f6862,plain,
( sQ241_spl
| ~ latt_str(sK202_skl) ),
inference(component_clause,[status(thm)],[f6860]) ).
fof(f6867,plain,
( sQ241_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6862,f2811]) ).
fof(f6868,plain,
sQ241_spl,
inference(contradiction_clause,[status(thm)],[f6867]) ).
fof(f6917,definition,
( sQ249_spl
<=> latt_str(sK205_skl) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f6919,plain,
( sQ249_spl
| ~ latt_str(sK205_skl) ),
inference(component_clause,[status(thm)],[f6917]) ).
fof(f6924,plain,
( sQ249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6919,f2824]) ).
fof(f6925,plain,
sQ249_spl,
inference(contradiction_clause,[status(thm)],[f6924]) ).
fof(f6968,plain,
( sQ231_spl
| ~ net_str(sK408_skl,sK407_skl)
| ~ one_sorted_str(sK407_skl) ),
inference(resolution,[status(thm)],[f6833,f3603]) ).
fof(f6969,plain,
( sQ231_spl
| ~ sQ234_spl
| ~ sQ233_spl ),
inference(split_clause,[status(thm)],[f6968,f6785,f6788,f6779]) ).
fof(f6970,plain,
$false,
inference(sat_refutation,[status(thm)],[f6791,f6793,f6795,f6797,f6812,f6868,f6925,f6969]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU373+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 06:17:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.42 % Drodi V4.1.1
% 0.58/0.63 % Refutation found
% 0.58/0.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.58/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.58/0.67 % Elapsed time: 0.291267 seconds
% 0.58/0.67 % CPU time: 1.686027 seconds
% 0.58/0.67 % Total memory used: 233.797 MB
% 0.58/0.67 % Net memory used: 231.876 MB
%------------------------------------------------------------------------------