%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:07:01 PM UTC 2026
% Result : Theorem 0.14s 0.65s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 36 ( 8 unt; 2 def)
% Number of atoms : 102 ( 31 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 110 ( 44 ~; 41 |; 14 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-4 aty)
% Number of variables : 99 ( 95 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
! [V_A_2,V_f_2,T_b,T_a] :
( c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2)
<=> ! [B_x] :
( c_member(T_a,B_x,V_A_2)
=> ! [B_xa] :
( c_member(T_a,B_xa,V_A_2)
=> ( hAPP(V_f_2,B_x) = hAPP(V_f_2,B_xa)
=> B_x = B_xa ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [V_A_2,T_a] :
( class_Finite__Set_Ofinite(T_a)
=> c_Finite__Set_Ofinite(T_a,V_A_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [V_A_2,V_f_2,T_b,T_a] :
( c_Finite__Set_Ofinite(T_a,c_Set_Oimage(T_b,T_a,V_f_2,V_A_2))
=> ( c_Fun_Oinj__on(T_b,T_a,V_f_2,V_A_2)
=> c_Finite__Set_Ofinite(T_b,V_A_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f223,axiom,
~ c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(tc_Nat_Onat,tc_HOL_Obool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f237,axiom,
! [V_nat_H_2,V_nat_2] :
( hAPP(c_Nat_OSuc,V_nat_2) = hAPP(c_Nat_OSuc,V_nat_H_2)
<=> V_nat_2 = V_nat_H_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f527,axiom,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f557,plain,
! [V_A_2,V_f_2,T_b,T_a] :
( c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2)
<=> ! [B_x] :
( ! [B_xa] :
( B_x = B_xa
| hAPP(V_f_2,B_x) != hAPP(V_f_2,B_xa)
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f558,plain,
! [V_A_2,V_f_2,T_b,T_a] :
( ( ? [B_x] :
( ? [B_xa] :
( B_x != B_xa
& hAPP(V_f_2,B_x) = hAPP(V_f_2,B_xa)
& c_member(T_a,B_xa,V_A_2) )
& c_member(T_a,B_x,V_A_2) )
| c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) )
& ( ! [B_x] :
( ! [B_xa] :
( B_x = B_xa
| hAPP(V_f_2,B_x) != hAPP(V_f_2,B_xa)
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ~ c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) ) ),
inference(NNF_transformation,[status(thm)],[f557]) ).
fof(f559,plain,
( ! [V_A_2,V_f_2,T_a] :
( ? [B_x] :
( ? [B_xa] :
( B_x != B_xa
& hAPP(V_f_2,B_x) = hAPP(V_f_2,B_xa)
& c_member(T_a,B_xa,V_A_2) )
& c_member(T_a,B_x,V_A_2) )
| ! [T_b] : c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) )
& ! [V_A_2,V_f_2,T_a] :
( ! [B_x] :
( ! [B_xa] :
( B_x = B_xa
| hAPP(V_f_2,B_x) != hAPP(V_f_2,B_xa)
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ! [T_b] : ~ c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) ) ),
inference(miniscoping,[status(thm)],[f558]) ).
fof(f560,plain,
( ! [V_A_2,V_f_2,T_a] :
( ( sK1_skl(T_a,V_f_2,V_A_2) != sK2_skl(T_a,V_f_2,V_A_2)
& hAPP(V_f_2,sK1_skl(T_a,V_f_2,V_A_2)) = hAPP(V_f_2,sK2_skl(T_a,V_f_2,V_A_2))
& c_member(T_a,sK2_skl(T_a,V_f_2,V_A_2),V_A_2)
& c_member(T_a,sK1_skl(T_a,V_f_2,V_A_2),V_A_2) )
| ! [T_b] : c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) )
& ! [V_A_2,V_f_2,T_a] :
( ! [B_x] :
( ! [B_xa] :
( B_x = B_xa
| hAPP(V_f_2,B_x) != hAPP(V_f_2,B_xa)
| ~ c_member(T_a,B_xa,V_A_2) )
| ~ c_member(T_a,B_x,V_A_2) )
| ! [T_b] : ~ c_Fun_Oinj__on(T_a,T_b,V_f_2,V_A_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B_x,sK1_skl(T_a,V_f_2,V_A_2)),skolemize(B_xa,sK2_skl(T_a,V_f_2,V_A_2))],[f559]) ).
fof(f564,plain,
! [X0,X1,X2,X3] :
( hAPP(X2,sK1_skl(X0,X2,X3)) = hAPP(X2,sK2_skl(X0,X2,X3))
| c_Fun_Oinj__on(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f565,plain,
! [X0,X1,X2,X3] :
( sK1_skl(X0,X2,X3) != sK2_skl(X0,X2,X3)
| c_Fun_Oinj__on(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f560]) ).
fof(f577,plain,
! [V_A_2,T_a] :
( c_Finite__Set_Ofinite(T_a,V_A_2)
| ~ class_Finite__Set_Ofinite(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f578,plain,
! [T_a] :
( ! [V_A_2] : c_Finite__Set_Ofinite(T_a,V_A_2)
| ~ class_Finite__Set_Ofinite(T_a) ),
inference(miniscoping,[status(thm)],[f577]) ).
fof(f579,plain,
! [X0,X1] :
( c_Finite__Set_Ofinite(X0,X1)
| ~ class_Finite__Set_Ofinite(X0) ),
inference(cnf_transformation,[status(thm)],[f578]) ).
fof(f602,plain,
! [V_A_2,V_f_2,T_b,T_a] :
( c_Finite__Set_Ofinite(T_b,V_A_2)
| ~ c_Fun_Oinj__on(T_b,T_a,V_f_2,V_A_2)
| ~ c_Finite__Set_Ofinite(T_a,c_Set_Oimage(T_b,T_a,V_f_2,V_A_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f603,plain,
! [X0,X1,X2,X3] :
( c_Finite__Set_Ofinite(X1,X3)
| ~ c_Fun_Oinj__on(X1,X0,X2,X3)
| ~ c_Finite__Set_Ofinite(X0,c_Set_Oimage(X1,X0,X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f602]) ).
fof(f1271,plain,
~ c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(tc_Nat_Onat,tc_HOL_Obool))),
inference(cnf_transformation,[status(thm)],[f223]) ).
fof(f1302,plain,
! [V_nat_H_2,V_nat_2] :
( ( V_nat_2 != V_nat_H_2
| hAPP(c_Nat_OSuc,V_nat_2) = hAPP(c_Nat_OSuc,V_nat_H_2) )
& ( V_nat_2 = V_nat_H_2
| hAPP(c_Nat_OSuc,V_nat_2) != hAPP(c_Nat_OSuc,V_nat_H_2) ) ),
inference(NNF_transformation,[status(thm)],[f237]) ).
fof(f1303,plain,
( ! [V_nat_H_2,V_nat_2] :
( V_nat_2 != V_nat_H_2
| hAPP(c_Nat_OSuc,V_nat_2) = hAPP(c_Nat_OSuc,V_nat_H_2) )
& ! [V_nat_H_2,V_nat_2] :
( V_nat_2 = V_nat_H_2
| hAPP(c_Nat_OSuc,V_nat_2) != hAPP(c_Nat_OSuc,V_nat_H_2) ) ),
inference(miniscoping,[status(thm)],[f1302]) ).
fof(f1304,plain,
! [X0,X1] :
( X0 = X1
| hAPP(c_Nat_OSuc,X0) != hAPP(c_Nat_OSuc,X1) ),
inference(cnf_transformation,[status(thm)],[f1303]) ).
fof(f2172,plain,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
inference(cnf_transformation,[status(thm)],[f527]) ).
fof(f2412,plain,
! [X0,X1,X2,X3] :
( ~ class_Finite__Set_Ofinite(X1)
| c_Finite__Set_Ofinite(X0,X3)
| ~ c_Fun_Oinj__on(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f603,f579]) ).
fof(f2514,plain,
! [X0,X1,X2] :
( c_Fun_Oinj__on(X0,X2,c_Nat_OSuc,X1)
| sK1_skl(X0,c_Nat_OSuc,X1) = sK2_skl(X0,c_Nat_OSuc,X1) ),
inference(resolution,[status(thm)],[f1304,f564]) ).
fof(f2519,plain,
! [X0,X1,X2] : c_Fun_Oinj__on(X0,X1,c_Nat_OSuc,X2),
inference(forward_subsumption_resolution,[status(thm)],[f2514,f565]) ).
fof(f2720,definition,
! [X0,X1] :
( sQ40_spl
<=> c_Finite__Set_Ofinite(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f2721,plain,
! [X0,X1] :
( ~ sQ40_spl
| c_Finite__Set_Ofinite(X0,X1) ),
inference(component_clause,[status(thm)],[f2720]) ).
fof(f2984,plain,
! [X0,X1,X2] :
( ~ class_Finite__Set_Ofinite(X2)
| c_Finite__Set_Ofinite(X0,X1) ),
inference(resolution,[status(thm)],[f2412,f2519]) ).
fof(f2986,definition,
! [X2] :
( sQ61_spl
<=> ~ class_Finite__Set_Ofinite(X2) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f2987,plain,
! [X0] :
( ~ sQ61_spl
| ~ class_Finite__Set_Ofinite(X0) ),
inference(component_clause,[status(thm)],[f2986]) ).
fof(f2989,plain,
( sQ61_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f2984,f2720,f2986]) ).
fof(f2991,plain,
( ~ sQ40_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1271,f2721]) ).
fof(f2992,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f2991]) ).
fof(f3016,plain,
( ~ sQ61_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2172,f2987]) ).
fof(f3018,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f3016]) ).
fof(f3019,plain,
$false,
inference(sat_refutation,[status(thm)],[f2989,f2992,f3018]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n004.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 04:35:37 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.14/0.60 % Drodi V4.1.1
% 0.14/0.65 % Refutation found
% 0.14/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.68 % Elapsed time: 0.122530 seconds
% 0.14/0.68 % CPU time: 0.417833 seconds
% 0.14/0.68 % Total memory used: 144.652 MB
% 0.14/0.68 % Net memory used: 143.995 MB
%------------------------------------------------------------------------------