%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWW478+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /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 09:12:05 AM UTC 2026
% Result : Theorem 40.43s 13.43s
% Output : CNFRefutation 40.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 2
% Syntax : Number of formulae : 6 ( 6 unt; 0 def)
% Number of atoms : 6 ( 0 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 2 ( 1 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-4 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_1_InitBlockRed_I1_J,axiom,
hBOOL(hAPP(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool,hAPP('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),fun(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool),member('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),fun('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),'product$uPair'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),ea),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),ha),hAPP(option(val),fun(list(char),option(val)),hAPP(list(char),fun(option(val),fun(list(char),option(val))),hAPP(fun(list(char),option(val)),fun(list(char),fun(option(val),fun(list(char),option(val)))),'fun$uupd'(list(char),option(val)),la),'v$u1'),hAPP(val,option(val),some(val),v))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'e$ua'),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'h$ua'),'l$ua')))),hAPP(list('product$uprod'(list(char),'product$uprod'(list(char),'product$uprod'(list('product$uprod'(list(char),ty)),list('product$uprod'(list(char),'product$uprod'(list(ty),'product$uprod'(ty,'product$uprod'(list(list(char)),exp(list(char))))))))))),fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),red,p))) ).
fof(conj_0,conjecture,
hBOOL(hAPP(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool,hAPP('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),fun(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool),member('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),fun('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),'product$uPair'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),ea),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),ha),hAPP(option(val),fun(list(char),option(val)),hAPP(list(char),fun(option(val),fun(list(char),option(val))),hAPP(fun(list(char),option(val)),fun(list(char),fun(option(val),fun(list(char),option(val)))),'fun$uupd'(list(char),option(val)),la),'v$u1'),hAPP(val,option(val),some(val),v))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'e$ua'),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'h$ua'),'l$ua')))),hAPP(list('product$uprod'(list(char),'product$uprod'(list(char),'product$uprod'(list('product$uprod'(list(char),ty)),list('product$uprod'(list(char),'product$uprod'(list(ty),'product$uprod'(ty,'product$uprod'(list(list(char)),exp(list(char))))))))))),fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),red,p))) ).
fof(negated_conjecture,negated_conjecture,
~ hBOOL(hAPP(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool,hAPP('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),fun(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool),member('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),fun('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),'product$uPair'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),ea),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),ha),hAPP(option(val),fun(list(char),option(val)),hAPP(list(char),fun(option(val),fun(list(char),option(val))),hAPP(fun(list(char),option(val)),fun(list(char),fun(option(val),fun(list(char),option(val)))),'fun$uupd'(list(char),option(val)),la),'v$u1'),hAPP(val,option(val),some(val),v))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'e$ua'),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'h$ua'),'l$ua')))),hAPP(list('product$uprod'(list(char),'product$uprod'(list(char),'product$uprod'(list('product$uprod'(list(char),ty)),list('product$uprod'(list(char),'product$uprod'(list(ty),'product$uprod'(ty,'product$uprod'(list(list(char)),exp(list(char))))))))))),fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),red,p))),
inference(negate_conjecture,[status(cth)],[conj_0]) ).
cnf(c149,plain,
hBOOL(hAPP(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool,hAPP('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),fun(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool),member('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),fun('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),'product$uPair'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),ea),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),ha),hAPP(option(val),fun(list(char),option(val)),hAPP(list(char),fun(option(val),fun(list(char),option(val))),hAPP(fun(list(char),option(val)),fun(list(char),fun(option(val),fun(list(char),option(val)))),'fun$uupd'(list(char),option(val)),la),'v$u1'),hAPP(val,option(val),some(val),v))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'e$ua'),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'h$ua'),'l$ua')))),hAPP(list('product$uprod'(list(char),'product$uprod'(list(char),'product$uprod'(list('product$uprod'(list(char),ty)),list('product$uprod'(list(char),'product$uprod'(list(ty),'product$uprod'(ty,'product$uprod'(list(list(char)),exp(list(char))))))))))),fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),red,p))),
inference(clausification,[status(esa)],[fact_1_InitBlockRed_I1_J]) ).
cnf(c1560,plain,
~ hBOOL(hAPP(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool,hAPP('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),fun(fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),bool),member('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),fun('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))))),'product$uPair'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),ea),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),ha),hAPP(option(val),fun(list(char),option(val)),hAPP(list(char),fun(option(val),fun(list(char),option(val))),hAPP(fun(list(char),option(val)),fun(list(char),fun(option(val),fun(list(char),option(val)))),'fun$uupd'(list(char),option(val)),la),'v$u1'),hAPP(val,option(val),some(val),v))))),hAPP('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),hAPP(exp(list(char)),fun('product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),'product$uPair'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'e$ua'),hAPP(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),hAPP(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(fun(list(char),option(val)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uPair'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))),'h$ua'),'l$ua')))),hAPP(list('product$uprod'(list(char),'product$uprod'(list(char),'product$uprod'(list('product$uprod'(list(char),ty)),list('product$uprod'(list(char),'product$uprod'(list(ty),'product$uprod'(ty,'product$uprod'(list(list(char)),exp(list(char))))))))))),fun('product$uprod'('product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val)))),'product$uprod'(exp(list(char)),'product$uprod'(fun(nat,option('product$uprod'(list(char),fun('product$uprod'(list(char),list(char)),option(val))))),fun(list(char),option(val))))),bool),red,p))),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
$false,
inference(resolution,[status(thm)],[c149,c1560]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW478+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 16:08:18 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.43/13.43 % SZS status Theorem for theBenchmark.p
% 40.43/13.43 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------