%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SCT131+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 : n019.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:32 AM UTC 2026
% Result : Theorem 109.73s 21.92s
% Output : CNFRefutation 109.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 18 ( 11 unt; 0 def)
% Number of atoms : 50 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 52 ( 20 ~; 20 |; 9 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-1 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-4 aty)
% Number of variables : 38 ( 1 sgn 24 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact__096_B_Bi_O_Ab_A_060_092_060_094bsub_062Q_Ai_092_060_094esub_062_Ab_H_096,axiom,
! [V_i_2] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_Q____,V_i_2))),
file('theBenchmark.p',fact__096_B_Bi_O_Ab_A_060_092_060_094bsub_062Q_Ai_092_060_094esub_062_Ab_H_096) ).
fof(fact_unanimity__def,axiom,
! [V_Fa_2] :
( c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2)
<=> ! [B_x] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf))
=> ! [B_a,B_b] :
( ! [B_i] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i)))
=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x))) ) ) ),
file('theBenchmark.p',fact_unanimity__def) ).
fof(conj_0,conjecture,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(fact_u,axiom,
c_Arrow__Order__Mirabelle_Ounanimity(v_F),
file('theBenchmark.p',fact_u) ).
cnf(c_502,plain,
c_Arrow__Order__Mirabelle_Ounanimity(v_F),
inference(clausify,[status(thm)],[fact_u]) ).
fof(nnf_228,plain,
! [V_Fa_2] :
( ( ? [B_x] :
( ? [B_a,B_b] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(V_Fa_2,B_x)))
& ! [B_i] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B_a),B_b)),hAPP(B_x,B_i))) )
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B_x),c_Arrow__Order__Mirabelle_OProf)) )
| c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2) )
& ( ! [X0] :
( ! [X1,X2] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),hAPP(V_Fa_2,X0)))
| ? [X3] : ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),hAPP(X0,X3))) )
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf)) )
| ~ c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2) ) ),
inference(fof_nnf,[status(thm)],[fact_unanimity__def]) ).
fof(sk_fact_unanimity__def_sk,plain,
! [V_Fa_2] :
( ( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK2(V_Fa_2)),sK3(V_Fa_2))),hAPP(V_Fa_2,sK1(V_Fa_2))))
& ! [B_i] : hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK2(V_Fa_2)),sK3(V_Fa_2))),hAPP(sK1(V_Fa_2),B_i)))
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK1(V_Fa_2)),c_Arrow__Order__Mirabelle_OProf)) )
| c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2) )
& ( ! [X0] :
( ! [X1,X2] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),hAPP(V_Fa_2,X0)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),hAPP(X0,sK0(V_Fa_2,X0,X1,X2)))) )
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf)) )
| ~ c_Arrow__Order__Mirabelle_Ounanimity(V_Fa_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X3,sK0(V_Fa_2,X0,X1,X2)),skolemize(B_x,sK1(V_Fa_2)),skolemize(B_a,sK2(V_Fa_2)),skolemize(B_b,sK3(V_Fa_2))],[nnf_228]) ).
fof(sk_fact_unanimity__def,plain,
( ! [VAR_0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK2(VAR_0)),sK3(VAR_0))),hAPP(VAR_0,sK1(VAR_0))))
| c_Arrow__Order__Mirabelle_Ounanimity(VAR_0) )
& ! [VAR_0,VAR_1] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK2(VAR_0)),sK3(VAR_0))),hAPP(sK1(VAR_0),VAR_1)))
| c_Arrow__Order__Mirabelle_Ounanimity(VAR_0) )
& ! [VAR_0] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK1(VAR_0)),c_Arrow__Order__Mirabelle_OProf))
| c_Arrow__Order__Mirabelle_Ounanimity(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),VAR_2),VAR_3)),hAPP(VAR_0,VAR_1)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),VAR_2),VAR_3)),hAPP(VAR_1,sK0(VAR_0,VAR_1,VAR_2,VAR_3))))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),VAR_1),c_Arrow__Order__Mirabelle_OProf))
| ~ c_Arrow__Order__Mirabelle_Ounanimity(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_unanimity__def_sk]) ).
cnf(c_575,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),C),D)),hAPP(A,B)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),C),D)),hAPP(B,sK0(A,B,C,D))))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),B),c_Arrow__Order__Mirabelle_OProf))
| ~ c_Arrow__Order__Mirabelle_Ounanimity(A) ),
inference(split_conjunct,[status(thm)],[sk_fact_unanimity__def]) ).
cnf(c_1020,plain,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_Q____,A))),
inference(clausify,[status(thm)],[fact__096_B_Bi_O_Ab_A_060_092_060_094bsub_062Q_Ai_092_060_094esub_062_Ab_H_096]) ).
fof(fact__096Q_A_058_AProf_096,axiom,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
file('theBenchmark.p',fact__096Q_A_058_AProf_096) ).
cnf(c_1042,plain,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
inference(clausify,[status(thm)],[fact__096Q_A_058_AProf_096]) ).
cnf(c_1318,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_6213,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B),C)),hAPP(v_F,A)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),B),C)),hAPP(A,sK0(v_F,A,B,C))))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),A),c_Arrow__Order__Mirabelle_OProf)) ),
inference(resolve,[status(thm)],[c_575,c_502]) ).
cnf(c_6214,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),A),B)),hAPP(v_F,v_Q____)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),A),B)),hAPP(v_Q____,sK0(v_F,v_Q____,A,B)))) ),
inference(resolve,[status(thm)],[c_6213,c_1042]) ).
cnf(c_6215,plain,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_b_H____)),hAPP(v_F,v_Q____))),
inference(resolve,[status(thm)],[c_6214,c_1020]) ).
cnf(c_6212,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1318,c_6215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT131+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.15/6.68 % Computer : n019.cluster.edu
% 0.15/6.68 % Model : x86_64 x86_64
% 0.15/6.68 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/6.68 % Memory : 8046.5625MB
% 0.15/6.68 % OS : Linux 6.8.0-71-generic
% 0.15/6.68 % CPULimit : 300
% 0.15/6.68 % WCLimit : 300
% 0.15/6.68 % DateTime : Sat Sep 26 06:31:27 UTC 2026
% 0.15/6.68 % CPUTime :
% 0.15/6.69 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/6.69 % Process 612726 was started by sandbox2 on n019,
% 0.15/6.69 % Sat Sep 26 06:31:27 2026
% 0.15/6.69 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/6.88
% 0.20/6.88 % From the command line: assign(max_seconds, 300).
% 0.20/6.88
% 0.20/6.88 % SInE: 219 to sos, 315 to usable, of 534 axioms (tolerance 2.00, depth 0 fixpoint).
% 109.73/21.92
% 109.73/21.92 % SZS status Theorem for theBenchmark
% 109.73/21.92
% 109.73/21.92 % Proof 1 at 5.92 (+ 0.75) seconds.
% 109.73/21.92 % Length of proof is 9.
% 109.73/21.92 % Level of proof is 2.
% 109.73/21.92 % Maximum clause weight is 37.000.
% 109.73/21.92 % Given clauses 63.
% 109.73/21.92
% 109.73/21.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------