%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET860-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:10:51 PM UTC 2026
% Result : Unsatisfiable 52.12s 7.11s
% Output : CNFRefutation 46.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 23
% Syntax : Number of formulae : 90 ( 18 unt; 6 def)
% Number of atoms : 232 ( 6 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 265 ( 123 ~; 136 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 7 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 155 ( 155 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f138,axiom,
! [T_a,V_i,V_k] :
( c_lessequals(V_i,V_k,T_a)
| ~ c_in(V_i,c_SetInterval_OatMost(V_k,T_a),T_a)
| ~ class_Orderings_Oord(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,axiom,
! [T_a,V_i,V_k] :
( c_in(V_i,c_SetInterval_OatMost(V_k,T_a),T_a)
| ~ c_lessequals(V_i,V_k,T_a)
| ~ class_Orderings_Oord(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f141,axiom,
! [T_a,V_x,V_y] :
( c_lessequals(c_SetInterval_OatMost(V_x,T_a),c_SetInterval_OatMost(V_y,T_a),tc_set(T_a))
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [V_A,V_X,T_a,V_C] :
( c_in(V_A,c_Union(V_C,T_a),T_a)
| ~ c_in(V_X,V_C,tc_set(T_a))
| ~ c_in(V_A,V_X,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,axiom,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f297,axiom,
! [V_A,V_C,T_a] :
( c_in(c_Main_OUnionE__1(V_A,V_C,T_a),V_C,tc_set(T_a))
| ~ c_in(V_A,c_Union(V_C,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f298,axiom,
! [V_A,V_C,T_a] :
( c_in(V_A,c_Main_OUnionE__1(V_A,V_C,T_a),T_a)
| ~ c_in(V_A,c_Union(V_C,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f299,axiom,
! [V_A,T_a] : c_lessequals(c_emptyset,V_A,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f306,axiom,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f307,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f308,axiom,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f309,axiom,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f447,axiom,
! [T_1] : class_Orderings_Oorder(tc_set(T_1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f652,axiom,
! [T] :
( class_Orderings_Oord(T)
| ~ class_Orderings_Oorder(T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1358,negated_conjecture,
~ c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1359,negated_conjecture,
~ c_lessequals(v_B,c_Union(v_C,t_a),tc_set(t_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1360,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,v_C,tc_set(t_a))
| c_lessequals(V_U,v_A,tc_set(t_a))
| c_lessequals(v_B,V_U,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1550,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,X2)
| ~ class_Orderings_Oord(X2)
| ~ c_in(X0,c_SetInterval_OatMost(X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f1551,plain,
! [X0,X1,X2] :
( c_in(X0,c_SetInterval_OatMost(X1,X2),X2)
| ~ class_Orderings_Oord(X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f1553,plain,
! [X0,X1,X2] :
( ~ class_Orderings_Oorder(X1)
| ~ c_lessequals(X0,X2,X1)
| c_lessequals(c_SetInterval_OatMost(X0,X1),c_SetInterval_OatMost(X2,X1),tc_set(X1)) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f1598,plain,
! [V_A,T_a,V_C] :
( c_in(V_A,c_Union(V_C,T_a),T_a)
| ! [V_X] :
( ~ c_in(V_X,V_C,tc_set(T_a))
| ~ c_in(V_A,V_X,T_a) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f1599,plain,
! [X0,X1,X2,X3] :
( ~ c_in(X3,X0,X2)
| c_in(X3,c_Union(X1,X2),X2)
| ~ c_in(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1598]) ).
fof(f1600,plain,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f1761,plain,
! [X0,X1,X2] :
( c_in(c_Main_OUnionE__1(X0,X1,X2),X1,tc_set(X2))
| ~ c_in(X0,c_Union(X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f1762,plain,
! [X0,X1,X2] :
( ~ c_in(X0,c_Union(X1,X2),X2)
| c_in(X0,c_Main_OUnionE__1(X0,X1,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f298]) ).
fof(f1763,plain,
! [X0,X1] : c_lessequals(c_emptyset,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f299]) ).
fof(f1773,plain,
! [V_c,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ! [V_A] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ) ),
inference(miniscoping,[status(thm)],[f306]) ).
fof(f1774,plain,
! [X0,X1,X2,X3] :
( ~ c_lessequals(X1,X3,tc_set(X2))
| c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1773]) ).
fof(f1775,plain,
! [X0,X1,X2] :
( c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f307]) ).
fof(f1776,plain,
! [X0,X1,X2] :
( ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f1777,plain,
! [V_B,V_A] :
( V_A = V_B
| ! [T_a] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f309]) ).
fof(f1778,plain,
! [X0,X1,X2] :
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1777]) ).
fof(f1924,plain,
! [X0] : class_Orderings_Oorder(tc_set(X0)),
inference(cnf_transformation,[status(thm)],[f447]) ).
fof(f2130,plain,
! [X0] :
( ~ class_Orderings_Oorder(X0)
| class_Orderings_Oord(X0) ),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f2836,plain,
~ c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a)),
inference(cnf_transformation,[status(thm)],[f1358]) ).
fof(f2837,plain,
~ c_lessequals(v_B,c_Union(v_C,t_a),tc_set(t_a)),
inference(cnf_transformation,[status(thm)],[f1359]) ).
fof(f2838,plain,
! [X0] :
( c_lessequals(X0,v_A,tc_set(t_a))
| ~ c_in(X0,v_C,tc_set(t_a))
| c_lessequals(v_B,X0,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f1360]) ).
fof(f5301,plain,
! [X0,X1] : ~ c_in(X0,c_Union(c_emptyset,X1),X1),
inference(resolution,[status(thm)],[f1761,f1600]) ).
fof(f5302,plain,
! [X0] :
( c_lessequals(c_Main_OUnionE__1(X0,v_C,t_a),v_A,tc_set(t_a))
| c_lessequals(v_B,c_Main_OUnionE__1(X0,v_C,t_a),tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a) ),
inference(resolution,[status(thm)],[f1761,f2838]) ).
fof(f5339,plain,
! [X0,X1] :
( c_lessequals(v_B,c_Main_OUnionE__1(X1,v_C,t_a),tc_set(t_a))
| c_in(X0,v_A,t_a)
| ~ c_in(X1,c_Union(v_C,t_a),t_a)
| ~ c_in(X0,c_Main_OUnionE__1(X1,v_C,t_a),t_a) ),
inference(resolution,[status(thm)],[f5302,f1774]) ).
fof(f5341,plain,
! [X0,X1,X2] :
( ~ c_in(X2,c_Union(v_C,t_a),t_a)
| ~ c_in(X1,v_B,t_a)
| ~ c_in(X0,c_Main_OUnionE__1(X2,v_C,t_a),t_a)
| c_in(X1,c_Main_OUnionE__1(X2,v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ),
inference(resolution,[status(thm)],[f5339,f1774]) ).
fof(f5467,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_emptyset,tc_set(X1))
| X0 = c_emptyset ),
inference(resolution,[status(thm)],[f1763,f1778]) ).
fof(f5708,plain,
! [X0,X1,X2,X3] :
( c_in(X1,c_SetInterval_OatMost(X3,X0),X0)
| ~ c_lessequals(X2,X3,X0)
| ~ c_in(X1,c_SetInterval_OatMost(X2,X0),X0)
| ~ class_Orderings_Oorder(X0) ),
inference(resolution,[status(thm)],[f1553,f1774]) ).
fof(f5716,plain,
! [X0,X1,X2,X3] :
( ~ class_Orderings_Oord(X0)
| ~ c_lessequals(X3,X1,X0)
| c_in(X3,c_SetInterval_OatMost(X2,X0),X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(resolution,[status(thm)],[f5708,f1551]) ).
fof(f5718,plain,
! [X0,X1,X2,X3] :
( ~ class_Orderings_Oorder(X2)
| ~ c_lessequals(X1,X3,X2)
| c_in(X0,c_SetInterval_OatMost(X3,X2),X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f5716,f2130]) ).
fof(f5771,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X0,X3,X2)
| ~ class_Orderings_Oord(X2)
| ~ class_Orderings_Oorder(X2)
| ~ c_lessequals(X1,X3,X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(resolution,[status(thm)],[f5718,f1550]) ).
fof(f5772,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X3,X1,X2)
| ~ class_Orderings_Oorder(X2)
| ~ c_lessequals(X3,X0,X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f5771,f2130]) ).
fof(f5816,definition,
( sQ21_spl
<=> class_Orderings_Oorder(tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f5818,plain,
( sQ21_spl
| ~ class_Orderings_Oorder(tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f5816]) ).
fof(f5840,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5818,f1924]) ).
fof(f5841,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f5840]) ).
fof(f7658,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X0,c_Union(X1,X2),tc_set(X2))
| ~ c_in(X3,X1,tc_set(X2))
| ~ c_in(c_Main_OsubsetI__1(X0,c_Union(X1,X2),X2),X3,X2) ),
inference(resolution,[status(thm)],[f1776,f1599]) ).
fof(f9733,plain,
! [X0,X1,X2] :
( c_lessequals(X0,c_Union(X1,X2),tc_set(X2))
| ~ c_in(X0,X1,tc_set(X2))
| c_lessequals(X0,c_Union(X1,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f1775,f7658]) ).
fof(f9744,plain,
! [X0,X1] : c_lessequals(c_Union(c_emptyset,X0),X1,tc_set(X0)),
inference(resolution,[status(thm)],[f1775,f5301]) ).
fof(f9774,plain,
! [X0,X1,X2] :
( ~ c_in(X0,X1,tc_set(X2))
| c_lessequals(X0,c_Union(X1,X2),tc_set(X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f9733]) ).
fof(f9842,plain,
! [X0] : c_emptyset = c_Union(c_emptyset,X0),
inference(resolution,[status(thm)],[f9744,f5467]) ).
fof(f11864,plain,
! [X0,X1] :
( c_in(X1,c_Main_OUnionE__1(X0,v_C,t_a),t_a)
| ~ c_in(X1,v_B,t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a) ),
inference(resolution,[status(thm)],[f1762,f5341]) ).
fof(f11865,plain,
! [X0,X1] :
( ~ c_in(X1,c_Union(v_C,t_a),t_a)
| c_in(X1,v_A,t_a)
| ~ c_in(X0,v_B,t_a)
| c_in(X0,c_Main_OUnionE__1(X1,v_C,t_a),t_a) ),
inference(duplicate_literals_removal,[status(thm)],[f11864]) ).
fof(f11867,plain,
! [X0,X1] :
( ~ c_in(c_Main_OsubsetI__1(X1,c_Main_OUnionE__1(X0,v_C,t_a),t_a),v_B,t_a)
| c_in(X0,v_A,t_a)
| c_lessequals(X1,c_Main_OUnionE__1(X0,v_C,t_a),tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a) ),
inference(resolution,[status(thm)],[f11865,f1776]) ).
fof(f12548,plain,
! [X0] :
( c_lessequals(v_B,c_Main_OUnionE__1(X0,v_C,t_a),tc_set(t_a))
| c_lessequals(v_B,c_Main_OUnionE__1(X0,v_C,t_a),tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ),
inference(resolution,[status(thm)],[f11867,f1775]) ).
fof(f12549,plain,
! [X0] :
( c_in(X0,v_A,t_a)
| c_lessequals(v_B,c_Main_OUnionE__1(X0,v_C,t_a),tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a) ),
inference(duplicate_literals_removal,[status(thm)],[f12548]) ).
fof(f12626,plain,
! [X0,X1] :
( c_lessequals(v_B,X1,tc_set(t_a))
| ~ class_Orderings_Oorder(tc_set(t_a))
| ~ c_lessequals(c_Main_OUnionE__1(X0,v_C,t_a),X1,tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ),
inference(resolution,[status(thm)],[f12549,f5772]) ).
fof(f12631,definition,
! [X0,X1] :
( sQ230_spl
<=> ( c_lessequals(v_B,X1,tc_set(t_a))
| ~ c_lessequals(c_Main_OUnionE__1(X0,v_C,t_a),X1,tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f12632,plain,
! [X0,X1] :
( ~ sQ230_spl
| c_lessequals(v_B,X1,tc_set(t_a))
| ~ c_lessequals(c_Main_OUnionE__1(X0,v_C,t_a),X1,tc_set(t_a))
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ),
inference(component_clause,[status(thm)],[f12631]) ).
fof(f12634,plain,
( ~ sQ21_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f12626,f12631,f5816]) ).
fof(f12687,plain,
! [X0,X1] :
( ~ sQ230_spl
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a)
| c_lessequals(v_B,c_Union(X1,t_a),tc_set(t_a))
| ~ c_in(c_Main_OUnionE__1(X0,v_C,t_a),X1,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f12632,f9774]) ).
fof(f13050,definition,
( sQ250_spl
<=> c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ250_spl])],[split_symbol_definition]) ).
fof(f13051,plain,
( ~ sQ250_spl
| c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f13050]) ).
fof(f13054,plain,
( ~ sQ250_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13051,f2836]) ).
fof(f13055,plain,
~ sQ250_spl,
inference(contradiction_clause,[status(thm)],[f13054]) ).
fof(f14210,plain,
! [X0] :
( ~ sQ230_spl
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a)
| c_lessequals(v_B,c_Union(v_C,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f12687,f1761]) ).
fof(f14236,definition,
( sQ289_spl
<=> c_lessequals(v_B,c_Union(v_C,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition]) ).
fof(f14237,plain,
( ~ sQ289_spl
| c_lessequals(v_B,c_Union(v_C,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f14236]) ).
fof(f14239,definition,
! [X0] :
( sQ290_spl
<=> ( ~ c_in(X0,c_Union(v_C,t_a),t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ) ),
introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition]) ).
fof(f14240,plain,
! [X0] :
( ~ sQ290_spl
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a)
| c_in(X0,v_A,t_a) ),
inference(component_clause,[status(thm)],[f14239]) ).
fof(f14242,plain,
( ~ sQ230_spl
| sQ290_spl
| sQ289_spl ),
inference(split_clause,[status(thm)],[f14210,f14236,f14239,f12631]) ).
fof(f14286,plain,
( ~ sQ289_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14237,f2837]) ).
fof(f14287,plain,
~ sQ289_spl,
inference(contradiction_clause,[status(thm)],[f14286]) ).
fof(f14288,plain,
! [X0] :
( ~ sQ290_spl
| c_in(X0,v_A,t_a)
| ~ c_in(X0,c_Union(v_C,t_a),t_a) ),
inference(duplicate_literals_removal,[status(thm)],[f14240]) ).
fof(f14289,plain,
! [X0] :
( ~ sQ290_spl
| c_in(c_Main_OsubsetI__1(c_Union(v_C,t_a),X0,t_a),v_A,t_a)
| c_lessequals(c_Union(v_C,t_a),X0,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f14288,f1775]) ).
fof(f14531,definition,
( sQ308_spl
<=> c_lessequals(v_B,c_Union(c_emptyset,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition]) ).
fof(f14532,plain,
( ~ sQ308_spl
| c_lessequals(v_B,c_Union(c_emptyset,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f14531]) ).
fof(f14554,plain,
( ~ sQ308_spl
| c_lessequals(v_B,c_emptyset,tc_set(t_a)) ),
inference(forward_demodulation,[status(thm)],[f9842,f14532]) ).
fof(f14555,plain,
( ~ sQ308_spl
| c_emptyset = v_B ),
inference(resolution,[status(thm)],[f14554,f5467]) ).
fof(f14621,plain,
! [X0,X1] :
( ~ sQ308_spl
| c_lessequals(v_B,X0,tc_set(X1)) ),
inference(backward_demodulation,[status(thm)],[f14555,f1763]) ).
fof(f14729,plain,
( ~ sQ308_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2837,f14621]) ).
fof(f14739,plain,
~ sQ308_spl,
inference(contradiction_clause,[status(thm)],[f14729]) ).
fof(f14879,plain,
( ~ sQ290_spl
| c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a))
| c_lessequals(c_Union(v_C,t_a),v_A,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f14289,f1776]) ).
fof(f14880,plain,
( ~ sQ290_spl
| sQ250_spl ),
inference(split_clause,[status(thm)],[f14879,f13050,f14239]) ).
fof(f14882,plain,
$false,
inference(sat_refutation,[status(thm)],[f5841,f12634,f13055,f14242,f14287,f14739,f14880]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET860-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 05:41:36 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 52.12/7.11 % Refutation found
% 52.12/7.11 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 52.12/7.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.53/7.26 % Elapsed time: 6.890932 seconds
% 3.53/7.26 % CPU time: 53.560222 seconds
% 3.53/7.26 % Total memory used: 591.519 MB
% 3.53/7.26 % Net memory used: 548.236 MB
%------------------------------------------------------------------------------