%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT166+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 : 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 02:07:02 PM UTC 2026
% Result : Theorem 117.95s 25.44s
% Output : CNFRefutation 117.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 44 ( 18 unt; 0 def)
% Number of atoms : 95 ( 21 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 89 ( 38 ~; 32 |; 11 &)
% ( 3 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-6 aty)
% Number of variables : 113 ( 107 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f40,axiom,
! [V_A_2,V_x_2,T_a] :
( hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2))
<=> hBOOL(hAPP(V_A_2,V_x_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f211,axiom,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_n),V_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f257,axiom,
c_Finite__Set_Ocard(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool))) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f353,axiom,
! [V_m] : hAPP(c_Nat_OSuc,V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f400,axiom,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f427,axiom,
! [V_A_2,T_a] :
( ( ~ c_Finite__Set_Ofinite(T_a,V_A_2)
=> c_Finite__Set_Ocard(T_a,V_A_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
& ( c_Finite__Set_Ofinite(T_a,V_A_2)
=> c_Finite__Set_Ocard(T_a,V_A_2) = c_Finite__Set_Ofold__image(tc_Nat_Onat,T_a,c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(c_COMBK(tc_Nat_Onat,T_a),c_Groups_Oone__class_Oone(tc_Nat_Onat)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_A_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f433,axiom,
! [V_ha_2,T_b,V_Fa_2,T_a] :
( c_Finite__Set_Ofinite(T_a,V_Fa_2)
=> c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_ha_2,V_Fa_2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f446,axiom,
! [T_b,T_a,V_x_2,V_f_2,V_ba_2] :
( V_ba_2 = hAPP(V_f_2,V_x_2)
=> hBOOL(hAPP(hAPP(c_member(T_a),V_ba_2),c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f486,axiom,
! [V_N_2] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)
<=> ? [B_m] :
! [B_x] :
( hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f525,axiom,
! [V_P,T_a] : hAPP(c_COMBI(T_a),V_P) = V_P,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f651,plain,
! [V_A_2,V_x_2,T_a] :
( ( ~ hBOOL(hAPP(V_A_2,V_x_2))
| hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)) )
& ( hBOOL(hAPP(V_A_2,V_x_2))
| ~ hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f652,plain,
( ! [V_A_2,V_x_2] :
( ~ hBOOL(hAPP(V_A_2,V_x_2))
| ! [T_a] : hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)) )
& ! [V_A_2,V_x_2] :
( hBOOL(hAPP(V_A_2,V_x_2))
| ! [T_a] : ~ hBOOL(hAPP(hAPP(c_member(T_a),V_x_2),V_A_2)) ) ),
inference(miniscoping,[status(thm)],[f651]) ).
fof(f653,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X2,X1))
| ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f654,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f1298,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X0),X0)),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f1431,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = c_Finite__Set_Ocard(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool))),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f1718,plain,
! [X0] : hAPP(c_Nat_OSuc,X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(thm)],[f353]) ).
fof(f1849,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f1920,plain,
! [V_A_2,T_a] :
( ( c_Finite__Set_Ocard(T_a,V_A_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Finite__Set_Ofinite(T_a,V_A_2) )
& ( c_Finite__Set_Ocard(T_a,V_A_2) = c_Finite__Set_Ofold__image(tc_Nat_Onat,T_a,c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(c_COMBK(tc_Nat_Onat,T_a),c_Groups_Oone__class_Oone(tc_Nat_Onat)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_A_2)
| ~ c_Finite__Set_Ofinite(T_a,V_A_2) ) ),
inference(pre_NNF_transformation,[status(thm)],[f427]) ).
fof(f1921,plain,
( ! [V_A_2,T_a] :
( c_Finite__Set_Ocard(T_a,V_A_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Finite__Set_Ofinite(T_a,V_A_2) )
& ! [V_A_2,T_a] :
( c_Finite__Set_Ocard(T_a,V_A_2) = c_Finite__Set_Ofold__image(tc_Nat_Onat,T_a,c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(c_COMBK(tc_Nat_Onat,T_a),c_Groups_Oone__class_Oone(tc_Nat_Onat)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_A_2)
| ~ c_Finite__Set_Ofinite(T_a,V_A_2) ) ),
inference(miniscoping,[status(thm)],[f1920]) ).
fof(f1923,plain,
! [X0,X1] :
( c_Finite__Set_Ocard(X0,X1) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Finite__Set_Ofinite(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1921]) ).
fof(f1937,plain,
! [V_ha_2,T_b,V_Fa_2,T_a] :
( c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_ha_2,V_Fa_2))
| ~ c_Finite__Set_Ofinite(T_a,V_Fa_2) ),
inference(pre_NNF_transformation,[status(thm)],[f433]) ).
fof(f1938,plain,
! [V_Fa_2,T_a] :
( ! [V_ha_2,T_b] : c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_ha_2,V_Fa_2))
| ~ c_Finite__Set_Ofinite(T_a,V_Fa_2) ),
inference(miniscoping,[status(thm)],[f1937]) ).
fof(f1939,plain,
! [X0,X1,X2,X3] :
( ~ c_Finite__Set_Ofinite(X1,X3)
| c_Finite__Set_Ofinite(X0,c_Set_Oimage(X1,X0,X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f1938]) ).
fof(f1986,plain,
! [T_b,T_a,V_x_2,V_f_2,V_ba_2] :
( hBOOL(hAPP(hAPP(c_member(T_a),V_ba_2),c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool)))))
| V_ba_2 != hAPP(V_f_2,V_x_2) ),
inference(pre_NNF_transformation,[status(thm)],[f446]) ).
fof(f1987,plain,
! [V_f_2,V_ba_2] :
( ! [T_b,T_a] : hBOOL(hAPP(hAPP(c_member(T_a),V_ba_2),c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool)))))
| ! [V_x_2] : V_ba_2 != hAPP(V_f_2,V_x_2) ),
inference(miniscoping,[status(thm)],[f1986]) ).
fof(f1988,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(c_member(X3),X0),c_Set_Oimage(X4,X3,X1,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))))
| X0 != hAPP(X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1987]) ).
fof(f2092,plain,
! [V_N_2] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)
<=> ? [B_m] :
! [B_x] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f486]) ).
fof(f2093,plain,
! [V_N_2] :
( ( ! [B_m] :
? [B_x] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) )
| c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) )
& ( ? [B_m] :
! [B_x] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) ) ),
inference(NNF_transformation,[status(thm)],[f2092]) ).
fof(f2094,plain,
( ! [V_N_2] :
( ! [B_m] :
? [B_x] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) )
| c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) )
& ! [V_N_2] :
( ? [B_m] :
! [B_x] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),B_m))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) ) ),
inference(miniscoping,[status(thm)],[f2093]) ).
fof(f2095,plain,
( ! [V_N_2] :
( ! [B_m] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),sK41_skl(B_m,V_N_2)),B_m))
& hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),sK41_skl(B_m,V_N_2)),V_N_2)) )
| c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) )
& ! [V_N_2] :
( ! [B_x] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),B_x),sK40_skl(V_N_2)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),B_x),V_N_2)) )
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl,sK41_skl]),skolemize(B_m,sK40_skl(V_N_2)),skolemize(B_x,sK41_skl(B_m,V_N_2))],[f2094]) ).
fof(f2096,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),sK40_skl(X0)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X1),X0))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(cnf_transformation,[status(thm)],[f2095]) ).
fof(f2165,plain,
! [X0,X1] : hAPP(c_COMBI(X0),X1) = X1,
inference(cnf_transformation,[status(thm)],[f525]) ).
fof(f2285,plain,
! [X0,X1,X2,X3] : hBOOL(hAPP(hAPP(c_member(X0),hAPP(X1,X2)),c_Set_Oimage(X3,X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))),
inference(destructive_equality_resolution,[status(thm)],[f1988]) ).
fof(f2640,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(paramodulation,[status(thm)],[f1849,f1718]) ).
fof(f2888,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),sK40_skl(X0)),X0))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(resolution,[status(thm)],[f2096,f1298]) ).
fof(f2910,plain,
! [X0] :
( ~ hBOOL(hAPP(X0,sK40_skl(X0)))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X0) ),
inference(resolution,[status(thm)],[f2888,f654]) ).
fof(f4307,plain,
( c_Finite__Set_Ofinite(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))
| c_Groups_Oone__class_Oone(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(paramodulation,[status(thm)],[f1923,f1431]) ).
fof(f4309,plain,
c_Finite__Set_Ofinite(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool))),
inference(forward_subsumption_resolution,[status(thm)],[f4307,f2640]) ).
fof(f4897,plain,
! [X0,X1,X2,X3] : hBOOL(hAPP(c_Set_Oimage(X0,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),hAPP(X2,X3))),
inference(resolution,[status(thm)],[f2285,f653]) ).
fof(f5013,plain,
! [X0,X1,X2,X3] : hBOOL(hAPP(c_Set_Oimage(X0,X1,c_COMBI(X2),c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),X3)),
inference(paramodulation,[status(thm)],[f2165,f4897]) ).
fof(f5487,plain,
! [X0,X1,X2] : ~ c_Finite__Set_Ofinite(tc_Nat_Onat,c_Set_Oimage(X0,X1,c_COMBI(X2),c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))),
inference(resolution,[status(thm)],[f5013,f2910]) ).
fof(f5489,plain,
! [X0] : ~ c_Finite__Set_Ofinite(X0,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),
inference(resolution,[status(thm)],[f5487,f1939]) ).
fof(f5513,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f4309,f5489]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT166+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.38 % Computer : n008.cluster.edu
% 0.12/10.38 % Model : x86_64 x86_64
% 0.12/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.38 % Memory : 8046.5625MB
% 0.12/10.38 % OS : Linux 6.8.0-71-generic
% 0.12/10.38 % CPULimit : 300
% 0.12/10.38 % WCLimit : 300
% 0.12/10.38 % DateTime : Mon Sep 21 04:36:06 UTC 2026
% 0.12/10.39 % CPUTime :
% 0.16/10.46 % Drodi V4.1.1
% 117.95/25.44 % Refutation found
% 117.95/25.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 117.95/25.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.78/25.94 % Elapsed time: 15.539214 seconds
% 6.78/25.94 % CPU time: 119.597842 seconds
% 6.78/25.94 % Total memory used: 814.610 MB
% 6.78/25.94 % Net memory used: 765.081 MB
%------------------------------------------------------------------------------