%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWC173+1 : TPTP v9.3.1. Released v2.4.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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:52:35 AM UTC 2026
% Result : Theorem 98.58s 39.65s
% Output : Refutation 101.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 119
% Syntax : Number of formulae : 848 ( 88 unt; 0 typ; 23 def)
% Number of atoms : 3877 ( 937 equ; 0 cnn)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 8452 (1393 ~;1450 |; 216 &;4693 @)
% ( 26 <=>; 674 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 51 ( 48 usr; 17 con; 0-2 aty)
% Number of variables : 995 ( 10 ^; 908 !; 54 ?; 995 :)
% ( 0 !>; 0 ?*; 0 @-; 23 @+)
% Comments :
%------------------------------------------------------------------------------
thf(ssList_decl,type,
ssList: $i > $o ).
thf(ssItem_decl,type,
ssItem: $i > $o ).
thf(app_decl,type,
app: $i > $i > $i ).
thf(cons_decl,type,
cons: $i > $i > $i ).
thf(nil_decl,type,
nil: $i ).
thf(neq_decl,type,
neq: $i > $i > $o ).
thf(memberP_decl,type,
memberP: $i > $i > $o ).
thf(lt_decl,type,
lt: $i > $i > $o ).
thf(strictorderedP_decl,type,
strictorderedP: $i > $o ).
thf(frontsegP_decl,type,
frontsegP: $i > $i > $o ).
thf(gt_decl,type,
gt: $i > $i > $o ).
thf(totalorderedP_decl,type,
totalorderedP: $i > $o ).
thf(hd_decl,type,
hd: $i > $i ).
thf(segmentP_decl,type,
segmentP: $i > $i > $o ).
thf(cyclefreeP_decl,type,
cyclefreeP: $i > $o ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(strictorderP_decl,type,
strictorderP: $i > $o ).
thf(duplicatefreeP_decl,type,
duplicatefreeP: $i > $o ).
thf(singletonP_decl,type,
singletonP: $i > $o ).
thf(tl_decl,type,
tl: $i > $i ).
thf(totalorderP_decl,type,
totalorderP: $i > $o ).
thf(rearsegP_decl,type,
rearsegP: $i > $i > $o ).
thf(equalelemsP_decl,type,
equalelemsP: $i > $o ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $o ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i ).
thf(sk16_decl,type,
sk16: $i > $i ).
thf(sk17_decl,type,
sk17: $i > $i ).
thf(sk18_decl,type,
sk18: $i > $i ).
thf(sk19_decl,type,
sk19: $i > $i ).
thf(sk20_decl,type,
sk20: $i > $i ).
thf(sk21_decl,type,
sk21: $i > $i ).
thf(sk22_decl,type,
sk22: $i > $i ).
thf(sk45_decl,type,
sk45: $i ).
thf(sk46_decl,type,
sk46: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil != C )
| ( nil != D ) )
& ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssList )
=> ! [G: $i] :
( ( G @ ssList )
=> ( ? [H: $i] :
( ( E @ ( H @ lt ) )
& ( H @ ( G @ memberP ) )
& ( H @ ssItem ) )
| ? [H: $i] :
( ( H @ ( E @ lt ) )
& ( H @ ( F @ memberP ) )
& ( H @ ssItem ) )
| ( ( G @ ( C @ ( F @ app ) @ app ) )
!= D )
| ( ( nil @ ( E @ cons ) )
!= C ) ) ) ) ) )
| ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssItem )
=> ( ( F @ ( E @ neq ) )
| ! [G: $i] :
( ( G @ ssList )
=> ! [H: $i] :
( ( H @ ssList )
=> ( ( H @ ( nil @ ( F @ cons ) @ ( nil @ ( E @ cons ) @ ( G @ app ) @ app ) @ app ) )
!= A ) ) ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( ( nil != B )
| ( nil != C ) )
& ! [D: $i] :
( ( D @ ssItem )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ? [G: $i] :
( ( D @ ( G @ lt ) )
& ( G @ ( F @ memberP ) )
& ( G @ ssItem ) )
| ? [G: $i] :
( ( G @ ( D @ lt ) )
& ( G @ ( E @ memberP ) )
& ( G @ ssItem ) )
| ( ( F @ ( B @ ( E @ app ) @ app ) )
!= C )
| ( ( nil @ ( D @ cons ) )
!= B ) ) ) ) ) )
| ! [D: $i] :
( ( D @ ssItem )
=> ! [E: $i] :
( ( E @ ssItem )
=> ( ( E @ ( D @ neq ) )
| ! [F: $i] :
( ( F @ ssList )
=> ! [G: $i] :
( ( G @ ssList )
=> ( ( G @ ( nil @ ( E @ cons ) @ ( nil @ ( D @ cons ) @ ( F @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) )
| ( sk1 != B )
| ( A != C ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( nil != A )
| ( nil != B ) )
& ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ? [F: $i] :
( ( C @ ( F @ lt ) )
& ( F @ ( E @ memberP ) )
& ( F @ ssItem ) )
| ? [F: $i] :
( ( F @ ( C @ lt ) )
& ( F @ ( D @ memberP ) )
& ( F @ ssItem ) )
| ( ( E @ ( A @ ( D @ app ) @ app ) )
!= B )
| ( ( nil @ ( C @ cons ) )
!= A ) ) ) ) ) )
| ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssItem )
=> ( ( D @ ( C @ neq ) )
| ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( F @ ( nil @ ( D @ cons ) @ ( nil @ ( C @ cons ) @ ( E @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) )
| ( sk1 != A )
| ( sk2 != B ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ( ( ( ( nil != sk3 )
| ( nil != A ) )
& ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ? [E: $i] :
( ( B @ ( E @ lt ) )
& ( E @ ( D @ memberP ) )
& ( E @ ssItem ) )
| ? [E: $i] :
( ( E @ ( B @ lt ) )
& ( E @ ( C @ memberP ) )
& ( E @ ssItem ) )
| ( ( D @ ( sk3 @ ( C @ app ) @ app ) )
!= A )
| ( ( nil @ ( B @ cons ) )
!= sk3 ) ) ) ) ) )
| ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( C @ ( B @ neq ) )
| ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( E @ ( nil @ ( C @ cons ) @ ( nil @ ( B @ cons ) @ ( D @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) )
| ( sk1 != sk3 )
| ( sk2 != A ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ neq ) )
| ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( D @ ( nil @ ( B @ cons ) @ ( nil @ ( A @ cons ) @ ( C @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( ( A @ ssItem )
=> ( ( A @ ( sk5 @ neq ) )
| ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( C @ ( nil @ ( A @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( B @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( nil @ ( sk6 @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( A @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ( ( A @ ( nil @ ( sk6 @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( sk7 @ app ) @ app ) @ app ) )
!= sk1 ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
~ ( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ? [D: $i] :
( ( A @ ( D @ lt ) )
& ( D @ ( C @ memberP ) )
& ( D @ ssItem ) )
| ? [D: $i] :
( ( D @ ( A @ lt ) )
& ( D @ ( B @ memberP ) )
& ( D @ ssItem ) )
| ( ( C @ ( sk3 @ ( B @ app ) @ app ) )
!= sk4 )
| ( ( nil @ ( A @ cons ) )
!= sk3 ) ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ? [C: $i] :
( ( sk10 @ ( C @ lt ) )
& ( C @ ( B @ memberP ) )
& ( C @ ssItem ) )
| ? [C: $i] :
( ( C @ ( sk10 @ lt ) )
& ( C @ ( A @ memberP ) )
& ( C @ ssItem ) )
| ( ( B @ ( sk3 @ ( A @ app ) @ app ) )
!= sk4 )
| ( ( nil @ ( sk10 @ cons ) )
!= sk3 ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ( ? [B: $i] :
( ( sk10 @ ( B @ lt ) )
& ( B @ ( A @ memberP ) )
& ( B @ ssItem ) )
| ? [B: $i] :
( ( B @ ( sk10 @ lt ) )
& ( B @ ( sk11 @ memberP ) )
& ( B @ ssItem ) )
| ( ( A @ ( sk3 @ ( sk11 @ app ) @ app ) )
!= sk4 )
| ( ( nil @ ( sk10 @ cons ) )
!= sk3 ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ~ ( ( B @ ( C @ leq ) )
& ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( B @ cons ) @ ( D @ ( A @ sk13 @ cons ) @ ( C @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk13 @ ( B @ leq ) )
& ( B @ ( A @ sk13 @ leq ) ) ) ) ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( D @ ( A @ sk14 @ cons ) @ ( C @ ( A @ sk13 @ cons ) @ ( B @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk13 @ ( A @ sk14 @ leq ) )
& ( A @ sk14 @ ( A @ sk13 @ leq ) ) ) ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( A @ sk14 @ cons ) @ ( B @ ( A @ sk13 @ cons ) @ ( A @ sk15 @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk13 @ ( A @ sk14 @ leq ) )
& ( A @ sk14 @ ( A @ sk13 @ leq ) ) ) ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ( ( ( B @ ( A @ sk14 @ cons ) @ ( A @ sk16 @ ( A @ sk13 @ cons ) @ ( A @ sk15 @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk13 @ ( A @ sk14 @ leq ) )
& ( A @ sk14 @ ( A @ sk13 @ leq ) ) ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) ) ) ) ) ) ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( B @ cons ) @ ( D @ ( A @ sk18 @ cons ) @ ( C @ app ) @ app ) )
= A )
=> ( ( A @ sk18 @ ( B @ lt ) )
| ( B @ ( A @ sk18 @ lt ) ) ) ) ) ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( D @ ( A @ sk19 @ cons ) @ ( C @ ( A @ sk18 @ cons ) @ ( B @ app ) @ app ) )
= A )
=> ( ( A @ sk18 @ ( A @ sk19 @ lt ) )
| ( A @ sk19 @ ( A @ sk18 @ lt ) ) ) ) ) ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( A @ sk19 @ cons ) @ ( B @ ( A @ sk18 @ cons ) @ ( A @ sk20 @ app ) @ app ) )
= A )
=> ( ( A @ sk18 @ ( A @ sk19 @ lt ) )
| ( A @ sk19 @ ( A @ sk18 @ lt ) ) ) ) ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ( ( ( B @ ( A @ sk19 @ cons ) @ ( A @ sk21 @ ( A @ sk18 @ cons ) @ ( A @ sk20 @ app ) @ app ) )
= A )
=> ( ( A @ sk18 @ ( A @ sk19 @ lt ) )
| ( A @ sk19 @ ( A @ sk18 @ lt ) ) ) ) ) ) ) ).
thf(sk45_def,definition,
( sk45
= ( @+[A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ) ) ) ).
thf(sk46_def,definition,
( sk46
= ( @+[A: $i] :
( ( sk45 != A )
& ( A @ ssItem ) ) ) ) ).
thf(1,conjecture,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil != C )
| ( nil != D ) )
& ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssList )
=> ! [G: $i] :
( ( G @ ssList )
=> ( ? [H: $i] :
( ( E @ ( H @ lt ) )
& ( H @ ( G @ memberP ) )
& ( H @ ssItem ) )
| ? [H: $i] :
( ( H @ ( E @ lt ) )
& ( H @ ( F @ memberP ) )
& ( H @ ssItem ) )
| ( ( G @ ( C @ ( F @ app ) @ app ) )
!= D )
| ( ( nil @ ( E @ cons ) )
!= C ) ) ) ) ) )
| ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssItem )
=> ( ( F @ ( E @ neq ) )
| ! [G: $i] :
( ( G @ ssList )
=> ! [H: $i] :
( ( H @ ssList )
=> ( ( H @ ( nil @ ( F @ cons ) @ ( nil @ ( E @ cons ) @ ( G @ app ) @ app ) @ app ) )
!= A ) ) ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil != C )
| ( nil != D ) )
& ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssList )
=> ! [G: $i] :
( ( G @ ssList )
=> ( ? [H: $i] :
( ( E @ ( H @ lt ) )
& ( H @ ( G @ memberP ) )
& ( H @ ssItem ) )
| ? [H: $i] :
( ( H @ ( E @ lt ) )
& ( H @ ( F @ memberP ) )
& ( H @ ssItem ) )
| ( ( G @ ( C @ ( F @ app ) @ app ) )
!= D )
| ( ( nil @ ( E @ cons ) )
!= C ) ) ) ) ) )
| ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssItem )
=> ( ( F @ ( E @ neq ) )
| ! [G: $i] :
( ( G @ ssList )
=> ! [H: $i] :
( ( H @ ssList )
=> ( ( H @ ( nil @ ( F @ cons ) @ ( nil @ ( E @ cons ) @ ( G @ app ) @ app ) @ app ) )
!= A ) ) ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(98,plain,
~ ! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil != C )
| ( nil != D ) )
& ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssList )
=> ! [G: $i] :
( ( G @ ssList )
=> ( ? [H: $i] :
( ( E @ ( H @ lt ) )
& ( H @ ( G @ memberP ) )
& ( H @ ssItem ) )
| ? [H: $i] :
( ( H @ ( E @ lt ) )
& ( H @ ( F @ memberP ) )
& ( H @ ssItem ) )
| ( ( G @ ( C @ ( F @ app ) @ app ) )
!= D )
| ( ( nil @ ( E @ cons ) )
!= C ) ) ) ) ) )
| ! [E: $i] :
( ( E @ ssItem )
=> ! [F: $i] :
( ( F @ ssItem )
=> ( ( F @ ( E @ neq ) )
| ! [G: $i] :
( ( G @ ssList )
=> ! [H: $i] :
( ( H @ ssList )
=> ( ( H @ ( nil @ ( F @ cons ) @ ( nil @ ( E @ cons ) @ ( G @ app ) @ app ) @ app ) )
!= A ) ) ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(99,plain,
! [B: $i,A: $i] :
( ( ( nil = sk3 )
| sk9 )
& ( ( nil = sk4 )
| sk9 )
& ( ~ sk9
| ~ ( sk10 @ ( B @ lt ) )
| ~ ( B @ ( sk12 @ memberP ) )
| ~ ( B @ ssItem ) )
& ( ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ ( A @ ssItem ) )
& ( ~ sk9
| ( ( sk12 @ ( sk3 @ ( sk11 @ app ) @ app ) )
= sk4 ) )
& ( ~ sk9
| ( ( nil @ ( sk10 @ cons ) )
= sk3 ) )
& ( ~ sk9
| ( sk12 @ ssList ) )
& ( ~ sk9
| ( sk11 @ ssList ) )
& ( ~ sk9
| ( sk10 @ ssItem ) )
& ~ ( sk6 @ ( sk5 @ neq ) )
& ( ( sk8 @ ( nil @ ( sk6 @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( sk7 @ app ) @ app ) @ app ) )
= sk1 )
& ( sk8 @ ssList )
& ( sk7 @ ssList )
& ( sk6 @ ssItem )
& ( sk5 @ ssItem )
& ( sk1 = sk3 )
& ( sk2 = sk4 )
& ( sk4 @ ssList )
& ( sk3 @ ssList )
& ( sk2 @ ssList )
& ( sk1 @ ssList ) ),
inference(cnf,[status(esa)],[98]) ).
thf(100,plain,
sk7 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(17,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ cyclefreeP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ~ ( ( B @ ( C @ leq ) )
& ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
thf(168,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ~ ( ( B @ ( C @ leq ) )
& ( C @ ( B @ leq ) ) ) ) ) ) ) ) )
=> ( A @ cyclefreeP ) )
& ( ( A @ cyclefreeP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ~ ( ( B @ ( C @ leq ) )
& ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(169,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ cyclefreeP )
| ( A @ sk13 @ ( A @ sk14 @ leq ) )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk14 @ ( A @ sk13 @ leq ) )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( ( A @ sk17 @ ( A @ sk14 @ cons ) @ ( A @ sk16 @ ( A @ sk13 @ cons ) @ ( A @ sk15 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ ( A @ ssList ) )
& ( ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( B @ leq ) )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ cyclefreeP )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[168]) ).
thf(177,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(9206,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,177]) ).
thf(9207,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem ) ),
inference(simp,[status(thm)],[9206]) ).
thf(9208,plain,
( ( sk7 @ cyclefreeP )
| ( sk7 @ sk13 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[9207:[bind(A,$thf( sk7 ))]]) ).
thf(107,plain,
sk2 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(9182,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,177]) ).
thf(9183,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem ) ),
inference(simp,[status(thm)],[9182]) ).
thf(9184,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk13 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[9183:[bind(A,$thf( sk2 ))]]) ).
thf(34,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( nil @ memberP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax38) ).
thf(247,plain,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( nil @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(248,plain,
! [A: $i] :
( ~ ( A @ ( nil @ memberP ) )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[247]) ).
thf(9456,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9184,248]) ).
thf(9457,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9456]) ).
thf(9458,plain,
( ~ ( sk2 @ sk13 @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9457:[bind(A,$thf( sk2 @ sk13 ))]]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ frontsegP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax46) ).
thf(134,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ( nil = A )
=> ( A @ ( nil @ frontsegP ) ) )
& ( ( A @ ( nil @ frontsegP ) )
=> ( nil = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(135,plain,
! [A: $i] :
( ( ( A @ ( nil @ frontsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[134]) ).
thf(136,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[135]) ).
thf(138,plain,
! [A: $i] :
( ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil = A ) ),
inference(lifteq,[status(thm)],[136]) ).
thf(53,axiom,
nil @ ssList,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
thf(360,plain,
nil @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(137,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[135]) ).
thf(139,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[137]) ).
thf(140,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[139]) ).
thf(878,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[140,360]) ).
thf(879,plain,
nil @ ( nil @ frontsegP ),
inference(simp,[status(thm)],[878]) ).
thf(61,axiom,
? [A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
thf(405,plain,
? [A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(406,plain,
( ( sk45 != sk46 )
& ( sk46 @ ssItem )
& ( sk45 @ ssItem ) ),
inference(cnf,[status(esa)],[405]) ).
thf(409,plain,
sk45 != sk46,
inference(cnfConj,[status(thm)],[406]) ).
thf(410,plain,
sk46 != sk45,
inference(lifteq,[status(thm)],[409]) ).
thf(1771,plain,
! [A: $i] :
( ( A != sk46 )
| ( sk45 != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[138,410]) ).
thf(1772,plain,
( ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) )
| ~ ( sk46 @ ssList ) ),
inference(pattern_uni,[status(thm)],[1771:[bind(A,$thf( sk46 ))]]) ).
thf(1951,plain,
( ( ( sk46 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ( sk45 != nil )
| ~ $true
| ~ ( sk46 @ ssList ) ),
inference(paramod_ordered,[status(thm)],[879,1772]) ).
thf(1952,plain,
( ( ( sk46 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ( sk45 != nil )
| ~ ( sk46 @ ssList ) ),
inference(simp,[status(thm)],[1951]) ).
thf(1971,plain,
( ( sk46 != nil )
| ( nil != nil )
| ( sk45 != nil )
| ~ ( sk46 @ ssList ) ),
inference(simp,[status(thm)],[1952]) ).
thf(1982,plain,
( ( sk46 != nil )
| ( sk45 != nil )
| ~ ( sk46 @ ssList ) ),
inference(simp,[status(thm)],[1971]) ).
thf(2266,plain,
( ( ( sk46 @ ssList )
!= ( nil @ ssList ) )
| ( sk46 != nil )
| ( sk45 != nil )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[360,1982]) ).
thf(2267,plain,
( ( ( sk46 @ ssList )
!= ( nil @ ssList ) )
| ( sk46 != nil )
| ( sk45 != nil ) ),
inference(simp,[status(thm)],[2266]) ).
thf(2288,plain,
( ( sk46 != nil )
| ( sk46 != nil )
| ( sk45 != nil ) ),
inference(simp,[status(thm)],[2267]) ).
thf(2291,plain,
( ( sk46 != nil )
| ( sk45 != nil ) ),
inference(simp,[status(thm)],[2288]) ).
thf(2293,plain,
! [A: $i] :
( ( A != sk45 )
| ( sk46 != nil )
| ( nil != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[138,2291]) ).
thf(2294,plain,
! [A: $i] :
( ( A != sk45 )
| ( sk46 != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[2293]) ).
thf(2295,plain,
( ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) )
| ~ ( sk45 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2294:[bind(A,$thf( sk45 ))]]) ).
thf(19,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ strictorderP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
thf(184,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) ) ) ) ) ) ) ) )
=> ( A @ strictorderP ) )
& ( ( A @ strictorderP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(185,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ strictorderP )
| ~ ( A @ sk18 @ ( A @ sk19 @ lt ) )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ~ ( A @ sk19 @ ( A @ sk18 @ lt ) )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( ( A @ sk22 @ ( A @ sk19 @ cons ) @ ( A @ sk21 @ ( A @ sk18 @ cons ) @ ( A @ sk20 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ ( A @ ssList ) )
& ( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ strictorderP )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[184]) ).
thf(187,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(12568,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,187]) ).
thf(12569,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem ) ),
inference(simp,[status(thm)],[12568]) ).
thf(12570,plain,
( ( sk7 @ strictorderP )
| ( sk7 @ sk18 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[12569:[bind(A,$thf( sk7 ))]]) ).
thf(35,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( B @ ( A @ segmentP ) )
=> ( B @ ( D @ ( A @ ( C @ app ) @ app ) @ segmentP ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax56) ).
thf(249,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( B @ ( A @ segmentP ) )
=> ( B @ ( D @ ( A @ ( C @ app ) @ app ) @ segmentP ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(90,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( B @ ( A @ rearsegP ) )
=> ( B @ ( A @ ( C @ app ) @ rearsegP ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax50) ).
thf(518,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( B @ ( A @ rearsegP ) )
=> ( B @ ( A @ ( C @ app ) @ rearsegP ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(78,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax42) ).
thf(468,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(33,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ strictorderedP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ lt ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
thf(234,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ lt ) ) ) ) ) ) ) )
=> ( A @ strictorderedP ) )
& ( ( A @ strictorderedP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ lt ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(101,plain,
sk6 @ ssItem,
inference(cnfConj,[status(thm)],[99]) ).
thf(30,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ neq ) )
<=> ( A != B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
thf(222,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A != B )
=> ( B @ ( A @ neq ) ) )
& ( ( B @ ( A @ neq ) )
=> ( A != B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(223,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ neq ) )
| ( A = B )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) )
& ( ( A != B )
| ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ) ),
inference(cnf,[status(esa)],[222]) ).
thf(224,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(cnfConj,[status(thm)],[223]) ).
thf(226,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ( A != B ) ),
inference(lifteq,[status(thm)],[224]) ).
thf(227,plain,
! [A: $i] :
( ~ ( A @ ( A @ neq ) )
| ~ ( A @ ssItem ) ),
inference(simp,[status(thm)],[226]) ).
thf(1293,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,227]) ).
thf(1294,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[1293]) ).
thf(1295,plain,
~ ( sk6 @ ( sk6 @ neq ) ),
inference(pattern_uni,[status(thm)],[1294:[bind(A,$thf( sk6 ))]]) ).
thf(108,plain,
( ( nil = sk4 )
| sk9 ),
inference(cnfConj,[status(thm)],[99]) ).
thf(127,plain,
( sk9
| ( sk4 = nil ) ),
inference(lifteq,[status(thm)],[108]) ).
thf(119,plain,
sk2 = sk4,
inference(cnfConj,[status(thm)],[99]) ).
thf(125,plain,
sk4 = sk2,
inference(lifteq,[status(thm)],[119]) ).
thf(607,plain,
( sk9
| ( sk2 = nil ) ),
inference(rewrite,[status(thm)],[127,125]) ).
thf(112,plain,
( ~ sk9
| ( sk12 @ ssList ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(608,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk12 @ ssList )
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,112]) ).
thf(609,plain,
( ( sk9 != sk9 )
| ( sk12 @ ssList )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[608]) ).
thf(610,plain,
( ( sk12 @ ssList )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[609:[]]) ).
thf(37,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax57) ).
thf(259,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(260,plain,
! [A: $i] :
( ( nil @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[259]) ).
thf(5591,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[610,260]) ).
thf(5592,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[5591]) ).
thf(5593,plain,
( ( nil @ ( sk12 @ segmentP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[5592:[bind(A,$thf( sk12 ))]]) ).
thf(115,plain,
sk1 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(28,axiom,
~ ( nil @ singletonP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax39) ).
thf(216,plain,
~ ( nil @ singletonP ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(217,plain,
~ ( nil @ singletonP ),
inference(polarity_switch,[status(thm)],[216]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ segmentP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax58) ).
thf(149,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ( nil = A )
=> ( A @ ( nil @ segmentP ) ) )
& ( ( A @ ( nil @ segmentP ) )
=> ( nil = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(150,plain,
! [A: $i] :
( ( ( A @ ( nil @ segmentP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[149]) ).
thf(151,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[150]) ).
thf(153,plain,
! [A: $i] :
( ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil = A ) ),
inference(lifteq,[status(thm)],[151]) ).
thf(2952,plain,
! [A: $i] :
( ( A != sk45 )
| ( sk46 != nil )
| ( nil != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[153,2291]) ).
thf(2953,plain,
! [A: $i] :
( ( A != sk45 )
| ( sk46 != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[2952]) ).
thf(2954,plain,
( ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) )
| ~ ( sk45 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2953:[bind(A,$thf( sk45 ))]]) ).
thf(7113,plain,
( ( ( sk45 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,2954]) ).
thf(7114,plain,
( ( ( sk45 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7113]) ).
thf(7208,plain,
( ( sk45 != sk1 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7114]) ).
thf(408,plain,
sk46 @ ssItem,
inference(cnfConj,[status(thm)],[406]) ).
thf(170,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk13 @ ( A @ sk14 @ leq ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(9619,plain,
! [A: $i] :
( ( ( sk7 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk7 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9208,248]) ).
thf(9620,plain,
! [A: $i] :
( ( ( sk7 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk7 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9619]) ).
thf(9621,plain,
( ~ ( sk7 @ sk13 @ ( nil @ memberP ) )
| ( sk7 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9620:[bind(A,$thf( sk7 @ sk13 ))]]) ).
thf(109,plain,
( ( nil = sk3 )
| sk9 ),
inference(cnfConj,[status(thm)],[99]) ).
thf(122,plain,
( sk9
| ( sk3 = nil ) ),
inference(lifteq,[status(thm)],[109]) ).
thf(116,plain,
sk1 = sk3,
inference(cnfConj,[status(thm)],[99]) ).
thf(121,plain,
sk3 = sk1,
inference(lifteq,[status(thm)],[116]) ).
thf(582,plain,
( sk9
| ( sk1 = nil ) ),
inference(rewrite,[status(thm)],[122,121]) ).
thf(102,plain,
sk8 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(194,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(17012,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,194]) ).
thf(17013,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList ) ),
inference(simp,[status(thm)],[17012]) ).
thf(17014,plain,
( ( sk8 @ strictorderP )
| ( sk8 @ sk22 @ ssList ) ),
inference(pattern_uni,[status(thm)],[17013:[bind(A,$thf( sk8 ))]]) ).
thf(178,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(9672,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,178]) ).
thf(9673,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList ) ),
inference(simp,[status(thm)],[9672]) ).
thf(9674,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk17 @ ssList ) ),
inference(pattern_uni,[status(thm)],[9673:[bind(A,$thf( sk1 ))]]) ).
thf(9899,plain,
! [A: $i] :
( ( ( sk1 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9674,260]) ).
thf(9900,plain,
! [A: $i] :
( ( ( sk1 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9899]) ).
thf(9901,plain,
( ( nil @ ( sk1 @ sk17 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9900:[bind(A,$thf( sk1 @ sk17 ))]]) ).
thf(120,plain,
( ~ sk9
| ( sk10 @ ssItem ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(21,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ segmentP ) )
& ( B @ ( A @ segmentP ) ) )
=> ( C @ ( A @ segmentP ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax53) ).
thf(201,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ segmentP ) )
& ( B @ ( A @ segmentP ) ) )
=> ( C @ ( A @ segmentP ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ segmentP ) )
| ~ ( C @ ( B @ segmentP ) )
| ~ ( B @ ( A @ segmentP ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[201]) ).
thf(118,plain,
( ~ sk9
| ( ( nil @ ( sk10 @ cons ) )
= sk3 ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(123,plain,
( ~ sk9
| ( ( nil @ ( sk10 @ cons ) )
= sk3 ) ),
inference(lifteq,[status(thm)],[118]) ).
thf(597,plain,
( ~ sk9
| ( ( nil @ ( sk10 @ cons ) )
= sk1 ) ),
inference(rewrite,[status(thm)],[123,121]) ).
thf(172,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(6969,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,172]) ).
thf(6970,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList ) ),
inference(simp,[status(thm)],[6969]) ).
thf(6971,plain,
( ( sk7 @ cyclefreeP )
| ( sk7 @ sk16 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6970:[bind(A,$thf( sk7 ))]]) ).
thf(58,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( A @ ( C @ ( B @ app ) @ memberP ) )
<=> ( ( A @ ( C @ memberP ) )
| ( A @ ( B @ memberP ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax36) ).
thf(384,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( ( A @ ( C @ memberP ) )
| ( A @ ( B @ memberP ) ) )
=> ( A @ ( C @ ( B @ app ) @ memberP ) ) )
& ( ( A @ ( C @ ( B @ app ) @ memberP ) )
=> ( ( A @ ( C @ memberP ) )
| ( A @ ( B @ memberP ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(174,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(7024,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,174]) ).
thf(7025,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem ) ),
inference(simp,[status(thm)],[7024]) ).
thf(7026,plain,
( ( sk8 @ cyclefreeP )
| ( sk8 @ sk14 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[7025:[bind(A,$thf( sk8 ))]]) ).
thf(7959,plain,
! [A: $i] :
( ( ( sk8 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk8 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7026,248]) ).
thf(7960,plain,
! [A: $i] :
( ( ( sk8 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk8 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7959]) ).
thf(7961,plain,
( ~ ( sk8 @ sk14 @ ( nil @ memberP ) )
| ( sk8 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7960:[bind(A,$thf( sk8 @ sk14 ))]]) ).
thf(20,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil @ ( A @ app ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax84) ).
thf(198,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil @ ( A @ app ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(199,plain,
! [A: $i] :
( ( ( nil @ ( A @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[198]) ).
thf(200,plain,
! [A: $i] :
( ~ ( A @ ssList )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[199]) ).
thf(21433,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,200]) ).
thf(21434,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A )
| ~ sk9 ),
inference(simp,[status(thm)],[21433]) ).
thf(21435,plain,
( ( ( nil @ ( sk12 @ app ) )
= sk12 )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[21434:[bind(A,$thf( sk12 ))]]) ).
thf(176,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(8340,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,176]) ).
thf(8341,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[8340]) ).
thf(8342,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[8341:[bind(A,$thf( sk1 ))]]) ).
thf(6839,plain,
( ( ( sk45 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,2295]) ).
thf(6840,plain,
( ( ( sk45 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6839]) ).
thf(6851,plain,
( ( sk45 != sk2 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6840]) ).
thf(188,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(13111,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,188]) ).
thf(13112,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList ) ),
inference(simp,[status(thm)],[13111]) ).
thf(13113,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk20 @ ssList ) ),
inference(pattern_uni,[status(thm)],[13112:[bind(A,$thf( sk1 ))]]) ).
thf(7746,plain,
! [A: $i] :
( ( ( sk7 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk7 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6971,260]) ).
thf(7747,plain,
! [A: $i] :
( ( ( sk7 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk7 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7746]) ).
thf(7748,plain,
( ( nil @ ( sk7 @ sk16 @ segmentP ) )
| ( sk7 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7747:[bind(A,$thf( sk7 @ sk16 ))]]) ).
thf(591,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk10 @ ssItem )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,120]) ).
thf(592,plain,
( ( sk9 != sk9 )
| ( sk10 @ ssItem )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[591]) ).
thf(593,plain,
( ( sk10 @ ssItem )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[592:[]]) ).
thf(1308,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[593,227]) ).
thf(1309,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[1308]) ).
thf(1310,plain,
( ~ ( sk10 @ ( sk10 @ neq ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[1309:[bind(A,$thf( sk10 ))]]) ).
thf(94,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ rearsegP ) )
& ( B @ ( A @ rearsegP ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax48) ).
thf(533,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ rearsegP ) )
& ( B @ ( A @ rearsegP ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(3363,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[107,153]) ).
thf(3364,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[3363]) ).
thf(3365,plain,
( ~ ( sk2 @ ( nil @ segmentP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[3364:[bind(A,$thf( sk2 ))]]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ gt ) )
=> ~ ( A @ ( B @ gt ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax94) ).
thf(141,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ gt ) )
=> ~ ( A @ ( B @ gt ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(142,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[141]) ).
thf(117,plain,
( ~ sk9
| ( sk11 @ ssList ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(2983,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,153]) ).
thf(2984,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A )
| ~ sk9 ),
inference(simp,[status(thm)],[2983]) ).
thf(2985,plain,
( ~ ( sk11 @ ( nil @ segmentP ) )
| ( sk11 = nil )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[2984:[bind(A,$thf( sk11 ))]]) ).
thf(6880,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,172]) ).
thf(6881,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList ) ),
inference(simp,[status(thm)],[6880]) ).
thf(6882,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk16 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6881:[bind(A,$thf( sk1 ))]]) ).
thf(7234,plain,
( ( sk1 != sk1 )
| ( sk1 @ cyclefreeP )
| ( nil @ sk16 @ ssList )
| sk9 ),
inference(paramod_ordered,[status(thm)],[582,6882]) ).
thf(7235,plain,
( ( sk1 @ cyclefreeP )
| ( nil @ sk16 @ ssList )
| sk9 ),
inference(pattern_uni,[status(thm)],[7234:[]]) ).
thf(1401,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[138,1295]) ).
thf(1402,plain,
( ~ ( sk6 @ ( nil @ neq ) )
| ~ ( sk6 @ ( nil @ frontsegP ) )
| ~ ( sk6 @ ssList ) ),
inference(pattern_uni,[status(thm)],[1401:[bind(A,$thf( sk6 ))]]) ).
thf(20525,plain,
( ( ( sk6 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ $true
| ~ ( sk6 @ ssList ) ),
inference(paramod_ordered,[status(thm)],[879,1402]) ).
thf(20526,plain,
( ( ( sk6 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[20525]) ).
thf(20641,plain,
( ( sk6 != nil )
| ( nil != nil )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[20526]) ).
thf(20654,plain,
( ( sk6 != nil )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[20641]) ).
thf(20727,plain,
( ( ( sk6 @ ssList )
!= ( nil @ ssList ) )
| ( sk6 != nil )
| ~ ( sk6 @ ( nil @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[360,20654]) ).
thf(20728,plain,
( ( ( sk6 @ ssList )
!= ( nil @ ssList ) )
| ( sk6 != nil )
| ~ ( sk6 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[20727]) ).
thf(20800,plain,
( ( sk6 != nil )
| ( sk6 != nil )
| ~ ( sk6 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[20728]) ).
thf(20845,plain,
( ( sk6 != nil )
| ~ ( sk6 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[20800]) ).
thf(190,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(14186,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,190]) ).
thf(14187,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList ) ),
inference(simp,[status(thm)],[14186]) ).
thf(14188,plain,
( ( sk8 @ strictorderP )
| ( sk8 @ sk21 @ ssList ) ),
inference(pattern_uni,[status(thm)],[14187:[bind(A,$thf( sk8 ))]]) ).
thf(594,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk11 @ ssList )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,117]) ).
thf(595,plain,
( ( sk9 != sk9 )
| ( sk11 @ ssList )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[594]) ).
thf(596,plain,
( ( sk11 @ ssList )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[595:[]]) ).
thf(5619,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[596,260]) ).
thf(5620,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[5619]) ).
thf(5621,plain,
( ( nil @ ( sk11 @ segmentP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[5620:[bind(A,$thf( sk11 ))]]) ).
thf(2955,plain,
! [A: $i] :
( ( A != sk46 )
| ( nil != nil )
| ( sk45 != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[153,2291]) ).
thf(2956,plain,
! [A: $i] :
( ( A != sk46 )
| ( sk45 != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[2955]) ).
thf(2957,plain,
( ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) )
| ~ ( sk46 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2956:[bind(A,$thf( sk46 ))]]) ).
thf(12541,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,187]) ).
thf(12542,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem ) ),
inference(simp,[status(thm)],[12541]) ).
thf(12543,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk18 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[12542:[bind(A,$thf( sk2 ))]]) ).
thf(8103,plain,
( ( ( sk46 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,2957]) ).
thf(8104,plain,
( ( ( sk46 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8103]) ).
thf(8122,plain,
( ( sk46 != sk7 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8104]) ).
thf(59,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax45) ).
thf(389,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(13278,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,188]) ).
thf(13279,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList ) ),
inference(simp,[status(thm)],[13278]) ).
thf(13280,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk20 @ ssList ) ),
inference(pattern_uni,[status(thm)],[13279:[bind(A,$thf( sk2 ))]]) ).
thf(1296,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,227]) ).
thf(1297,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[1296]) ).
thf(1298,plain,
~ ( sk46 @ ( sk46 @ neq ) ),
inference(pattern_uni,[status(thm)],[1297:[bind(A,$thf( sk46 ))]]) ).
thf(9714,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,178]) ).
thf(9715,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList ) ),
inference(simp,[status(thm)],[9714]) ).
thf(9716,plain,
( ( sk8 @ cyclefreeP )
| ( sk8 @ sk17 @ ssList ) ),
inference(pattern_uni,[status(thm)],[9715:[bind(A,$thf( sk8 ))]]) ).
thf(10051,plain,
! [A: $i] :
( ( ( sk8 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk8 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9716,260]) ).
thf(10052,plain,
! [A: $i] :
( ( ( sk8 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(simp,[status(thm)],[10051]) ).
thf(10053,plain,
( ( nil @ ( sk8 @ sk17 @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[10052:[bind(A,$thf( sk8 @ sk17 ))]]) ).
thf(84,axiom,
nil @ equalelemsP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax74) ).
thf(504,plain,
nil @ equalelemsP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(110,plain,
sk5 @ ssItem,
inference(cnfConj,[status(thm)],[99]) ).
thf(21352,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,200]) ).
thf(21353,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A )
| ~ sk9 ),
inference(simp,[status(thm)],[21352]) ).
thf(21354,plain,
( ( ( nil @ ( sk11 @ app ) )
= sk11 )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[21353:[bind(A,$thf( sk11 ))]]) ).
thf(619,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk10 @ ssItem )
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,120]) ).
thf(620,plain,
( ( sk9 != sk9 )
| ( sk10 @ ssItem )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[619]) ).
thf(621,plain,
( ( sk10 @ ssItem )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[620:[]]) ).
thf(1311,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[621,227]) ).
thf(1312,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[1311]) ).
thf(1313,plain,
( ~ ( sk10 @ ( sk10 @ neq ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[1312:[bind(A,$thf( sk10 ))]]) ).
thf(13,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ frontsegP ) )
& ( B @ ( A @ frontsegP ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax41) ).
thf(157,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ frontsegP ) )
& ( B @ ( A @ frontsegP ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(9798,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,178]) ).
thf(9799,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList ) ),
inference(simp,[status(thm)],[9798]) ).
thf(9800,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk17 @ ssList ) ),
inference(pattern_uni,[status(thm)],[9799:[bind(A,$thf( sk2 ))]]) ).
thf(6903,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,172]) ).
thf(6904,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList ) ),
inference(simp,[status(thm)],[6903]) ).
thf(6905,plain,
( ( sk8 @ cyclefreeP )
| ( sk8 @ sk16 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6904:[bind(A,$thf( sk8 ))]]) ).
thf(14332,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,190]) ).
thf(14333,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList ) ),
inference(simp,[status(thm)],[14332]) ).
thf(14334,plain,
( ( sk7 @ strictorderP )
| ( sk7 @ sk21 @ ssList ) ),
inference(pattern_uni,[status(thm)],[14333:[bind(A,$thf( sk7 ))]]) ).
thf(114,plain,
! [A: $i] :
( ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ ( A @ ssItem ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(558,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,114]) ).
thf(559,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) ) ),
inference(simp,[status(thm)],[558]) ).
thf(560,plain,
( ~ sk9
| ~ ( sk6 @ ( sk10 @ lt ) )
| ~ ( sk6 @ ( sk11 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[559:[bind(A,$thf( sk6 ))]]) ).
thf(604,plain,
( ( sk9 != sk9 )
| ~ $true
| ~ ( sk6 @ ( sk10 @ lt ) )
| ~ ( sk6 @ ( sk11 @ memberP ) )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,560]) ).
thf(605,plain,
( ( sk9 != sk9 )
| ~ ( sk6 @ ( sk10 @ lt ) )
| ~ ( sk6 @ ( sk11 @ memberP ) )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[604]) ).
thf(606,plain,
( ~ ( sk6 @ ( sk10 @ lt ) )
| ~ ( sk6 @ ( sk11 @ memberP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[605:[]]) ).
thf(152,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[150]) ).
thf(154,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[152]) ).
thf(155,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[154]) ).
thf(880,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[155,360]) ).
thf(881,plain,
nil @ ( nil @ segmentP ),
inference(simp,[status(thm)],[880]) ).
thf(23,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax55) ).
thf(206,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(207,plain,
! [A: $i] :
( ( A @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[206]) ).
thf(25245,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,207]) ).
thf(25246,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[25245]) ).
thf(25247,plain,
sk2 @ ( sk2 @ segmentP ),
inference(pattern_uni,[status(thm)],[25246:[bind(A,$thf( sk2 ))]]) ).
thf(41,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
!= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
thf(289,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
!= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(74,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ rearsegP ) )
<=> ? [C: $i] :
( ( ( B @ ( C @ app ) )
= A )
& ( C @ ssList ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
thf(448,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ? [C: $i] :
( ( ( B @ ( C @ app ) )
= A )
& ( C @ ssList ) )
=> ( B @ ( A @ rearsegP ) ) )
& ( ( B @ ( A @ rearsegP ) )
=> ? [C: $i] :
( ( ( B @ ( C @ app ) )
= A )
& ( C @ ssList ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(47,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssItem )
=> ( ( ( A @ ( C @ cons ) )
= ( B @ ( D @ cons ) ) )
=> ( ( B = A )
& ( C = D ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
thf(316,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssItem )
=> ( ( ( A @ ( C @ cons ) )
= ( B @ ( D @ cons ) ) )
=> ( ( B = A )
& ( C = D ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(38,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ tl )
= B )
& ( B @ ssList ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax76) ).
thf(261,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ tl )
= B )
& ( B @ ssList ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(5,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderedP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax68) ).
thf(132,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(133,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[132]) ).
thf(1230,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,133]) ).
thf(1231,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[1230]) ).
thf(1232,plain,
nil @ ( sk6 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[1231:[bind(A,$thf( sk6 ))]]) ).
thf(7186,plain,
( ( ( sk45 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,2954]) ).
thf(7187,plain,
( ( ( sk45 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7186]) ).
thf(7209,plain,
( ( sk45 != sk7 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7187]) ).
thf(64,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ duplicatefreeP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax71) ).
thf(421,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ duplicatefreeP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(15,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( B @ ( A @ frontsegP ) )
=> ( B @ ( C @ ( A @ app ) @ frontsegP ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax43) ).
thf(163,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( B @ ( A @ frontsegP ) )
=> ( B @ ( C @ ( A @ app ) @ frontsegP ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(164,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ app ) @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[163]) ).
thf(13293,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,188]) ).
thf(13294,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList ) ),
inference(simp,[status(thm)],[13293]) ).
thf(13295,plain,
( ( sk7 @ strictorderP )
| ( sk7 @ sk20 @ ssList ) ),
inference(pattern_uni,[status(thm)],[13294:[bind(A,$thf( sk7 ))]]) ).
thf(1680,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,138]) ).
thf(1681,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A )
| ~ sk9 ),
inference(simp,[status(thm)],[1680]) ).
thf(1682,plain,
( ~ ( sk12 @ ( nil @ frontsegP ) )
| ( sk12 = nil )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[1681:[bind(A,$thf( sk12 ))]]) ).
thf(106,plain,
~ ( sk6 @ ( sk5 @ neq ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(25084,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,207]) ).
thf(25085,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[25084]) ).
thf(25086,plain,
sk1 @ ( sk1 @ segmentP ),
inference(pattern_uni,[status(thm)],[25085:[bind(A,$thf( sk1 ))]]) ).
thf(8097,plain,
( ( ( sk46 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,2957]) ).
thf(8098,plain,
( ( ( sk46 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8097]) ).
thf(8109,plain,
( ( sk46 != sk2 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8098]) ).
thf(1841,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[100,138]) ).
thf(1842,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[1841]) ).
thf(1843,plain,
( ~ ( sk7 @ ( nil @ frontsegP ) )
| ( sk7 = nil ) ),
inference(pattern_uni,[status(thm)],[1842:[bind(A,$thf( sk7 ))]]) ).
thf(6945,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,172]) ).
thf(6946,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ sk9 ),
inference(simp,[status(thm)],[6945]) ).
thf(6947,plain,
( ( sk12 @ cyclefreeP )
| ( sk12 @ sk16 @ ssList )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[6946:[bind(A,$thf( sk12 ))]]) ).
thf(8376,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,176]) ).
thf(8377,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[8376]) ).
thf(8378,plain,
( ( sk8 @ cyclefreeP )
| ( sk8 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[8377:[bind(A,$thf( sk8 ))]]) ).
thf(8689,plain,
! [A: $i] :
( ( ( sk8 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk8 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[8378,260]) ).
thf(8690,plain,
! [A: $i] :
( ( ( sk8 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(simp,[status(thm)],[8689]) ).
thf(8691,plain,
( ( nil @ ( sk8 @ sk15 @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[8690:[bind(A,$thf( sk8 @ sk15 ))]]) ).
thf(62,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( A @ ( C @ ( B @ cons ) @ memberP ) )
<=> ( ( A @ ( C @ memberP ) )
| ( A = B ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax37) ).
thf(411,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( ( A @ ( C @ memberP ) )
| ( A = B ) )
=> ( A @ ( C @ ( B @ cons ) @ memberP ) ) )
& ( ( A @ ( C @ ( B @ cons ) @ memberP ) )
=> ( ( A @ ( C @ memberP ) )
| ( A = B ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(67,axiom,
nil @ strictorderP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax64) ).
thf(428,plain,
nil @ strictorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(86,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ segmentP ) )
& ( B @ ( A @ segmentP ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax54) ).
thf(507,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A @ ( B @ segmentP ) )
& ( B @ ( A @ segmentP ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(45,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax51) ).
thf(312,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(8457,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,176]) ).
thf(8458,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[8457]) ).
thf(8459,plain,
( ( sk7 @ cyclefreeP )
| ( sk7 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[8458:[bind(A,$thf( sk7 ))]]) ).
thf(3241,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,153]) ).
thf(3242,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A )
| ~ sk9 ),
inference(simp,[status(thm)],[3241]) ).
thf(3243,plain,
( ~ ( sk12 @ ( nil @ segmentP ) )
| ( sk12 = nil )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[3242:[bind(A,$thf( sk12 ))]]) ).
thf(1945,plain,
( ( ( sk46 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,1772]) ).
thf(1946,plain,
( ( ( sk46 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1945]) ).
thf(1975,plain,
( ( sk46 != sk1 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1946]) ).
thf(7076,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,174]) ).
thf(7077,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem ) ),
inference(simp,[status(thm)],[7076]) ).
thf(7078,plain,
( ( sk7 @ cyclefreeP )
| ( sk7 @ sk14 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[7077:[bind(A,$thf( sk7 ))]]) ).
thf(8287,plain,
! [A: $i] :
( ( ( sk7 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk7 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7078,248]) ).
thf(8288,plain,
! [A: $i] :
( ( ( sk7 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk7 @ cyclefreeP ) ),
inference(simp,[status(thm)],[8287]) ).
thf(8289,plain,
( ~ ( sk7 @ sk14 @ ( nil @ memberP ) )
| ( sk7 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[8288:[bind(A,$thf( sk7 @ sk14 ))]]) ).
thf(42,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ cons ) @ strictorderedP )
<=> ( ( ( B @ hd @ ( A @ lt ) )
& ( B @ strictorderedP )
& ( nil != B ) )
| ( nil = B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax70) ).
thf(292,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( ( B @ hd @ ( A @ lt ) )
& ( B @ strictorderedP )
& ( nil != B ) )
| ( nil = B ) )
=> ( B @ ( A @ cons ) @ strictorderedP ) )
& ( ( B @ ( A @ cons ) @ strictorderedP )
=> ( ( ( B @ hd @ ( A @ lt ) )
& ( B @ strictorderedP )
& ( nil != B ) )
| ( nil = B ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(97,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ geq ) )
<=> ( A @ ( B @ leq ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax32) ).
thf(546,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ leq ) )
=> ( B @ ( A @ geq ) ) )
& ( ( B @ ( A @ geq ) )
=> ( A @ ( B @ leq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(7004,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,174]) ).
thf(7005,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem ) ),
inference(simp,[status(thm)],[7004]) ).
thf(7006,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk14 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[7005:[bind(A,$thf( sk1 ))]]) ).
thf(7857,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7006,248]) ).
thf(7858,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7857]) ).
thf(7859,plain,
( ~ ( sk1 @ sk14 @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7858:[bind(A,$thf( sk1 @ sk14 ))]]) ).
thf(25154,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,207]) ).
thf(25155,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[25154]) ).
thf(25156,plain,
sk8 @ ( sk8 @ segmentP ),
inference(pattern_uni,[status(thm)],[25155:[bind(A,$thf( sk8 ))]]) ).
thf(21355,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[102,200]) ).
thf(21356,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[21355]) ).
thf(21357,plain,
( ( nil @ ( sk8 @ app ) )
= sk8 ),
inference(pattern_uni,[status(thm)],[21356:[bind(A,$thf( sk8 ))]]) ).
thf(7826,plain,
( ( sk1 != sk1 )
| ( sk1 @ cyclefreeP )
| ( nil @ sk14 @ ssItem )
| sk9 ),
inference(paramod_ordered,[status(thm)],[582,7006]) ).
thf(7827,plain,
( ( sk1 @ cyclefreeP )
| ( nil @ sk14 @ ssItem )
| sk9 ),
inference(pattern_uni,[status(thm)],[7826:[]]) ).
thf(14,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax81) ).
thf(160,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(68,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( ( A @ tl @ ( A @ hd @ cons ) )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax78) ).
thf(429,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( ( A @ tl @ ( A @ hd @ cons ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(16,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( C @ ( B @ ( A @ app ) @ app ) )
= ( C @ ( B @ app ) @ ( A @ app ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax82) ).
thf(165,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( C @ ( B @ ( A @ app ) @ app ) )
= ( C @ ( B @ app ) @ ( A @ app ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(1236,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,133]) ).
thf(1237,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[1236]) ).
thf(1238,plain,
nil @ ( sk46 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[1237:[bind(A,$thf( sk46 ))]]) ).
thf(17176,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,194]) ).
thf(17177,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList ) ),
inference(simp,[status(thm)],[17176]) ).
thf(17178,plain,
( ( sk7 @ strictorderP )
| ( sk7 @ sk22 @ ssList ) ),
inference(pattern_uni,[status(thm)],[17177:[bind(A,$thf( sk7 ))]]) ).
thf(21475,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[107,200]) ).
thf(21476,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[21475]) ).
thf(21477,plain,
( ( nil @ ( sk2 @ app ) )
= sk2 ),
inference(pattern_uni,[status(thm)],[21476:[bind(A,$thf( sk2 ))]]) ).
thf(192,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ sk19 @ ( A @ sk18 @ lt ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(407,plain,
sk45 @ ssItem,
inference(cnfConj,[status(thm)],[406]) ).
thf(13156,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,188]) ).
thf(13157,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk20 @ ssList ) ),
inference(simp,[status(thm)],[13156]) ).
thf(13158,plain,
( ( sk8 @ strictorderP )
| ( sk8 @ sk20 @ ssList ) ),
inference(pattern_uni,[status(thm)],[13157:[bind(A,$thf( sk8 ))]]) ).
thf(191,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ strictorderP )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(196,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ lt ) )
| ( C @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ strictorderP )
| ~ ( A @ ssList )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A ) ),
inference(lifteq,[status(thm)],[191]) ).
thf(197,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ lt ) )
| ( B @ ( A @ lt ) )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) @ strictorderP )
| ~ ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) @ ssList ) ),
inference(simp,[status(thm)],[196]) ).
thf(54,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( B @ tl )
= ( A @ tl ) )
& ( ( B @ hd )
= ( A @ hd ) )
& ( nil != A )
& ( nil != B ) )
=> ( B = A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax77) ).
thf(361,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( B @ tl )
= ( A @ tl ) )
& ( ( B @ hd )
= ( A @ hd ) )
& ( nil != A )
& ( nil != B ) )
=> ( B = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(92,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( nil
!= ( A @ ( B @ cons ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
thf(522,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( nil
!= ( A @ ( B @ cons ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(103,plain,
! [A: $i] :
( ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ ( A @ ssItem ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(126,plain,
! [A: $i] :
( ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ ( A @ ssItem ) ),
inference(simp,[status(thm)],[103]) ).
thf(755,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[407,126]) ).
thf(756,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) ) ),
inference(simp,[status(thm)],[755]) ).
thf(757,plain,
( ~ sk9
| ~ ( sk10 @ ( sk45 @ lt ) )
| ~ ( sk45 @ ( sk12 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[756:[bind(A,$thf( sk45 ))]]) ).
thf(75,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ rearsegP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax52) ).
thf(456,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ( nil = A )
=> ( A @ ( nil @ rearsegP ) ) )
& ( ( A @ ( nil @ rearsegP ) )
=> ( nil = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(31,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ app ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
thf(229,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ app ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(564,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[407,114]) ).
thf(565,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) ) ),
inference(simp,[status(thm)],[564]) ).
thf(566,plain,
( ~ sk9
| ~ ( sk45 @ ( sk10 @ lt ) )
| ~ ( sk45 @ ( sk11 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[565:[bind(A,$thf( sk45 ))]]) ).
thf(576,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[120,114]) ).
thf(577,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ sk9 ),
inference(simp,[status(thm)],[576]) ).
thf(578,plain,
( ~ ( sk10 @ ( sk10 @ lt ) )
| ~ ( sk10 @ ( sk11 @ memberP ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[577:[bind(A,$thf( sk10 ))]]) ).
thf(5607,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,260]) ).
thf(5608,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ sk9 ),
inference(simp,[status(thm)],[5607]) ).
thf(5609,plain,
( ( nil @ ( sk12 @ segmentP ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[5608:[bind(A,$thf( sk12 ))]]) ).
thf(8543,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[8342,260]) ).
thf(8544,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[8543]) ).
thf(8545,plain,
( ( nil @ ( sk1 @ sk15 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[8544:[bind(A,$thf( sk1 @ sk15 ))]]) ).
thf(12,axiom,
nil @ cyclefreeP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax60) ).
thf(156,plain,
nil @ cyclefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(21496,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[100,200]) ).
thf(21497,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[21496]) ).
thf(21498,plain,
( ( nil @ ( sk7 @ app ) )
= sk7 ),
inference(pattern_uni,[status(thm)],[21497:[bind(A,$thf( sk7 ))]]) ).
thf(625,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk11 @ ssList )
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,117]) ).
thf(626,plain,
( ( sk9 != sk9 )
| ( sk11 @ ssList )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[625]) ).
thf(627,plain,
( ( sk11 @ ssList )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[626:[]]) ).
thf(5613,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[627,260]) ).
thf(5614,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[5613]) ).
thf(5615,plain,
( ( nil @ ( sk11 @ segmentP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[5614:[bind(A,$thf( sk11 ))]]) ).
thf(1967,plain,
( ( ( sk46 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,1772]) ).
thf(1968,plain,
( ( ( sk46 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1967]) ).
thf(1970,plain,
( ( sk46 != sk7 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1968]) ).
thf(8045,plain,
( ( ( sk46 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,2957]) ).
thf(8046,plain,
( ( ( sk46 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8045]) ).
thf(8117,plain,
( ( sk46 != sk8 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8046]) ).
thf(2988,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[102,153]) ).
thf(2989,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[2988]) ).
thf(2990,plain,
( ~ ( sk8 @ ( nil @ segmentP ) )
| ( sk8 = nil ) ),
inference(pattern_uni,[status(thm)],[2989:[bind(A,$thf( sk8 ))]]) ).
thf(193,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(16282,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,193]) ).
thf(16283,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem ) ),
inference(simp,[status(thm)],[16282]) ).
thf(16284,plain,
( ( sk8 @ strictorderP )
| ( sk8 @ sk19 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[16283:[bind(A,$thf( sk8 ))]]) ).
thf(49,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( D @ ( B @ cons ) @ ( C @ ( A @ cons ) @ frontsegP ) )
<=> ( ( D @ ( C @ frontsegP ) )
& ( A = B ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax44) ).
thf(328,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( D @ ( C @ frontsegP ) )
& ( A = B ) )
=> ( D @ ( B @ cons ) @ ( C @ ( A @ cons ) @ frontsegP ) ) )
& ( ( D @ ( B @ cons ) @ ( C @ ( A @ cons ) @ frontsegP ) )
=> ( ( D @ ( C @ frontsegP ) )
& ( A = B ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(1491,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[102,138]) ).
thf(1492,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[1491]) ).
thf(1493,plain,
( ~ ( sk8 @ ( nil @ frontsegP ) )
| ( sk8 = nil ) ),
inference(pattern_uni,[status(thm)],[1492:[bind(A,$thf( sk8 ))]]) ).
thf(104,plain,
( ( sk8 @ ( nil @ ( sk6 @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( sk7 @ app ) @ app ) @ app ) )
= sk1 ),
inference(cnfConj,[status(thm)],[99]) ).
thf(124,plain,
( ( sk8 @ ( nil @ ( sk6 @ cons ) @ ( nil @ ( sk5 @ cons ) @ ( sk7 @ app ) @ app ) @ app ) )
= sk1 ),
inference(lifteq,[status(thm)],[104]) ).
thf(51,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ neq ) )
<=> ( A != B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
thf(339,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( A != B )
=> ( B @ ( A @ neq ) ) )
& ( ( B @ ( A @ neq ) )
=> ( A != B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(552,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,248]) ).
thf(553,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[552]) ).
thf(554,plain,
~ ( sk6 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[553:[bind(A,$thf( sk6 ))]]) ).
thf(1412,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[115,138]) ).
thf(1413,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[1412]) ).
thf(1414,plain,
( ~ ( sk1 @ ( nil @ frontsegP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[1413:[bind(A,$thf( sk1 ))]]) ).
thf(96,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ memberP ) )
<=> ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ cons ) @ ( C @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
thf(537,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ cons ) @ ( C @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) )
=> ( B @ ( A @ memberP ) ) )
& ( ( B @ ( A @ memberP ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ cons ) @ ( C @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(8022,plain,
( ( ( sk46 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,2957]) ).
thf(8023,plain,
( ( ( sk46 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8022]) ).
thf(8132,plain,
( ( sk46 != sk1 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8023]) ).
thf(82,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ rearsegP ) )
& ( B @ ( A @ rearsegP ) ) )
=> ( C @ ( A @ rearsegP ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax47) ).
thf(489,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ rearsegP ) )
& ( B @ ( A @ rearsegP ) ) )
=> ( C @ ( A @ rearsegP ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(1247,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[593,133]) ).
thf(1248,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[1247]) ).
thf(1249,plain,
( ( nil @ ( sk10 @ cons ) @ strictorderedP )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[1248:[bind(A,$thf( sk10 ))]]) ).
thf(1949,plain,
( ( ( sk46 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,1772]) ).
thf(1950,plain,
( ( ( sk46 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1949]) ).
thf(1974,plain,
( ( sk46 != sk8 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1950]) ).
thf(3,axiom,
nil @ strictorderedP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax69) ).
thf(129,plain,
nil @ strictorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(567,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[407,248]) ).
thf(568,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[567]) ).
thf(569,plain,
~ ( sk45 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[568:[bind(A,$thf( sk45 ))]]) ).
thf(1244,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[110,133]) ).
thf(1245,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[1244]) ).
thf(1246,plain,
nil @ ( sk5 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[1245:[bind(A,$thf( sk5 ))]]) ).
thf(1239,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[120,133]) ).
thf(1240,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ sk9 ),
inference(simp,[status(thm)],[1239]) ).
thf(1241,plain,
( ( nil @ ( sk10 @ cons ) @ strictorderedP )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[1240:[bind(A,$thf( sk10 ))]]) ).
thf(22,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( B @ ( C @ app ) )
= ( B @ ( A @ app ) ) )
=> ( C = A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax79) ).
thf(203,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( B @ ( C @ app ) )
= ( B @ ( A @ app ) ) )
=> ( C = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(204,plain,
! [C: $i,B: $i,A: $i] :
( ( C = A )
| ( ( B @ ( C @ app ) )
!= ( B @ ( A @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[203]) ).
thf(205,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( C = A )
| ( ( B @ ( C @ app ) )
!= ( B @ ( A @ app ) ) ) ),
inference(lifteq,[status(thm)],[204]) ).
thf(56,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( nil
= ( B @ ( A @ app ) ) )
<=> ( ( nil = A )
& ( nil = B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax83) ).
thf(373,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( nil = A )
& ( nil = B ) )
=> ( nil
= ( B @ ( A @ app ) ) ) )
& ( ( nil
= ( B @ ( A @ app ) ) )
=> ( ( nil = A )
& ( nil = B ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(374,plain,
! [B: $i,A: $i] :
( ( ( nil
= ( B @ ( A @ app ) ) )
| ( nil != A )
| ( nil != B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ( nil
!= ( B @ ( A @ app ) ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) )
& ( ( nil = B )
| ( nil
!= ( B @ ( A @ app ) ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[373]) ).
thf(377,plain,
! [B: $i,A: $i] :
( ( nil
= ( B @ ( A @ app ) ) )
| ( nil != A )
| ( nil != B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[374]) ).
thf(380,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
= nil )
| ( nil != A )
| ( nil != B ) ),
inference(lifteq,[status(thm)],[377]) ).
thf(381,plain,
( ~ ( nil @ ssList )
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(simp,[status(thm)],[380]) ).
thf(1034,plain,
( ~ $true
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(rewrite,[status(thm)],[381,360]) ).
thf(1035,plain,
( ( nil @ ( nil @ app ) )
= nil ),
inference(simp,[status(thm)],[1034]) ).
thf(3420,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[100,153]) ).
thf(3421,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[3420]) ).
thf(3422,plain,
( ~ ( sk7 @ ( nil @ segmentP ) )
| ( sk7 = nil ) ),
inference(pattern_uni,[status(thm)],[3421:[bind(A,$thf( sk7 ))]]) ).
thf(10188,plain,
! [A: $i] :
( ( ( sk2 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9800,260]) ).
thf(10189,plain,
! [A: $i] :
( ( ( sk2 @ sk17 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[10188]) ).
thf(10190,plain,
( ( nil @ ( sk2 @ sk17 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[10189:[bind(A,$thf( sk2 @ sk17 ))]]) ).
thf(9107,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,177]) ).
thf(9108,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem ) ),
inference(simp,[status(thm)],[9107]) ).
thf(9109,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk13 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[9108:[bind(A,$thf( sk1 ))]]) ).
thf(9267,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9109,248]) ).
thf(9268,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9267]) ).
thf(9269,plain,
( ~ ( sk1 @ sk13 @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9268:[bind(A,$thf( sk1 @ sk13 ))]]) ).
thf(88,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
thf(513,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(10,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ hd )
= B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
thf(146,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ hd )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ cons ) @ hd )
= B )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[146]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( ( A @ ( B @ cons ) @ hd )
= B ) ),
inference(lifteq,[status(thm)],[147]) ).
thf(1299,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[120,227]) ).
thf(1300,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ sk9 ),
inference(simp,[status(thm)],[1299]) ).
thf(1301,plain,
( ~ ( sk10 @ ( sk10 @ neq ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[1300:[bind(A,$thf( sk10 ))]]) ).
thf(173,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( B @ leq ) )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(179,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ leq ) )
| ~ ( C @ ( B @ leq ) )
| ~ ( F @ ssList )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ cyclefreeP )
| ~ ( A @ ssList )
| ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
!= A ) ),
inference(lifteq,[status(thm)],[173]) ).
thf(180,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ~ ( E @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) @ cyclefreeP )
| ~ ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) @ ssList ) ),
inference(simp,[status(thm)],[179]) ).
thf(72,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
thf(444,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(65,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ app ) )
= ( A @ ( B @ app ) ) )
=> ( C = A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax80) ).
thf(423,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ app ) )
= ( A @ ( B @ app ) ) )
=> ( C = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(770,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[110,126]) ).
thf(771,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) ) ),
inference(simp,[status(thm)],[770]) ).
thf(772,plain,
( ~ sk9
| ~ ( sk10 @ ( sk5 @ lt ) )
| ~ ( sk5 @ ( sk12 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[771:[bind(A,$thf( sk5 ))]]) ).
thf(583,plain,
( ( sk9 != sk9 )
| ~ $true
| ( sk12 @ ssList )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,112]) ).
thf(584,plain,
( ( sk9 != sk9 )
| ( sk12 @ ssList )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
( ( sk12 @ ssList )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[584:[]]) ).
thf(5610,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[585,260]) ).
thf(5611,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[5610]) ).
thf(5612,plain,
( ( nil @ ( sk12 @ segmentP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[5611:[bind(A,$thf( sk12 ))]]) ).
thf(40,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ? [B: $i] :
( ? [C: $i] :
( ( ( B @ ( C @ cons ) )
= A )
& ( C @ ssItem ) )
& ( B @ ssList ) )
| ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
thf(281,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ? [B: $i] :
( ? [C: $i] :
( ( ( B @ ( C @ cons ) )
= A )
& ( C @ ssItem ) )
& ( B @ ssList ) )
| ( nil = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(1486,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A )
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,138]) ).
thf(1487,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A )
| ~ sk9 ),
inference(simp,[status(thm)],[1486]) ).
thf(1488,plain,
( ~ ( sk11 @ ( nil @ frontsegP ) )
| ( sk11 = nil )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[1487:[bind(A,$thf( sk11 ))]]) ).
thf(21302,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[115,200]) ).
thf(21303,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[21302]) ).
thf(21304,plain,
( ( nil @ ( sk1 @ app ) )
= sk1 ),
inference(pattern_uni,[status(thm)],[21303:[bind(A,$thf( sk1 ))]]) ).
thf(12439,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,187]) ).
thf(12440,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem ) ),
inference(simp,[status(thm)],[12439]) ).
thf(12441,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk18 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[12440:[bind(A,$thf( sk1 ))]]) ).
thf(60,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ duplicatefreeP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( B != C ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
thf(391,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( B != C ) ) ) ) ) ) )
=> ( A @ duplicatefreeP ) )
& ( ( A @ duplicatefreeP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( B != C ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(1784,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[107,138]) ).
thf(1785,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[1784]) ).
thf(1786,plain,
( ~ ( sk2 @ ( nil @ frontsegP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[1785:[bind(A,$thf( sk2 ))]]) ).
thf(9,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ frontsegP ) )
& ( B @ ( A @ frontsegP ) ) )
=> ( C @ ( A @ frontsegP ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax40) ).
thf(144,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( B @ frontsegP ) )
& ( B @ ( A @ frontsegP ) ) )
=> ( C @ ( A @ frontsegP ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(14132,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,190]) ).
thf(14133,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList ) ),
inference(simp,[status(thm)],[14132]) ).
thf(14134,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk21 @ ssList ) ),
inference(pattern_uni,[status(thm)],[14133:[bind(A,$thf( sk1 ))]]) ).
thf(77,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ lt ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ lt ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax91) ).
thf(466,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ lt ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ lt ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(6963,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,172]) ).
thf(6964,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList ) ),
inference(simp,[status(thm)],[6963]) ).
thf(6965,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk16 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6964:[bind(A,$thf( sk2 ))]]) ).
thf(7534,plain,
! [A: $i] :
( ( ( sk2 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6965,260]) ).
thf(7535,plain,
! [A: $i] :
( ( ( sk2 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7534]) ).
thf(7536,plain,
( ( nil @ ( sk2 @ sk16 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7535:[bind(A,$thf( sk2 @ sk16 ))]]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[157]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( A = B ) ),
inference(lifteq,[status(thm)],[158]) ).
thf(57,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax61) ).
thf(382,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(7132,plain,
( ( ( sk45 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,2954]) ).
thf(7133,plain,
( ( ( sk45 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7132]) ).
thf(7201,plain,
( ( sk45 != sk8 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7133]) ).
thf(570,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,114]) ).
thf(571,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) ) ),
inference(simp,[status(thm)],[570]) ).
thf(572,plain,
( ~ sk9
| ~ ( sk46 @ ( sk10 @ lt ) )
| ~ ( sk46 @ ( sk11 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[571:[bind(A,$thf( sk46 ))]]) ).
thf(1996,plain,
( ( ( nil @ ( sk10 @ cons ) )
!= ( nil @ ( sk10 @ cons ) ) )
| ( sk1 @ strictorderedP )
| ~ sk9
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[597,1241]) ).
thf(1997,plain,
( ( ( nil @ ( sk10 @ cons ) )
!= ( nil @ ( sk10 @ cons ) ) )
| ( sk1 @ strictorderedP )
| ~ sk9 ),
inference(simp,[status(thm)],[1996]) ).
thf(1998,plain,
( ( sk1 @ strictorderedP )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[1997:[]]) ).
thf(2027,plain,
( ( sk9 != sk9 )
| ( sk1 @ strictorderedP )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,1998]) ).
thf(2028,plain,
( ( sk9 != sk9 )
| ( sk1 @ strictorderedP )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[2027]) ).
thf(2029,plain,
( ( sk1 @ strictorderedP )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[2028:[]]) ).
thf(171,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( ( A @ sk17 @ ( A @ sk14 @ cons ) @ ( A @ sk16 @ ( A @ sk13 @ cons ) @ ( A @ sk15 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(181,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ~ ( A @ ssList )
| ( ( A @ sk17 @ ( A @ sk14 @ cons ) @ ( A @ sk16 @ ( A @ sk13 @ cons ) @ ( A @ sk15 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[171]) ).
thf(1403,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[138,1295]) ).
thf(1404,plain,
( ~ ( nil @ ( sk6 @ neq ) )
| ~ ( sk6 @ ( nil @ frontsegP ) )
| ~ ( sk6 @ ssList ) ),
inference(pattern_uni,[status(thm)],[1403:[bind(A,$thf( sk6 ))]]) ).
thf(24595,plain,
( ( ( sk6 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ $true
| ~ ( sk6 @ ssList ) ),
inference(paramod_ordered,[status(thm)],[879,1404]) ).
thf(24596,plain,
( ( ( sk6 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[24595]) ).
thf(24690,plain,
( ( sk6 != nil )
| ( nil != nil )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[24596]) ).
thf(24739,plain,
( ( sk6 != nil )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ ( sk6 @ ssList ) ),
inference(simp,[status(thm)],[24690]) ).
thf(24803,plain,
( ( ( sk6 @ ssList )
!= ( nil @ ssList ) )
| ( sk6 != nil )
| ~ ( nil @ ( sk6 @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[360,24739]) ).
thf(24804,plain,
( ( ( sk6 @ ssList )
!= ( nil @ ssList ) )
| ( sk6 != nil )
| ~ ( nil @ ( sk6 @ neq ) ) ),
inference(simp,[status(thm)],[24803]) ).
thf(24873,plain,
( ( sk6 != nil )
| ( sk6 != nil )
| ~ ( nil @ ( sk6 @ neq ) ) ),
inference(simp,[status(thm)],[24804]) ).
thf(24919,plain,
( ( sk6 != nil )
| ~ ( nil @ ( sk6 @ neq ) ) ),
inference(simp,[status(thm)],[24873]) ).
thf(63,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ geq ) )
& ( B @ ( A @ geq ) ) )
=> ( C @ ( A @ geq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax88) ).
thf(419,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ geq ) )
& ( B @ ( A @ geq ) ) )
=> ( C @ ( A @ geq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(70,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ singletonP )
<=> ? [B: $i] :
( ( ( nil @ ( B @ cons ) )
= A )
& ( B @ ssItem ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
thf(434,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ? [B: $i] :
( ( ( nil @ ( B @ cons ) )
= A )
& ( B @ ssItem ) )
=> ( A @ singletonP ) )
& ( ( A @ singletonP )
=> ? [B: $i] :
( ( ( nil @ ( B @ cons ) )
= A )
& ( B @ ssItem ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(2869,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[115,153]) ).
thf(2870,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[2869]) ).
thf(2871,plain,
( ~ ( sk1 @ ( nil @ segmentP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[2870:[bind(A,$thf( sk1 ))]]) ).
thf(1305,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[407,227]) ).
thf(1306,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[1305]) ).
thf(1307,plain,
~ ( sk45 @ ( sk45 @ neq ) ),
inference(pattern_uni,[status(thm)],[1306:[bind(A,$thf( sk45 ))]]) ).
thf(7413,plain,
! [A: $i] :
( ( ( sk8 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk8 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6905,260]) ).
thf(7414,plain,
! [A: $i] :
( ( ( sk8 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7413]) ).
thf(7415,plain,
( ( nil @ ( sk8 @ sk16 @ segmentP ) )
| ( sk8 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7414:[bind(A,$thf( sk8 @ sk16 ))]]) ).
thf(24,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderedP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax65) ).
thf(208,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(16229,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,193]) ).
thf(16230,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem ) ),
inference(simp,[status(thm)],[16229]) ).
thf(16231,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk19 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[16230:[bind(A,$thf( sk1 ))]]) ).
thf(26,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax95) ).
thf(213,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ gt ) )
& ( B @ ( A @ gt ) ) )
=> ( C @ ( A @ gt ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(36,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ frontsegP ) )
<=> ? [C: $i] :
( ( ( C @ ( B @ app ) )
= A )
& ( C @ ssList ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
thf(251,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ? [C: $i] :
( ( ( C @ ( B @ app ) )
= A )
& ( C @ ssList ) )
=> ( B @ ( A @ frontsegP ) ) )
& ( ( B @ ( A @ frontsegP ) )
=> ? [C: $i] :
( ( ( C @ ( B @ app ) )
= A )
& ( C @ ssList ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(767,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[120,126]) ).
thf(768,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ sk9 ),
inference(simp,[status(thm)],[767]) ).
thf(769,plain,
( ~ ( sk10 @ ( sk10 @ lt ) )
| ~ ( sk10 @ ( sk12 @ memberP ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[768:[bind(A,$thf( sk10 ))]]) ).
thf(6843,plain,
( ( ( sk45 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,2295]) ).
thf(6844,plain,
( ( ( sk45 @ ssList )
!= ( sk7 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6843]) ).
thf(6847,plain,
( ( sk45 != sk7 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6844]) ).
thf(16364,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,193]) ).
thf(16365,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem ) ),
inference(simp,[status(thm)],[16364]) ).
thf(16366,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk19 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[16365:[bind(A,$thf( sk2 ))]]) ).
thf(111,plain,
( ~ sk9
| ( ( sk12 @ ( sk3 @ ( sk11 @ app ) @ app ) )
= sk4 ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(128,plain,
( ~ sk9
| ( ( sk12 @ ( sk3 @ ( sk11 @ app ) @ app ) )
= sk4 ) ),
inference(lifteq,[status(thm)],[111]) ).
thf(848,plain,
( ~ sk9
| ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 ) ),
inference(rewrite,[status(thm)],[128,121,125]) ).
thf(91,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax49) ).
thf(520,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(7021,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,174]) ).
thf(7022,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ sk9 ),
inference(simp,[status(thm)],[7021]) ).
thf(7023,plain,
( ( sk11 @ cyclefreeP )
| ( sk11 @ sk14 @ ssItem )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[7022:[bind(A,$thf( sk11 ))]]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ lt ) )
& ( B @ ( A @ lt ) ) )
=> ( C @ ( A @ lt ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax34) ).
thf(130,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ lt ) )
& ( B @ ( A @ lt ) ) )
=> ( C @ ( A @ lt ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(457,plain,
! [A: $i] :
( ( ( A @ ( nil @ rearsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[456]) ).
thf(459,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[457]) ).
thf(461,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[459]) ).
thf(462,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[461]) ).
thf(882,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[462,360]) ).
thf(883,plain,
nil @ ( nil @ rearsegP ),
inference(simp,[status(thm)],[882]) ).
thf(9139,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,177]) ).
thf(9140,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk13 @ ssItem ) ),
inference(simp,[status(thm)],[9139]) ).
thf(9141,plain,
( ( sk8 @ cyclefreeP )
| ( sk8 @ sk13 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[9140:[bind(A,$thf( sk8 ))]]) ).
thf(9369,plain,
! [A: $i] :
( ( ( sk8 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk8 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[9141,248]) ).
thf(9370,plain,
! [A: $i] :
( ( ( sk8 @ sk13 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk8 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9369]) ).
thf(9371,plain,
( ~ ( sk8 @ sk13 @ ( nil @ memberP ) )
| ( sk8 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9370:[bind(A,$thf( sk8 @ sk13 ))]]) ).
thf(561,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[110,114]) ).
thf(562,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( A @ ( sk10 @ lt ) )
| ~ ( A @ ( sk11 @ memberP ) ) ),
inference(simp,[status(thm)],[561]) ).
thf(563,plain,
( ~ sk9
| ~ ( sk5 @ ( sk10 @ lt ) )
| ~ ( sk5 @ ( sk11 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[562:[bind(A,$thf( sk5 ))]]) ).
thf(39,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ totalorderP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ leq ) )
| ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
thf(267,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ leq ) )
| ( C @ ( B @ leq ) ) ) ) ) ) ) ) )
=> ( A @ totalorderP ) )
& ( ( A @ totalorderP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( ( B @ ( C @ leq ) )
| ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(85,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ geq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax89) ).
thf(505,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(166,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ app ) @ app ) )
= ( C @ ( B @ app ) @ ( A @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[165]) ).
thf(167,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( C @ ( B @ ( A @ app ) @ app ) )
= ( C @ ( B @ app ) @ ( A @ app ) ) ) ),
inference(lifteq,[status(thm)],[166]) ).
thf(5573,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,260]) ).
thf(5574,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[5573]) ).
thf(5575,plain,
nil @ ( sk1 @ segmentP ),
inference(pattern_uni,[status(thm)],[5574:[bind(A,$thf( sk1 ))]]) ).
thf(43,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ hd @ ssItem ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
thf(306,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ hd @ ssItem ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(80,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ equalelemsP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( C @ cons ) @ ( B @ cons ) @ ( D @ app ) )
= A )
=> ( B = C ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
thf(473,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( C @ cons ) @ ( B @ cons ) @ ( D @ app ) )
= A )
=> ( B = C ) ) ) ) ) )
=> ( A @ equalelemsP ) )
& ( ( A @ equalelemsP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( C @ cons ) @ ( B @ cons ) @ ( D @ app ) )
= A )
=> ( B = C ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(5585,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,260]) ).
thf(5586,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ sk9 ),
inference(simp,[status(thm)],[5585]) ).
thf(5587,plain,
( ( nil @ ( sk11 @ segmentP ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[5586:[bind(A,$thf( sk11 ))]]) ).
thf(1302,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[110,227]) ).
thf(1303,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[1302]) ).
thf(1304,plain,
~ ( sk5 @ ( sk5 @ neq ) ),
inference(pattern_uni,[status(thm)],[1303:[bind(A,$thf( sk5 ))]]) ).
thf(66,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
thf(426,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[160]) ).
thf(162,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) ) ),
inference(lifteq,[status(thm)],[161]) ).
thf(6804,plain,
( ( ( sk45 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,2295]) ).
thf(6805,plain,
( ( ( sk45 @ ssList )
!= ( sk8 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6804]) ).
thf(6853,plain,
( ( sk45 != sk8 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6805]) ).
thf(752,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,126]) ).
thf(753,plain,
! [A: $i] :
( ( ( sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) ) ),
inference(simp,[status(thm)],[752]) ).
thf(754,plain,
( ~ sk9
| ~ ( sk10 @ ( sk6 @ lt ) )
| ~ ( sk6 @ ( sk12 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[753:[bind(A,$thf( sk6 ))]]) ).
thf(17161,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,194]) ).
thf(17162,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList ) ),
inference(simp,[status(thm)],[17161]) ).
thf(17163,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk22 @ ssList ) ),
inference(pattern_uni,[status(thm)],[17162:[bind(A,$thf( sk2 ))]]) ).
thf(89,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ lt ) )
=> ~ ( A @ ( B @ lt ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax33) ).
thf(516,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ lt ) )
=> ~ ( A @ ( B @ lt ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(145,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ frontsegP ) )
| ~ ( C @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[144]) ).
thf(555,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[110,248]) ).
thf(556,plain,
! [A: $i] :
( ( ( sk5 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[555]) ).
thf(557,plain,
~ ( sk5 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[556:[bind(A,$thf( sk5 ))]]) ).
thf(853,plain,
( ( sk9 != sk9 )
| ~ $true
| ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,848]) ).
thf(854,plain,
( ( sk9 != sk9 )
| ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[853]) ).
thf(855,plain,
( ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[854:[]]) ).
thf(7180,plain,
( ( ( sk45 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,2954]) ).
thf(7181,plain,
( ( ( sk45 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7180]) ).
thf(7211,plain,
( ( sk45 != sk2 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[7181]) ).
thf(6900,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[117,172]) ).
thf(6901,plain,
! [A: $i] :
( ( ( sk11 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk16 @ ssList )
| ~ sk9 ),
inference(simp,[status(thm)],[6900]) ).
thf(6902,plain,
( ( sk11 @ cyclefreeP )
| ( sk11 @ sk16 @ ssList )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[6901:[bind(A,$thf( sk11 ))]]) ).
thf(1250,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[621,133]) ).
thf(1251,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[1250]) ).
thf(1252,plain,
( ( nil @ ( sk10 @ cons ) @ strictorderedP )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[1251:[bind(A,$thf( sk10 ))]]) ).
thf(25260,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,207]) ).
thf(25261,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[25260]) ).
thf(25262,plain,
sk7 @ ( sk7 @ segmentP ),
inference(pattern_uni,[status(thm)],[25261:[bind(A,$thf( sk7 ))]]) ).
thf(93,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ lt ) )
<=> ( ( B @ ( A @ leq ) )
& ( A != B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax93) ).
thf(525,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( ( B @ ( A @ leq ) )
& ( A != B ) )
=> ( B @ ( A @ lt ) ) )
& ( ( B @ ( A @ lt ) )
=> ( ( B @ ( A @ leq ) )
& ( A != B ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(5622,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,260]) ).
thf(5623,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[5622]) ).
thf(5624,plain,
nil @ ( sk7 @ segmentP ),
inference(pattern_uni,[status(thm)],[5623:[bind(A,$thf( sk7 ))]]) ).
thf(14317,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,190]) ).
thf(14318,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk21 @ ssList ) ),
inference(simp,[status(thm)],[14317]) ).
thf(14319,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk21 @ ssList ) ),
inference(pattern_uni,[status(thm)],[14318:[bind(A,$thf( sk2 ))]]) ).
thf(1233,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[407,133]) ).
thf(1234,plain,
! [A: $i] :
( ( ( sk45 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[1233]) ).
thf(1235,plain,
nil @ ( sk45 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( sk45 ))]]) ).
thf(76,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( nil != A )
=> ( ( B @ ( A @ app ) @ hd )
= ( A @ hd ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax85) ).
thf(463,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( nil != A )
=> ( ( B @ ( A @ app ) @ hd )
= ( A @ hd ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(79,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( nil != A )
=> ( ( B @ ( A @ app ) @ tl )
= ( B @ ( A @ tl @ app ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax86) ).
thf(470,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( nil != A )
=> ( ( B @ ( A @ app ) @ tl )
= ( B @ ( A @ tl @ app ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(18,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( A @ ( B @ cons ) @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
thf(182,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( A @ ( B @ cons ) @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(50,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ geq ) )
& ( B @ ( A @ geq ) ) )
=> ( A = B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax87) ).
thf(336,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ geq ) )
& ( B @ ( A @ geq ) ) )
=> ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(579,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[120,248]) ).
thf(580,plain,
! [A: $i] :
( ( ( sk10 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ sk9 ),
inference(simp,[status(thm)],[579]) ).
thf(581,plain,
( ~ ( sk10 @ ( nil @ memberP ) )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[580:[bind(A,$thf( sk10 ))]]) ).
thf(611,plain,
( ( sk9 != sk9 )
| ~ ( sk10 @ ( nil @ memberP ) )
| ~ $true
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,581]) ).
thf(612,plain,
( ( sk9 != sk9 )
| ~ ( sk10 @ ( nil @ memberP ) )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[611]) ).
thf(613,plain,
( ~ ( sk10 @ ( nil @ memberP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[612:[]]) ).
thf(598,plain,
( ( sk9 != sk9 )
| ~ $true
| ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,597]) ).
thf(599,plain,
( ( sk9 != sk9 )
| ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[598]) ).
thf(600,plain,
( ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[599:[]]) ).
thf(16949,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,194]) ).
thf(16950,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk22 @ ssList ) ),
inference(simp,[status(thm)],[16949]) ).
thf(16951,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk22 @ ssList ) ),
inference(pattern_uni,[status(thm)],[16950:[bind(A,$thf( sk1 ))]]) ).
thf(175,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk14 @ ( A @ sk13 @ leq ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(46,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ equalelemsP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax73) ).
thf(314,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ equalelemsP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(73,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax63) ).
thf(446,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(8,axiom,
nil @ totalorderedP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax66) ).
thf(143,plain,
nil @ totalorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(29,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ gt ) )
<=> ( A @ ( B @ lt ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax35) ).
thf(218,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( ( A @ ( B @ lt ) )
=> ( B @ ( A @ gt ) ) )
& ( ( B @ ( A @ gt ) )
=> ( A @ ( B @ lt ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(7055,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,174]) ).
thf(7056,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem ) ),
inference(simp,[status(thm)],[7055]) ).
thf(7057,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk14 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[7056:[bind(A,$thf( sk2 ))]]) ).
thf(8181,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7057,248]) ).
thf(8182,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[8181]) ).
thf(8183,plain,
( ~ ( sk2 @ sk14 @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[8182:[bind(A,$thf( sk2 @ sk14 ))]]) ).
thf(9027,plain,
! [A: $i] :
( ( ( sk7 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk7 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[8459,260]) ).
thf(9028,plain,
! [A: $i] :
( ( ( sk7 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk7 @ cyclefreeP ) ),
inference(simp,[status(thm)],[9027]) ).
thf(9029,plain,
( ( nil @ ( sk7 @ sk15 @ segmentP ) )
| ( sk7 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[9028:[bind(A,$thf( sk7 @ sk15 ))]]) ).
thf(186,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ sk18 @ ( A @ sk19 @ lt ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(6787,plain,
( ( ( sk45 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,2295]) ).
thf(6788,plain,
( ( ( sk45 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6787]) ).
thf(6854,plain,
( ( sk45 != sk1 )
| ( sk46 != nil )
| ~ ( sk45 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[6788]) ).
thf(87,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( A @ ( B @ app ) @ ( C @ cons ) )
= ( A @ ( B @ ( C @ cons ) @ app ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
thf(510,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssItem )
=> ( ( A @ ( B @ app ) @ ( C @ cons ) )
= ( A @ ( B @ ( C @ cons ) @ app ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(761,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,126]) ).
thf(762,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ sk9
| ~ ( sk10 @ ( A @ lt ) )
| ~ ( A @ ( sk12 @ memberP ) ) ),
inference(simp,[status(thm)],[761]) ).
thf(763,plain,
( ~ sk9
| ~ ( sk10 @ ( sk46 @ lt ) )
| ~ ( sk46 @ ( sk12 @ memberP ) ) ),
inference(pattern_uni,[status(thm)],[762:[bind(A,$thf( sk46 ))]]) ).
thf(5588,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,260]) ).
thf(5589,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[5588]) ).
thf(5590,plain,
nil @ ( sk8 @ segmentP ),
inference(pattern_uni,[status(thm)],[5589:[bind(A,$thf( sk8 ))]]) ).
thf(52,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ cons ) @ totalorderedP )
<=> ( ( ( B @ hd @ ( A @ leq ) )
& ( B @ totalorderedP )
& ( nil != B ) )
| ( nil = B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax67) ).
thf(346,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( ( B @ hd @ ( A @ leq ) )
& ( B @ totalorderedP )
& ( nil != B ) )
| ( nil = B ) )
=> ( B @ ( A @ cons ) @ totalorderedP ) )
& ( ( B @ ( A @ cons ) @ totalorderedP )
=> ( ( ( B @ hd @ ( A @ leq ) )
& ( B @ totalorderedP )
& ( nil != B ) )
| ( nil = B ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(95,axiom,
nil @ totalorderP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax62) ).
thf(536,plain,
nil @ totalorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(16391,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,193]) ).
thf(16392,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk19 @ ssItem ) ),
inference(simp,[status(thm)],[16391]) ).
thf(16393,plain,
( ( sk7 @ strictorderP )
| ( sk7 @ sk19 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[16392:[bind(A,$thf( sk7 ))]]) ).
thf(69,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ cyclefreeP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax59) ).
thf(432,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ cyclefreeP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(183,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[182]) ).
thf(7046,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ $true
| ~ sk9 ),
inference(paramod_ordered,[status(thm)],[112,174]) ).
thf(7047,plain,
! [A: $i] :
( ( ( sk12 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk14 @ ssItem )
| ~ sk9 ),
inference(simp,[status(thm)],[7046]) ).
thf(7048,plain,
( ( sk12 @ cyclefreeP )
| ( sk12 @ sk14 @ ssItem )
| ~ sk9 ),
inference(pattern_uni,[status(thm)],[7047:[bind(A,$thf( sk12 ))]]) ).
thf(9810,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,178]) ).
thf(9811,plain,
! [A: $i] :
( ( ( sk7 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk17 @ ssList ) ),
inference(simp,[status(thm)],[9810]) ).
thf(9812,plain,
( ( sk7 @ cyclefreeP )
| ( sk7 @ sk17 @ ssList ) ),
inference(pattern_uni,[status(thm)],[9811:[bind(A,$thf( sk7 ))]]) ).
thf(1346,plain,
( ( ( nil @ ( sk10 @ cons ) )
!= ( nil @ ( sk10 @ cons ) ) )
| ( sk1 @ strictorderedP )
| ( sk1 = nil )
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[600,1249]) ).
thf(1347,plain,
( ( ( nil @ ( sk10 @ cons ) )
!= ( nil @ ( sk10 @ cons ) ) )
| ( sk1 @ strictorderedP )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[1346]) ).
thf(1348,plain,
( ( sk1 @ strictorderedP )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[1347:[]]) ).
thf(601,plain,
( ( sk9 != sk9 )
| ~ ( sk10 @ ( nil @ memberP ) )
| ~ $true
| ( sk1 = nil ) ),
inference(paramod_ordered,[status(thm)],[582,581]) ).
thf(602,plain,
( ( sk9 != sk9 )
| ~ ( sk10 @ ( nil @ memberP ) )
| ( sk1 = nil ) ),
inference(simp,[status(thm)],[601]) ).
thf(603,plain,
( ~ ( sk10 @ ( nil @ memberP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[602:[]]) ).
thf(25,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ lt ) )
| ( A = B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax92) ).
thf(210,plain,
! [A: $i] :
( ( A @ ssItem )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ lt ) )
| ( A = B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(189,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( ( A @ sk22 @ ( A @ sk19 @ cons ) @ ( A @ sk21 @ ( A @ sk18 @ cons ) @ ( A @ sk20 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[185]) ).
thf(195,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ( ( A @ sk22 @ ( A @ sk19 @ cons ) @ ( A @ sk21 @ ( A @ sk18 @ cons ) @ ( A @ sk20 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[189]) ).
thf(7276,plain,
! [A: $i] :
( ( ( sk1 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6882,260]) ).
thf(7277,plain,
! [A: $i] :
( ( ( sk1 @ sk16 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7276]) ).
thf(7278,plain,
( ( nil @ ( sk1 @ sk16 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7277:[bind(A,$thf( sk1 @ sk16 ))]]) ).
thf(12474,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,187]) ).
thf(12475,plain,
! [A: $i] :
( ( ( sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk18 @ ssItem ) ),
inference(simp,[status(thm)],[12474]) ).
thf(12476,plain,
( ( sk8 @ strictorderP )
| ( sk8 @ sk18 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[12475:[bind(A,$thf( sk8 ))]]) ).
thf(8451,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,176]) ).
thf(8452,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[8451]) ).
thf(8453,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[8452:[bind(A,$thf( sk2 ))]]) ).
thf(8820,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[8453,260]) ).
thf(8821,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[8820]) ).
thf(8822,plain,
( ( nil @ ( sk2 @ sk15 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[8821:[bind(A,$thf( sk2 @ sk15 ))]]) ).
thf(622,plain,
( ( sk9 != sk9 )
| ~ $true
| ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,597]) ).
thf(623,plain,
( ( sk9 != sk9 )
| ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[622]) ).
thf(624,plain,
( ( ( nil @ ( sk10 @ cons ) )
= sk1 )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[623:[]]) ).
thf(1963,plain,
( ( ( sk46 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,1772]) ).
thf(1964,plain,
( ( ( sk46 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1963]) ).
thf(1977,plain,
( ( sk46 != sk2 )
| ( sk45 != nil )
| ~ ( sk46 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1964]) ).
thf(573,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[408,248]) ).
thf(574,plain,
! [A: $i] :
( ( ( sk46 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[573]) ).
thf(575,plain,
~ ( sk46 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[574:[bind(A,$thf( sk46 ))]]) ).
thf(131,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) )
| ~ ( C @ ssItem )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[130]) ).
thf(71,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( B @ ( A @ app ) @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
thf(442,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( B @ ( A @ app ) @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(869,plain,
( ( sk9 != sk9 )
| ~ $true
| ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk2 = nil ) ),
inference(paramod_ordered,[status(thm)],[607,848]) ).
thf(870,plain,
( ( sk9 != sk9 )
| ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk2 = nil ) ),
inference(simp,[status(thm)],[869]) ).
thf(871,plain,
( ( ( sk12 @ ( sk1 @ ( sk11 @ app ) @ app ) )
= sk2 )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[870:[]]) ).
thf(7616,plain,
( ( sk2 != sk2 )
| ( sk2 @ cyclefreeP )
| ( nil @ sk16 @ ssList )
| sk9 ),
inference(paramod_ordered,[status(thm)],[607,6965]) ).
thf(7617,plain,
( ( sk2 @ cyclefreeP )
| ( nil @ sk16 @ ssList )
| sk9 ),
inference(pattern_uni,[status(thm)],[7616:[]]) ).
thf(48,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ hd )
= B )
& ( B @ ssItem ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax75) ).
thf(322,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ hd )
= B )
& ( B @ ssItem ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(81,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ tl )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
thf(486,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ tl )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(5616,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,260]) ).
thf(5617,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[5616]) ).
thf(5618,plain,
nil @ ( sk2 @ segmentP ),
inference(pattern_uni,[status(thm)],[5617:[bind(A,$thf( sk2 ))]]) ).
thf(44,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ tl @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
thf(309,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ tl @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(27,axiom,
nil @ duplicatefreeP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax72) ).
thf(215,plain,
nil @ duplicatefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(83,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ totalorderedP )
<=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
thf(491,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ leq ) ) ) ) ) ) ) )
=> ( A @ totalorderedP ) )
& ( ( A @ totalorderedP )
=> ! [B: $i] :
( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssItem )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ! [F: $i] :
( ( F @ ssList )
=> ( ( ( F @ ( C @ cons ) @ ( E @ ( B @ cons ) @ ( D @ app ) @ app ) )
= A )
=> ( C @ ( B @ leq ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(55,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( B @ ( A @ segmentP ) )
<=> ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ ( C @ app ) @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
thf(364,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ ( C @ app ) @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) )
=> ( B @ ( A @ segmentP ) ) )
& ( ( B @ ( A @ segmentP ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( B @ ( C @ app ) @ app ) )
= A )
& ( D @ ssList ) )
& ( C @ ssList ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(32,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( A @ lt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax90) ).
thf(232,plain,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(37761,plain,
$false,
inference(e,[status(thm)],[9208,9458,138,2295,12570,249,518,468,234,1295,101,5593,115,217,7208,408,170,9621,582,17014,9901,120,247,202,597,6971,9184,384,7961,21435,8342,6851,13113,153,7748,1310,533,3365,142,174,2985,7235,20845,14188,5621,2957,12543,8122,389,13280,184,1298,10053,504,110,21354,125,1313,157,9800,6905,14334,606,881,25247,289,448,316,261,1232,7209,421,164,13295,1682,106,121,2291,25086,8109,216,1843,6947,132,133,8691,411,428,507,312,206,8459,3243,1975,8289,292,248,117,546,201,7859,102,7078,25156,21357,2954,7827,260,160,429,165,1238,17178,21477,192,407,13158,197,361,879,522,757,456,229,566,1402,578,5609,8545,156,21498,5615,1970,188,141,610,8117,1772,2990,593,16284,328,1493,124,339,554,1414,193,537,8132,489,1249,1974,129,569,1246,134,1241,360,205,1035,8378,3422,10190,9269,9716,513,148,1301,180,444,149,176,423,772,5612,281,1488,259,21304,12441,391,1786,144,14134,466,7536,159,382,7201,572,2029,181,7006,172,24919,419,434,98,2871,1307,187,7415,208,16231,213,621,251,769,6847,198,16366,848,520,9674,7023,130,883,9371,563,267,505,167,5575,306,473,5587,1304,426,162,112,6853,754,17163,516,194,145,557,855,7211,6902,1252,25262,525,7026,5624,14319,585,1235,463,470,177,182,1404,9109,336,613,600,16951,175,314,446,143,627,6965,203,218,1998,8183,581,6882,9141,9029,186,114,6854,510,207,763,5590,346,536,16393,432,410,168,146,405,190,183,7048,9812,1348,373,603,210,107,126,195,7278,12476,8822,624,1977,575,596,131,178,442,871,607,7617,8453,163,200,227,322,486,5618,309,215,560,491,364,232,100,222,7057]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC173+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.15/15.59 % Computer : n006.cluster.edu
% 0.15/15.59 % Model : x86_64 x86_64
% 0.15/15.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/15.59 % Memory : 8046.5625MB
% 0.15/15.59 % OS : Linux 6.8.0-71-generic
% 0.15/15.59 % CPULimit : 300
% 0.15/15.59 % WCLimit : 300
% 0.15/15.59 % DateTime : Sat Sep 26 12:25:44 UTC 2026
% 0.15/15.59 % CPUTime :
% 0.15/15.59 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
% 1.15/16.39 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.96/16.77 % [INFO] Parsing done (369ms).
% 1.96/16.79 % [INFO] Running in sequential loop mode.
% 3.07/17.34 % [INFO] eprover registered as external prover.
% 3.07/17.35 % [INFO] Scanning for conjecture ...
% 3.46/17.56 % [INFO] Found a conjecture (or negated_conjecture) and 95 axioms. Running axiom selection ...
% 3.88/17.71 % [INFO] Axiom selection finished. Selected 95 axioms (removed 0 axioms).
% 4.13/17.87 % [INFO] Problem is first-order (TPTP FOF).
% 4.39/17.90 % [INFO] Type checking passed.
% 4.39/17.91 % [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 ...
% 98.58/39.64 % External prover 'e' found a proof!
% 98.58/39.64 % [INFO] Killing All external provers ...
% 98.58/39.65 % Time passed: 23851ms (effective reasoning time: 22850ms)
% 98.58/39.65 % 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)>
% 98.58/39.65 % Axioms used in derivation (95): ax74, ax13, ax37, ax14, ax12, ax79, ax20, ax52, ax67, ax24, ax63, ax56, ax4, ax47, ax41, ax90, ax31, ax28, ax9, ax17, ax6, ax45, ax40, ax85, ax35, ax58, ax69, ax78, ax39, ax89, ax27, ax66, ax8, ax91, ax73, ax51, ax48, ax21, ax88, ax62, ax10, ax55, ax32, ax95, ax16, ax80, ax59, ax1, ax7, ax77, ax38, ax44, ax84, ax92, ax94, ax33, ax26, ax61, ax11, ax50, ax87, ax72, ax65, ax22, ax15, ax81, ax76, ax43, ax83, ax19, ax2, ax70, ax54, ax49, ax46, ax34, ax23, ax86, ax25, ax60, ax71, ax57, ax68, ax30, ax42, ax82, ax18, ax3, ax5, ax36, ax64, ax29, ax75, ax53, ax93
% 98.58/39.65 % No. of inferences in proof: 825
% 98.58/39.65 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 23851 ms resp. 22850 ms w/o parsing
% 101.64/40.11 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 101.64/40.13 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------