%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT161+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 : n012.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.56s 0.83s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 7
% Syntax : Number of formulae : 30 ( 12 unt; 0 def)
% Number of atoms : 82 ( 25 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 84 ( 32 ~; 32 |; 12 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-4 aty)
% Number of variables : 90 ( 86 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f69,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] :
( hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2))
=> ! [B_xa] :
( hBOOL(hAPP(hAPP(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,axiom,
! [V_A_2,T_a] :
( class_Finite__Set_Ofinite(T_a)
=> c_Finite__Set_Ofinite(T_a,V_A_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f229,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f254,axiom,
~ c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(tc_Nat_Onat,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f388,axiom,
! [V_n] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n) = V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f415,axiom,
c_Orderings_Obot__class_Obot(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f518,axiom,
class_Finite__Set_Ofinite(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f742,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)
| ~ hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
| ~ hBOOL(hAPP(hAPP(c_member(T_a),B_x),V_A_2)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f743,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)
& hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
& hBOOL(hAPP(hAPP(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)
| ~ hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
| ~ hBOOL(hAPP(hAPP(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)],[f742]) ).
fof(f744,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)
& hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
& hBOOL(hAPP(hAPP(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)
| ~ hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
| ~ hBOOL(hAPP(hAPP(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)],[f743]) ).
fof(f745,plain,
( ! [V_A_2,V_f_2,T_a] :
( ( sK8_skl(T_a,V_f_2,V_A_2) != sK9_skl(T_a,V_f_2,V_A_2)
& hAPP(V_f_2,sK8_skl(T_a,V_f_2,V_A_2)) = hAPP(V_f_2,sK9_skl(T_a,V_f_2,V_A_2))
& hBOOL(hAPP(hAPP(c_member(T_a),sK9_skl(T_a,V_f_2,V_A_2)),V_A_2))
& hBOOL(hAPP(hAPP(c_member(T_a),sK8_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)
| ~ hBOOL(hAPP(hAPP(c_member(T_a),B_xa),V_A_2)) )
| ~ hBOOL(hAPP(hAPP(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,[sK8_skl,sK9_skl]),skolemize(B_x,sK8_skl(T_a,V_f_2,V_A_2)),skolemize(B_xa,sK9_skl(T_a,V_f_2,V_A_2))],[f744]) ).
fof(f749,plain,
! [X0,X1,X2,X3] :
( hAPP(X2,sK8_skl(X0,X2,X3)) = hAPP(X2,sK9_skl(X0,X2,X3))
| c_Fun_Oinj__on(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f745]) ).
fof(f750,plain,
! [X0,X1,X2,X3] :
( sK8_skl(X0,X2,X3) != sK9_skl(X0,X2,X3)
| c_Fun_Oinj__on(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f745]) ).
fof(f1113,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)],[f158]) ).
fof(f1114,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)],[f1113]) ).
fof(f1115,plain,
! [X0,X1] :
( c_Finite__Set_Ofinite(X0,X1)
| ~ class_Finite__Set_Ofinite(X0) ),
inference(cnf_transformation,[status(thm)],[f1114]) ).
fof(f1361,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)],[f229]) ).
fof(f1362,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)],[f1361]) ).
fof(f1440,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)],[f254]) ).
fof(f1802,plain,
! [X0] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f1891,plain,
c_Orderings_Obot__class_Obot(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(thm)],[f415]) ).
fof(f2203,plain,
class_Finite__Set_Ofinite(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f518]) ).
fof(f3102,plain,
! [X0] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X0) = X0,
inference(forward_demodulation,[status(thm)],[f1891,f1802]) ).
fof(f5110,plain,
! [X0,X1,X2] :
( sK8_skl(X0,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),sK9_skl(X0,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2))
| c_Fun_Oinj__on(X0,X1,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2) ),
inference(paramodulation,[status(thm)],[f3102,f749]) ).
fof(f5305,plain,
! [X0,X1,X2] :
( sK8_skl(X0,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2) = sK9_skl(X0,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2)
| c_Fun_Oinj__on(X0,X1,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2) ),
inference(forward_demodulation,[status(thm)],[f3102,f5110]) ).
fof(f5306,plain,
! [X0,X1,X2] : c_Fun_Oinj__on(X0,X1,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Orderings_Obot__class_Obot(tc_Nat_Onat)),X2),
inference(forward_subsumption_resolution,[status(thm)],[f5305,f750]) ).
fof(f5643,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)],[f1362,f1115]) ).
fof(f5649,plain,
! [X0,X1,X2] :
( ~ class_Finite__Set_Ofinite(X2)
| c_Finite__Set_Ofinite(X0,X1) ),
inference(resolution,[status(thm)],[f5643,f5306]) ).
fof(f5665,plain,
! [X0] : ~ class_Finite__Set_Ofinite(X0),
inference(resolution,[status(thm)],[f5649,f1440]) ).
fof(f5668,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f2203,f5665]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT161+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:35:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.42 % Drodi V4.1.1
% 0.56/0.83 % Refutation found
% 0.56/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.56/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.29/0.88 % Elapsed time: 0.502313 seconds
% 0.29/0.88 % CPU time: 3.203995 seconds
% 0.29/0.88 % Total memory used: 223.317 MB
% 0.29/0.88 % Net memory used: 219.500 MB
%------------------------------------------------------------------------------