%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP142^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n018.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 : Wed Sep 30 08:06:55 AM UTC 2026
% Result : Theorem 18.35s 5.04s
% Output : Refutation 19.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 177
% Syntax : Number of formulae : 356 ( 176 unt; 0 typ; 0 def)
% Number of atoms : 822 ( 548 equ; 0 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 3716 ( 206 ~; 16 |; 90 &;2934 @)
% ( 0 <=>; 470 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Number of types : 41 ( 40 usr)
% Number of type conns : 240 ( 240 >; 0 *; 0 +; 0 <<)
% Number of symbols : 41 ( 39 usr; 9 con; 0-3 aty)
% Number of variables : 1384 ( 10 ^;1316 !; 58 ?;1384 :)
% Comments :
%------------------------------------------------------------------------------
thf(set_Pr1696918727_state_type,type,
set_Pr1696918727_state: $tType ).
thf(produc270545127_state_type,type,
produc270545127_state: $tType ).
thf(set_Pr541394119_state_type,type,
set_Pr541394119_state: $tType ).
thf(produc2046512871_state_type,type,
produc2046512871_state: $tType ).
thf(set_Pr1847866567_state_type,type,
set_Pr1847866567_state: $tType ).
thf(produc1519776487_state_type,type,
produc1519776487_state: $tType ).
thf(set_Pr1325664839_state_type,type,
set_Pr1325664839_state: $tType ).
thf(produc1586269031_state_type,type,
produc1586269031_state: $tType ).
thf(set_Pr2096893127_state_type,type,
set_Pr2096893127_state: $tType ).
thf(produc186437863_state_type,type,
produc186437863_state: $tType ).
thf(set_Pr1419004359_state_type,type,
set_Pr1419004359_state: $tType ).
thf(set_Pr135335153st_com_type,type,
set_Pr135335153st_com: $tType ).
thf(produc392316135_state_type,type,
produc392316135_state: $tType ).
thf(produc1440412305st_com_type,type,
produc1440412305st_com: $tType ).
thf(set_Pr1142642759_state_type,type,
set_Pr1142642759_state: $tType ).
thf(set_Pr2083163591st_com_type,type,
set_Pr2083163591st_com: $tType ).
thf(list_P1627643054te_nat_type,type,
list_P1627643054te_nat: $tType ).
thf(produc1225889383_state_type,type,
produc1225889383_state: $tType ).
thf(produc1762014951st_com_type,type,
produc1762014951st_com: $tType ).
thf(list_P890094829_state_type,type,
list_P890094829_state: $tType ).
thf(set_Pr1165141447_state_type,type,
set_Pr1165141447_state: $tType ).
thf(produc410756839_state_type,type,
produc410756839_state: $tType ).
thf(set_Pr391631483_state_type,type,
set_Pr391631483_state: $tType ).
thf(list_P1178430914te_nat_type,type,
list_P1178430914te_nat: $tType ).
thf(produc1393453339_state_type,type,
produc1393453339_state: $tType ).
thf(produc2058209240st_com_type,type,
produc2058209240st_com: $tType ).
thf(set_Pr602326075st_com_type,type,
set_Pr602326075st_com: $tType ).
thf(list_P1040014977_state_type,type,
list_P1040014977_state: $tType ).
thf(set_Pr849496667_state_type,type,
set_Pr849496667_state: $tType ).
thf(produc258871771st_com_type,type,
produc258871771st_com: $tType ).
thf(produc2041926651_state_type,type,
produc2041926651_state: $tType ).
thf(set_Pr1822651163om_com_type,type,
set_Pr1822651163om_com: $tType ).
thf(product_prod_com_com_type,type,
product_prod_com_com: $tType ).
thf(list_list_com_type,type,
list_list_com: $tType ).
thf(list_state_type,type,
list_state: $tType ).
thf(set_state_type,type,
set_state: $tType ).
thf(list_com_type,type,
list_com: $tType ).
thf(state_type,type,
state: $tType ).
thf(com_type,type,
com: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(append_com_decl,type,
append_com: list_com > list_com > list_com ).
thf(bind_com_com_decl,type,
bind_com_com: list_com > ( com > list_com ) > list_com ).
thf(butlast_com_decl,type,
butlast_com: list_com > list_com ).
thf(insert_com_decl,type,
insert_com: com > list_com > list_com ).
thf(last_com_decl,type,
last_com: list_com > com ).
thf(cons_com_decl,type,
cons_com: com > list_com > list_com ).
thf(nil_Pr1876916290te_nat_decl,type,
nil_Pr1876916290te_nat: list_P1178430914te_nat ).
thf(nil_com_decl,type,
nil_com: list_com ).
thf(list_ex1_com_decl,type,
list_ex1_com: ( com > $o ) > list_com > $o ).
thf(list_update_com_decl,type,
list_update_com: list_com > nat > com > list_com ).
thf(maps_com_com_decl,type,
maps_com_com: ( com > list_com ) > list_com > list_com ).
thf(measur1071343867_state_decl,type,
measur1071343867_state: list_P1178430914te_nat > set_Pr1165141447_state ).
thf(nth_com_decl,type,
nth_com: list_com > nat > com ).
thf(rotate1_com_decl,type,
rotate1_com: list_com > list_com ).
thf(size_size_list_com_decl,type,
size_size_list_com: list_com > nat ).
thf(pHoare259243666_exec1_decl,type,
pHoare259243666_exec1: set_Pr1165141447_state ).
thf(pHoare259243732_execs_decl,type,
pHoare259243732_execs: state > list_com > state > $o ).
thf(pHoare806997636termis_decl,type,
pHoare806997636termis: list_com > state > $o ).
thf(cond_decl,type,
cond: ( state > $o ) > com > com > com ).
thf(do_decl,type,
do: ( state > set_state ) > com ).
thf(semi_decl,type,
semi: com > com > com ).
thf(while_decl,type,
while: ( state > $o ) > com > com ).
thf(exec_decl,type,
exec: state > com > state > $o ).
thf(termi_decl,type,
termi: com > state > $o ).
thf(produc1914379986st_com_decl,type,
produc1914379986st_com: ( com > com > $o ) > list_com > produc2058209240st_com ).
thf(produc1307105171st_com_decl,type,
produc1307105171st_com: list_com > list_com > produc258871771st_com ).
thf(produc1204172211_state_decl,type,
produc1204172211_state: list_com > state > produc2041926651_state ).
thf(produc1909270103_state_decl,type,
produc1909270103_state: produc2041926651_state > produc2041926651_state > produc410756839_state ).
thf(produc2065881943_state_decl,type,
produc2065881943_state: produc410756839_state > produc410756839_state > produc186437863_state ).
thf(irrefl654089520_state_decl,type,
irrefl654089520_state: set_Pr1165141447_state > $o ).
thf(collec300063826_state_decl,type,
collec300063826_state: ( produc410756839_state > $o ) > set_Pr1165141447_state ).
thf(transi1302705790_state_decl,type,
transi1302705790_state: set_Pr1165141447_state > set_Pr1165141447_state ).
thf(member_state_decl,type,
member_state: state > set_state > $o ).
thf(member1069318160_state_decl,type,
member1069318160_state: produc410756839_state > set_Pr1165141447_state > $o ).
thf(c_decl,type,
c: com ).
thf(c2_decl,type,
c2: com ).
thf(cs_decl,type,
cs: list_com ).
thf(s_decl,type,
s: state ).
thf(s2_decl,type,
s2: state ).
thf(55,axiom,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc2041926651_state,E: list_com,F: state] : ( A @ ( produc2065881943_state @ C @ ( produc1909270103_state @ D @ ( produc1204172211_state @ E @ F ) ) ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_prod__induct4) ).
thf(383,plain,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc2041926651_state,E: list_com,F: state] : ( A @ ( produc2065881943_state @ C @ ( produc1909270103_state @ D @ ( produc1204172211_state @ E @ F ) ) ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(146,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_Pair__inject) ).
thf(892,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(44,axiom,
! [A: list_com] :
( ( append_com @ nil_com @ A )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_append__Nil) ).
thf(347,plain,
! [A: list_com] :
( ( append_com @ nil_com @ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(175,axiom,
! [A: state > $o,B: state,C: com,D: com] :
( ~ ( A @ B )
=> ( ( termi @ C @ B )
=> ( termi @ ( cond @ A @ D @ C ) @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_termi_OIfFalse) ).
thf(1031,plain,
! [A: state > $o,B: state,C: com,D: com] :
( ~ ( A @ B )
=> ( ( termi @ C @ B )
=> ( termi @ ( cond @ A @ D @ C ) @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(15,axiom,
! [A: com,B: list_com] :
( ( rotate1_com @ ( cons_com @ A @ B ) )
= ( append_com @ B @ ( cons_com @ A @ nil_com ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_275_rotate1_Osimps_I2_J) ).
thf(234,plain,
! [A: com,B: list_com] :
( ( rotate1_com @ ( cons_com @ A @ B ) )
= ( append_com @ B @ ( cons_com @ A @ nil_com ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(157,axiom,
! [A: produc410756839_state,B: produc410756839_state > $o] :
( ( member1069318160_state @ A @ ( collec300063826_state @ B ) )
= ( B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_mem__Collect__eq) ).
thf(941,plain,
! [A: produc410756839_state,B: produc410756839_state > $o] :
( ( member1069318160_state @ A @ ( collec300063826_state @ B ) )
= ( B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(121,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( A != B )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ C )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ ( transi1302705790_state @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_converse__rtranclE) ).
thf(777,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( A != B )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ C )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ ( transi1302705790_state @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(76,axiom,
! [A: state > $o,B: com,C: list_com,D: state,E: list_com,F: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ E @ F ) ) @ pHoare259243666_exec1 )
=> ( ( ( E = C )
=> ( ( F = D )
=> ( A @ D ) ) )
=> ~ ( ( E
= ( cons_com @ B @ ( cons_com @ ( while @ A @ B ) @ C ) ) )
=> ( ( F = D )
=> ~ ( A @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_exec1E_I5_J) ).
thf(523,plain,
! [A: state > $o,B: com,C: list_com,D: state,E: list_com,F: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ E @ F ) ) @ pHoare259243666_exec1 )
=> ( ( ( E = C )
=> ( ( F = D )
=> ( A @ D ) ) )
=> ~ ( ( E
= ( cons_com @ B @ ( cons_com @ ( while @ A @ B ) @ C ) ) )
=> ( ( F = D )
=> ~ ( A @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(102,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ ( transi1302705790_state @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_rtrancl__trans) ).
thf(683,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ ( transi1302705790_state @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(8,axiom,
! [A: list_com,B: list_com] :
( ( A != B )
=> ( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ? [C: list_com,D: com,E: list_com,F: com,G: list_com] :
( ( D != F )
& ( A
= ( append_com @ C @ ( append_com @ ( cons_com @ D @ nil_com ) @ E ) ) )
& ( B
= ( append_com @ C @ ( append_com @ ( cons_com @ F @ nil_com ) @ G ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_331_same__length__different) ).
thf(202,plain,
! [A: list_com,B: list_com] :
( ( A != B )
=> ( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ? [C: list_com,D: com,E: list_com,F: com,G: list_com] :
( ( D != F )
& ( A
= ( append_com @ C @ ( append_com @ ( cons_com @ D @ nil_com ) @ E ) ) )
& ( B
= ( append_com @ C @ ( append_com @ ( cons_com @ F @ nil_com ) @ G ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(78,axiom,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state,F: list_com > state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ A @ B )
=> ( ! [G: list_com,H: state,I: list_com,J: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ G @ H ) ) @ ( transi1302705790_state @ E ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ G @ H ) @ ( produc1204172211_state @ I @ J ) ) @ E )
=> ( ( F @ G @ H )
=> ( F @ I @ J ) ) ) )
=> ( F @ C @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_rtrancl__induct2) ).
thf(550,plain,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state,F: list_com > state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ A @ B )
=> ( ! [G: list_com,H: state,I: list_com,J: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ G @ H ) ) @ ( transi1302705790_state @ E ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ G @ H ) @ ( produc1204172211_state @ I @ J ) ) @ E )
=> ( ( F @ G @ H )
=> ( F @ I @ J ) ) ) )
=> ( F @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(110,axiom,
! [A: list_com,B: com,C: list_com] :
( ( A
= ( cons_com @ B @ C ) )
=> ( A != nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_list_OdiscI) ).
thf(715,plain,
! [A: list_com,B: com,C: list_com] :
( ( A
= ( cons_com @ B @ C ) )
=> ( A != nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(150,axiom,
! [A: ( com > com ) > list_com > list_com > $o,B: com > com,C: list_com,D: list_com] :
( ! [E: com > com,F: list_com] : ( A @ E @ nil_com @ F )
=> ( ! [E: com > com,F: com,G: list_com,H: list_com] :
( ( A @ E @ G @ ( cons_com @ ( E @ F ) @ H ) )
=> ( A @ E @ ( cons_com @ F @ G ) @ H ) )
=> ( A @ B @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_map__tailrec__rev_Oinduct) ).
thf(913,plain,
! [A: ( com > com ) > list_com > list_com > $o,B: com > com,C: list_com,D: list_com] :
( ! [E: com > com,F: list_com] : ( A @ E @ nil_com @ F )
=> ( ! [E: com > com,F: com,G: list_com,H: list_com] :
( ( A @ E @ G @ ( cons_com @ ( E @ F ) @ H ) )
=> ( A @ E @ ( cons_com @ F @ G ) @ H ) )
=> ( A @ B @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(28,axiom,
! [A: com,B: list_com,C: list_com,D: list_com,E: list_com] :
( ( ( cons_com @ A @ B )
= C )
=> ( ( D
= ( append_com @ B @ E ) )
=> ( ( cons_com @ A @ D )
= ( append_com @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_Cons__eq__appendI) ).
thf(288,plain,
! [A: com,B: list_com,C: list_com,D: list_com,E: list_com] :
( ( ( cons_com @ A @ B )
= C )
=> ( ( D
= ( append_com @ B @ E ) )
=> ( ( cons_com @ A @ D )
= ( append_com @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(36,axiom,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= B )
= ( A = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_append__self__conv2) ).
thf(320,plain,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= B )
= ( A = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(96,axiom,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ( A @ nil_com @ nil_com )
=> ( ! [D: com,E: list_com] : ( A @ ( cons_com @ D @ E ) @ nil_com )
=> ( ! [D: com,E: list_com] : ( A @ nil_com @ ( cons_com @ D @ E ) )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( A @ E @ G )
=> ( A @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) )
=> ( A @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_list__induct2_H) ).
thf(651,plain,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ( A @ nil_com @ nil_com )
=> ( ! [D: com,E: list_com] : ( A @ ( cons_com @ D @ E ) @ nil_com )
=> ( ! [D: com,E: list_com] : ( A @ nil_com @ ( cons_com @ D @ E ) )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( A @ E @ G )
=> ( A @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) )
=> ( A @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(123,axiom,
! [A: list_com] :
( ( A != nil_com )
=> ( ! [B: com] :
( A
!= ( cons_com @ B @ nil_com ) )
=> ~ ! [B: com,C: com,D: list_com] :
( A
!= ( cons_com @ B @ ( cons_com @ C @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_remdups__adj_Ocases) ).
thf(785,plain,
! [A: list_com] :
( ( A != nil_com )
=> ( ! [B: com] :
( A
!= ( cons_com @ B @ nil_com ) )
=> ~ ! [B: com,C: com,D: list_com] :
( A
!= ( cons_com @ B @ ( cons_com @ C @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(6,axiom,
! [A: list_com,B: list_com] :
( ( A
= ( append_com @ A @ B ) )
= ( B = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_self__append__conv) ).
thf(196,plain,
! [A: list_com,B: list_com] :
( ( A
= ( append_com @ A @ B ) )
= ( B = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(147,axiom,
! [A: state > $o,B: state,C: com,D: list_com] :
( ~ ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ C ) @ D ) @ B ) @ ( produc1204172211_state @ D @ B ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_exec1_OWhileFalse) ).
thf(902,plain,
! [A: state > $o,B: state,C: com,D: list_com] :
( ~ ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ C ) @ D ) @ B ) @ ( produc1204172211_state @ D @ B ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(80,axiom,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: produc2041926651_state] : ( A @ ( produc1909270103_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_old_Oprod_Oinducts) ).
thf(559,plain,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: produc2041926651_state] : ( A @ ( produc1909270103_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(92,axiom,
! [A: list_com] :
( ( A != nil_com )
= ( ? [B: com,C: list_com] :
( A
= ( cons_com @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_neq__Nil__conv) ).
thf(638,plain,
! [A: list_com] :
( ( A != nil_com )
= ( ? [B: com,C: list_com] :
( A
= ( cons_com @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(61,axiom,
! [A: produc2041926651_state > $o,B: produc2041926651_state] :
( ! [C: list_com,D: state] : ( A @ ( produc1204172211_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_old_Oprod_Oinducts) ).
thf(421,plain,
! [A: produc2041926651_state > $o,B: produc2041926651_state] :
( ! [C: list_com,D: state] : ( A @ ( produc1204172211_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(22,axiom,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
| ( ( size_size_list_com @ C )
= ( size_size_list_com @ D ) ) )
=> ( ( ( append_com @ A @ C )
= ( append_com @ B @ D ) )
= ( ( A = B )
& ( C = D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_328_append__eq__append__conv) ).
thf(261,plain,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
| ( ( size_size_list_com @ C )
= ( size_size_list_com @ D ) ) )
=> ( ( ( append_com @ A @ C )
= ( append_com @ B @ D ) )
= ( ( A = B )
& ( C = D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(11,axiom,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc410756839_state] :
( A
!= ( produc2065881943_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_old_Oprod_Oexhaust) ).
thf(216,plain,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc410756839_state] :
( A
!= ( produc2065881943_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(124,axiom,
! [A: state > $o,B: com,C: com,D: state > $o,E: com,F: com] :
( ( ( cond @ A @ B @ C )
= ( cond @ D @ E @ F ) )
= ( ( A = D )
& ( B = E )
& ( C = F ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_com_Oinject_I3_J) ).
thf(789,plain,
! [A: state > $o,B: com,C: com,D: state > $o,E: com,F: com] :
( ( ( cond @ A @ B @ C )
= ( cond @ D @ E @ F ) )
= ( ( A = D )
& ( B = E )
& ( C = F ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(1,conjecture,
termi @ c2 @ s2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3) ).
thf(2,negated_conjecture,
~ ( termi @ c2 @ s2 ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(179,plain,
~ ( termi @ c2 @ s2 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(53,axiom,
! [A: state > $o,B: com,C: com,D: state > $o,E: com] :
( ( cond @ A @ B @ C )
!= ( while @ D @ E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_com_Odistinct_I19_J) ).
thf(376,plain,
! [A: state > $o,B: com,C: com,D: state > $o,E: com] :
( ( cond @ A @ B @ C )
!= ( while @ D @ E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(88,axiom,
! [A: state > set_state,B: com,C: com] :
( ( do @ A )
!= ( semi @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_com_Odistinct_I1_J) ).
thf(623,plain,
! [A: state > set_state,B: com,C: com] :
( ( do @ A )
!= ( semi @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(9,axiom,
( ( butlast_com @ nil_com )
= nil_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_282_butlast_Osimps_I1_J) ).
thf(211,plain,
( ( butlast_com @ nil_com )
= nil_com ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(172,axiom,
! [A: state > $o,B: com,C: state,D: state] :
( ( termi @ ( while @ A @ B ) @ C )
=> ( ( A @ C )
=> ( ( exec @ C @ B @ D )
=> ( termi @ ( while @ A @ B ) @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_while__termiE2) ).
thf(1020,plain,
! [A: state > $o,B: com,C: state,D: state] :
( ( termi @ ( while @ A @ B ) @ C )
=> ( ( A @ C )
=> ( ( exec @ C @ B @ D )
=> ( termi @ ( while @ A @ B ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(46,axiom,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= nil_com )
= ( ( A = nil_com )
& ( B = nil_com ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_append__is__Nil__conv) ).
thf(353,plain,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= nil_com )
= ( ( A = nil_com )
& ( B = nil_com ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(148,axiom,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( ( produc1204172211_state @ A @ B )
!= ( produc1204172211_state @ C @ D ) )
=> ~ ! [F: list_com,G: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ F @ G ) ) @ E )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ F @ G ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_converse__rtranclE2) ).
thf(905,plain,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( ( produc1204172211_state @ A @ B )
!= ( produc1204172211_state @ C @ D ) )
=> ~ ! [F: list_com,G: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ F @ G ) ) @ E )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ F @ G ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(141,axiom,
! [A: list_com,B: nat,C: com] :
( ( ( list_update_com @ A @ B @ C )
= nil_com )
= ( A = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_353_list__update__nonempty) ).
thf(877,plain,
! [A: list_com,B: nat,C: com] :
( ( ( list_update_com @ A @ B @ C )
= nil_com )
= ( A = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(113,axiom,
! [A: ( com > com > $o ) > list_com > $o,B: com > com > $o,C: list_com] :
( ! [D: com > com > $o] : ( A @ D @ nil_com )
=> ( ! [D: com > com > $o,E: com] : ( A @ D @ ( cons_com @ E @ nil_com ) )
=> ( ! [D: com > com > $o,E: com,F: com,G: list_com] :
( ( A @ D @ ( cons_com @ F @ G ) )
=> ( A @ D @ ( cons_com @ E @ ( cons_com @ F @ G ) ) ) )
=> ( A @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_successively_Oinduct) ).
thf(734,plain,
! [A: ( com > com > $o ) > list_com > $o,B: com > com > $o,C: list_com] :
( ! [D: com > com > $o] : ( A @ D @ nil_com )
=> ( ! [D: com > com > $o,E: com] : ( A @ D @ ( cons_com @ E @ nil_com ) )
=> ( ! [D: com > com > $o,E: com,F: com,G: list_com] :
( ( A @ D @ ( cons_com @ F @ G ) )
=> ( A @ D @ ( cons_com @ E @ ( cons_com @ F @ G ) ) ) )
=> ( A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(29,axiom,
! [A: list_com,B: com] :
( ( last_com @ ( append_com @ A @ ( cons_com @ B @ nil_com ) ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_301_last__snoc) ).
thf(293,plain,
! [A: list_com,B: com] :
( ( last_com @ ( append_com @ A @ ( cons_com @ B @ nil_com ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(18,axiom,
! [A: list_com,B: list_com] :
( ( ( A = nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ B ) ) )
& ( ( A != nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_306_last__append) ).
thf(243,plain,
! [A: list_com,B: list_com] :
( ( ( A = nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ B ) ) )
& ( ( A != nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(152,axiom,
! [A: com > $o] :
~ ( list_ex1_com @ A @ nil_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_338_list__ex1__simps_I1_J) ).
thf(920,plain,
! [A: com > $o] :
~ ( list_ex1_com @ A @ nil_com ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(54,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
= ( ? [D: produc2041926651_state] :
( ( A = D )
& ( B = D ) )
| ? [D: produc2041926651_state,E: produc2041926651_state,F: produc2041926651_state] :
( ( A = D )
& ( B = F )
& ( member1069318160_state @ ( produc1909270103_state @ D @ E ) @ ( transi1302705790_state @ C ) )
& ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_rtrancl_Osimps) ).
thf(380,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
= ( ? [D: produc2041926651_state] :
( ( A = D )
& ( B = D ) )
| ? [D: produc2041926651_state,E: produc2041926651_state,F: produc2041926651_state] :
( ( A = D )
& ( B = F )
& ( member1069318160_state @ ( produc1909270103_state @ D @ E ) @ ( transi1302705790_state @ C ) )
& ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(101,axiom,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ! [D: list_com] : ( A @ nil_com @ D )
=> ( ! [D: com,E: list_com,F: list_com] :
( ( A @ F @ E )
=> ( A @ ( cons_com @ D @ E ) @ F ) )
=> ( A @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_splice_Oinduct) ).
thf(678,plain,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ! [D: list_com] : ( A @ nil_com @ D )
=> ( ! [D: com,E: list_com,F: list_com] :
( ( A @ F @ E )
=> ( A @ ( cons_com @ D @ E ) @ F ) )
=> ( A @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(24,axiom,
! [A: list_com] :
( ( append_com @ A @ nil_com )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_append__Nil2) ).
thf(270,plain,
! [A: list_com] :
( ( append_com @ A @ nil_com )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(77,axiom,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc2041926651_state,D: list_com,E: state] :
( A
!= ( produc2065881943_state @ B @ ( produc1909270103_state @ C @ ( produc1204172211_state @ D @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_prod__cases4) ).
thf(546,plain,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc2041926651_state,D: list_com,E: state] :
( A
!= ( produc2065881943_state @ B @ ( produc1909270103_state @ C @ ( produc1204172211_state @ D @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(118,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ C )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_rtrancl_Ortrancl__into__rtrancl) ).
thf(761,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ C )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(12,axiom,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc410756839_state] : ( A @ ( produc2065881943_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_prod__cases) ).
thf(220,plain,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc410756839_state] : ( A @ ( produc2065881943_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(32,axiom,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_prod_Oinject) ).
thf(302,plain,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(57,axiom,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_prod_Oinject) ).
thf(392,plain,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(90,axiom,
! [A: state > set_state,B: list_com,C: state,D: list_com,E: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( do @ A ) @ B ) @ C ) @ ( produc1204172211_state @ D @ E ) ) @ pHoare259243666_exec1 )
=> ~ ( ( D = B )
=> ~ ( member_state @ E @ ( A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_exec1E_I2_J) ).
thf(630,plain,
! [A: state > set_state,B: list_com,C: state,D: list_com,E: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( do @ A ) @ B ) @ C ) @ ( produc1204172211_state @ D @ E ) ) @ pHoare259243666_exec1 )
=> ~ ( ( D = B )
=> ~ ( member_state @ E @ ( A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(26,axiom,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc2041926651_state,D: produc2041926651_state] :
( A
!= ( produc2065881943_state @ B @ ( produc1909270103_state @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_prod__cases3) ).
thf(275,plain,
! [A: produc186437863_state] :
~ ! [B: produc410756839_state,C: produc2041926651_state,D: produc2041926651_state] :
( A
!= ( produc2065881943_state @ B @ ( produc1909270103_state @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(127,axiom,
! [A: com,B: list_com] :
( nil_com
!= ( cons_com @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_list_Odistinct_I1_J) ).
thf(815,plain,
! [A: com,B: list_com] :
( nil_com
!= ( cons_com @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(82,axiom,
! [A: list_com,B: state,C: list_com,D: state,E: list_com] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( append_com @ A @ E ) @ B ) @ ( produc1204172211_state @ ( append_com @ C @ E ) @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_app__execs) ).
thf(566,plain,
! [A: list_com,B: state,C: list_com,D: state,E: list_com] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( append_com @ A @ E ) @ B ) @ ( produc1204172211_state @ ( append_com @ C @ E ) @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(19,axiom,
! [A: list_com,B: list_com,C: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ A @ C ) )
= ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_same__append__eq) ).
thf(252,plain,
! [A: list_com,B: list_com,C: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ A @ C ) )
= ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(48,axiom,
! [A: produc186437863_state] :
? [B: produc410756839_state,C: produc410756839_state] :
( A
= ( produc2065881943_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_surj__pair) ).
thf(361,plain,
! [A: produc186437863_state] :
? [B: produc410756839_state,C: produc410756839_state] :
( A
= ( produc2065881943_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(98,axiom,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ! [D: list_com] : ( A @ nil_com @ D )
=> ( ! [D: list_com] : ( A @ D @ nil_com )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( A @ E @ ( cons_com @ F @ G ) )
=> ( ( A @ ( cons_com @ D @ E ) @ G )
=> ( A @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) ) )
=> ( A @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_shuffles_Oinduct) ).
thf(665,plain,
! [A: list_com > list_com > $o,B: list_com,C: list_com] :
( ! [D: list_com] : ( A @ nil_com @ D )
=> ( ! [D: list_com] : ( A @ D @ nil_com )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( A @ E @ ( cons_com @ F @ G ) )
=> ( ( A @ ( cons_com @ D @ E ) @ G )
=> ( A @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) ) )
=> ( A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(134,axiom,
! [A: state,B: com,C: state,D: list_com,E: state] :
( ( exec @ A @ B @ C )
=> ( ( pHoare259243732_execs @ C @ D @ E )
=> ( pHoare259243732_execs @ A @ ( cons_com @ B @ D ) @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_execs_Ointros_I2_J) ).
thf(842,plain,
! [A: state,B: com,C: state,D: list_com,E: state] :
( ( exec @ A @ B @ C )
=> ( ( pHoare259243732_execs @ C @ D @ E )
=> ( pHoare259243732_execs @ A @ ( cons_com @ B @ D ) @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(115,axiom,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com,D: list_com] :
( ( A @ D )
=> ( A @ ( append_com @ D @ ( cons_com @ C @ nil_com ) ) ) )
=> ( A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_rev__induct) ).
thf(742,plain,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com,D: list_com] :
( ( A @ D )
=> ( A @ ( append_com @ D @ ( cons_com @ C @ nil_com ) ) ) )
=> ( A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(140,axiom,
! [A: produc410756839_state] :
? [B: produc2041926651_state,C: produc2041926651_state] :
( A
= ( produc1909270103_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_surj__pair) ).
thf(874,plain,
! [A: produc410756839_state] :
? [B: produc2041926651_state,C: produc2041926651_state] :
( A
= ( produc1909270103_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(35,axiom,
! [A: com > list_com,B: com,C: list_com] :
( ( maps_com_com @ A @ ( cons_com @ B @ C ) )
= ( append_com @ ( A @ B ) @ ( maps_com_com @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_maps__simps_I1_J) ).
thf(317,plain,
! [A: com > list_com,B: com,C: list_com] :
( ( maps_com_com @ A @ ( cons_com @ B @ C ) )
= ( append_com @ ( A @ B ) @ ( maps_com_com @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(167,axiom,
! [A: list_com,B: state,C: list_com,D: state,E: list_com] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ pHoare259243666_exec1 )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( append_com @ A @ E ) @ B ) @ ( produc1204172211_state @ ( append_com @ C @ E ) @ D ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_app__exec) ).
thf(1006,plain,
! [A: list_com,B: state,C: list_com,D: state,E: list_com] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ pHoare259243666_exec1 )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( append_com @ A @ E ) @ B ) @ ( produc1204172211_state @ ( append_com @ C @ E ) @ D ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(56,axiom,
! [A: com,B: com,C: state > $o,D: com,E: com] :
( ( semi @ A @ B )
!= ( cond @ C @ D @ E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_com_Odistinct_I11_J) ).
thf(388,plain,
! [A: com,B: com,C: state > $o,D: com,E: com] :
( ( semi @ A @ B )
!= ( cond @ C @ D @ E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(47,axiom,
! [A: list_com,B: list_com,C: list_com,D: list_com,E: list_com] :
( ( ( append_com @ A @ B )
= C )
=> ( ( D
= ( append_com @ B @ E ) )
=> ( ( append_com @ A @ D )
= ( append_com @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_append__eq__appendI) ).
thf(356,plain,
! [A: list_com,B: list_com,C: list_com,D: list_com,E: list_com] :
( ( ( append_com @ A @ B )
= C )
=> ( ( D
= ( append_com @ B @ E ) )
=> ( ( append_com @ A @ D )
= ( append_com @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(122,axiom,
! [A: com,B: com,C: list_com,D: state] : ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( semi @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ ( cons_com @ A @ ( cons_com @ B @ C ) ) @ D ) ) @ pHoare259243666_exec1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_exec1_OSemi) ).
thf(783,plain,
! [A: com,B: com,C: list_com,D: state] : ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( semi @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ ( cons_com @ A @ ( cons_com @ B @ C ) ) @ D ) ) @ pHoare259243666_exec1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(143,axiom,
! [A: com,B: list_com,C: list_com,D: list_com] :
( ( ( cons_com @ A @ B )
= ( append_com @ C @ D ) )
= ( ( ( C = nil_com )
& ( ( cons_com @ A @ B )
= D ) )
| ? [E: list_com] :
( ( ( cons_com @ A @ E )
= C )
& ( B
= ( append_com @ E @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_Cons__eq__append__conv) ).
thf(884,plain,
! [A: com,B: list_com,C: list_com,D: list_com] :
( ( ( cons_com @ A @ B )
= ( append_com @ C @ D ) )
= ( ( ( C = nil_com )
& ( ( cons_com @ A @ B )
= D ) )
| ? [E: list_com] :
( ( ( cons_com @ A @ E )
= C )
& ( B
= ( append_com @ E @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(174,axiom,
! [A: state > $o,B: state,C: com] :
( ~ ( A @ B )
=> ( termi @ ( while @ A @ C ) @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_termi_OWhileFalse) ).
thf(1028,plain,
! [A: state > $o,B: state,C: com] :
( ~ ( A @ B )
=> ( termi @ ( while @ A @ C ) @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(13,axiom,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc2041926651_state,E: produc2041926651_state] : ( A @ ( produc2065881943_state @ C @ ( produc1909270103_state @ D @ E ) ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_prod__induct3) ).
thf(225,plain,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc2041926651_state,E: produc2041926651_state] : ( A @ ( produc2065881943_state @ C @ ( produc1909270103_state @ D @ E ) ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(41,axiom,
! [A: com > com > $o,B: list_com,C: com > com > $o,D: list_com] :
( ( ( produc1914379986st_com @ A @ B )
= ( produc1914379986st_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_prod_Oinject) ).
thf(339,plain,
! [A: com > com > $o,B: list_com,C: com > com > $o,D: list_com] :
( ( ( produc1914379986st_com @ A @ B )
= ( produc1914379986st_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(116,axiom,
! [A: ( com > com > $o ) > list_com > $o,B: com > com > $o,C: list_com] :
( ! [D: com > com > $o] : ( A @ D @ nil_com )
=> ( ! [D: com > com > $o,E: com,F: list_com] :
( ( A @ D @ F )
=> ( A @ D @ ( cons_com @ E @ F ) ) )
=> ( A @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_sorted__wrt_Oinduct) ).
thf(753,plain,
! [A: ( com > com > $o ) > list_com > $o,B: com > com > $o,C: list_com] :
( ! [D: com > com > $o] : ( A @ D @ nil_com )
=> ( ! [D: com > com > $o,E: com,F: list_com] :
( ( A @ D @ F )
=> ( A @ D @ ( cons_com @ E @ F ) ) )
=> ( A @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(103,axiom,
! [A: list_com,B: list_com,C: com,D: list_com] :
( ( ( append_com @ A @ B )
= ( cons_com @ C @ D ) )
= ( ( ( A = nil_com )
& ( B
= ( cons_com @ C @ D ) ) )
| ? [E: list_com] :
( ( A
= ( cons_com @ C @ E ) )
& ( ( append_com @ E @ B )
= D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_append__eq__Cons__conv) ).
thf(686,plain,
! [A: list_com,B: list_com,C: com,D: list_com] :
( ( ( append_com @ A @ B )
= ( cons_com @ C @ D ) )
= ( ( ( A = nil_com )
& ( B
= ( cons_com @ C @ D ) ) )
| ? [E: list_com] :
( ( A
= ( cons_com @ C @ E ) )
& ( ( append_com @ E @ B )
= D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(170,axiom,
! [A: com,B: list_com,C: state] :
( ( pHoare806997636termis @ ( cons_com @ A @ B ) @ C )
= ( ( termi @ A @ C )
& ! [D: state] :
( ( exec @ C @ A @ D )
=> ( pHoare806997636termis @ B @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_termis_Osimps_I2_J) ).
thf(1016,plain,
! [A: com,B: list_com,C: state] :
( ( pHoare806997636termis @ ( cons_com @ A @ B ) @ C )
= ( ( termi @ A @ C )
& ! [D: state] :
( ( exec @ C @ A @ D )
=> ( pHoare806997636termis @ B @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(108,axiom,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: produc2041926651_state] : ( A @ ( produc1909270103_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_prod__cases) ).
thf(706,plain,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: produc2041926651_state] : ( A @ ( produc1909270103_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(38,axiom,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ C @ D ) )
= ( ? [E: list_com] :
( ( ( A
= ( append_com @ C @ E ) )
& ( ( append_com @ E @ B )
= D ) )
| ( ( ( append_com @ A @ E )
= C )
& ( B
= ( append_com @ E @ D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_append__eq__append__conv2) ).
thf(328,plain,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ C @ D ) )
= ( ? [E: list_com] :
( ( ( A
= ( append_com @ C @ E ) )
& ( ( append_com @ E @ B )
= D ) )
| ( ( ( append_com @ A @ E )
= C )
& ( B
= ( append_com @ E @ D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(67,axiom,
! [A: produc2041926651_state,B: set_Pr1165141447_state] : ( member1069318160_state @ ( produc1909270103_state @ A @ A ) @ ( transi1302705790_state @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_rtrancl_Ortrancl__refl) ).
thf(471,plain,
! [A: produc2041926651_state,B: set_Pr1165141447_state] : ( member1069318160_state @ ( produc1909270103_state @ A @ A ) @ ( transi1302705790_state @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(178,axiom,
! [A: state > $o,B: state,C: com,D: com] :
( ( A @ B )
=> ( ( termi @ C @ B )
=> ( termi @ ( cond @ A @ C @ D ) @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_termi_OIfTrue) ).
thf(1039,plain,
! [A: state > $o,B: state,C: com,D: com] :
( ( A @ B )
=> ( ( termi @ C @ B )
=> ( termi @ ( cond @ A @ C @ D ) @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(160,axiom,
! [A: list_com,B: list_com > $o] :
( ( A != nil_com )
=> ( ! [C: com] : ( B @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: list_com] :
( ( D != nil_com )
=> ( ( B @ D )
=> ( B @ ( append_com @ D @ ( cons_com @ C @ nil_com ) ) ) ) )
=> ( B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_rev__nonempty__induct) ).
thf(970,plain,
! [A: list_com,B: list_com > $o] :
( ( A != nil_com )
=> ( ! [C: com] : ( B @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: list_com] :
( ( D != nil_com )
=> ( ( B @ D )
=> ( B @ ( append_com @ D @ ( cons_com @ C @ nil_com ) ) ) ) )
=> ( B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(161,axiom,
! [A: list_com,B: state,C: list_com,D: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ pHoare259243666_exec1 )
=> ( ( pHoare806997636termis @ A @ B )
=> ( pHoare806997636termis @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_exec1__pres__termis) ).
thf(985,plain,
! [A: list_com,B: state,C: list_com,D: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ pHoare259243666_exec1 )
=> ( ( pHoare806997636termis @ A @ B )
=> ( pHoare806997636termis @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(149,axiom,
( pHoare259243732_execs
= ( ^ [A: state,B: list_com,C: state] :
( ? [D: state] :
( ( A = D )
& ( B = nil_com )
& ( C = D ) )
| ? [D: state,E: com,F: state,G: list_com,H: state] :
( ( A = D )
& ( B
= ( cons_com @ E @ G ) )
& ( C = H )
& ( exec @ D @ E @ F )
& ( pHoare259243732_execs @ F @ G @ H ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_execs_Osimps) ).
thf(911,plain,
( pHoare259243732_execs
= ( ^ [A: state,B: list_com,C: state] :
( ? [D: state] :
( ( A = D )
& ( B = nil_com )
& ( C = D ) )
| ? [D: state,E: com,F: state,G: list_com,H: state] :
( ( A = D )
& ( B
= ( cons_com @ E @ G ) )
& ( C = H )
& ( exec @ D @ E @ F )
& ( pHoare259243732_execs @ F @ G @ H ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(166,axiom,
! [A: list_com] :
( ( A != nil_com )
=> ~ ! [B: list_com,C: com] :
( A
!= ( append_com @ B @ ( cons_com @ C @ nil_com ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_rev__exhaust) ).
thf(1002,plain,
! [A: list_com] :
( ( A != nil_com )
=> ~ ! [B: list_com,C: com] :
( A
!= ( append_com @ B @ ( cons_com @ C @ nil_com ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(83,axiom,
! [A: list_com,B: com] :
( ( A != nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= ( last_com @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_302_last__ConsR) ).
thf(569,plain,
! [A: list_com,B: com] :
( ( A != nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= ( last_com @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(51,axiom,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_old_Oprod_Oinject) ).
thf(371,plain,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(16,axiom,
! [A: list_com,B: list_com,C: list_com] :
( ( append_com @ ( append_com @ A @ B ) @ C )
= ( append_com @ A @ ( append_com @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_append_Oassoc) ).
thf(237,plain,
! [A: list_com,B: list_com,C: list_com] :
( ( append_com @ ( append_com @ A @ B ) @ C )
= ( append_com @ A @ ( append_com @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(125,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ! [E: produc2041926651_state] : ( D @ E @ E )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state,G: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ E @ F )
=> ( ( member1069318160_state @ ( produc1909270103_state @ F @ G ) @ C )
=> ( D @ E @ G ) ) ) )
=> ( D @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_rtrancl_Oinducts) ).
thf(792,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ! [E: produc2041926651_state] : ( D @ E @ E )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state,G: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ E @ F )
=> ( ( member1069318160_state @ ( produc1909270103_state @ F @ G ) @ C )
=> ( D @ E @ G ) ) ) )
=> ( D @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(156,axiom,
! [A: set_Pr1165141447_state] :
( ( collec300063826_state
@ ^ [B: produc410756839_state] : ( member1069318160_state @ B @ A ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_Collect__mem__eq) ).
thf(938,plain,
! [A: set_Pr1165141447_state] :
( ( collec300063826_state
@ ^ [B: produc410756839_state] : ( member1069318160_state @ B @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(120,axiom,
! [A: state > set_state,B: state > $o,C: com,D: com] :
( ( do @ A )
!= ( cond @ B @ C @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_com_Odistinct_I3_J) ).
thf(773,plain,
! [A: state > set_state,B: state > $o,C: com,D: com] :
( ( do @ A )
!= ( cond @ B @ C @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(97,axiom,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_old_Oprod_Oinject) ).
thf(662,plain,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(154,axiom,
! [A: list_com,B: com] :
( ( ( A = nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= B ) )
& ( ( A != nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= ( last_com @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_304_last_Osimps) ).
thf(926,plain,
! [A: list_com,B: com] :
( ( ( A = nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= B ) )
& ( ( A != nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= ( last_com @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(130,axiom,
! [A: list_com] :
( ( ( rotate1_com @ A )
= nil_com )
= ( A = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_277_rotate1__is__Nil__conv) ).
thf(824,plain,
! [A: list_com] :
( ( ( rotate1_com @ A )
= nil_com )
= ( A = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(27,axiom,
! [A: list_com,B: list_com] :
? [C: list_com,D: list_com,E: list_com] :
( ( A
= ( append_com @ D @ C ) )
& ( B
= ( append_com @ E @ C ) )
& ( ( D = nil_com )
| ( E = nil_com )
| ( ( last_com @ D )
!= ( last_com @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_305_longest__common__suffix) ).
thf(279,plain,
! [A: list_com,B: list_com] :
? [C: list_com,D: list_com,E: list_com] :
( ( A
= ( append_com @ D @ C ) )
& ( B
= ( append_com @ E @ C ) )
& ( ( D = nil_com )
| ( E = nil_com )
| ( ( last_com @ D )
!= ( last_com @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(84,axiom,
! [A: state > $o,B: state,C: com,D: state,E: com] :
( ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( exec @ B @ ( cond @ A @ C @ E ) @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_exec_OIfTrue) ).
thf(573,plain,
! [A: state > $o,B: state,C: com,D: state,E: com] :
( ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( exec @ B @ ( cond @ A @ C @ E ) @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(64,axiom,
! [A: state,B: list_com,C: state,D: state > list_com > state > $o] :
( ( pHoare259243732_execs @ A @ B @ C )
=> ( ! [E: state] : ( D @ E @ nil_com @ E )
=> ( ! [E: state,F: com,G: state,H: list_com,I: state] :
( ( exec @ E @ F @ G )
=> ( ( pHoare259243732_execs @ G @ H @ I )
=> ( ( D @ G @ H @ I )
=> ( D @ E @ ( cons_com @ F @ H ) @ I ) ) ) )
=> ( D @ A @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_execs_Oinducts) ).
thf(444,plain,
! [A: state,B: list_com,C: state,D: state > list_com > state > $o] :
( ( pHoare259243732_execs @ A @ B @ C )
=> ( ! [E: state] : ( D @ E @ nil_com @ E )
=> ( ! [E: state,F: com,G: state,H: list_com,I: state] :
( ( exec @ E @ F @ G )
=> ( ( pHoare259243732_execs @ G @ H @ I )
=> ( ( D @ G @ H @ I )
=> ( D @ E @ ( cons_com @ F @ H ) @ I ) ) ) )
=> ( D @ A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(73,axiom,
! [A: state > $o,B: state,C: com,D: com,E: list_com] :
( ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ C @ D ) @ E ) @ B ) @ ( produc1204172211_state @ ( cons_com @ C @ E ) @ B ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_exec1_OIfTrue) ).
thf(513,plain,
! [A: state > $o,B: state,C: com,D: com,E: list_com] :
( ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ C @ D ) @ E ) @ B ) @ ( produc1204172211_state @ ( cons_com @ C @ E ) @ B ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(63,axiom,
! [A: state,B: list_com,C: state] :
( ( pHoare259243732_execs @ A @ B @ C )
=> ( ( ( B = nil_com )
=> ( C != A ) )
=> ~ ! [D: com,E: state,F: list_com] :
( ( B
= ( cons_com @ D @ F ) )
=> ( ( exec @ A @ D @ E )
=> ~ ( pHoare259243732_execs @ E @ F @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_execs_Ocases) ).
thf(430,plain,
! [A: state,B: list_com,C: state] :
( ( pHoare259243732_execs @ A @ B @ C )
=> ( ( ( B = nil_com )
=> ( C != A ) )
=> ~ ! [D: com,E: state,F: list_com] :
( ( B
= ( cons_com @ D @ F ) )
=> ( ( exec @ A @ D @ E )
=> ~ ( pHoare259243732_execs @ E @ F @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(3,axiom,
! [A: list_com] :
( ( A != nil_com )
=> ( ( append_com @ ( butlast_com @ A ) @ ( cons_com @ ( last_com @ A ) @ nil_com ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_297_append__butlast__last__id) ).
thf(180,plain,
! [A: list_com] :
( ( A != nil_com )
=> ( ( append_com @ ( butlast_com @ A ) @ ( cons_com @ ( last_com @ A ) @ nil_com ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(104,axiom,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state,F: list_com > state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ C @ D )
=> ( ! [G: list_com,H: state,I: list_com,J: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ G @ H ) @ ( produc1204172211_state @ I @ J ) ) @ E )
=> ( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ I @ J ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ I @ J )
=> ( F @ G @ H ) ) ) )
=> ( F @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_converse__rtrancl__induct2) ).
thf(689,plain,
! [A: list_com,B: state,C: list_com,D: state,E: set_Pr1165141447_state,F: list_com > state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ C @ D )
=> ( ! [G: list_com,H: state,I: list_com,J: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ G @ H ) @ ( produc1204172211_state @ I @ J ) ) @ E )
=> ( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ I @ J ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ E ) )
=> ( ( F @ I @ J )
=> ( F @ G @ H ) ) ) )
=> ( F @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(30,axiom,
! [A: list_com] :
( ( append_com @ nil_com @ A )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_append_Oleft__neutral) ).
thf(296,plain,
! [A: list_com] :
( ( append_com @ nil_com @ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(128,axiom,
! [A: produc2041926651_state] :
? [B: list_com,C: state] :
( A
= ( produc1204172211_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_surj__pair) ).
thf(819,plain,
! [A: produc2041926651_state] :
? [B: list_com,C: state] :
( A
= ( produc1204172211_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(109,axiom,
! [A: produc258871771st_com] :
( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ nil_com @ B ) )
=> ( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ B @ nil_com ) )
=> ~ ! [B: com,C: list_com,D: com,E: list_com] :
( A
!= ( produc1307105171st_com @ ( cons_com @ B @ C ) @ ( cons_com @ D @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_shuffles_Ocases) ).
thf(711,plain,
! [A: produc258871771st_com] :
( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ nil_com @ B ) )
=> ( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ B @ nil_com ) )
=> ~ ! [B: com,C: list_com,D: com,E: list_com] :
( A
!= ( produc1307105171st_com @ ( cons_com @ B @ C ) @ ( cons_com @ D @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(93,axiom,
! [A: com,B: com,C: com,D: com] :
( ( ( semi @ A @ B )
= ( semi @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_com_Oinject_I2_J) ).
thf(641,plain,
! [A: com,B: com,C: com,D: com] :
( ( ( semi @ A @ B )
= ( semi @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(66,axiom,
! [A: produc2041926651_state > $o,B: produc2041926651_state] :
( ! [C: list_com,D: state] : ( A @ ( produc1204172211_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_prod__cases) ).
thf(466,plain,
! [A: produc2041926651_state > $o,B: produc2041926651_state] :
( ! [C: list_com,D: state] : ( A @ ( produc1204172211_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(45,axiom,
! [A: list_com,B: com] :
( ( butlast_com @ ( append_com @ A @ ( cons_com @ B @ nil_com ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_276_butlast__snoc) ).
thf(350,plain,
! [A: list_com,B: com] :
( ( butlast_com @ ( append_com @ A @ ( cons_com @ B @ nil_com ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(169,axiom,
! [A: com,B: state,C: com] :
( ( termi @ A @ B )
=> ( ! [D: state] :
( ( exec @ B @ A @ D )
=> ( termi @ C @ D ) )
=> ( termi @ ( semi @ A @ C ) @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_termi_OSemi) ).
thf(1011,plain,
! [A: com,B: state,C: com] :
( ( termi @ A @ B )
=> ( ! [D: state] :
( ( exec @ B @ A @ D )
=> ( termi @ C @ D ) )
=> ( termi @ ( semi @ A @ C ) @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(164,axiom,
! [A: state > $o,B: state,C: com,D: state,E: com] :
( ~ ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( exec @ B @ ( cond @ A @ E @ C ) @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_exec_OIfFalse) ).
thf(996,plain,
! [A: state > $o,B: state,C: com,D: state,E: com] :
( ~ ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( exec @ B @ ( cond @ A @ E @ C ) @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(14,axiom,
! [A: list_com,B: list_com] :
( ( A = B )
=> ( A
= ( append_com @ nil_com @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_eq__Nil__appendI) ).
thf(230,plain,
! [A: list_com,B: list_com] :
( ( A = B )
=> ( A
= ( append_com @ nil_com @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(65,axiom,
! [A: list_com,B: list_com > $o] :
( ( A != nil_com )
=> ( ! [C: com] : ( B @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: list_com] :
( ( D != nil_com )
=> ( ( B @ D )
=> ( B @ ( cons_com @ C @ D ) ) ) )
=> ( B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_list__nonempty__induct) ).
thf(451,plain,
! [A: list_com,B: list_com > $o] :
( ( A != nil_com )
=> ( ! [C: com] : ( B @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: list_com] :
( ( D != nil_com )
=> ( ( B @ D )
=> ( B @ ( cons_com @ C @ D ) ) ) )
=> ( B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(119,axiom,
! [A: list_com,B: com] :
( ( ( A = nil_com )
=> ( ( butlast_com @ ( cons_com @ B @ A ) )
= nil_com ) )
& ( ( A != nil_com )
=> ( ( butlast_com @ ( cons_com @ B @ A ) )
= ( cons_com @ B @ ( butlast_com @ A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_288_butlast_Osimps_I2_J) ).
thf(764,plain,
! [A: list_com,B: com] :
( ( ( A = nil_com )
=> ( ( butlast_com @ ( cons_com @ B @ A ) )
= nil_com ) )
& ( ( A != nil_com )
=> ( ( butlast_com @ ( cons_com @ B @ A ) )
= ( cons_com @ B @ ( butlast_com @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(87,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ B )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C )
=> ( ( member1069318160_state @ ( produc1909270103_state @ F @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ F )
=> ( D @ E ) ) ) )
=> ( D @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_converse__rtrancl__induct) ).
thf(604,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ B )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C )
=> ( ( member1069318160_state @ ( produc1909270103_state @ F @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ F )
=> ( D @ E ) ) ) )
=> ( D @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(72,axiom,
! [A: produc2041926651_state] :
~ ! [B: list_com,C: state] :
( A
!= ( produc1204172211_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_old_Oprod_Oexhaust) ).
thf(509,plain,
! [A: produc2041926651_state] :
~ ! [B: list_com,C: state] :
( A
!= ( produc1204172211_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(142,axiom,
! [A: com,B: com,C: state > $o,D: com] :
( ( semi @ A @ B )
!= ( while @ C @ D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_com_Odistinct_I13_J) ).
thf(880,plain,
! [A: com,B: com,C: state > $o,D: com] :
( ( semi @ A @ B )
!= ( while @ C @ D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(145,axiom,
! [A: state] : ( pHoare806997636termis @ nil_com @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_termis_Osimps_I1_J) ).
thf(890,plain,
! [A: state] : ( pHoare806997636termis @ nil_com @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(126,axiom,
! [A: produc410756839_state] :
~ ! [B: produc2041926651_state,C: produc2041926651_state] :
( A
!= ( produc1909270103_state @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_old_Oprod_Oexhaust) ).
thf(811,plain,
! [A: produc410756839_state] :
~ ! [B: produc2041926651_state,C: produc2041926651_state] :
( A
!= ( produc1909270103_state @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(117,axiom,
! [A: com > list_com] :
( ( bind_com_com @ nil_com @ A )
= nil_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_bind__simps_I1_J) ).
thf(758,plain,
! [A: com > list_com] :
( ( bind_com_com @ nil_com @ A )
= nil_com ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(37,axiom,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc410756839_state] : ( A @ ( produc2065881943_state @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_old_Oprod_Oinducts) ).
thf(323,plain,
! [A: produc186437863_state > $o,B: produc186437863_state] :
( ! [C: produc410756839_state,D: produc410756839_state] : ( A @ ( produc2065881943_state @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(10,axiom,
! [A: list_com,B: com,C: list_com] :
( ( ( append_com @ A @ ( cons_com @ B @ nil_com ) )
= C )
= ( ( C != nil_com )
& ( ( butlast_com @ C )
= A )
& ( ( last_com @ C )
= B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_298_snoc__eq__iff__butlast) ).
thf(213,plain,
! [A: list_com,B: com,C: list_com] :
( ( ( append_com @ A @ ( cons_com @ B @ nil_com ) )
= C )
= ( ( C != nil_com )
& ( ( butlast_com @ C )
= A )
& ( ( last_com @ C )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(69,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ A )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ E ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C )
=> ( ( D @ E )
=> ( D @ F ) ) ) )
=> ( D @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_rtrancl__induct) ).
thf(483,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state > $o] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( D @ A )
=> ( ! [E: produc2041926651_state,F: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ E ) @ ( transi1302705790_state @ C ) )
=> ( ( member1069318160_state @ ( produc1909270103_state @ E @ F ) @ C )
=> ( ( D @ E )
=> ( D @ F ) ) ) )
=> ( D @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(17,axiom,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( produc1307105171st_com @ A @ B )
= ( produc1307105171st_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_prod_Oinject) ).
thf(240,plain,
! [A: list_com,B: list_com,C: list_com,D: list_com] :
( ( ( produc1307105171st_com @ A @ B )
= ( produc1307105171st_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(43,axiom,
! [A: state] : ( pHoare259243732_execs @ A @ nil_com @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_execs_Ointros_I1_J) ).
thf(345,plain,
! [A: state] : ( pHoare259243732_execs @ A @ nil_com @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(50,axiom,
! [A: list_com,B: list_com] :
( ( A != nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_299_last__appendR) ).
thf(367,plain,
! [A: list_com,B: list_com] :
( ( A != nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(136,axiom,
! [A: state,B: state > set_state,C: state,D: list_com] :
( ( member_state @ A @ ( B @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( do @ B ) @ D ) @ C ) @ ( produc1204172211_state @ D @ A ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_exec1_ODo) ).
thf(848,plain,
! [A: state,B: state > set_state,C: state,D: list_com] :
( ( member_state @ A @ ( B @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( do @ B ) @ D ) @ C ) @ ( produc1204172211_state @ D @ A ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(106,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_prod_Oinject) ).
thf(700,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(75,axiom,
! [A: state > $o,B: state,C: com] :
( ~ ( A @ B )
=> ( exec @ B @ ( while @ A @ C ) @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_exec_OWhileFalse) ).
thf(520,plain,
! [A: state > $o,B: state,C: com] :
( ~ ( A @ B )
=> ( exec @ B @ ( while @ A @ C ) @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(159,axiom,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com,D: list_com] :
( ( A @ D )
=> ( A @ ( cons_com @ C @ D ) ) )
=> ( A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_list_Oinducts) ).
thf(959,plain,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com,D: list_com] :
( ( A @ D )
=> ( A @ ( cons_com @ C @ D ) ) )
=> ( A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(131,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( B != A )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_rtrancl_Ocases) ).
thf(827,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( B != A )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(31,axiom,
! [A: list_com,B: list_com,C: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ C @ B ) )
= ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_append__same__eq) ).
thf(299,plain,
! [A: list_com,B: list_com,C: list_com] :
( ( ( append_com @ A @ B )
= ( append_com @ C @ B ) )
= ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(71,axiom,
! [A: com,B: list_com] :
( ( cons_com @ A @ B )
!= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_not__Cons__self2) ).
thf(505,plain,
! [A: com,B: list_com] :
( ( cons_com @ A @ B )
!= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(23,axiom,
! [A: com,B: list_com,C: com > list_com] :
( ( bind_com_com @ ( cons_com @ A @ B ) @ C )
= ( append_com @ ( C @ A ) @ ( bind_com_com @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_bind__simps_I2_J) ).
thf(267,plain,
! [A: com,B: list_com,C: com > list_com] :
( ( bind_com_com @ ( cons_com @ A @ B ) @ C )
= ( append_com @ ( C @ A ) @ ( bind_com_com @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(137,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ C )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ ( transi1302705790_state @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_converse__rtrancl__into__rtrancl) ).
thf(851,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state,D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ C )
=> ( ( member1069318160_state @ ( produc1909270103_state @ B @ D ) @ ( transi1302705790_state @ C ) )
=> ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(68,axiom,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_Pair__inject) ).
thf(473,plain,
! [A: list_com,B: state,C: list_com,D: state] :
( ( ( produc1204172211_state @ A @ B )
= ( produc1204172211_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(176,axiom,
! [A: state,B: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ c @ nil_com ) @ A ) @ ( produc1204172211_state @ ( cons_com @ c2 @ cs ) @ B ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( ( termi @ c @ A )
=> ( ( termi @ c2 @ B )
& ! [C: state] :
( ( exec @ B @ c2 @ C )
=> ( pHoare806997636termis @ cs @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2) ).
thf(1034,plain,
! [A: state,B: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ c @ nil_com ) @ A ) @ ( produc1204172211_state @ ( cons_com @ c2 @ cs ) @ B ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( ( termi @ c @ A )
=> ( ( termi @ c2 @ B )
& ! [C: state] :
( ( exec @ B @ c2 @ C )
=> ( pHoare806997636termis @ cs @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(100,axiom,
! [A: state > $o,B: com,C: state > $o,D: com] :
( ( ( while @ A @ B )
= ( while @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_com_Oinject_I4_J) ).
thf(675,plain,
! [A: state > $o,B: com,C: state > $o,D: com] :
( ( ( while @ A @ B )
= ( while @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(62,axiom,
! [A: list_com] :
( ( A != nil_com )
=> ~ ! [B: com,C: list_com] :
( A
!= ( cons_com @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_list_Oexhaust) ).
thf(426,plain,
! [A: list_com] :
( ( A != nil_com )
=> ~ ! [B: com,C: list_com] :
( A
!= ( cons_com @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(158,axiom,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com] : ( A @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: com,E: list_com] :
( ( A @ E )
=> ( ( A @ ( cons_com @ D @ E ) )
=> ( A @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) )
=> ( A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_induct__list012) ).
thf(944,plain,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com] : ( A @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: com,E: list_com] :
( ( A @ E )
=> ( ( A @ ( cons_com @ D @ E ) )
=> ( A @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) )
=> ( A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(52,axiom,
! [A: com,B: state,C: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ A @ nil_com ) @ B ) @ ( produc1204172211_state @ nil_com @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( exec @ B @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_exec1s__impl__exec) ).
thf(374,plain,
! [A: com,B: state,C: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ A @ nil_com ) @ B ) @ ( produc1204172211_state @ nil_com @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( exec @ B @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(20,axiom,
! [A: state > set_state,B: state > set_state] :
( ( ( do @ A )
= ( do @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_com_Oinject_I1_J) ).
thf(255,plain,
! [A: state > set_state,B: state > set_state] :
( ( ( do @ A )
= ( do @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(95,axiom,
! [A: set_Pr1165141447_state] :
( ! [B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ B @ B ) @ A )
=> ( irrefl654089520_state @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_307_irreflI) ).
thf(648,plain,
! [A: set_Pr1165141447_state] :
( ! [B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ B @ B ) @ A )
=> ( irrefl654089520_state @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(74,axiom,
! [A: produc410756839_state] :
~ ! [B: produc2041926651_state,C: list_com,D: state] :
( A
!= ( produc1909270103_state @ B @ ( produc1204172211_state @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_prod__cases3) ).
thf(516,plain,
! [A: produc410756839_state] :
~ ! [B: produc2041926651_state,C: list_com,D: state] :
( A
!= ( produc1909270103_state @ B @ ( produc1204172211_state @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(42,axiom,
! [A: com,B: list_com,C: list_com] :
( ( append_com @ ( cons_com @ A @ B ) @ C )
= ( cons_com @ A @ ( append_com @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_append__Cons) ).
thf(342,plain,
! [A: com,B: list_com,C: list_com] :
( ( append_com @ ( cons_com @ A @ B ) @ C )
= ( cons_com @ A @ ( append_com @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(79,axiom,
( ( rotate1_com @ nil_com )
= nil_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_283_rotate1_Osimps_I1_J) ).
thf(557,plain,
( ( rotate1_com @ nil_com )
= nil_com ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(139,axiom,
( irrefl654089520_state
= ( ^ [A: set_Pr1165141447_state] :
! [B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ B @ B ) @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_309_irrefl__def) ).
thf(872,plain,
( irrefl654089520_state
= ( ^ [A: set_Pr1165141447_state] :
! [B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ B @ B ) @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(144,axiom,
! [A: state > $o,B: state,C: com,D: state,E: state] :
( ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( ( exec @ D @ ( while @ A @ C ) @ E )
=> ( exec @ B @ ( while @ A @ C ) @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_exec_OWhileTrue) ).
thf(887,plain,
! [A: state > $o,B: state,C: com,D: state,E: state] :
( ( A @ B )
=> ( ( exec @ B @ C @ D )
=> ( ( exec @ D @ ( while @ A @ C ) @ E )
=> ( exec @ B @ ( while @ A @ C ) @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(114,axiom,
! [A: produc2041926651_state,B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( measur1071343867_state @ nil_Pr1876916290te_nat ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_344_in__measures_I1_J) ).
thf(739,plain,
! [A: produc2041926651_state,B: produc2041926651_state] :
~ ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( measur1071343867_state @ nil_Pr1876916290te_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(7,axiom,
! [A: list_com,B: list_com] :
( ( nil_com
= ( append_com @ A @ B ) )
= ( ( A = nil_com )
& ( B = nil_com ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_Nil__is__append__conv) ).
thf(199,plain,
! [A: list_com,B: list_com] :
( ( nil_com
= ( append_com @ A @ B ) )
= ( ( A = nil_com )
& ( B = nil_com ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(39,axiom,
! [A: list_com,B: list_com] :
( ( A = nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_300_last__appendL) ).
thf(331,plain,
! [A: list_com,B: list_com] :
( ( A = nil_com )
=> ( ( last_com @ ( append_com @ B @ A ) )
= ( last_com @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(177,axiom,
termi @ c @ s,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
thf(1038,plain,
termi @ c @ s,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(70,axiom,
! [A: com] :
( ( insert_com @ A @ nil_com )
= ( cons_com @ A @ nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_insert__Nil) ).
thf(502,plain,
! [A: com] :
( ( insert_com @ A @ nil_com )
= ( cons_com @ A @ nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(85,axiom,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: list_com,E: state] : ( A @ ( produc1909270103_state @ C @ ( produc1204172211_state @ D @ E ) ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_prod__induct3) ).
thf(576,plain,
! [A: produc410756839_state > $o,B: produc410756839_state] :
( ! [C: produc2041926651_state,D: list_com,E: state] : ( A @ ( produc1909270103_state @ C @ ( produc1204172211_state @ D @ E ) ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(40,axiom,
! [A: list_com,B: list_com,C: list_com] :
( ( append_com @ ( append_com @ A @ B ) @ C )
= ( append_com @ A @ ( append_com @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_append__assoc) ).
thf(336,plain,
! [A: list_com,B: list_com,C: list_com] :
( ( append_com @ ( append_com @ A @ B ) @ C )
= ( append_com @ A @ ( append_com @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(107,axiom,
! [A: state,B: list_com,C: state] :
~ ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ nil_com @ A ) @ ( produc1204172211_state @ B @ C ) ) @ pHoare259243666_exec1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_exec1E_I1_J) ).
thf(703,plain,
! [A: state,B: list_com,C: state] :
~ ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ nil_com @ A ) @ ( produc1204172211_state @ B @ C ) ) @ pHoare259243666_exec1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(173,axiom,
! [A: state > $o,B: state,C: com] :
( ( A @ B )
=> ( ( termi @ C @ B )
=> ( ! [D: state] :
( ( exec @ B @ C @ D )
=> ( termi @ ( while @ A @ C ) @ D ) )
=> ( termi @ ( while @ A @ C ) @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_termi_OWhileTrue) ).
thf(1023,plain,
! [A: state > $o,B: state,C: com] :
( ( A @ B )
=> ( ( termi @ C @ B )
=> ( ! [D: state] :
( ( exec @ B @ C @ D )
=> ( termi @ ( while @ A @ C ) @ D ) )
=> ( termi @ ( while @ A @ C ) @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(34,axiom,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= A )
= ( B = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_append__self__conv) ).
thf(314,plain,
! [A: list_com,B: list_com] :
( ( ( append_com @ A @ B )
= A )
= ( B = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(135,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_old_Oprod_Oinject) ).
thf(845,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: produc2041926651_state,D: produc2041926651_state] :
( ( ( produc1909270103_state @ A @ B )
= ( produc1909270103_state @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(89,axiom,
! [A: com > list_com] :
( ( maps_com_com @ A @ nil_com )
= nil_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_maps__simps_I2_J) ).
thf(627,plain,
! [A: com > list_com] :
( ( maps_com_com @ A @ nil_com )
= nil_com ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(99,axiom,
! [A: produc258871771st_com] :
( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ nil_com @ B ) )
=> ~ ! [B: com,C: list_com,D: list_com] :
( A
!= ( produc1307105171st_com @ ( cons_com @ B @ C ) @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_splice_Ocases) ).
thf(671,plain,
! [A: produc258871771st_com] :
( ! [B: list_com] :
( A
!= ( produc1307105171st_com @ nil_com @ B ) )
=> ~ ! [B: com,C: list_com,D: list_com] :
( A
!= ( produc1307105171st_com @ ( cons_com @ B @ C ) @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(86,axiom,
! [A: state > $o,B: com,C: com,D: list_com,E: state,F: list_com,G: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ B @ C ) @ D ) @ E ) @ ( produc1204172211_state @ F @ G ) ) @ pHoare259243666_exec1 )
=> ( ( ( F
= ( cons_com @ B @ D ) )
=> ( ( G = E )
=> ~ ( A @ E ) ) )
=> ~ ( ( F
= ( cons_com @ C @ D ) )
=> ( ( G = E )
=> ( A @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_exec1E_I4_J) ).
thf(581,plain,
! [A: state > $o,B: com,C: com,D: list_com,E: state,F: list_com,G: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ B @ C ) @ D ) @ E ) @ ( produc1204172211_state @ F @ G ) ) @ pHoare259243666_exec1 )
=> ( ( ( F
= ( cons_com @ B @ D ) )
=> ( ( G = E )
=> ~ ( A @ E ) ) )
=> ~ ( ( F
= ( cons_com @ C @ D ) )
=> ( ( G = E )
=> ( A @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(21,axiom,
! [A: list_com] :
( ( append_com @ A @ nil_com )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_append_Oright__neutral) ).
thf(258,plain,
! [A: list_com] :
( ( append_com @ A @ nil_com )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(5,axiom,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Pair__inject) ).
thf(186,plain,
! [A: produc410756839_state,B: produc410756839_state,C: produc410756839_state,D: produc410756839_state] :
( ( ( produc2065881943_state @ A @ B )
= ( produc2065881943_state @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(59,axiom,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com] : ( A @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: com,E: list_com] :
( ( ( C = D )
=> ( A @ ( cons_com @ C @ E ) ) )
=> ( ( ( C != D )
=> ( A @ ( cons_com @ D @ E ) ) )
=> ( A @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) )
=> ( A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_remdups__adj_Oinduct) ).
thf(401,plain,
! [A: list_com > $o,B: list_com] :
( ( A @ nil_com )
=> ( ! [C: com] : ( A @ ( cons_com @ C @ nil_com ) )
=> ( ! [C: com,D: com,E: list_com] :
( ( ( C = D )
=> ( A @ ( cons_com @ C @ E ) ) )
=> ( ( ( C != D )
=> ( A @ ( cons_com @ D @ E ) ) )
=> ( A @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) )
=> ( A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(60,axiom,
! [A: com,B: list_com,C: com,D: list_com] :
( ( ( cons_com @ A @ B )
= ( cons_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_list_Oinject) ).
thf(418,plain,
! [A: com,B: list_com,C: com,D: list_com] :
( ( ( cons_com @ A @ B )
= ( cons_com @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(165,axiom,
! [A: set_Pr1165141447_state] :
( ( transi1302705790_state @ ( transi1302705790_state @ A ) )
= ( transi1302705790_state @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_rtrancl__idemp) ).
thf(999,plain,
! [A: set_Pr1165141447_state] :
( ( transi1302705790_state @ ( transi1302705790_state @ A ) )
= ( transi1302705790_state @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(132,axiom,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( A != B )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_rtranclE) ).
thf(833,plain,
! [A: produc2041926651_state,B: produc2041926651_state,C: set_Pr1165141447_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ B ) @ ( transi1302705790_state @ C ) )
=> ( ( A != B )
=> ~ ! [D: produc2041926651_state] :
( ( member1069318160_state @ ( produc1909270103_state @ A @ D ) @ ( transi1302705790_state @ C ) )
=> ~ ( member1069318160_state @ ( produc1909270103_state @ D @ B ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(138,axiom,
! [A: list_com,B: list_com,C: list_com > list_com > $o] :
( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ( ( C @ nil_com @ nil_com )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( ( size_size_list_com @ E )
= ( size_size_list_com @ G ) )
=> ( ( C @ E @ G )
=> ( C @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) ) )
=> ( C @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_330_list__induct2) ).
thf(854,plain,
! [A: list_com,B: list_com,C: list_com > list_com > $o] :
( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ( ( C @ nil_com @ nil_com )
=> ( ! [D: com,E: list_com,F: com,G: list_com] :
( ( ( size_size_list_com @ E )
= ( size_size_list_com @ G ) )
=> ( ( C @ E @ G )
=> ( C @ ( cons_com @ D @ E ) @ ( cons_com @ F @ G ) ) ) )
=> ( C @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(4,axiom,
! [A: list_com,B: list_com] :
( ( A
= ( append_com @ B @ A ) )
= ( B = nil_com ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_self__append__conv2) ).
thf(183,plain,
! [A: list_com,B: list_com] :
( ( A
= ( append_com @ B @ A ) )
= ( B = nil_com ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(25,axiom,
! [A: state,B: state > set_state,C: state] :
( ( member_state @ A @ ( B @ C ) )
=> ( exec @ C @ ( do @ B ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_exec_ODo) ).
thf(273,plain,
! [A: state,B: state > set_state,C: state] :
( ( member_state @ A @ ( B @ C ) )
=> ( exec @ C @ ( do @ B ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(81,axiom,
! [A: list_com,B: state,C: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ nil_com @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( pHoare259243732_execs @ B @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_exec1s__impl__execs) ).
thf(564,plain,
! [A: list_com,B: state,C: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ nil_com @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( pHoare259243732_execs @ B @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(33,axiom,
! [A: list_com,B: list_com] :
( ( ( A = nil_com )
=> ( ( butlast_com @ ( append_com @ B @ A ) )
= ( butlast_com @ B ) ) )
& ( ( A != nil_com )
=> ( ( butlast_com @ ( append_com @ B @ A ) )
= ( append_com @ B @ ( butlast_com @ A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_290_butlast__append) ).
thf(305,plain,
! [A: list_com,B: list_com] :
( ( ( A = nil_com )
=> ( ( butlast_com @ ( append_com @ B @ A ) )
= ( butlast_com @ B ) ) )
& ( ( A != nil_com )
=> ( ( butlast_com @ ( append_com @ B @ A ) )
= ( append_com @ B @ ( butlast_com @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(151,axiom,
! [A: list_com,B: state,C: list_com,D: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( ( pHoare806997636termis @ A @ B )
=> ( pHoare806997636termis @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_execs__pres__termis) ).
thf(918,plain,
! [A: list_com,B: state,C: list_com,D: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ A @ B ) @ ( produc1204172211_state @ C @ D ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) )
=> ( ( pHoare806997636termis @ A @ B )
=> ( pHoare806997636termis @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(91,axiom,
! [A: state > $o,B: state,C: com,D: list_com] :
( ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ C ) @ D ) @ B ) @ ( produc1204172211_state @ ( cons_com @ C @ ( cons_com @ ( while @ A @ C ) @ D ) ) @ B ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_exec1_OWhileTrue) ).
thf(635,plain,
! [A: state > $o,B: state,C: com,D: list_com] :
( ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( while @ A @ C ) @ D ) @ B ) @ ( produc1204172211_state @ ( cons_com @ C @ ( cons_com @ ( while @ A @ C ) @ D ) ) @ B ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(105,axiom,
! [A: produc2058209240st_com] :
( ! [B: com > com > $o] :
( A
!= ( produc1914379986st_com @ B @ nil_com ) )
=> ( ! [B: com > com > $o,C: com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ nil_com ) ) )
=> ~ ! [B: com > com > $o,C: com,D: com,E: list_com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_successively_Ocases) ).
thf(696,plain,
! [A: produc2058209240st_com] :
( ! [B: com > com > $o] :
( A
!= ( produc1914379986st_com @ B @ nil_com ) )
=> ( ! [B: com > com > $o,C: com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ nil_com ) ) )
=> ~ ! [B: com > com > $o,C: com,D: com,E: list_com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ ( cons_com @ D @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(111,axiom,
! [A: state > $o,B: state,C: com,D: com,E: list_com] :
( ~ ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ C @ D ) @ E ) @ B ) @ ( produc1204172211_state @ ( cons_com @ D @ E ) @ B ) ) @ pHoare259243666_exec1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_exec1_OIfFalse) ).
thf(720,plain,
! [A: state > $o,B: state,C: com,D: com,E: list_com] :
( ~ ( A @ B )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( cond @ A @ C @ D ) @ E ) @ B ) @ ( produc1204172211_state @ ( cons_com @ D @ E ) @ B ) ) @ pHoare259243666_exec1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(162,axiom,
! [A: list_com,B: com] :
( ( A = nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_303_last__ConsL) ).
thf(987,plain,
! [A: list_com,B: com] :
( ( A = nil_com )
=> ( ( last_com @ ( cons_com @ B @ A ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(171,axiom,
member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ c @ nil_com ) @ s ) @ ( produc1204172211_state @ ( cons_com @ c2 @ cs ) @ s2 ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(1019,plain,
member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ c @ nil_com ) @ s ) @ ( produc1204172211_state @ ( cons_com @ c2 @ cs ) @ s2 ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(94,axiom,
! [A: state > set_state,B: state > $o,C: com] :
( ( do @ A )
!= ( while @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_com_Odistinct_I5_J) ).
thf(644,plain,
! [A: state > set_state,B: state > $o,C: com] :
( ( do @ A )
!= ( while @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(163,axiom,
! [A: produc2058209240st_com] :
( ! [B: com > com > $o] :
( A
!= ( produc1914379986st_com @ B @ nil_com ) )
=> ~ ! [B: com > com > $o,C: com,D: list_com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_sorted__wrt_Ocases) ).
thf(992,plain,
! [A: produc2058209240st_com] :
( ! [B: com > com > $o] :
( A
!= ( produc1914379986st_com @ B @ nil_com ) )
=> ~ ! [B: com > com > $o,C: com,D: list_com] :
( A
!= ( produc1914379986st_com @ B @ ( cons_com @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(112,axiom,
! [A: list_com,B: list_com,C: list_com,D: list_com > list_com > list_com > $o] :
( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ( ( ( size_size_list_com @ B )
= ( size_size_list_com @ C ) )
=> ( ( D @ nil_com @ nil_com @ nil_com )
=> ( ! [E: com,F: list_com,G: com,H: list_com,I: com,J: list_com] :
( ( ( size_size_list_com @ F )
= ( size_size_list_com @ H ) )
=> ( ( ( size_size_list_com @ H )
= ( size_size_list_com @ J ) )
=> ( ( D @ F @ H @ J )
=> ( D @ ( cons_com @ E @ F ) @ ( cons_com @ G @ H ) @ ( cons_com @ I @ J ) ) ) ) )
=> ( D @ A @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_329_list__induct3) ).
thf(723,plain,
! [A: list_com,B: list_com,C: list_com,D: list_com > list_com > list_com > $o] :
( ( ( size_size_list_com @ A )
= ( size_size_list_com @ B ) )
=> ( ( ( size_size_list_com @ B )
= ( size_size_list_com @ C ) )
=> ( ( D @ nil_com @ nil_com @ nil_com )
=> ( ! [E: com,F: list_com,G: com,H: list_com,I: com,J: list_com] :
( ( ( size_size_list_com @ F )
= ( size_size_list_com @ H ) )
=> ( ( ( size_size_list_com @ H )
= ( size_size_list_com @ J ) )
=> ( ( D @ F @ H @ J )
=> ( D @ ( cons_com @ E @ F ) @ ( cons_com @ G @ H ) @ ( cons_com @ I @ J ) ) ) ) )
=> ( D @ A @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(129,axiom,
! [A: produc410756839_state,B: set_Pr1165141447_state] :
( ( member1069318160_state @ A @ B )
=> ( member1069318160_state @ A @ ( transi1302705790_state @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_r__into__rtrancl) ).
thf(822,plain,
! [A: produc410756839_state,B: set_Pr1165141447_state] :
( ( member1069318160_state @ A @ B )
=> ( member1069318160_state @ A @ ( transi1302705790_state @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(58,axiom,
! [A: com,B: com,C: list_com,D: state,E: list_com,F: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( semi @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ E @ F ) ) @ pHoare259243666_exec1 )
=> ~ ( ( E
= ( cons_com @ A @ ( cons_com @ B @ C ) ) )
=> ( F != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_exec1E_I3_J) ).
thf(395,plain,
! [A: com,B: com,C: list_com,D: state,E: list_com,F: state] :
( ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ ( semi @ A @ B ) @ C ) @ D ) @ ( produc1204172211_state @ E @ F ) ) @ pHoare259243666_exec1 )
=> ~ ( ( E
= ( cons_com @ A @ ( cons_com @ B @ C ) ) )
=> ( F != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(133,axiom,
! [A: state,B: com,C: state,D: com,E: state] :
( ( exec @ A @ B @ C )
=> ( ( exec @ C @ D @ E )
=> ( exec @ A @ ( semi @ B @ D ) @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_exec_OSemi) ).
thf(839,plain,
! [A: state,B: com,C: state,D: com,E: state] :
( ( exec @ A @ B @ C )
=> ( ( exec @ C @ D @ E )
=> ( exec @ A @ ( semi @ B @ D ) @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(153,axiom,
! [A: state,B: com,C: state,D: list_com] :
( ( exec @ A @ B @ C )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ B @ D ) @ A ) @ ( produc1204172211_state @ D @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_exec__impl__execs) ).
thf(923,plain,
! [A: state,B: com,C: state,D: list_com] :
( ( exec @ A @ B @ C )
=> ( member1069318160_state @ ( produc1909270103_state @ ( produc1204172211_state @ ( cons_com @ B @ D ) @ A ) @ ( produc1204172211_state @ D @ C ) ) @ ( transi1302705790_state @ pHoare259243666_exec1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(49,axiom,
! [A: list_com,B: com,C: list_com] :
( ( nth_com @ ( append_com @ A @ ( cons_com @ B @ C ) ) @ ( size_size_list_com @ A ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_346_nth__append__length) ).
thf(364,plain,
! [A: list_com,B: com,C: list_com] :
( ( nth_com @ ( append_com @ A @ ( cons_com @ B @ C ) ) @ ( size_size_list_com @ A ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(155,axiom,
! [A: list_com,B: com,C: list_com,D: com] :
( ( ( append_com @ A @ ( cons_com @ B @ nil_com ) )
= ( append_com @ C @ ( cons_com @ D @ nil_com ) ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_append1__eq__conv) ).
thf(935,plain,
! [A: list_com,B: com,C: list_com,D: com] :
( ( ( append_com @ A @ ( cons_com @ B @ nil_com ) )
= ( append_com @ C @ ( cons_com @ D @ nil_com ) ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(168,axiom,
! [A: state > $o,B: com,C: state] :
( ( termi @ ( while @ A @ B ) @ C )
=> ( ( A @ C )
=> ( termi @ B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_while__termiE) ).
thf(1009,plain,
! [A: state > $o,B: com,C: state] :
( ( termi @ ( while @ A @ B ) @ C )
=> ( ( A @ C )
=> ( termi @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(1049,plain,
$false,
inference(e,[status(thm)],[383,892,347,1031,234,941,777,523,683,202,550,715,913,288,320,651,785,196,902,559,638,421,261,216,789,179,376,623,211,1020,353,905,877,734,293,243,920,380,678,270,546,761,220,302,392,630,275,815,566,252,361,665,842,742,874,317,1006,388,356,783,884,1028,225,339,753,686,1016,706,328,471,1039,970,985,911,1002,569,371,237,792,938,773,662,926,824,279,573,444,513,430,180,689,296,819,711,641,466,350,1011,996,230,451,764,604,509,880,890,811,758,323,213,483,240,345,367,848,700,520,959,827,299,505,267,851,473,1034,675,426,944,374,255,648,516,342,557,872,887,739,199,331,1038,502,576,336,703,1023,314,845,627,671,581,258,186,401,418,999,833,854,183,273,564,305,918,635,696,720,987,1019,644,992,723,822,395,839,923,364,935,1009]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP142^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20 % Computer : n018.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 20:01:56 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.53/1.23 % [INFO] Parsing done (437ms).
% 2.53/1.25 % [INFO] Running in sequential loop mode.
% 3.82/1.62 % [INFO] eprover registered as external prover.
% 3.82/1.63 % [INFO] Scanning for conjecture ...
% 4.28/1.81 % [INFO] Found a conjecture (or negated_conjecture) and 357 axioms. Running axiom selection ...
% 4.53/1.96 % [INFO] Axiom selection finished. Selected 176 axioms (removed 181 axioms).
% 5.56/2.21 % [INFO] Problem is higher-order (TPTP THF).
% 5.56/2.24 % [INFO] Type checking passed.
% 5.56/2.24 % [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 ...
% 18.35/5.03 % External prover 'e' found a proof!
% 18.35/5.03 % [INFO] Killing All external provers ...
% 18.35/5.03 % Time passed: 4690ms (effective reasoning time: 3781ms)
% 18.35/5.03 % 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)>
% 18.35/5.04 % Axioms used in derivation (176): fact_172_insert__Nil, fact_70_old_Oprod_Oinducts, fact_157_termi_OWhileFalse, fact_65_sorted__wrt_Ocases, fact_127_rtrancl_Osimps, fact_94_mem__Collect__eq, fact_188_append_Oright__neutral, fact_275_rotate1_Osimps_I2_J, fact_304_last_Osimps, fact_202_append__eq__Cons__conv, fact_187_append__is__Nil__conv, fact_68_execs_Ointros_I1_J, fact_203_rev__nonempty__induct, fact_141_exec1_OIfTrue, fact_5_exec1__pres__termis, fact_93_shuffles_Oinduct, fact_303_last__ConsL, fact_166_com_Odistinct_I3_J, fact_234_maps__simps_I1_J, fact_71_old_Oprod_Oinducts, fact_149_termi_OWhileTrue, fact_75_Pair__inject, fact_87_list__nonempty__induct, fact_84_not__Cons__self2, fact_101_splice_Oinduct, fact_307_irreflI, fact_22_converse__rtranclE2, fact_131_rtranclE, fact_150_com_Oinject_I2_J, fact_81_surj__pair, fact_168_com_Odistinct_I1_J, fact_140_exec1_OIfFalse, fact_192_append__Cons, fact_85_execs_Ointros_I2_J, fact_194_append_Oleft__neutral, fact_67_splice_Ocases, fact_146_while__termiE2, fact_31_exec1s__impl__execs, fact_301_last__snoc, fact_167_com_Odistinct_I11_J, fact_135_prod__induct3, fact_89_remdups__adj_Oinduct, fact_180_same__append__eq, fact_136_exec1_OSemi, fact_302_last__ConsR, fact_76_Pair__inject, fact_72_old_Oprod_Oexhaust, fact_288_butlast_Osimps_I2_J, fact_200_rev__exhaust, fact_300_last__appendL, fact_54_prod_Oinject, fact_297_append__butlast__last__id, fact_113_rtrancl_Ortrancl__into__rtrancl, fact_276_butlast__snoc, fact_159_exec_OIfFalse, fact_282_butlast_Osimps_I1_J, fact_153_com_Oinject_I4_J, fact_57_prod_Oinject, fact_123_rtrancl__induct, fact_181_append__Nil2, fact_195_append__Nil, fact_328_append__eq__append__conv, fact_58_old_Oprod_Oinject, fact_298_snoc__eq__iff__butlast, fact_56_prod_Oinject, fact_185_self__append__conv2, fact_142_exec1E_I4_J, fact_104_list_Oinducts, fact_125_rtrancl__trans, fact_133_prod__induct4, fact_106_list_OdiscI, fact_162_exec_ODo, fact_111_converse__rtrancl__into__rtrancl, fact_186_Nil__is__append__conv, fact_305_longest__common__suffix, conj_2, fact_137_exec1E_I3_J, fact_139_exec1E_I2_J, fact_102_list__induct2_H, fact_63_prod__cases4, fact_6_execs__pres__termis, fact_338_list__ex1__simps_I1_J, fact_155_exec_OWhileTrue, fact_306_last__append, fact_37_rtrancl__idemp, fact_4_exec1s__impl__exec, fact_199_rev__induct, fact_236_bind__simps_I1_J, fact_51_list_Oinject, fact_230_bind__simps_I2_J, fact_66_shuffles_Ocases, fact_109_execs_Osimps, fact_105_list_Oexhaust, fact_83_surj__pair, fact_156_com_Odistinct_I19_J, fact_183_self__append__conv, fact_177_append_Oassoc, fact_151_com_Oinject_I1_J, fact_250_maps__simps_I2_J, fact_59_old_Oprod_Oinject, fact_2_termis_Osimps_I1_J, fact_115_converse__rtrancl__induct, fact_0_exec1E_I1_J, fact_88_successively_Oinduct, fact_77_Pair__inject, fact_184_append__self__conv2, fact_344_in__measures_I1_J, fact_62_prod__cases3, fact_78_prod__cases, fact_290_butlast__append, fact_60_old_Oprod_Oinject, fact_179_append__same__eq, fact_90_sorted__wrt_Oinduct, fact_86_map__tailrec__rev_Oinduct, fact_61_prod__cases3, fact_1_termis_Osimps_I2_J, fact_108_execs_Oinducts, fact_163_exec_OSemi, fact_103_neq__Nil__conv, fact_91_remdups__adj_Ocases, fact_160_exec_OIfTrue, fact_201_Cons__eq__append__conv, fact_161_com_Odistinct_I13_J, fact_299_last__appendR, fact_69_old_Oprod_Oinducts, conj_1, fact_148_termi_OSemi, fact_178_append__assoc, fact_138_exec1_ODo, fact_119_converse__rtranclE, fact_3_exec__impl__execs, fact_82_surj__pair, fact_346_nth__append__length, fact_30_converse__rtrancl__induct2, fact_197_append__eq__appendI, fact_73_old_Oprod_Oexhaust, fact_331_same__length__different, fact_198_append__eq__append__conv2, fact_107_list_Odistinct_I1_J, fact_64_successively_Ocases, fact_193_Cons__eq__appendI, fact_97_Collect__mem__eq, fact_74_old_Oprod_Oexhaust, fact_309_irrefl__def, fact_164_termi_OIfFalse, fact_55_prod_Oinject, fact_330_list__induct2, fact_145_while__termiE, fact_100_induct__list012, fact_189_append1__eq__conv, fact_283_rotate1_Osimps_I1_J, fact_80_prod__cases, fact_14_rtrancl__induct2, fact_158_com_Odistinct_I5_J, fact_196_eq__Nil__appendI, fact_121_rtrancl_Oinducts, fact_147_exec1E_I5_J, fact_152_com_Oinject_I3_J, fact_182_append__self__conv, fact_79_prod__cases, fact_134_prod__induct3, fact_110_execs_Ocases, fact_329_list__induct3, fact_143_exec1_OWhileFalse, conj_0, fact_44_r__into__rtrancl, fact_221_app__exec, fact_144_exec1_OWhileTrue, fact_154_exec_OWhileFalse, fact_117_rtrancl_Ortrancl__refl, fact_171_app__execs, fact_165_termi_OIfTrue, fact_277_rotate1__is__Nil__conv, fact_353_list__update__nonempty, fact_129_rtrancl_Ocases, fact_52_prod_Oinject
% 18.35/5.04 % No. of inferences in proof: 356
% 18.35/5.04 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4690 ms resp. 3781 ms w/o parsing
% 19.17/5.23 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 19.17/5.24 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------