%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT146+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 : 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:33 AM UTC 2026
% Result : Theorem 227.18s 30.71s
% Output : CNFRefutation 227.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 3
% Syntax : Number of formulae : 10 ( 10 unt; 0 def)
% Number of atoms : 10 ( 9 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 0 con; 1-3 aty)
% Number of variables : 40 ( 18 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_not__Cons__self2,axiom,
! [V_xs,V_x,T_a] : hAPP(hAPP(c_List_Olist_OCons(T_a),V_x),V_xs) != V_xs,
file('theBenchmark.p',fact_not__Cons__self2) ).
fof(help_c__COMBS__1,axiom,
! [V_R_2,V_Q_2,V_Pa_2,T_a,T_c,T_b] : hAPP(hAPP(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(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_730,plain,
hAPP(c_COMBI(A),B) = B,
inference(clausify,[status(thm)],[help_c__COMBI__1]) ).
cnf(c_784,plain,
hAPP(hAPP(c_List_Olist_OCons(A),B),C) != C,
inference(clausify,[status(thm)],[fact_not__Cons__self2]) ).
cnf(c_1244,plain,
hAPP(hAPP(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_58899,plain,
hAPP(hAPP(hAPP(c_COMBS(A,B,C),D),c_COMBI(E)),F) = hAPP(hAPP(D,F),F),
inference(paramod,[status(thm)],[c_730,c_1244]) ).
cnf(c_59190,plain,
hAPP(hAPP(hAPP(c_COMBS(A,B,C),c_List_Olist_OCons(D)),E),F) != hAPP(E,F),
inference(paramod,[status(thm)],[c_1244,c_784]) ).
cnf(c_59192,plain,
hAPP(hAPP(D,F),F) = hAPP(hAPP(hAPP(c_COMBS(A,B,C),D),c_COMBI(E)),F),
inference(copy,[status(thm)],[c_58899]) ).
cnf(c_59191,plain,
$false,
inference(resolve,[status(thm)],[c_59190,c_59192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT146+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n020.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Sat Sep 26 06:33:33 UTC 2026
% 0.19/0.43 % CPUTime :
% 0.19/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.44 % Process 866775 was started by sandbox on n020,
% 0.19/0.44 % Sat Sep 26 06:33:33 2026
% 0.19/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.40/0.63
% 0.40/0.63 % From the command line: assign(max_seconds, 300).
% 0.40/0.63
% 0.40/0.63 % SInE: 385 to sos, 137 to usable, of 522 axioms (tolerance 2.00, depth 0 fixpoint).
% 227.18/30.71
% 227.18/30.71 % given #500 (F,wt=26): 4527 hAPP(hAPP(c_Product__Type_Ointernal__split(A,B,C),c_List_Olist_OCons(D)),hAPP(hAPP(c_Product__Type_Ointernal__split(E,F,V6),c_Product__Type_OPair(A,B)),hAPP(hAPP(c_Product__Type_OPair(E,F),V7),V8))) != V8. [para(578(a,2),4526(a,1,2))].
% 227.18/30.71
% 227.18/30.71 % given #1000 (W,wt=15): 3743 hBOOL(hAPP(hAPP(c_member(A),B),hAPP(c_fequal,c_List_Olist_Olist__case(C,D,B,E,c_List_Olist_ONil(D))))). [resolve(780,b,576,a)].
% 227.18/30.71
% 227.18/30.71 % given #1500 (F,wt=19): 17839 hAPP(c_COMBI(A),c_COMBI(B)) != hAPP(hAPP(c_List_Olist_OCons(C),D),c_List_Olist_Olist__case(E,F,c_COMBI(V6),V7,c_List_Olist_ONil(F))). [para(13704(a,2),17802(a,2,2))].
% 227.18/30.71
% 227.18/30.71 % given #2000 (T,wt=13): 21023 hBOOL(hAPP(hAPP(c_member(tc_prod(A,A)),v_P____),c_Transitive__Closure_Ortrancl(A,c_Transitive__Closure_Ortrancl(B,c_Arrow__Order__Mirabelle_OProf)))). [resolve(21012,a,922,a)].
% 227.18/30.71
% 227.18/30.71 % given #2500 (F,wt=25): 21471 c_List_Orotate1(A,hAPP(hAPP(c_Product__Type_Ointernal__split(B,C,D),c_List_Olist_OCons(A)),hAPP(hAPP(c_Product__Type_OPair(B,C),E),c_COMBI(F)))) != c_List_Osplice(V6,c_COMBI(V7),c_List_Olist_ONil(V6)). [para(578(a,2),21169(a,1,2))].
% 227.18/30.71
% 227.18/30.71 % given #3000 (T,wt=14): 20997 c_Transitive__Closure_Ortrancl(A,c_Arrow__Order__Mirabelle_OProf) != B | hBOOL(hAPP(hAPP(c_member(tc_prod(A,A)),v_P____),B)). [resolve(20929,a,743,c),flip(a)].
% 227.18/30.71
% 227.18/30.71 % given #3500 (F,wt=26): 31416 c_Nat_Osize__class_Osize(tc_List_Olist(A),c_COMBI(B)) != hAPP(hAPP(c_List_Olist_OCons(C),D),hAPP(hAPP(c_List_Olist_OCons(C),E),hAPP(hAPP(c_List_Oappend(C),F),c_Nat_Osize__class_Osize(tc_List_Olist(A),c_COMBI(V6))))). [para(846(a,1),31307(a,2,2))].
% 227.18/30.71
% 227.18/30.71 % given #4000 (T,wt=11): 38678 -hBOOL(A) | c_Predicate_ODomainP(B,C,hAPP(c_COMBI(D),c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)),A). [para(38640(a,1),14227(a,1))].
% 227.18/30.71
% 227.18/30.71 % given #4500 (A,wt=241): 1202 hBOOL(hAPP(hAPP(c_member(tc_prod(tc_List_Olist(A),tc_List_Olist(A))),hAPP(hAPP(c_Product__Type_OPair(tc_List_Olist(A),tc_List_Olist(A)),B),C)),c_List_Olistrel(A,D))) | c_Nat_Osize__class_Osize(tc_List_Olist(A),C) != c_Nat_Osize__class_Osize(tc_List_Olist(A),B) | c_Orderings_Oord__class_Oless(tc_Nat_Onat,f76(D,C,B,A),c_Nat_Osize__class_Osize(tc_List_Olist(A),B)) # tptp_name(fact_listrel__iff__nth) # sine_depth(3). [clausify(340)].
% 227.18/30.71
% 227.18/30.71 % SZS status Theorem for theBenchmark
% 227.18/30.71
% 227.18/30.71 % Proof 1 at 24.85 (+ 4.66) seconds.
% 227.18/30.71 % Length of proof is 9.
% 227.18/30.71 % Level of proof is 3.
% 227.18/30.71 % Maximum clause weight is 418.000.
% 227.18/30.71 % Given clauses 4874.
% 227.18/30.71
% 227.18/30.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------