%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET837-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:45 PM UTC 2026
% Result : Unsatisfiable 17.34s 2.67s
% Output : CNFRefutation 17.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 35
% Syntax : Number of formulae : 169 ( 13 unt; 22 def)
% Number of atoms : 403 ( 35 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 398 ( 164 ~; 212 |; 0 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 23 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 180 ( 180 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [V_U] :
( ~ c_lessequals(v_Y,V_U,tc_set(t_a))
| ~ c_lessequals(v_Z,V_U,tc_set(t_a))
| c_lessequals(v_X,V_U,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V_c,V_B,T_a,V_A] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [V_c,V_A,V_B,T_a] :
( c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,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(f11,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(f12,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(f13,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(f14,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f15,plain,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f16,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f17,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f18,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f19,plain,
! [X0] :
( ~ c_lessequals(v_Y,X0,tc_set(t_a))
| ~ c_lessequals(v_Z,X0,tc_set(t_a))
| c_lessequals(v_X,X0,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f20,plain,
! [V_c,V_B,T_a] :
( ! [V_A] : c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f21,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_union(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [V_c,V_A,T_a] :
( ! [V_B] : c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( c_in(X0,c_union(X1,X3,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [V_c,V_A,T_a] :
( c_in(V_c,V_A,T_a)
| ! [V_B] :
( c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f25,plain,
! [X0,X1,X2,X3] :
( c_in(X0,X1,X3)
| c_in(X0,X2,X3)
| ~ c_in(X0,c_union(X1,X2,X3),X3) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,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)],[f10]) ).
fof(f27,plain,
! [X0,X1,X2,X3] :
( c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f29,plain,
! [X0,X1,X2] :
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f30,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)],[f13]) ).
fof(f31,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)],[f30]) ).
fof(f32,definition,
( sQ0_spl
<=> v_X = c_union(v_Y,v_Z,t_a) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f33,plain,
( ~ sQ0_spl
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(component_clause,[status(thm)],[f32]) ).
fof(f35,definition,
( sQ1_spl
<=> c_lessequals(v_Y,v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f36,plain,
( ~ sQ1_spl
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f35]) ).
fof(f38,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f14,f32,f35]) ).
fof(f39,definition,
( sQ2_spl
<=> c_lessequals(v_Z,v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f40,plain,
( ~ sQ2_spl
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f39]) ).
fof(f42,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f15,f32,f39]) ).
fof(f43,definition,
( sQ3_spl
<=> c_lessequals(v_Y,v_x,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f44,plain,
( ~ sQ3_spl
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f43]) ).
fof(f46,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| ~ sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f16,f43,f39,f35,f32]) ).
fof(f47,definition,
( sQ4_spl
<=> c_lessequals(v_Z,v_x,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f48,plain,
( ~ sQ4_spl
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f47]) ).
fof(f50,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| ~ sQ2_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f17,f47,f39,f35,f32]) ).
fof(f51,definition,
( sQ5_spl
<=> c_lessequals(v_X,v_x,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f53,plain,
( sQ5_spl
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f51]) ).
fof(f54,plain,
( ~ sQ0_spl
| ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f18,f51,f39,f35,f32]) ).
fof(f55,definition,
! [X0] :
( sQ6_spl
<=> ( ~ c_lessequals(v_Y,X0,tc_set(t_a))
| ~ c_lessequals(v_Z,X0,tc_set(t_a))
| c_lessequals(v_X,X0,tc_set(t_a)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f56,plain,
! [X0] :
( ~ sQ6_spl
| ~ c_lessequals(v_Y,X0,tc_set(t_a))
| ~ c_lessequals(v_Z,X0,tc_set(t_a))
| c_lessequals(v_X,X0,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f55]) ).
fof(f58,plain,
( sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f19,f32,f55]) ).
fof(f65,plain,
! [X0,X1] :
( c_lessequals(X0,X0,tc_set(X1))
| c_lessequals(X0,X0,tc_set(X1)) ),
inference(resolution,[status(thm)],[f29,f28]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_union(X1,X2,X3),X3),X1,X3)
| c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3)) ),
inference(resolution,[status(thm)],[f29,f23]) ).
fof(f67,plain,
! [X0,X1,X2,X3] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_union(X1,X2,X3),X3),X2,X3)
| c_lessequals(X0,c_union(X1,X2,X3),tc_set(X3)) ),
inference(resolution,[status(thm)],[f29,f21]) ).
fof(f68,plain,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
inference(duplicate_literals_removal,[status(thm)],[f65]) ).
fof(f77,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2)
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X1,X2) ),
inference(resolution,[status(thm)],[f25,f28]) ).
fof(f81,plain,
! [X0] :
( ~ sQ1_spl
| c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Y,t_a) ),
inference(resolution,[status(thm)],[f27,f36]) ).
fof(f82,plain,
! [X0] :
( ~ sQ4_spl
| c_in(X0,v_x,t_a)
| ~ c_in(X0,v_Z,t_a) ),
inference(resolution,[status(thm)],[f27,f48]) ).
fof(f102,plain,
! [X0] :
( ~ sQ2_spl
| c_in(X0,v_X,t_a)
| ~ c_in(X0,v_Z,t_a) ),
inference(resolution,[status(thm)],[f40,f27]) ).
fof(f113,plain,
! [X0] :
( ~ sQ3_spl
| c_in(X0,v_x,t_a)
| ~ c_in(X0,v_Y,t_a) ),
inference(resolution,[status(thm)],[f44,f27]) ).
fof(f140,plain,
! [X0,X1,X2] :
( c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2))
| c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f66,f28]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_in(c_Main_OsubsetI__1(X0,c_union(c_union(X1,X2,X3),X4,X3),X3),X1,X3)
| c_lessequals(X0,c_union(c_union(X1,X2,X3),X4,X3),tc_set(X3)) ),
inference(resolution,[status(thm)],[f66,f23]) ).
fof(f143,plain,
! [X0] :
( ~ sQ0_spl
| ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,c_union(v_Y,v_Z,t_a),tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f33,f66]) ).
fof(f144,plain,
! [X0,X1,X2] : c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)),
inference(duplicate_literals_removal,[status(thm)],[f140]) ).
fof(f145,plain,
! [X0] :
( ~ sQ0_spl
| ~ c_in(c_Main_OsubsetI__1(X0,v_X,t_a),v_Y,t_a)
| c_lessequals(X0,v_X,tc_set(t_a)) ),
inference(forward_demodulation,[status(thm)],[f33,f143]) ).
fof(f146,plain,
! [X0,X1,X2] :
( c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2))
| c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f67,f28]) ).
fof(f150,plain,
! [X0,X1,X2] : c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)),
inference(duplicate_literals_removal,[status(thm)],[f146]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X3,X1,X2),X2),X0,X2) ),
inference(resolution,[status(thm)],[f77,f67]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X1,X3,X2),X2),X0,X2) ),
inference(resolution,[status(thm)],[f77,f66]) ).
fof(f154,plain,
! [X0,X1,X2] :
( c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X1,X2),X0,X2) ),
inference(resolution,[status(thm)],[f77,f29]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X3,X1,X2),X2),X0,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f152]) ).
fof(f159,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),c_union(X1,X3,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X1,X3,X2),X2),X0,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f153]) ).
fof(f160,plain,
! [X0,X1,X2] :
( c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X1,X2),X0,X2) ),
inference(duplicate_literals_removal,[status(thm)],[f154]) ).
fof(f169,plain,
! [X0,X1,X2] :
( X0 = c_union(X0,X1,X2)
| ~ c_lessequals(c_union(X0,X1,X2),X0,tc_set(X2)) ),
inference(resolution,[status(thm)],[f144,f31]) ).
fof(f172,plain,
! [X0,X1,X2] :
( X1 = c_union(X0,X1,X2)
| ~ c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2)) ),
inference(resolution,[status(thm)],[f150,f31]) ).
fof(f191,plain,
! [X0] :
( ~ sQ6_spl
| ~ c_lessequals(v_Y,c_union(X0,v_Z,t_a),tc_set(t_a))
| c_lessequals(v_X,c_union(X0,v_Z,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f56,f150]) ).
fof(f194,definition,
( sQ20_spl
<=> c_lessequals(v_X,v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f196,plain,
( sQ20_spl
| ~ c_lessequals(v_X,v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f194]) ).
fof(f216,definition,
( sQ21_spl
<=> v_X = c_union(v_Y,v_X,t_a) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( ~ sQ21_spl
| v_X = c_union(v_Y,v_X,t_a) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f229,plain,
! [X0,X1,X2,X3,X4] :
( c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X4,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X4,X2),X2),X0,X2)
| c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X4,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f141,f77]) ).
fof(f233,plain,
! [X0,X1,X2,X3,X4] :
( c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X4,X2),X2),X0,X2)
| c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X4,X2),tc_set(X2)) ),
inference(duplicate_literals_removal,[status(thm)],[f229]) ).
fof(f308,plain,
( ~ sQ0_spl
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f33,f150]) ).
fof(f309,plain,
( ~ sQ0_spl
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f33,f144]) ).
fof(f335,definition,
( sQ26_spl
<=> c_lessequals(v_Y,v_Y,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( sQ26_spl
| ~ c_lessequals(v_Y,v_Y,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f463,plain,
! [X0,X1] :
( ~ sQ4_spl
| c_in(c_Main_OsubsetI__1(c_union(v_Z,X0,t_a),c_union(X1,X0,t_a),t_a),v_x,t_a)
| c_lessequals(c_union(v_Z,X0,t_a),c_union(X1,X0,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f158,f82]) ).
fof(f565,plain,
! [X0,X1,X2] :
( c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f159,f67]) ).
fof(f576,plain,
! [X0,X1,X2] : c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)),
inference(duplicate_literals_removal,[status(thm)],[f565]) ).
fof(f588,plain,
! [X0] :
( ~ sQ1_spl
| c_in(c_Main_OsubsetI__1(c_union(v_Y,X0,t_a),X0,t_a),v_X,t_a)
| c_lessequals(c_union(v_Y,X0,t_a),X0,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f160,f81]) ).
fof(f850,plain,
! [X0,X1,X2] :
( c_union(X1,X0,X2) = c_union(X0,X1,X2)
| ~ c_lessequals(c_union(X0,X1,X2),c_union(X1,X0,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f576,f31]) ).
fof(f854,plain,
! [X0,X1,X2] : c_union(X0,X1,X2) = c_union(X1,X0,X2),
inference(forward_subsumption_resolution,[status(thm)],[f850,f576]) ).
fof(f893,plain,
! [X0,X1,X2] :
( X1 = c_union(X1,X0,X2)
| ~ c_lessequals(c_union(X0,X1,X2),X1,tc_set(X2)) ),
inference(paramodulation,[status(thm)],[f854,f169]) ).
fof(f949,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X0,X2),tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X0,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[f233,f67]) ).
fof(f969,plain,
! [X0,X1,X2,X3] : c_lessequals(c_union(X0,X1,X2),c_union(c_union(X1,X3,X2),X0,X2),tc_set(X2)),
inference(duplicate_literals_removal,[status(thm)],[f949]) ).
fof(f1114,plain,
( ~ sQ0_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f308,f39,f32]) ).
fof(f1117,plain,
( ~ sQ0_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f309,f35,f32]) ).
fof(f1238,plain,
! [X0] :
( ~ sQ2_spl
| c_lessequals(c_union(v_Z,X0,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_Z,X0,t_a),X0,t_a),v_X,t_a) ),
inference(resolution,[status(thm)],[f102,f160]) ).
fof(f1256,plain,
! [X0] :
( ~ sQ3_spl
| c_lessequals(c_union(v_Y,X0,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_Y,X0,t_a),X0,t_a),v_x,t_a) ),
inference(resolution,[status(thm)],[f113,f160]) ).
fof(f1442,plain,
( ~ sQ0_spl
| c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f145,f160]) ).
fof(f1455,definition,
( sQ40_spl
<=> c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1456,plain,
( ~ sQ40_spl
| c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f1455]) ).
fof(f1458,plain,
( ~ sQ0_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1442,f1455,f32]) ).
fof(f1539,plain,
( ~ sQ40_spl
| v_X = c_union(v_Y,v_X,t_a) ),
inference(resolution,[status(thm)],[f1456,f172]) ).
fof(f1544,plain,
( ~ sQ40_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1539,f216,f1455]) ).
fof(f1545,definition,
( sQ41_spl
<=> c_lessequals(v_X,c_union(v_Y,v_X,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1547,plain,
( sQ41_spl
| ~ c_lessequals(v_X,c_union(v_Y,v_X,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f1545]) ).
fof(f1549,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1547,f150]) ).
fof(f1550,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1549]) ).
fof(f1624,plain,
( ~ sQ21_spl
| v_X = c_union(v_X,v_Y,t_a) ),
inference(paramodulation,[status(thm)],[f854,f217]) ).
fof(f1718,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f196,f68]) ).
fof(f1719,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1718]) ).
fof(f1856,plain,
( ~ sQ21_spl
| v_X = c_union(v_X,v_Y,t_a)
| ~ c_lessequals(v_X,v_X,tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f1624,f169]) ).
fof(f1897,definition,
( sQ45_spl
<=> v_X = c_union(v_X,v_Y,t_a) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1900,plain,
( ~ sQ21_spl
| sQ45_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f1856,f194,f1897,f216]) ).
fof(f2085,definition,
( sQ48_spl
<=> c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2086,plain,
( ~ sQ48_spl
| c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f2085]) ).
fof(f2213,definition,
( sQ50_spl
<=> c_union(v_Z,v_Y,t_a) = v_X ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f2214,plain,
( ~ sQ50_spl
| c_union(v_Z,v_Y,t_a) = v_X ),
inference(component_clause,[status(thm)],[f2213]) ).
fof(f2215,plain,
( sQ50_spl
| c_union(v_Z,v_Y,t_a) != v_X ),
inference(component_clause,[status(thm)],[f2213]) ).
fof(f2343,plain,
( sQ50_spl
| c_union(v_Y,v_Z,t_a) != v_X ),
inference(paramodulation,[status(thm)],[f854,f2215]) ).
fof(f2345,plain,
( sQ50_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f2343,f32,f2213]) ).
fof(f2542,plain,
( ~ sQ48_spl
| v_X = c_union(v_Z,v_X,t_a) ),
inference(resolution,[status(thm)],[f2086,f172]) ).
fof(f2547,definition,
( sQ54_spl
<=> c_lessequals(v_X,c_union(v_Z,v_X,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f2549,plain,
( sQ54_spl
| ~ c_lessequals(v_X,c_union(v_Z,v_X,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f2547]) ).
fof(f2554,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2549,f150]) ).
fof(f2555,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f2554]) ).
fof(f5428,plain,
! [X0] :
( ~ sQ48_spl
| c_lessequals(c_union(X0,v_Z,t_a),c_union(v_X,X0,t_a),tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f2542,f969]) ).
fof(f5810,plain,
( ~ sQ1_spl
| c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Y,v_X,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f588,f29]) ).
fof(f5833,plain,
( ~ sQ1_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f5810,f1455,f35]) ).
fof(f12166,definition,
( sQ87_spl
<=> c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f12168,plain,
( sQ87_spl
| ~ c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f12166]) ).
fof(f12691,plain,
( ~ sQ2_spl
| c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f1238,f29]) ).
fof(f12714,plain,
( ~ sQ2_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f12691,f2085,f39]) ).
fof(f14296,plain,
( ~ sQ21_spl
| ~ sQ48_spl
| c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f1624,f5428]) ).
fof(f14898,plain,
( ~ sQ3_spl
| c_lessequals(c_union(v_Y,v_x,t_a),v_x,tc_set(t_a))
| c_lessequals(c_union(v_Y,v_x,t_a),v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f1256,f29]) ).
fof(f14920,definition,
( sQ149_spl
<=> c_lessequals(c_union(v_Y,v_x,t_a),v_x,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f14921,plain,
( ~ sQ149_spl
| c_lessequals(c_union(v_Y,v_x,t_a),v_x,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f14920]) ).
fof(f14923,plain,
( ~ sQ3_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f14898,f14920,f43]) ).
fof(f14938,plain,
( ~ sQ149_spl
| v_x = c_union(v_x,v_Y,t_a) ),
inference(resolution,[status(thm)],[f14921,f893]) ).
fof(f14942,definition,
( sQ153_spl
<=> c_lessequals(v_x,c_union(v_Y,v_x,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f14944,plain,
( sQ153_spl
| ~ c_lessequals(v_x,c_union(v_Y,v_x,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f14942]) ).
fof(f14949,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14944,f150]) ).
fof(f14950,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f14949]) ).
fof(f15186,definition,
( sQ169_spl
<=> c_lessequals(c_union(v_Z,v_Y,t_a),c_union(v_x,v_Y,t_a),tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f15187,plain,
( ~ sQ169_spl
| c_lessequals(c_union(v_Z,v_Y,t_a),c_union(v_x,v_Y,t_a),tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f15186]) ).
fof(f15317,definition,
( sQ174_spl
<=> c_lessequals(v_x,v_x,tc_set(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f15319,plain,
( sQ174_spl
| ~ c_lessequals(v_x,v_x,tc_set(t_a)) ),
inference(component_clause,[status(thm)],[f15317]) ).
fof(f15364,plain,
( sQ174_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15319,f68]) ).
fof(f15365,plain,
sQ174_spl,
inference(contradiction_clause,[status(thm)],[f15364]) ).
fof(f15366,plain,
( ~ sQ169_spl
| ~ sQ50_spl
| c_lessequals(v_X,c_union(v_x,v_Y,t_a),tc_set(t_a)) ),
inference(forward_demodulation,[status(thm)],[f2214,f15187]) ).
fof(f15367,plain,
( ~ sQ169_spl
| ~ sQ50_spl
| ~ sQ149_spl
| c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(forward_demodulation,[status(thm)],[f14938,f15366]) ).
fof(f15368,plain,
( ~ sQ169_spl
| ~ sQ50_spl
| ~ sQ149_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15367,f53]) ).
fof(f15369,plain,
( ~ sQ169_spl
| ~ sQ50_spl
| ~ sQ149_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f15368]) ).
fof(f15806,plain,
( ~ sQ149_spl
| ~ sQ4_spl
| c_in(c_Main_OsubsetI__1(c_union(v_Z,v_Y,t_a),v_x,t_a),v_x,t_a)
| c_lessequals(c_union(v_Z,v_Y,t_a),c_union(v_x,v_Y,t_a),tc_set(t_a)) ),
inference(paramodulation,[status(thm)],[f14938,f463]) ).
fof(f15841,definition,
( sQ190_spl
<=> c_in(c_Main_OsubsetI__1(c_union(v_Z,v_Y,t_a),v_x,t_a),v_x,t_a) ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f15842,plain,
( ~ sQ190_spl
| c_in(c_Main_OsubsetI__1(c_union(v_Z,v_Y,t_a),v_x,t_a),v_x,t_a) ),
inference(component_clause,[status(thm)],[f15841]) ).
fof(f15844,plain,
( ~ sQ149_spl
| ~ sQ4_spl
| sQ190_spl
| sQ169_spl ),
inference(split_clause,[status(thm)],[f15806,f15186,f15841,f47,f14920]) ).
fof(f15865,plain,
( ~ sQ190_spl
| ~ sQ50_spl
| c_in(c_Main_OsubsetI__1(v_X,v_x,t_a),v_x,t_a) ),
inference(forward_demodulation,[status(thm)],[f2214,f15842]) ).
fof(f16177,plain,
( ~ sQ190_spl
| ~ sQ50_spl
| c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f15865,f29]) ).
fof(f16178,plain,
( ~ sQ190_spl
| ~ sQ50_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f16177,f51,f2213,f15841]) ).
fof(f16287,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f337,f68]) ).
fof(f16288,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f16287]) ).
fof(f17824,plain,
( ~ sQ6_spl
| c_lessequals(v_X,c_union(v_Y,v_Z,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[f191,f144]) ).
fof(f17955,plain,
( ~ sQ6_spl
| v_X = c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[f17824,f31]) ).
fof(f17957,plain,
( ~ sQ6_spl
| sQ0_spl
| ~ sQ87_spl ),
inference(split_clause,[status(thm)],[f17955,f12166,f32,f55]) ).
fof(f17958,plain,
( sQ87_spl
| ~ sQ21_spl
| ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12168,f14296]) ).
fof(f17959,plain,
( sQ87_spl
| ~ sQ21_spl
| ~ sQ48_spl ),
inference(contradiction_clause,[status(thm)],[f17958]) ).
fof(f17960,plain,
$false,
inference(sat_refutation,[status(thm)],[f38,f42,f46,f50,f54,f58,f1114,f1117,f1458,f1544,f1550,f1719,f1900,f2345,f2555,f5833,f12714,f14923,f14950,f15365,f15369,f15844,f16178,f16288,f17957,f17959]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET837-2 : 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.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:43:37 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 17.34/2.67 % Refutation found
% 17.34/2.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.34/2.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.25/2.71 % Elapsed time: 2.328400 seconds
% 8.25/2.71 % CPU time: 18.115370 seconds
% 8.25/2.71 % Total memory used: 259.709 MB
% 8.25/2.71 % Net memory used: 238.275 MB
%------------------------------------------------------------------------------