%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWW478_2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:10:28 AM UTC 2026
% Result : Theorem 170.29s 86.35s
% Output : Refutation 170.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of formulae : 33 ( 17 unt; 0 typ; 1 def)
% Number of atoms : 70 ( 37 equ; 0 cnn)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 358 ( 20 ~; 23 |; 4 &; 306 @)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Number of types : 437 ( 436 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 33 ( 30 usr; 18 con; 0-3 aty)
% Number of variables : 22 ( 1 ^; 15 !; 5 ?; 22 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(bop_type,type,
bop: $tType ).
thf(exp_list_char_type,type,
exp_list_char: $tType ).
thf(bool_type,type,
bool: $tType ).
thf(list_char_type,type,
list_char: $tType ).
thf(list_P1999446415t_char_type,type,
list_P1999446415t_char: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(option_ty_type,type,
option_ty: $tType ).
thf(option_val_type,type,
option_val: $tType ).
thf(option466449911r_bool_type,type,
option466449911r_bool: $tType ).
thf(option1479284511on_val_type,type,
option1479284511on_val: $tType ).
thf(ty_type,type,
ty: $tType ).
thf(val_type,type,
val: $tType ).
thf(fun_bo1454185032l_bool_type,type,
fun_bo1454185032l_bool: $tType ).
thf(fun_bo1422795267r_bool_type,type,
fun_bo1422795267r_bool: $tType ).
thf(fun_bo1211200491t_bool_type,type,
fun_bo1211200491t_bool: $tType ).
thf(fun_bo1226433611l_bool_type,type,
fun_bo1226433611l_bool: $tType ).
thf(fun_bo1845219066l_bool_type,type,
fun_bo1845219066l_bool: $tType ).
thf(fun_bo2065098379l_bool_type,type,
fun_bo2065098379l_bool: $tType ).
thf(fun_bo1673925482l_bool_type,type,
fun_bo1673925482l_bool: $tType ).
thf(fun_bo1337967738l_bool_type,type,
fun_bo1337967738l_bool: $tType ).
thf(fun_bo1153317747al_val_type,type,
fun_bo1153317747al_val: $tType ).
thf(fun_bo180791194on_val_type,type,
fun_bo180791194on_val: $tType ).
thf(fun_ex1201926843l_bool_type,type,
fun_ex1201926843l_bool: $tType ).
thf(fun_ex2119256656r_bool_type,type,
fun_ex2119256656r_bool: $tType ).
thf(fun_ex389763294t_bool_type,type,
fun_ex389763294t_bool: $tType ).
thf(fun_ex1944467352l_bool_type,type,
fun_ex1944467352l_bool: $tType ).
thf(fun_ex1732109805l_bool_type,type,
fun_ex1732109805l_bool: $tType ).
thf(fun_ex17205502l_bool_type,type,
fun_ex17205502l_bool: $tType ).
thf(fun_ex1270309303l_bool_type,type,
fun_ex1270309303l_bool: $tType ).
thf(fun_ex1123147373l_bool_type,type,
fun_ex1123147373l_bool: $tType ).
thf(fun_ex977868519on_val_type,type,
fun_ex977868519on_val: $tType ).
thf(fun_ex1005552999on_val_type,type,
fun_ex1005552999on_val: $tType ).
thf(fun_bool_bool_type,type,
fun_bool_bool: $tType ).
thf(fun_bo1549164019l_bool_type,type,
fun_bo1549164019l_bool: $tType ).
thf(fun_list_char_bool_type,type,
fun_list_char_bool: $tType ).
thf(fun_li688206603ion_ty_type,type,
fun_li688206603ion_ty: $tType ).
thf(fun_li1432931796on_val_type,type,
fun_li1432931796on_val: $tType ).
thf(fun_li1107892380r_bool_type,type,
fun_li1107892380r_bool: $tType ).
thf(fun_li1309482948on_val_type,type,
fun_li1309482948on_val: $tType ).
thf(fun_li860735411r_bool_type,type,
fun_li860735411r_bool: $tType ).
thf(fun_li1918653272r_bool_type,type,
fun_li1918653272r_bool: $tType ).
thf(fun_li683301334t_bool_type,type,
fun_li683301334t_bool: $tType ).
thf(fun_li1452996768l_bool_type,type,
fun_li1452996768l_bool: $tType ).
thf(fun_li1084227301l_bool_type,type,
fun_li1084227301l_bool: $tType ).
thf(fun_li507112950l_bool_type,type,
fun_li507112950l_bool: $tType ).
thf(fun_li1782471359l_bool_type,type,
fun_li1782471359l_bool: $tType ).
thf(fun_li610758501l_bool_type,type,
fun_li610758501l_bool: $tType ).
thf(fun_li835958565t_char_type,type,
fun_li835958565t_char: $tType ).
thf(fun_li916220527on_val_type,type,
fun_li916220527on_val: $tType ).
thf(fun_li378593189t_bool_type,type,
fun_li378593189t_bool: $tType ).
thf(fun_li823162622l_bool_type,type,
fun_li823162622l_bool: $tType ).
thf(fun_li1701804749r_bool_type,type,
fun_li1701804749r_bool: $tType ).
thf(fun_li649007521t_bool_type,type,
fun_li649007521t_bool: $tType ).
thf(fun_li2040914709l_bool_type,type,
fun_li2040914709l_bool: $tType ).
thf(fun_li673202352l_bool_type,type,
fun_li673202352l_bool: $tType ).
thf(fun_li1596536641l_bool_type,type,
fun_li1596536641l_bool: $tType ).
thf(fun_li1577539636l_bool_type,type,
fun_li1577539636l_bool: $tType ).
thf(fun_li1569131568l_bool_type,type,
fun_li1569131568l_bool: $tType ).
thf(fun_li1436431093on_val_type,type,
fun_li1436431093on_val: $tType ).
thf(fun_li1382912868on_val_type,type,
fun_li1382912868on_val: $tType ).
thf(fun_li2076121851l_bool_type,type,
fun_li2076121851l_bool: $tType ).
thf(fun_li923379764l_bool_type,type,
fun_li923379764l_bool: $tType ).
thf(fun_li1428515013l_bool_type,type,
fun_li1428515013l_bool: $tType ).
thf(fun_li616154692r_bool_type,type,
fun_li616154692r_bool: $tType ).
thf(fun_li537151130l_bool_type,type,
fun_li537151130l_bool: $tType ).
thf(fun_li415052468l_bool_type,type,
fun_li415052468l_bool: $tType ).
thf(fun_li1857149300t_char_type,type,
fun_li1857149300t_char: $tType ).
thf(fun_li1793507146on_val_type,type,
fun_li1793507146on_val: $tType ).
thf(fun_li318226104r_bool_type,type,
fun_li318226104r_bool: $tType ).
thf(fun_nat_bool_type,type,
fun_nat_bool: $tType ).
thf(fun_nat_option_ty_type,type,
fun_nat_option_ty: $tType ).
thf(fun_nat_option_val_type,type,
fun_nat_option_val: $tType ).
thf(fun_na402763290r_bool_type,type,
fun_na402763290r_bool: $tType ).
thf(fun_na939144002on_val_type,type,
fun_na939144002on_val: $tType ).
thf(fun_ty_option_ty_type,type,
fun_ty_option_ty: $tType ).
thf(fun_val_bool_type,type,
fun_val_bool: $tType ).
thf(fun_val_option_val_type,type,
fun_val_option_val: $tType ).
thf(fun_va151260549r_bool_type,type,
fun_va151260549r_bool: $tType ).
thf(fun_val_fun_nat_bool_type,type,
fun_val_fun_nat_bool: $tType ).
thf(fun_val_fun_val_bool_type,type,
fun_val_fun_val_bool: $tType ).
thf(fun_va1711094920r_bool_type,type,
fun_va1711094920r_bool: $tType ).
thf(fun_va17865894t_bool_type,type,
fun_va17865894t_bool: $tType ).
thf(fun_va2047554000l_bool_type,type,
fun_va2047554000l_bool: $tType ).
thf(fun_va2114888117l_bool_type,type,
fun_va2114888117l_bool: $tType ).
thf(fun_va1468324038l_bool_type,type,
fun_va1468324038l_bool: $tType ).
thf(fun_va547415023l_bool_type,type,
fun_va547415023l_bool: $tType ).
thf(fun_va189260341l_bool_type,type,
fun_va189260341l_bool: $tType ).
thf(fun_va959426509al_val_type,type,
fun_va959426509al_val: $tType ).
thf(fun_va2094201759on_val_type,type,
fun_va2094201759on_val: $tType ).
thf(fun_va679853773l_bool_type,type,
fun_va679853773l_bool: $tType ).
thf(fun_va267341538l_bool_type,type,
fun_va267341538l_bool: $tType ).
thf(fun_va830487155l_bool_type,type,
fun_va830487155l_bool: $tType ).
thf(fun_va621701228l_bool_type,type,
fun_va621701228l_bool: $tType ).
thf(fun_va934618978l_bool_type,type,
fun_va934618978l_bool: $tType ).
thf(fun_va1923334394al_val_type,type,
fun_va1923334394al_val: $tType ).
thf(fun_va1157788700on_val_type,type,
fun_va1157788700on_val: $tType ).
thf(fun_fu1638830325l_bool_type,type,
fun_fu1638830325l_bool: $tType ).
thf(fun_fu1534370419l_bool_type,type,
fun_fu1534370419l_bool: $tType ).
thf(fun_fu647359111r_bool_type,type,
fun_fu647359111r_bool: $tType ).
thf(fun_fu1969117875t_bool_type,type,
fun_fu1969117875t_bool: $tType ).
thf(fun_fu612116759l_bool_type,type,
fun_fu612116759l_bool: $tType ).
thf(fun_fu1462073459l_bool_type,type,
fun_fu1462073459l_bool: $tType ).
thf(fun_fu1347521459l_bool_type,type,
fun_fu1347521459l_bool: $tType ).
thf(fun_fu86538581l_bool_type,type,
fun_fu86538581l_bool: $tType ).
thf(fun_fu1737014131l_bool_type,type,
fun_fu1737014131l_bool: $tType ).
thf(fun_fu1725641376l_bool_type,type,
fun_fu1725641376l_bool: $tType ).
thf(fun_fu298067067l_bool_type,type,
fun_fu298067067l_bool: $tType ).
thf(fun_fu370674997on_val_type,type,
fun_fu370674997on_val: $tType ).
thf(fun_fu2122484477l_bool_type,type,
fun_fu2122484477l_bool: $tType ).
thf(fun_fu254083683l_bool_type,type,
fun_fu254083683l_bool: $tType ).
thf(fun_fu1091766663r_bool_type,type,
fun_fu1091766663r_bool: $tType ).
thf(fun_fu43046697t_bool_type,type,
fun_fu43046697t_bool: $tType ).
thf(fun_fu878752391l_bool_type,type,
fun_fu878752391l_bool: $tType ).
thf(fun_fu1162814663l_bool_type,type,
fun_fu1162814663l_bool: $tType ).
thf(fun_fu388140521l_bool_type,type,
fun_fu388140521l_bool: $tType ).
thf(fun_fu1869012551l_bool_type,type,
fun_fu1869012551l_bool: $tType ).
thf(fun_fu1913539015l_bool_type,type,
fun_fu1913539015l_bool: $tType ).
thf(fun_fu1241242885l_bool_type,type,
fun_fu1241242885l_bool: $tType ).
thf(fun_fu676595845l_bool_type,type,
fun_fu676595845l_bool: $tType ).
thf(fun_fu1924376903on_val_type,type,
fun_fu1924376903on_val: $tType ).
thf(fun_fu2039604123r_bool_type,type,
fun_fu2039604123r_bool: $tType ).
thf(fun_fu2022309923l_bool_type,type,
fun_fu2022309923l_bool: $tType ).
thf(fun_fu114905943l_bool_type,type,
fun_fu114905943l_bool: $tType ).
thf(fun_fu1543849205l_bool_type,type,
fun_fu1543849205l_bool: $tType ).
thf(fun_fu2003389793l_bool_type,type,
fun_fu2003389793l_bool: $tType ).
thf(fun_fu2057241435l_bool_type,type,
fun_fu2057241435l_bool: $tType ).
thf(fun_fu1485943649l_bool_type,type,
fun_fu1485943649l_bool: $tType ).
thf(fun_fu781882819l_bool_type,type,
fun_fu781882819l_bool: $tType ).
thf(fun_fu450339090r_bool_type,type,
fun_fu450339090r_bool: $tType ).
thf(fun_fu297867453r_bool_type,type,
fun_fu297867453r_bool: $tType ).
thf(fun_fu964075521y_bool_type,type,
fun_fu964075521y_bool: $tType ).
thf(fun_fu2075294830l_bool_type,type,
fun_fu2075294830l_bool: $tType ).
thf(fun_fu863769827l_bool_type,type,
fun_fu863769827l_bool: $tType ).
thf(fun_fu1693644106l_bool_type,type,
fun_fu1693644106l_bool: $tType ).
thf(fun_fu503916907r_bool_type,type,
fun_fu503916907r_bool: $tType ).
thf(fun_fu347446253t_bool_type,type,
fun_fu347446253t_bool: $tType ).
thf(fun_fu1670877422y_bool_type,type,
fun_fu1670877422y_bool: $tType ).
thf(fun_fu1515717811l_bool_type,type,
fun_fu1515717811l_bool: $tType ).
thf(fun_fu1677251708l_bool_type,type,
fun_fu1677251708l_bool: $tType ).
thf(fun_fu615344397l_bool_type,type,
fun_fu615344397l_bool: $tType ).
thf(fun_fu1346254930l_bool_type,type,
fun_fu1346254930l_bool: $tType ).
thf(fun_fu905586428l_bool_type,type,
fun_fu905586428l_bool: $tType ).
thf(fun_fu544554869al_val_type,type,
fun_fu544554869al_val: $tType ).
thf(fun_fu277794946on_val_type,type,
fun_fu277794946on_val: $tType ).
thf(fun_fu593680828t_char_type,type,
fun_fu593680828t_char: $tType ).
thf(fun_fu194330259on_val_type,type,
fun_fu194330259on_val: $tType ).
thf(fun_fu1481433236al_val_type,type,
fun_fu1481433236al_val: $tType ).
thf(fun_fu1690035458on_val_type,type,
fun_fu1690035458on_val: $tType ).
thf(fun_fu1622757844on_val_type,type,
fun_fu1622757844on_val: $tType ).
thf(fun_fu1756175179r_bool_type,type,
fun_fu1756175179r_bool: $tType ).
thf(fun_fu552814479r_bool_type,type,
fun_fu552814479r_bool: $tType ).
thf(fun_fu1856038613r_bool_type,type,
fun_fu1856038613r_bool: $tType ).
thf(fun_fu351878095t_bool_type,type,
fun_fu351878095t_bool: $tType ).
thf(fun_fu1421250149l_bool_type,type,
fun_fu1421250149l_bool: $tType ).
thf(fun_fu1080564751l_bool_type,type,
fun_fu1080564751l_bool: $tType ).
thf(fun_fu283662671l_bool_type,type,
fun_fu283662671l_bool: $tType ).
thf(fun_fu1675319075l_bool_type,type,
fun_fu1675319075l_bool: $tType ).
thf(fun_fu1451507727l_bool_type,type,
fun_fu1451507727l_bool: $tType ).
thf(fun_fu1847833789r_bool_type,type,
fun_fu1847833789r_bool: $tType ).
thf(fun_fu408016699r_bool_type,type,
fun_fu408016699r_bool: $tType ).
thf(fun_fu1134959491on_val_type,type,
fun_fu1134959491on_val: $tType ).
thf(fun_fu1758230717l_bool_type,type,
fun_fu1758230717l_bool: $tType ).
thf(fun_fu1011371575l_bool_type,type,
fun_fu1011371575l_bool: $tType ).
thf(fun_fu252645753r_bool_type,type,
fun_fu252645753r_bool: $tType ).
thf(fun_fu1622098173t_bool_type,type,
fun_fu1622098173t_bool: $tType ).
thf(fun_fu1502964089l_bool_type,type,
fun_fu1502964089l_bool: $tType ).
thf(fun_fu1340506651l_bool_type,type,
fun_fu1340506651l_bool: $tType ).
thf(fun_fu1459957565l_bool_type,type,
fun_fu1459957565l_bool: $tType ).
thf(fun_fu1128668857l_bool_type,type,
fun_fu1128668857l_bool: $tType ).
thf(fun_fu431935003l_bool_type,type,
fun_fu431935003l_bool: $tType ).
thf(fun_fu515606202l_bool_type,type,
fun_fu515606202l_bool: $tType ).
thf(fun_fu134864139l_bool_type,type,
fun_fu134864139l_bool: $tType ).
thf(fun_fu1678064953on_val_type,type,
fun_fu1678064953on_val: $tType ).
thf(fun_fu1749814731r_bool_type,type,
fun_fu1749814731r_bool: $tType ).
thf(fun_fu936776617r_bool_type,type,
fun_fu936776617r_bool: $tType ).
thf(fun_fu1246919812l_bool_type,type,
fun_fu1246919812l_bool: $tType ).
thf(fun_fu250820942l_bool_type,type,
fun_fu250820942l_bool: $tType ).
thf(fun_fu570492181l_bool_type,type,
fun_fu570492181l_bool: $tType ).
thf(fun_fu100249073l_bool_type,type,
fun_fu100249073l_bool: $tType ).
thf(fun_fu684057754r_bool_type,type,
fun_fu684057754r_bool: $tType ).
thf(fun_fu1758268692t_bool_type,type,
fun_fu1758268692t_bool: $tType ).
thf(fun_fu2141444501y_bool_type,type,
fun_fu2141444501y_bool: $tType ).
thf(fun_fu1980233698l_bool_type,type,
fun_fu1980233698l_bool: $tType ).
thf(fun_fu606696995l_bool_type,type,
fun_fu606696995l_bool: $tType ).
thf(fun_fu217462836l_bool_type,type,
fun_fu217462836l_bool: $tType ).
thf(fun_fu266921985l_bool_type,type,
fun_fu266921985l_bool: $tType ).
thf(fun_fu110544035l_bool_type,type,
fun_fu110544035l_bool: $tType ).
thf(fun_fu1978109084al_val_type,type,
fun_fu1978109084al_val: $tType ).
thf(fun_fu2073188913on_val_type,type,
fun_fu2073188913on_val: $tType ).
thf(fun_fu1104134499t_char_type,type,
fun_fu1104134499t_char: $tType ).
thf(fun_fu540338626on_val_type,type,
fun_fu540338626on_val: $tType ).
thf(fun_fu2114777659al_val_type,type,
fun_fu2114777659al_val: $tType ).
thf(fun_fu1639641777on_val_type,type,
fun_fu1639641777on_val: $tType ).
thf(fun_fu1133203323on_val_type,type,
fun_fu1133203323on_val: $tType ).
thf(fun_fu1806184744l_bool_type,type,
fun_fu1806184744l_bool: $tType ).
thf(fun_fu351211973l_bool_type,type,
fun_fu351211973l_bool: $tType ).
thf(fun_fu448518251l_bool_type,type,
fun_fu448518251l_bool: $tType ).
thf(fun_fu228202007l_bool_type,type,
fun_fu228202007l_bool: $tType ).
thf(fun_fu1331974445r_bool_type,type,
fun_fu1331974445r_bool: $tType ).
thf(fun_fu1380761303t_bool_type,type,
fun_fu1380761303t_bool: $tType ).
thf(fun_fu910697661l_bool_type,type,
fun_fu910697661l_bool: $tType ).
thf(fun_fu830480791l_bool_type,type,
fun_fu830480791l_bool: $tType ).
thf(fun_fu102926423l_bool_type,type,
fun_fu102926423l_bool: $tType ).
thf(fun_fu2111126267l_bool_type,type,
fun_fu2111126267l_bool: $tType ).
thf(fun_fu551435671l_bool_type,type,
fun_fu551435671l_bool: $tType ).
thf(fun_fu394346421l_bool_type,type,
fun_fu394346421l_bool: $tType ).
thf(fun_fu649880763l_bool_type,type,
fun_fu649880763l_bool: $tType ).
thf(fun_fu1935975259on_val_type,type,
fun_fu1935975259on_val: $tType ).
thf(fun_fu740225039l_bool_type,type,
fun_fu740225039l_bool: $tType ).
thf(fun_fu192068197l_bool_type,type,
fun_fu192068197l_bool: $tType ).
thf(fun_fu48585473l_bool_type,type,
fun_fu48585473l_bool: $tType ).
thf(fun_fu1190526859r_bool_type,type,
fun_fu1190526859r_bool: $tType ).
thf(fun_fu1590192889l_bool_type,type,
fun_fu1590192889l_bool: $tType ).
thf(fun_fu2083094209l_bool_type,type,
fun_fu2083094209l_bool: $tType ).
thf(fun_fu79989156l_bool_type,type,
fun_fu79989156l_bool: $tType ).
thf(fun_fu1640122725l_bool_type,type,
fun_fu1640122725l_bool: $tType ).
thf(fun_fu1255792747l_bool_type,type,
fun_fu1255792747l_bool: $tType ).
thf(fun_fu1358756598l_bool_type,type,
fun_fu1358756598l_bool: $tType ).
thf(fun_fu680686147l_bool_type,type,
fun_fu680686147l_bool: $tType ).
thf(fun_fu1176066021l_bool_type,type,
fun_fu1176066021l_bool: $tType ).
thf(fun_fu964448643l_bool_type,type,
fun_fu964448643l_bool: $tType ).
thf(fun_fu1839934575r_bool_type,type,
fun_fu1839934575r_bool: $tType ).
thf(fun_fu1304373193r_bool_type,type,
fun_fu1304373193r_bool: $tType ).
thf(fun_fu1457514859l_bool_type,type,
fun_fu1457514859l_bool: $tType ).
thf(fun_fu1989717467l_bool_type,type,
fun_fu1989717467l_bool: $tType ).
thf(fun_fu1680591819l_bool_type,type,
fun_fu1680591819l_bool: $tType ).
thf(fun_fu459093885l_bool_type,type,
fun_fu459093885l_bool: $tType ).
thf(fun_fu947198233l_bool_type,type,
fun_fu947198233l_bool: $tType ).
thf(fun_fu201937213r_bool_type,type,
fun_fu201937213r_bool: $tType ).
thf(fun_fu1278173919t_bool_type,type,
fun_fu1278173919t_bool: $tType ).
thf(fun_fu712248957l_bool_type,type,
fun_fu712248957l_bool: $tType ).
thf(fun_fu1091135037l_bool_type,type,
fun_fu1091135037l_bool: $tType ).
thf(fun_fu1343174525l_bool_type,type,
fun_fu1343174525l_bool: $tType ).
thf(fun_fu823189407l_bool_type,type,
fun_fu823189407l_bool: $tType ).
thf(fun_fu1099749117l_bool_type,type,
fun_fu1099749117l_bool: $tType ).
thf(fun_fu1871906941l_bool_type,type,
fun_fu1871906941l_bool: $tType ).
thf(fun_fu285633298l_bool_type,type,
fun_fu285633298l_bool: $tType ).
thf(fun_fu405972463al_val_type,type,
fun_fu405972463al_val: $tType ).
thf(fun_fu1262577777l_bool_type,type,
fun_fu1262577777l_bool: $tType ).
thf(fun_fu192331261on_val_type,type,
fun_fu192331261on_val: $tType ).
thf(fun_fu1642197899l_bool_type,type,
fun_fu1642197899l_bool: $tType ).
thf(fun_fu1409163261t_char_type,type,
fun_fu1409163261t_char: $tType ).
thf(fun_fu233425312l_bool_type,type,
fun_fu233425312l_bool: $tType ).
thf(fun_fu21671997on_val_type,type,
fun_fu21671997on_val: $tType ).
thf(fun_fu892541875l_bool_type,type,
fun_fu892541875l_bool: $tType ).
thf(fun_fu967282605al_val_type,type,
fun_fu967282605al_val: $tType ).
thf(fun_fu1722968561l_bool_type,type,
fun_fu1722968561l_bool: $tType ).
thf(fun_fu911981683l_bool_type,type,
fun_fu911981683l_bool: $tType ).
thf(fun_fu442091053on_val_type,type,
fun_fu442091053on_val: $tType ).
thf(fun_fu1931670947l_bool_type,type,
fun_fu1931670947l_bool: $tType ).
thf(fun_fu942042787l_bool_type,type,
fun_fu942042787l_bool: $tType ).
thf(fun_fu1299212805l_bool_type,type,
fun_fu1299212805l_bool: $tType ).
thf(fun_fu816125185l_bool_type,type,
fun_fu816125185l_bool: $tType ).
thf(fun_fu938561337l_bool_type,type,
fun_fu938561337l_bool: $tType ).
thf(fun_fu783298731l_bool_type,type,
fun_fu783298731l_bool: $tType ).
thf(fun_fu626845499l_bool_type,type,
fun_fu626845499l_bool: $tType ).
thf(fun_fu574939677l_bool_type,type,
fun_fu574939677l_bool: $tType ).
thf(fun_fu1813077499l_bool_type,type,
fun_fu1813077499l_bool: $tType ).
thf(fun_fu621800173l_bool_type,type,
fun_fu621800173l_bool: $tType ).
thf(fun_fu698854459l_bool_type,type,
fun_fu698854459l_bool: $tType ).
thf(fun_fu1755700589l_bool_type,type,
fun_fu1755700589l_bool: $tType ).
thf(fun_fu1980133923l_bool_type,type,
fun_fu1980133923l_bool: $tType ).
thf(fun_fu1394314709l_bool_type,type,
fun_fu1394314709l_bool: $tType ).
thf(fun_fu722886165l_bool_type,type,
fun_fu722886165l_bool: $tType ).
thf(fun_fu1506313313l_bool_type,type,
fun_fu1506313313l_bool: $tType ).
thf(fun_fu1452544581l_bool_type,type,
fun_fu1452544581l_bool: $tType ).
thf(fun_fu470662369l_bool_type,type,
fun_fu470662369l_bool: $tType ).
thf(fun_fu820520599l_bool_type,type,
fun_fu820520599l_bool: $tType ).
thf(fun_fu1039024310l_bool_type,type,
fun_fu1039024310l_bool: $tType ).
thf(fun_fu1384113317l_bool_type,type,
fun_fu1384113317l_bool: $tType ).
thf(fun_fu1475575669l_bool_type,type,
fun_fu1475575669l_bool: $tType ).
thf(fun_fu1231936587l_bool_type,type,
fun_fu1231936587l_bool: $tType ).
thf(fun_fu775697111l_bool_type,type,
fun_fu775697111l_bool: $tType ).
thf(fun_fu2023535095l_bool_type,type,
fun_fu2023535095l_bool: $tType ).
thf(fun_fu610694927l_bool_type,type,
fun_fu610694927l_bool: $tType ).
thf(fun_fu1104572687l_bool_type,type,
fun_fu1104572687l_bool: $tType ).
thf(fun_fu164521751l_bool_type,type,
fun_fu164521751l_bool: $tType ).
thf(fun_fu229059973l_bool_type,type,
fun_fu229059973l_bool: $tType ).
thf(fun_fu369322201l_bool_type,type,
fun_fu369322201l_bool: $tType ).
thf(fun_fu1002878233l_bool_type,type,
fun_fu1002878233l_bool: $tType ).
thf(fun_fu983865091l_bool_type,type,
fun_fu983865091l_bool: $tType ).
thf(fun_fu1934636263l_bool_type,type,
fun_fu1934636263l_bool: $tType ).
thf(fun_fu371764249l_bool_type,type,
fun_fu371764249l_bool: $tType ).
thf(fun_fu1914454703r_bool_type,type,
fun_fu1914454703r_bool: $tType ).
thf(fun_fu2007671769t_bool_type,type,
fun_fu2007671769t_bool: $tType ).
thf(fun_fu1479301695l_bool_type,type,
fun_fu1479301695l_bool: $tType ).
thf(fun_fu1562135449l_bool_type,type,
fun_fu1562135449l_bool: $tType ).
thf(fun_fu1345961817l_bool_type,type,
fun_fu1345961817l_bool: $tType ).
thf(fun_fu937561981l_bool_type,type,
fun_fu937561981l_bool: $tType ).
thf(fun_fu2138074009l_bool_type,type,
fun_fu2138074009l_bool: $tType ).
thf(fun_fu1176482875l_bool_type,type,
fun_fu1176482875l_bool: $tType ).
thf(fun_fu1753546205on_val_type,type,
fun_fu1753546205on_val: $tType ).
thf(fun_fu151382129l_bool_type,type,
fun_fu151382129l_bool: $tType ).
thf(fun_fu2085256997l_bool_type,type,
fun_fu2085256997l_bool: $tType ).
thf(fun_fu1587641869l_bool_type,type,
fun_fu1587641869l_bool: $tType ).
thf(fun_fu1116138167r_bool_type,type,
fun_fu1116138167r_bool: $tType ).
thf(fun_fu981148631l_bool_type,type,
fun_fu981148631l_bool: $tType ).
thf(fun_fu177229913l_bool_type,type,
fun_fu177229913l_bool: $tType ).
thf(fun_fu2000143900r_bool_type,type,
fun_fu2000143900r_bool: $tType ).
thf(fun_fu62768508t_bool_type,type,
fun_fu62768508t_bool: $tType ).
thf(fun_fu1380567140l_bool_type,type,
fun_fu1380567140l_bool: $tType ).
thf(fun_fu1615233035l_bool_type,type,
fun_fu1615233035l_bool: $tType ).
thf(fun_fu1221203484l_bool_type,type,
fun_fu1221203484l_bool: $tType ).
thf(fun_fu1912681219l_bool_type,type,
fun_fu1912681219l_bool: $tType ).
thf(fun_fu1025487243l_bool_type,type,
fun_fu1025487243l_bool: $tType ).
thf(fun_fu1718160452on_val_type,type,
fun_fu1718160452on_val: $tType ).
thf(fun_fu1329575219on_val_type,type,
fun_fu1329575219on_val: $tType ).
thf(fun_fu1354978043l_bool_type,type,
fun_fu1354978043l_bool: $tType ).
thf(fun_fu1545449147l_bool_type,type,
fun_fu1545449147l_bool: $tType ).
thf(fun_fu1061236771l_bool_type,type,
fun_fu1061236771l_bool: $tType ).
thf(fun_fu353473623l_bool_type,type,
fun_fu353473623l_bool: $tType ).
thf(fun_fu586179709l_bool_type,type,
fun_fu586179709l_bool: $tType ).
thf(fun_fu1952537362l_bool_type,type,
fun_fu1952537362l_bool: $tType ).
thf(fun_fu436897911l_bool_type,type,
fun_fu436897911l_bool: $tType ).
thf(fun_fu1542084125r_bool_type,type,
fun_fu1542084125r_bool: $tType ).
thf(fun_fu524930393l_bool_type,type,
fun_fu524930393l_bool: $tType ).
thf(fun_fu121169625l_bool_type,type,
fun_fu121169625l_bool: $tType ).
thf(fun_fu819253913l_bool_type,type,
fun_fu819253913l_bool: $tType ).
thf(fun_fu1929656089l_bool_type,type,
fun_fu1929656089l_bool: $tType ).
thf(fun_fu908828651l_bool_type,type,
fun_fu908828651l_bool: $tType ).
thf(fun_fu1802993177l_bool_type,type,
fun_fu1802993177l_bool: $tType ).
thf(fun_fu1319073539l_bool_type,type,
fun_fu1319073539l_bool: $tType ).
thf(fun_fu1929378469l_bool_type,type,
fun_fu1929378469l_bool: $tType ).
thf(fun_fu225006629l_bool_type,type,
fun_fu225006629l_bool: $tType ).
thf(fun_fu169292119l_bool_type,type,
fun_fu169292119l_bool: $tType ).
thf(fun_fu1003774433l_bool_type,type,
fun_fu1003774433l_bool: $tType ).
thf(fun_Pr252072522l_bool_type,type,
fun_Pr252072522l_bool: $tType ).
thf(fun_Pr1232540755ion_ty_type,type,
fun_Pr1232540755ion_ty: $tType ).
thf(fun_Pr1013877532on_val_type,type,
fun_Pr1013877532on_val: $tType ).
thf(fun_Pr84112868r_bool_type,type,
fun_Pr84112868r_bool: $tType ).
thf(fun_Pr1938343180on_val_type,type,
fun_Pr1938343180on_val: $tType ).
thf(fun_Pr1521028203r_bool_type,type,
fun_Pr1521028203r_bool: $tType ).
thf(fun_Pr2147252461t_bool_type,type,
fun_Pr2147252461t_bool: $tType ).
thf(fun_Pr1713170355l_bool_type,type,
fun_Pr1713170355l_bool: $tType ).
thf(fun_Pr1298510204l_bool_type,type,
fun_Pr1298510204l_bool: $tType ).
thf(fun_Pr324453901l_bool_type,type,
fun_Pr324453901l_bool: $tType ).
thf(fun_Pr1649941330l_bool_type,type,
fun_Pr1649941330l_bool: $tType ).
thf(fun_Pr842269692l_bool_type,type,
fun_Pr842269692l_bool: $tType ).
thf(fun_Pr1439582210on_val_type,type,
fun_Pr1439582210on_val: $tType ).
thf(fun_Pr680585871l_bool_type,type,
fun_Pr680585871l_bool: $tType ).
thf(fun_Pr1298293016ion_ty_type,type,
fun_Pr1298293016ion_ty: $tType ).
thf(fun_Pr1215677793on_val_type,type,
fun_Pr1215677793on_val: $tType ).
thf(fun_Pr1780479017r_bool_type,type,
fun_Pr1780479017r_bool: $tType ).
thf(fun_Pr1790314577on_val_type,type,
fun_Pr1790314577on_val: $tType ).
thf(fun_Pr2007843174r_bool_type,type,
fun_Pr2007843174r_bool: $tType ).
thf(fun_Pr704700594t_bool_type,type,
fun_Pr704700594t_bool: $tType ).
thf(fun_Pr165898670l_bool_type,type,
fun_Pr165898670l_bool: $tType ).
thf(fun_Pr633696065l_bool_type,type,
fun_Pr633696065l_bool: $tType ).
thf(fun_Pr1590835018r_bool_type,type,
fun_Pr1590835018r_bool: $tType ).
thf(fun_Pr1454982756t_bool_type,type,
fun_Pr1454982756t_bool: $tType ).
thf(fun_Pr1094589074l_bool_type,type,
fun_Pr1094589074l_bool: $tType ).
thf(fun_Pr741412723l_bool_type,type,
fun_Pr741412723l_bool: $tType ).
thf(fun_Pr351033732l_bool_type,type,
fun_Pr351033732l_bool: $tType ).
thf(fun_Pr243522225l_bool_type,type,
fun_Pr243522225l_bool: $tType ).
thf(fun_Pr293514739l_bool_type,type,
fun_Pr293514739l_bool: $tType ).
thf(fun_Pr1719283041on_val_type,type,
fun_Pr1719283041on_val: $tType ).
thf(fun_Pr1391347915on_val_type,type,
fun_Pr1391347915on_val: $tType ).
thf(fun_Pr1763091538l_bool_type,type,
fun_Pr1763091538l_bool: $tType ).
thf(fun_Pr741448269l_bool_type,type,
fun_Pr741448269l_bool: $tType ).
thf(fun_Pr134674113l_bool_type,type,
fun_Pr134674113l_bool: $tType ).
thf(fun_Pr2087158653on_val_type,type,
fun_Pr2087158653on_val: $tType ).
thf(fun_Pr714818201on_val_type,type,
fun_Pr714818201on_val: $tType ).
thf(fun_Pr565113489r_bool_type,type,
fun_Pr565113489r_bool: $tType ).
thf(fun_Pr806764899on_val_type,type,
fun_Pr806764899on_val: $tType ).
thf(fun_Pr1241534948r_bool_type,type,
fun_Pr1241534948r_bool: $tType ).
thf(fun_Pr1377794996t_bool_type,type,
fun_Pr1377794996t_bool: $tType ).
thf(fun_Pr929778732l_bool_type,type,
fun_Pr929778732l_bool: $tType ).
thf(fun_Pr1315489347l_bool_type,type,
fun_Pr1315489347l_bool: $tType ).
thf(fun_Pr1057736788l_bool_type,type,
fun_Pr1057736788l_bool: $tType ).
thf(fun_Pr454045387l_bool_type,type,
fun_Pr454045387l_bool: $tType ).
thf(fun_Pr1243525059l_bool_type,type,
fun_Pr1243525059l_bool: $tType ).
thf(fun_Pr100252923on_val_type,type,
fun_Pr100252923on_val: $tType ).
thf(fun_Pr315804320l_bool_type,type,
fun_Pr315804320l_bool: $tType ).
thf(fun_Pr876827561ion_ty_type,type,
fun_Pr876827561ion_ty: $tType ).
thf(fun_Pr828669810on_val_type,type,
fun_Pr828669810on_val: $tType ).
thf(fun_Pr1385456186r_bool_type,type,
fun_Pr1385456186r_bool: $tType ).
thf(fun_Pr357631842on_val_type,type,
fun_Pr357631842on_val: $tType ).
thf(fun_Pr1889776021r_bool_type,type,
fun_Pr1889776021r_bool: $tType ).
thf(fun_Pr462529091t_bool_type,type,
fun_Pr462529091t_bool: $tType ).
thf(fun_Pr1142346461l_bool_type,type,
fun_Pr1142346461l_bool: $tType ).
thf(fun_Pr688287442l_bool_type,type,
fun_Pr688287442l_bool: $tType ).
thf(fun_Pr788853347l_bool_type,type,
fun_Pr788853347l_bool: $tType ).
thf(fun_Pr1040313468l_bool_type,type,
fun_Pr1040313468l_bool: $tType ).
thf(fun_Pr193017682l_bool_type,type,
fun_Pr193017682l_bool: $tType ).
thf(fun_Pr1517604908on_val_type,type,
fun_Pr1517604908on_val: $tType ).
thf(fun_Pr70170387r_bool_type,type,
fun_Pr70170387r_bool: $tType ).
thf(fun_Pr2081272681l_bool_type,type,
fun_Pr2081272681l_bool: $tType ).
thf(fun_Pr1325259506ion_ty_type,type,
fun_Pr1325259506ion_ty: $tType ).
thf(fun_Pr759034427on_val_type,type,
fun_Pr759034427on_val: $tType ).
thf(fun_Pr192342275r_bool_type,type,
fun_Pr192342275r_bool: $tType ).
thf(fun_Pr1900992299on_val_type,type,
fun_Pr1900992299on_val: $tType ).
thf(fun_Pr1756358412r_bool_type,type,
fun_Pr1756358412r_bool: $tType ).
thf(fun_Pr1087127692t_bool_type,type,
fun_Pr1087127692t_bool: $tType ).
thf(fun_Pr583235924l_bool_type,type,
fun_Pr583235924l_bool: $tType ).
thf(fun_Pr307551003l_bool_type,type,
fun_Pr307551003l_bool: $tType ).
thf(fun_Pr1667914028l_bool_type,type,
fun_Pr1667914028l_bool: $tType ).
thf(fun_Pr324760563l_bool_type,type,
fun_Pr324760563l_bool: $tType ).
thf(fun_Pr1619270811l_bool_type,type,
fun_Pr1619270811l_bool: $tType ).
thf(fun_Pr1615326228al_val_type,type,
fun_Pr1615326228al_val: $tType ).
thf(fun_Pr1618910755on_val_type,type,
fun_Pr1618910755on_val: $tType ).
thf(fun_Pr1696029455l_bool_type,type,
fun_Pr1696029455l_bool: $tType ).
thf(fun_Pr733352344ion_ty_type,type,
fun_Pr733352344ion_ty: $tType ).
thf(fun_Pr385431009on_val_type,type,
fun_Pr385431009on_val: $tType ).
thf(fun_Pr1386046633r_bool_type,type,
fun_Pr1386046633r_bool: $tType ).
thf(fun_Pr1625553105on_val_type,type,
fun_Pr1625553105on_val: $tType ).
thf(fun_Pr1439232230r_bool_type,type,
fun_Pr1439232230r_bool: $tType ).
thf(fun_Pr1288966450t_bool_type,type,
fun_Pr1288966450t_bool: $tType ).
thf(fun_Pr656644398l_bool_type,type,
fun_Pr656644398l_bool: $tType ).
thf(fun_Pr1793564609l_bool_type,type,
fun_Pr1793564609l_bool: $tType ).
thf(fun_Pr562304210l_bool_type,type,
fun_Pr562304210l_bool: $tType ).
thf(fun_Pr974014925l_bool_type,type,
fun_Pr974014925l_bool: $tType ).
thf(fun_Pr598845249l_bool_type,type,
fun_Pr598845249l_bool: $tType ).
thf(fun_Pr1009028282al_val_type,type,
fun_Pr1009028282al_val: $tType ).
thf(fun_Pr231134077on_val_type,type,
fun_Pr231134077on_val: $tType ).
thf(fun_Pr2135303553t_char_type,type,
fun_Pr2135303553t_char: $tType ).
thf(fun_Pr1684668686on_val_type,type,
fun_Pr1684668686on_val: $tType ).
thf(fun_Pr143388889al_val_type,type,
fun_Pr143388889al_val: $tType ).
thf(fun_Pr1833267965on_val_type,type,
fun_Pr1833267965on_val: $tType ).
thf(fun_Pr336360217on_val_type,type,
fun_Pr336360217on_val: $tType ).
thf(fun_Pr691271849l_bool_type,type,
fun_Pr691271849l_bool: $tType ).
thf(fun_Pr129626572r_bool_type,type,
fun_Pr129626572r_bool: $tType ).
thf(fun_Pr592733644t_bool_type,type,
fun_Pr592733644t_bool: $tType ).
thf(fun_Pr2142553108l_bool_type,type,
fun_Pr2142553108l_bool: $tType ).
thf(fun_Pr650805339l_bool_type,type,
fun_Pr650805339l_bool: $tType ).
thf(fun_Pr381296236l_bool_type,type,
fun_Pr381296236l_bool: $tType ).
thf(fun_Pr1931476659l_bool_type,type,
fun_Pr1931476659l_bool: $tType ).
thf(fun_Pr1404764635l_bool_type,type,
fun_Pr1404764635l_bool: $tType ).
thf(fun_Pr1727285475on_val_type,type,
fun_Pr1727285475on_val: $tType ).
thf(produc1645268488al_val_type,type,
produc1645268488al_val: $tType ).
thf(produc124828825on_val_type,type,
produc124828825on_val: $tType ).
thf(produc1278157519t_char_type,type,
produc1278157519t_char: $tType ).
thf(produc639455274on_val_type,type,
produc639455274on_val: $tType ).
thf(produc1013743697t_char_type,type,
produc1013743697t_char: $tType ).
thf(product_prod_val_val_type,type,
product_prod_val_val: $tType ).
thf(produc12694297on_val_type,type,
produc12694297on_val: $tType ).
thf(produc1102272487on_val_type,type,
produc1102272487on_val: $tType ).
thf(fun_up1149430426on_val_decl,type,
fun_up1149430426on_val: fun_li1432931796on_val > list_char > option_val > fun_li1432931796on_val ).
thf(some_val_decl,type,
some_val: fun_val_option_val ).
thf(produc1259058957on_val_decl,type,
produc1259058957on_val: fun_ex977868519on_val ).
thf(produc899768717on_val_decl,type,
produc899768717on_val: fun_fu1639641777on_val ).
thf(produc1441475159on_val_decl,type,
produc1441475159on_val: fun_Pr1391347915on_val ).
thf(red_decl,type,
red: list_P1999446415t_char > fun_Pr691271849l_bool ).
thf(is_refT_decl,type,
is_refT: ty > bool ).
thf(class_decl,type,
class: list_char > ty ).
thf(nt_decl,type,
nt: ty ).
thf(fFalse_decl,type,
fFalse: bool ).
thf(fTrue_decl,type,
fTrue: bool ).
thf(hAPP_e1659493427on_val_decl,type,
hAPP_e1659493427on_val: fun_ex977868519on_val > exp_list_char > fun_Pr231134077on_val ).
thf(hAPP_val_option_val_decl,type,
hAPP_val_option_val: fun_val_option_val > val > option_val ).
thf(hAPP_f1727192346on_val_decl,type,
hAPP_f1727192346on_val: fun_fu1690035458on_val > fun_li1432931796on_val > produc12694297on_val ).
thf(hAPP_f1849790461on_val_decl,type,
hAPP_f1849790461on_val: fun_fu1639641777on_val > fun_na939144002on_val > fun_fu1690035458on_val ).
thf(hAPP_P1870962205on_val_decl,type,
hAPP_P1870962205on_val: fun_Pr1391347915on_val > produc124828825on_val > fun_Pr714818201on_val ).
thf(hAPP_P1886180715on_val_decl,type,
hAPP_P1886180715on_val: fun_Pr714818201on_val > produc124828825on_val > produc1102272487on_val ).
thf(hAPP_P604205461on_val_decl,type,
hAPP_P604205461on_val: fun_Pr231134077on_val > produc12694297on_val > produc124828825on_val ).
thf(hBOOL_decl,type,
hBOOL: bool > $o ).
thf(member773094996on_val_decl,type,
member773094996on_val: produc1102272487on_val > fun_Pr691271849l_bool > bool ).
thf(p_decl,type,
p: list_P1999446415t_char ).
thf(v_1_decl,type,
v_1: list_char ).
thf(e_a_decl,type,
e_a: exp_list_char ).
thf(ea_decl,type,
ea: exp_list_char ).
thf(h_a_decl,type,
h_a: fun_na939144002on_val ).
thf(ha_decl,type,
ha: fun_na939144002on_val ).
thf(l_a_decl,type,
l_a: fun_li1432931796on_val ).
thf(la_decl,type,
la: fun_li1432931796on_val ).
thf(v_decl,type,
v: val ).
thf(sk99_decl,type,
sk99: ty > list_char ).
thf(sk99_def,definition,
( sk99
= ( ^ [A: ty] :
@+[B: list_char] :
( A
= ( B @ class ) ) ) ) ).
thf(559,axiom,
~ ( fFalse @ hBOOL ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
thf(3021,plain,
~ ( fFalse @ hBOOL ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[559]) ).
thf(3022,plain,
~ ( fFalse @ hBOOL ),
inference(polarity_switch,[status(thm)],[3021]) ).
thf(594,axiom,
p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) @ hBOOL,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_InitBlockRed_I1_J) ).
thf(3162,plain,
p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) @ hBOOL,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[594]) ).
thf(95,axiom,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
thf(1126,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(1127,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(cnf,[status(esa)],[1126]) ).
thf(1128,plain,
! [A: bool] :
( ( A = fFalse )
| ( A = fTrue ) ),
inference(lifteq,[status(thm)],[1127]) ).
thf(1,conjecture,
p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) @ hBOOL,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) @ hBOOL ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(760,plain,
~ ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) @ hBOOL ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(3893,plain,
! [A: bool] :
( ( A
!= ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) ) )
| ~ ( fTrue @ hBOOL )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[1128,760]) ).
thf(3894,plain,
( ~ ( fTrue @ hBOOL )
| ( ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) )
= fFalse ) ),
inference(pattern_uni,[status(thm)],[3893:[bind(A,$thf( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) ))]]) ).
thf(289,axiom,
! [A: ty] :
( ( A @ is_refT @ hBOOL )
<=> ( ? [B: list_char] :
( A
= ( B @ class ) )
| ( A = nt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_657_is__refT__def) ).
thf(1933,plain,
! [A: ty] :
( ( ( ? [B: list_char] :
( A
= ( B @ class ) )
| ( A = nt ) )
=> ( A @ is_refT @ hBOOL ) )
& ( ( A @ is_refT @ hBOOL )
=> ( ? [B: list_char] :
( A
= ( B @ class ) )
| ( A = nt ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[289]) ).
thf(1934,plain,
( ! [A: ty] :
( ( ? [B: list_char] :
( A
= ( B @ class ) )
| ( A = nt ) )
=> ( A @ is_refT @ hBOOL ) )
& ! [A: ty] :
( ( A @ is_refT @ hBOOL )
=> ( ? [B: list_char] :
( A
= ( B @ class ) )
| ( A = nt ) ) ) ),
inference(miniscope,[status(thm)],[1933]) ).
thf(1935,plain,
! [C: list_char,B: ty,A: ty] :
( ( ( B @ is_refT @ hBOOL )
| ( B
!= ( C @ class ) ) )
& ( ( B @ is_refT @ hBOOL )
| ( B != nt ) )
& ( ( A
= ( A @ sk99 @ class ) )
| ( A = nt )
| ~ ( A @ is_refT @ hBOOL ) ) ),
inference(cnf,[status(esa)],[1934]) ).
thf(1937,plain,
! [A: ty] :
( ( A @ is_refT @ hBOOL )
| ( A != nt ) ),
inference(cnfConj,[status(thm)],[1935]) ).
thf(1940,plain,
! [A: ty] :
( ( A @ is_refT @ hBOOL )
| ( A != nt ) ),
inference(lifteq,[status(thm)],[1937]) ).
thf(1941,plain,
nt @ is_refT @ hBOOL,
inference(simp,[status(thm)],[1940]) ).
thf(3932,plain,
! [A: bool] :
( ( A
!= ( nt @ is_refT ) )
| ( fTrue @ hBOOL )
| ( A = fFalse ) ),
inference(paramod_ordered,[status(thm)],[1128,1941]) ).
thf(3933,plain,
( ( fTrue @ hBOOL )
| ( ( nt @ is_refT )
= fFalse ) ),
inference(pattern_uni,[status(thm)],[3932:[bind(A,$thf( nt @ is_refT ))]]) ).
thf(3767,plain,
( ( ( nt @ is_refT @ hBOOL )
!= ( fFalse @ hBOOL ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1941,3022]) ).
thf(3768,plain,
( ( nt @ is_refT @ hBOOL )
!= ( fFalse @ hBOOL ) ),
inference(simp,[status(thm)],[3767]) ).
thf(3770,plain,
( ( nt @ is_refT )
!= fFalse ),
inference(simp,[status(thm)],[3768]) ).
thf(4009,plain,
fTrue @ hBOOL,
inference(simplifyReflect,[status(thm)],[3933,3770]) ).
thf(4010,plain,
( ~ $true
| ( ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) )
= fFalse ) ),
inference(rewrite,[status(thm)],[3894,4009]) ).
thf(4011,plain,
( ( p @ red @ ( l_a @ ( h_a @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( e_a @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( v @ ( some_val @ hAPP_val_option_val ) @ ( v_1 @ ( la @ fun_up1149430426on_val ) ) @ ( ha @ ( produc899768717on_val @ hAPP_f1849790461on_val ) @ hAPP_f1727192346on_val ) @ ( ea @ ( produc1259058957on_val @ hAPP_e1659493427on_val ) @ hAPP_P604205461on_val ) @ ( produc1441475159on_val @ hAPP_P1870962205on_val ) @ hAPP_P1886180715on_val ) @ member773094996on_val ) )
= fFalse ),
inference(simp,[status(thm)],[4010]) ).
thf(24864,plain,
fFalse @ hBOOL,
inference(rewrite,[status(thm)],[3162,4011]) ).
thf(24865,plain,
~ $true,
inference(rewrite,[status(thm)],[3022,24864]) ).
thf(24866,plain,
$false,
inference(simp,[status(thm)],[24865]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW478_2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.39 % Computer : n011.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sat Sep 26 16:07:29 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.84/0.97 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.78/1.50 % [INFO] Parsing done (526ms).
% 2.78/1.52 % [INFO] Running in sequential loop mode.
% 3.54/1.88 % [INFO] eprover registered as external prover.
% 3.54/1.89 % [INFO] Scanning for conjecture ...
% 4.58/2.24 % [INFO] Found a conjecture (or negated_conjecture) and 765 axioms. Running axiom selection ...
% 6.68/2.72 % [INFO] Axiom selection finished. Selected 757 axioms (removed 8 axioms).
% 9.30/3.42 % [INFO] Problem is typed first-order (TPTP TFF).
% 9.30/3.45 % [INFO] Type checking passed.
% 9.30/3.45 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 13.67/4.74 % [INFO] [Domain constraints] Detected constraint on bool
% 13.67/4.74 % [INFO] [Domain constraints] dom(bool) ⊆ {fTrue,fFalse}
% 15.83/5.25 % [INFO] [Domain constraints] Detected constraint on bop
% 15.83/5.25 % [INFO] [Domain constraints] dom(bop) ⊆ {c_Expr_Obop_OEq,add}
% 170.29/86.35 % [INFO] Killing All external provers ...
% 170.29/86.35 % Time passed: 85812ms (effective reasoning time: 84823ms)
% 170.29/86.35 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 170.29/86.35 % Axioms used in derivation (4): help_fFalse_1_1_U, fact_1_InitBlockRed_I1_J, help_fFalse_1_1_T, fact_657_is__refT__def
% 170.29/86.35 % No. of inferences in proof: 32
% 170.29/86.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 85812 ms resp. 84823 ms w/o parsing
% 170.29/86.39 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 170.29/86.39 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------