%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT162+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 : n011.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 262.03s 40.17s
% Output : CNFRefutation 262.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 58 ( 44 unt; 0 def)
% Number of atoms : 78 ( 49 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 36 ( 16 ~; 13 |; 1 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-5 aty)
% Number of variables : 166 ( 48 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_list_Oinject,axiom,
! [V_list_H_2,V_a_H_2,V_list_2,V_aa_2,T_a] :
( c_List_Olist_OCons(T_a,V_aa_2,V_list_2) = c_List_Olist_OCons(T_a,V_a_H_2,V_list_H_2)
<=> ( V_list_2 = V_list_H_2
& V_aa_2 = V_a_H_2 ) ),
file('theBenchmark.p',fact_list_Oinject) ).
fof(fact_le__antisym,axiom,
! [V_n,V_m] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m),V_n))
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n),V_m))
=> V_m = V_n ) ),
file('theBenchmark.p',fact_le__antisym) ).
fof(fact_le__trans,axiom,
! [V_k,V_j,V_i] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i),V_j))
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_j),V_k))
=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_i),V_k)) ) ),
file('theBenchmark.p',fact_le__trans) ).
fof(fact_eq__imp__le,axiom,
! [V_n,V_m] :
( V_m = V_n
=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m),V_n)) ),
file('theBenchmark.p',fact_eq__imp__le) ).
fof(fact_Suc__n__not__n,axiom,
! [V_n] : hAPP(c_Nat_OSuc,V_n) != V_n,
file('theBenchmark.p',fact_Suc__n__not__n) ).
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_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__size,axiom,
! [V_n] : c_Nat_Osize__class_Osize(tc_Nat_Onat,V_n) = V_n,
file('theBenchmark.p',fact_nat__size) ).
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_548,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_747,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,A) = A,
inference(clausify,[status(thm)],[fact_nat__size]) ).
cnf(c_816,plain,
hAPP(c_COMBI(A),B) = B,
inference(clausify,[status(thm)],[help_c__COMBI__1]) ).
cnf(c_888,plain,
( C != E
| B != D
| c_List_Olist_OCons(A,B,C) = c_List_Olist_OCons(A,D,E) ),
inference(clausify,[status(thm)],[fact_list_Oinject]) ).
cnf(c_924,plain,
( A = B
| ~ 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_le__antisym]) ).
cnf(c_925,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),C))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B),C))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B)) ),
inference(clausify,[status(thm)],[fact_le__trans]) ).
cnf(c_927,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B))
| A != B ),
inference(clausify,[status(thm)],[fact_eq__imp__le]) ).
cnf(c_1092,plain,
hAPP(c_Nat_OSuc,A) != A,
inference(clausify,[status(thm)],[fact_Suc__n__not__n]) ).
cnf(c_1210,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_1212,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_1232,plain,
( B != C
| c_List_Olist_OCons(A,B,B) = c_List_Olist_OCons(A,C,C) ),
inference(factor,[status(thm)],[c_888]) ).
cnf(c_1398,plain,
c_List_Olist_OCons(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,B),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = c_List_Olist_OCons(A,B,B),
inference(resolve,[status(thm)],[c_1232,c_747]) ).
cnf(c_1406,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_COMBI(A),B)),B)),
inference(resolve,[status(thm)],[c_927,c_816]) ).
cnf(c_1412,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),A)),
inference(resolve,[status(thm)],[c_927,c_747]) ).
cnf(c_3915,plain,
B = hAPP(c_COMBI(A),B),
inference(copy,[status(thm)],[c_816]) ).
cnf(c_1420,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),hAPP(c_COMBI(B),A))),
inference(resolve,[status(thm)],[c_927,c_3915]) ).
cnf(c_3916,plain,
A = c_Nat_Osize__class_Osize(tc_Nat_Onat,A),
inference(copy,[status(thm)],[c_747]) ).
cnf(c_1423,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),c_Nat_Osize__class_Osize(tc_Nat_Onat,A))),
inference(resolve,[status(thm)],[c_927,c_3916]) ).
cnf(c_1555,plain,
c_List_Olist_Olist__case(A,B,C,D,c_List_Olist_OCons(B,E,E)) = hAPP(hAPP(D,c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),
inference(paramod,[status(thm)],[c_1398,c_548]) ).
cnf(c_1556,plain,
c_List_Olist_OCons(A,B,c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = c_List_Olist_OCons(A,B,B),
inference(paramod,[status(thm)],[c_747,c_1398]) ).
cnf(c_3917,plain,
c_List_Olist_Olist__case(A,B,C,D,c_List_Olist_OCons(B,E,E)) = hAPP(hAPP(D,E),c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),
inference(paramod,[status(thm)],[c_1556,c_548]) ).
cnf(c_1560,plain,
hAPP(hAPP(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,B)),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = hAPP(hAPP(A,B),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)),
inference(paramod,[status(thm)],[c_1555,c_3917]) ).
cnf(c_1563,plain,
c_List_Olist_Olist__case(A,B,C,D,c_List_Olist_OCons(B,E,E)) = hAPP(hAPP(D,E),c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),
inference(paramod,[status(thm)],[c_1560,c_1555]) ).
cnf(c_1780,plain,
hAPP(c_COMBS(A,B,C,c_COMBI(D),E),F) = hAPP(F,hAPP(E,F)),
inference(paramod,[status(thm)],[c_816,c_1212]) ).
cnf(c_1991,plain,
hAPP(hAPP(A,B),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = hAPP(hAPP(A,B),B),
inference(paramod,[status(thm)],[c_1563,c_548]) ).
cnf(c_3918,plain,
c_List_Olist_Olist__case(A,B,C,c_COMBI(D),c_List_Olist_OCons(B,E,E)) = hAPP(E,c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),
inference(paramod,[status(thm)],[c_816,c_1563]) ).
cnf(c_3919,plain,
hAPP(hAPP(c_COMBI(D),E),c_Nat_Osize__class_Osize(tc_Nat_Onat,E)) = hAPP(E,c_Nat_Osize__class_Osize(tc_Nat_Onat,E)),
inference(paramod,[status(thm)],[c_1563,c_3918]) ).
cnf(c_1992,plain,
hAPP(hAPP(c_COMBI(A),B),B) = hAPP(B,c_Nat_Osize__class_Osize(tc_Nat_Onat,B)),
inference(paramod,[status(thm)],[c_1991,c_3919]) ).
cnf(c_3920,plain,
hAPP(hAPP(c_COMBI(A),B),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = hAPP(B,B),
inference(paramod,[status(thm)],[c_816,c_1991]) ).
cnf(c_3921,plain,
hAPP(hAPP(c_COMBI(A),B),B) = hAPP(B,B),
inference(paramod,[status(thm)],[c_1991,c_3920]) ).
cnf(c_1999,plain,
hAPP(A,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)) = hAPP(A,A),
inference(paramod,[status(thm)],[c_1992,c_3921]) ).
cnf(c_2214,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)),B)) ),
inference(resolve,[status(thm)],[c_925,c_1423]) ).
cnf(c_2231,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B)) ),
inference(resolve,[status(thm)],[c_925,c_1423]) ).
cnf(c_2234,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),B))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B))) ),
inference(resolve,[status(thm)],[c_925,c_1412]) ).
cnf(c_2242,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)))),
inference(resolve,[status(thm)],[c_2231,c_1423]) ).
cnf(c_2247,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A))),A)),
inference(resolve,[status(thm)],[c_2234,c_1412]) ).
cnf(c_3922,plain,
( c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)) = A
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A))),A)) ),
inference(resolve,[status(thm)],[c_2242,c_924]) ).
cnf(c_2294,plain,
c_Nat_Osize__class_Osize(tc_Nat_Onat,c_Nat_Osize__class_Osize(tc_Nat_Onat,A)) = A,
inference(resolve,[status(thm)],[c_2247,c_3922]) ).
cnf(c_3023,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_COMBI(A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B))),B)),
inference(resolve,[status(thm)],[c_1406,c_2234]) ).
cnf(c_3165,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A),hAPP(c_COMBI(B),c_Nat_Osize__class_Osize(tc_Nat_Onat,A)))),
inference(resolve,[status(thm)],[c_2214,c_1420]) ).
cnf(c_3923,plain,
( hAPP(c_COMBI(A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = B
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_COMBI(A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B))),B)) ),
inference(resolve,[status(thm)],[c_3165,c_924]) ).
cnf(c_3172,plain,
hAPP(c_COMBI(A),c_Nat_Osize__class_Osize(tc_Nat_Onat,B)) = B,
inference(resolve,[status(thm)],[c_3023,c_3923]) ).
cnf(c_3183,plain,
hAPP(c_COMBI(A),B) = c_Nat_Osize__class_Osize(tc_Nat_Onat,B),
inference(paramod,[status(thm)],[c_2294,c_3172]) ).
cnf(c_3924,plain,
hAPP(c_COMBS(A,B,C,c_COMBI(D),c_COMBI(E)),F) = hAPP(F,c_Nat_Osize__class_Osize(tc_Nat_Onat,F)),
inference(paramod,[status(thm)],[c_3183,c_1780]) ).
cnf(c_3783,plain,
hAPP(c_COMBS(A,B,C,c_COMBI(D),c_COMBI(E)),F) = hAPP(F,F),
inference(paramod,[status(thm)],[c_1999,c_3924]) ).
cnf(c_3913,plain,
hAPP(c_COMBS(A,B,C,c_COMBI(D),c_COMBI(E)),hAPP(c_COMBB(F,V6,V7,V8),V9)) = hAPP(V8,hAPP(V9,hAPP(c_COMBB(F,V6,V7,V8),V9))),
inference(paramod,[status(thm)],[c_3783,c_1210]) ).
cnf(c_3925,plain,
A != hAPP(c_Nat_OSuc,A),
inference(copy,[status(thm)],[c_1092]) ).
cnf(c_3914,plain,
$false,
inference(resolve,[status(thm)],[c_3913,c_3925]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT162+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n011.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.45 % DateTime : Sat Sep 26 06:34:49 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.17/5.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.45 % Process 3994780 was started by sandbox on n011,
% 0.17/5.45 % Sat Sep 26 06:34:49 2026
% 0.17/5.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.21/5.63
% 0.21/5.63 % From the command line: assign(max_seconds, 300).
% 0.21/5.63
% 0.21/5.63 % SInE: 306 to sos, 225 to usable, of 531 axioms (tolerance 2.00, depth 0 fixpoint).
% 262.03/40.17
% 262.03/40.17 % given #500 (W,wt=35): 1780 hAPP(c_COMBS(A,B,C,c_COMBI(D),E),F) = hAPP(F,hAPP(E,F)). [para(816(a,1),1212(a,2,1))].
% 262.03/40.17
% 262.03/40.17 % SZS status Theorem for theBenchmark
% 262.03/40.17
% 262.03/40.17 % Proof 1 at 1.59 (+ 0.30) seconds.
% 262.03/40.17 % Length of proof is 47.
% 262.03/40.17 % Level of proof is 12.
% 262.03/40.17 % Maximum clause weight is 215.000.
% 262.03/40.17 % Given clauses 506.
% 262.03/40.17
% 262.03/40.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------