%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT163+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 08:28:35 AM UTC 2026
% Result : Theorem 239.60s 40.32s
% Output : CNFRefutation 239.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 97 ( 83 unt; 0 def)
% Number of atoms : 116 ( 102 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 42 ( 23 ~; 13 |; 0 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 3 con; 0-5 aty)
% Number of variables : 266 ( 69 sgn 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_nat__neq__iff,axiom,
! [V_na_2,V_m_2] :
( V_m_2 != V_na_2
<=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_na_2),V_m_2))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_m_2),V_na_2)) ) ),
file('theBenchmark.p',fact_nat__neq__iff) ).
fof(fact_inv__f__eq,axiom,
! [V_y_2,V_x_2,V_f_2,T_b,T_a] :
( c_Fun_Oinj__on(T_a,T_b,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)))
=> ( hAPP(V_f_2,V_x_2) = V_y_2
=> hAPP(c_Hilbert__Choice_Oinv__into(T_a,T_b,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)),V_f_2),V_y_2) = V_x_2 ) ),
file('theBenchmark.p',fact_inv__f__eq) ).
fof(fact_inv__f__f,axiom,
! [V_x_2,V_f_2,T_b,T_a] :
( c_Fun_Oinj__on(T_a,T_b,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)))
=> hAPP(c_Hilbert__Choice_Oinv__into(T_a,T_b,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)),V_f_2),hAPP(V_f_2,V_x_2)) = V_x_2 ),
file('theBenchmark.p',fact_inv__f__f) ).
fof(fact_inj__eq,axiom,
! [V_y_2,V_x_2,V_f_2,T_b,T_a] :
( c_Fun_Oinj__on(T_a,T_b,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)))
=> ( hAPP(V_f_2,V_x_2) = hAPP(V_f_2,V_y_2)
<=> V_x_2 = V_y_2 ) ),
file('theBenchmark.p',fact_inj__eq) ).
fof(fact_Nat_Oadd__0__right,axiom,
! [V_m] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_m),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = V_m,
file('theBenchmark.p',fact_Nat_Oadd__0__right) ).
fof(fact_less__add__Suc1,axiom,
! [V_m,V_i] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_i),hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_i),V_m)))),
file('theBenchmark.p',fact_less__add__Suc1) ).
fof(fact_Suc__eq__plus1,axiom,
! [V_n] : hAPP(c_Nat_OSuc,V_n) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),V_n),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
file('theBenchmark.p',fact_Suc__eq__plus1) ).
fof(help_c__COMBB__1,axiom,
! [V_R_2,V_Q_2,V_Pa_2,T_c,T_a,T_b] : hAPP(hAPP(c_COMBB(T_b,T_a,T_c,V_Pa_2),V_Q_2),V_R_2) = hAPP(V_Pa_2,hAPP(V_Q_2,V_R_2)),
file('theBenchmark.p',help_c__COMBB__1) ).
fof(help_c__COMBS__1,axiom,
! [V_R_2,V_Q_2,V_Pa_2,T_a,T_c,T_b] : hAPP(c_COMBS(T_b,T_c,T_a,V_Pa_2,V_Q_2),V_R_2) = hAPP(hAPP(V_Pa_2,V_R_2),hAPP(V_Q_2,V_R_2)),
file('theBenchmark.p',help_c__COMBS__1) ).
fof(fact_inj__on__id2,axiom,
! [V_A_2,T_a] : c_Fun_Oinj__on(T_a,T_a,c_COMBI(T_a),V_A_2),
file('theBenchmark.p',fact_inj__on__id2) ).
fof(fact_list_Osimps_I5_J,axiom,
! [V_list_2,V_aa_2,V_f2_2,V_f1_2,T_b,T_a] : c_List_Olist_Olist__case(T_a,T_b,V_f1_2,V_f2_2,c_List_Olist_OCons(T_b,V_aa_2,V_list_2)) = hAPP(hAPP(V_f2_2,V_aa_2),V_list_2),
file('theBenchmark.p',fact_list_Osimps_I5_J) ).
fof(fact_nat_Osize_I2_J,axiom,
! [V_nat] : c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,V_nat)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Onat_Onat__size(V_nat)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
file('theBenchmark.p',fact_nat_Osize_I2_J) ).
fof(fact_nat_Osize_I4_J,axiom,
! [V_nat] : c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,V_nat)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Osize__class_Osize(tc_Nat_Onat,V_nat)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
file('theBenchmark.p',fact_nat_Osize_I4_J) ).
fof(fact_nat__size,axiom,
! [V_n] : c_Nat_Osize__class_Osize(tc_Nat_Onat,V_n) = V_n,
file('theBenchmark.p',fact_nat__size) ).
fof(fact_list_Osize_I2_J,axiom,
! [V_list_2,V_aa_2,V_fa_2,T_a] : c_List_Olist_Olist__size(T_a,V_fa_2,c_List_Olist_OCons(T_a,V_aa_2,V_list_2)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(V_fa_2,V_aa_2)),c_List_Olist_Olist__size(T_a,V_fa_2,V_list_2))),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
file('theBenchmark.p',fact_list_Osize_I2_J) ).
fof(fact_list_Osize_I1_J,axiom,
! [V_fa_2,T_a] : c_List_Olist_Olist__size(T_a,V_fa_2,c_List_Olist_ONil(T_a)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('theBenchmark.p',fact_list_Osize_I1_J) ).
fof(fact_nat__case__Suc,axiom,
! [V_nat_2,V_f2_2,V_f1_2,T_a] : c_Nat_Onat_Onat__case(T_a,V_f1_2,V_f2_2,hAPP(c_Nat_OSuc,V_nat_2)) = hAPP(V_f2_2,V_nat_2),
file('theBenchmark.p',fact_nat__case__Suc) ).
fof(help_c__COMBI__1,axiom,
! [V_P,T_a] : hAPP(c_COMBI(T_a),V_P) = V_P,
file('theBenchmark.p',help_c__COMBI__1) ).
cnf(c_523,plain,
c_Fun_Oinj__on(A,A,c_COMBI(A),B),
inference(clausify,[status(thm)],[fact_inj__on__id2]) ).
cnf(c_557,plain,
c_List_Olist_Olist__case(A,B,C,D,c_List_Olist_OCons(B,E,F)) = hAPP(hAPP(D,E),F),
inference(clausify,[status(thm)],[fact_list_Osimps_I5_J]) ).
cnf(c_752,plain,
c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Onat_Onat__size(A)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(clausify,[status(thm)],[fact_nat_Osize_I2_J]) ).
cnf(c_753,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Onat_Onat__size(A)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)),
inference(copy,[status(thm)],[c_752]) ).
cnf(c_754,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(clausify,[status(thm)],[fact_nat_Osize_I4_J]) ).
cnf(c_755,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)),
inference(copy,[status(thm)],[c_754]) ).
cnf(c_756,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,A) = A,
inference(clausify,[status(thm)],[fact_nat__size]) ).
fof(fact_nat_Osize_I1_J,axiom,
c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('theBenchmark.p',fact_nat_Osize_I1_J) ).
cnf(c_758,plain,
c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(clausify,[status(thm)],[fact_nat_Osize_I1_J]) ).
cnf(c_759,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,D)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(B,C)),c_List_Olist_Olist__size(A,B,D))),hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(clausify,[status(thm)],[fact_list_Osize_I2_J]) ).
cnf(c_765,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_ONil(A)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(clausify,[status(thm)],[fact_list_Osize_I1_J]) ).
cnf(c_790,plain,
c_Nat_Onat_Onat__case(A,B,C,hAPP(c_Nat_OSuc,D)) = hAPP(C,D),
inference(clausify,[status(thm)],[fact_nat__case__Suc]) ).
cnf(c_824,plain,
hAPP(c_COMBI(A),B) = B,
inference(clausify,[status(thm)],[help_c__COMBI__1]) ).
cnf(c_859,plain,
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B))
| A != B ),
inference(clausify,[status(thm)],[fact_nat__neq__iff]) ).
cnf(c_878,plain,
( hAPP(c_Hilbert__Choice_Oinv__into(A,B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),C),E) = D
| hAPP(C,D) != E
| ~ c_Fun_Oinj__on(A,B,C,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool))) ),
inference(clausify,[status(thm)],[fact_inv__f__eq]) ).
cnf(c_879,plain,
( hAPP(c_Hilbert__Choice_Oinv__into(A,B,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),C),hAPP(C,D)) = D
| ~ c_Fun_Oinj__on(A,B,C,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool))) ),
inference(clausify,[status(thm)],[fact_inv__f__f]) ).
cnf(c_884,plain,
( D != E
| hAPP(C,D) = hAPP(C,E)
| ~ c_Fun_Oinj__on(A,B,C,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool))) ),
inference(clausify,[status(thm)],[fact_inj__eq]) ).
cnf(c_1057,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = A,
inference(clausify,[status(thm)],[fact_Nat_Oadd__0__right]) ).
cnf(c_1121,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)))),
inference(clausify,[status(thm)],[fact_less__add__Suc1]) ).
fof(fact_One__nat__def,axiom,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('theBenchmark.p',fact_One__nat__def) ).
cnf(c_1131,plain,
c_Groups_Oone__class_Oone(tc_Nat_Onat) = hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(clausify,[status(thm)],[fact_One__nat__def]) ).
cnf(c_1132,plain,
hAPP(c_Nat_OSuc,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Groups_Oone__class_Oone(tc_Nat_Onat),
inference(copy,[status(thm)],[c_1131]) ).
cnf(c_1137,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = hAPP(c_Nat_OSuc,A),
inference(clausify,[status(thm)],[fact_Suc__eq__plus1]) ).
cnf(c_1192,plain,
hAPP(hAPP(c_COMBB(A,B,C,D),E),F) = hAPP(D,hAPP(E,F)),
inference(clausify,[status(thm)],[help_c__COMBB__1]) ).
cnf(c_1194,plain,
hAPP(c_COMBS(A,B,C,D,E),F) = hAPP(hAPP(D,F),hAPP(E,F)),
inference(clausify,[status(thm)],[help_c__COMBS__1]) ).
cnf(c_20063,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,D)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(B,C)),c_List_Olist_Olist__size(A,B,D))),c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_1132,c_759]) ).
cnf(c_1225,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,D)) = hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(B,C)),c_List_Olist_Olist__size(A,B,D))),
inference(paramod,[status(thm)],[c_1137,c_20063]) ).
cnf(c_20064,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)),
inference(paramod,[status(thm)],[c_1132,c_755]) ).
cnf(c_20065,plain,
hAPP(c_Nat_OSuc,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)) = c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)),
inference(paramod,[status(thm)],[c_1137,c_20064]) ).
cnf(c_1270,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)) = hAPP(c_Nat_OSuc,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),
inference(copy,[status(thm)],[c_20065]) ).
cnf(c_20066,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Onat_Onat__size(A)),c_Groups_Oone__class_Oone(tc_Nat_Onat)) = c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)),
inference(paramod,[status(thm)],[c_1132,c_753]) ).
cnf(c_20067,plain,
hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(A)) = c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)),
inference(paramod,[status(thm)],[c_1137,c_20066]) ).
cnf(c_1271,plain,
c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)) = hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(A)),
inference(copy,[status(thm)],[c_20067]) ).
cnf(c_1354,plain,
hAPP(c_Nat_OSuc,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)) = hAPP(c_Nat_OSuc,A),
inference(paramod,[status(thm)],[c_1270,c_756]) ).
cnf(c_1356,plain,
c_Nat_Onat_Onat__case(A,B,C,hAPP(c_Nat_OSuc,D)) = hAPP(C,c_Nat_Osize__class_Osize(tc_Nat_Onat,D)),
inference(paramod,[status(thm)],[c_1354,c_790]) ).
cnf(c_20068,plain,
c_Nat_Onat_Onat__size(hAPP(c_Nat_OSuc,A)) = hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,A))),
inference(paramod,[status(thm)],[c_1354,c_1271]) ).
cnf(c_20069,plain,
hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(A)) = hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,A))),
inference(paramod,[status(thm)],[c_1271,c_20068]) ).
cnf(c_1357,plain,
hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,A))) = hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(A)),
inference(copy,[status(thm)],[c_20069]) ).
cnf(c_1361,plain,
hAPP(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = hAPP(A,B),
inference(paramod,[status(thm)],[c_1356,c_790]) ).
cnf(c_1362,plain,
c_Nat_Onat_Onat__case(A,B,C,hAPP(c_Nat_OSuc,D)) = hAPP(C,D),
inference(paramod,[status(thm)],[c_1361,c_1356]) ).
cnf(c_1366,plain,
hAPP(c_COMBI(A),B) = c_Nat_Osize__class_Osize(tc_Nat_Onat,B),
inference(paramod,[status(thm)],[c_1361,c_824]) ).
cnf(c_1367,plain,
c_List_Olist_Olist__case(A,B,C,c_COMBI(D),c_List_Olist_OCons(B,E,F)) = hAPP(c_Nat_Osize__class_Osize(tc_Nat_Onat,E),F),
inference(paramod,[status(thm)],[c_1366,c_557]) ).
cnf(c_20070,plain,
c_Nat_Onat_Onat__case(A,B,C,hAPP(c_Nat_OSuc,c_Nat_Onat_Onat__size(D))) = hAPP(C,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,D))),
inference(paramod,[status(thm)],[c_1357,c_1362]) ).
cnf(c_20071,plain,
hAPP(C,c_Nat_Onat_Onat__size(D)) = hAPP(C,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,D))),
inference(paramod,[status(thm)],[c_1362,c_20070]) ).
cnf(c_1489,plain,
hAPP(A,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,B))) = hAPP(A,c_Nat_Onat_Onat__size(B)),
inference(copy,[status(thm)],[c_20071]) ).
cnf(c_20072,plain,
c_List_Olist_Olist__case(A,B,C,c_COMBI(D),c_List_Olist_OCons(B,E,F)) = hAPP(E,F),
inference(paramod,[status(thm)],[c_756,c_1367]) ).
cnf(c_1521,plain,
hAPP(c_Nat_Osize__class_Osize(tc_Nat_Onat,A),B) = hAPP(A,B),
inference(paramod,[status(thm)],[c_1367,c_20072]) ).
cnf(c_20073,plain,
hAPP(A,c_Nat_Onat_Onat__size(c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = hAPP(A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_758,c_1489]) ).
cnf(c_1594,plain,
hAPP(A,c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = hAPP(A,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_1489,c_20073]) ).
cnf(c_20074,plain,
hAPP(c_COMBI(A),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_1594,c_1366]) ).
cnf(c_20075,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_1366,c_20074]) ).
cnf(c_1608,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(copy,[status(thm)],[c_20075]) ).
cnf(c_1619,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_1608,c_756]) ).
cnf(c_20076,plain,
( hAPP(c_Hilbert__Choice_Oinv__into(A,A,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),c_COMBI(A)),C) = B
| hAPP(c_COMBI(A),B) != C ),
inference(resolve,[status(thm)],[c_878,c_523]) ).
cnf(c_2267,plain,
( hAPP(c_Hilbert__Choice_Oinv__into(C,C,c_Orderings_Otop__class_Otop(tc_fun(C,tc_HOL_Obool)),c_COMBI(C)),B) = A
| c_Nat_Osize__class_Osize(tc_Nat_Onat,A) != B ),
inference(paramod,[status(thm)],[c_1366,c_20076]) ).
cnf(c_20077,plain,
hAPP(c_Hilbert__Choice_Oinv__into(A,A,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),c_COMBI(A)),hAPP(c_COMBI(A),B)) = B,
inference(resolve,[status(thm)],[c_879,c_523]) ).
cnf(c_20078,plain,
hAPP(c_Hilbert__Choice_Oinv__into(A,A,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),c_COMBI(A)),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = B,
inference(paramod,[status(thm)],[c_1366,c_20077]) ).
cnf(c_2299,plain,
hAPP(c_Hilbert__Choice_Oinv__into(A,A,c_Orderings_Otop__class_Otop(tc_fun(A,tc_HOL_Obool)),c_COMBI(A)),B) = B,
inference(paramod,[status(thm)],[c_1361,c_20078]) ).
cnf(c_2300,plain,
( B = A
| c_Nat_Osize__class_Osize(tc_Nat_Onat,A) != B ),
inference(paramod,[status(thm)],[c_2299,c_2267]) ).
cnf(c_20079,plain,
( B != C
| hAPP(c_COMBI(A),B) = hAPP(c_COMBI(A),C) ),
inference(resolve,[status(thm)],[c_884,c_523]) ).
cnf(c_20080,plain,
( B != C
| c_Nat_Osize__class_Osize(tc_Nat_Onat,B) = hAPP(c_COMBI(A),C) ),
inference(paramod,[status(thm)],[c_1366,c_20079]) ).
cnf(c_2360,plain,
( A != B
| c_Nat_Osize__class_Osize(tc_Nat_Onat,A) = c_Nat_Osize__class_Osize(tc_Nat_Onat,B) ),
inference(paramod,[status(thm)],[c_1366,c_20080]) ).
cnf(c_20081,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_List_Olist_Olist__size(A,B,c_List_Olist_ONil(A))) = c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(resolve,[status(thm)],[c_2360,c_765]) ).
cnf(c_2368,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_List_Olist_Olist__size(A,B,c_List_Olist_ONil(A))) = c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(paramod,[status(thm)],[c_1619,c_20081]) ).
cnf(c_20082,plain,
c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) = c_List_Olist_Olist__size(A,B,c_List_Olist_ONil(A)),
inference(resolve,[status(thm)],[c_2368,c_2300]) ).
cnf(c_2401,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_ONil(A)) = c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(copy,[status(thm)],[c_20082]) ).
cnf(c_20083,plain,
A != hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)),
inference(resolve,[status(thm)],[c_1121,c_859]) ).
cnf(c_12820,plain,
hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),A),B)) != A,
inference(copy,[status(thm)],[c_20083]) ).
cnf(c_20084,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,c_List_Olist_ONil(A))) = hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(B,C)),c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),
inference(paramod,[status(thm)],[c_2401,c_1225]) ).
cnf(c_20085,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,c_List_Olist_ONil(A))) = hAPP(c_Nat_OSuc,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(B,C)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(paramod,[status(thm)],[c_1594,c_20084]) ).
cnf(c_18267,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,c_List_Olist_ONil(A))) = hAPP(c_Nat_OSuc,hAPP(B,C)),
inference(paramod,[status(thm)],[c_1057,c_20085]) ).
cnf(c_18353,plain,
c_List_Olist_Olist__size(A,B,c_List_Olist_OCons(A,C,D)) != hAPP(B,C),
inference(paramod,[status(thm)],[c_1225,c_12820]) ).
cnf(c_18494,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,E,F),c_List_Olist_OCons(A,V6,V7)) != hAPP(hAPP(E,V6),hAPP(F,V6)),
inference(paramod,[status(thm)],[c_1194,c_18353]) ).
cnf(c_20086,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,c_COMBI(E),F),c_List_Olist_OCons(A,V6,V7)) != hAPP(c_Nat_Osize__class_Osize(tc_Nat_Onat,V6),hAPP(F,V6)),
inference(paramod,[status(thm)],[c_1366,c_18494]) ).
cnf(c_19090,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,c_COMBI(E),F),c_List_Olist_OCons(A,V6,V7)) != hAPP(V6,hAPP(F,V6)),
inference(paramod,[status(thm)],[c_1521,c_20086]) ).
cnf(c_20087,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,c_COMBI(E),c_COMBI(F)),c_List_Olist_OCons(A,V6,V7)) != hAPP(V6,c_Nat_Osize__class_Osize(tc_Nat_Onat,V6)),
inference(paramod,[status(thm)],[c_1366,c_19090]) ).
cnf(c_20015,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,c_COMBI(E),c_COMBI(F)),c_List_Olist_OCons(A,V6,V7)) != hAPP(V6,V6),
inference(paramod,[status(thm)],[c_1361,c_20087]) ).
cnf(c_20061,plain,
c_List_Olist_Olist__size(A,c_COMBS(B,C,D,c_COMBI(E),c_COMBI(F)),c_List_Olist_OCons(A,hAPP(c_COMBB(V6,V7,V8,V9),V10),V11)) != hAPP(V9,hAPP(V10,hAPP(c_COMBB(V6,V7,V8,V9),V10))),
inference(paramod,[status(thm)],[c_1192,c_20015]) ).
cnf(c_20062,plain,
$false,
inference(resolve,[status(thm)],[c_20061,c_18267]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT163+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.54 % Computer : n002.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.54 % CPULimit : 300
% 0.09/0.54 % WCLimit : 300
% 0.09/0.54 % DateTime : Sat Sep 26 06:37:23 UTC 2026
% 0.09/0.54 % CPUTime :
% 0.09/0.54 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.54 % Process 1037872 was started by sandbox on n002,
% 0.09/0.54 % Sat Sep 26 06:37:23 2026
% 0.09/0.54 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.66
% 0.14/0.66 % From the command line: assign(max_seconds, 300).
% 0.14/0.66
% 0.14/0.66 % SInE: 304 to sos, 228 to usable, of 532 axioms (tolerance 2.00, depth 0 fixpoint).
% 239.60/40.32
% 239.60/40.32 % given #500 (F,wt=42): 4557 -hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),f5(f5(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),f5(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,A))))). [para(4274(a,1),4308(a,1,1,2))].
% 239.60/40.32
% 239.60/40.32 % given #1000 (A,wt=246): 1046 hBOOL(hAPP(hAPP(c_member(A),B),C)) | hBOOL(hAPP(hAPP(c_member(A),B),D)) | c_Set_Oinsert(A,B,D) = c_Set_Oinsert(A,B,C) | D != C # tptp_name(fact_insert__ident) # sine_depth(3). [clausify(157)].
% 239.60/40.32
% 239.60/40.32 % given #1500 (T,wt=28): 15471 c_Set_Oinsert(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,B),C) = c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Set_Oinsert(A,B,C)). [para(756(a,1),15394(a,1,3))].
% 239.60/40.32
% 239.60/40.32 % SZS status Theorem for theBenchmark
% 239.60/40.32
% 239.60/40.32 % Proof 1 at 5.86 (+ 1.19) seconds.
% 239.60/40.32 % Length of proof is 70.
% 239.60/40.32 % Level of proof is 15.
% 239.60/40.32 % Maximum clause weight is 150.000.
% 239.60/40.32 % Given clauses 1999.
% 239.60/40.32
% 239.60/40.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------