%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 03:07:42 PM UTC 2026
% Result : Theorem 29.73s 5.45s
% Output : CNFRefutation 27.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 12
% Syntax : Number of formulae : 46 ( 14 unt; 5 def)
% Number of atoms : 100 ( 15 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 98 ( 44 ~; 43 |; 0 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 45 ( 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [V_h_2,T_c,V_F_2,T_b] :
( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2))
=> hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [V_A_2,V_B_2,T_b] :
( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))
=> V_A_2 = V_B_2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [V_A_2,V_B_2,T_b] :
( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))
=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5224,hypothesis,
hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),v_U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5225,hypothesis,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5226,hypothesis,
hAPP(c_Finite__Set_Ocard(t_a),v_G) = hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5228,conjecture,
v_G = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5229,negated_conjecture,
v_G != hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),
inference(negated_conjecture,[status(cth)],[f5228]) ).
fof(f5235,plain,
! [V_h_2,T_c,V_F_2,T_b] :
( hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2)))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f5236,plain,
! [V_F_2,T_b] :
( ! [V_h_2,T_c] : hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2)))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2)) ),
inference(miniscoping,[status(thm)],[f5235]) ).
fof(f5237,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(c_Finite__Set_Ofinite(X2),hAPP(c_Set_Oimage(X0,X2,X3),X1)))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f5236]) ).
fof(f5272,plain,
! [V_A_2,V_B_2,T_b] :
( V_A_2 = V_B_2
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f5273,plain,
! [V_B_2,T_b] :
( ! [V_A_2] :
( V_A_2 = V_B_2
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)) )
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2)) ),
inference(miniscoping,[status(thm)],[f5272]) ).
fof(f5274,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(X0),X1)),hAPP(c_Finite__Set_Ocard(X0),X2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X2),X1))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f5273]) ).
fof(f5275,plain,
! [V_A_2,V_B_2,T_b] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f5276,plain,
! [V_B_2,T_b] :
( ! [V_A_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)) )
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2)) ),
inference(miniscoping,[status(thm)],[f5275]) ).
fof(f5277,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(X0),X2)),hAPP(c_Finite__Set_Ocard(X0),X1)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X2),X1))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f5276]) ).
fof(f20146,plain,
hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),v_U)),
inference(cnf_transformation,[status(thm)],[f5224]) ).
fof(f20147,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))),
inference(cnf_transformation,[status(thm)],[f5225]) ).
fof(f20148,plain,
hAPP(c_Finite__Set_Ocard(t_a),v_G) = hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)),
inference(cnf_transformation,[status(thm)],[f5226]) ).
fof(f20150,plain,
v_G != hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),
inference(cnf_transformation,[status(thm)],[f5229]) ).
fof(f20986,plain,
! [X0,X1] : hBOOL(hAPP(c_Finite__Set_Ofinite(X0),hAPP(c_Set_Oimage(tc_Com_Opname,X0,X1),v_U))),
inference(resolution,[status(thm)],[f20146,f5237]) ).
fof(f21116,plain,
! [X0] :
( X0 = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(paramodulation,[status(thm)],[f20148,f5274]) ).
fof(f21118,definition,
( sQ15_spl
<=> hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f21120,plain,
( sQ15_spl
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(component_clause,[status(thm)],[f21118]) ).
fof(f21121,definition,
! [X0] :
( sQ16_spl
<=> ( X0 = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f21122,plain,
! [X0] :
( ~ sQ16_spl
| X0 = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(component_clause,[status(thm)],[f21121]) ).
fof(f21124,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f21116,f21118,f21121]) ).
fof(f21125,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21120,f20986]) ).
fof(f21126,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f21125]) ).
fof(f21136,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))))
| ~ hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(resolution,[status(thm)],[f20147,f5277]) ).
fof(f21148,definition,
( sQ19_spl
<=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f21149,plain,
( ~ sQ19_spl
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))) ),
inference(component_clause,[status(thm)],[f21148]) ).
fof(f21151,plain,
( sQ19_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f21136,f21118,f21148]) ).
fof(f21156,definition,
( sQ21_spl
<=> hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U) = v_G ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f21157,plain,
( ~ sQ21_spl
| hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U) = v_G ),
inference(component_clause,[status(thm)],[f21156]) ).
fof(f21164,plain,
( ~ sQ19_spl
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),v_G))) ),
inference(forward_demodulation,[status(thm)],[f20148,f21149]) ).
fof(f29760,plain,
( ~ sQ19_spl
| ~ sQ16_spl
| v_G = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(resolution,[status(thm)],[f21122,f21164]) ).
fof(f29762,definition,
( sQ71_spl
<=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f29764,plain,
( sQ71_spl
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
inference(component_clause,[status(thm)],[f29762]) ).
fof(f29765,plain,
( ~ sQ19_spl
| ~ sQ16_spl
| sQ21_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f29760,f29762,f21156,f21121,f21148]) ).
fof(f29773,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21157,f20150]) ).
fof(f29774,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f29773]) ).
fof(f29775,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29764,f20147]) ).
fof(f29776,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f29775]) ).
fof(f29777,plain,
$false,
inference(sat_refutation,[status(thm)],[f21124,f21126,f21151,f29765,f29774,f29776]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n008.cluster.edu
% 0.18/0.49 % Model : x86_64 x86_64
% 0.18/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49 % Memory : 8046.5625MB
% 0.18/0.49 % OS : Linux 6.8.0-71-generic
% 0.18/0.49 % CPULimit : 300
% 0.18/0.49 % WCLimit : 300
% 0.18/0.49 % DateTime : Mon Sep 21 09:50:09 UTC 2026
% 0.18/0.49 % CPUTime :
% 1.28/1.60 % Drodi V4.1.1
% 29.73/5.45 % Refutation found
% 29.73/5.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.73/5.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.89/5.67 % Elapsed time: 5.149543 seconds
% 5.89/5.67 % CPU time: 31.434767 seconds
% 5.89/5.67 % Total memory used: 906.846 MB
% 5.89/5.67 % Net memory used: 896.079 MB
%------------------------------------------------------------------------------