%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP168^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 : n017.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:07:02 AM UTC 2026
% Result : Theorem 128.55s 60.01s
% Output : Refutation 129.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 164
% Syntax : Number of formulae : 528 ( 273 unt; 0 typ; 49 def)
% Number of atoms : 1954 ( 659 equ; 10 cnn)
% Maximal formula atoms : 122 ( 3 avg)
% Number of connectives : 8860 ( 727 ~; 660 |; 234 &;6843 @)
% ( 0 <=>; 396 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 7 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 309 ( 309 >; 0 *; 0 +; 0 <<)
% Number of symbols : 86 ( 82 usr; 12 con; 0-4 aty)
% Number of variables : 2154 ( 463 ^;1395 !; 247 ?;2154 :)
% ( 0 !>; 0 ?*; 0 @-; 49 @+)
% Comments :
%------------------------------------------------------------------------------
thf(view_e665166499t_unit_type,type,
view_e665166499t_unit: $tType ).
thf(view_e774982825t_unit_type,type,
view_e774982825t_unit: $tType ).
thf(view_ext_real_int_type,type,
view_ext_real_int: $tType ).
thf(view_ext_nat_int_type,type,
view_ext_nat_int: $tType ).
thf(view_ext_nat_type,type,
view_ext_nat: $tType ).
thf(product_unit_type,type,
product_unit: $tType ).
thf(real_int_type,type,
real_int: $tType ).
thf(nat_int_type,type,
nat_int: $tType ).
thf(traffic_type,type,
traffic: $tType ).
thf(real_type,type,
real: $tType ).
thf(cars_type,type,
cars: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(minus_minus_real_decl,type,
minus_minus_real: real > real > real ).
thf(defaul1399868459t_unit_decl,type,
defaul1399868459t_unit: product_unit ).
thf(move_decl,type,
move: traffic > traffic > view_e774982825t_unit > view_e774982825t_unit ).
thf(bot_bot_Product_unit_decl,type,
bot_bot_Product_unit: product_unit ).
thf(ord_less_eq_nat_int_decl,type,
ord_less_eq_nat_int: nat_int > nat_int > $o ).
thf(ord_less_eq_real_decl,type,
ord_less_eq_real: real > real > $o ).
thf(product_Unity_decl,type,
product_Unity: product_unit ).
thf(real_R_Chop_decl,type,
real_R_Chop: real_int > real_int > real_int > $o ).
thf(real_shift_decl,type,
real_shift: real_int > real > real_int ).
thf(abstract_decl,type,
abstract: traffic > traffic > $o ).
thf(clm_decl,type,
clm: traffic > cars > nat_int ).
thf(create_claim_decl,type,
create_claim: traffic > cars > nat > traffic > $o ).
thf(create_reservation_decl,type,
create_reservation: traffic > cars > traffic > $o ).
thf(evolve_decl,type,
evolve: traffic > traffic > $o ).
thf(pos_decl,type,
pos: traffic > cars > real ).
thf(res_decl,type,
res: traffic > cars > nat_int ).
thf(withdraw_claim_decl,type,
withdraw_claim: traffic > cars > traffic > $o ).
thf(withdraw_reservation_decl,type,
withdraw_reservation: traffic > cars > nat > traffic > $o ).
thf(ext_Product_unit_decl,type,
ext_Product_unit: view_e774982825t_unit > real_int ).
thf(hchop_decl,type,
hchop: view_e774982825t_unit > view_e774982825t_unit > view_e774982825t_unit > $o ).
thf(lan_Product_unit_decl,type,
lan_Product_unit: view_e774982825t_unit > nat_int ).
thf(more_Product_unit_decl,type,
more_Product_unit: view_e774982825t_unit > product_unit ).
thf(own_Product_unit_decl,type,
own_Product_unit: view_e774982825t_unit > cars ).
thf(switch_decl,type,
switch: view_e774982825t_unit > cars > view_e774982825t_unit > $o ).
thf(view_e912666823t_unit_decl,type,
view_e912666823t_unit: real_int > nat_int > cars > product_unit > view_e774982825t_unit ).
thf(ts_decl,type,
ts: traffic ).
thf(ts2_decl,type,
ts2: traffic ).
thf(ts_a_decl,type,
ts_a: traffic ).
thf(ts3_decl,type,
ts3: traffic ).
thf(v_decl,type,
v: view_e774982825t_unit ).
thf(sk1_decl,type,
sk1: nat_int > nat_int > ( nat_int > nat_int ) > nat_int > nat_int ).
thf(sk2_decl,type,
sk2: nat_int > nat_int > ( nat_int > nat_int ) > nat_int > nat_int ).
thf(sk3_decl,type,
sk3: nat_int > nat_int > ( nat_int > nat_int ) > nat_int > nat_int ).
thf(sk4_decl,type,
sk4: nat_int > nat_int > ( nat_int > nat_int ) > nat_int > nat_int ).
thf(sk5_decl,type,
sk5: nat_int > ( nat_int > nat_int ) > nat_int > nat_int > nat_int ).
thf(sk6_decl,type,
sk6: nat_int > ( nat_int > nat_int ) > nat_int > nat_int > nat_int ).
thf(sk7_decl,type,
sk7: nat_int > ( nat_int > nat_int ) > nat_int > nat_int > nat_int ).
thf(sk8_decl,type,
sk8: nat_int > ( nat_int > nat_int ) > nat_int > nat_int > nat_int ).
thf(sk9_decl,type,
sk9: view_e774982825t_unit > traffic > ( traffic > view_e774982825t_unit > $o ) > view_e774982825t_unit ).
thf(sk10_decl,type,
sk10: view_e774982825t_unit > traffic > ( traffic > view_e774982825t_unit > $o ) > view_e774982825t_unit ).
thf(sk11_decl,type,
sk11: view_e774982825t_unit > traffic > ( traffic > view_e774982825t_unit > $o ) > view_e774982825t_unit ).
thf(sk12_decl,type,
sk12: view_e774982825t_unit > traffic > ( traffic > view_e774982825t_unit > $o ) > view_e774982825t_unit ).
thf(sk13_decl,type,
sk13: view_e774982825t_unit > cars ).
thf(sk14_decl,type,
sk14: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk15_decl,type,
sk15: real_int > real_int ).
thf(sk16_decl,type,
sk16: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk33_decl,type,
sk33: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk34_decl,type,
sk34: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk42_decl,type,
sk42: cars > view_e774982825t_unit > view_e774982825t_unit ).
thf(sk43_decl,type,
sk43: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk44_decl,type,
sk44: real_int > real_int ).
thf(sk45_decl,type,
sk45: view_e774982825t_unit > view_e774982825t_unit ).
thf(sk46_decl,type,
sk46: real_int > real_int ).
thf(sk47_decl,type,
sk47: real_int > real_int ).
thf(sk56_decl,type,
sk56: traffic > ( traffic > $o ) > traffic > $o ).
thf(sk57_decl,type,
sk57: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk58_decl,type,
sk58: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk59_decl,type,
sk59: traffic > ( traffic > $o ) > traffic > $o ).
thf(sk60_decl,type,
sk60: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk61_decl,type,
sk61: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk62_decl,type,
sk62: ( traffic > $o ) > traffic > traffic > cars ).
thf(sk63_decl,type,
sk63: ( traffic > $o ) > traffic > traffic > nat ).
thf(sk64_decl,type,
sk64: traffic > ( traffic > $o ) > traffic > $o ).
thf(sk65_decl,type,
sk65: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk66_decl,type,
sk66: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk67_decl,type,
sk67: ( traffic > $o ) > traffic > traffic > cars ).
thf(sk68_decl,type,
sk68: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk69_decl,type,
sk69: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk70_decl,type,
sk70: ( traffic > $o ) > traffic > traffic > cars ).
thf(sk71_decl,type,
sk71: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk72_decl,type,
sk72: ( traffic > $o ) > traffic > traffic > traffic ).
thf(sk73_decl,type,
sk73: ( traffic > $o ) > traffic > traffic > cars ).
thf(sk74_decl,type,
sk74: ( traffic > $o ) > traffic > traffic > nat ).
thf(sk78_decl,type,
sk78: view_e774982825t_unit > real_int ).
thf(sk79_decl,type,
sk79: view_e774982825t_unit > nat_int ).
thf(sk80_decl,type,
sk80: view_e774982825t_unit > cars ).
thf(sk81_decl,type,
sk81: view_e774982825t_unit > product_unit ).
thf(sk96_decl,type,
sk96: view_e774982825t_unit > real_int ).
thf(sk97_decl,type,
sk97: view_e774982825t_unit > nat_int ).
thf(sk98_decl,type,
sk98: view_e774982825t_unit > cars ).
thf(sk103_decl,type,
sk103: traffic > cars > traffic ).
thf(sk104_decl,type,
sk104: cars ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
@+[E: nat_int] :
~ ! [F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
@+[E: nat_int] :
~ ( ( ord_less_eq_nat_int @ ( sk1 @ A @ B @ C @ D ) @ E )
=> ( ord_less_eq_nat_int @ ( C @ ( sk1 @ A @ B @ C @ D ) ) @ ( C @ E ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
@+[E: nat_int] :
~ ! [F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
@+[E: nat_int] :
~ ( ( ord_less_eq_nat_int @ ( sk3 @ A @ B @ C @ D ) @ E )
=> ( ord_less_eq_nat_int @ ( C @ ( sk3 @ A @ B @ C @ D ) ) @ ( C @ E ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
@+[E: nat_int] :
~ ! [F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
@+[E: nat_int] :
~ ( ( ord_less_eq_nat_int @ ( sk5 @ A @ B @ C @ D ) @ E )
=> ( ord_less_eq_nat_int @ ( B @ ( sk5 @ A @ B @ C @ D ) ) @ ( B @ E ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
@+[E: nat_int] :
~ ! [F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
@+[E: nat_int] :
~ ( ( ord_less_eq_nat_int @ ( sk7 @ A @ B @ C @ D ) @ E )
=> ( ord_less_eq_nat_int @ ( B @ ( sk7 @ A @ B @ C @ D ) ) @ ( B @ E ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: view_e774982825t_unit,B: traffic,C: traffic > view_e774982825t_unit > $o] :
@+[D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ A @ D @ E )
& ( C @ B @ D ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: view_e774982825t_unit,B: traffic,C: traffic > view_e774982825t_unit > $o] :
@+[D: view_e774982825t_unit] : ( hchop @ A @ ( sk9 @ A @ B @ C ) @ D ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: view_e774982825t_unit,B: traffic,C: traffic > view_e774982825t_unit > $o] :
@+[D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ A @ D @ E )
& ~ ( C @ B @ D ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: view_e774982825t_unit,B: traffic,C: traffic > view_e774982825t_unit > $o] :
@+[D: view_e774982825t_unit] : ( hchop @ A @ ( sk11 @ A @ B @ C ) @ D ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: view_e774982825t_unit] :
@+[B: cars] :
? [C: view_e774982825t_unit] : ( switch @ A @ B @ C ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] : ( switch @ A @ ( sk13 @ A ) @ B ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: real_int] :
@+[B: real_int] : ( real_R_Chop @ A @ B @ A ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] : ( hchop @ A @ B @ A ) ) ) ).
thf(sk33_def,definition,
( sk33
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] :
? [C: view_e774982825t_unit] : ( hchop @ A @ B @ C ) ) ) ).
thf(sk34_def,definition,
( sk34
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] : ( hchop @ A @ ( sk33 @ A ) @ B ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( ^ [A: cars,B: view_e774982825t_unit] :
@+[C: view_e774982825t_unit] : ( switch @ B @ A @ C ) ) ) ).
thf(sk43_def,definition,
( sk43
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] : ( switch @ B @ ( own_Product_unit @ A ) @ A ) ) ) ).
thf(sk44_def,definition,
( sk44
= ( ^ [A: real_int] :
@+[B: real_int] : ( real_R_Chop @ A @ A @ B ) ) ) ).
thf(sk45_def,definition,
( sk45
= ( ^ [A: view_e774982825t_unit] :
@+[B: view_e774982825t_unit] : ( hchop @ A @ A @ B ) ) ) ).
thf(sk46_def,definition,
( sk46
= ( ^ [A: real_int] :
@+[B: real_int] :
? [C: real_int] : ( real_R_Chop @ A @ B @ C ) ) ) ).
thf(sk47_def,definition,
( sk47
= ( ^ [A: real_int] :
@+[B: real_int] : ( real_R_Chop @ A @ ( sk46 @ A ) @ B ) ) ) ).
thf(sk57_def,definition,
( sk57
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( abstract @ C @ D )
=> ( ( A @ D )
=> ! [E: traffic] :
( ( evolve @ D @ E )
=> ( A @ E ) ) ) ) ) ) ).
thf(sk58_def,definition,
( sk58
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( evolve @ ( sk57 @ A @ B @ C ) @ D )
=> ( A @ D ) ) ) ) ).
thf(sk60_def,definition,
( sk60
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( abstract @ C @ D )
=> ( ( A @ D )
=> ! [E: traffic] :
( ? [F: cars,G: nat] : ( create_claim @ D @ F @ G @ E )
=> ( A @ E ) ) ) ) ) ) ).
thf(sk61_def,definition,
( sk61
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ? [E: cars,F: nat] : ( create_claim @ ( sk60 @ A @ B @ C ) @ E @ F @ D )
=> ( A @ D ) ) ) ) ).
thf(sk62_def,definition,
( sk62
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: cars] :
? [E: nat] : ( create_claim @ ( sk60 @ A @ B @ C ) @ D @ E @ ( sk61 @ A @ B @ C ) ) ) ) ).
thf(sk63_def,definition,
( sk63
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: nat] : ( create_claim @ ( sk60 @ A @ B @ C ) @ ( sk62 @ A @ B @ C ) @ D @ ( sk61 @ A @ B @ C ) ) ) ) ).
thf(sk65_def,definition,
( sk65
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( abstract @ C @ D )
=> ( ( A @ D )
=> ! [E: traffic] :
( ? [F: cars] : ( withdraw_claim @ D @ F @ E )
=> ( A @ E ) ) ) ) ) ) ).
thf(sk66_def,definition,
( sk66
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ? [E: cars] : ( withdraw_claim @ ( sk65 @ A @ B @ C ) @ E @ D )
=> ( A @ D ) ) ) ) ).
thf(sk67_def,definition,
( sk67
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: cars] : ( withdraw_claim @ ( sk65 @ A @ B @ C ) @ D @ ( sk66 @ A @ B @ C ) ) ) ) ).
thf(sk68_def,definition,
( sk68
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( abstract @ C @ D )
=> ( ( A @ D )
=> ! [E: traffic] :
( ? [F: cars] : ( create_reservation @ D @ F @ E )
=> ( A @ E ) ) ) ) ) ) ).
thf(sk69_def,definition,
( sk69
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ? [E: cars] : ( create_reservation @ ( sk68 @ A @ B @ C ) @ E @ D )
=> ( A @ D ) ) ) ) ).
thf(sk70_def,definition,
( sk70
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: cars] : ( create_reservation @ ( sk68 @ A @ B @ C ) @ D @ ( sk69 @ A @ B @ C ) ) ) ) ).
thf(sk71_def,definition,
( sk71
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ( abstract @ C @ D )
=> ( ( A @ D )
=> ! [E: traffic] :
( ? [F: cars,G: nat] : ( withdraw_reservation @ D @ F @ G @ E )
=> ( A @ E ) ) ) ) ) ) ).
thf(sk72_def,definition,
( sk72
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: traffic] :
~ ( ? [E: cars,F: nat] : ( withdraw_reservation @ ( sk71 @ A @ B @ C ) @ E @ F @ D )
=> ( A @ D ) ) ) ) ).
thf(sk73_def,definition,
( sk73
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: cars] :
? [E: nat] : ( withdraw_reservation @ ( sk71 @ A @ B @ C ) @ D @ E @ ( sk72 @ A @ B @ C ) ) ) ) ).
thf(sk74_def,definition,
( sk74
= ( ^ [A: traffic > $o,B: traffic,C: traffic] :
@+[D: nat] : ( withdraw_reservation @ ( sk71 @ A @ B @ C ) @ ( sk73 @ A @ B @ C ) @ D @ ( sk72 @ A @ B @ C ) ) ) ) ).
thf(sk78_def,definition,
( sk78
= ( ^ [A: view_e774982825t_unit] :
@+[B: real_int] :
? [C: nat_int,D: cars,E: product_unit] :
( A
= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ) ) ).
thf(sk79_def,definition,
( sk79
= ( ^ [A: view_e774982825t_unit] :
@+[B: nat_int] :
? [C: cars,D: product_unit] :
( A
= ( view_e912666823t_unit @ ( sk78 @ A ) @ B @ C @ D ) ) ) ) ).
thf(sk80_def,definition,
( sk80
= ( ^ [A: view_e774982825t_unit] :
@+[B: cars] :
? [C: product_unit] :
( A
= ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ B @ C ) ) ) ) ).
thf(sk81_def,definition,
( sk81
= ( ^ [A: view_e774982825t_unit] :
@+[B: product_unit] :
( A
= ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ B ) ) ) ) ).
thf(sk96_def,definition,
( sk96
= ( ^ [A: view_e774982825t_unit] :
@+[B: real_int] :
? [C: nat_int,D: cars] :
( A
= ( view_e912666823t_unit @ B @ C @ D @ product_Unity ) ) ) ) ).
thf(sk97_def,definition,
( sk97
= ( ^ [A: view_e774982825t_unit] :
@+[B: nat_int] :
? [C: cars] :
( A
= ( view_e912666823t_unit @ ( sk96 @ A ) @ B @ C @ product_Unity ) ) ) ) ).
thf(sk98_def,definition,
( sk98
= ( ^ [A: view_e774982825t_unit] :
@+[B: cars] :
( A
= ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ B @ product_Unity ) ) ) ) ).
thf(sk103_def,definition,
( sk103
= ( ^ [A: traffic,B: cars] :
@+[C: traffic] : ( create_reservation @ A @ B @ C ) ) ) ).
thf(sk104_def,definition,
( sk104
= ( @+[A: cars] : ( create_reservation @ ts_a @ A @ ts ) ) ) ).
thf(7,axiom,
! [A: nat_int,B: nat_int] :
( ( A = B )
=> ( ord_less_eq_nat_int @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_eq__refl) ).
thf(138,plain,
! [A: nat_int,B: nat_int] :
( ( A = B )
=> ( ord_less_eq_nat_int @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(63,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_local_Ohmlsl_Oat__hchop__dist) ).
thf(333,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(78,axiom,
bot_bot_Product_unit = product_Unity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_bot__unit__def) ).
thf(468,plain,
bot_bot_Product_unit = product_Unity,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(35,axiom,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ A @ D @ E ) )
=> ( switch @ C @ D @ E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_view_Oswitch__triangle) ).
thf(234,plain,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ A @ D @ E ) )
=> ( switch @ C @ D @ E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(106,axiom,
! [A: traffic,B: view_e774982825t_unit] :
( ( move @ A @ A @ B )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_traffic_Omove__nothing) ).
thf(576,plain,
! [A: traffic,B: view_e774982825t_unit] :
( ( move @ A @ A @ B )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(577,plain,
! [B: view_e774982825t_unit,A: traffic] :
( ( move @ A @ A @ B )
= B ),
inference(cnf,[status(esa)],[576]) ).
thf(578,plain,
! [B: view_e774982825t_unit,A: traffic] :
( ( move @ A @ A @ B )
= B ),
inference(lifteq,[status(thm)],[577]) ).
thf(1,conjecture,
( ( move @ ts3 @ ts_a @ v )
= ( move @ ts3 @ ts @ v ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
( ( move @ ts3 @ ts_a @ v )
!= ( move @ ts3 @ ts @ v ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(117,plain,
( ( move @ ts3 @ ts_a @ v )
!= ( move @ ts3 @ ts @ v ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(118,plain,
( ( move @ ts3 @ ts_a @ v )
!= ( move @ ts3 @ ts @ v ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(5579,plain,
! [B: view_e774982825t_unit,A: traffic] :
( ( B
!= ( move @ ts3 @ ts @ v ) )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,118]) ).
thf(5583,plain,
! [A: traffic] :
( ( move @ A @ A @ ( move @ ts3 @ ts @ v ) )
!= ( move @ ts3 @ ts_a @ v ) ),
inference(simp,[status(thm)],[5579]) ).
thf(5997,plain,
! [C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( B
!= ( move @ C @ C @ ( move @ ts3 @ ts @ v ) ) )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,5583]) ).
thf(6002,plain,
! [B: traffic,A: traffic] :
( ( move @ A @ A @ ( move @ B @ B @ ( move @ ts3 @ ts @ v ) ) )
!= ( move @ ts3 @ ts_a @ v ) ),
inference(simp,[status(thm)],[5997]) ).
thf(6014,plain,
! [B: traffic,A: traffic] :
( ( move @ A @ A @ ( move @ B @ B @ ( move @ ts3 @ ts @ v ) ) )
!= ( move @ ts3 @ ts_a @ v ) ),
inference(simp,[status(thm)],[6002]) ).
thf(82,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ( evolve @ B @ C )
=> ( abstract @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_traffic_Oevolve) ).
thf(481,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ( evolve @ B @ C )
=> ( abstract @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(14,axiom,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_order__class_Oorder_Oantisym) ).
thf(170,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(57,axiom,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( hchop @ A @ A @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_view_Ohorizontal__chop__empty__right) ).
thf(308,plain,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( hchop @ A @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(100,axiom,
! [A: cars,B: traffic] :
? [C: traffic] : ( create_reservation @ B @ A @ C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_traffic_Oalways__create__res) ).
thf(562,plain,
! [A: cars,B: traffic] :
? [C: traffic] : ( create_reservation @ B @ A @ C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(563,plain,
! [B: traffic,A: cars] : ( create_reservation @ B @ A @ ( sk103 @ B @ A ) ),
inference(cnf,[status(esa)],[562]) ).
thf(20,axiom,
! [A: traffic,B: cars,C: traffic] :
( ( create_reservation @ A @ B @ C )
=> ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_traffic_Ocreate__res__subseteq1) ).
thf(185,plain,
! [A: traffic,B: cars,C: traffic] :
( ( create_reservation @ A @ B @ C )
=> ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(186,plain,
! [C: traffic,B: cars,A: traffic] :
( ~ ( create_reservation @ A @ B @ C )
| ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ C @ B ) ) ),
inference(cnf,[status(esa)],[185]) ).
thf(7324,plain,
! [E: traffic,D: cars,C: traffic,B: traffic,A: cars] :
( ~ $true
| ( ord_less_eq_nat_int @ ( res @ C @ D ) @ ( res @ E @ D ) )
| ( ( create_reservation @ B @ A @ ( sk103 @ B @ A ) )
!= ( create_reservation @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[563,186]) ).
thf(7325,plain,
! [E: traffic,D: cars,C: traffic,B: traffic,A: cars] :
( ( ord_less_eq_nat_int @ ( res @ C @ D ) @ ( res @ E @ D ) )
| ( ( create_reservation @ B @ A @ ( sk103 @ B @ A ) )
!= ( create_reservation @ C @ D @ E ) ) ),
inference(simp,[status(thm)],[7324]) ).
thf(7326,plain,
! [B: cars,A: traffic] : ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ ( sk103 @ A @ B ) @ B ) ),
inference(pattern_uni,[status(thm)],[7325:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( sk103 @ F @ G ))]]) ).
thf(7332,plain,
! [B: cars,A: traffic] : ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ ( sk103 @ A @ B ) @ B ) ),
inference(simp,[status(thm)],[7326]) ).
thf(90,axiom,
! [A: traffic,B: traffic] :
( ( abstract @ A @ B )
=> ( ( B != A )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ( evolve @ C @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars,E: nat] : ( create_claim @ C @ D @ E @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars] : ( withdraw_claim @ C @ D @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars] : ( create_reservation @ C @ D @ B ) )
=> ~ ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars,E: nat] : ( withdraw_reservation @ C @ D @ E @ B ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_traffic_Oabstract_Ocases) ).
thf(511,plain,
! [A: traffic,B: traffic] :
( ( abstract @ A @ B )
=> ( ( B != A )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ( evolve @ C @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars,E: nat] : ( create_claim @ C @ D @ E @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars] : ( withdraw_claim @ C @ D @ B ) )
=> ( ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars] : ( create_reservation @ C @ D @ B ) )
=> ~ ! [C: traffic] :
( ( abstract @ A @ C )
=> ~ ? [D: cars,E: nat] : ( withdraw_reservation @ C @ D @ E @ B ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(613,plain,
( ( ts3 != ts3 )
| ( ts_a != ts )
| ( v != v ) ),
inference(simp,[status(thm)],[118]) ).
thf(614,plain,
ts_a != ts,
inference(simp,[status(thm)],[613]) ).
thf(5994,plain,
! [C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( ( move @ C @ C @ B )
!= ( move @ ts3 @ ts_a @ v ) )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,5583]) ).
thf(6005,plain,
! [C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( ( move @ C @ C @ B )
!= ( move @ ts3 @ ts_a @ v ) )
| ( A != ts3 )
| ( A != ts )
| ( B != v ) ),
inference(simp,[status(thm)],[5994]) ).
thf(6017,plain,
! [A: traffic] :
( ( ( move @ A @ A @ v )
!= ( move @ ts3 @ ts_a @ v ) )
| ( ts3 != ts ) ),
inference(simp,[status(thm)],[6005]) ).
thf(113,axiom,
! [A: traffic,B: cars,C: traffic,D: view_e774982825t_unit] :
( ( create_reservation @ A @ B @ C )
=> ( ( move @ A @ C @ D )
= D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_traffic_Omove__stability__res) ).
thf(597,plain,
! [A: traffic,B: cars,C: traffic,D: view_e774982825t_unit] :
( ( create_reservation @ A @ B @ C )
=> ( ( move @ A @ C @ D )
= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(31,axiom,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( hchop @ A @ B @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_view_Ohorizontal__chop__empty__left) ).
thf(217,plain,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( hchop @ A @ B @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(47,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) )
=> ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_local_Ohmlsl_Oat__neg1) ).
thf(276,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) )
=> ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(73,axiom,
! [A: traffic,B: traffic,C: traffic > $o] :
( ( abstract @ A @ B )
=> ( ( C @ A )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ( evolve @ D @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars,G: nat] : ( create_claim @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars] : ( withdraw_claim @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars] : ( create_reservation @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars,G: nat] : ( withdraw_reservation @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( C @ B ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_traffic_Oabstract_Oinducts) ).
thf(368,plain,
! [A: traffic,B: traffic,C: traffic > $o] :
( ( abstract @ A @ B )
=> ( ( C @ A )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ( evolve @ D @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars,G: nat] : ( create_claim @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars] : ( withdraw_claim @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars] : ( create_reservation @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic,E: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ( ? [F: cars,G: nat] : ( withdraw_reservation @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( C @ B ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(369,plain,
! [A: traffic,B: traffic] :
( ( abstract @ A @ B )
=> ! [C: traffic > $o] :
( ( C @ A )
=> ( ! [D: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ! [E: traffic] :
( ( evolve @ D @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ! [E: traffic] :
( ? [F: cars,G: nat] : ( create_claim @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ! [E: traffic] :
( ? [F: cars] : ( withdraw_claim @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ! [E: traffic] :
( ? [F: cars] : ( create_reservation @ D @ F @ E )
=> ( C @ E ) ) ) )
=> ( ! [D: traffic] :
( ( abstract @ A @ D )
=> ( ( C @ D )
=> ! [E: traffic] :
( ? [F: cars,G: nat] : ( withdraw_reservation @ D @ F @ G @ E )
=> ( C @ E ) ) ) )
=> ( C @ B ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[368]) ).
thf(370,plain,
! [C: traffic > $o,B: traffic,A: traffic] :
( ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ( abstract @ A @ ( sk57 @ C @ B @ A ) )
| ( sk56 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ( C @ ( sk57 @ C @ B @ A ) )
| ( sk56 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ( evolve @ ( sk57 @ C @ B @ A ) @ ( sk58 @ C @ B @ A ) )
| ( sk56 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( C @ ( sk58 @ C @ B @ A ) )
| ( sk56 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ( abstract @ A @ ( sk60 @ C @ B @ A ) )
| ( sk59 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ( C @ ( sk60 @ C @ B @ A ) )
| ( sk59 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ( create_claim @ ( sk60 @ C @ B @ A ) @ ( sk62 @ C @ B @ A ) @ ( sk63 @ C @ B @ A ) @ ( sk61 @ C @ B @ A ) )
| ( sk59 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( C @ ( sk61 @ C @ B @ A ) )
| ( sk59 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ( abstract @ A @ ( sk65 @ C @ B @ A ) )
| ( sk64 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ( C @ ( sk65 @ C @ B @ A ) )
| ( sk64 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ( withdraw_claim @ ( sk65 @ C @ B @ A ) @ ( sk67 @ C @ B @ A ) @ ( sk66 @ C @ B @ A ) )
| ( sk64 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( C @ ( sk66 @ C @ B @ A ) )
| ( sk64 @ A @ C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( abstract @ A @ ( sk68 @ C @ B @ A ) )
| ( abstract @ A @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( abstract @ A @ ( sk68 @ C @ B @ A ) )
| ( C @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( abstract @ A @ ( sk68 @ C @ B @ A ) )
| ( withdraw_reservation @ ( sk71 @ C @ B @ A ) @ ( sk73 @ C @ B @ A ) @ ( sk74 @ C @ B @ A ) @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( abstract @ A @ ( sk68 @ C @ B @ A ) )
| ~ ( C @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( C @ ( sk68 @ C @ B @ A ) )
| ( abstract @ A @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( C @ ( sk68 @ C @ B @ A ) )
| ( C @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( C @ ( sk68 @ C @ B @ A ) )
| ( withdraw_reservation @ ( sk71 @ C @ B @ A ) @ ( sk73 @ C @ B @ A ) @ ( sk74 @ C @ B @ A ) @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( C @ ( sk68 @ C @ B @ A ) )
| ~ ( C @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( create_reservation @ ( sk68 @ C @ B @ A ) @ ( sk70 @ C @ B @ A ) @ ( sk69 @ C @ B @ A ) )
| ( abstract @ A @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( create_reservation @ ( sk68 @ C @ B @ A ) @ ( sk70 @ C @ B @ A ) @ ( sk69 @ C @ B @ A ) )
| ( C @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( create_reservation @ ( sk68 @ C @ B @ A ) @ ( sk70 @ C @ B @ A ) @ ( sk69 @ C @ B @ A ) )
| ( withdraw_reservation @ ( sk71 @ C @ B @ A ) @ ( sk73 @ C @ B @ A ) @ ( sk74 @ C @ B @ A ) @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ( create_reservation @ ( sk68 @ C @ B @ A ) @ ( sk70 @ C @ B @ A ) @ ( sk69 @ C @ B @ A ) )
| ~ ( C @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ( abstract @ A @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ( C @ ( sk71 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ( withdraw_reservation @ ( sk71 @ C @ B @ A ) @ ( sk73 @ C @ B @ A ) @ ( sk74 @ C @ B @ A ) @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) )
& ( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ~ ( C @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) ) ),
inference(cnf,[status(esa)],[369]) ).
thf(385,plain,
! [C: traffic > $o,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ~ ( C @ ( sk72 @ C @ B @ A ) )
| ( C @ B ) ),
inference(cnfConj,[status(thm)],[370]) ).
thf(91,axiom,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( own_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_select__convs_I3_J) ).
thf(533,plain,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( own_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(8,axiom,
! [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_ord__le__eq__subst) ).
thf(142,plain,
! [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(79,axiom,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( lan_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_select__convs_I2_J) ).
thf(470,plain,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( lan_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(471,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( lan_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= B ),
inference(cnf,[status(esa)],[470]) ).
thf(472,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( lan_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= B ),
inference(lifteq,[status(thm)],[471]) ).
thf(9,axiom,
! [A: traffic,B: cars,C: nat,D: traffic,E: cars] :
( ( withdraw_reservation @ A @ B @ C @ D )
=> ( ord_less_eq_nat_int @ ( res @ D @ E ) @ ( res @ A @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_traffic_Owithdraw__res__subseteq) ).
thf(151,plain,
! [A: traffic,B: cars,C: nat,D: traffic,E: cars] :
( ( withdraw_reservation @ A @ B @ C @ D )
=> ( ord_less_eq_nat_int @ ( res @ D @ E ) @ ( res @ A @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(152,plain,
! [A: traffic,B: cars,C: nat,D: traffic] :
( ( withdraw_reservation @ A @ B @ C @ D )
=> ! [E: cars] : ( ord_less_eq_nat_int @ ( res @ D @ E ) @ ( res @ A @ E ) ) ),
inference(miniscope,[status(thm)],[151]) ).
thf(153,plain,
! [E: cars,D: traffic,C: nat,B: cars,A: traffic] :
( ~ ( withdraw_reservation @ A @ B @ C @ D )
| ( ord_less_eq_nat_int @ ( res @ D @ E ) @ ( res @ A @ E ) ) ),
inference(cnf,[status(esa)],[152]) ).
thf(68,axiom,
! [A: product_unit > $o,B: product_unit] :
( ( A @ product_Unity )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_old_Ounit_Oinducts) ).
thf(349,plain,
! [A: product_unit > $o,B: product_unit] :
( ( A @ product_Unity )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(350,plain,
! [A: product_unit > $o] :
( ( A @ product_Unity )
=> ! [B: product_unit] : ( A @ B ) ),
inference(miniscope,[status(thm)],[349]) ).
thf(351,plain,
! [B: product_unit,A: product_unit > $o] :
( ~ ( A @ product_Unity )
| ( A @ B ) ),
inference(cnf,[status(esa)],[350]) ).
thf(352,plain,
! [A: product_unit] :
( ( product_Unity != product_Unity )
| ( product_Unity = A ) ),
inference(replace_leibeq,[status(thm)],[351:[bind(A,$thf( (=) @ product_unit @ product_Unity ))]]) ).
thf(353,plain,
! [A: product_unit] :
( ( product_Unity != product_Unity )
| ( product_Unity = A ) ),
inference(lifteq,[status(thm)],[352]) ).
thf(354,plain,
! [A: product_unit] : ( product_Unity = A ),
inference(simp,[status(thm)],[353]) ).
thf(469,plain,
product_Unity = bot_bot_Product_unit,
inference(lifteq,[status(thm)],[468]) ).
thf(85,axiom,
defaul1399868459t_unit = product_Unity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_default__unit__def) ).
thf(490,plain,
defaul1399868459t_unit = product_Unity,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(491,plain,
product_Unity = defaul1399868459t_unit,
inference(lifteq,[status(thm)],[490]) ).
thf(611,plain,
bot_bot_Product_unit = defaul1399868459t_unit,
inference(rewrite,[status(thm)],[491,469]) ).
thf(612,plain,
product_Unity = defaul1399868459t_unit,
inference(rewrite,[status(thm)],[469,611]) ).
thf(615,plain,
! [A: product_unit] : ( defaul1399868459t_unit = A ),
inference(rewrite,[status(thm)],[354,612]) ).
thf(92,axiom,
! [A: view_e774982825t_unit] :
~ ! [B: real_int,C: nat_int,D: cars] :
( A
!= ( view_e912666823t_unit @ B @ C @ D @ product_Unity ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_cases) ).
thf(536,plain,
! [A: view_e774982825t_unit] :
~ ! [B: real_int,C: nat_int,D: cars] :
( A
!= ( view_e912666823t_unit @ B @ C @ D @ product_Unity ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(537,plain,
~ ~ ! [A: view_e774982825t_unit] :
? [B: real_int,C: nat_int,D: cars] :
( A
= ( view_e912666823t_unit @ B @ C @ D @ product_Unity ) ),
inference(miniscope,[status(thm)],[536]) ).
thf(538,plain,
! [A: view_e774982825t_unit] :
( A
= ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ ( sk98 @ A ) @ product_Unity ) ),
inference(cnf,[status(esa)],[537]) ).
thf(539,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ ( sk98 @ A ) @ product_Unity )
= A ),
inference(lifteq,[status(thm)],[538]) ).
thf(6204,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ ( sk98 @ A ) @ defaul1399868459t_unit )
= A ),
inference(rewrite,[status(thm)],[539,612]) ).
thf(6205,plain,
! [B: view_e774982825t_unit,A: product_unit] :
( ( ( view_e912666823t_unit @ ( sk96 @ B ) @ ( sk97 @ B ) @ ( sk98 @ B ) @ A )
= B )
| ( defaul1399868459t_unit != defaul1399868459t_unit ) ),
inference(paramod_ordered,[status(thm)],[615,6204]) ).
thf(6206,plain,
! [B: view_e774982825t_unit,A: product_unit] :
( ( view_e912666823t_unit @ ( sk96 @ B ) @ ( sk97 @ B ) @ ( sk98 @ B ) @ A )
= B ),
inference(pattern_uni,[status(thm)],[6205:[]]) ).
thf(6377,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( lan_Product_unit @ A )
= C )
| ( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ ( sk98 @ A ) @ defaul1399868459t_unit )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[6204,472]) ).
thf(6378,plain,
! [A: view_e774982825t_unit] :
( ( sk97 @ A )
= ( lan_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[6377:[bind(A,$thf( H )),bind(B,$thf( sk96 @ H )),bind(C,$thf( sk97 @ H )),bind(D,$thf( sk98 @ H )),bind(E,$thf( defaul1399868459t_unit ))]]) ).
thf(6460,plain,
! [A: view_e774982825t_unit] :
( ( sk97 @ A )
= ( lan_Product_unit @ A ) ),
inference(simp,[status(thm)],[6378]) ).
thf(6465,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( lan_Product_unit @ A ) @ ( sk98 @ A ) @ defaul1399868459t_unit )
= A ),
inference(rewrite,[status(thm)],[6204,6460]) ).
thf(534,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( own_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= C ),
inference(cnf,[status(esa)],[533]) ).
thf(535,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( own_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= C ),
inference(lifteq,[status(thm)],[534]) ).
thf(6776,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( own_Product_unit @ A )
= D )
| ( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( lan_Product_unit @ A ) @ ( sk98 @ A ) @ defaul1399868459t_unit )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[6465,535]) ).
thf(6777,plain,
! [A: view_e774982825t_unit] :
( ( sk98 @ A )
= ( own_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[6776:[bind(A,$thf( H )),bind(B,$thf( sk96 @ H )),bind(C,$thf( lan_Product_unit @ H )),bind(D,$thf( sk98 @ H )),bind(E,$thf( defaul1399868459t_unit ))]]) ).
thf(6784,plain,
! [A: view_e774982825t_unit] :
( ( sk98 @ A )
= ( own_Product_unit @ A ) ),
inference(simp,[status(thm)],[6777]) ).
thf(6787,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ defaul1399868459t_unit )
= A ),
inference(rewrite,[status(thm)],[6465,6784]) ).
thf(93,axiom,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( ext_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_select__convs_I1_J) ).
thf(540,plain,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( ext_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(541,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( ext_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= A ),
inference(cnf,[status(esa)],[540]) ).
thf(542,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( ext_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= A ),
inference(lifteq,[status(thm)],[541]) ).
thf(6815,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= B )
| ( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ defaul1399868459t_unit )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[6787,542]) ).
thf(6816,plain,
! [A: view_e774982825t_unit] :
( ( sk96 @ A )
= ( ext_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[6815:[bind(A,$thf( H )),bind(B,$thf( sk96 @ H )),bind(C,$thf( lan_Product_unit @ H )),bind(D,$thf( own_Product_unit @ H )),bind(E,$thf( defaul1399868459t_unit ))]]) ).
thf(6817,plain,
! [A: view_e774982825t_unit] :
( ( sk96 @ A )
= ( ext_Product_unit @ A ) ),
inference(simp,[status(thm)],[6816]) ).
thf(6877,plain,
! [B: view_e774982825t_unit,A: product_unit] :
( ( view_e912666823t_unit @ ( ext_Product_unit @ B ) @ ( lan_Product_unit @ B ) @ ( own_Product_unit @ B ) @ A )
= B ),
inference(rewrite,[status(thm)],[6206,6784,6817,6460]) ).
thf(111,axiom,
! [A: traffic,B: traffic] :
( own_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( own_Product_unit @ ( move @ A @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_traffic_Omove__keeps__owner) ).
thf(590,plain,
! [A: traffic,B: traffic] :
( own_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( own_Product_unit @ ( move @ A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(591,plain,
! [B: traffic,A: traffic] :
( own_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( own_Product_unit @ ( move @ A @ B @ C ) ) ) ),
inference(cnf,[status(esa)],[590]) ).
thf(592,plain,
! [B: traffic,A: traffic] :
( ( ^ [C: view_e774982825t_unit] : ( own_Product_unit @ ( move @ A @ B @ C ) ) )
= own_Product_unit ),
inference(lifteq,[status(thm)],[591]) ).
thf(1100,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic] :
( ( own_Product_unit @ ( move @ A @ B @ C ) )
= ( own_Product_unit @ C ) ),
inference(func_ext,[status(esa)],[592]) ).
thf(59,axiom,
! [A: view_e774982825t_unit] : ( switch @ A @ ( own_Product_unit @ A ) @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_view_Oswitch__refl) ).
thf(312,plain,
! [A: view_e774982825t_unit] : ( switch @ A @ ( own_Product_unit @ A ) @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(313,plain,
! [A: view_e774982825t_unit] : ( switch @ A @ ( own_Product_unit @ A ) @ A ),
inference(cnf,[status(esa)],[312]) ).
thf(6198,plain,
! [D: view_e774982825t_unit,C: view_e774982825t_unit,B: traffic,A: traffic] :
( ( switch @ D @ ( own_Product_unit @ C ) @ D )
| ( ( own_Product_unit @ ( move @ A @ B @ C ) )
!= ( own_Product_unit @ D ) ) ),
inference(paramod_ordered,[status(thm)],[1100,313]) ).
thf(6199,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic] : ( switch @ ( move @ A @ B @ C ) @ ( own_Product_unit @ C ) @ ( move @ A @ B @ C ) ),
inference(pattern_uni,[status(thm)],[6198:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( move @ E @ F @ G ))]]) ).
thf(6202,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic] : ( switch @ ( move @ A @ B @ C ) @ ( own_Product_unit @ C ) @ ( move @ A @ B @ C ) ),
inference(simp,[status(thm)],[6199]) ).
thf(10661,plain,
! [E: view_e774982825t_unit,D: traffic,C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( switch @ ( move @ C @ D @ E ) @ ( own_Product_unit @ E ) @ B )
| ( ( move @ A @ A @ B )
!= ( move @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[578,6202]) ).
thf(10662,plain,
! [B: view_e774982825t_unit,A: traffic] : ( switch @ ( move @ A @ A @ B ) @ ( own_Product_unit @ B ) @ B ),
inference(pattern_uni,[status(thm)],[10661:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(49,axiom,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ A @ B @ D ) )
=> ( C = D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_view_Oswitch__unique) ).
thf(288,plain,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ A @ B @ D ) )
=> ( C = D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(54,axiom,
! [A: view_e774982825t_unit,B: cars,C: traffic > view_e774982825t_unit > $o,D: traffic] :
( ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ A @ B @ E )
=> ( C @ D @ E ) ) )
= ( ! [E: view_e774982825t_unit] :
( ( switch @ A @ B @ E )
=> ~ ( C @ D @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_local_Ohmlsl_Oat__neg_H) ).
thf(301,plain,
! [A: view_e774982825t_unit,B: cars,C: traffic > view_e774982825t_unit > $o,D: traffic] :
( ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ A @ B @ E )
=> ( C @ D @ E ) ) )
= ( ! [E: view_e774982825t_unit] :
( ( switch @ A @ B @ E )
=> ~ ( C @ D @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(41,axiom,
! [A: traffic,B: cars,C: traffic] :
( ( create_reservation @ A @ B @ C )
=> ( ord_less_eq_nat_int @ ( clm @ A @ B ) @ ( res @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_traffic_Ocreate__res__subseteq2) ).
thf(257,plain,
! [A: traffic,B: cars,C: traffic] :
( ( create_reservation @ A @ B @ C )
=> ( ord_less_eq_nat_int @ ( clm @ A @ B ) @ ( res @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(103,axiom,
( move
= ( ^ [A: traffic,B: traffic,C: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ C ) @ ( minus_minus_real @ ( pos @ B @ ( own_Product_unit @ C ) ) @ ( pos @ A @ ( own_Product_unit @ C ) ) ) ) @ ( lan_Product_unit @ C ) @ ( own_Product_unit @ C ) @ product_Unity ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_traffic_Omove__def) ).
thf(570,plain,
( move
= ( ^ [A: traffic,B: traffic,C: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ C ) @ ( minus_minus_real @ ( pos @ B @ ( own_Product_unit @ C ) ) @ ( pos @ A @ ( own_Product_unit @ C ) ) ) ) @ ( lan_Product_unit @ C ) @ ( own_Product_unit @ C ) @ product_Unity ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(3,axiom,
! [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_ord__eq__le__subst) ).
thf(119,plain,
! [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(120,plain,
! [A: nat_int,B: nat_int > nat_int,C: nat_int] :
( ( A
= ( B @ C ) )
=> ! [D: nat_int] :
( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ( ord_less_eq_nat_int @ ( sk1 @ D @ C @ B @ A ) @ ( sk2 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) )
& ( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ~ ( ord_less_eq_nat_int @ ( B @ ( sk1 @ D @ C @ B @ A ) ) @ ( B @ ( sk2 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ),
inference(cnf,[status(esa)],[120]) ).
thf(122,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ( ord_less_eq_nat_int @ ( sk1 @ D @ C @ B @ A ) @ ( sk2 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(124,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ( ord_less_eq_nat_int @ ( sk1 @ D @ C @ B @ A ) @ ( sk2 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(lifteq,[status(thm)],[122]) ).
thf(125,plain,
! [C: nat_int,B: nat_int,A: nat_int > nat_int] :
( ~ ( ord_less_eq_nat_int @ B @ C )
| ( ord_less_eq_nat_int @ ( sk1 @ C @ B @ A @ ( A @ B ) ) @ ( sk2 @ C @ B @ A @ ( A @ B ) ) )
| ( ord_less_eq_nat_int @ ( A @ B ) @ ( A @ C ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(99,axiom,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( ( create_reservation @ A @ B @ C )
& ( B != D ) )
=> ( ( clm @ A @ D )
= ( clm @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_traffic_Ocreate__res__subseteq2__neq) ).
thf(559,plain,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( ( create_reservation @ A @ B @ C )
& ( B != D ) )
=> ( ( clm @ A @ D )
= ( clm @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(3604,plain,
! [B: product_unit,A: product_unit > $o] :
( ~ ( A @ defaul1399868459t_unit )
| ( A @ B ) ),
inference(rewrite,[status(thm)],[351,612]) ).
thf(3741,plain,
! [B: product_unit,A: product_unit > $o] :
( ~ ( A @ defaul1399868459t_unit )
| ( ( A @ B )
!= ( ~ ( A @ defaul1399868459t_unit ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[3604]) ).
thf(3874,plain,
! [B: product_unit,A: product_unit > $o] :
( ~ ( A @ defaul1399868459t_unit )
| ( ( A @ B )
!= ( ~ ( A @ defaul1399868459t_unit ) ) ) ),
inference(simp,[status(thm)],[3741]) ).
thf(4357,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ defaul1399868459t_unit )
| ( ( ~ ( B @ A ) )
!= ( B @ C ) )
| ( defaul1399868459t_unit != defaul1399868459t_unit ) ),
inference(paramod_ordered,[status(thm)],[615,3874]) ).
thf(4358,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ defaul1399868459t_unit )
| ( ( ~ ( B @ A ) )
!= ( B @ C ) ) ),
inference(pattern_uni,[status(thm)],[4357:[]]) ).
thf(115,axiom,
( ( move @ ts3 @ ts_a @ v )
= ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5__092_060open_062move_Ats_Ats_H_Av_A_061_Amove_Ats_H_Ats_H_H_A_Imove_Ats_Ats_H_Av_J_092_060close_062) ).
thf(605,plain,
( ( move @ ts3 @ ts_a @ v )
= ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(606,plain,
( ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) )
= ( move @ ts3 @ ts_a @ v ) ),
inference(lifteq,[status(thm)],[605]) ).
thf(571,plain,
( ( ^ [A: traffic,B: traffic,C: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ C ) @ ( minus_minus_real @ ( pos @ B @ ( own_Product_unit @ C ) ) @ ( pos @ A @ ( own_Product_unit @ C ) ) ) ) @ ( lan_Product_unit @ C ) @ ( own_Product_unit @ C ) @ product_Unity ) )
= move ),
inference(lifteq,[status(thm)],[570]) ).
thf(3596,plain,
( ( ^ [A: traffic,B: traffic,C: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ C ) @ ( minus_minus_real @ ( pos @ B @ ( own_Product_unit @ C ) ) @ ( pos @ A @ ( own_Product_unit @ C ) ) ) ) @ ( lan_Product_unit @ C ) @ ( own_Product_unit @ C ) @ defaul1399868459t_unit ) )
= move ),
inference(rewrite,[status(thm)],[571,612]) ).
thf(3600,plain,
! [A: product_unit] :
( ( ( ^ [B: traffic,C: traffic,D: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ D ) @ ( minus_minus_real @ ( pos @ C @ ( own_Product_unit @ D ) ) @ ( pos @ B @ ( own_Product_unit @ D ) ) ) ) @ ( lan_Product_unit @ D ) @ ( own_Product_unit @ D ) @ A ) )
= move )
| ( defaul1399868459t_unit != defaul1399868459t_unit ) ),
inference(paramod_ordered,[status(thm)],[615,3596]) ).
thf(3601,plain,
! [A: product_unit] :
( ( ^ [B: traffic,C: traffic,D: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ D ) @ ( minus_minus_real @ ( pos @ C @ ( own_Product_unit @ D ) ) @ ( pos @ B @ ( own_Product_unit @ D ) ) ) ) @ ( lan_Product_unit @ D ) @ ( own_Product_unit @ D ) @ A ) )
= move ),
inference(pattern_uni,[status(thm)],[3600:[]]) ).
thf(5851,plain,
! [B: traffic,A: product_unit] :
( ( ^ [C: traffic,D: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ D ) @ ( minus_minus_real @ ( pos @ C @ ( own_Product_unit @ D ) ) @ ( pos @ B @ ( own_Product_unit @ D ) ) ) ) @ ( lan_Product_unit @ D ) @ ( own_Product_unit @ D ) @ A ) )
= ( move @ B ) ),
inference(func_ext,[status(esa)],[3601]) ).
thf(84,axiom,
! [A: view_e774982825t_unit] :
~ ! [B: real_int,C: nat_int,D: cars,E: product_unit] :
( A
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_cases__scheme) ).
thf(486,plain,
! [A: view_e774982825t_unit] :
~ ! [B: real_int,C: nat_int,D: cars,E: product_unit] :
( A
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(487,plain,
~ ~ ! [A: view_e774982825t_unit] :
? [B: real_int,C: nat_int,D: cars,E: product_unit] :
( A
= ( view_e912666823t_unit @ B @ C @ D @ E ) ),
inference(miniscope,[status(thm)],[486]) ).
thf(488,plain,
! [A: view_e774982825t_unit] :
( A
= ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ ( sk81 @ A ) ) ),
inference(cnf,[status(esa)],[487]) ).
thf(489,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ ( sk81 @ A ) )
= A ),
inference(lifteq,[status(thm)],[488]) ).
thf(7622,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( own_Product_unit @ A )
= D )
| ( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ ( sk81 @ A ) )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[489,535]) ).
thf(7623,plain,
! [A: view_e774982825t_unit] :
( ( sk80 @ A )
= ( own_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[7622:[bind(A,$thf( I )),bind(B,$thf( sk78 @ I )),bind(C,$thf( sk79 @ I )),bind(D,$thf( sk80 @ I )),bind(E,$thf( sk81 @ I ))]]) ).
thf(7633,plain,
! [A: view_e774982825t_unit] :
( ( sk80 @ A )
= ( own_Product_unit @ A ) ),
inference(simp,[status(thm)],[7623]) ).
thf(30,axiom,
! [A: real_int] :
? [B: real_int] : ( real_R_Chop @ A @ B @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_chop__singleton__left) ).
thf(215,plain,
! [A: real_int] :
? [B: real_int] : ( real_R_Chop @ A @ B @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(216,plain,
! [A: real_int] : ( real_R_Chop @ A @ ( sk15 @ A ) @ A ),
inference(cnf,[status(esa)],[215]) ).
thf(680,plain,
! [C: traffic > $o,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( C @ A )
| ~ ( sk56 @ A @ C @ B )
| ~ ( sk59 @ A @ C @ B )
| ~ ( sk64 @ A @ C @ B )
| ~ ( C @ ( sk69 @ C @ B @ A ) )
| ( C @ B )
| ( ( C @ ( sk72 @ C @ B @ A ) )
!= ( abstract @ A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[385]) ).
thf(812,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( abstract
@ ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
@ ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) ) )
| ( abstract @ ( C @ B ) @ ( D @ B ) )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A ) ),
inference(pre_uni,[status(thm)],[680:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( ^ [F: traffic] : ( abstract @ ( D @ F ) @ ( E @ F ) ) ))]]) ).
thf(813,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ( abstract @ ( C @ B ) @ ( D @ B ) )
| ~ ( abstract
@ ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
@ ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) ) )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A ) ),
inference(pre_uni,[status(thm)],[812:[]]) ).
thf(856,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ( abstract @ ( C @ B ) @ ( D @ B ) )
| ~ ( abstract
@ ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
@ ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) ) )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A ) ),
inference(simp,[status(thm)],[813]) ).
thf(950,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ( abstract @ ( C @ B ) @ ( D @ B ) )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A )
| ( ( abstract
@ ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
@ ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) ) )
!= ( abstract @ A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[856]) ).
thf(969,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ( abstract @ ( C @ B ) @ ( D @ B ) )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A ) ),
inference(pre_uni,[status(thm)],[950:[]]) ).
thf(970,plain,
! [D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk59 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ~ ( sk64 @ A
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B )
| ( abstract @ ( C @ B ) @ ( D @ B ) )
| ( ( D
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [E: traffic] : ( abstract @ ( C @ E ) @ ( D @ E ) )
@ B
@ A ) )
!= A ) ),
inference(pre_uni,[status(thm)],[969:[]]) ).
thf(1112,plain,
! [H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk59 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk64 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ( ( D
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ~ ( abstract @ E @ F )
| ~ $true
| ~ ( sk56 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk59 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk64 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ( abstract @ ( G @ F ) @ ( H @ F ) )
| ( ( H
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( abstract @ ( C @ B ) @ ( D @ B ) )
!= ( abstract @ ( G @ E ) @ ( H @ E ) ) ) ),
inference(paramod_ordered,[status(thm)],[970,970]) ).
thf(1113,plain,
! [H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk59 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk64 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ( ( D
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ~ ( abstract @ E @ F )
| ~ ( sk56 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk59 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk64 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ( abstract @ ( G @ F ) @ ( H @ F ) )
| ( ( H
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( abstract @ ( C @ B ) @ ( D @ B ) )
!= ( abstract @ ( G @ E ) @ ( H @ E ) ) ) ),
inference(simp,[status(thm)],[1112]) ).
thf(1168,plain,
! [H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk59 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk64 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ( ( D
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ~ ( abstract @ E @ F )
| ~ ( sk56 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk59 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk64 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ( abstract @ ( G @ F ) @ ( H @ F ) )
| ( ( H
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) ) ),
inference(pre_uni,[status(thm)],[1113:[]]) ).
thf(1169,plain,
! [H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ( abstract @ ( G @ F ) @ ( H @ F ) )
| ~ ( sk64 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk59 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( sk56 @ E
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F )
| ~ ( abstract @ E @ F )
| ~ ( sk64 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk59 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( sk56 @ A
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( C @ I ) @ ( D @ I ) )
@ B
@ A ) )
!= A )
| ( ( H
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [I: traffic] : ( abstract @ ( G @ I ) @ ( H @ I ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) ) ),
inference(pre_uni,[status(thm)],[1168:[]]) ).
thf(1269,plain,
! [P: traffic > traffic,O: traffic > traffic,N: traffic,M: traffic,L: traffic > traffic,K: traffic > traffic,J: traffic,I: traffic,H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( sk64 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk59 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk56 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( abstract @ E @ F )
| ~ ( sk64 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk59 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk56 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( H
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) )
| ( abstract @ ( O @ N ) @ ( P @ N ) )
| ~ ( sk64 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk59 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk56 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( abstract @ M @ N )
| ~ ( sk64 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk59 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk56 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ $true
| ~ ( abstract @ I @ J )
| ( ( L
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( L
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( P
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( P
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( L @ J )
!= ( P @ M ) )
| ( ( K @ J )
!= ( O @ M ) )
| ( ( abstract @ ( G @ F ) @ ( H @ F ) )
!= ( abstract @ ( K @ I ) @ ( L @ I ) ) ) ),
inference(paramod_ordered,[status(thm)],[1169,1169]) ).
thf(1270,plain,
! [P: traffic > traffic,O: traffic > traffic,N: traffic,M: traffic,L: traffic > traffic,K: traffic > traffic,J: traffic,I: traffic,H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( sk64 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk59 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk56 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( abstract @ E @ F )
| ~ ( sk64 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk59 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk56 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( H
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) )
| ( abstract @ ( O @ N ) @ ( P @ N ) )
| ~ ( sk64 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk59 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk56 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( abstract @ M @ N )
| ~ ( sk64 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk59 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk56 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( abstract @ I @ J )
| ( ( L
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( L
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( P
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( P
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( L @ J )
!= ( P @ M ) )
| ( ( K @ J )
!= ( O @ M ) )
| ( ( abstract @ ( G @ F ) @ ( H @ F ) )
!= ( abstract @ ( K @ I ) @ ( L @ I ) ) ) ),
inference(simp,[status(thm)],[1269]) ).
thf(1449,plain,
! [P: traffic > traffic,O: traffic > traffic,N: traffic,M: traffic,L: traffic > traffic,K: traffic > traffic,J: traffic,I: traffic,H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( sk64 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk59 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk56 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( abstract @ E @ F )
| ~ ( sk64 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk59 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk56 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( abstract @ A @ B )
| ( ( D
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( H
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) )
| ( abstract @ ( O @ N ) @ ( P @ N ) )
| ~ ( sk64 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk59 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk56 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( abstract @ M @ N )
| ~ ( sk64 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk59 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk56 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( abstract @ I @ J )
| ( ( L
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( L
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( P
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( P
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( L @ J )
!= ( P @ M ) )
| ( ( K @ J )
!= ( O @ M ) )
| ( ( H @ F )
!= ( L @ I ) )
| ( ( G @ F )
!= ( K @ I ) ) ),
inference(pre_uni,[status(thm)],[1270:[]]) ).
thf(1450,plain,
! [P: traffic > traffic,O: traffic > traffic,N: traffic,M: traffic,L: traffic > traffic,K: traffic > traffic,J: traffic,I: traffic,H: traffic > traffic,G: traffic > traffic,F: traffic,E: traffic,D: traffic > traffic,C: traffic > traffic,B: traffic,A: traffic] :
( ~ ( abstract @ I @ J )
| ~ ( sk56 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk59 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( sk64 @ I
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J )
| ~ ( abstract @ M @ N )
| ~ ( sk56 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk59 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ~ ( sk64 @ M
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N )
| ( abstract @ ( O @ N ) @ ( P @ N ) )
| ~ ( abstract @ A @ B )
| ~ ( abstract @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk56 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk59 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( sk64 @ A
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B )
| ~ ( abstract @ E @ F )
| ~ ( sk56 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk59 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ~ ( sk64 @ E
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F )
| ( ( D
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( D
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= B )
| ( ( C
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( C @ Q ) @ ( D @ Q ) )
@ B
@ A ) )
!= A )
| ( ( H
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( H
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= F )
| ( ( G
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( G @ Q ) @ ( H @ Q ) )
@ F
@ E ) )
!= E )
| ( ( D @ B )
!= ( H @ E ) )
| ( ( C @ B )
!= ( G @ E ) )
| ( ( L
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( L
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= J )
| ( ( K
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( K @ Q ) @ ( L @ Q ) )
@ J
@ I ) )
!= I )
| ( ( P
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk72
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( P
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= N )
| ( ( O
@ ( sk69
@ ^ [Q: traffic] : ( abstract @ ( O @ Q ) @ ( P @ Q ) )
@ N
@ M ) )
!= M )
| ( ( L @ J )
!= ( P @ M ) )
| ( ( K @ J )
!= ( O @ M ) )
| ( ( H @ F )
!= ( L @ I ) )
| ( ( G @ F )
!= ( K @ I ) ) ),
inference(pre_uni,[status(thm)],[1449:[]]) ).
thf(83,axiom,
! [A: traffic] : ( abstract @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_traffic_Oabstract_Orefl) ).
thf(484,plain,
! [A: traffic] : ( abstract @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(485,plain,
! [A: traffic] : ( abstract @ A @ A ),
inference(cnf,[status(esa)],[484]) ).
thf(67,axiom,
! [A: $o] :
( ( A
= ( product_Unity = product_Unity ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_eq__sym__Unity__conv) ).
thf(348,plain,
$true,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(6822,plain,
! [C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( B
!= ( move @ ts3 @ ts_a @ v ) )
| ( ts3 != ts )
| ( ( move @ A @ A @ B )
!= ( move @ C @ C @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,6017]) ).
thf(6823,plain,
( ( ( move @ ts3 @ ts_a @ v )
!= v )
| ( ts3 != ts ) ),
inference(pattern_uni,[status(thm)],[6822:[bind(A,$thf( A )),bind(B,$thf( v )),bind(C,$thf( A ))]]) ).
thf(86,axiom,
! [A: real,B: real,C: real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ord_less_eq_real @ ( minus_minus_real @ A @ D ) @ ( minus_minus_real @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_diff__mono) ).
thf(492,plain,
! [A: real,B: real,C: real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ord_less_eq_real @ ( minus_minus_real @ A @ D ) @ ( minus_minus_real @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(12,axiom,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_order_Otrans) ).
thf(164,plain,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(33,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_local_Ohmlsl_Oat__hchop__dist1) ).
thf(221,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(51,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( hchop @ B @ D @ E ) )
=> ? [F: view_e774982825t_unit] :
( ( hchop @ A @ D @ F )
& ( hchop @ F @ E @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_view_Ohorizontal__chop__assoc2) ).
thf(293,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( hchop @ B @ D @ E ) )
=> ? [F: view_e774982825t_unit] :
( ( hchop @ A @ D @ F )
& ( hchop @ F @ E @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(107,axiom,
? [A: cars] : ( create_reservation @ ts_a @ A @ ts ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_cr__res_Ohyps_I2_J) ).
thf(579,plain,
? [A: cars] : ( create_reservation @ ts_a @ A @ ts ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(580,plain,
create_reservation @ ts_a @ sk104 @ ts,
inference(cnf,[status(esa)],[579]) ).
thf(7327,plain,
! [C: traffic,B: cars,A: traffic] :
( ~ $true
| ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ C @ B ) )
| ( ( create_reservation @ ts_a @ sk104 @ ts )
!= ( create_reservation @ A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[580,186]) ).
thf(7328,plain,
! [C: traffic,B: cars,A: traffic] :
( ( ord_less_eq_nat_int @ ( res @ A @ B ) @ ( res @ C @ B ) )
| ( ( create_reservation @ ts_a @ sk104 @ ts )
!= ( create_reservation @ A @ B @ C ) ) ),
inference(simp,[status(thm)],[7327]) ).
thf(7329,plain,
ord_less_eq_nat_int @ ( res @ ts_a @ sk104 ) @ ( res @ ts @ sk104 ),
inference(pattern_uni,[status(thm)],[7328:[bind(A,$thf( ts_a )),bind(B,$thf( sk104 )),bind(C,$thf( ts ))]]) ).
thf(18,axiom,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ B @ A )
& ( ord_less_eq_nat_int @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_dual__order_Oeq__iff) ).
thf(181,plain,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ B @ A )
& ( ord_less_eq_nat_int @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(182,plain,
( ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ B @ A )
& ( ord_less_eq_nat_int @ A @ B ) ) )
= ( (=) @ nat_int ) ),
inference(lifteq,[status(thm)],[181]) ).
thf(633,plain,
! [B: nat_int,A: nat_int] :
( ( ( ord_less_eq_nat_int @ B @ A )
& ( ord_less_eq_nat_int @ A @ B ) )
= ( A = B ) ),
inference(func_ext,[status(esa)],[182]) ).
thf(9378,plain,
! [B: nat_int,A: nat_int] :
( ( ( $true
& ( ord_less_eq_nat_int @ A @ B ) )
= ( A = B ) )
| ( ( ord_less_eq_nat_int @ ( res @ ts_a @ sk104 ) @ ( res @ ts @ sk104 ) )
!= ( ord_less_eq_nat_int @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7329,633]) ).
thf(9379,plain,
! [B: nat_int,A: nat_int] :
( ( ( ord_less_eq_nat_int @ A @ B )
= ( A = B ) )
| ( ( ord_less_eq_nat_int @ ( res @ ts_a @ sk104 ) @ ( res @ ts @ sk104 ) )
!= ( ord_less_eq_nat_int @ B @ A ) ) ),
inference(simp,[status(thm)],[9378]) ).
thf(9380,plain,
( ( ord_less_eq_nat_int @ ( res @ ts @ sk104 ) @ ( res @ ts_a @ sk104 ) )
= ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) ) ),
inference(pattern_uni,[status(thm)],[9379:[bind(A,$thf( res @ ts @ sk104 )),bind(B,$thf( res @ ts_a @ sk104 ))]]) ).
thf(9375,plain,
! [B: nat_int,A: nat_int] :
( ( ( ( ord_less_eq_nat_int @ B @ A )
& $true )
= ( A = B ) )
| ( ( ord_less_eq_nat_int @ ( res @ ts_a @ sk104 ) @ ( res @ ts @ sk104 ) )
!= ( ord_less_eq_nat_int @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7329,633]) ).
thf(9376,plain,
! [B: nat_int,A: nat_int] :
( ( ( ord_less_eq_nat_int @ B @ A )
= ( A = B ) )
| ( ( ord_less_eq_nat_int @ ( res @ ts_a @ sk104 ) @ ( res @ ts @ sk104 ) )
!= ( ord_less_eq_nat_int @ A @ B ) ) ),
inference(simp,[status(thm)],[9375]) ).
thf(9377,plain,
( ( ord_less_eq_nat_int @ ( res @ ts @ sk104 ) @ ( res @ ts_a @ sk104 ) )
= ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) ) ),
inference(pattern_uni,[status(thm)],[9376:[bind(A,$thf( res @ ts_a @ sk104 )),bind(B,$thf( res @ ts @ sk104 ))]]) ).
thf(9743,plain,
( ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) )
= ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) ) ),
inference(rewrite,[status(thm)],[9380,9377]) ).
thf(5,axiom,
! [A: nat_int] : ( ord_less_eq_nat_int @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_order__refl) ).
thf(131,plain,
! [A: nat_int] : ( ord_less_eq_nat_int @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(132,plain,
! [A: nat_int] : ( ord_less_eq_nat_int @ A @ A ),
inference(cnf,[status(esa)],[131]) ).
thf(6,axiom,
! [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ ( B @ C ) )
=> ( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_order__subst1) ).
thf(133,plain,
! [A: nat_int,B: nat_int > nat_int,C: nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ ( B @ C ) )
=> ( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(43,axiom,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit,C: view_e774982825t_unit] : ( hchop @ A @ B @ C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_view_Ohorizontal__chop1) ).
thf(265,plain,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit,C: view_e774982825t_unit] : ( hchop @ A @ B @ C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(7640,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( own_Product_unit @ A ) @ ( sk81 @ A ) )
= A ),
inference(rewrite,[status(thm)],[489,7633]) ).
thf(7610,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( lan_Product_unit @ A )
= C )
| ( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ ( sk81 @ A ) )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[489,472]) ).
thf(7611,plain,
! [A: view_e774982825t_unit] :
( ( sk79 @ A )
= ( lan_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[7610:[bind(A,$thf( I )),bind(B,$thf( sk78 @ I )),bind(C,$thf( sk79 @ I )),bind(D,$thf( sk80 @ I )),bind(E,$thf( sk81 @ I ))]]) ).
thf(7635,plain,
! [A: view_e774982825t_unit] :
( ( sk79 @ A )
= ( lan_Product_unit @ A ) ),
inference(simp,[status(thm)],[7611]) ).
thf(7614,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= B )
| ( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ ( sk81 @ A ) )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[489,542]) ).
thf(7615,plain,
! [A: view_e774982825t_unit] :
( ( sk78 @ A )
= ( ext_Product_unit @ A ) ),
inference(pattern_uni,[status(thm)],[7614:[bind(A,$thf( I )),bind(B,$thf( sk78 @ I )),bind(C,$thf( sk79 @ I )),bind(D,$thf( sk80 @ I )),bind(E,$thf( sk81 @ I ))]]) ).
thf(7639,plain,
! [A: view_e774982825t_unit] :
( ( sk78 @ A )
= ( ext_Product_unit @ A ) ),
inference(simp,[status(thm)],[7615]) ).
thf(9024,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( ext_Product_unit @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ ( sk81 @ A ) )
= A ),
inference(rewrite,[status(thm)],[7640,7635,7639]) ).
thf(26,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) )
=> ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_local_Ohmlsl_Oat__neg2) ).
thf(206,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) )
=> ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(56,axiom,
! [A: real_int] :
? [B: real_int] : ( real_R_Chop @ A @ A @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_chop__singleton__right) ).
thf(306,plain,
! [A: real_int] :
? [B: real_int] : ( real_R_Chop @ A @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(307,plain,
! [A: real_int] : ( real_R_Chop @ A @ A @ ( sk44 @ A ) ),
inference(cnf,[status(esa)],[306]) ).
thf(39,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( ( B @ D @ F )
| ( C @ D @ F ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( B @ D @ F ) )
| ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( C @ D @ F ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_local_Ohmlsl_Oat__disj__dist) ).
thf(248,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( ( B @ D @ F )
| ( C @ D @ F ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( B @ D @ F ) )
| ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( C @ D @ F ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(95,axiom,
! [A: view_e774982825t_unit > $o,B: view_e774982825t_unit] :
( ! [C: real_int,D: nat_int,E: cars,F: product_unit] : ( A @ ( view_e912666823t_unit @ C @ D @ E @ F ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_induct__scheme) ).
thf(546,plain,
! [A: view_e774982825t_unit > $o,B: view_e774982825t_unit] :
( ! [C: real_int,D: nat_int,E: cars,F: product_unit] : ( A @ ( view_e912666823t_unit @ C @ D @ E @ F ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(24,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ~ ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ( A @ B @ D ) )
=> ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ~ ( A @ B @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_local_Ohmlsl_Ohchop__neg1) ).
thf(197,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ~ ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ( A @ B @ D ) )
=> ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ~ ( A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(198,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ( hchop @ C @ ( sk11 @ C @ B @ A ) @ ( sk12 @ C @ B @ A ) ) )
& ( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ~ ( A @ B @ ( sk11 @ C @ B @ A ) ) )
& ( ( A @ B @ ( sk9 @ C @ B @ A ) )
| ( hchop @ C @ ( sk11 @ C @ B @ A ) @ ( sk12 @ C @ B @ A ) ) )
& ( ( A @ B @ ( sk9 @ C @ B @ A ) )
| ~ ( A @ B @ ( sk11 @ C @ B @ A ) ) ) ),
inference(cnf,[status(esa)],[197]) ).
thf(201,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( A @ B @ ( sk9 @ C @ B @ A ) )
| ( hchop @ C @ ( sk11 @ C @ B @ A ) @ ( sk12 @ C @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(52,axiom,
! [A: view_e774982825t_unit,B: cars] :
? [C: view_e774982825t_unit] : ( switch @ A @ B @ C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_view_Oswitch__always__exists) ).
thf(297,plain,
! [A: view_e774982825t_unit,B: cars] :
? [C: view_e774982825t_unit] : ( switch @ A @ B @ C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(22,axiom,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
= ( B = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_antisym__conv) ).
thf(192,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
= ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(134,plain,
! [A: nat_int,B: nat_int > nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ ( B @ C ) )
=> ! [D: nat_int] :
( ( ord_less_eq_nat_int @ C @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ) ),
inference(miniscope,[status(thm)],[133]) ).
thf(135,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( ~ ( ord_less_eq_nat_int @ A @ ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ( ord_less_eq_nat_int @ ( sk3 @ D @ C @ B @ A ) @ ( sk4 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) )
& ( ~ ( ord_less_eq_nat_int @ A @ ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ~ ( ord_less_eq_nat_int @ ( B @ ( sk3 @ D @ C @ B @ A ) ) @ ( B @ ( sk4 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ) ),
inference(cnf,[status(esa)],[134]) ).
thf(137,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ~ ( ord_less_eq_nat_int @ ( B @ ( sk3 @ D @ C @ B @ A ) ) @ ( B @ ( sk4 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(cnfConj,[status(thm)],[135]) ).
thf(71,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars] : ( create_reservation @ B @ D @ C )
=> ( abstract @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_traffic_Ocr__res) ).
thf(361,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars] : ( create_reservation @ B @ D @ C )
=> ( abstract @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(96,axiom,
! [A: real_int,B: nat_int,C: cars,D: product_unit,E: real_int,F: nat_int,G: cars,H: product_unit] :
( ( ( view_e912666823t_unit @ A @ B @ C @ D )
= ( view_e912666823t_unit @ E @ F @ G @ H ) )
= ( ( A = E )
& ( B = F )
& ( C = G )
& ( D = H ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_ext__inject) ).
thf(551,plain,
! [A: real_int,B: nat_int,C: cars,D: product_unit,E: real_int,F: nat_int,G: cars,H: product_unit] :
( ( ( view_e912666823t_unit @ A @ B @ C @ D )
= ( view_e912666823t_unit @ E @ F @ G @ H ) )
= ( ( A = E )
& ( B = F )
& ( C = G )
& ( D = H ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(74,axiom,
( hchop
= ( ^ [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( real_R_Chop @ ( ext_Product_unit @ A ) @ ( ext_Product_unit @ B ) @ ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_view_Ohchop__def) ).
thf(456,plain,
( hchop
= ( ^ [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( real_R_Chop @ ( ext_Product_unit @ A ) @ ( ext_Product_unit @ B ) @ ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(102,axiom,
! [A: traffic,B: cars,C: nat,D: traffic,E: view_e774982825t_unit] :
( ( withdraw_reservation @ A @ B @ C @ D )
=> ( ( move @ A @ D @ E )
= E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_traffic_Omove__stability__wdr) ).
thf(566,plain,
! [A: traffic,B: cars,C: nat,D: traffic,E: view_e774982825t_unit] :
( ( withdraw_reservation @ A @ B @ C @ D )
=> ( ( move @ A @ D @ E )
= E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(6824,plain,
! [C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( B
!= ( move @ C @ C @ v ) )
| ( ts3 != ts )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,6017]) ).
thf(6826,plain,
! [B: traffic,A: traffic] :
( ( ts3 != ts )
| ( ( move @ A @ A @ ( move @ B @ B @ v ) )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(simp,[status(thm)],[6824]) ).
thf(6833,plain,
! [B: traffic,A: traffic] :
( ( ts3 != ts )
| ( ( move @ A @ A @ ( move @ B @ B @ v ) )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(simp,[status(thm)],[6826]) ).
thf(76,axiom,
! [A: traffic,B: cars,C: nat,D: traffic,E: cars] :
( ( create_claim @ A @ B @ C @ D )
=> ( ( res @ A @ E )
= ( res @ D @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_traffic_Ocreate__clm__eq__res) ).
thf(461,plain,
! [A: traffic,B: cars,C: nat,D: traffic,E: cars] :
( ( create_claim @ A @ B @ C @ D )
=> ( ( res @ A @ E )
= ( res @ D @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(112,axiom,
! [A: traffic,B: traffic,C: traffic,D: view_e774982825t_unit] :
( ( ( abstract @ A @ B )
& ( abstract @ B @ C ) )
=> ( ( move @ B @ C @ ( move @ A @ B @ D ) )
= ( move @ A @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_traffic_Omove__trans) ).
thf(593,plain,
! [A: traffic,B: traffic,C: traffic,D: view_e774982825t_unit] :
( ( ( abstract @ A @ B )
& ( abstract @ B @ C ) )
=> ( ( move @ B @ C @ ( move @ A @ B @ D ) )
= ( move @ A @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(65,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ~ ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ( A @ B @ E ) )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ~ ( A @ B @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_local_Ohmlsl_Ohchop__neg2) ).
thf(339,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ~ ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ( A @ B @ E ) )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ~ ( A @ B @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(97,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars,E: nat] : ( withdraw_reservation @ B @ D @ E @ C )
=> ( abstract @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_traffic_Owd__res) ).
thf(554,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars,E: nat] : ( withdraw_reservation @ B @ D @ E @ C )
=> ( abstract @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(457,plain,
( hchop
= ( ^ [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( real_R_Chop @ ( ext_Product_unit @ A ) @ ( ext_Product_unit @ B ) @ ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ B ) ) ) ) ),
inference(lifteq,[status(thm)],[456]) ).
thf(69,axiom,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( more_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= D ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_select__convs_I4_J) ).
thf(355,plain,
! [A: real_int,B: nat_int,C: cars,D: product_unit] :
( ( more_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= D ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(356,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( more_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= D ),
inference(cnf,[status(esa)],[355]) ).
thf(357,plain,
! [D: product_unit,C: cars,B: nat_int,A: real_int] :
( ( more_Product_unit @ ( view_e912666823t_unit @ A @ B @ C @ D ) )
= D ),
inference(lifteq,[status(thm)],[356]) ).
thf(6216,plain,
! [E: product_unit,D: cars,C: nat_int,B: real_int,A: view_e774982825t_unit] :
( ( ( more_Product_unit @ A )
= E )
| ( ( view_e912666823t_unit @ ( sk96 @ A ) @ ( sk97 @ A ) @ ( sk98 @ A ) @ defaul1399868459t_unit )
!= ( view_e912666823t_unit @ B @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[6204,357]) ).
thf(6217,plain,
! [A: view_e774982825t_unit] :
( ( more_Product_unit @ A )
= defaul1399868459t_unit ),
inference(pattern_uni,[status(thm)],[6216:[bind(A,$thf( H )),bind(B,$thf( sk96 @ H )),bind(C,$thf( sk97 @ H )),bind(D,$thf( sk98 @ H )),bind(E,$thf( defaul1399868459t_unit ))]]) ).
thf(6224,plain,
! [A: view_e774982825t_unit] :
( ( more_Product_unit @ A )
= defaul1399868459t_unit ),
inference(simp,[status(thm)],[6217]) ).
thf(7317,plain,
( hchop
= ( ^ [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( real_R_Chop @ ( ext_Product_unit @ A ) @ ( ext_Product_unit @ B ) @ ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ C ) )
& ( defaul1399868459t_unit = defaul1399868459t_unit )
& ( defaul1399868459t_unit = defaul1399868459t_unit ) ) ) ),
inference(rewrite,[status(thm)],[457,6224]) ).
thf(7318,plain,
( hchop
= ( ^ [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( real_R_Chop @ ( ext_Product_unit @ A ) @ ( ext_Product_unit @ B ) @ ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
& ( ( own_Product_unit @ A )
= ( own_Product_unit @ C ) ) ) ) ),
inference(simp,[status(thm)],[7317]) ).
thf(81,axiom,
! [A: view_e774982825t_unit > $o,B: view_e774982825t_unit] :
( ! [C: real_int,D: nat_int,E: cars] : ( A @ ( view_e912666823t_unit @ C @ D @ E @ product_Unity ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_induct) ).
thf(476,plain,
! [A: view_e774982825t_unit > $o,B: view_e774982825t_unit] :
( ! [C: real_int,D: nat_int,E: cars] : ( A @ ( view_e912666823t_unit @ C @ D @ E @ product_Unity ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(104,axiom,
! [A: traffic,B: traffic] :
( lan_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( lan_Product_unit @ ( move @ A @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_traffic_Omove__keeps__lanes) ).
thf(572,plain,
! [A: traffic,B: traffic] :
( lan_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( lan_Product_unit @ ( move @ A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(573,plain,
! [B: traffic,A: traffic] :
( lan_Product_unit
= ( ^ [C: view_e774982825t_unit] : ( lan_Product_unit @ ( move @ A @ B @ C ) ) ) ),
inference(cnf,[status(esa)],[572]) ).
thf(574,plain,
! [B: traffic,A: traffic] :
( ( ^ [C: view_e774982825t_unit] : ( lan_Product_unit @ ( move @ A @ B @ C ) ) )
= lan_Product_unit ),
inference(lifteq,[status(thm)],[573]) ).
thf(1099,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic] :
( ( lan_Product_unit @ ( move @ A @ B @ C ) )
= ( lan_Product_unit @ C ) ),
inference(func_ext,[status(esa)],[574]) ).
thf(15,axiom,
! [A: nat_int] : ( ord_less_eq_nat_int @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_dual__order_Orefl) ).
thf(173,plain,
! [A: nat_int] : ( ord_less_eq_nat_int @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(4355,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ A )
| ( ( B @ C )
!= ( ~ ( B @ defaul1399868459t_unit ) ) )
| ( defaul1399868459t_unit != defaul1399868459t_unit ) ),
inference(paramod_ordered,[status(thm)],[615,3874]) ).
thf(4356,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ A )
| ( ( B @ C )
!= ( ~ ( B @ defaul1399868459t_unit ) ) ) ),
inference(pattern_uni,[status(thm)],[4355:[]]) ).
thf(9790,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ A )
| ( ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) )
!= ( ~ ( B @ defaul1399868459t_unit ) ) )
| ( ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) )
!= ( B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[9743,4356]) ).
thf(9826,plain,
( ( ( res @ ts @ sk104 )
!= ( res @ ts_a @ sk104 ) )
| ( ( ( res @ ts @ sk104 )
!= ( res @ ts_a @ sk104 ) )
!= ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) ) ) ),
inference(pre_uni,[status(thm)],[9790:[bind(A,$thf( A )),bind(B,$thf( ^ [D: product_unit] : ( ( res @ ts @ sk104 ) = ( res @ ts_a @ sk104 ) ) )),bind(C,$thf( C ))]]) ).
thf(9846,plain,
( ( ( res @ ts_a @ sk104 )
!= ( res @ ts @ sk104 ) )
| ( ( ( res @ ts @ sk104 )
!= ( res @ ts_a @ sk104 ) )
!= ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) ) ) ),
inference(lifteq,[status(thm)],[9826]) ).
thf(4,axiom,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ C @ A )
=> ( ord_less_eq_nat_int @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_dual__order_Otrans) ).
thf(128,plain,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ C @ A )
=> ( ord_less_eq_nat_int @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(38,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( hchop @ C @ D @ E ) )
=> ? [F: view_e774982825t_unit] :
( ( hchop @ A @ F @ E )
& ( hchop @ F @ B @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_view_Ohorizontal__chop__assoc1) ).
thf(244,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( hchop @ C @ D @ E ) )
=> ? [F: view_e774982825t_unit] :
( ( hchop @ A @ F @ E )
& ( hchop @ F @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(266,plain,
! [A: view_e774982825t_unit] : ( hchop @ A @ ( sk33 @ A ) @ ( sk34 @ A ) ),
inference(cnf,[status(esa)],[265]) ).
thf(89,axiom,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( ( create_reservation @ A @ B @ C )
& ( B != D ) )
=> ( ( res @ A @ D )
= ( res @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_traffic_Ocreate__res__subseteq1__neq) ).
thf(508,plain,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( ( create_reservation @ A @ B @ C )
& ( B != D ) )
=> ( ( res @ A @ D )
= ( res @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(58,axiom,
! [A: real_int] :
? [B: real_int,C: real_int] : ( real_R_Chop @ A @ B @ C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_real__int__class_Ochop__always__possible) ).
thf(310,plain,
! [A: real_int] :
? [B: real_int,C: real_int] : ( real_R_Chop @ A @ B @ C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(311,plain,
! [A: real_int] : ( real_R_Chop @ A @ ( sk46 @ A ) @ ( sk47 @ A ) ),
inference(cnf,[status(esa)],[310]) ).
thf(110,axiom,
! [A: traffic,B: cars,C: traffic,D: view_e774982825t_unit] :
( ( withdraw_claim @ A @ B @ C )
=> ( ( move @ A @ C @ D )
= D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_traffic_Omove__stability__wdc) ).
thf(586,plain,
! [A: traffic,B: cars,C: traffic,D: view_e774982825t_unit] :
( ( withdraw_claim @ A @ B @ C )
=> ( ( move @ A @ C @ D )
= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(298,plain,
! [B: cars,A: view_e774982825t_unit] : ( switch @ A @ B @ ( sk42 @ B @ A ) ),
inference(cnf,[status(esa)],[297]) ).
thf(165,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ! [C: nat_int] :
( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
inference(miniscope,[status(thm)],[164]) ).
thf(166,plain,
! [C: nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ B @ C )
| ( ord_less_eq_nat_int @ A @ C ) ),
inference(cnf,[status(esa)],[165]) ).
thf(143,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ! [C: nat_int > nat_int,D: nat_int] :
( ( ( C @ B )
= D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
inference(miniscope,[status(thm)],[142]) ).
thf(144,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ( C @ B )
!= D )
| ( ord_less_eq_nat_int @ ( sk5 @ D @ C @ B @ A ) @ ( sk6 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) )
& ( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ( C @ B )
!= D )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk5 @ D @ C @ B @ A ) ) @ ( C @ ( sk6 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ),
inference(cnf,[status(esa)],[143]) ).
thf(145,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ( C @ B )
!= D )
| ( ord_less_eq_nat_int @ ( sk5 @ D @ C @ B @ A ) @ ( sk6 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(cnfConj,[status(thm)],[144]) ).
thf(147,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ( ( C @ B )
!= D )
| ~ ( ord_less_eq_nat_int @ A @ B )
| ( ord_less_eq_nat_int @ ( sk5 @ D @ C @ B @ A ) @ ( sk6 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(lifteq,[status(thm)],[145]) ).
thf(148,plain,
! [C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ord_less_eq_nat_int @ ( sk5 @ ( C @ B ) @ C @ B @ A ) @ ( sk6 @ ( C @ B ) @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ ( C @ B ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(114,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ! [D: traffic] :
( ( abstract @ B @ D )
=> ( A @ D @ ( move @ B @ D @ C ) ) )
=> ( A @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_local_Ohmlsl_Oglobally__refl) ).
thf(601,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ! [D: traffic] :
( ( abstract @ B @ D )
=> ( A @ D @ ( move @ B @ D @ C ) ) )
=> ( A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(21,axiom,
! [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ ( C @ B ) @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_order__subst2) ).
thf(187,plain,
! [A: nat_int,B: nat_int,C: nat_int > nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ ( C @ B ) @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(188,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ! [C: nat_int > nat_int,D: nat_int] :
( ( ord_less_eq_nat_int @ ( C @ B ) @ D )
=> ( ! [E: nat_int,F: nat_int] :
( ( ord_less_eq_nat_int @ E @ F )
=> ( ord_less_eq_nat_int @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ) ),
inference(miniscope,[status(thm)],[187]) ).
thf(189,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ B ) @ D )
| ( ord_less_eq_nat_int @ ( sk7 @ D @ C @ B @ A ) @ ( sk8 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) )
& ( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ B ) @ D )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk7 @ D @ C @ B @ A ) ) @ ( C @ ( sk8 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ) ),
inference(cnf,[status(esa)],[188]) ).
thf(191,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ B ) @ D )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk7 @ D @ C @ B @ A ) ) @ ( C @ ( sk8 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(200,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ~ ( A @ B @ ( sk11 @ C @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(11112,plain,
! [B: view_e774982825t_unit,A: traffic] :
( ( hchop @ B
@ ( sk9 @ B @ A
@ ^ [C: traffic,D: view_e774982825t_unit] : $true )
@ ( sk10 @ B @ A
@ ^ [C: traffic,D: view_e774982825t_unit] : $true ) )
| ~ $true ),
inference(prim_subst,[status(thm)],[200:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : $true ))]]) ).
thf(11254,plain,
! [B: view_e774982825t_unit,A: traffic] :
( hchop @ B
@ ( sk9 @ B @ A
@ ^ [C: traffic,D: view_e774982825t_unit] : $true )
@ ( sk10 @ B @ A
@ ^ [C: traffic,D: view_e774982825t_unit] : $true ) ),
inference(simp,[status(thm)],[11112]) ).
thf(42,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: cars] :
( ( ( hchop @ A @ B @ C )
& ( switch @ D @ E @ A ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( switch @ F @ E @ B )
& ( switch @ G @ E @ C )
& ( hchop @ D @ F @ G ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_view_Oswitch__hchop2) ).
thf(259,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: view_e774982825t_unit,E: cars] :
( ( ( hchop @ A @ B @ C )
& ( switch @ D @ E @ A ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( switch @ F @ E @ B )
& ( switch @ G @ E @ C )
& ( hchop @ D @ F @ G ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(50,axiom,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( switch @ A @ B @ C )
=> ( switch @ C @ ( own_Product_unit @ A ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_view_Oswitch__symm) ).
thf(291,plain,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( switch @ A @ B @ C )
=> ( switch @ C @ ( own_Product_unit @ A ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(105,axiom,
abstract @ ts3 @ ts_a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_cr__res_Ohyps_I1_J) ).
thf(575,plain,
abstract @ ts3 @ ts_a,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(11083,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ~ $true
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( abstract @ ts3 @ ts_a ) ) ),
inference(paramod_ordered,[status(thm)],[575,200]) ).
thf(11084,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( abstract @ ts3 @ ts_a ) ) ),
inference(simp,[status(thm)],[11083]) ).
thf(11185,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts_a ) )
@ ( sk10 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts_a ) ) ),
inference(pre_uni,[status(thm)],[11084:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( abstract @ D @ ts_a ) )),bind(B,$thf( ts3 )),bind(C,$thf( C ))]]) ).
thf(11301,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts_a ) )
@ ( sk10 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts_a ) ) ),
inference(simp,[status(thm)],[11185]) ).
thf(88,axiom,
! [A: product_unit > $o,B: product_unit > $o] :
( ( ( A @ product_Unity )
=> ( B @ product_Unity ) )
=> ! [C: product_unit] :
( ( A @ C )
=> ( B @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_unit__all__impI) ).
thf(498,plain,
! [A: product_unit > $o,B: product_unit > $o] :
( ( ( A @ product_Unity )
=> ( B @ product_Unity ) )
=> ! [C: product_unit] :
( ( A @ C )
=> ( B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(36,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ? [F: view_e774982825t_unit] :
( ? [G: view_e774982825t_unit] : ( hchop @ E @ F @ G )
& ( A @ B @ F ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_local_Ohmlsl_Ohchop__weaken) ).
thf(236,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ? [F: view_e774982825t_unit] :
( ? [G: view_e774982825t_unit] : ( hchop @ E @ F @ G )
& ( A @ B @ F ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(7616,plain,
! [B: view_e774982825t_unit,A: product_unit] :
( ( ( view_e912666823t_unit @ ( sk78 @ B ) @ ( sk79 @ B ) @ ( sk80 @ B ) @ defaul1399868459t_unit )
= B )
| ( A
!= ( sk81 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[615,489]) ).
thf(7617,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ defaul1399868459t_unit )
= A ),
inference(pattern_uni,[status(thm)],[7616:[bind(A,$thf( sk81 @ C )),bind(B,$thf( C ))]]) ).
thf(7630,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( sk78 @ A ) @ ( sk79 @ A ) @ ( sk80 @ A ) @ defaul1399868459t_unit )
= A ),
inference(simp,[status(thm)],[7617]) ).
thf(8202,plain,
! [A: view_e774982825t_unit] :
( ( view_e912666823t_unit @ ( ext_Product_unit @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ defaul1399868459t_unit )
= A ),
inference(rewrite,[status(thm)],[7630,7633,7635,7639]) ).
thf(11,axiom,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( B = C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_ord__le__eq__trans) ).
thf(159,plain,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( B = C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(171,plain,
! [B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ B @ A )
| ( A = B ) ),
inference(cnf,[status(esa)],[170]) ).
thf(172,plain,
! [B: nat_int,A: nat_int] :
( ( A = B )
| ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ B @ A ) ),
inference(lifteq,[status(thm)],[171]) ).
thf(32,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: cars] :
! [E: view_e774982825t_unit] :
( ( switch @ C @ D @ E )
=> ( A @ B @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_local_Ohmlsl_Oat__exists) ).
thf(219,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: cars] :
! [E: view_e774982825t_unit] :
( ( switch @ C @ D @ E )
=> ( A @ B @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(46,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) )
=> ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_local_Ohmlsl_Oat__neg__neg2) ).
thf(274,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) )
=> ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(34,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ( A @ B @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_local_Ohmlsl_Ohchop__weaken2) ).
thf(230,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit,E: view_e774982825t_unit] :
( ( hchop @ C @ D @ E )
& ( A @ B @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(45,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( hchop @ A @ B @ C )
=> ( ( own_Product_unit @ B )
= ( own_Product_unit @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_view_Ohorizontal__chop__own__trans) ).
thf(271,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit] :
( ( hchop @ A @ B @ C )
=> ( ( own_Product_unit @ B )
= ( own_Product_unit @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(27,axiom,
! [A: view_e774982825t_unit] :
? [B: cars,C: view_e774982825t_unit] : ( switch @ A @ B @ C ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_view_Oswitch__exists) ).
thf(208,plain,
! [A: view_e774982825t_unit] :
? [B: cars,C: view_e774982825t_unit] : ( switch @ A @ B @ C ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(66,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( ( A @ D @ F )
| ( B @ D @ F ) )
& ( C @ D @ G ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( C @ D @ G ) )
| ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( B @ D @ F )
& ( C @ D @ G ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_local_Ohmlsl_Ohchop__disj__distr2) ).
thf(345,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( ( A @ D @ F )
| ( B @ D @ F ) )
& ( C @ D @ G ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( C @ D @ G ) )
| ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( B @ D @ F )
& ( C @ D @ G ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(29,axiom,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ C @ D @ E ) )
=> ( switch @ A @ D @ E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_view_Oswitch__trans) ).
thf(213,plain,
! [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( switch @ A @ B @ C )
& ( switch @ C @ D @ E ) )
=> ( switch @ A @ D @ E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(40,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( switch @ A @ D @ E ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( switch @ B @ D @ F )
& ( switch @ C @ D @ G )
& ( hchop @ E @ F @ G ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_view_Oswitch__hchop1) ).
thf(251,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit,C: view_e774982825t_unit,D: cars,E: view_e774982825t_unit] :
( ( ( hchop @ A @ B @ C )
& ( switch @ A @ D @ E ) )
=> ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( switch @ B @ D @ F )
& ( switch @ C @ D @ G )
& ( hchop @ E @ F @ G ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(62,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) )
= ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_local_Ohmlsl_Oat__neg) ).
thf(330,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) )
= ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(53,axiom,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( switch @ B @ ( own_Product_unit @ A ) @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_view_Oswitch__origin) ).
thf(299,plain,
! [A: view_e774982825t_unit] :
? [B: view_e774982825t_unit] : ( switch @ B @ ( own_Product_unit @ A ) @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(44,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ( A @ B @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_local_Ohmlsl_Ohchop__weaken1) ).
thf(267,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ( A @ B @ C )
=> ? [D: view_e774982825t_unit] :
( ? [E: view_e774982825t_unit] : ( hchop @ C @ D @ E )
& ( A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(37,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( ( B @ D @ F )
& ( C @ D @ F ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( B @ D @ F ) )
& ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( C @ D @ F ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_local_Ohmlsl_Oat__conj__distr) ).
thf(241,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( ( B @ D @ F )
& ( C @ D @ F ) ) ) )
= ( ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( B @ D @ F ) )
& ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ( C @ D @ F ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(13,axiom,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_order__trans) ).
thf(167,plain,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(10659,plain,
! [E: view_e774982825t_unit,D: traffic,C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( switch @ B @ ( own_Product_unit @ E ) @ ( move @ C @ D @ E ) )
| ( ( move @ A @ A @ B )
!= ( move @ C @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[578,6202]) ).
thf(10660,plain,
! [B: view_e774982825t_unit,A: traffic] : ( switch @ B @ ( own_Product_unit @ B ) @ ( move @ A @ A @ B ) ),
inference(pattern_uni,[status(thm)],[10659:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(129,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ! [C: nat_int] :
( ( ord_less_eq_nat_int @ C @ A )
=> ( ord_less_eq_nat_int @ C @ B ) ) ),
inference(miniscope,[status(thm)],[128]) ).
thf(130,plain,
! [C: nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ C @ A )
| ( ord_less_eq_nat_int @ C @ B ) ),
inference(cnf,[status(esa)],[129]) ).
thf(80,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars] : ( withdraw_claim @ B @ D @ C )
=> ( abstract @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_traffic_Owd__clm) ).
thf(473,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars] : ( withdraw_claim @ B @ D @ C )
=> ( abstract @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(209,plain,
! [A: view_e774982825t_unit] : ( switch @ A @ ( sk13 @ A ) @ ( sk14 @ A ) ),
inference(cnf,[status(esa)],[208]) ).
thf(75,axiom,
! [A: product_unit] : ( A = product_Unity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_old_Ounit_Oexhaust) ).
thf(458,plain,
! [A: product_unit] : ( A = product_Unity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(193,plain,
! [B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ( ord_less_eq_nat_int @ B @ A )
= ( B = A ) ) ),
inference(cnf,[status(esa)],[192]) ).
thf(194,plain,
! [B: nat_int,A: nat_int] :
( ( ( ord_less_eq_nat_int @ B @ A )
= ( B = A ) )
| ~ ( ord_less_eq_nat_int @ A @ B ) ),
inference(lifteq,[status(thm)],[193]) ).
thf(98,axiom,
( switch
= ( ^ [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_view_Oswitch__def) ).
thf(557,plain,
( switch
= ( ^ [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(5584,plain,
! [A: traffic] :
( ( A != ts3 )
| ( A != ts_a )
| ( ( move @ ts3 @ ts @ v )
!= v ) ),
inference(simp,[status(thm)],[5579]) ).
thf(5585,plain,
( ( ts3 != ts_a )
| ( ( move @ ts3 @ ts @ v )
!= v ) ),
inference(simp,[status(thm)],[5584]) ).
thf(5589,plain,
( ( ts3 != ts_a )
| ( ( move @ ts3 @ ts_a @ v )
!= v )
| ( ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) )
!= ( move @ ts3 @ ts @ v ) ) ),
inference(paramod_ordered,[status(thm)],[606,5585]) ).
thf(5591,plain,
( ( ts3 != ts_a )
| ( ( move @ ts3 @ ts_a @ v )
!= v )
| ( ts3 != ts_a )
| ( ts != ts )
| ( ( move @ ts3 @ ts_a @ v )
!= v ) ),
inference(simp,[status(thm)],[5589]) ).
thf(5594,plain,
( ( ts3 != ts_a )
| ( ( move @ ts3 @ ts_a @ v )
!= v ) ),
inference(simp,[status(thm)],[5591]) ).
thf(5598,plain,
! [B: view_e774982825t_unit,A: traffic] :
( ( ts3 != ts_a )
| ( B != v )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,5594]) ).
thf(5601,plain,
! [A: traffic] :
( ( ts3 != ts_a )
| ( A != ts3 )
| ( A != ts_a )
| ( v != v ) ),
inference(simp,[status(thm)],[5598]) ).
thf(5602,plain,
ts3 != ts_a,
inference(simp,[status(thm)],[5601]) ).
thf(48,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) )
=> ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_local_Ohmlsl_Oat__neg__neg1) ).
thf(282,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) )
=> ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(146,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ( ( C @ B )
!= D )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk5 @ D @ C @ B @ A ) ) @ ( C @ ( sk6 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(cnfConj,[status(thm)],[144]) ).
thf(149,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ( ( C @ B )
!= D )
| ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk5 @ D @ C @ B @ A ) ) @ ( C @ ( sk6 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(lifteq,[status(thm)],[146]) ).
thf(150,plain,
! [C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ ( sk5 @ ( C @ B ) @ C @ B @ A ) ) @ ( C @ ( sk6 @ ( C @ B ) @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ ( C @ B ) ) ),
inference(simp,[status(thm)],[149]) ).
thf(11057,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ~ $true
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( create_reservation @ ts_a @ sk104 @ ts ) ) ),
inference(paramod_ordered,[status(thm)],[580,200]) ).
thf(11058,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( create_reservation @ ts_a @ sk104 @ ts ) ) ),
inference(simp,[status(thm)],[11057]) ).
thf(11144,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ B @ sk104 @ ts ) )
@ ( sk10 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ B @ sk104 @ ts ) ) ),
inference(pre_uni,[status(thm)],[11058:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( create_reservation @ D @ sk104 @ ts ) )),bind(B,$thf( ts_a )),bind(C,$thf( C ))]]) ).
thf(11275,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ B @ sk104 @ ts ) )
@ ( sk10 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ B @ sk104 @ ts ) ) ),
inference(simp,[status(thm)],[11144]) ).
thf(61,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ? [H: view_e774982825t_unit,I: view_e774982825t_unit] :
( ( hchop @ G @ H @ I )
& ( B @ D @ H )
& ( C @ D @ I ) ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ? [H: view_e774982825t_unit,I: view_e774982825t_unit] :
( ( hchop @ F @ H @ I )
& ( A @ D @ H )
& ( B @ D @ I ) )
& ( C @ D @ G ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_local_Ohmlsl_Ohchop__assoc) ).
thf(327,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ? [H: view_e774982825t_unit,I: view_e774982825t_unit] :
( ( hchop @ G @ H @ I )
& ( B @ D @ H )
& ( C @ D @ I ) ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ? [H: view_e774982825t_unit,I: view_e774982825t_unit] :
( ( hchop @ F @ H @ I )
& ( A @ D @ H )
& ( B @ D @ I ) )
& ( C @ D @ G ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(558,plain,
( switch
= ( ^ [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B )
& ( ( more_Product_unit @ A )
= ( more_Product_unit @ C ) ) ) ) ),
inference(lifteq,[status(thm)],[557]) ).
thf(6229,plain,
( switch
= ( ^ [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B )
& ( defaul1399868459t_unit = defaul1399868459t_unit ) ) ) ),
inference(rewrite,[status(thm)],[558,6224]) ).
thf(6230,plain,
( switch
= ( ^ [A: view_e774982825t_unit,B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B ) ) ) ),
inference(simp,[status(thm)],[6229]) ).
thf(6367,plain,
! [A: view_e774982825t_unit] :
( ( switch @ A )
= ( ^ [B: cars,C: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ C ) )
& ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ C ) )
& ( ( own_Product_unit @ C )
= B ) ) ) ),
inference(func_ext,[status(esa)],[6230]) ).
thf(199,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ( hchop @ C @ ( sk11 @ C @ B @ A ) @ ( sk12 @ C @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(109,axiom,
abstract @ ts3 @ ts2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_abs) ).
thf(585,plain,
abstract @ ts3 @ ts2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(123,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ~ ( ord_less_eq_nat_int @ ( B @ ( sk1 @ D @ C @ B @ A ) ) @ ( B @ ( sk2 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(126,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ( A
!= ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ~ ( ord_less_eq_nat_int @ ( B @ ( sk1 @ D @ C @ B @ A ) ) @ ( B @ ( sk2 @ D @ C @ B @ A ) ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(lifteq,[status(thm)],[123]) ).
thf(127,plain,
! [C: nat_int,B: nat_int,A: nat_int > nat_int] :
( ~ ( ord_less_eq_nat_int @ B @ C )
| ~ ( ord_less_eq_nat_int @ ( A @ ( sk1 @ C @ B @ A @ ( A @ B ) ) ) @ ( A @ ( sk2 @ C @ B @ A @ ( A @ B ) ) ) )
| ( ord_less_eq_nat_int @ ( A @ B ) @ ( A @ C ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(10653,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic] :
( ( switch @ ( move @ ts3 @ ts_a @ v ) @ ( own_Product_unit @ C ) @ ( move @ A @ B @ C ) )
| ( ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) )
!= ( move @ A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[606,6202]) ).
thf(10654,plain,
switch @ ( move @ ts3 @ ts_a @ v ) @ ( own_Product_unit @ ( move @ ts3 @ ts_a @ v ) ) @ ( move @ ts_a @ ts @ ( move @ ts3 @ ts_a @ v ) ),
inference(pattern_uni,[status(thm)],[10653:[bind(A,$thf( ts_a )),bind(B,$thf( ts )),bind(C,$thf( move @ ts3 @ ts_a @ v ))]]) ).
thf(10739,plain,
switch @ ( move @ ts3 @ ts_a @ v ) @ ( own_Product_unit @ v ) @ ( move @ ts3 @ ts_a @ v ),
inference(rewrite,[status(thm)],[10654,1100,606]) ).
thf(64,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( evolve @ A @ B )
=> ( ( evolve @ B @ C )
=> ( evolve @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_traffic_Oevolve__trans) ).
thf(336,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( evolve @ A @ B )
=> ( ( evolve @ B @ C )
=> ( evolve @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(10,axiom,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( A = B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_ord__eq__le__trans) ).
thf(154,plain,
! [A: nat_int,B: nat_int,C: nat_int] :
( ( A = B )
=> ( ( ord_less_eq_nat_int @ B @ C )
=> ( ord_less_eq_nat_int @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(16,axiom,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( B = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_dual__order_Oantisym) ).
thf(175,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(60,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) )
=> ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_local_Ohmlsl_Oat__hchop__dist2) ).
thf(314,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ! [H: view_e774982825t_unit] :
( ( switch @ F @ A @ H )
=> ( B @ D @ H ) )
& ! [H: view_e774982825t_unit] :
( ( switch @ G @ A @ H )
=> ( C @ D @ H ) ) )
=> ! [F: view_e774982825t_unit] :
( ( switch @ E @ A @ F )
=> ? [G: view_e774982825t_unit,H: view_e774982825t_unit] :
( ( hchop @ F @ G @ H )
& ( B @ D @ G )
& ( C @ D @ H ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(11186,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) )
@ ( sk10 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) ) ),
inference(pre_uni,[status(thm)],[11084:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( abstract @ ts3 @ D ) )),bind(B,$thf( ts_a )),bind(C,$thf( C ))]]) ).
thf(11302,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) )
@ ( sk10 @ A @ ts_a
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) ) ),
inference(simp,[status(thm)],[11186]) ).
thf(77,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ( abstract @ C @ A )
=> ( abstract @ C @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_traffic_Oabs__trans) ).
thf(465,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ( abstract @ C @ A )
=> ( abstract @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(25,axiom,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) )
= ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_local_Ohmlsl_Oat__neg__neg) ).
thf(203,plain,
! [A: cars,B: traffic > view_e774982825t_unit > $o,C: traffic,D: view_e774982825t_unit] :
( ( ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ( B @ C @ E ) ) )
= ( ~ ! [E: view_e774982825t_unit] :
( ( switch @ D @ A @ E )
=> ~ ( B @ C @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(108,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ! [D: traffic] :
( ( abstract @ B @ D )
=> ( A @ D @ ( move @ B @ D @ C ) ) )
=> ! [D: traffic] :
( ( abstract @ B @ D )
=> ! [E: traffic] :
( ( abstract @ D @ E )
=> ( A @ E @ ( move @ D @ E @ ( move @ B @ D @ C ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_local_Ohmlsl_Oglobally__4) ).
thf(581,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic,C: view_e774982825t_unit] :
( ! [D: traffic] :
( ( abstract @ B @ D )
=> ( A @ D @ ( move @ B @ D @ C ) ) )
=> ! [D: traffic] :
( ( abstract @ B @ D )
=> ! [E: traffic] :
( ( abstract @ D @ E )
=> ( A @ E @ ( move @ D @ E @ ( move @ B @ D @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(87,axiom,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars,E: nat] : ( create_claim @ B @ D @ E @ C )
=> ( abstract @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_traffic_Ocr__clm) ).
thf(495,plain,
! [A: traffic,B: traffic,C: traffic] :
( ( abstract @ A @ B )
=> ( ? [D: cars,E: nat] : ( create_claim @ B @ D @ E @ C )
=> ( abstract @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(3621,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ A )
| ( B @ C )
| ( defaul1399868459t_unit != defaul1399868459t_unit ) ),
inference(paramod_ordered,[status(thm)],[615,3604]) ).
thf(3622,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ A )
| ( B @ C ) ),
inference(pattern_uni,[status(thm)],[3621:[]]) ).
thf(3789,plain,
! [B: product_unit,A: product_unit] :
( ( A != A )
| ( A = B ) ),
inference(replace_leibeq,[status(thm)],[3622:[bind(A,$thf( A )),bind(B,$thf( (=) @ product_unit @ A ))]]) ).
thf(3799,plain,
! [B: product_unit,A: product_unit] :
( ( A != A )
| ( A = B ) ),
inference(lifteq,[status(thm)],[3789]) ).
thf(3848,plain,
! [B: product_unit,A: product_unit] : ( A = B ),
inference(pattern_uni,[status(thm)],[3799:[]]) ).
thf(3928,plain,
! [B: product_unit,A: product_unit] : ( A = B ),
inference(simp,[status(thm)],[3848]) ).
thf(218,plain,
! [A: view_e774982825t_unit] : ( hchop @ A @ ( sk16 @ A ) @ A ),
inference(cnf,[status(esa)],[217]) ).
thf(55,axiom,
! [A: traffic] : ( evolve @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_traffic_Oevolve_Orefl) ).
thf(304,plain,
! [A: traffic] : ( evolve @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(11063,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ~ $true
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( abstract @ ts3 @ ts2 ) ) ),
inference(paramod_ordered,[status(thm)],[585,200]) ).
thf(11064,plain,
! [C: view_e774982825t_unit,B: traffic,A: traffic > view_e774982825t_unit > $o] :
( ( hchop @ C @ ( sk9 @ C @ B @ A ) @ ( sk10 @ C @ B @ A ) )
| ( ( A @ B @ ( sk11 @ C @ B @ A ) )
!= ( abstract @ ts3 @ ts2 ) ) ),
inference(simp,[status(thm)],[11063]) ).
thf(11159,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts2
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) )
@ ( sk10 @ A @ ts2
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) ) ),
inference(pre_uni,[status(thm)],[11064:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( abstract @ ts3 @ D ) )),bind(B,$thf( ts2 )),bind(C,$thf( C ))]]) ).
thf(11287,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts2
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) )
@ ( sk10 @ A @ ts2
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ ts3 @ B ) ) ),
inference(simp,[status(thm)],[11159]) ).
thf(19,axiom,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_eq__iff) ).
thf(183,plain,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(184,plain,
( ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) )
= ( (=) @ nat_int ) ),
inference(lifteq,[status(thm)],[183]) ).
thf(634,plain,
! [A: nat_int] :
( ( ^ [B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) )
= ( (=) @ nat_int @ A ) ),
inference(func_ext,[status(esa)],[184]) ).
thf(9338,plain,
! [A: nat_int] :
( ( ^ [B: nat_int] : ( B = A ) )
= ( (=) @ nat_int @ A ) ),
inference(rewrite,[status(thm)],[634,633]) ).
thf(3598,plain,
! [B: traffic,A: traffic] :
( ( ^ [C: view_e774982825t_unit] : ( view_e912666823t_unit @ ( real_shift @ ( ext_Product_unit @ C ) @ ( minus_minus_real @ ( pos @ B @ ( own_Product_unit @ C ) ) @ ( pos @ A @ ( own_Product_unit @ C ) ) ) ) @ ( lan_Product_unit @ C ) @ ( own_Product_unit @ C ) @ defaul1399868459t_unit ) )
= ( move @ A @ B ) ),
inference(func_ext,[status(esa)],[3596]) ).
thf(300,plain,
! [A: view_e774982825t_unit] : ( switch @ ( sk43 @ A ) @ ( own_Product_unit @ A ) @ A ),
inference(cnf,[status(esa)],[299]) ).
thf(190,plain,
! [D: nat_int,C: nat_int > nat_int,B: nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ B )
| ~ ( ord_less_eq_nat_int @ ( C @ B ) @ D )
| ( ord_less_eq_nat_int @ ( sk7 @ D @ C @ B @ A ) @ ( sk8 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ ( C @ A ) @ D ) ),
inference(cnfConj,[status(thm)],[189]) ).
thf(7236,plain,
! [D: traffic,C: traffic,B: view_e774982825t_unit,A: traffic] :
( ( ts3 != ts )
| ( B
!= ( move @ C @ C @ ( move @ D @ D @ v ) ) )
| ( ( move @ A @ A @ B )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(paramod_ordered,[status(thm)],[578,6833]) ).
thf(7237,plain,
! [C: traffic,B: traffic,A: traffic] :
( ( ts3 != ts )
| ( ( move @ A @ A @ ( move @ B @ B @ ( move @ C @ C @ v ) ) )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(simp,[status(thm)],[7236]) ).
thf(7248,plain,
! [C: traffic,B: traffic,A: traffic] :
( ( ts3 != ts )
| ( ( move @ A @ A @ ( move @ B @ B @ ( move @ C @ C @ v ) ) )
!= ( move @ ts3 @ ts_a @ v ) ) ),
inference(simp,[status(thm)],[7237]) ).
thf(9754,plain,
! [C: product_unit,B: product_unit > $o,A: product_unit] :
( ~ ( B @ defaul1399868459t_unit )
| ( ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) )
!= ( ~ ( B @ A ) ) )
| ( ( ( res @ ts_a @ sk104 )
= ( res @ ts @ sk104 ) )
!= ( B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[9743,4358]) ).
thf(9824,plain,
( ( ( res @ ts_a @ sk104 )
!= ( res @ ts @ sk104 ) )
| ( ( ( res @ ts_a @ sk104 )
!= ( res @ ts @ sk104 ) )
!= ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) ) ) ),
inference(pre_uni,[status(thm)],[9754:[bind(A,$thf( A )),bind(B,$thf( ^ [D: product_unit] : ( ( res @ ts_a @ sk104 ) = ( res @ ts @ sk104 ) ) )),bind(C,$thf( C ))]]) ).
thf(9844,plain,
( ( ( res @ ts_a @ sk104 )
!= ( res @ ts @ sk104 ) )
| ( ( ( res @ ts_a @ sk104 )
!= ( res @ ts @ sk104 ) )
!= ( ( res @ ts @ sk104 )
= ( res @ ts_a @ sk104 ) ) ) ),
inference(lifteq,[status(thm)],[9824]) ).
thf(101,axiom,
( abstract
= ( ^ [A: traffic,B: traffic] :
( ( B = A )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ( evolve @ C @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars,F: nat] : ( create_claim @ C @ E @ F @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars] : ( withdraw_claim @ C @ E @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars] : ( create_reservation @ C @ E @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars,F: nat] : ( withdraw_reservation @ C @ E @ F @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_traffic_Oabstract_Osimps) ).
thf(564,plain,
( abstract
= ( ^ [A: traffic,B: traffic] :
( ( B = A )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ( evolve @ C @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars,F: nat] : ( create_claim @ C @ E @ F @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars] : ( withdraw_claim @ C @ E @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars] : ( create_reservation @ C @ E @ D ) )
| ? [C: traffic,D: traffic] :
( ( B = D )
& ( abstract @ A @ C )
& ? [E: cars,F: nat] : ( withdraw_reservation @ C @ E @ F @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(305,plain,
! [A: traffic] : ( evolve @ A @ A ),
inference(cnf,[status(esa)],[304]) ).
thf(28,axiom,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( ( B @ D @ G )
| ( C @ D @ G ) ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( B @ D @ G ) )
| ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( C @ D @ G ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_local_Ohmlsl_Ohchop__disj__distr1) ).
thf(210,plain,
! [A: traffic > view_e774982825t_unit > $o,B: traffic > view_e774982825t_unit > $o,C: traffic > view_e774982825t_unit > $o,D: traffic,E: view_e774982825t_unit] :
( ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( ( B @ D @ G )
| ( C @ D @ G ) ) ) )
= ( ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( B @ D @ G ) )
| ? [F: view_e774982825t_unit,G: view_e774982825t_unit] :
( ( hchop @ E @ F @ G )
& ( A @ D @ F )
& ( C @ D @ G ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(136,plain,
! [D: nat_int,C: nat_int,B: nat_int > nat_int,A: nat_int] :
( ~ ( ord_less_eq_nat_int @ A @ ( B @ C ) )
| ~ ( ord_less_eq_nat_int @ C @ D )
| ( ord_less_eq_nat_int @ ( sk3 @ D @ C @ B @ A ) @ ( sk4 @ D @ C @ B @ A ) )
| ( ord_less_eq_nat_int @ A @ ( B @ D ) ) ),
inference(cnfConj,[status(thm)],[135]) ).
thf(70,axiom,
! [A: view_e774982825t_unit] :
( A
= ( view_e912666823t_unit @ ( ext_Product_unit @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ ( more_Product_unit @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_surjective) ).
thf(358,plain,
! [A: view_e774982825t_unit] :
( A
= ( view_e912666823t_unit @ ( ext_Product_unit @ A ) @ ( lan_Product_unit @ A ) @ ( own_Product_unit @ A ) @ ( more_Product_unit @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(23,axiom,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_order__class_Oorder_Oeq__iff) ).
thf(195,plain,
( ( (=) @ nat_int )
= ( ^ [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
& ( ord_less_eq_nat_int @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(9541,plain,
! [B: nat_int,A: nat_int] :
( ( B = A )
= ( A = B ) ),
inference(func_ext,[status(esa)],[9338]) ).
thf(17,axiom,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_antisym) ).
thf(178,plain,
! [A: nat_int,B: nat_int] :
( ( ord_less_eq_nat_int @ A @ B )
=> ( ( ord_less_eq_nat_int @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(11145,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ ts_a @ sk104 @ B ) )
@ ( sk10 @ A @ ts
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ ts_a @ sk104 @ B ) ) ),
inference(pre_uni,[status(thm)],[11058:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( create_reservation @ ts_a @ sk104 @ D ) )),bind(B,$thf( ts )),bind(C,$thf( C ))]]) ).
thf(11276,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ ts_a @ sk104 @ B ) )
@ ( sk10 @ A @ ts
@ ^ [B: traffic,C: view_e774982825t_unit] : ( create_reservation @ ts_a @ sk104 @ B ) ) ),
inference(simp,[status(thm)],[11145]) ).
thf(116,axiom,
! [A: traffic,B: cars,C: nat,D: traffic,E: view_e774982825t_unit] :
( ( create_claim @ A @ B @ C @ D )
=> ( ( move @ A @ D @ E )
= E ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_traffic_Omove__stability__clm) ).
thf(607,plain,
! [A: traffic,B: cars,C: nat,D: traffic,E: view_e774982825t_unit] :
( ( create_claim @ A @ B @ C @ D )
=> ( ( move @ A @ D @ E )
= E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(11158,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts2 ) )
@ ( sk10 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts2 ) ) ),
inference(pre_uni,[status(thm)],[11064:[bind(A,$thf( ^ [D: traffic] : ^ [E: view_e774982825t_unit] : ( abstract @ D @ ts2 ) )),bind(B,$thf( ts3 )),bind(C,$thf( C ))]]) ).
thf(11286,plain,
! [A: view_e774982825t_unit] :
( hchop @ A
@ ( sk9 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts2 ) )
@ ( sk10 @ A @ ts3
@ ^ [B: traffic,C: view_e774982825t_unit] : ( abstract @ B @ ts2 ) ) ),
inference(simp,[status(thm)],[11158]) ).
thf(309,plain,
! [A: view_e774982825t_unit] : ( hchop @ A @ A @ ( sk45 @ A ) ),
inference(cnf,[status(esa)],[308]) ).
thf(94,axiom,
! [A: view_e774982825t_unit,B: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ B ) )
=> ( ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
=> ( ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
=> ( ( ( more_Product_unit @ A )
= ( more_Product_unit @ B ) )
=> ( A = B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_equality) ).
thf(543,plain,
! [A: view_e774982825t_unit,B: view_e774982825t_unit] :
( ( ( ext_Product_unit @ A )
= ( ext_Product_unit @ B ) )
=> ( ( ( lan_Product_unit @ A )
= ( lan_Product_unit @ B ) )
=> ( ( ( own_Product_unit @ A )
= ( own_Product_unit @ B ) )
=> ( ( ( more_Product_unit @ A )
= ( more_Product_unit @ B ) )
=> ( A = B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(72,axiom,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( withdraw_claim @ A @ B @ C )
=> ( ( res @ A @ D )
= ( res @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_traffic_Owithdraw__clm__eq__res) ).
thf(364,plain,
! [A: traffic,B: cars,C: traffic,D: cars] :
( ( withdraw_claim @ A @ B @ C )
=> ( ( res @ A @ D )
= ( res @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(13431,plain,
$false,
inference(e,[status(thm)],[138,333,468,234,6014,481,170,308,7332,511,614,6017,597,217,276,385,533,142,472,153,6877,10662,185,288,301,257,570,125,542,559,4358,606,5851,7633,1100,216,1450,485,348,6823,492,164,1169,221,293,9743,132,133,265,9024,312,206,307,248,117,546,201,349,297,192,137,197,361,551,456,566,484,6833,461,578,7329,615,5583,593,339,554,7318,476,590,970,1099,173,9846,6784,6224,605,128,244,266,633,508,311,586,298,166,148,856,601,562,191,7639,118,3604,11254,259,579,291,572,313,11301,611,498,236,181,8202,540,159,187,172,219,274,9377,230,6460,271,208,345,535,213,251,6817,330,306,563,299,267,241,167,10660,130,473,490,209,355,458,194,6202,557,580,7635,5602,282,150,11275,327,6367,310,199,585,127,10739,470,576,336,154,175,314,612,11302,465,203,3874,581,495,3928,218,368,304,186,11287,9338,119,3598,536,151,300,4356,190,183,7248,9844,564,305,210,136,358,195,9541,575,131,200,178,11276,607,486,11286,309,543,215,364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP168^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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.11/0.21 % Computer : n017.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 20:00:22 UTC 2026
% 0.11/0.21 % CPUTime :
% 0.11/0.21 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.86/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.03/1.20 % [INFO] Parsing done (412ms).
% 2.34/1.21 % [INFO] Running in sequential loop mode.
% 3.14/1.58 % [INFO] eprover registered as external prover.
% 3.14/1.59 % [INFO] Scanning for conjecture ...
% 3.56/1.73 % [INFO] Found a conjecture (or negated_conjecture) and 357 axioms. Running axiom selection ...
% 3.74/1.84 % [INFO] Axiom selection finished. Selected 114 axioms (removed 243 axioms).
% 4.14/2.02 % [INFO] Problem is higher-order (TPTP THF).
% 4.44/2.04 % [INFO] Type checking passed.
% 4.44/2.04 % [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 ...
% 6.92/2.75 % [INFO] [Domain constraints] Detected constraint on product_unit
% 6.92/2.75 % [INFO] [Domain constraints] dom(product_unit) ⊆ {product_Unity}
% 7.42/2.83 % [INFO] [Domain constraints] Detected constraint on product_unit
% 7.42/2.83 % [INFO] [Domain constraints] dom(product_unit) ⊆ {product_Unity}
% 128.55/60.00 % External prover 'e' found a proof!
% 128.55/60.00 % [INFO] Killing All external provers ...
% 128.55/60.00 % Time passed: 59646ms (effective reasoning time: 58786ms)
% 128.55/60.00 % 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)>
% 128.55/60.00 % Axioms used in derivation (114): fact_98_local_Ohmlsl_Oat__hchop__dist, fact_95_local_Ohmlsl_Oat__neg__neg, fact_57_select__convs_I4_J, fact_115_unit__all__impI, fact_2_local_Ohmlsl_Oglobally__4, fact_84_chop__singleton__right, fact_38_traffic_Oabs__trans, fact_117_bot__unit__def, fact_15_local_Ohmlsl_Ohchop__assoc, fact_17_local_Ohmlsl_Ohchop__disj__distr2, fact_87_view_Oswitch__def, fact_211_dual__order_Otrans, fact_101_view_Oswitch__always__exists, fact_0_cr__res_Ohyps_I1_J, fact_1_cr__res_Ohyps_I2_J, fact_237_traffic_Ocreate__res__subseteq1, fact_22_local_Ohmlsl_Ohchop__neg1, fact_53_traffic_Oevolve__trans, fact_35_view_Ohorizontal__chop__assoc1, fact_106_view_Oswitch__hchop1, fact_93_local_Ohmlsl_Oat__neg1, fact_20_local_Ohmlsl_Ohchop__weaken, fact_18_local_Ohmlsl_Ohchop__weaken2, fact_43_select__convs_I1_J, fact_194_ord__le__eq__trans, fact_105_view_Oswitch__trans, fact_67_view_Ohchop__def, fact_9_traffic_Omove__keeps__owner, fact_40_cases__scheme, fact_49_traffic_Owithdraw__clm__eq__res, fact_26_traffic_Ocr__clm, fact_42_view_Ohorizontal__chop__own__trans, fact_32_view_Ohorizontal__chop__empty__right, fact_56_traffic_Oevolve, fact_58_equality, fact_88_local_Ohmlsl_Oat__conj__distr, fact_52_traffic_Ocreate__res__subseteq2__neq, fact_102_view_Oswitch__triangle, fact_100_local_Ohmlsl_Oat__hchop__dist2, fact_3_local_Ohmlsl_Oglobally__refl, fact_238_traffic_Owithdraw__res__subseteq, fact_177_order_Otrans, fact_103_view_Oswitch__unique, fact_46_traffic_Oabstract_Osimps, fact_39_induct__scheme, fact_13_traffic_Omove__stability__wdc, fact_86_chop__singleton__left, fact_23_ext__inject, fact_215_dual__order_Oeq__iff, fact_239_default__unit__def, fact_143_ord__eq__le__subst, fact_206_dual__order_Orefl, fact_5__092_060open_062move_Ats_Ats_H_Av_A_061_Amove_Ats_H_Ats_H_H_A_Imove_Ats_Ats_H_Av_J_092_060close_062, fact_45_traffic_Oabstract_Oinducts, fact_186_order__class_Oorder_Oeq__iff, fact_116_eq__sym__Unity__conv, fact_113_old_Ounit_Oexhaust, fact_7_traffic_Omove__def, fact_182_antisym__conv, fact_24_cases, fact_30_select__convs_I3_J, fact_219_dual__order_Oantisym, fact_12_traffic_Omove__stability__clm, fact_123_order__subst1, fact_108_view_Oswitch__refl, fact_10_traffic_Omove__trans, fact_91_local_Ohmlsl_Oat__neg, fact_202_order__trans, fact_96_local_Ohmlsl_Oat__neg__neg1, fact_36_view_Ohorizontal__chop1, fact_16_local_Ohmlsl_Ohchop__disj__distr1, fact_50_traffic_Ocreate__clm__eq__res, fact_28_traffic_Owd__res, fact_34_view_Ohorizontal__chop__assoc2, fact_41_traffic_Oalways__create__res, fact_6_traffic_Omove__nothing, fact_85_real__int__class_Ochop__always__possible, fact_110_view_Oswitch__origin, fact_37_traffic_Oabstract_Orefl, fact_89_local_Ohmlsl_Oat__disj__dist, fact_167_antisym, fact_245_diff__mono, fact_29_traffic_Ocr__res, fact_47_traffic_Oabstract_Ocases, fact_54_traffic_Oevolve_Orefl, fact_114_old_Ounit_Oinducts, fact_4_abs, fact_33_view_Ohorizontal__chop__empty__left, fact_107_view_Oswitch__hchop2, fact_90_local_Ohmlsl_Oat__exists, fact_31_select__convs_I2_J, fact_163_eq__iff, fact_92_local_Ohmlsl_Oat__neg_H, fact_48_surjective, fact_99_local_Ohmlsl_Oat__hchop__dist1, fact_97_local_Ohmlsl_Oat__neg__neg2, fact_172_eq__refl, fact_190_ord__eq__le__trans, fact_8_traffic_Omove__stability__res, fact_51_traffic_Ocreate__res__subseteq1__neq, fact_198_order__class_Oorder_Oantisym, fact_119_order__refl, fact_94_local_Ohmlsl_Oat__neg2, fact_153_ord__le__eq__subst, fact_27_traffic_Owd__clm, fact_133_order__subst2, fact_19_local_Ohmlsl_Ohchop__weaken1, fact_14_traffic_Omove__stability__wdr, fact_21_local_Ohmlsl_Ohchop__neg2, fact_118_traffic_Ocreate__res__subseteq2, fact_104_view_Oswitch__exists, fact_11_traffic_Omove__keeps__lanes, fact_109_view_Oswitch__symm, fact_25_induct
% 128.55/60.00 % No. of inferences in proof: 479
% 128.55/60.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 59646 ms resp. 58786 ms w/o parsing
% 129.84/60.30 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 129.84/60.30 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------