%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT164+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 178.20s 29.41s
% Output : CNFRefutation 178.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 22 ( 16 unt; 0 def)
% Number of atoms : 28 ( 18 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 16 ( 10 ~; 5 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-5 aty)
% Number of variables : 68 ( 24 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_less__not__refl3,axiom,
! [V_t,V_s] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_s),V_t))
=> V_s != V_t ),
file('theBenchmark.p',fact_less__not__refl3) ).
fof(fact_nat__le__linear,axiom,
! [V_n,V_m] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n),V_m))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m),V_n)) ),
file('theBenchmark.p',fact_nat__le__linear) ).
fof(fact_plus__nat_Oadd__0,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('theBenchmark.p',fact_plus__nat_Oadd__0) ).
fof(fact_less__eq__Suc__le__raw,axiom,
! [V_na_2] : hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),V_na_2) = c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,V_na_2)),
file('theBenchmark.p',fact_less__eq__Suc__le__raw) ).
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) ).
cnf(c_968,plain,
( B != A
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),B)) ),
inference(clausify,[status(thm)],[fact_less__not__refl3]) ).
cnf(c_973,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B),A))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B)) ),
inference(clausify,[status(thm)],[fact_nat__le__linear]) ).
cnf(c_1026,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A) = A,
inference(clausify,[status(thm)],[fact_plus__nat_Oadd__0]) ).
cnf(c_1109,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)) = hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A),
inference(clausify,[status(thm)],[fact_less__eq__Suc__le__raw]) ).
cnf(c_1110,plain,
hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),A) = c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)),
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_1204,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_1206,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_1314,plain,
( B != A
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,A)),B)) ),
inference(paramod,[status(thm)],[c_1110,c_968]) ).
cnf(c_1534,plain,
( A != B
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),hAPP(c_Nat_OSuc,B))) ),
inference(resolve,[status(thm)],[c_973,c_1314]) ).
cnf(c_1660,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),hAPP(c_Nat_OSuc,A))),
inference(xxres,[status(thm)],[c_1534]) ).
cnf(c_1665,plain,
hAPP(c_Nat_OSuc,hAPP(c_Nat_OSuc,A)) != A,
inference(resolve,[status(thm)],[c_1660,c_1314]) ).
cnf(c_15883,plain,
hAPP(hAPP(c_COMBB(A,B,C,c_Nat_OSuc),c_Nat_OSuc),D) != D,
inference(paramod,[status(thm)],[c_1204,c_1665]) ).
cnf(c_16470,plain,
hAPP(hAPP(c_COMBB(A,B,C,hAPP(c_COMBB(D,E,F,c_Nat_OSuc),c_Nat_OSuc)),V6),V7) != hAPP(V6,V7),
inference(paramod,[status(thm)],[c_1204,c_15883]) ).
cnf(c_16675,plain,
hAPP(c_COMBS(A,B,C,D,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),E) = hAPP(hAPP(D,E),E),
inference(paramod,[status(thm)],[c_1026,c_1206]) ).
cnf(c_16677,plain,
hAPP(V6,V7) != hAPP(hAPP(c_COMBB(A,B,C,hAPP(c_COMBB(D,E,F,c_Nat_OSuc),c_Nat_OSuc)),V6),V7),
inference(copy,[status(thm)],[c_16470]) ).
cnf(c_16676,plain,
$false,
inference(resolve,[status(thm)],[c_16675,c_16677]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT164+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n020.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 06:35:54 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 871339 was started by sandbox2 on n020,
% 0.10/5.39 % Sat Sep 26 06:35:54 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/5.54
% 0.16/5.54 % From the command line: assign(max_seconds, 300).
% 0.16/5.54
% 0.16/5.54 % SInE: 330 to sos, 202 to usable, of 532 axioms (tolerance 2.00, depth 0 fixpoint).
% 178.20/29.41
% 178.20/29.41 % given #500 (F,wt=39): 1440 hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat))),A) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat). [resolve(1434,a,677,e(flip)),unit_del(a,756),unit_del(b,1024),unit_del(c,1024)].
% 178.20/29.41
% 178.20/29.41 % given #1000 (W,wt=30): 9803 c_Nat_Onat_Onat__size(c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Nat_Onat_Onat__size(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)). [resolve(9795,a,6389,a),flip(a)].
% 178.20/29.41
% 178.20/29.41 % SZS status Theorem for theBenchmark
% 178.20/29.41
% 178.20/29.41 % Proof 1 at 6.70 (+ 0.62) seconds.
% 178.20/29.41 % Length of proof is 21.
% 178.20/29.41 % Level of proof is 9.
% 178.20/29.41 % Maximum clause weight is 225.000.
% 178.20/29.41 % Given clauses 1210.
% 178.20/29.41
% 178.20/29.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------