%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWC015+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 : n005.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:51:48 AM UTC 2026
% Result : Theorem 65.90s 23.94s
% Output : Refutation 68.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 112
% Syntax : Number of formulae : 845 ( 84 unt; 0 typ; 16 def)
% Number of atoms : 3721 ( 786 equ; 0 cnn)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 8526 (1247 ~;1378 |; 223 &;5043 @)
% ( 26 <=>; 609 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 44 ( 41 usr; 10 con; 0-2 aty)
% Number of variables : 1000 ( 10 ^; 912 !; 62 ?;1000 :)
% ( 0 !>; 0 ?*; 0 @-; 16 @+)
% Comments :
%------------------------------------------------------------------------------
thf(ssList_decl,type,
ssList: $i > $o ).
thf(neq_decl,type,
neq: $i > $i > $o ).
thf(nil_decl,type,
nil: $i ).
thf(tl_decl,type,
tl: $i > $i ).
thf(app_decl,type,
app: $i > $i > $i ).
thf(ssItem_decl,type,
ssItem: $i > $o ).
thf(cons_decl,type,
cons: $i > $i > $i ).
thf(strictorderedP_decl,type,
strictorderedP: $i > $o ).
thf(lt_decl,type,
lt: $i > $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(memberP_decl,type,
memberP: $i > $i > $o ).
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: $o ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i ).
thf(sk38_decl,type,
sk38: $i ).
thf(sk39_decl,type,
sk39: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil @ ( D @ neq ) )
| ~ ( nil @ ( B @ neq ) ) )
& ( ? [E: $i] :
( ? [F: $i] :
( ( ( F @ ( nil @ ( E @ cons ) @ app ) )
= B )
& ( ( nil @ ( E @ cons ) )
= A )
& ( F @ ssList ) )
& ( E @ ssItem ) )
| ? [E: $i] :
( ? [F: $i] :
( ( D @ ( nil @ neq ) )
& ( ( F @ ( C @ app ) )
= E )
& ( ( D @ tl )
= F )
& ( F @ ssList ) )
& ( D != E )
& ( E @ ssList ) )
| ~ ( nil @ ( B @ neq ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( ( nil @ ( C @ neq ) )
| ~ ( nil @ ( A @ neq ) ) )
& ( ? [D: $i] :
( ? [E: $i] :
( ( ( E @ ( nil @ ( D @ cons ) @ app ) )
= A )
& ( ( nil @ ( D @ cons ) )
= sk1 )
& ( E @ ssList ) )
& ( D @ ssItem ) )
| ? [D: $i] :
( ? [E: $i] :
( ( C @ ( nil @ neq ) )
& ( ( E @ ( B @ app ) )
= D )
& ( ( C @ tl )
= E )
& ( E @ ssList ) )
& ( C != D )
& ( D @ ssList ) )
| ~ ( nil @ ( A @ neq ) ) ) )
| ( sk1 != B )
| ( A != C ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( ( ( ( nil @ ( B @ neq ) )
| ~ ( nil @ ( sk2 @ neq ) ) )
& ( ? [C: $i] :
( ? [D: $i] :
( ( ( D @ ( nil @ ( C @ cons ) @ app ) )
= sk2 )
& ( ( nil @ ( C @ cons ) )
= sk1 )
& ( D @ ssList ) )
& ( C @ ssItem ) )
| ? [C: $i] :
( ? [D: $i] :
( ( B @ ( nil @ neq ) )
& ( ( D @ ( A @ app ) )
= C )
& ( ( B @ tl )
= D )
& ( D @ ssList ) )
& ( B != C )
& ( C @ ssList ) )
| ~ ( nil @ ( sk2 @ neq ) ) ) )
| ( sk1 != A )
| ( sk2 != B ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ( A @ ssList )
=> ( ( ( ( nil @ ( A @ neq ) )
| ~ ( nil @ ( sk2 @ neq ) ) )
& ( ? [B: $i] :
( ? [C: $i] :
( ( ( C @ ( nil @ ( B @ cons ) @ app ) )
= sk2 )
& ( ( nil @ ( B @ cons ) )
= sk1 )
& ( C @ ssList ) )
& ( B @ ssItem ) )
| ? [B: $i] :
( ? [C: $i] :
( ( A @ ( nil @ neq ) )
& ( ( C @ ( sk3 @ app ) )
= B )
& ( ( A @ tl )
= C )
& ( C @ ssList ) )
& ( A != B )
& ( B @ ssList ) )
| ~ ( nil @ ( sk2 @ neq ) ) ) )
| ( sk1 != sk3 )
| ( sk2 != A ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [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(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( B @ cons ) @ ( D @ ( A @ sk6 @ cons ) @ ( C @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk6 @ ( B @ leq ) )
& ( B @ ( A @ sk6 @ leq ) ) ) ) ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( D @ ( A @ sk7 @ cons ) @ ( C @ ( A @ sk6 @ cons ) @ ( B @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk6 @ ( A @ sk7 @ leq ) )
& ( A @ sk7 @ ( A @ sk6 @ leq ) ) ) ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( A @ sk7 @ cons ) @ ( B @ ( A @ sk6 @ cons ) @ ( A @ sk8 @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk6 @ ( A @ sk7 @ leq ) )
& ( A @ sk7 @ ( A @ sk6 @ leq ) ) ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ( ( ( B @ ( A @ sk7 @ cons ) @ ( A @ sk9 @ ( A @ sk6 @ cons ) @ ( A @ sk8 @ app ) @ app ) )
= A )
=> ~ ( ( A @ sk6 @ ( A @ sk7 @ leq ) )
& ( A @ sk7 @ ( A @ sk6 @ leq ) ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [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(sk12_def,definition,
( sk12
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssItem )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ! [E: $i] :
( ( E @ ssList )
=> ( ( ( E @ ( B @ cons ) @ ( D @ ( A @ sk11 @ cons ) @ ( C @ app ) @ app ) )
= A )
=> ( ( A @ sk11 @ ( B @ lt ) )
| ( B @ ( A @ sk11 @ lt ) ) ) ) ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( D @ ( A @ sk12 @ cons ) @ ( C @ ( A @ sk11 @ cons ) @ ( B @ app ) @ app ) )
= A )
=> ( ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ( A @ sk12 @ ( A @ sk11 @ lt ) ) ) ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ( ( ( C @ ( A @ sk12 @ cons ) @ ( B @ ( A @ sk11 @ cons ) @ ( A @ sk13 @ app ) @ app ) )
= A )
=> ( ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ( A @ sk12 @ ( A @ sk11 @ lt ) ) ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( B @ ssList )
=> ( ( ( B @ ( A @ sk12 @ cons ) @ ( A @ sk14 @ ( A @ sk11 @ cons ) @ ( A @ sk13 @ app ) @ app ) )
= A )
=> ( ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ( A @ sk12 @ ( A @ sk11 @ lt ) ) ) ) ) ) ) ).
thf(sk38_def,definition,
( sk38
= ( @+[A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: $i] :
( ( sk38 != A )
& ( A @ ssItem ) ) ) ) ).
thf(1,conjecture,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ! [C: $i] :
( ( C @ ssList )
=> ! [D: $i] :
( ( D @ ssList )
=> ( ( ( ( nil @ ( D @ neq ) )
| ~ ( nil @ ( B @ neq ) ) )
& ( ? [E: $i] :
( ? [F: $i] :
( ( ( F @ ( nil @ ( E @ cons ) @ app ) )
= B )
& ( ( nil @ ( E @ cons ) )
= A )
& ( F @ ssList ) )
& ( E @ ssItem ) )
| ? [E: $i] :
( ? [F: $i] :
( ( D @ ( nil @ neq ) )
& ( ( F @ ( C @ app ) )
= E )
& ( ( D @ tl )
= F )
& ( F @ ssList ) )
& ( D != E )
& ( E @ ssList ) )
| ~ ( nil @ ( B @ neq ) ) ) )
| ( 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 @ ( D @ neq ) )
| ~ ( nil @ ( B @ neq ) ) )
& ( ? [E: $i] :
( ? [F: $i] :
( ( ( F @ ( nil @ ( E @ cons ) @ app ) )
= B )
& ( ( nil @ ( E @ cons ) )
= A )
& ( F @ ssList ) )
& ( E @ ssItem ) )
| ? [E: $i] :
( ? [F: $i] :
( ( D @ ( nil @ neq ) )
& ( ( F @ ( C @ app ) )
= E )
& ( ( D @ tl )
= F )
& ( F @ ssList ) )
& ( D != E )
& ( E @ ssList ) )
| ~ ( nil @ ( B @ neq ) ) ) )
| ( 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 @ ( D @ neq ) )
| ~ ( nil @ ( B @ neq ) ) )
& ( ? [E: $i] :
( ? [F: $i] :
( ( ( F @ ( nil @ ( E @ cons ) @ app ) )
= B )
& ( ( nil @ ( E @ cons ) )
= A )
& ( F @ ssList ) )
& ( E @ ssItem ) )
| ? [E: $i] :
( ? [F: $i] :
( ( D @ ( nil @ neq ) )
& ( ( F @ ( C @ app ) )
= E )
& ( ( D @ tl )
= F )
& ( F @ ssList ) )
& ( D != E )
& ( E @ ssList ) )
| ~ ( nil @ ( B @ neq ) ) ) )
| ( A != C )
| ( B != D ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(99,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( nil @ ( sk4 @ neq ) )
| sk5 )
& ( ( nil @ ( sk2 @ neq ) )
| sk5 )
& ( ~ sk5
| ( ( D @ ( nil @ ( C @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( C @ cons ) )
!= sk1 )
| ~ ( D @ ssList )
| ~ ( C @ ssItem ) )
& ( ~ sk5
| ~ ( sk4 @ ( nil @ neq ) )
| ( ( B @ ( sk3 @ app ) )
!= A )
| ( ( sk4 @ tl )
!= B )
| ~ ( B @ ssList )
| ( sk4 = A )
| ~ ( A @ ssList ) )
& ( ~ sk5
| ( nil @ ( sk2 @ neq ) ) )
& ( sk1 = sk3 )
& ( sk2 = sk4 )
& ( sk4 @ ssList )
& ( sk3 @ ssList )
& ( sk2 @ ssList )
& ( sk1 @ ssList ) ),
inference(cnf,[status(esa)],[98]) ).
thf(104,plain,
sk2 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(37,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax57) ).
thf(247,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(248,plain,
! [A: $i] :
( ( nil @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[247]) ).
thf(1584,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,248]) ).
thf(1585,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[1584]) ).
thf(1586,plain,
nil @ ( sk2 @ segmentP ),
inference(pattern_uni,[status(thm)],[1585:[bind(A,$thf( sk2 ))]]) ).
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(156,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(157,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( ( A @ sk10 @ ( A @ sk7 @ cons ) @ ( A @ sk9 @ ( A @ sk6 @ cons ) @ ( A @ sk8 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk10 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk9 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem )
| ~ ( A @ ssList ) )
& ( ( A @ cyclefreeP )
| ( A @ sk6 @ 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)],[156]) ).
thf(160,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk6 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(5749,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,160]) ).
thf(5750,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ssItem ) ),
inference(simp,[status(thm)],[5749]) ).
thf(5751,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk6 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[5750:[bind(A,$thf( sk2 ))]]) ).
thf(46,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ equalelemsP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax73) ).
thf(302,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ equalelemsP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(303,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ equalelemsP )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[302]) ).
thf(5916,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,303]) ).
thf(5917,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5916]) ).
thf(5918,plain,
( ( nil @ ( sk2 @ sk6 @ cons ) @ equalelemsP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5917:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(105,plain,
sk1 @ ssList,
inference(cnfConj,[status(thm)],[99]) ).
thf(45,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax51) ).
thf(300,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(301,plain,
! [A: $i] :
( ( nil @ ( A @ rearsegP ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[300]) ).
thf(1765,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,301]) ).
thf(1766,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) ) ),
inference(simp,[status(thm)],[1765]) ).
thf(1767,plain,
nil @ ( sk1 @ rearsegP ),
inference(pattern_uni,[status(thm)],[1766:[bind(A,$thf( sk1 ))]]) ).
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(479,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(162,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk9 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(6429,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk9 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,162]) ).
thf(6430,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk9 @ ssList ) ),
inference(simp,[status(thm)],[6429]) ).
thf(6431,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk9 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6430:[bind(A,$thf( sk1 ))]]) ).
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(352,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(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(172,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(173,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ~ ( A @ sk12 @ ( A @ sk11 @ lt ) )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( ( A @ sk15 @ ( A @ sk12 @ cons ) @ ( A @ sk14 @ ( A @ sk11 @ cons ) @ ( A @ sk13 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk15 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk14 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk13 @ ssList )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk12 @ ssItem )
| ~ ( A @ ssList ) )
& ( ( A @ strictorderP )
| ( A @ sk11 @ 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)],[172]) ).
thf(175,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk15 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(10373,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,175]) ).
thf(10374,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[10373]) ).
thf(10375,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[10374:[bind(A,$thf( sk2 ))]]) ).
thf(59,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax45) ).
thf(377,plain,
! [A: $i] :
( ( A @ ssList )
=> ( nil @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(378,plain,
! [A: $i] :
( ( nil @ ( A @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[377]) ).
thf(10728,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10375,378]) ).
thf(10729,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[10728]) ).
thf(10730,plain,
( ( nil @ ( sk2 @ sk15 @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10729:[bind(A,$thf( sk2 @ sk15 ))]]) ).
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(249,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ tl )
= B )
& ( B @ ssList ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(18,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( A @ ( B @ cons ) @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
thf(170,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( A @ ( B @ cons ) @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(158,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(648,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,158]) ).
thf(649,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList ) ),
inference(simp,[status(thm)],[648]) ).
thf(650,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk8 @ ssList ) ),
inference(pattern_uni,[status(thm)],[649:[bind(A,$thf( sk2 ))]]) ).
thf(3988,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[650,378]) ).
thf(3989,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[3988]) ).
thf(3990,plain,
( ( nil @ ( sk2 @ sk8 @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[3989:[bind(A,$thf( sk2 @ sk8 ))]]) ).
thf(61,axiom,
? [A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
thf(393,plain,
? [A: $i] :
( ? [B: $i] :
( ( A != B )
& ( B @ ssItem ) )
& ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(394,plain,
( ( sk38 != sk39 )
& ( sk39 @ ssItem )
& ( sk38 @ ssItem ) ),
inference(cnf,[status(esa)],[393]) ).
thf(395,plain,
sk38 @ ssItem,
inference(cnfConj,[status(thm)],[394]) ).
thf(5,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderedP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax68) ).
thf(120,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(121,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[120]) ).
thf(760,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,121]) ).
thf(761,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[760]) ).
thf(762,plain,
nil @ ( sk38 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[761:[bind(A,$thf( sk38 ))]]) ).
thf(20,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil @ ( A @ app ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax84) ).
thf(186,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil @ ( A @ app ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(187,plain,
! [A: $i] :
( ( ( nil @ ( A @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[186]) ).
thf(188,plain,
! [A: $i] :
( ~ ( A @ ssList )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[187]) ).
thf(16084,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[104,188]) ).
thf(16085,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[16084]) ).
thf(16086,plain,
( ( nil @ ( sk2 @ app ) )
= sk2 ),
inference(pattern_uni,[status(thm)],[16085:[bind(A,$thf( sk2 ))]]) ).
thf(31,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ app ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
thf(217,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ app ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(5725,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,160]) ).
thf(5726,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ssItem ) ),
inference(simp,[status(thm)],[5725]) ).
thf(5727,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk6 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[5726:[bind(A,$thf( sk1 ))]]) ).
thf(5840,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,303]) ).
thf(5841,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5840]) ).
thf(5842,plain,
( ( nil @ ( sk1 @ sk6 @ cons ) @ equalelemsP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5841:[bind(A,$thf( sk1 @ sk6 ))]]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ segmentP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax58) ).
thf(137,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(138,plain,
! [A: $i] :
( ( ( A @ ( nil @ segmentP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[137]) ).
thf(139,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[138]) ).
thf(141,plain,
! [A: $i] :
( ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil = A ) ),
inference(lifteq,[status(thm)],[139]) ).
thf(2012,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[105,141]) ).
thf(2013,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[2012]) ).
thf(2014,plain,
( ~ ( sk1 @ ( nil @ segmentP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[2013:[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(379,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(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(269,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(159,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(5225,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,159]) ).
thf(5226,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem ) ),
inference(simp,[status(thm)],[5225]) ).
thf(5227,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk7 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[5226:[bind(A,$thf( sk2 ))]]) ).
thf(5587,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,121]) ).
thf(5588,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5587]) ).
thf(5589,plain,
( ( nil @ ( sk2 @ sk7 @ cons ) @ strictorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5588:[bind(A,$thf( sk2 @ sk7 ))]]) ).
thf(177,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(11012,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,177]) ).
thf(11013,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) ) ),
inference(simp,[status(thm)],[11012]) ).
thf(11014,plain,
( ( sk1 @ strictorderP )
| ~ ( sk1 @ sk11 @ ( sk1 @ sk12 @ lt ) ) ),
inference(pattern_uni,[status(thm)],[11013:[bind(A,$thf( sk1 ))]]) ).
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(327,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(328,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ neq ) )
| ( A = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) )
& ( ( A != B )
| ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[327]) ).
thf(329,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[328]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( A != B ) ),
inference(lifteq,[status(thm)],[329]) ).
thf(332,plain,
! [A: $i] :
( ~ ( A @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[331]) ).
thf(795,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,332]) ).
thf(796,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[795]) ).
thf(797,plain,
~ ( sk2 @ ( sk2 @ neq ) ),
inference(pattern_uni,[status(thm)],[796:[bind(A,$thf( sk2 ))]]) ).
thf(103,plain,
( ~ sk5
| ( nil @ ( sk2 @ neq ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(109,plain,
( ( nil @ ( sk2 @ neq ) )
| sk5 ),
inference(cnfConj,[status(thm)],[99]) ).
thf(102,plain,
( ~ ( nil @ ( sk4 @ neq ) )
| sk5 ),
inference(cnfConj,[status(thm)],[99]) ).
thf(107,plain,
sk2 = sk4,
inference(cnfConj,[status(thm)],[99]) ).
thf(112,plain,
sk4 = sk2,
inference(lifteq,[status(thm)],[107]) ).
thf(540,plain,
( ~ ( nil @ ( sk2 @ neq ) )
| sk5 ),
inference(rewrite,[status(thm)],[102,112]) ).
thf(548,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true
| sk5
| sk5 ),
inference(paramod_ordered,[status(thm)],[109,540]) ).
thf(549,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| sk5 ),
inference(simp,[status(thm)],[548]) ).
thf(550,plain,
sk5,
inference(pattern_uni,[status(thm)],[549:[]]) ).
thf(555,plain,
( ~ $true
| ( nil @ ( sk2 @ neq ) ) ),
inference(rewrite,[status(thm)],[103,550]) ).
thf(556,plain,
nil @ ( sk2 @ neq ),
inference(simp,[status(thm)],[555]) ).
thf(787,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,332]) ).
thf(788,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[787]) ).
thf(789,plain,
~ ( sk1 @ ( sk1 @ neq ) ),
inference(pattern_uni,[status(thm)],[788:[bind(A,$thf( sk1 ))]]) ).
thf(826,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( sk1 @ ( sk1 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,789]) ).
thf(827,plain,
( ( nil @ ( sk2 @ neq ) )
!= ( sk1 @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[826]) ).
thf(828,plain,
( ( sk1 != nil )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[827]) ).
thf(2446,plain,
( ( sk1 != sk1 )
| ( nil != nil )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(paramod_ordered,[status(thm)],[2014,828]) ).
thf(2447,plain,
( ( sk1 != sk1 )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[2446]) ).
thf(2448,plain,
( ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(pattern_uni,[status(thm)],[2447:[]]) ).
thf(53,axiom,
nil @ ssList,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
thf(348,plain,
nil @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ frontsegP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax46) ).
thf(122,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(123,plain,
! [A: $i] :
( ( ( A @ ( nil @ frontsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[122]) ).
thf(125,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[123]) ).
thf(127,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[125]) ).
thf(128,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[127]) ).
thf(697,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[128,348]) ).
thf(698,plain,
nil @ ( nil @ frontsegP ),
inference(simp,[status(thm)],[697]) ).
thf(124,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[123]) ).
thf(126,plain,
! [A: $i] :
( ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil = A ) ),
inference(lifteq,[status(thm)],[124]) ).
thf(397,plain,
sk38 != sk39,
inference(cnfConj,[status(thm)],[394]) ).
thf(398,plain,
sk39 != sk38,
inference(lifteq,[status(thm)],[397]) ).
thf(963,plain,
! [A: $i] :
( ( A != sk39 )
| ( sk38 != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[126,398]) ).
thf(964,plain,
( ( sk38 != nil )
| ~ ( sk39 @ ( nil @ frontsegP ) )
| ~ ( sk39 @ ssList ) ),
inference(pattern_uni,[status(thm)],[963:[bind(A,$thf( sk39 ))]]) ).
thf(4934,plain,
( ( ( sk39 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ( sk38 != nil )
| ~ $true
| ~ ( sk39 @ ssList ) ),
inference(paramod_ordered,[status(thm)],[698,964]) ).
thf(4935,plain,
( ( ( sk39 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ( sk38 != nil )
| ~ ( sk39 @ ssList ) ),
inference(simp,[status(thm)],[4934]) ).
thf(5008,plain,
( ( sk39 != nil )
| ( nil != nil )
| ( sk38 != nil )
| ~ ( sk39 @ ssList ) ),
inference(simp,[status(thm)],[4935]) ).
thf(5026,plain,
( ( sk39 != nil )
| ( sk38 != nil )
| ~ ( sk39 @ ssList ) ),
inference(simp,[status(thm)],[5008]) ).
thf(5041,plain,
( ( ( sk39 @ ssList )
!= ( nil @ ssList ) )
| ( sk39 != nil )
| ( sk38 != nil )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[348,5026]) ).
thf(5042,plain,
( ( ( sk39 @ ssList )
!= ( nil @ ssList ) )
| ( sk39 != nil )
| ( sk38 != nil ) ),
inference(simp,[status(thm)],[5041]) ).
thf(5088,plain,
( ( sk39 != nil )
| ( sk39 != nil )
| ( sk38 != nil ) ),
inference(simp,[status(thm)],[5042]) ).
thf(5098,plain,
( ( sk39 != nil )
| ( sk38 != nil ) ),
inference(simp,[status(thm)],[5088]) ).
thf(5314,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk39 != nil )
| ( nil != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[141,5098]) ).
thf(5315,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk39 != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[5314]) ).
thf(5316,plain,
( ( sk39 != nil )
| ~ ( sk38 @ ( nil @ segmentP ) )
| ~ ( sk38 @ ssList ) ),
inference(pattern_uni,[status(thm)],[5315:[bind(A,$thf( sk38 ))]]) ).
thf(6465,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk9 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,162]) ).
thf(6466,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk9 @ ssList ) ),
inference(simp,[status(thm)],[6465]) ).
thf(6467,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk9 @ ssList ) ),
inference(pattern_uni,[status(thm)],[6466:[bind(A,$thf( sk2 ))]]) ).
thf(6653,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6467,301]) ).
thf(6654,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6653]) ).
thf(6655,plain,
( ( nil @ ( sk2 @ sk9 @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6654:[bind(A,$thf( sk2 @ sk9 ))]]) ).
thf(734,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[650,158]) ).
thf(735,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[734]) ).
thf(736,plain,
( ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ sk8 @ sk8 @ ssList )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[735:[bind(A,$thf( sk2 @ sk8 ))]]) ).
thf(812,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[736,158]) ).
thf(813,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[812]) ).
thf(814,plain,
( ( sk2 @ sk8 @ sk8 @ cyclefreeP )
| ( sk2 @ sk8 @ sk8 @ sk8 @ ssList )
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[813:[bind(A,$thf( sk2 @ sk8 @ sk8 ))]]) ).
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(153,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(641,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,158]) ).
thf(642,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList ) ),
inference(simp,[status(thm)],[641]) ).
thf(643,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk8 @ ssList ) ),
inference(pattern_uni,[status(thm)],[642:[bind(A,$thf( sk1 ))]]) ).
thf(4009,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[643,378]) ).
thf(4010,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[4009]) ).
thf(4011,plain,
( ( nil @ ( sk1 @ sk8 @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[4010:[bind(A,$thf( sk1 @ sk8 ))]]) ).
thf(164,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk10 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(7035,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk10 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,164]) ).
thf(7036,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk10 @ ssList ) ),
inference(simp,[status(thm)],[7035]) ).
thf(7037,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk10 @ ssList ) ),
inference(pattern_uni,[status(thm)],[7036:[bind(A,$thf( sk1 ))]]) ).
thf(7145,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7037,301]) ).
thf(7146,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7145]) ).
thf(7147,plain,
( ( nil @ ( sk1 @ sk10 @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7146:[bind(A,$thf( sk1 @ sk10 ))]]) ).
thf(178,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk12 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(11342,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk12 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,178]) ).
thf(11343,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk12 @ ssItem ) ),
inference(simp,[status(thm)],[11342]) ).
thf(11344,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk12 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[11343:[bind(A,$thf( sk1 ))]]) ).
thf(24,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderedP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax65) ).
thf(196,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(197,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[196]) ).
thf(11447,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,197]) ).
thf(11448,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11447]) ).
thf(11449,plain,
( ( nil @ ( sk1 @ sk12 @ cons ) @ totalorderedP )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11448:[bind(A,$thf( sk1 @ sk12 ))]]) ).
thf(176,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( ( A @ sk15 @ ( A @ sk12 @ cons ) @ ( A @ sk14 @ ( A @ sk11 @ cons ) @ ( A @ sk13 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(185,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ( ( A @ sk15 @ ( A @ sk12 @ cons ) @ ( A @ sk14 @ ( A @ sk11 @ cons ) @ ( A @ sk13 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[176]) ).
thf(396,plain,
sk39 @ ssItem,
inference(cnfConj,[status(thm)],[394]) ).
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(210,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(211,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)],[210]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(cnfConj,[status(thm)],[211]) ).
thf(214,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ( A != B ) ),
inference(lifteq,[status(thm)],[212]) ).
thf(215,plain,
! [A: $i] :
( ~ ( A @ ( A @ neq ) )
| ~ ( A @ ssItem ) ),
inference(simp,[status(thm)],[214]) ).
thf(592,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,215]) ).
thf(593,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[592]) ).
thf(594,plain,
~ ( sk39 @ ( sk39 @ neq ) ),
inference(pattern_uni,[status(thm)],[593:[bind(A,$thf( sk39 ))]]) ).
thf(629,plain,
( ( ( sk39 @ ( sk39 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,594]) ).
thf(630,plain,
( ( sk39 @ ( sk39 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[629]) ).
thf(631,plain,
( ( sk39 != nil )
| ( sk39 != sk2 ) ),
inference(simp,[status(thm)],[630]) ).
thf(1001,plain,
! [A: $i] :
( ( A != sk39 )
| ( nil != nil )
| ( sk39 != sk2 )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[126,631]) ).
thf(1002,plain,
! [A: $i] :
( ( A != sk39 )
| ( sk39 != sk2 )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[1001]) ).
thf(1003,plain,
( ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ frontsegP ) )
| ~ ( sk39 @ ssList ) ),
inference(pattern_uni,[status(thm)],[1002:[bind(A,$thf( sk39 ))]]) ).
thf(5468,plain,
( ( ( sk39 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,1003]) ).
thf(5469,plain,
( ( ( sk39 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[5468]) ).
thf(5495,plain,
( ( sk39 != sk2 )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[5469]) ).
thf(5518,plain,
( ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[5495]) ).
thf(32,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( A @ lt ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax90) ).
thf(220,plain,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(221,plain,
! [A: $i] :
( ~ ( A @ ( A @ lt ) )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[220]) ).
thf(707,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,221]) ).
thf(708,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[707]) ).
thf(709,plain,
~ ( sk39 @ ( sk39 @ lt ) ),
inference(pattern_uni,[status(thm)],[708:[bind(A,$thf( sk39 ))]]) ).
thf(5901,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,221]) ).
thf(5902,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5901]) ).
thf(5903,plain,
( ~ ( sk2 @ sk6 @ ( sk2 @ sk6 @ lt ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5902:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(6752,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6467,332]) ).
thf(6753,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6752]) ).
thf(6754,plain,
( ~ ( sk2 @ sk9 @ ( sk2 @ sk9 @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6753:[bind(A,$thf( sk2 @ sk9 ))]]) ).
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(436,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(7074,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk10 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,164]) ).
thf(7075,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk10 @ ssList ) ),
inference(simp,[status(thm)],[7074]) ).
thf(7076,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk10 @ ssList ) ),
inference(pattern_uni,[status(thm)],[7075:[bind(A,$thf( sk2 ))]]) ).
thf(7309,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7076,248]) ).
thf(7310,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7309]) ).
thf(7311,plain,
( ( nil @ ( sk2 @ sk10 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7310:[bind(A,$thf( sk2 @ sk10 ))]]) ).
thf(68,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( ( A @ tl @ ( A @ hd @ cons ) )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax78) ).
thf(417,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( ( A @ tl @ ( A @ hd @ cons ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(180,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk13 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(12678,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk13 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,180]) ).
thf(12679,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk13 @ ssList ) ),
inference(simp,[status(thm)],[12678]) ).
thf(12680,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk13 @ ssList ) ),
inference(pattern_uni,[status(thm)],[12679:[bind(A,$thf( sk2 ))]]) ).
thf(12990,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12680,248]) ).
thf(12991,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[12990]) ).
thf(12992,plain,
( ( nil @ ( sk2 @ sk13 @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12991:[bind(A,$thf( sk2 @ sk13 ))]]) ).
thf(722,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[643,158]) ).
thf(723,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[722]) ).
thf(724,plain,
( ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ sk8 @ sk8 @ ssList )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[723:[bind(A,$thf( sk1 @ sk8 ))]]) ).
thf(174,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)],[173]) ).
thf(183,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)],[174]) ).
thf(184,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)],[183]) ).
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(372,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(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(504,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(179,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk14 @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(11890,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk14 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,179]) ).
thf(11891,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk14 @ ssList ) ),
inference(simp,[status(thm)],[11890]) ).
thf(11892,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk14 @ ssList ) ),
inference(pattern_uni,[status(thm)],[11891:[bind(A,$thf( sk2 ))]]) ).
thf(12152,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11892,301]) ).
thf(12153,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[12152]) ).
thf(12154,plain,
( ( nil @ ( sk2 @ sk14 @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12153:[bind(A,$thf( sk2 @ sk14 ))]]) ).
thf(75,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( A @ ( nil @ rearsegP ) )
<=> ( nil = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax52) ).
thf(444,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(445,plain,
! [A: $i] :
( ( ( A @ ( nil @ rearsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) )
& ( ( nil = A )
| ~ ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList ) ) ),
inference(cnf,[status(esa)],[444]) ).
thf(447,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[445]) ).
thf(449,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[447]) ).
thf(450,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[449]) ).
thf(701,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[450,348]) ).
thf(702,plain,
nil @ ( nil @ rearsegP ),
inference(simp,[status(thm)],[701]) ).
thf(1575,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,248]) ).
thf(1576,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) ) ),
inference(simp,[status(thm)],[1575]) ).
thf(1577,plain,
nil @ ( sk1 @ segmentP ),
inference(pattern_uni,[status(thm)],[1576:[bind(A,$thf( sk1 ))]]) ).
thf(57,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax61) ).
thf(370,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ totalorderP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(371,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderP )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[370]) ).
thf(5834,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,371]) ).
thf(5835,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5834]) ).
thf(5836,plain,
( ( nil @ ( sk1 @ sk6 @ cons ) @ totalorderP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5835:[bind(A,$thf( sk1 @ sk6 ))]]) ).
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(189,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(5602,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,221]) ).
thf(5603,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5602]) ).
thf(5604,plain,
( ~ ( sk2 @ sk7 @ ( sk2 @ sk7 @ lt ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5603:[bind(A,$thf( sk2 @ sk7 ))]]) ).
thf(67,axiom,
nil @ strictorderP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax64) ).
thf(416,plain,
nil @ strictorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(1771,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[643,301]) ).
thf(1772,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1771]) ).
thf(1773,plain,
( ( nil @ ( sk1 @ sk8 @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1772:[bind(A,$thf( sk1 @ 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(316,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(2118,plain,
! [A: $i] :
( ( A != sk39 )
| ( nil != nil )
| ( sk39 != sk2 )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[141,631]) ).
thf(2119,plain,
! [A: $i] :
( ( A != sk39 )
| ( sk39 != sk2 )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[2118]) ).
thf(2120,plain,
( ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ segmentP ) )
| ~ ( sk39 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2119:[bind(A,$thf( sk39 ))]]) ).
thf(10064,plain,
( ( ( sk39 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,2120]) ).
thf(10065,plain,
( ( ( sk39 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[10064]) ).
thf(10114,plain,
( ( sk39 != sk2 )
| ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[10065]) ).
thf(10117,plain,
( ( sk39 != sk2 )
| ~ ( sk39 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[10114]) ).
thf(2387,plain,
( ( sk1 != sk1 )
| ~ ( nil @ ( sk1 @ neq ) )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(paramod_ordered,[status(thm)],[2014,789]) ).
thf(2388,plain,
( ~ ( nil @ ( sk1 @ neq ) )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(pattern_uni,[status(thm)],[2387:[]]) ).
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(151,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(152,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)],[151]) ).
thf(1566,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[724,248]) ).
thf(1567,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1566]) ).
thf(1568,plain,
( ( nil @ ( sk1 @ sk8 @ sk8 @ segmentP ) )
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1567:[bind(A,$thf( sk1 @ sk8 @ sk8 ))]]) ).
thf(34,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( nil @ memberP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax38) ).
thf(235,plain,
! [A: $i] :
( ( A @ ssItem )
=> ~ ( A @ ( nil @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(236,plain,
! [A: $i] :
( ~ ( A @ ( nil @ memberP ) )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[235]) ).
thf(589,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,236]) ).
thf(590,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[589]) ).
thf(591,plain,
~ ( sk39 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[590:[bind(A,$thf( sk39 ))]]) ).
thf(5201,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,159]) ).
thf(5202,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ssItem ) ),
inference(simp,[status(thm)],[5201]) ).
thf(5203,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk7 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[5202:[bind(A,$thf( sk1 ))]]) ).
thf(5331,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,197]) ).
thf(5332,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5331]) ).
thf(5333,plain,
( ( nil @ ( sk1 @ sk7 @ cons ) @ totalorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5332:[bind(A,$thf( sk1 @ sk7 ))]]) ).
thf(84,axiom,
nil @ equalelemsP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax74) ).
thf(492,plain,
nil @ equalelemsP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(5886,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,121]) ).
thf(5887,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5886]) ).
thf(5888,plain,
( ( nil @ ( sk2 @ sk6 @ cons ) @ strictorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5887:[bind(A,$thf( sk2 @ sk6 ))]]) ).
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(145,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(146,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[145]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( A = B ) ),
inference(lifteq,[status(thm)],[146]) ).
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(280,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(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(132,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(133,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)],[132]) ).
thf(11488,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,371]) ).
thf(11489,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11488]) ).
thf(11490,plain,
( ( nil @ ( sk1 @ sk12 @ cons ) @ totalorderP )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11489:[bind(A,$thf( sk1 @ sk12 ))]]) ).
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(411,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(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(206,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(12616,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk13 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,180]) ).
thf(12617,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk13 @ ssList ) ),
inference(simp,[status(thm)],[12616]) ).
thf(12618,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk13 @ ssList ) ),
inference(pattern_uni,[status(thm)],[12617:[bind(A,$thf( sk1 ))]]) ).
thf(12822,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12618,248]) ).
thf(12823,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[12822]) ).
thf(12824,plain,
( ( nil @ ( sk1 @ sk13 @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12823:[bind(A,$thf( sk1 @ sk13 ))]]) ).
thf(11831,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk14 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,179]) ).
thf(11832,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk14 @ ssList ) ),
inference(simp,[status(thm)],[11831]) ).
thf(11833,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk14 @ ssList ) ),
inference(pattern_uni,[status(thm)],[11832:[bind(A,$thf( sk1 ))]]) ).
thf(11991,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11833,301]) ).
thf(11992,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11991]) ).
thf(11993,plain,
( ( nil @ ( sk1 @ sk14 @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11992:[bind(A,$thf( sk1 @ sk14 ))]]) ).
thf(10323,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk15 @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,175]) ).
thf(10324,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk15 @ ssList ) ),
inference(simp,[status(thm)],[10323]) ).
thf(10325,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk15 @ ssList ) ),
inference(pattern_uni,[status(thm)],[10324:[bind(A,$thf( sk1 ))]]) ).
thf(10591,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10325,332]) ).
thf(10592,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[10591]) ).
thf(10593,plain,
( ~ ( sk1 @ sk15 @ ( sk1 @ sk15 @ neq ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10592:[bind(A,$thf( sk1 @ sk15 ))]]) ).
thf(5837,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,236]) ).
thf(5838,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5837]) ).
thf(5839,plain,
( ~ ( sk1 @ sk6 @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5838:[bind(A,$thf( sk1 @ sk6 ))]]) ).
thf(7267,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7076,301]) ).
thf(7268,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7267]) ).
thf(7269,plain,
( ( nil @ ( sk2 @ sk10 @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7268:[bind(A,$thf( sk2 @ sk10 ))]]) ).
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(534,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(5873,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,215]) ).
thf(5874,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5873]) ).
thf(5875,plain,
( ~ ( sk1 @ sk6 @ ( sk1 @ sk6 @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5874:[bind(A,$thf( sk1 @ sk6 ))]]) ).
thf(3,axiom,
nil @ strictorderedP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax69) ).
thf(117,plain,
nil @ strictorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
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(201,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(4529,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,197]) ).
thf(4530,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[4529]) ).
thf(4531,plain,
nil @ ( sk39 @ cons ) @ totalorderedP,
inference(pattern_uni,[status(thm)],[4530:[bind(A,$thf( sk39 ))]]) ).
thf(165,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(7640,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,165]) ).
thf(7641,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) ) ),
inference(simp,[status(thm)],[7640]) ).
thf(7642,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk6 @ ( sk1 @ sk7 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[7641:[bind(A,$thf( sk1 ))]]) ).
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(334,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(6633,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6431,332]) ).
thf(6634,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6633]) ).
thf(6635,plain,
( ~ ( sk1 @ sk9 @ ( sk1 @ sk9 @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6634:[bind(A,$thf( sk1 @ sk9 ))]]) ).
thf(1578,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[736,248]) ).
thf(1579,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1578]) ).
thf(1580,plain,
( ( nil @ ( sk2 @ sk8 @ sk8 @ segmentP ) )
| ( sk2 @ sk8 @ cyclefreeP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1579:[bind(A,$thf( sk2 @ sk8 @ sk8 ))]]) ).
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(349,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(44,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ tl @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
thf(297,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ tl @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
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(407,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(6618,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6431,378]) ).
thf(6619,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6618]) ).
thf(6620,plain,
( ( nil @ ( sk1 @ sk9 @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6619:[bind(A,$thf( sk1 @ sk9 ))]]) ).
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(361,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(182,plain,
! [A: $i] :
( ( A @ strictorderP )
| ( A @ sk11 @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(13808,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk11 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,182]) ).
thf(13809,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk11 @ ssItem ) ),
inference(simp,[status(thm)],[13808]) ).
thf(13810,plain,
( ( sk1 @ strictorderP )
| ( sk1 @ sk11 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[13809:[bind(A,$thf( sk1 ))]]) ).
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(461,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(85,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ geq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax89) ).
thf(493,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(78,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax42) ).
thf(456,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
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(324,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(956,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[105,126]) ).
thf(957,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ frontsegP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[956]) ).
thf(958,plain,
( ~ ( sk1 @ ( nil @ frontsegP ) )
| ( sk1 = nil ) ),
inference(pattern_uni,[status(thm)],[957:[bind(A,$thf( sk1 ))]]) ).
thf(1142,plain,
( ( sk1 != sk1 )
| ~ ( sk1 @ ( nil @ neq ) )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(paramod_ordered,[status(thm)],[958,789]) ).
thf(1143,plain,
( ~ ( sk1 @ ( nil @ neq ) )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(pattern_uni,[status(thm)],[1142:[]]) ).
thf(7247,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7037,332]) ).
thf(7248,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7247]) ).
thf(7249,plain,
( ~ ( sk1 @ sk10 @ ( sk1 @ sk10 @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7248:[bind(A,$thf( sk1 @ sk10 ))]]) ).
thf(166,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)],[157]) ).
thf(168,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)],[166]) ).
thf(169,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)],[168]) ).
thf(161,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(6109,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,161]) ).
thf(6110,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) ) ),
inference(simp,[status(thm)],[6109]) ).
thf(6111,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ sk7 @ ( sk1 @ sk6 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[6110:[bind(A,$thf( sk1 ))]]) ).
thf(69,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ cyclefreeP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax59) ).
thf(420,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ cyclefreeP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(5949,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,215]) ).
thf(5950,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5949]) ).
thf(5951,plain,
( ~ ( sk2 @ sk6 @ ( sk2 @ sk6 @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5950:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(7187,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7037,248]) ).
thf(7188,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7187]) ).
thf(7189,plain,
( ( nil @ ( sk1 @ sk10 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7188:[bind(A,$thf( sk1 @ sk10 ))]]) ).
thf(5913,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,236]) ).
thf(5914,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5913]) ).
thf(5915,plain,
( ~ ( sk2 @ sk6 @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5914:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(11494,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,303]) ).
thf(11495,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11494]) ).
thf(11496,plain,
( ( nil @ ( sk1 @ sk12 @ cons ) @ equalelemsP )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11495:[bind(A,$thf( sk1 @ sk12 ))]]) ).
thf(1774,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,301]) ).
thf(1775,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) ) ),
inference(simp,[status(thm)],[1774]) ).
thf(1776,plain,
nil @ ( sk2 @ rearsegP ),
inference(pattern_uni,[status(thm)],[1775:[bind(A,$thf( sk2 ))]]) ).
thf(5372,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,303]) ).
thf(5373,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5372]) ).
thf(5374,plain,
( ( nil @ ( sk1 @ sk7 @ cons ) @ equalelemsP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5373:[bind(A,$thf( sk1 @ sk7 ))]]) ).
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(129,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(5799,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,197]) ).
thf(5800,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5799]) ).
thf(5801,plain,
( ( nil @ ( sk1 @ sk6 @ cons ) @ totalorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5800:[bind(A,$thf( sk1 @ sk6 ))]]) ).
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(134,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ hd )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
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(237,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(790,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[643,332]) ).
thf(791,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[790]) ).
thf(792,plain,
( ~ ( sk1 @ sk8 @ ( sk1 @ sk8 @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[791:[bind(A,$thf( sk1 @ sk8 ))]]) ).
thf(28,axiom,
~ ( nil @ singletonP ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax39) ).
thf(204,plain,
~ ( nil @ singletonP ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(205,plain,
~ ( nil @ singletonP ),
inference(polarity_switch,[status(thm)],[204]) ).
thf(91,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax49) ).
thf(508,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(11378,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk12 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,178]) ).
thf(11379,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk12 @ ssItem ) ),
inference(simp,[status(thm)],[11378]) ).
thf(11380,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk12 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[11379:[bind(A,$thf( sk2 ))]]) ).
thf(11542,plain,
! [A: $i] :
( ( ( sk2 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11380,197]) ).
thf(11543,plain,
! [A: $i] :
( ( ( sk2 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[11542]) ).
thf(11544,plain,
( ( nil @ ( sk2 @ sk12 @ cons ) @ totalorderedP )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11543:[bind(A,$thf( sk2 @ sk12 ))]]) ).
thf(100,plain,
! [B: $i,A: $i] :
( ~ sk5
| ~ ( sk4 @ ( nil @ neq ) )
| ( ( B @ ( sk3 @ app ) )
!= A )
| ( ( sk4 @ tl )
!= B )
| ~ ( B @ ssList )
| ( sk4 = A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ~ sk5
| ~ ( sk4 @ ( nil @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( sk3 @ app ) )
!= A )
| ( ( sk4 @ tl )
!= B )
| ( sk4 = A ) ),
inference(lifteq,[status(thm)],[100]) ).
thf(114,plain,
( ~ sk5
| ~ ( sk4 @ ( nil @ neq ) )
| ~ ( sk4 @ tl @ ssList )
| ~ ( sk4 @ tl @ ( sk3 @ app ) @ ssList )
| ( ( sk4 @ tl @ ( sk3 @ app ) )
= sk4 ) ),
inference(simp,[status(thm)],[113]) ).
thf(106,plain,
sk1 = sk3,
inference(cnfConj,[status(thm)],[99]) ).
thf(111,plain,
sk3 = sk1,
inference(lifteq,[status(thm)],[106]) ).
thf(557,plain,
( ~ $true
| ~ ( sk2 @ ( nil @ neq ) )
| ~ ( sk2 @ tl @ ssList )
| ~ ( sk2 @ tl @ ( sk1 @ app ) @ ssList )
| ( ( sk2 @ tl @ ( sk1 @ app ) )
= sk2 ) ),
inference(rewrite,[status(thm)],[114,112,550,111]) ).
thf(558,plain,
( ~ ( sk2 @ ( nil @ neq ) )
| ~ ( sk2 @ tl @ ssList )
| ~ ( sk2 @ tl @ ( sk1 @ app ) @ ssList )
| ( ( sk2 @ tl @ ( sk1 @ app ) )
= sk2 ) ),
inference(simp,[status(thm)],[557]) ).
thf(1165,plain,
( ( sk1 != sk1 )
| ( nil != nil )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(paramod_ordered,[status(thm)],[958,828]) ).
thf(1166,plain,
( ( sk1 != sk1 )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1165]) ).
thf(1167,plain,
( ( sk2 != sk1 )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(pattern_uni,[status(thm)],[1166:[]]) ).
thf(4919,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,371]) ).
thf(4920,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP ) ),
inference(simp,[status(thm)],[4919]) ).
thf(4921,plain,
nil @ ( sk38 @ cons ) @ totalorderP,
inference(pattern_uni,[status(thm)],[4920:[bind(A,$thf( sk38 ))]]) ).
thf(1762,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[650,301]) ).
thf(1763,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1762]) ).
thf(1764,plain,
( ( nil @ ( sk2 @ sk8 @ rearsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1763:[bind(A,$thf( sk2 @ sk8 ))]]) ).
thf(5357,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,221]) ).
thf(5358,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5357]) ).
thf(5359,plain,
( ~ ( sk1 @ sk7 @ ( sk1 @ sk7 @ lt ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5358:[bind(A,$thf( sk1 @ sk7 ))]]) ).
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(148,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(2027,plain,
! [A: $i] :
( ( A != sk39 )
| ( sk38 != nil )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[141,398]) ).
thf(2028,plain,
( ( sk38 != nil )
| ~ ( sk39 @ ( nil @ segmentP ) )
| ~ ( sk39 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2027:[bind(A,$thf( sk39 ))]]) ).
thf(586,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,215]) ).
thf(587,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[586]) ).
thf(588,plain,
~ ( sk38 @ ( sk38 @ neq ) ),
inference(pattern_uni,[status(thm)],[587:[bind(A,$thf( sk38 ))]]) ).
thf(595,plain,
( ( ( sk38 @ ( sk38 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,588]) ).
thf(596,plain,
( ( sk38 @ ( sk38 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[595]) ).
thf(601,plain,
( ( sk38 != nil )
| ( sk38 != sk2 ) ),
inference(simp,[status(thm)],[596]) ).
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(513,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(71,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( B @ ( A @ app ) @ ssList ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
thf(430,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssList )
=> ( B @ ( A @ app ) @ ssList ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
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(191,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(12036,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11833,248]) ).
thf(12037,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[12036]) ).
thf(12038,plain,
( ( nil @ ( sk1 @ sk14 @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12037:[bind(A,$thf( sk1 @ sk14 ))]]) ).
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(118,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(12197,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11892,248]) ).
thf(12198,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[12197]) ).
thf(12199,plain,
( ( nil @ ( sk2 @ sk14 @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12198:[bind(A,$thf( sk2 @ sk14 ))]]) ).
thf(12,axiom,
nil @ cyclefreeP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax60) ).
thf(144,plain,
nil @ cyclefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
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(498,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(4820,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,303]) ).
thf(4821,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP ) ),
inference(simp,[status(thm)],[4820]) ).
thf(4822,plain,
nil @ ( sk38 @ cons ) @ equalelemsP,
inference(pattern_uni,[status(thm)],[4821:[bind(A,$thf( sk38 ))]]) ).
thf(181,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ sk12 @ ( A @ sk11 @ lt ) )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[173]) ).
thf(1263,plain,
( ( ( sk1 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( sk1 @ ( nil @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[698,1143]) ).
thf(1264,plain,
( ( ( sk1 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( sk1 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[1263]) ).
thf(1279,plain,
( ( sk1 != nil )
| ( nil != nil )
| ~ ( sk1 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[1264]) ).
thf(1282,plain,
( ( sk1 != nil )
| ~ ( sk1 @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[1279]) ).
thf(1572,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[650,248]) ).
thf(1573,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1572]) ).
thf(1574,plain,
( ( nil @ ( sk2 @ sk8 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1573:[bind(A,$thf( sk2 @ sk8 ))]]) ).
thf(5825,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,221]) ).
thf(5826,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5825]) ).
thf(5827,plain,
( ~ ( sk1 @ sk6 @ ( sk1 @ sk6 @ lt ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5826:[bind(A,$thf( sk1 @ sk6 ))]]) ).
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(451,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(5405,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,215]) ).
thf(5406,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5405]) ).
thf(5407,plain,
( ~ ( sk1 @ sk7 @ ( sk1 @ sk7 @ neq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5406:[bind(A,$thf( sk1 @ sk7 ))]]) ).
thf(73,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax63) ).
thf(434,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ strictorderP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(5614,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,236]) ).
thf(5615,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5614]) ).
thf(5616,plain,
( ~ ( sk2 @ sk7 @ ( nil @ memberP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5615:[bind(A,$thf( sk2 @ sk7 ))]]) ).
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(477,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(12109,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11833,378]) ).
thf(12110,plain,
! [A: $i] :
( ( ( sk1 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[12109]) ).
thf(12111,plain,
( ( nil @ ( sk1 @ sk14 @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12110:[bind(A,$thf( sk1 @ sk14 ))]]) ).
thf(140,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ( nil != A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[138]) ).
thf(142,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[140]) ).
thf(143,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[142]) ).
thf(699,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[143,348]) ).
thf(700,plain,
nil @ ( nil @ segmentP ),
inference(simp,[status(thm)],[699]) ).
thf(1144,plain,
( ( sk1 != sk1 )
| ~ ( nil @ ( sk1 @ neq ) )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(paramod_ordered,[status(thm)],[958,789]) ).
thf(1145,plain,
( ~ ( nil @ ( sk1 @ neq ) )
| ~ ( sk1 @ ( nil @ frontsegP ) ) ),
inference(pattern_uni,[status(thm)],[1144:[]]) ).
thf(1306,plain,
( ( ( sk1 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( nil @ ( sk1 @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[698,1145]) ).
thf(1307,plain,
( ( ( sk1 @ ( nil @ frontsegP ) )
!= ( nil @ ( nil @ frontsegP ) ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[1306]) ).
thf(1322,plain,
( ( sk1 != nil )
| ( nil != nil )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[1307]) ).
thf(1325,plain,
( ( sk1 != nil )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[1322]) ).
thf(7652,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,165]) ).
thf(7653,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk6 @ ( A @ sk7 @ leq ) ) ),
inference(simp,[status(thm)],[7652]) ).
thf(7654,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk6 @ ( sk2 @ sk7 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[7653:[bind(A,$thf( sk2 ))]]) ).
thf(5883,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,197]) ).
thf(5884,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5883]) ).
thf(5885,plain,
( ( nil @ ( sk2 @ sk6 @ cons ) @ totalorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5884:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(154,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)],[153]) ).
thf(155,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)],[154]) ).
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(198,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(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(399,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(362,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)],[361]) ).
thf(365,plain,
! [B: $i,A: $i] :
( ( nil
= ( B @ ( A @ app ) ) )
| ( nil != A )
| ( nil != B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[362]) ).
thf(368,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
= nil )
| ( nil != A )
| ( nil != B ) ),
inference(lifteq,[status(thm)],[365]) ).
thf(369,plain,
( ~ ( nil @ ssList )
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(simp,[status(thm)],[368]) ).
thf(767,plain,
( ~ $true
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(rewrite,[status(thm)],[369,348]) ).
thf(768,plain,
( ( nil @ ( nil @ app ) )
= nil ),
inference(simp,[status(thm)],[767]) ).
thf(12777,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12618,301]) ).
thf(12778,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[12777]) ).
thf(12779,plain,
( ( nil @ ( sk1 @ sk13 @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12778:[bind(A,$thf( sk1 @ sk13 ))]]) ).
thf(778,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[650,332]) ).
thf(779,plain,
! [A: $i] :
( ( ( sk2 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[778]) ).
thf(780,plain,
( ~ ( sk2 @ sk8 @ ( sk2 @ sk8 @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[779:[bind(A,$thf( sk2 @ sk8 ))]]) ).
thf(7354,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7076,378]) ).
thf(7355,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7354]) ).
thf(7356,plain,
( ( nil @ ( sk2 @ sk10 @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7355:[bind(A,$thf( sk2 @ sk10 ))]]) ).
thf(5617,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,303]) ).
thf(5618,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5617]) ).
thf(5619,plain,
( ( nil @ ( sk2 @ sk7 @ cons ) @ equalelemsP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5618:[bind(A,$thf( sk2 @ sk7 ))]]) ).
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(521,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(784,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[348,332]) ).
thf(785,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[784]) ).
thf(786,plain,
~ ( nil @ ( nil @ neq ) ),
inference(pattern_uni,[status(thm)],[785:[bind(A,$thf( nil ))]]) ).
thf(804,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( nil @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[556,786]) ).
thf(805,plain,
( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( nil @ neq ) ) ),
inference(simp,[status(thm)],[804]) ).
thf(806,plain,
( ( nil != nil )
| ( sk2 != nil ) ),
inference(simp,[status(thm)],[805]) ).
thf(807,plain,
sk2 != nil,
inference(simp,[status(thm)],[806]) ).
thf(1079,plain,
! [A: $i] :
( ( A != sk2 )
| ( nil != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[126,807]) ).
thf(1080,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[1079]) ).
thf(1081,plain,
( ~ ( sk2 @ ( nil @ frontsegP ) )
| ~ ( sk2 @ ssList ) ),
inference(pattern_uni,[status(thm)],[1080:[bind(A,$thf( sk2 ))]]) ).
thf(1170,plain,
( ~ ( sk2 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[1081,104]) ).
thf(1171,plain,
~ ( sk2 @ ( nil @ frontsegP ) ),
inference(simp,[status(thm)],[1170]) ).
thf(10658,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10375,248]) ).
thf(10659,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[10658]) ).
thf(10660,plain,
( ( nil @ ( sk2 @ sk15 @ segmentP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10659:[bind(A,$thf( sk2 @ sk15 ))]]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[129]) ).
thf(11491,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,236]) ).
thf(11492,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11491]) ).
thf(11493,plain,
( ~ ( sk1 @ sk12 @ ( nil @ memberP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11492:[bind(A,$thf( sk1 @ sk12 ))]]) ).
thf(163,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ( ( A @ sk10 @ ( A @ sk7 @ cons ) @ ( A @ sk9 @ ( A @ sk6 @ cons ) @ ( A @ sk8 @ app ) @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(cnfConj,[status(thm)],[157]) ).
thf(167,plain,
! [A: $i] :
( ( A @ cyclefreeP )
| ~ ( A @ ssList )
| ( ( A @ sk10 @ ( A @ sk7 @ cons ) @ ( A @ sk9 @ ( A @ sk6 @ cons ) @ ( A @ sk8 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[163]) ).
thf(5810,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5727,121]) ).
thf(5811,plain,
! [A: $i] :
( ( ( sk1 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5810]) ).
thf(5812,plain,
( ( nil @ ( sk1 @ sk6 @ cons ) @ strictorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5811:[bind(A,$thf( sk1 @ sk6 ))]]) ).
thf(1581,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[643,248]) ).
thf(1582,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[1581]) ).
thf(1583,plain,
( ( nil @ ( sk1 @ sk8 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[1582:[bind(A,$thf( sk1 @ sk8 ))]]) ).
thf(860,plain,
! [A: $i] :
( ( A != sk38 )
| ( nil != nil )
| ( sk38 != sk2 )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[126,601]) ).
thf(861,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk38 != sk2 )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[860]) ).
thf(862,plain,
( ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ frontsegP ) )
| ~ ( sk38 @ ssList ) ),
inference(pattern_uni,[status(thm)],[861:[bind(A,$thf( sk38 ))]]) ).
thf(1632,plain,
( ( ( sk38 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,862]) ).
thf(1633,plain,
( ( ( sk38 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1632]) ).
thf(1648,plain,
( ( sk38 != sk2 )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1633]) ).
thf(1662,plain,
( ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[1648]) ).
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(255,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(5650,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,215]) ).
thf(5651,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5650]) ).
thf(5652,plain,
( ~ ( sk2 @ sk7 @ ( sk2 @ sk7 @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5651:[bind(A,$thf( sk2 @ sk7 ))]]) ).
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(458,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(7369,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7076,332]) ).
thf(7370,plain,
! [A: $i] :
( ( ( sk2 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7369]) ).
thf(7371,plain,
( ~ ( sk2 @ sk10 @ ( sk2 @ sk10 @ neq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7370:[bind(A,$thf( sk2 @ sk10 ))]]) ).
thf(13850,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk11 @ ssItem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,182]) ).
thf(13851,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ( A @ sk11 @ ssItem ) ),
inference(simp,[status(thm)],[13850]) ).
thf(13852,plain,
( ( sk2 @ strictorderP )
| ( sk2 @ sk11 @ ssItem ) ),
inference(pattern_uni,[status(thm)],[13851:[bind(A,$thf( sk2 ))]]) ).
thf(23,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax55) ).
thf(194,plain,
! [A: $i] :
( ( A @ ssList )
=> ( A @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
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(525,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(710,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,221]) ).
thf(711,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) ) ),
inference(simp,[status(thm)],[710]) ).
thf(712,plain,
~ ( sk38 @ ( sk38 @ lt ) ),
inference(pattern_uni,[status(thm)],[711:[bind(A,$thf( sk38 ))]]) ).
thf(13965,plain,
! [A: $i] :
( ( ( sk1 @ sk11 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[13810,236]) ).
thf(13966,plain,
! [A: $i] :
( ( ( sk1 @ sk11 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[13965]) ).
thf(13967,plain,
( ~ ( sk1 @ sk11 @ ( nil @ memberP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[13966:[bind(A,$thf( sk1 @ sk11 ))]]) ).
thf(11458,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,121]) ).
thf(11459,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11458]) ).
thf(11460,plain,
( ( nil @ ( sk1 @ sk12 @ cons ) @ strictorderedP )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11459:[bind(A,$thf( sk1 @ sk12 ))]]) ).
thf(149,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[148]) ).
thf(150,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( ( A @ ( B @ cons ) )
= ( A @ ( nil @ ( B @ cons ) @ app ) ) ) ),
inference(lifteq,[status(thm)],[149]) ).
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(414,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(2385,plain,
( ( sk1 != sk1 )
| ~ ( sk1 @ ( nil @ neq ) )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(paramod_ordered,[status(thm)],[2014,789]) ).
thf(2386,plain,
( ~ ( sk1 @ ( nil @ neq ) )
| ~ ( sk1 @ ( nil @ segmentP ) ) ),
inference(pattern_uni,[status(thm)],[2385:[]]) ).
thf(64,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ duplicatefreeP ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax71) ).
thf(409,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( nil @ ( A @ cons ) @ duplicatefreeP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
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(310,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ? [B: $i] :
( ( ( A @ hd )
= B )
& ( B @ ssItem ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(6118,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,161]) ).
thf(6119,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk7 @ ( A @ sk6 @ leq ) ) ),
inference(simp,[status(thm)],[6118]) ).
thf(6120,plain,
( ( sk2 @ cyclefreeP )
| ( sk2 @ sk7 @ ( sk2 @ sk6 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[6119:[bind(A,$thf( sk2 ))]]) ).
thf(12945,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12680,301]) ).
thf(12946,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[12945]) ).
thf(12947,plain,
( ( nil @ ( sk2 @ sk13 @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12946:[bind(A,$thf( sk2 @ sk13 ))]]) ).
thf(4903,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,371]) ).
thf(4904,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP ) ),
inference(simp,[status(thm)],[4903]) ).
thf(4905,plain,
nil @ ( sk39 @ cons ) @ totalorderP,
inference(pattern_uni,[status(thm)],[4904:[bind(A,$thf( sk39 ))]]) ).
thf(5910,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5751,371]) ).
thf(5911,plain,
! [A: $i] :
( ( ( sk2 @ sk6 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5910]) ).
thf(5912,plain,
( ( nil @ ( sk2 @ sk6 @ cons ) @ totalorderP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5911:[bind(A,$thf( sk2 @ sk6 ))]]) ).
thf(10464,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10325,301]) ).
thf(10465,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[10464]) ).
thf(10466,plain,
( ( nil @ ( sk1 @ sk15 @ rearsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10465:[bind(A,$thf( sk1 @ sk15 ))]]) ).
thf(11473,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11344,221]) ).
thf(11474,plain,
! [A: $i] :
( ( ( sk1 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ lt ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[11473]) ).
thf(11475,plain,
( ~ ( sk1 @ sk12 @ ( sk1 @ sk12 @ lt ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11474:[bind(A,$thf( sk1 @ sk12 ))]]) ).
thf(583,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,236]) ).
thf(584,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
~ ( sk38 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[584:[bind(A,$thf( sk38 ))]]) ).
thf(5611,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,371]) ).
thf(5612,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5611]) ).
thf(5613,plain,
( ( nil @ ( sk2 @ sk7 @ cons ) @ totalorderP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5612:[bind(A,$thf( sk2 @ sk7 ))]]) ).
thf(7232,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[7037,378]) ).
thf(7233,plain,
! [A: $i] :
( ( ( sk1 @ sk10 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[7232]) ).
thf(7234,plain,
( ( nil @ ( sk1 @ sk10 @ frontsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[7233:[bind(A,$thf( sk1 @ sk10 ))]]) ).
thf(95,axiom,
nil @ totalorderP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax62) ).
thf(524,plain,
nil @ totalorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
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(495,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(757,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,121]) ).
thf(758,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP ) ),
inference(simp,[status(thm)],[757]) ).
thf(759,plain,
nil @ ( sk39 @ cons ) @ strictorderedP,
inference(pattern_uni,[status(thm)],[758:[bind(A,$thf( sk39 ))]]) ).
thf(10576,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10325,378]) ).
thf(10577,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[10576]) ).
thf(10578,plain,
( ( nil @ ( sk1 @ sk15 @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10577:[bind(A,$thf( sk1 @ sk15 ))]]) ).
thf(27,axiom,
nil @ duplicatefreeP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax72) ).
thf(203,plain,
nil @ duplicatefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(10506,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10325,248]) ).
thf(10507,plain,
! [A: $i] :
( ( ( sk1 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[10506]) ).
thf(10508,plain,
( ( nil @ ( sk1 @ sk15 @ segmentP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10507:[bind(A,$thf( sk1 @ sk15 ))]]) ).
thf(4804,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[396,303]) ).
thf(4805,plain,
! [A: $i] :
( ( ( sk39 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ equalelemsP ) ),
inference(simp,[status(thm)],[4804]) ).
thf(4806,plain,
nil @ ( sk39 @ cons ) @ equalelemsP,
inference(pattern_uni,[status(thm)],[4805:[bind(A,$thf( sk39 ))]]) ).
thf(746,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ~ $true
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[724,158]) ).
thf(747,plain,
! [A: $i] :
( ( ( sk1 @ sk8 @ sk8 @ ssList )
!= ( A @ ssList ) )
| ( A @ cyclefreeP )
| ( A @ sk8 @ ssList )
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[746]) ).
thf(748,plain,
( ( sk1 @ sk8 @ sk8 @ cyclefreeP )
| ( sk1 @ sk8 @ sk8 @ sk8 @ ssList )
| ( sk1 @ sk8 @ cyclefreeP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[747:[bind(A,$thf( sk1 @ sk8 @ sk8 ))]]) ).
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(304,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(5366,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,371]) ).
thf(5367,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5366]) ).
thf(5368,plain,
( ( nil @ ( sk1 @ sk7 @ cons ) @ totalorderP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5367:[bind(A,$thf( sk1 @ sk7 ))]]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[170]) ).
thf(4978,plain,
( ( ( sk39 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk38 != nil )
| ~ ( sk39 @ ( nil @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,964]) ).
thf(4979,plain,
( ( ( sk39 @ ssList )
!= ( sk1 @ ssList ) )
| ( sk38 != nil )
| ~ ( sk39 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[4978]) ).
thf(5010,plain,
( ( sk39 != sk1 )
| ( sk38 != nil )
| ~ ( sk39 @ ( nil @ frontsegP ) ) ),
inference(simp,[status(thm)],[4979]) ).
thf(6692,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6467,248]) ).
thf(6693,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6692]) ).
thf(6694,plain,
( ( nil @ ( sk2 @ sk9 @ segmentP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6693:[bind(A,$thf( sk2 @ sk9 ))]]) ).
thf(92,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( nil
!= ( A @ ( B @ cons ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
thf(510,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( nil
!= ( A @ ( B @ cons ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(14052,plain,
! [A: $i] :
( ( ( sk2 @ sk11 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[13852,236]) ).
thf(14053,plain,
! [A: $i] :
( ( ( sk2 @ sk11 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[14052]) ).
thf(14054,plain,
( ~ ( sk2 @ sk11 @ ( nil @ memberP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[14053:[bind(A,$thf( sk2 @ sk11 ))]]) ).
thf(6534,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6431,301]) ).
thf(6535,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6534]) ).
thf(6536,plain,
( ( nil @ ( sk1 @ sk9 @ rearsegP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6535:[bind(A,$thf( sk1 @ sk9 ))]]) ).
thf(16036,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[105,188]) ).
thf(16037,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( ( nil @ ( A @ app ) )
= A ) ),
inference(simp,[status(thm)],[16036]) ).
thf(16038,plain,
( ( nil @ ( sk1 @ app ) )
= sk1 ),
inference(pattern_uni,[status(thm)],[16037:[bind(A,$thf( sk1 ))]]) ).
thf(119,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)],[118]) ).
thf(11578,plain,
! [A: $i] :
( ( ( sk2 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11380,236]) ).
thf(11579,plain,
! [A: $i] :
( ( ( sk2 @ sk12 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[11578]) ).
thf(11580,plain,
( ~ ( sk2 @ sk12 @ ( nil @ memberP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[11579:[bind(A,$thf( sk2 @ sk12 ))]]) ).
thf(4012,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,378]) ).
thf(4013,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) ) ),
inference(simp,[status(thm)],[4012]) ).
thf(4014,plain,
nil @ ( sk2 @ frontsegP ),
inference(pattern_uni,[status(thm)],[4013:[bind(A,$thf( sk2 ))]]) ).
thf(11033,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,177]) ).
thf(11034,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderP )
| ~ ( A @ sk11 @ ( A @ sk12 @ lt ) ) ),
inference(simp,[status(thm)],[11033]) ).
thf(11035,plain,
( ( sk2 @ strictorderP )
| ~ ( sk2 @ sk11 @ ( sk2 @ sk12 @ lt ) ) ),
inference(pattern_uni,[status(thm)],[11034:[bind(A,$thf( sk2 ))]]) ).
thf(190,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)],[189]) ).
thf(12270,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[11892,378]) ).
thf(12271,plain,
! [A: $i] :
( ( ( sk2 @ sk14 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[12270]) ).
thf(12272,plain,
( ( nil @ ( sk2 @ sk14 @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12271:[bind(A,$thf( sk2 @ sk14 ))]]) ).
thf(72,axiom,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ leq ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
thf(432,plain,
! [A: $i] :
( ( A @ ssItem )
=> ( A @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(3995,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,378]) ).
thf(3996,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) ) ),
inference(simp,[status(thm)],[3995]) ).
thf(3997,plain,
nil @ ( sk1 @ frontsegP ),
inference(pattern_uni,[status(thm)],[3996:[bind(A,$thf( sk1 ))]]) ).
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(422,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(5369,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,236]) ).
thf(5370,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5369]) ).
thf(5371,plain,
( ~ ( sk1 @ sk7 @ ( nil @ memberP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5370:[bind(A,$thf( sk1 @ sk7 ))]]) ).
thf(12902,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk1 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12618,378]) ).
thf(12903,plain,
! [A: $i] :
( ( ( sk1 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(simp,[status(thm)],[12902]) ).
thf(12904,plain,
( ( nil @ ( sk1 @ sk13 @ frontsegP ) )
| ( sk1 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[12903:[bind(A,$thf( sk1 @ sk13 ))]]) ).
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(239,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(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(506,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(13066,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[12680,378]) ).
thf(13067,plain,
! [A: $i] :
( ( ( sk2 @ sk13 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[13066]) ).
thf(13068,plain,
( ( nil @ ( sk2 @ sk13 @ frontsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[13067:[bind(A,$thf( sk2 @ sk13 ))]]) ).
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(474,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) @ tl )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(5584,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5227,197]) ).
thf(5585,plain,
! [A: $i] :
( ( ( sk2 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5584]) ).
thf(5586,plain,
( ( nil @ ( sk2 @ sk7 @ cons ) @ totalorderedP )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5585:[bind(A,$thf( sk2 @ sk7 ))]]) ).
thf(5320,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk39 != nil )
| ( nil != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[126,5098]) ).
thf(5321,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk39 != nil )
| ~ ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[5320]) ).
thf(5322,plain,
( ( sk39 != nil )
| ~ ( sk38 @ ( nil @ frontsegP ) )
| ~ ( sk38 @ ssList ) ),
inference(pattern_uni,[status(thm)],[5321:[bind(A,$thf( sk38 ))]]) ).
thf(43,axiom,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ hd @ ssItem ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
thf(294,plain,
! [A: $i] :
( ( A @ ssList )
=> ( ( nil != A )
=> ( A @ hd @ ssItem ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ cons ) @ hd )
= B )
| ~ ( B @ ssItem )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[134]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( ( A @ ( B @ cons ) @ hd )
= B ) ),
inference(lifteq,[status(thm)],[135]) ).
thf(2241,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[104,141]) ).
thf(2242,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( nil @ segmentP ) )
| ( nil = A ) ),
inference(simp,[status(thm)],[2241]) ).
thf(2243,plain,
( ~ ( sk2 @ ( nil @ segmentP ) )
| ( sk2 = nil ) ),
inference(pattern_uni,[status(thm)],[2242:[bind(A,$thf( sk2 ))]]) ).
thf(2467,plain,
~ ( sk2 @ ( nil @ segmentP ) ),
inference(simplifyReflect,[status(thm)],[2243,807]) ).
thf(8,axiom,
nil @ totalorderedP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax66) ).
thf(131,plain,
nil @ totalorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(41,axiom,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
!= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
thf(277,plain,
! [A: $i] :
( ( A @ ssList )
=> ! [B: $i] :
( ( B @ ssItem )
=> ( ( A @ ( B @ cons ) )
!= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
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(501,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(108,plain,
! [B: $i,A: $i] :
( ~ sk5
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) )
!= sk1 )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ~ sk5
| ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) )
!= sk1 ) ),
inference(lifteq,[status(thm)],[108]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ~ sk5
| ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) )
!= sk1 ) ),
inference(simp,[status(thm)],[115]) ).
thf(606,plain,
! [B: $i,A: $i] :
( ~ $true
| ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) )
!= sk1 ) ),
inference(rewrite,[status(thm)],[116,550]) ).
thf(607,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) )
!= sk1 ) ),
inference(simp,[status(thm)],[606]) ).
thf(5342,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[5203,121]) ).
thf(5343,plain,
! [A: $i] :
( ( ( sk1 @ sk7 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ strictorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[5342]) ).
thf(5344,plain,
( ( nil @ ( sk1 @ sk7 @ cons ) @ strictorderedP )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[5343:[bind(A,$thf( sk1 @ sk7 ))]]) ).
thf(4545,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[395,197]) ).
thf(4546,plain,
! [A: $i] :
( ( ( sk38 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[4545]) ).
thf(4547,plain,
nil @ ( sk38 @ cons ) @ totalorderedP,
inference(pattern_uni,[status(thm)],[4546:[bind(A,$thf( sk38 ))]]) ).
thf(10616,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10375,301]) ).
thf(10617,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[10616]) ).
thf(10618,plain,
( ( nil @ ( sk2 @ sk15 @ rearsegP ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10617:[bind(A,$thf( sk2 @ sk15 ))]]) ).
thf(6573,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ~ $true
| ( sk1 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6431,248]) ).
thf(6574,plain,
! [A: $i] :
( ( ( sk1 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6573]) ).
thf(6575,plain,
( ( nil @ ( sk1 @ sk9 @ segmentP ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6574:[bind(A,$thf( sk1 @ sk9 ))]]) ).
thf(10743,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ~ $true
| ( sk2 @ strictorderP ) ),
inference(paramod_ordered,[status(thm)],[10375,332]) ).
thf(10744,plain,
! [A: $i] :
( ( ( sk2 @ sk15 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) )
| ( sk2 @ strictorderP ) ),
inference(simp,[status(thm)],[10743]) ).
thf(10745,plain,
( ~ ( sk2 @ sk15 @ ( sk2 @ sk15 @ neq ) )
| ( sk2 @ strictorderP ) ),
inference(pattern_uni,[status(thm)],[10744:[bind(A,$thf( sk2 @ sk15 ))]]) ).
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(454,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(2073,plain,
! [A: $i] :
( ( A != sk38 )
| ( nil != nil )
| ( sk38 != sk2 )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[141,601]) ).
thf(2074,plain,
! [A: $i] :
( ( A != sk38 )
| ( sk38 != sk2 )
| ~ ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[2073]) ).
thf(2075,plain,
( ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ segmentP ) )
| ~ ( sk38 @ ssList ) ),
inference(pattern_uni,[status(thm)],[2074:[bind(A,$thf( sk38 ))]]) ).
thf(8608,plain,
( ( ( sk38 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,2075]) ).
thf(8609,plain,
( ( ( sk38 @ ssList )
!= ( sk2 @ ssList ) )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8608]) ).
thf(8634,plain,
( ( sk38 != sk2 )
| ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8609]) ).
thf(8670,plain,
( ( sk38 != sk2 )
| ~ ( sk38 @ ( nil @ segmentP ) ) ),
inference(simp,[status(thm)],[8634]) ).
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(222,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(6737,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ~ $true
| ( sk2 @ cyclefreeP ) ),
inference(paramod_ordered,[status(thm)],[6467,378]) ).
thf(6738,plain,
! [A: $i] :
( ( ( sk2 @ sk9 @ ssList )
!= ( A @ ssList ) )
| ( nil @ ( A @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(simp,[status(thm)],[6737]) ).
thf(6739,plain,
( ( nil @ ( sk2 @ sk9 @ frontsegP ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[6738:[bind(A,$thf( sk2 @ sk9 ))]]) ).
thf(29092,plain,
$false,
inference(e,[status(thm)],[1586,5918,1767,479,6431,352,10730,249,170,3990,762,16086,217,5842,2014,379,269,120,247,5589,11014,797,2448,5316,6655,814,153,4011,550,7147,698,11449,185,5227,5518,709,5903,301,6754,436,7311,417,12992,724,184,372,504,12154,702,1577,196,5836,189,5604,416,5727,1773,316,10117,2388,152,1568,179,591,5333,121,348,492,164,5888,11344,789,147,280,132,396,133,11490,411,206,12824,221,248,11993,10593,5751,5839,7269,534,5875,117,201,4531,7037,7642,220,334,6635,1580,302,349,160,297,407,137,165,6620,197,361,13810,12618,461,493,456,324,1143,5098,650,7249,156,188,169,6111,141,420,5951,7189,5915,11496,11892,393,1776,5374,129,11833,5801,371,134,237,105,792,205,508,11544,398,558,1167,4921,1764,5359,148,161,2028,180,444,601,513,430,191,12038,204,958,118,12199,144,498,4822,236,181,159,172,1282,1574,736,5827,377,451,5407,434,5616,98,303,477,631,10375,594,12111,700,1325,7654,964,5885,155,198,399,768,12779,780,11380,7356,5619,12680,521,1171,10660,130,11493,167,5812,1583,1662,162,255,112,1145,5652,458,7371,13852,194,145,525,712,13967,11460,150,414,327,2386,409,310,6120,12947,4905,5912,10466,5203,643,11475,177,182,585,370,5613,175,6467,7234,556,524,495,759,104,10578,203,10508,588,4806,748,304,158,5368,171,5010,786,6694,10325,186,235,510,14054,6536,16038,119,378,151,300,11580,4014,11035,190,12272,432,3997,422,5371,12904,210,239,506,807,13068,474,5586,828,5322,7076,294,126,136,395,332,2467,131,178,277,501,607,5344,111,122,4547,215,10618,6575,10745,454,8670,222,6739]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC015+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/0.39 % Computer : n005.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.39 % CPULimit : 300
% 0.15/0.39 % WCLimit : 300
% 0.15/0.39 % DateTime : Sat Sep 26 12:03:46 UTC 2026
% 0.15/0.39 % CPUTime :
% 0.15/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.91/1.16 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.50/1.55 % [INFO] Parsing done (387ms).
% 1.50/1.58 % [INFO] Running in sequential loop mode.
% 2.14/2.10 % [INFO] eprover registered as external prover.
% 2.14/2.11 % [INFO] Scanning for conjecture ...
% 2.55/2.26 % [INFO] Found a conjecture (or negated_conjecture) and 95 axioms. Running axiom selection ...
% 2.75/2.43 % [INFO] Axiom selection finished. Selected 95 axioms (removed 0 axioms).
% 3.08/2.61 % [INFO] Problem is first-order (TPTP FOF).
% 3.08/2.65 % [INFO] Type checking passed.
% 3.08/2.66 % [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 ...
% 65.90/23.92 % External prover 'e' found a proof!
% 65.90/23.93 % [INFO] Killing All external provers ...
% 65.90/23.93 % Time passed: 23302ms (effective reasoning time: 22344ms)
% 65.90/23.93 % 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)>
% 65.90/23.94 % 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
% 65.90/23.94 % No. of inferences in proof: 829
% 65.90/23.94 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 23302 ms resp. 22344 ms w/o parsing
% 68.20/24.59 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 68.20/24.61 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------