%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SCT171+7 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 22:11:14 EDT 2022
% Result : Theorem 3.55s 3.79s
% Output : Refutation 3.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 4
% Syntax : Number of clauses : 7 ( 6 unt; 0 nHn; 6 RR)
% Number of literals : 8 ( 1 equ; 3 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 19 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 14 con; 0-4 aty)
% Number of variables : 6 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(135,axiom,
hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto) ).
cnf(136,axiom,
( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
| ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_PW) ).
cnf(137,plain,
hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))),
inference('REWRITE',[status(thm)],[136,135]) ).
cnf(1426,axiom,
hAPP(X,Y,hAPP(Z,fun(X,Y),hAPP(fun(X,fun(Z,Y)),fun(Z,fun(X,Y)),combc(X,Z,Y),U),V),W) = hAPP(Z,Y,hAPP(X,fun(Z,Y),U,W),V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).
cnf(1440,negated_conjecture,
~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
cnf(1441,plain,
~ hBOOL(hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool,hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool)),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),combc(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d))),
inference('REWRITE',[status(thm)],[1440,1426,theory(equality)]) ).
cnf(1601,plain,
$false,
inference('REWRITE',[status(thm)],[137,1441,1426,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SCT171+7 : TPTP v8.1.0. Released v5.3.0.
% 0.07/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jul 2 06:30:38 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.46 *
% 0.18/0.46 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-02T06:30:38
% 0.18/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n003.cluster.edu at 2022-07-02T06:30:38
% 0.89/1.07 WARNING:
% 0.89/1.07 |ab_sem1668676832m_mult| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linord1117847801e_zero| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linord1278240602ring_1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |ordered_ring| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linord581940658strict| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linordered_ring| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |ring_n68954251visors| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linord626643107strict| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |ring_char_0| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linordered_field| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linord219039673up_add| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |linordered_idom| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |dense_linorder| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 0.89/1.07 WARNING:
% 0.89/1.07 |ring_1| is a 1-ary relation that occurs only negatively; disabling rows that contain it.
% 3.55/3.79
% 3.55/3.79
% 3.55/3.79 #||
% 3.55/3.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.55/3.79 % SZS output start Refutation
% See solution above
% 3.65/3.85 ||#
% 3.65/3.85
% 3.65/3.85 ; Summary of computation:
% 3.65/3.85 ; 2138 formulas have been input or derived (from 1 formulas).
% 3.65/3.85 ; 1601 (75%) were retained. Of these,
% 3.65/3.85 ; 422 (26%) were simplified or subsumed later,
% 3.65/3.85 ; 1179 (74%) are still being kept.
% 3.65/3.85 ;
% 3.65/3.85 ; Run time in seconds excluding printing time:
% 3.65/3.85 ; 0.543 16% Read assertion file (1 call)
% 3.65/3.85 ; 0.047 1% Assert (1,173 calls)
% 3.65/3.85 ; 0.474 14% Process new row (1,882 calls)
% 3.65/3.85 ; 0.048 1% Condensing (1,418 calls)
% 3.65/3.85 ; 0.328 10% Forward subsumption (1,418 calls)
% 3.65/3.85 ; 0.130 4% Backward subsumption (1,181 calls)
% 3.65/3.85 ; 0.009 0% Clause clause subsumption (1,514 calls)
% 3.65/3.85 ; 0.202 6% Forward simplification (1,760 calls)
% 3.65/3.85 ; 0.189 6% Backward simplification (1,480 calls)
% 3.65/3.85 ; 1.335 40% Ordering (11,171 calls)
% 3.65/3.85 ; 0.000 0% Sortal reasoning (32 calls)
% 3.65/3.85 ; 0.003 0% Purity testing (1 call)
% 3.65/3.85 ; 0.021 1% Other
% 3.65/3.85 ; 3.329 Total
% 3.65/3.85 ; 3.389 Real time
% 3.65/3.85 ;
% 3.65/3.85 ; Term-hash-array has 5,808 terms in all.
% 3.65/3.85 ; Feature-vector-row-index has 909 entries (909 at peak, 1,181 added, 272 deleted).
% 3.65/3.85 ; Feature-vector-row-index has 16,594 nodes (16,594 at peak, 23,156 added, 6,562 deleted).
% 3.65/3.85 ; Retrieved 1,560 possibly forward subsuming rows in 1,418 calls.
% 3.65/3.85 ; Retrieved 447 possibly backward subsumed rows in 1,181 calls.
% 3.65/3.85 ; Path-index has 4,721 entries (4,721 at peak, 6,280 added, 1,559 deleted).
% 3.65/3.85 ; Path-index has 51,536 nodes (51,536 at peak, 60,640 added, 9,104 deleted).
% 3.65/3.85 ; Trie-index has 4,721 entries (4,721 at peak, 6,280 added, 1,559 deleted).
% 3.65/3.85 ; Trie-index has 70,186 nodes (70,186 at peak, 106,893 added, 36,707 deleted).
% 3.65/3.85 ; Retrieved 9,173 generalization terms in 18,358 calls.
% 3.65/3.85 ; Retrieved 3,614 instance terms in 355 calls.
% 3.65/3.85 ;
% 3.65/3.85 ; The agenda of backward simplifiable rows to process has 134 entries:
% 3.65/3.85 ; 134 with value 0
% 3.65/3.85 ; The agenda of input rows to give has 1178 entries:
% 3.65/3.85 ; 51 with value 3 10 with value 72 6 with value 147
% 3.65/3.85 ; 2 with value 4 3 with value 73 4 with value 148
% 3.65/3.85 ; 8 with value 7 4 with value 74 2 with value 150
% 3.65/3.85 ; 1 with value 8 4 with value 75 1 with value 151
% 3.65/3.85 ; 13 with value 9 8 with value 76 2 with value 152
% 3.65/3.85 ; 10 with value 10 2 with value 77 2 with value 155
% 3.65/3.85 ; 3 with value 11 22 with value 78 3 with value 156
% 3.65/3.85 ; 8 with value 12 15 with value 79 1 with value 157
% 3.65/3.85 ; 9 with value 13 10 with value 80 1 with value 158
% 3.65/3.85 ; 1 with value 14 7 with value 81 1 with value 159
% 3.65/3.85 ; 4 with value 15 1 with value 82 1 with value 160
% 3.65/3.85 ; 6 with value 16 4 with value 83 2 with value 164
% 3.65/3.85 ; 10 with value 17 8 with value 84 1 with value 166
% 3.65/3.85 ; 20 with value 18 15 with value 85 1 with value 167
% 3.65/3.85 ; 11 with value 19 8 with value 86 3 with value 168
% 3.65/3.85 ; 11 with value 20 6 with value 87 3 with value 169
% 3.65/3.85 ; 10 with value 21 11 with value 88 2 with value 172
% 3.65/3.85 ; 10 with value 22 1 with value 89 1 with value 177
% 3.65/3.85 ; 16 with value 23 7 with value 90 3 with value 178
% 3.65/3.85 ; 27 with value 24 4 with value 91 1 with value 183
% 3.65/3.85 ; 10 with value 25 2 with value 92 1 with value 187
% 3.65/3.85 ; 13 with value 26 4 with value 93 2 with value 190
% 3.65/3.85 ; 4 with value 27 4 with value 94 1 with value 191
% 3.65/3.85 ; 8 with value 28 11 with value 95 1 with value 193
% 3.65/3.85 ; 18 with value 29 6 with value 96 1 with value 194
% 3.65/3.85 ; 11 with value 30 2 with value 97 2 with value 195
% 3.65/3.85 ; 6 with value 31 7 with value 98 1 with value 198
% 3.65/3.85 ; 15 with value 32 5 with value 99 6 with value 199
% 3.65/3.85 ; 11 with value 33 6 with value 100 1 with value 205
% 3.65/3.85 ; 2 with value 34 6 with value 101 10 with value 208
% 3.65/3.85 ; 12 with value 35 5 with value 102 2 with value 209
% 3.65/3.85 ; 7 with value 36 2 with value 103 1 with value 210
% 3.65/3.85 ; 18 with value 37 5 with value 105 2 with value 212
% 3.65/3.85 ; 21 with value 38 6 with value 106 2 with value 217
% 3.65/3.85 ; 8 with value 39 2 with value 108 1 with value 221
% 3.65/3.85 ; 15 with value 40 4 with value 109 1 with value 222
% 3.65/3.85 ; 13 with value 41 4 with value 110 1 with value 224
% 3.65/3.85 ; 11 with value 42 3 with value 111 2 with value 235
% 3.65/3.85 ; 10 with value 43 7 with value 112 2 with value 237
% 3.65/3.85 ; 10 with value 44 9 with value 114 1 with value 244
% 3.65/3.85 ; 8 with value 45 14 with value 115 1 with value 246
% 3.65/3.85 ; 15 with value 46 2 with value 116 9 with value 247
% 3.65/3.85 ; 9 with value 47 1 with value 117 1 with value 268
% 3.65/3.85 ; 12 with value 48 3 with value 118 1 with value 269
% 3.65/3.85 ; 15 with value 49 2 with value 119 1 with value 271
% 3.65/3.85 ; 15 with value 50 1 with value 120 1 with value 272
% 3.65/3.85 ; 5 with value 51 1 with value 121 1 with value 276
% 3.65/3.85 ; 9 with value 52 2 with value 122 1 with value 283
% 3.65/3.85 ; 7 with value 53 5 with value 123 3 with value 286
% 3.65/3.85 ; 15 with value 54 4 with value 124 1 with value 290
% 3.65/3.85 ; 13 with value 55 4 with value 125 2 with value 295
% 3.65/3.85 ; 11 with value 56 5 with value 126 1 with value 300
% 3.65/3.85 ; 4 with value 57 2 with value 127 1 with value 304
% 3.65/3.85 ; 20 with value 58 2 with value 128 1 with value 309
% 3.65/3.85 ; 10 with value 59 3 with value 129 1 with value 316
% 3.65/3.85 ; 6 with value 60 5 with value 131 1 with value 338
% 3.65/3.85 ; 19 with value 61 2 with value 132 1 with value 356
% 3.65/3.85 ; 3 with value 62 1 with value 133 1 with value 362
% 3.65/3.85 ; 3 with value 63 2 with value 135 1 with value 364
% 3.65/3.85 ; 3 with value 64 6 with value 136 1 with value 396
% 3.65/3.85 ; 3 with value 65 2 with value 138 1 with value 403
% 3.65/3.85 ; 13 with value 66 2 with value 139 1 with value 452
% 3.65/3.85 ; 14 with value 67 2 with value 141 1 with value 487
% 3.65/3.85 ; 6 with value 68 3 with value 142 1 with value 710
% 3.65/3.85 ; 8 with value 69 4 with value 144 4 with value 912
% 3.65/3.85 ; 6 with value 70 5 with value 145 1 with value 1403
% 3.65/3.85 ; 7 with value 71 7 with value 146 1 with value 1431
% 3.65/3.85 Evaluation took:
% 3.65/3.85 3.391 seconds of real time
% 3.65/3.85 3.288677 seconds of user run time
% 3.65/3.85 0.102811 seconds of system run time
% 3.65/3.85 [Run times include 0.372 seconds GC run time.]
% 3.65/3.85 0 calls to %EVAL
% 3.65/3.85 0 page faults and
% 3.65/3.85 242,041,640 bytes consed.
% 3.65/3.85 :PROOF-FOUND
% 3.65/3.85 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-07-02T06:30:42
% 3.65/3.85 :PROOF-FOUND
% 3.65/3.85 *
%------------------------------------------------------------------------------