%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWC088-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:52:10 AM UTC 2026
% Result : Unsatisfiable 106.66s 24.04s
% Output : Refutation 112.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 195
% Syntax : Number of formulae : 878 ( 292 unt; 0 typ; 0 def)
% Number of atoms : 2758 ( 544 equ; 0 cnn)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 7642 (1622 ~;1430 |; 0 &;4590 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 75 ( 72 usr; 9 con; 0-2 aty)
% Number of variables : 1254 ( 0 ^;1254 !; 0 ?;1254 :)
% Comments :
%------------------------------------------------------------------------------
thf(ssList_decl,type,
ssList: $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(neq_decl,type,
neq: $i > $i > $o ).
thf(nil_decl,type,
nil: $i ).
thf(segmentP_decl,type,
segmentP: $i > $i > $o ).
thf(ssItem_decl,type,
ssItem: $i > $o ).
thf(app_decl,type,
app: $i > $i > $i ).
thf(cons_decl,type,
cons: $i > $i > $i ).
thf(skac3_decl,type,
skac3: $i ).
thf(skac2_decl,type,
skac2: $i ).
thf(skaf43_decl,type,
skaf43: $i > $i > $i ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(geq_decl,type,
geq: $i > $i > $o ).
thf(totalorderedP_decl,type,
totalorderedP: $i > $o ).
thf(lt_decl,type,
lt: $i > $i > $o ).
thf(gt_decl,type,
gt: $i > $i > $o ).
thf(skaf62_decl,type,
skaf62: $i > $i ).
thf(memberP_decl,type,
memberP: $i > $i > $o ).
thf(skaf69_decl,type,
skaf69: $i > $i ).
thf(skaf70_decl,type,
skaf70: $i > $i ).
thf(strictorderedP_decl,type,
strictorderedP: $i > $o ).
thf(cyclefreeP_decl,type,
cyclefreeP: $i > $o ).
thf(skaf49_decl,type,
skaf49: $i > $i ).
thf(skaf50_decl,type,
skaf50: $i > $i ).
thf(singletonP_decl,type,
singletonP: $i > $o ).
thf(skaf44_decl,type,
skaf44: $i > $i ).
thf(duplicatefreeP_decl,type,
duplicatefreeP: $i > $o ).
thf(skaf75_decl,type,
skaf75: $i > $i ).
thf(skaf74_decl,type,
skaf74: $i > $i ).
thf(skaf76_decl,type,
skaf76: $i > $i ).
thf(skaf77_decl,type,
skaf77: $i > $i ).
thf(skaf72_decl,type,
skaf72: $i > $i ).
thf(skaf79_decl,type,
skaf79: $i > $i ).
thf(hd_decl,type,
hd: $i > $i ).
thf(frontsegP_decl,type,
frontsegP: $i > $i > $o ).
thf(skaf71_decl,type,
skaf71: $i > $i ).
thf(skaf73_decl,type,
skaf73: $i > $i ).
thf(skaf46_decl,type,
skaf46: $i > $i > $i ).
thf(skaf64_decl,type,
skaf64: $i > $i ).
thf(tl_decl,type,
tl: $i > $i ).
thf(skaf66_decl,type,
skaf66: $i > $i ).
thf(skaf67_decl,type,
skaf67: $i > $i ).
thf(skaf65_decl,type,
skaf65: $i > $i ).
thf(skaf68_decl,type,
skaf68: $i > $i ).
thf(skaf45_decl,type,
skaf45: $i > $i > $i ).
thf(rearsegP_decl,type,
rearsegP: $i > $i > $o ).
thf(strictorderP_decl,type,
strictorderP: $i > $o ).
thf(skaf61_decl,type,
skaf61: $i > $i ).
thf(skaf59_decl,type,
skaf59: $i > $i ).
thf(skaf60_decl,type,
skaf60: $i > $i ).
thf(skaf63_decl,type,
skaf63: $i > $i ).
thf(skaf51_decl,type,
skaf51: $i > $i ).
thf(skaf52_decl,type,
skaf52: $i > $i ).
thf(skaf53_decl,type,
skaf53: $i > $i ).
thf(skaf57_decl,type,
skaf57: $i > $i ).
thf(equalelemsP_decl,type,
equalelemsP: $i > $o ).
thf(totalorderP_decl,type,
totalorderP: $i > $o ).
thf(skaf56_decl,type,
skaf56: $i > $i ).
thf(skaf54_decl,type,
skaf54: $i > $i ).
thf(skaf55_decl,type,
skaf55: $i > $i ).
thf(skaf58_decl,type,
skaf58: $i > $i ).
thf(skaf48_decl,type,
skaf48: $i > $i > $i ).
thf(skaf80_decl,type,
skaf80: $i > $i ).
thf(skaf47_decl,type,
skaf47: $i > $i > $i ).
thf(skaf78_decl,type,
skaf78: $i > $i ).
thf(skaf81_decl,type,
skaf81: $i > $i ).
thf(skaf83_decl,type,
skaf83: $i > $i ).
thf(skaf82_decl,type,
skaf82: $i > $i ).
thf(skaf42_decl,type,
skaf42: $i > $i > $i ).
thf(1,negated_conjecture,
sk1 @ ssList,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_1) ).
thf(198,plain,
sk1 @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(16,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
thf(225,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(226,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[225]) ).
thf(227,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[226]) ).
thf(228,plain,
! [A: $i] :
( ~ ( A @ ssList )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[227]) ).
thf(643,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[198,228]) ).
thf(644,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[643]) ).
thf(645,plain,
~ ( sk1 @ ( sk1 @ neq ) ),
inference(pattern_uni,[status(thm)],[644:[bind(A,$thf( sk1 ))]]) ).
thf(145,axiom,
! [A: $i] : ( A @ skaf51 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
thf(527,plain,
! [A: $i] : ( A @ skaf51 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(1313,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf51 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[527,228]) ).
thf(1314,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf51 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1313]) ).
thf(1315,plain,
! [A: $i] :
~ ( A @ skaf51 @ ( A @ skaf51 @ neq ) ),
inference(pattern_uni,[status(thm)],[1314:[bind(A,$thf( C )),bind(B,$thf( C @ skaf51 ))]]) ).
thf(1322,plain,
! [A: $i] :
~ ( A @ skaf51 @ ( A @ skaf51 @ neq ) ),
inference(simp,[status(thm)],[1315]) ).
thf(2,negated_conjecture,
sk2 @ ssList,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_2) ).
thf(201,plain,
sk2 @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(22,axiom,
! [A: $i] :
( ( ( nil @ ( A @ skaf44 @ cons ) )
= A )
| ~ ( A @ ssList )
| ~ ( A @ singletonP ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
thf(238,plain,
! [A: $i] :
( ( ( nil @ ( A @ skaf44 @ cons ) )
= A )
| ~ ( A @ ssList )
| ~ ( A @ singletonP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(239,plain,
! [A: $i] :
( ( ( nil @ ( A @ skaf44 @ cons ) )
= A )
| ~ ( A @ ssList )
| ~ ( A @ singletonP ) ),
inference(cnf,[status(esa)],[238]) ).
thf(240,plain,
! [A: $i] :
( ~ ( A @ ssList )
| ~ ( A @ singletonP )
| ( ( nil @ ( A @ skaf44 @ cons ) )
= A ) ),
inference(lifteq,[status(thm)],[239]) ).
thf(2304,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ singletonP )
| ( ( nil @ ( A @ skaf44 @ cons ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[201,240]) ).
thf(2305,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ singletonP )
| ( ( nil @ ( A @ skaf44 @ cons ) )
= A ) ),
inference(simp,[status(thm)],[2304]) ).
thf(2306,plain,
( ~ ( sk2 @ singletonP )
| ( ( nil @ ( sk2 @ skaf44 @ cons ) )
= sk2 ) ),
inference(pattern_uni,[status(thm)],[2305:[bind(A,$thf( sk2 ))]]) ).
thf(7,negated_conjecture,
nil @ ( sk2 @ neq ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
thf(202,plain,
nil @ ( sk2 @ neq ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(36,axiom,
! [A: $i] :
( ( nil = A )
| ( A @ tl @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
thf(269,plain,
! [A: $i] :
( ( nil = A )
| ( A @ tl @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(270,plain,
! [A: $i] :
( ( nil = A )
| ( A @ tl @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[269]) ).
thf(271,plain,
! [A: $i] :
( ( A @ tl @ ssList )
| ~ ( A @ ssList )
| ( nil = A ) ),
inference(lifteq,[status(thm)],[270]) ).
thf(10257,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ tl @ ssList )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[201,271]) ).
thf(10258,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ tl @ ssList )
| ( nil = A ) ),
inference(simp,[status(thm)],[10257]) ).
thf(10259,plain,
( ( sk2 @ tl @ ssList )
| ( nil = sk2 ) ),
inference(pattern_uni,[status(thm)],[10258:[bind(A,$thf( sk2 ))]]) ).
thf(640,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[201,228]) ).
thf(641,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[640]) ).
thf(642,plain,
~ ( sk2 @ ( sk2 @ neq ) ),
inference(pattern_uni,[status(thm)],[641:[bind(A,$thf( sk2 ))]]) ).
thf(651,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( sk2 @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,642]) ).
thf(652,plain,
( ( nil @ ( sk2 @ neq ) )
!= ( sk2 @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[651]) ).
thf(653,plain,
( ( nil != sk2 )
| ( sk2 != sk2 ) ),
inference(simp,[status(thm)],[652]) ).
thf(654,plain,
nil != sk2,
inference(simp,[status(thm)],[653]) ).
thf(11794,plain,
sk2 @ tl @ ssList,
inference(simplifyReflect,[status(thm)],[10259,654]) ).
thf(11801,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[11794,228]) ).
thf(11802,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[11801]) ).
thf(11803,plain,
~ ( sk2 @ tl @ ( sk2 @ tl @ neq ) ),
inference(pattern_uni,[status(thm)],[11802:[bind(A,$thf( sk2 @ tl ))]]) ).
thf(12534,plain,
( ( ( sk2 @ tl @ ( sk2 @ tl @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,11803]) ).
thf(12535,plain,
( ( sk2 @ tl @ ( sk2 @ tl @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[12534]) ).
thf(12564,plain,
( ( ( sk2 @ tl )
!= nil )
| ( ( sk2 @ tl )
!= sk2 ) ),
inference(simp,[status(thm)],[12535]) ).
thf(128,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ lt ) )
| ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
thf(479,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ lt ) )
| ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(168,axiom,
! [A: $i] : ( A @ skaf65 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
thf(575,plain,
! [A: $i] : ( A @ skaf65 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(14,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
thf(219,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(220,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(cnf,[status(esa)],[219]) ).
thf(221,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[220]) ).
thf(222,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[221]) ).
thf(39,axiom,
nil @ ssList,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
thf(279,plain,
nil @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(939,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem )
| ~ $true ),
inference(rewrite,[status(thm)],[222,279]) ).
thf(940,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem ) ),
inference(simp,[status(thm)],[939]) ).
thf(1831,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf65 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[575,940]) ).
thf(1832,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf65 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1831]) ).
thf(1833,plain,
! [A: $i] : ( nil @ ( A @ skaf65 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1832:[bind(A,$thf( C )),bind(B,$thf( C @ skaf65 ))]]) ).
thf(1840,plain,
! [A: $i] : ( nil @ ( A @ skaf65 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1833]) ).
thf(142,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ leq ) )
| ~ ( F @ ssList )
| ~ ( F @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
thf(518,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ leq ) )
| ~ ( F @ ssList )
| ~ ( F @ totalorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(122,axiom,
! [A: $i] :
( ( nil @ ( A @ frontsegP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
thf(468,plain,
! [A: $i] :
( ( nil @ ( A @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(20,axiom,
! [A: $i] :
( ( A @ strictorderedP )
| ~ ( A @ ssList )
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
thf(234,plain,
! [A: $i] :
( ( A @ strictorderedP )
| ~ ( A @ ssList )
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(113,axiom,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
thf(445,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(446,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(cnf,[status(esa)],[445]) ).
thf(447,plain,
! [A: $i] :
( ( A @ ( nil @ segmentP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[446]) ).
thf(448,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[447]) ).
thf(6013,plain,
( ( nil @ ( nil @ segmentP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[448,279]) ).
thf(6014,plain,
nil @ ( nil @ segmentP ),
inference(simp,[status(thm)],[6013]) ).
thf(27,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ app ) @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
thf(249,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ app ) @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(63,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( A @ cons ) @ hd )
= A )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
thf(333,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ cons ) @ hd )
= A )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(193,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ strictorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
thf(628,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ strictorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(171,axiom,
! [A: $i] : ( A @ skaf56 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
thf(582,plain,
! [A: $i] : ( A @ skaf56 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(13,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
thf(217,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(164,axiom,
! [A: $i] : ( A @ skaf74 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
thf(570,plain,
! [A: $i] : ( A @ skaf74 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(1719,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf74 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[570,940]) ).
thf(1720,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf74 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1719]) ).
thf(1721,plain,
! [A: $i] : ( nil @ ( A @ skaf74 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1720:[bind(A,$thf( C )),bind(B,$thf( C @ skaf74 ))]]) ).
thf(1728,plain,
! [A: $i] : ( nil @ ( A @ skaf74 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1721]) ).
thf(114,axiom,
! [C: $i,B: $i,A: $i] :
( ( C = A )
| ( C @ ( B @ memberP ) )
| ~ ( C @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( C @ ( B @ ( A @ cons ) @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
thf(449,plain,
! [C: $i,B: $i,A: $i] :
( ( C = A )
| ( C @ ( B @ memberP ) )
| ~ ( C @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( C @ ( B @ ( A @ cons ) @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(80,axiom,
! [A: $i] : ( A @ skaf73 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
thf(379,plain,
! [A: $i] : ( A @ skaf73 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(187,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
thf(614,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cons ) @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(180,axiom,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
thf(597,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(2344,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ singletonP )
| ( ( nil @ ( A @ skaf44 @ cons ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[198,240]) ).
thf(2345,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ singletonP )
| ( ( nil @ ( A @ skaf44 @ cons ) )
= A ) ),
inference(simp,[status(thm)],[2344]) ).
thf(2346,plain,
( ~ ( sk1 @ singletonP )
| ( ( nil @ ( sk1 @ skaf44 @ cons ) )
= sk1 ) ),
inference(pattern_uni,[status(thm)],[2345:[bind(A,$thf( sk1 ))]]) ).
thf(70,axiom,
! [A: $i] : ( A @ skaf44 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
thf(353,plain,
! [A: $i] : ( A @ skaf44 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(947,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf44 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[353,940]) ).
thf(948,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf44 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[947]) ).
thf(949,plain,
! [A: $i] : ( nil @ ( A @ skaf44 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[948:[bind(A,$thf( C )),bind(B,$thf( C @ skaf44 ))]]) ).
thf(967,plain,
! [A: $i] : ( nil @ ( A @ skaf44 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[949]) ).
thf(2606,plain,
! [A: $i] :
( ( ( nil @ ( sk1 @ skaf44 @ cons ) )
!= ( nil @ ( A @ skaf44 @ cons ) ) )
| ( sk1 @ totalorderedP )
| ~ ( sk1 @ singletonP ) ),
inference(paramod_ordered,[status(thm)],[2346,967]) ).
thf(2607,plain,
( ( sk1 @ totalorderedP )
| ~ ( sk1 @ singletonP ) ),
inference(pattern_uni,[status(thm)],[2606:[bind(A,$thf( sk1 ))]]) ).
thf(134,axiom,
! [A: $i] : ( A @ skaf81 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
thf(495,plain,
! [A: $i] : ( A @ skaf81 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(1301,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf81 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[495,228]) ).
thf(1302,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf81 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1301]) ).
thf(1303,plain,
! [A: $i] :
~ ( A @ skaf81 @ ( A @ skaf81 @ neq ) ),
inference(pattern_uni,[status(thm)],[1302:[bind(A,$thf( C )),bind(B,$thf( C @ skaf81 ))]]) ).
thf(1310,plain,
! [A: $i] :
~ ( A @ skaf81 @ ( A @ skaf81 @ neq ) ),
inference(simp,[status(thm)],[1303]) ).
thf(156,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( A @ cons ) @ tl )
= B )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
thf(550,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ cons ) @ tl )
= B )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(136,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ duplicatefreeP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
thf(500,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ duplicatefreeP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(124,axiom,
nil @ cyclefreeP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
thf(472,plain,
nil @ cyclefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(104,axiom,
! [A: $i] : ( A @ skaf80 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
thf(428,plain,
! [A: $i] : ( A @ skaf80 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(1011,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf80 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[428,228]) ).
thf(1012,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf80 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1011]) ).
thf(1013,plain,
! [A: $i] :
~ ( A @ skaf80 @ ( A @ skaf80 @ neq ) ),
inference(pattern_uni,[status(thm)],[1012:[bind(A,$thf( C )),bind(B,$thf( C @ skaf80 ))]]) ).
thf(1020,plain,
! [A: $i] :
~ ( A @ skaf80 @ ( A @ skaf80 @ neq ) ),
inference(simp,[status(thm)],[1013]) ).
thf(3610,plain,
! [A: $i] :
( ( ( A @ skaf80 @ ( A @ skaf80 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,1020]) ).
thf(3611,plain,
! [A: $i] :
( ( A @ skaf80 @ ( A @ skaf80 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[3610]) ).
thf(3616,plain,
! [A: $i] :
( ( ( A @ skaf80 )
!= nil )
| ( ( A @ skaf80 )
!= sk2 ) ),
inference(simp,[status(thm)],[3611]) ).
thf(8,negated_conjecture,
! [A: $i] :
( ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
thf(204,plain,
! [A: $i] :
( ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(209,plain,
! [A: $i] :
( ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[204]) ).
thf(661,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[198,209]) ).
thf(662,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[661]) ).
thf(663,plain,
( ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ ( sk1 @ ( sk2 @ segmentP ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( sk1 ))]]) ).
thf(749,plain,
( ~ $true
| ( ( sk1 @ ( sk2 @ segmentP ) )
!= ( sk1 @ ( sk1 @ segmentP ) ) )
| ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(eqfactor_ordered,[status(thm)],[663]) ).
thf(752,plain,
( ( sk1 != sk1 )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[749]) ).
thf(753,plain,
( ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[752]) ).
thf(811,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( sk1 @ neq ) ) )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,753]) ).
thf(812,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( sk1 @ neq ) ) )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[811]) ).
thf(813,plain,
( ( nil != nil )
| ( sk2 != sk1 )
| ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[812]) ).
thf(814,plain,
( ( sk2 != sk1 )
| ~ ( sk1 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[813]) ).
thf(66,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ gt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
thf(340,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ gt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(667,plain,
! [A: $i] :
( ~ $true
| ( ( A @ ( sk2 @ segmentP ) )
!= ( A @ ( sk1 @ segmentP ) ) )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(eqfactor_ordered,[status(thm)],[209]) ).
thf(669,plain,
! [A: $i] :
( ( A != A )
| ( sk2 != sk1 )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[667]) ).
thf(670,plain,
! [A: $i] :
( ( sk2 != sk1 )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( A @ neq ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[669]) ).
thf(93,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
thf(404,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(99,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
thf(417,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ gt ) )
| ~ ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(43,axiom,
! [A: $i] :
( ( ( A @ skaf63 @ ( A @ skaf60 @ cons ) @ ( A @ skaf62 @ ( A @ skaf59 @ cons ) @ ( A @ skaf61 @ app ) @ app ) )
= A )
| ( A @ strictorderP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
thf(288,plain,
! [A: $i] :
( ( ( A @ skaf63 @ ( A @ skaf60 @ cons ) @ ( A @ skaf62 @ ( A @ skaf59 @ cons ) @ ( A @ skaf61 @ app ) @ app ) )
= A )
| ( A @ strictorderP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(173,axiom,
! [A: $i] : ( A @ skaf50 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
thf(585,plain,
! [A: $i] : ( A @ skaf50 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(1997,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf50 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[585,940]) ).
thf(1998,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf50 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1997]) ).
thf(1999,plain,
! [A: $i] : ( nil @ ( A @ skaf50 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1998:[bind(A,$thf( C )),bind(B,$thf( C @ skaf50 ))]]) ).
thf(2010,plain,
! [A: $i] : ( nil @ ( A @ skaf50 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1999]) ).
thf(250,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ app ) @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[249]) ).
thf(3702,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ssList )
!= ( B @ ssList ) )
| ( A @ ( B @ app ) @ ssList )
| ~ $true
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[201,250]) ).
thf(3703,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ssList )
!= ( B @ ssList ) )
| ( A @ ( B @ app ) @ ssList )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[3702]) ).
thf(3704,plain,
! [A: $i] :
( ( A @ ( sk2 @ app ) @ ssList )
| ~ ( A @ ssList ) ),
inference(pattern_uni,[status(thm)],[3703:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(6580,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[201,3704]) ).
thf(6581,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6580]) ).
thf(6582,plain,
sk2 @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[6581:[bind(A,$thf( sk2 ))]]) ).
thf(6752,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[6582,228]) ).
thf(6753,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[6752]) ).
thf(6754,plain,
~ ( sk2 @ ( sk2 @ app ) @ ( sk2 @ ( sk2 @ app ) @ neq ) ),
inference(pattern_uni,[status(thm)],[6753:[bind(A,$thf( sk2 @ ( sk2 @ app ) ))]]) ).
thf(30,axiom,
! [A: $i] :
( ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A )
| ( A @ strictorderedP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
thf(255,plain,
! [A: $i] :
( ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A )
| ( A @ strictorderedP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(256,plain,
! [A: $i] :
( ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A )
| ( A @ strictorderedP )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[255]) ).
thf(257,plain,
! [A: $i] :
( ( A @ strictorderedP )
| ~ ( A @ ssList )
| ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[256]) ).
thf(751,plain,
( ( ( sk1 @ ( sk2 @ segmentP ) )
!= ( sk1 @ ( sk1 @ segmentP ) ) )
| ~ ( sk1 @ ( sk1 @ segmentP ) )
| ~ ( nil @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[749]) ).
thf(185,axiom,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
thf(609,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(610,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(cnf,[status(esa)],[609]) ).
thf(611,plain,
! [A: $i] :
( ( A @ ( nil @ frontsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[610]) ).
thf(612,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[611]) ).
thf(6433,plain,
( ( nil @ ( nil @ frontsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[612,279]) ).
thf(6434,plain,
nil @ ( nil @ frontsegP ),
inference(simp,[status(thm)],[6433]) ).
thf(5,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
thf(196,plain,
sk2 = sk4,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(153,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ app ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
thf(542,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ app ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(118,axiom,
! [A: $i] :
( ( nil = A )
| ( ( A @ tl @ ( A @ hd @ cons ) )
= A )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
thf(460,plain,
! [A: $i] :
( ( nil = A )
| ( ( A @ tl @ ( A @ hd @ cons ) )
= A )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(84,axiom,
! [A: $i] : ( A @ skaf55 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
thf(387,plain,
! [A: $i] : ( A @ skaf55 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(105,axiom,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( nil @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
thf(429,plain,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(430,plain,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(cnf,[status(esa)],[429]) ).
thf(898,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf55 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[387,430]) ).
thf(899,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf55 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[898]) ).
thf(900,plain,
! [A: $i] :
~ ( A @ skaf55 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[899:[bind(A,$thf( C )),bind(B,$thf( C @ skaf55 ))]]) ).
thf(902,plain,
! [A: $i] :
~ ( A @ skaf55 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[900]) ).
thf(159,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
thf(559,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(120,axiom,
! [A: $i] : ( A @ skaf68 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
thf(466,plain,
! [A: $i] : ( A @ skaf68 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(1138,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf68 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[466,228]) ).
thf(1139,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf68 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1138]) ).
thf(1140,plain,
! [A: $i] :
~ ( A @ skaf68 @ ( A @ skaf68 @ neq ) ),
inference(pattern_uni,[status(thm)],[1139:[bind(A,$thf( C )),bind(B,$thf( C @ skaf68 ))]]) ).
thf(1147,plain,
! [A: $i] :
~ ( A @ skaf68 @ ( A @ skaf68 @ neq ) ),
inference(simp,[status(thm)],[1140]) ).
thf(59,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ gt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
thf(325,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ gt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(31,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
thf(258,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(259,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(cnf,[status(esa)],[258]) ).
thf(260,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ lt ) )
| ~ ( F @ ssList )
| ~ ( F @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(lifteq,[status(thm)],[259]) ).
thf(261,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ lt ) )
| ~ ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) @ ssList )
| ~ ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) @ strictorderedP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList ) ),
inference(simp,[status(thm)],[260]) ).
thf(956,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf55 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[387,940]) ).
thf(957,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf55 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[956]) ).
thf(958,plain,
! [A: $i] : ( nil @ ( A @ skaf55 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[957:[bind(A,$thf( C )),bind(B,$thf( C @ skaf55 ))]]) ).
thf(969,plain,
! [A: $i] : ( nil @ ( A @ skaf55 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[958]) ).
thf(184,axiom,
! [B: $i,A: $i] :
( ( ( A @ ( B @ skaf48 ) @ ( B @ ( B @ ( A @ skaf47 ) @ app ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
thf(606,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ skaf48 ) @ ( B @ ( B @ ( A @ skaf47 ) @ app ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(150,axiom,
! [A: $i] : ( A @ skaf66 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
thf(535,plain,
! [A: $i] : ( A @ skaf66 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(1337,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf66 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[535,228]) ).
thf(1338,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf66 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1337]) ).
thf(1339,plain,
! [A: $i] :
~ ( A @ skaf66 @ ( A @ skaf66 @ neq ) ),
inference(pattern_uni,[status(thm)],[1338:[bind(A,$thf( C )),bind(B,$thf( C @ skaf66 ))]]) ).
thf(1347,plain,
! [A: $i] :
~ ( A @ skaf66 @ ( A @ skaf66 @ neq ) ),
inference(simp,[status(thm)],[1339]) ).
thf(11839,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11794,3704]) ).
thf(11840,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[11839]) ).
thf(11841,plain,
sk2 @ tl @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[11840:[bind(A,$thf( sk2 @ tl ))]]) ).
thf(12619,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11841,3704]) ).
thf(12620,plain,
! [A: $i] :
( ( ( sk2 @ tl @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[12619]) ).
thf(12621,plain,
sk2 @ tl @ ( sk2 @ app ) @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[12620:[bind(A,$thf( sk2 @ tl @ ( sk2 @ app ) ))]]) ).
thf(98,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf48 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
thf(416,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf48 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(133,axiom,
! [A: $i] :
( ( ( A @ skaf81 @ ( A @ skaf79 @ cons ) @ ( A @ skaf78 @ cons ) @ ( A @ skaf80 @ app ) )
= A )
| ( A @ equalelemsP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
thf(492,plain,
! [A: $i] :
( ( ( A @ skaf81 @ ( A @ skaf79 @ cons ) @ ( A @ skaf78 @ cons ) @ ( A @ skaf80 @ app ) )
= A )
| ( A @ equalelemsP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(57,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf45 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
thf(321,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf45 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(3976,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf45 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[321,228]) ).
thf(3977,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf45 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[3976]) ).
thf(3978,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf45 ) @ ( B @ ( A @ skaf45 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[3977:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf45 ) ))]]) ).
thf(4018,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf45 ) @ ( B @ ( A @ skaf45 ) @ neq ) ),
inference(simp,[status(thm)],[3978]) ).
thf(111,axiom,
! [A: $i] : ( A @ skaf53 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
thf(443,plain,
! [A: $i] : ( A @ skaf53 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(29,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
thf(253,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(130,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ lt ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
thf(485,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ lt ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(10600,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ tl @ ssList )
| ~ $true
| ( nil = A ) ),
inference(paramod_ordered,[status(thm)],[198,271]) ).
thf(10601,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ tl @ ssList )
| ( nil = A ) ),
inference(simp,[status(thm)],[10600]) ).
thf(10602,plain,
( ( sk1 @ tl @ ssList )
| ( nil = sk1 ) ),
inference(pattern_uni,[status(thm)],[10601:[bind(A,$thf( sk1 ))]]) ).
thf(21,axiom,
! [A: $i] :
( ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
thf(236,plain,
! [A: $i] :
( ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(237,plain,
! [A: $i] :
( ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[236]) ).
thf(2220,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[198,237]) ).
thf(2221,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP ) ),
inference(simp,[status(thm)],[2220]) ).
thf(2222,plain,
( ( sk1 @ skaf50 @ ( sk1 @ skaf49 @ leq ) )
| ( sk1 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[2221:[bind(A,$thf( sk1 ))]]) ).
thf(12,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf43 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
thf(216,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf43 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(32,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf46 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
thf(262,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf46 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(3921,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf46 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[262,228]) ).
thf(3922,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf46 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[3921]) ).
thf(3923,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf46 ) @ ( B @ ( A @ skaf46 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[3922:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf46 ) ))]]) ).
thf(3966,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf46 ) @ ( B @ ( A @ skaf46 ) @ neq ) ),
inference(simp,[status(thm)],[3923]) ).
thf(179,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf42 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
thf(596,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf42 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(4529,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf42 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[596,228]) ).
thf(4530,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf42 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[4529]) ).
thf(4531,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf42 ) @ ( B @ ( A @ skaf42 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[4530:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf42 ) ))]]) ).
thf(4583,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf42 ) @ ( B @ ( A @ skaf42 ) @ neq ) ),
inference(simp,[status(thm)],[4531]) ).
thf(23,axiom,
! [A: $i] :
( ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A )
| ( A @ duplicatefreeP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
thf(241,plain,
! [A: $i] :
( ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A )
| ( A @ duplicatefreeP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(242,plain,
! [A: $i] :
( ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A )
| ( A @ duplicatefreeP )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[241]) ).
thf(243,plain,
! [A: $i] :
( ( A @ duplicatefreeP )
| ~ ( A @ ssList )
| ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[242]) ).
thf(2467,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ duplicatefreeP )
| ~ $true
| ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[201,243]) ).
thf(2468,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ duplicatefreeP )
| ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A ) ),
inference(simp,[status(thm)],[2467]) ).
thf(2469,plain,
( ( sk2 @ duplicatefreeP )
| ( ( sk2 @ skaf77 @ ( sk2 @ skaf74 @ cons ) @ ( sk2 @ skaf76 @ ( sk2 @ skaf74 @ cons ) @ ( sk2 @ skaf75 @ app ) @ app ) )
= sk2 ) ),
inference(pattern_uni,[status(thm)],[2468:[bind(A,$thf( sk2 ))]]) ).
thf(167,axiom,
! [A: $i] : ( A @ skaf54 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
thf(574,plain,
! [A: $i] : ( A @ skaf54 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(83,axiom,
! [A: $i] : ( A @ skaf69 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
thf(386,plain,
! [A: $i] : ( A @ skaf69 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(962,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf69 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[386,940]) ).
thf(963,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf69 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[962]) ).
thf(964,plain,
! [A: $i] : ( nil @ ( A @ skaf69 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[963:[bind(A,$thf( C )),bind(B,$thf( C @ skaf69 ))]]) ).
thf(966,plain,
! [A: $i] : ( nil @ ( A @ skaf69 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[964]) ).
thf(182,axiom,
! [A: $i] :
( ( A @ equalelemsP )
| ~ ( A @ ssList )
| ( ( A @ skaf79 )
!= ( A @ skaf78 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
thf(602,plain,
! [A: $i] :
( ( A @ equalelemsP )
| ~ ( A @ ssList )
| ( ( A @ skaf79 )
!= ( A @ skaf78 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(40,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( A @ skaf45 ) @ ( B @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
thf(280,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ skaf45 ) @ ( B @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(655,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( A @ neq ) ) )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ $true
| ~ ( A @ ssList ) ),
inference(paramod_ordered,[status(thm)],[202,209]) ).
thf(656,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ neq ) )
!= ( nil @ ( A @ neq ) ) )
| ~ ( A @ ( sk1 @ segmentP ) )
| ~ ( A @ ( sk2 @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(simp,[status(thm)],[655]) ).
thf(657,plain,
( ~ ( sk2 @ ( sk1 @ segmentP ) )
| ~ ( sk2 @ ( sk2 @ segmentP ) )
| ~ ( sk2 @ ssList ) ),
inference(pattern_uni,[status(thm)],[656:[bind(A,$thf( sk2 ))]]) ).
thf(731,plain,
( ~ ( sk2 @ ( sk1 @ segmentP ) )
| ~ ( sk2 @ ( sk2 @ segmentP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[657,201]) ).
thf(732,plain,
( ~ ( sk2 @ ( sk1 @ segmentP ) )
| ~ ( sk2 @ ( sk2 @ segmentP ) ) ),
inference(simp,[status(thm)],[731]) ).
thf(733,plain,
( ~ $true
| ( ( sk2 @ ( sk2 @ segmentP ) )
!= ( sk2 @ ( sk1 @ segmentP ) ) )
| ~ ( sk2 @ ( sk1 @ segmentP ) ) ),
inference(eqfactor_ordered,[status(thm)],[732]) ).
thf(734,plain,
( ( ( sk2 @ ( sk2 @ segmentP ) )
!= ( sk2 @ ( sk1 @ segmentP ) ) )
| ~ ( sk2 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[733]) ).
thf(33,axiom,
! [A: $i] : ( A @ skaf64 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
thf(263,plain,
! [A: $i] : ( A @ skaf64 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(770,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf64 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[263,430]) ).
thf(771,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf64 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[770]) ).
thf(772,plain,
! [A: $i] :
~ ( A @ skaf64 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[771:[bind(A,$thf( C )),bind(B,$thf( C @ skaf64 ))]]) ).
thf(774,plain,
! [A: $i] :
~ ( A @ skaf64 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[772]) ).
thf(17,axiom,
! [A: $i] : ( A @ skaf62 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
thf(229,plain,
! [A: $i] : ( A @ skaf62 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(707,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf62 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[229,228]) ).
thf(708,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf62 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[707]) ).
thf(709,plain,
! [A: $i] :
~ ( A @ skaf62 @ ( A @ skaf62 @ neq ) ),
inference(pattern_uni,[status(thm)],[708:[bind(A,$thf( C )),bind(B,$thf( C @ skaf62 ))]]) ).
thf(716,plain,
! [A: $i] :
~ ( A @ skaf62 @ ( A @ skaf62 @ neq ) ),
inference(simp,[status(thm)],[709]) ).
thf(1349,plain,
! [A: $i] :
( ( ( A @ skaf62 @ ( A @ skaf62 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,716]) ).
thf(1350,plain,
! [A: $i] :
( ( A @ skaf62 @ ( A @ skaf62 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[1349]) ).
thf(1351,plain,
! [A: $i] :
( ( ( A @ skaf62 )
!= nil )
| ( ( A @ skaf62 )
!= sk2 ) ),
inference(simp,[status(thm)],[1350]) ).
thf(90,axiom,
! [A: $i] : ( A @ skaf60 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
thf(398,plain,
! [A: $i] : ( A @ skaf60 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(980,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf60 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[398,430]) ).
thf(981,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf60 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[980]) ).
thf(982,plain,
! [A: $i] :
~ ( A @ skaf60 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[981:[bind(A,$thf( C )),bind(B,$thf( C @ skaf60 ))]]) ).
thf(988,plain,
! [A: $i] :
~ ( A @ skaf60 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[982]) ).
thf(34,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
thf(264,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(265,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) ) ),
inference(cnf,[status(esa)],[264]) ).
thf(192,axiom,
! [A: $i] : ( A @ skaf59 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
thf(627,plain,
! [A: $i] : ( A @ skaf59 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(2141,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf59 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[627,940]) ).
thf(2142,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf59 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[2141]) ).
thf(2143,plain,
! [A: $i] : ( nil @ ( A @ skaf59 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[2142:[bind(A,$thf( C )),bind(B,$thf( C @ skaf59 ))]]) ).
thf(2154,plain,
! [A: $i] : ( nil @ ( A @ skaf59 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[2143]) ).
thf(206,plain,
sk4 = sk2,
inference(lifteq,[status(thm)],[196]) ).
thf(51,axiom,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf59 @ ( A @ skaf60 @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
thf(307,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf59 @ ( A @ skaf60 @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(45,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( F @ ssList )
| ~ ( F @ cyclefreeP )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ~ ( D @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) )
!= F )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
thf(292,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( F @ ssList )
| ~ ( F @ cyclefreeP )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ~ ( D @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( B @ cons ) @ ( D @ ( A @ cons ) @ ( C @ app ) @ app ) )
!= F )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(26,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ hd @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
thf(246,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ hd @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(247,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ hd @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP ) ),
inference(cnf,[status(esa)],[246]) ).
thf(248,plain,
! [B: $i,A: $i] :
( ( B @ hd @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ strictorderedP )
| ( nil = B ) ),
inference(lifteq,[status(thm)],[247]) ).
thf(81,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ rearsegP ) )
| ~ ( B @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
thf(380,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ rearsegP ) )
| ~ ( B @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(75,axiom,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ app ) @ app ) )
= ( A @ ( B @ app ) @ ( C @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
thf(366,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ app ) @ app ) )
= ( A @ ( B @ app ) @ ( C @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(149,axiom,
! [A: $i] : ( A @ skaf63 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
thf(534,plain,
! [A: $i] : ( A @ skaf63 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(19,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ memberP ) )
| ( C @ ( B @ memberP ) )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ( B @ ( A @ app ) @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
thf(232,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ memberP ) )
| ( C @ ( B @ memberP ) )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ( B @ ( A @ app ) @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(233,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ memberP ) )
| ( C @ ( B @ memberP ) )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ( B @ ( A @ app ) @ memberP ) ) ),
inference(cnf,[status(esa)],[232]) ).
thf(115,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( E @ ssList )
| ~ ( E @ duplicatefreeP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( D @ ssList )
| ( ( D @ ( B @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= E ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
thf(452,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( E @ ssList )
| ~ ( E @ duplicatefreeP )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( D @ ssList )
| ( ( D @ ( B @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(147,axiom,
skac3 @ ssItem,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
thf(530,plain,
skac3 @ ssItem,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(950,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[530,940]) ).
thf(951,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[950]) ).
thf(952,plain,
nil @ ( skac3 @ cons ) @ totalorderedP,
inference(pattern_uni,[status(thm)],[951:[bind(A,$thf( skac3 ))]]) ).
thf(69,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( A @ app ) )
= nil )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( nil != B )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
thf(349,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ app ) )
= nil )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( nil != B )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(160,axiom,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ segmentP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
thf(561,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(87,axiom,
! [A: $i] :
( ( A @ ( A @ rearsegP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
thf(392,plain,
! [A: $i] :
( ( A @ ( A @ rearsegP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(47,axiom,
! [A: $i] :
( ( ( A @ skaf53 @ ( A @ skaf50 @ cons ) @ ( A @ skaf52 @ ( A @ skaf49 @ cons ) @ ( A @ skaf51 @ app ) @ app ) )
= A )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
thf(297,plain,
! [A: $i] :
( ( ( A @ skaf53 @ ( A @ skaf50 @ cons ) @ ( A @ skaf52 @ ( A @ skaf49 @ cons ) @ ( A @ skaf51 @ app ) @ app ) )
= A )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(94,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( nil @ ( A @ cons ) @ app ) )
= ( B @ ( A @ cons ) ) )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
thf(407,plain,
! [B: $i,A: $i] :
( ( ( B @ ( nil @ ( A @ cons ) @ app ) )
= ( B @ ( A @ cons ) ) )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(38,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
thf(275,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(175,axiom,
! [A: $i] : ( A @ skaf71 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
thf(589,plain,
! [A: $i] : ( A @ skaf71 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(2014,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf71 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[589,228]) ).
thf(2015,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf71 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[2014]) ).
thf(2016,plain,
! [A: $i] :
~ ( A @ skaf71 @ ( A @ skaf71 @ neq ) ),
inference(pattern_uni,[status(thm)],[2015:[bind(A,$thf( C )),bind(B,$thf( C @ skaf71 ))]]) ).
thf(2032,plain,
! [A: $i] :
~ ( A @ skaf71 @ ( A @ skaf71 @ neq ) ),
inference(simp,[status(thm)],[2016]) ).
thf(6618,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[279,3704]) ).
thf(6619,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6618]) ).
thf(6620,plain,
nil @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[6619:[bind(A,$thf( nil ))]]) ).
thf(121,axiom,
nil @ totalorderP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
thf(467,plain,
nil @ totalorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(28,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ frontsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
thf(251,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ frontsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(252,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ frontsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ frontsegP ) )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(cnf,[status(esa)],[251]) ).
thf(10,negated_conjecture,
( ( nil != sk4 )
| ( nil = sk3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
thf(197,plain,
( ( nil != sk4 )
| ( nil = sk3 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(108,axiom,
! [A: $i] :
( ( ( nil @ ( A @ app ) )
= A )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
thf(435,plain,
! [A: $i] :
( ( ( nil @ ( A @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(129,axiom,
~ ( nil @ singletonP ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
thf(483,plain,
~ ( nil @ singletonP ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(484,plain,
~ ( nil @ singletonP ),
inference(polarity_switch,[status(thm)],[483]) ).
thf(11979,plain,
( ( nil != nil )
| ~ ( sk1 @ singletonP )
| ( sk1 @ tl @ ssList ) ),
inference(paramod_ordered,[status(thm)],[10602,484]) ).
thf(11980,plain,
( ~ ( sk1 @ singletonP )
| ( sk1 @ tl @ ssList ) ),
inference(pattern_uni,[status(thm)],[11979:[]]) ).
thf(126,axiom,
! [A: $i] : ( A @ skaf52 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
thf(477,plain,
! [A: $i] : ( A @ skaf52 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(1150,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf52 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[477,228]) ).
thf(1151,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf52 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1150]) ).
thf(1152,plain,
! [A: $i] :
~ ( A @ skaf52 @ ( A @ skaf52 @ neq ) ),
inference(pattern_uni,[status(thm)],[1151:[bind(A,$thf( C )),bind(B,$thf( C @ skaf52 ))]]) ).
thf(1159,plain,
! [A: $i] :
~ ( A @ skaf52 @ ( A @ skaf52 @ neq ) ),
inference(simp,[status(thm)],[1152]) ).
thf(6636,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[198,3704]) ).
thf(6637,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6636]) ).
thf(6638,plain,
sk1 @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[6637:[bind(A,$thf( sk1 ))]]) ).
thf(9289,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6638,3704]) ).
thf(9290,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[9289]) ).
thf(9291,plain,
sk1 @ ( sk2 @ app ) @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[9290:[bind(A,$thf( sk1 @ ( sk2 @ app ) ))]]) ).
thf(116,axiom,
! [A: $i] :
( ( A @ ( A @ leq ) )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
thf(456,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(162,axiom,
! [A: $i] : ( A @ skaf83 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
thf(566,plain,
! [A: $i] : ( A @ skaf83 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(172,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ ( D @ app ) @ app ) @ segmentP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
thf(583,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ ( D @ app ) @ app ) @ segmentP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(143,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ app ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
thf(522,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ app ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(42,axiom,
! [B: $i,A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= nil ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
thf(285,plain,
! [B: $i,A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= nil ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(15,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
thf(223,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(224,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ gt ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ lt ) ) ),
inference(cnf,[status(esa)],[223]) ).
thf(52,axiom,
! [A: $i] : ( A @ skaf57 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
thf(309,plain,
! [A: $i] : ( A @ skaf57 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(6683,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf57 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[309,3704]) ).
thf(6684,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf57 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6683]) ).
thf(6685,plain,
! [A: $i] : ( A @ skaf57 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6684:[bind(A,$thf( C )),bind(B,$thf( C @ skaf57 ))]]) ).
thf(6709,plain,
! [A: $i] : ( A @ skaf57 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6685]) ).
thf(6793,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6582,3704]) ).
thf(6794,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6793]) ).
thf(6795,plain,
sk2 @ ( sk2 @ app ) @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[6794:[bind(A,$thf( sk2 @ ( sk2 @ app ) ))]]) ).
thf(85,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
thf(388,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(177,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
thf(593,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ lt ) )
| ~ ( B @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(165,axiom,
! [A: $i] : ( A @ skaf82 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
thf(571,plain,
! [A: $i] : ( A @ skaf82 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(1736,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf82 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[571,228]) ).
thf(1737,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf82 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1736]) ).
thf(1738,plain,
! [A: $i] :
~ ( A @ skaf82 @ ( A @ skaf82 @ neq ) ),
inference(pattern_uni,[status(thm)],[1737:[bind(A,$thf( C )),bind(B,$thf( C @ skaf82 ))]]) ).
thf(1755,plain,
! [A: $i] :
~ ( A @ skaf82 @ ( A @ skaf82 @ neq ) ),
inference(simp,[status(thm)],[1738]) ).
thf(101,axiom,
! [A: $i] :
( ( nil @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
thf(420,plain,
! [A: $i] :
( ( nil @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(983,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf60 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[398,940]) ).
thf(984,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf60 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[983]) ).
thf(985,plain,
! [A: $i] : ( nil @ ( A @ skaf60 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[984:[bind(A,$thf( C )),bind(B,$thf( C @ skaf60 ))]]) ).
thf(989,plain,
! [A: $i] : ( nil @ ( A @ skaf60 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[985]) ).
thf(61,axiom,
! [A: $i] :
( ( ( A @ ( nil @ app ) )
= A )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
thf(328,plain,
! [A: $i] :
( ( ( A @ ( nil @ app ) )
= A )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(65,axiom,
! [A: $i] : ( A @ skaf58 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
thf(339,plain,
! [A: $i] : ( A @ skaf58 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(9,negated_conjecture,
! [B: $i,A: $i] :
( ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk4 )
| ( ( nil @ ( A @ cons ) @ ( B @ app ) )
= sk3 )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk4 )
| ( ( nil @ ( A @ cons ) @ ( B @ app ) )
= sk3 )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(211,plain,
! [B: $i,A: $i] :
( ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk4 )
| ( ( nil @ ( A @ cons ) @ ( B @ app ) )
= sk3 )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(cnf,[status(esa)],[200]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk4 )
| ( ( nil @ ( A @ cons ) @ ( B @ app ) )
= sk3 ) ),
inference(lifteq,[status(thm)],[211]) ).
thf(6,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
thf(199,plain,
sk1 = sk3,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(210,plain,
sk3 = sk1,
inference(lifteq,[status(thm)],[199]) ).
thf(686,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( nil @ ( A @ cons ) @ app ) )
!= sk2 )
| ( ( nil @ ( A @ cons ) @ ( B @ app ) )
= sk1 ) ),
inference(rewrite,[status(thm)],[212,210,206]) ).
thf(131,axiom,
! [A: $i] : ( A @ skaf67 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
thf(489,plain,
! [A: $i] : ( A @ skaf67 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(176,axiom,
! [B: $i,A: $i] :
( ( ( A @ ( B @ skaf43 ) @ ( B @ cons ) @ ( B @ ( A @ skaf42 ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
thf(590,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ skaf43 ) @ ( B @ cons ) @ ( B @ ( A @ skaf42 ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(155,axiom,
! [A: $i] :
( ( nil = A )
| ( ( A @ skaf82 @ ( A @ skaf83 @ cons ) )
= A )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
thf(547,plain,
! [A: $i] :
( ( nil = A )
| ( ( A @ skaf82 @ ( A @ skaf83 @ cons ) )
= A )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(677,plain,
( ( ( nil @ ( sk2 @ neq ) )
!= ( sk1 @ ( sk1 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,645]) ).
thf(678,plain,
( ( nil @ ( sk2 @ neq ) )
!= ( sk1 @ ( sk1 @ neq ) ) ),
inference(simp,[status(thm)],[677]) ).
thf(679,plain,
( ( nil != sk1 )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[678]) ).
thf(86,axiom,
! [A: $i] : ( A @ skaf70 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
thf(391,plain,
! [A: $i] : ( A @ skaf70 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(941,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf70 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[391,940]) ).
thf(942,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf70 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[941]) ).
thf(943,plain,
! [A: $i] : ( nil @ ( A @ skaf70 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[942:[bind(A,$thf( C )),bind(B,$thf( C @ skaf70 ))]]) ).
thf(970,plain,
! [A: $i] : ( nil @ ( A @ skaf70 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[943]) ).
thf(2123,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf59 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[627,430]) ).
thf(2124,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf59 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[2123]) ).
thf(2125,plain,
! [A: $i] :
~ ( A @ skaf59 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[2124:[bind(A,$thf( C )),bind(B,$thf( C @ skaf59 ))]]) ).
thf(2153,plain,
! [A: $i] :
~ ( A @ skaf59 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[2125]) ).
thf(350,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ app ) )
= nil )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( nil != B )
| ( nil != A ) ),
inference(cnf,[status(esa)],[349]) ).
thf(351,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
= nil )
| ( nil != B )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[350]) ).
thf(352,plain,
( ~ ( nil @ ssList )
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(simp,[status(thm)],[351]) ).
thf(6449,plain,
( ~ $true
| ( ( nil @ ( nil @ app ) )
= nil ) ),
inference(rewrite,[status(thm)],[352,279]) ).
thf(6450,plain,
( ( nil @ ( nil @ app ) )
= nil ),
inference(simp,[status(thm)],[6449]) ).
thf(4031,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf48 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[416,228]) ).
thf(4032,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf48 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[4031]) ).
thf(4033,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf48 ) @ ( B @ ( A @ skaf48 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[4032:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf48 ) ))]]) ).
thf(4069,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf48 ) @ ( B @ ( A @ skaf48 ) @ neq ) ),
inference(simp,[status(thm)],[4033]) ).
thf(77,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
thf(371,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ neq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(183,axiom,
! [A: $i] : ( A @ skaf78 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
thf(605,plain,
! [A: $i] : ( A @ skaf78 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
thf(24,axiom,
! [A: $i] : ( A @ skaf72 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
thf(244,plain,
! [A: $i] : ( A @ skaf72 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(35,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(195,axiom,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
thf(633,plain,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(4,negated_conjecture,
sk4 @ ssList,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
thf(205,plain,
sk4 @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(54,axiom,
! [B: $i,A: $i] :
( ( B @ singletonP )
| ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( nil @ ( A @ cons ) )
!= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
thf(311,plain,
! [B: $i,A: $i] :
( ( B @ singletonP )
| ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( nil @ ( A @ cons ) )
!= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(6565,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf51 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[527,3704]) ).
thf(6566,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf51 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6565]) ).
thf(6567,plain,
! [A: $i] : ( A @ skaf51 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6566:[bind(A,$thf( C )),bind(B,$thf( C @ skaf51 ))]]) ).
thf(6716,plain,
! [A: $i] : ( A @ skaf51 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6567]) ).
thf(174,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( D @ ( C @ cons ) @ ( B @ ( A @ cons ) @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
thf(586,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( D @ ( C @ cons ) @ ( B @ ( A @ cons ) @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(103,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ hd @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ totalorderedP ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
thf(425,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ hd @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ totalorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(88,axiom,
! [A: $i] : ( A @ skaf61 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
thf(394,plain,
! [A: $i] : ( A @ skaf61 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(921,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf61 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[394,228]) ).
thf(922,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf61 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[921]) ).
thf(923,plain,
! [A: $i] :
~ ( A @ skaf61 @ ( A @ skaf61 @ neq ) ),
inference(pattern_uni,[status(thm)],[922:[bind(A,$thf( C )),bind(B,$thf( C @ skaf61 ))]]) ).
thf(931,plain,
! [A: $i] :
~ ( A @ skaf61 @ ( A @ skaf61 @ neq ) ),
inference(simp,[status(thm)],[923]) ).
thf(3601,plain,
! [A: $i] :
( ( ( A @ skaf61 @ ( A @ skaf61 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,931]) ).
thf(3602,plain,
! [A: $i] :
( ( A @ skaf61 @ ( A @ skaf61 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[3601]) ).
thf(3607,plain,
! [A: $i] :
( ( ( A @ skaf61 )
!= nil )
| ( ( A @ skaf61 )
!= sk2 ) ),
inference(simp,[status(thm)],[3602]) ).
thf(46,axiom,
! [A: $i] : ( A @ skaf77 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
thf(296,plain,
! [A: $i] : ( A @ skaf77 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(112,axiom,
! [A: $i] : ( A @ skaf75 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
thf(444,plain,
! [A: $i] : ( A @ skaf75 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(1126,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf75 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[444,228]) ).
thf(1127,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf75 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1126]) ).
thf(1128,plain,
! [A: $i] :
~ ( A @ skaf75 @ ( A @ skaf75 @ neq ) ),
inference(pattern_uni,[status(thm)],[1127:[bind(A,$thf( C )),bind(B,$thf( C @ skaf75 ))]]) ).
thf(1135,plain,
! [A: $i] :
~ ( A @ skaf75 @ ( A @ skaf75 @ neq ) ),
inference(simp,[status(thm)],[1128]) ).
thf(96,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ cons ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
thf(412,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ cons ) @ memberP ) )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ( A @ memberP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(959,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf64 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[263,940]) ).
thf(960,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf64 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[959]) ).
thf(961,plain,
! [A: $i] : ( nil @ ( A @ skaf64 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[960:[bind(A,$thf( C )),bind(B,$thf( C @ skaf64 ))]]) ).
thf(965,plain,
! [A: $i] : ( nil @ ( A @ skaf64 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[961]) ).
thf(1701,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf74 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[570,430]) ).
thf(1702,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf74 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1701]) ).
thf(1703,plain,
! [A: $i] :
~ ( A @ skaf74 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1702:[bind(A,$thf( C )),bind(B,$thf( C @ skaf74 ))]]) ).
thf(1727,plain,
! [A: $i] :
~ ( A @ skaf74 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1703]) ).
thf(188,axiom,
! [B: $i,A: $i] :
( ( nil = A )
| ( A = B )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( A @ hd )
!= ( B @ hd ) )
| ( ( A @ tl )
!= ( B @ tl ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
thf(618,plain,
! [B: $i,A: $i] :
( ( nil = A )
| ( A = B )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( A @ hd )
!= ( B @ hd ) )
| ( ( A @ tl )
!= ( B @ tl ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(787,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf57 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[309,228]) ).
thf(788,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf57 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[787]) ).
thf(789,plain,
! [A: $i] :
~ ( A @ skaf57 @ ( A @ skaf57 @ neq ) ),
inference(pattern_uni,[status(thm)],[788:[bind(A,$thf( C )),bind(B,$thf( C @ skaf57 ))]]) ).
thf(796,plain,
! [A: $i] :
~ ( A @ skaf57 @ ( A @ skaf57 @ neq ) ),
inference(simp,[status(thm)],[789]) ).
thf(2411,plain,
! [A: $i] :
( ( ( A @ skaf57 @ ( A @ skaf57 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,796]) ).
thf(2412,plain,
! [A: $i] :
( ( A @ skaf57 @ ( A @ skaf57 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[2411]) ).
thf(2413,plain,
! [A: $i] :
( ( ( A @ skaf57 )
!= nil )
| ( ( A @ skaf57 )
!= sk2 ) ),
inference(simp,[status(thm)],[2412]) ).
thf(140,axiom,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ frontsegP ) )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
thf(513,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ frontsegP ) )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(170,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D = B )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ( ( B @ ( A @ cons ) )
!= ( D @ ( C @ cons ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
thf(579,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D = B )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ( ( B @ ( A @ cons ) )
!= ( D @ ( C @ cons ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(44,axiom,
nil @ strictorderP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
thf(291,plain,
nil @ strictorderP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(1114,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf53 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[443,228]) ).
thf(1115,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf53 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1114]) ).
thf(1116,plain,
! [A: $i] :
~ ( A @ skaf53 @ ( A @ skaf53 @ neq ) ),
inference(pattern_uni,[status(thm)],[1115:[bind(A,$thf( C )),bind(B,$thf( C @ skaf53 ))]]) ).
thf(1124,plain,
! [A: $i] :
~ ( A @ skaf53 @ ( A @ skaf53 @ neq ) ),
inference(simp,[status(thm)],[1116]) ).
thf(166,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
thf(572,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(235,plain,
! [A: $i] :
( ( A @ strictorderedP )
| ~ ( A @ ssList )
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(cnf,[status(esa)],[234]) ).
thf(1895,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ~ $true
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(paramod_ordered,[status(thm)],[201,235]) ).
thf(1896,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(simp,[status(thm)],[1895]) ).
thf(1897,plain,
( ( sk2 @ strictorderedP )
| ~ ( sk2 @ skaf70 @ ( sk2 @ skaf69 @ lt ) ) ),
inference(pattern_uni,[status(thm)],[1896:[bind(A,$thf( sk2 ))]]) ).
thf(11899,plain,
( ( nil != nil )
| ( sk1 @ cyclefreeP )
| ( sk1 @ tl @ ssList ) ),
inference(paramod_ordered,[status(thm)],[10602,472]) ).
thf(11900,plain,
( ( sk1 @ cyclefreeP )
| ( sk1 @ tl @ ssList ) ),
inference(pattern_uni,[status(thm)],[11899:[]]) ).
thf(755,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf43 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[216,228]) ).
thf(756,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf43 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[755]) ).
thf(757,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf43 ) @ ( B @ ( A @ skaf43 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[756:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf43 ) ))]]) ).
thf(764,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf43 ) @ ( B @ ( A @ skaf43 ) @ neq ) ),
inference(simp,[status(thm)],[757]) ).
thf(37,axiom,
! [A: $i] :
( ( ( A @ skaf68 @ ( A @ skaf65 @ cons ) @ ( A @ skaf67 @ ( A @ skaf64 @ cons ) @ ( A @ skaf66 @ app ) @ app ) )
= A )
| ( A @ totalorderedP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
thf(272,plain,
! [A: $i] :
( ( ( A @ skaf68 @ ( A @ skaf65 @ cons ) @ ( A @ skaf67 @ ( A @ skaf64 @ cons ) @ ( A @ skaf66 @ app ) @ app ) )
= A )
| ( A @ totalorderedP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(273,plain,
! [A: $i] :
( ( ( A @ skaf68 @ ( A @ skaf65 @ cons ) @ ( A @ skaf67 @ ( A @ skaf64 @ cons ) @ ( A @ skaf66 @ app ) @ app ) )
= A )
| ( A @ totalorderedP )
| ~ ( A @ ssList ) ),
inference(cnf,[status(esa)],[272]) ).
thf(274,plain,
! [A: $i] :
( ( A @ totalorderedP )
| ~ ( A @ ssList )
| ( ( A @ skaf68 @ ( A @ skaf65 @ cons ) @ ( A @ skaf67 @ ( A @ skaf64 @ cons ) @ ( A @ skaf66 @ app ) @ app ) )
= A ) ),
inference(lifteq,[status(thm)],[273]) ).
thf(775,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf77 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[296,228]) ).
thf(776,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf77 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[775]) ).
thf(777,plain,
! [A: $i] :
~ ( A @ skaf77 @ ( A @ skaf77 @ neq ) ),
inference(pattern_uni,[status(thm)],[776:[bind(A,$thf( C )),bind(B,$thf( C @ skaf77 ))]]) ).
thf(784,plain,
! [A: $i] :
~ ( A @ skaf77 @ ( A @ skaf77 @ neq ) ),
inference(simp,[status(thm)],[777]) ).
thf(100,axiom,
! [A: $i] : ( A @ skaf49 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
thf(419,plain,
! [A: $i] : ( A @ skaf49 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(735,plain,
( ( sk2 != sk2 )
| ( sk2 != sk1 )
| ~ ( sk2 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[733]) ).
thf(736,plain,
( ( sk2 != sk1 )
| ~ ( sk2 @ ( sk1 @ segmentP ) ) ),
inference(simp,[status(thm)],[735]) ).
thf(25,axiom,
! [A: $i] : ( A @ skaf79 @ ssItem ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
thf(245,plain,
! [A: $i] : ( A @ skaf79 @ ssItem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(49,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
thf(303,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(178,axiom,
! [A: $i] : ( A @ skaf76 @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
thf(595,plain,
! [A: $i] : ( A @ skaf76 @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(2042,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf76 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[595,228]) ).
thf(2043,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf76 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[2042]) ).
thf(2044,plain,
! [A: $i] :
~ ( A @ skaf76 @ ( A @ skaf76 @ neq ) ),
inference(pattern_uni,[status(thm)],[2043:[bind(A,$thf( C )),bind(B,$thf( C @ skaf76 ))]]) ).
thf(2065,plain,
! [A: $i] :
~ ( A @ skaf76 @ ( A @ skaf76 @ neq ) ),
inference(simp,[status(thm)],[2044]) ).
thf(79,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ geq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
thf(377,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ geq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(1931,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ~ $true
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(paramod_ordered,[status(thm)],[198,235]) ).
thf(1932,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ~ ( A @ skaf70 @ ( A @ skaf69 @ lt ) ) ),
inference(simp,[status(thm)],[1931]) ).
thf(1933,plain,
( ( sk1 @ strictorderedP )
| ~ ( sk1 @ skaf70 @ ( sk1 @ skaf69 @ lt ) ) ),
inference(pattern_uni,[status(thm)],[1932:[bind(A,$thf( sk1 ))]]) ).
thf(18,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
thf(230,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(9183,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6620,3704]) ).
thf(9184,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ( A @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[9183]) ).
thf(9185,plain,
nil @ ( sk2 @ app ) @ ( sk2 @ app ) @ ssList,
inference(pattern_uni,[status(thm)],[9184:[bind(A,$thf( nil @ ( sk2 @ app ) ))]]) ).
thf(73,axiom,
! [A: $i] :
( ( A @ totalorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf54 @ ( A @ skaf55 @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
thf(362,plain,
! [A: $i] :
( ( A @ totalorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf54 @ ( A @ skaf55 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(163,axiom,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
thf(567,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(194,axiom,
! [A: $i] :
( ( A @ ( A @ frontsegP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
thf(631,plain,
! [A: $i] :
( ( A @ ( A @ frontsegP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[194]) ).
thf(68,axiom,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
thf(345,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(11,axiom,
skac3 != skac2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
thf(213,plain,
skac3 != skac2,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(189,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ segmentP ) )
| ~ ( B @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
thf(621,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( A @ ( B @ segmentP ) )
| ~ ( B @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(191,axiom,
nil @ totalorderedP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
thf(626,plain,
nil @ totalorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(346,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(cnf,[status(esa)],[345]) ).
thf(347,plain,
! [A: $i] :
( ( A @ ( nil @ rearsegP ) )
| ~ ( A @ ssList )
| ( nil != A ) ),
inference(lifteq,[status(thm)],[346]) ).
thf(348,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ ( nil @ ssList ) ),
inference(simp,[status(thm)],[347]) ).
thf(6003,plain,
( ( nil @ ( nil @ rearsegP ) )
| ~ $true ),
inference(rewrite,[status(thm)],[348,279]) ).
thf(6004,plain,
nil @ ( nil @ rearsegP ),
inference(simp,[status(thm)],[6003]) ).
thf(2408,plain,
! [A: $i] :
( ( ( A @ skaf77 @ ( A @ skaf77 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,784]) ).
thf(2409,plain,
! [A: $i] :
( ( A @ skaf77 @ ( A @ skaf77 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[2408]) ).
thf(2410,plain,
! [A: $i] :
( ( ( A @ skaf77 )
!= nil )
| ( ( A @ skaf77 )
!= sk2 ) ),
inference(simp,[status(thm)],[2409]) ).
thf(6655,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf76 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[595,3704]) ).
thf(6656,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf76 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6655]) ).
thf(6657,plain,
! [A: $i] : ( A @ skaf76 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6656:[bind(A,$thf( C )),bind(B,$thf( C @ skaf76 ))]]) ).
thf(6692,plain,
! [A: $i] : ( A @ skaf76 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6657]) ).
thf(91,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ app ) @ frontsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
thf(399,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ app ) @ frontsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(276,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(cnf,[status(esa)],[275]) ).
thf(277,plain,
! [B: $i,A: $i] :
( ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ neq ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[276]) ).
thf(278,plain,
! [A: $i] :
( ~ ( A @ ssItem )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(6548,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf53 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[443,3704]) ).
thf(6549,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf53 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6548]) ).
thf(6550,plain,
! [A: $i] : ( A @ skaf53 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6549:[bind(A,$thf( C )),bind(B,$thf( C @ skaf53 ))]]) ).
thf(6704,plain,
! [A: $i] : ( A @ skaf53 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6550]) ).
thf(2079,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf78 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[605,430]) ).
thf(2080,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf78 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[2079]) ).
thf(2081,plain,
! [A: $i] :
~ ( A @ skaf78 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[2080:[bind(A,$thf( C )),bind(B,$thf( C @ skaf78 ))]]) ).
thf(2101,plain,
! [A: $i] :
~ ( A @ skaf78 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[2081]) ).
thf(109,axiom,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
thf(438,plain,
! [B: $i,A: $i] :
( ( B = A )
| ( A @ ( B @ neq ) )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(106,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ equalelemsP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
thf(431,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ equalelemsP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(4963,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ~ $true
| ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[201,257]) ).
thf(4964,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ strictorderedP )
| ( ( A @ skaf73 @ ( A @ skaf70 @ cons ) @ ( A @ skaf72 @ ( A @ skaf69 @ cons ) @ ( A @ skaf71 @ app ) @ app ) )
= A ) ),
inference(simp,[status(thm)],[4963]) ).
thf(4965,plain,
( ( sk2 @ strictorderedP )
| ( ( sk2 @ skaf73 @ ( sk2 @ skaf70 @ cons ) @ ( sk2 @ skaf72 @ ( sk2 @ skaf69 @ cons ) @ ( sk2 @ skaf71 @ app ) @ app ) )
= sk2 ) ),
inference(pattern_uni,[status(thm)],[4964:[bind(A,$thf( sk2 ))]]) ).
thf(125,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ leq ) )
| ( D @ ( B @ leq ) )
| ~ ( F @ ssList )
| ~ ( F @ totalorderP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
thf(473,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ leq ) )
| ( D @ ( B @ leq ) )
| ~ ( F @ ssList )
| ~ ( F @ totalorderP )
| ~ ( B @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ~ ( E @ ssList )
| ( ( E @ ( D @ cons ) @ ( C @ ( B @ cons ) @ ( A @ app ) @ app ) )
!= F ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(132,axiom,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf60 @ ( A @ skaf59 @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
thf(490,plain,
! [A: $i] :
( ( A @ strictorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf60 @ ( A @ skaf59 @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(148,axiom,
! [A: $i] :
( ( nil = A )
| ( A @ hd @ ssItem )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
thf(531,plain,
! [A: $i] :
( ( nil = A )
| ( A @ hd @ ssItem )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(78,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= nil ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
thf(374,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= nil ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(67,axiom,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ skaf46 ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
thf(342,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ skaf46 ) @ app ) )
= A )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(861,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf73 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[379,228]) ).
thf(862,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf73 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[861]) ).
thf(863,plain,
! [A: $i] :
~ ( A @ skaf73 @ ( A @ skaf73 @ neq ) ),
inference(pattern_uni,[status(thm)],[862:[bind(A,$thf( C )),bind(B,$thf( C @ skaf73 ))]]) ).
thf(872,plain,
! [A: $i] :
~ ( A @ skaf73 @ ( A @ skaf73 @ neq ) ),
inference(simp,[status(thm)],[863]) ).
thf(2595,plain,
! [A: $i] :
( ( ( A @ skaf73 @ ( A @ skaf73 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,872]) ).
thf(2596,plain,
! [A: $i] :
( ( A @ skaf73 @ ( A @ skaf73 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[2595]) ).
thf(2597,plain,
! [A: $i] :
( ( ( A @ skaf73 )
!= nil )
| ( ( A @ skaf73 )
!= sk2 ) ),
inference(simp,[status(thm)],[2596]) ).
thf(157,axiom,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
thf(553,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(646,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[279,228]) ).
thf(647,plain,
! [A: $i] :
( ( ( nil @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[646]) ).
thf(648,plain,
~ ( nil @ ( nil @ neq ) ),
inference(pattern_uni,[status(thm)],[647:[bind(A,$thf( nil ))]]) ).
thf(953,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf79 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[245,940]) ).
thf(954,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf79 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[953]) ).
thf(955,plain,
! [A: $i] : ( nil @ ( A @ skaf79 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[954:[bind(A,$thf( C )),bind(B,$thf( C @ skaf79 ))]]) ).
thf(968,plain,
! [A: $i] : ( nil @ ( A @ skaf79 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[955]) ).
thf(117,axiom,
! [A: $i] :
( ( A @ totalorderedP )
| ~ ( A @ ssList )
| ~ ( A @ skaf65 @ ( A @ skaf64 @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
thf(458,plain,
! [A: $i] :
( ( A @ totalorderedP )
| ~ ( A @ ssList )
| ~ ( A @ skaf65 @ ( A @ skaf64 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(1787,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf54 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[574,940]) ).
thf(1788,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf54 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1787]) ).
thf(1789,plain,
! [A: $i] : ( nil @ ( A @ skaf54 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1788:[bind(A,$thf( C )),bind(B,$thf( C @ skaf54 ))]]) ).
thf(1798,plain,
! [A: $i] : ( nil @ ( A @ skaf54 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1789]) ).
thf(97,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ frontsegP ) )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( D @ ( C @ cons ) @ ( B @ ( A @ cons ) @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
thf(414,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ frontsegP ) )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( D @ ( C @ cons ) @ ( B @ ( A @ cons ) @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(60,axiom,
nil @ duplicatefreeP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
thf(327,plain,
nil @ duplicatefreeP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(53,axiom,
nil @ equalelemsP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
thf(310,plain,
nil @ equalelemsP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(62,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(110,axiom,
! [A: $i] :
( ( A @ totalorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf55 @ ( A @ skaf54 @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
thf(441,plain,
! [A: $i] :
( ( A @ totalorderP )
| ~ ( A @ ssList )
| ~ ( A @ skaf55 @ ( A @ skaf54 @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(119,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( A @ cons ) )
!= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
thf(463,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( A @ cons ) )
!= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(799,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf58 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[339,228]) ).
thf(800,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf58 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[799]) ).
thf(801,plain,
! [A: $i] :
~ ( A @ skaf58 @ ( A @ skaf58 @ neq ) ),
inference(pattern_uni,[status(thm)],[800:[bind(A,$thf( C )),bind(B,$thf( C @ skaf58 ))]]) ).
thf(808,plain,
! [A: $i] :
~ ( A @ skaf58 @ ( A @ skaf58 @ neq ) ),
inference(simp,[status(thm)],[801]) ).
thf(11968,plain,
( ( nil != nil )
| ( sk1 @ totalorderP )
| ( sk1 @ tl @ ssList ) ),
inference(paramod_ordered,[status(thm)],[10602,467]) ).
thf(11969,plain,
( ( sk1 @ totalorderP )
| ( sk1 @ tl @ ssList ) ),
inference(pattern_uni,[status(thm)],[11968:[]]) ).
thf(1325,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf63 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[534,228]) ).
thf(1326,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf63 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1325]) ).
thf(1327,plain,
! [A: $i] :
~ ( A @ skaf63 @ ( A @ skaf63 @ neq ) ),
inference(pattern_uni,[status(thm)],[1326:[bind(A,$thf( C )),bind(B,$thf( C @ skaf63 ))]]) ).
thf(1336,plain,
! [A: $i] :
~ ( A @ skaf63 @ ( A @ skaf63 @ neq ) ),
inference(simp,[status(thm)],[1327]) ).
thf(6562,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf80 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[428,3704]) ).
thf(6563,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf80 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6562]) ).
thf(6564,plain,
! [A: $i] : ( A @ skaf80 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6563:[bind(A,$thf( C )),bind(B,$thf( C @ skaf80 ))]]) ).
thf(6715,plain,
! [A: $i] : ( A @ skaf80 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6564]) ).
thf(154,axiom,
! [A: $i] :
( ( nil = A )
| ( A @ tl @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
thf(544,plain,
! [A: $i] :
( ( nil = A )
| ( A @ tl @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(141,axiom,
skac2 @ ssItem,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
thf(517,plain,
skac2 @ ssItem,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(671,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ~ $true
| ~ ( A @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[517,430]) ).
thf(672,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[671]) ).
thf(673,plain,
~ ( skac2 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[672:[bind(A,$thf( skac2 ))]]) ).
thf(137,axiom,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ cons ) @ memberP ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
thf(502,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ cons ) @ memberP ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssList )
| ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(1850,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf56 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[582,228]) ).
thf(1851,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf56 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1850]) ).
thf(1852,plain,
! [A: $i] :
~ ( A @ skaf56 @ ( A @ skaf56 @ neq ) ),
inference(pattern_uni,[status(thm)],[1851:[bind(A,$thf( C )),bind(B,$thf( C @ skaf56 ))]]) ).
thf(1869,plain,
! [A: $i] :
~ ( A @ skaf56 @ ( A @ skaf56 @ neq ) ),
inference(simp,[status(thm)],[1852]) ).
thf(123,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ cyclefreeP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
thf(470,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ cyclefreeP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(169,axiom,
! [B: $i,A: $i] :
( ( ( A @ ( B @ app ) @ hd )
= ( B @ hd ) )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ app ) @ hd )
= ( B @ hd ) )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(740,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf79 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[245,430]) ).
thf(741,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf79 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[740]) ).
thf(742,plain,
! [A: $i] :
~ ( A @ skaf79 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[741:[bind(A,$thf( C )),bind(B,$thf( C @ skaf79 ))]]) ).
thf(744,plain,
! [A: $i] :
~ ( A @ skaf79 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[742]) ).
thf(64,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ totalorderedP )
| ~ ( B @ hd @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
thf(336,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ ( A @ cons ) @ totalorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ totalorderedP )
| ~ ( B @ hd @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(186,axiom,
nil @ strictorderedP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
thf(613,plain,
nil @ strictorderedP,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[186]) ).
thf(181,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ cons ) @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
thf(600,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cons ) @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(1769,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf54 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[574,430]) ).
thf(1770,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf54 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1769]) ).
thf(1771,plain,
! [A: $i] :
~ ( A @ skaf54 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1770:[bind(A,$thf( C )),bind(B,$thf( C @ skaf54 ))]]) ).
thf(1797,plain,
! [A: $i] :
~ ( A @ skaf54 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1771]) ).
thf(2509,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ duplicatefreeP )
| ~ $true
| ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[198,243]) ).
thf(2510,plain,
! [A: $i] :
( ( ( sk1 @ ssList )
!= ( A @ ssList ) )
| ( A @ duplicatefreeP )
| ( ( A @ skaf77 @ ( A @ skaf74 @ cons ) @ ( A @ skaf76 @ ( A @ skaf74 @ cons ) @ ( A @ skaf75 @ app ) @ app ) )
= A ) ),
inference(simp,[status(thm)],[2509]) ).
thf(2511,plain,
( ( sk1 @ duplicatefreeP )
| ( ( sk1 @ skaf77 @ ( sk1 @ skaf74 @ cons ) @ ( sk1 @ skaf76 @ ( sk1 @ skaf74 @ cons ) @ ( sk1 @ skaf75 @ app ) @ app ) )
= sk1 ) ),
inference(pattern_uni,[status(thm)],[2510:[bind(A,$thf( sk1 ))]]) ).
thf(1813,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf65 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[575,430]) ).
thf(1814,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf65 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1813]) ).
thf(1815,plain,
! [A: $i] :
~ ( A @ skaf65 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1814:[bind(A,$thf( C )),bind(B,$thf( C @ skaf65 ))]]) ).
thf(1839,plain,
! [A: $i] :
~ ( A @ skaf65 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1815]) ).
thf(158,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ totalorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ totalorderedP ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
thf(556,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ totalorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ ( A @ cons ) @ totalorderedP ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(3,negated_conjecture,
sk3 @ ssList,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
thf(203,plain,
sk3 @ ssList,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(144,axiom,
! [B: $i,A: $i] :
( ( ( A @ ( B @ app ) @ tl )
= ( A @ ( B @ tl @ app ) ) )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
thf(524,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ app ) @ tl )
= ( A @ ( B @ tl @ app ) ) )
| ( nil = B )
| ~ ( B @ ssList )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ geq ) )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[217]) ).
thf(231,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ lt ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( C @ ( B @ lt ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[230]) ).
thf(152,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ( ( B @ ( A @ cons ) )
!= ( D @ ( C @ cons ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
thf(539,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( B @ ssList )
| ~ ( D @ ssList )
| ~ ( A @ ssItem )
| ~ ( C @ ssItem )
| ( ( B @ ( A @ cons ) )
!= ( D @ ( C @ cons ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(1003,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf49 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[419,940]) ).
thf(1004,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf49 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1003]) ).
thf(1005,plain,
! [A: $i] : ( nil @ ( A @ skaf49 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1004:[bind(A,$thf( C )),bind(B,$thf( C @ skaf49 ))]]) ).
thf(1010,plain,
! [A: $i] : ( nil @ ( A @ skaf49 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1005]) ).
thf(9139,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[6620,228]) ).
thf(9140,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[9139]) ).
thf(9141,plain,
~ ( nil @ ( sk2 @ app ) @ ( nil @ ( sk2 @ app ) @ neq ) ),
inference(pattern_uni,[status(thm)],[9140:[bind(A,$thf( nil @ ( sk2 @ app ) ))]]) ).
thf(56,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
thf(319,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(92,axiom,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ strictorderedP )
| ~ ( B @ hd @ ( A @ lt ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
thf(401,plain,
! [B: $i,A: $i] :
( ( nil = B )
| ( B @ ( A @ cons ) @ strictorderedP )
| ~ ( A @ ssItem )
| ~ ( B @ ssList )
| ~ ( B @ strictorderedP )
| ~ ( B @ hd @ ( A @ lt ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(6659,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf81 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[495,3704]) ).
thf(6660,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf81 @ ssList )
!= ( B @ ssList ) )
| ( B @ ( sk2 @ app ) @ ssList ) ),
inference(simp,[status(thm)],[6659]) ).
thf(6661,plain,
! [A: $i] : ( A @ skaf81 @ ( sk2 @ app ) @ ssList ),
inference(pattern_uni,[status(thm)],[6660:[bind(A,$thf( C )),bind(B,$thf( C @ skaf81 ))]]) ).
thf(6694,plain,
! [A: $i] : ( A @ skaf81 @ ( sk2 @ app ) @ ssList ),
inference(simp,[status(thm)],[6661]) ).
thf(1379,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf83 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[566,940]) ).
thf(1380,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf83 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[1379]) ).
thf(1381,plain,
! [A: $i] : ( nil @ ( A @ skaf83 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[1380:[bind(A,$thf( C )),bind(B,$thf( C @ skaf83 ))]]) ).
thf(1385,plain,
! [A: $i] : ( nil @ ( A @ skaf83 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[1381]) ).
thf(2592,plain,
! [A: $i] :
( ( ( A @ skaf58 @ ( A @ skaf58 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,808]) ).
thf(2593,plain,
! [A: $i] :
( ( A @ skaf58 @ ( A @ skaf58 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[2592]) ).
thf(2594,plain,
! [A: $i] :
( ( ( A @ skaf58 )
!= nil )
| ( ( A @ skaf58 )
!= sk2 ) ),
inference(simp,[status(thm)],[2593]) ).
thf(944,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[517,940]) ).
thf(945,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ( nil @ ( A @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[944]) ).
thf(946,plain,
nil @ ( skac2 @ cons ) @ totalorderedP,
inference(pattern_uni,[status(thm)],[945:[bind(A,$thf( skac2 ))]]) ).
thf(1979,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf50 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[585,430]) ).
thf(1980,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf50 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1979]) ).
thf(1981,plain,
! [A: $i] :
~ ( A @ skaf50 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1980:[bind(A,$thf( C )),bind(B,$thf( C @ skaf50 ))]]) ).
thf(2009,plain,
! [A: $i] :
~ ( A @ skaf50 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1981]) ).
thf(127,axiom,
! [B: $i,A: $i] : ( B @ ( A @ skaf47 ) @ ssList ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
thf(478,plain,
! [B: $i,A: $i] : ( B @ ( A @ skaf47 ) @ ssList ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(82,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( A @ cons ) )
!= nil ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
thf(383,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssList )
| ~ ( A @ ssItem )
| ( ( B @ ( A @ cons ) )
!= nil ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(151,axiom,
! [C: $i,B: $i,A: $i] :
( ( B = C )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= ( C @ ( A @ app ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
thf(536,plain,
! [C: $i,B: $i,A: $i] :
( ( B = C )
| ~ ( C @ ssList )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( ( B @ ( A @ app ) )
!= ( C @ ( A @ app ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(107,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ segmentP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ segmentP ) )
| ~ ( B @ ( A @ segmentP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
thf(433,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ segmentP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ segmentP ) )
| ~ ( B @ ( A @ segmentP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(139,axiom,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ app ) @ ( A @ cons ) )
= ( C @ ( B @ ( A @ cons ) @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
thf(510,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ app ) @ ( A @ cons ) )
= ( C @ ( B @ ( A @ cons ) @ app ) ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(48,axiom,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ rearsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
thf(300,plain,
! [A: $i] :
( ( nil = A )
| ~ ( A @ ssList )
| ~ ( A @ ( nil @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(2097,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf78 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[605,940]) ).
thf(2098,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf78 @ ssItem )
!= ( B @ ssItem ) )
| ( nil @ ( B @ cons ) @ totalorderedP ) ),
inference(simp,[status(thm)],[2097]) ).
thf(2099,plain,
! [A: $i] : ( nil @ ( A @ skaf78 @ cons ) @ totalorderedP ),
inference(pattern_uni,[status(thm)],[2098:[bind(A,$thf( C )),bind(B,$thf( C @ skaf78 ))]]) ).
thf(2102,plain,
! [A: $i] : ( nil @ ( A @ skaf78 @ cons ) @ totalorderedP ),
inference(simp,[status(thm)],[2099]) ).
thf(55,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ rearsegP ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
!= C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
thf(315,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ rearsegP ) )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
!= C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(102,axiom,
! [A: $i] :
( ( nil = A )
| ( A @ hd @ ssItem )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
thf(422,plain,
! [A: $i] :
( ( nil = A )
| ( A @ hd @ ssItem )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(95,axiom,
! [A: $i] :
( ( A @ skaf49 @ ( A @ skaf50 @ leq ) )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
thf(410,plain,
! [A: $i] :
( ( A @ skaf49 @ ( A @ skaf50 @ leq ) )
| ( A @ cyclefreeP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(161,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ rearsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ rearsegP ) )
| ~ ( B @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
thf(564,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ rearsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( C @ ( B @ rearsegP ) )
| ~ ( B @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(50,axiom,
! [B: $i,A: $i] :
( ( B @ ssItem )
| ( A @ duplicatefreeP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
thf(305,plain,
! [B: $i,A: $i] :
( ( B @ ssItem )
| ( A @ duplicatefreeP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(914,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf70 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[391,430]) ).
thf(915,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf70 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[914]) ).
thf(916,plain,
! [A: $i] :
~ ( A @ skaf70 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[915:[bind(A,$thf( C )),bind(B,$thf( C @ skaf70 ))]]) ).
thf(918,plain,
! [A: $i] :
~ ( A @ skaf70 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[916]) ).
thf(2184,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[201,237]) ).
thf(2185,plain,
! [A: $i] :
( ( ( sk2 @ ssList )
!= ( A @ ssList ) )
| ( A @ skaf50 @ ( A @ skaf49 @ leq ) )
| ( A @ cyclefreeP ) ),
inference(simp,[status(thm)],[2184]) ).
thf(2186,plain,
( ( sk2 @ skaf50 @ ( sk2 @ skaf49 @ leq ) )
| ( sk2 @ cyclefreeP ) ),
inference(pattern_uni,[status(thm)],[2185:[bind(A,$thf( sk2 ))]]) ).
thf(72,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ cons ) @ ( A @ ( C @ cons ) @ frontsegP ) )
| ~ ( C @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( C != D )
| ~ ( B @ ( A @ frontsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
thf(358,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ cons ) @ ( A @ ( C @ cons ) @ frontsegP ) )
| ~ ( C @ ssItem )
| ~ ( D @ ssItem )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ( C != D )
| ~ ( B @ ( A @ frontsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(9248,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[6638,228]) ).
thf(9249,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ app ) @ ssList )
!= ( A @ ssList ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[9248]) ).
thf(9250,plain,
~ ( sk1 @ ( sk2 @ app ) @ ( sk1 @ ( sk2 @ app ) @ neq ) ),
inference(pattern_uni,[status(thm)],[9249:[bind(A,$thf( sk1 @ ( sk2 @ app ) ))]]) ).
thf(882,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf69 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[386,430]) ).
thf(883,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf69 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[882]) ).
thf(884,plain,
! [A: $i] :
~ ( A @ skaf69 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[883:[bind(A,$thf( C )),bind(B,$thf( C @ skaf69 ))]]) ).
thf(886,plain,
! [A: $i] :
~ ( A @ skaf69 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[884]) ).
thf(4104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf47 ) @ ssList )
!= ( C @ ssList ) )
| ~ $true
| ~ ( C @ ( C @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[478,228]) ).
thf(4105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ skaf47 ) @ ssList )
!= ( C @ ssList ) )
| ~ ( C @ ( C @ neq ) ) ),
inference(simp,[status(thm)],[4104]) ).
thf(4106,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf47 ) @ ( B @ ( A @ skaf47 ) @ neq ) ),
inference(pattern_uni,[status(thm)],[4105:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ skaf47 ) ))]]) ).
thf(4146,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ skaf47 ) @ ( B @ ( A @ skaf47 ) @ neq ) ),
inference(simp,[status(thm)],[4106]) ).
thf(138,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ memberP ) )
| ~ ( D @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ( ( C @ ( B @ cons ) @ ( A @ app ) )
!= D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
thf(506,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ memberP ) )
| ~ ( D @ ssList )
| ~ ( B @ ssItem )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ( ( C @ ( B @ cons ) @ ( A @ app ) )
!= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(267,plain,
! [B: $i,A: $i] :
( ( B = A )
| ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) ) ),
inference(cnf,[status(esa)],[266]) ).
thf(268,plain,
! [B: $i,A: $i] :
( ~ ( B @ ssItem )
| ~ ( A @ ssItem )
| ~ ( A @ ( B @ geq ) )
| ~ ( B @ ( A @ geq ) )
| ( B = A ) ),
inference(lifteq,[status(thm)],[267]) ).
thf(1162,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf67 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[489,228]) ).
thf(1163,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf67 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[1162]) ).
thf(1164,plain,
! [A: $i] :
~ ( A @ skaf67 @ ( A @ skaf67 @ neq ) ),
inference(pattern_uni,[status(thm)],[1163:[bind(A,$thf( C )),bind(B,$thf( C @ skaf67 ))]]) ).
thf(1172,plain,
! [A: $i] :
~ ( A @ skaf67 @ ( A @ skaf67 @ neq ) ),
inference(simp,[status(thm)],[1164]) ).
thf(2416,plain,
! [A: $i] :
( ( ( nil @ ( sk2 @ skaf44 @ cons ) )
!= ( nil @ ( A @ skaf44 @ cons ) ) )
| ( sk2 @ totalorderedP )
| ~ ( sk2 @ singletonP ) ),
inference(paramod_ordered,[status(thm)],[2306,967]) ).
thf(2417,plain,
( ( sk2 @ totalorderedP )
| ~ ( sk2 @ singletonP ) ),
inference(pattern_uni,[status(thm)],[2416:[bind(A,$thf( sk2 ))]]) ).
thf(41,axiom,
! [A: $i] :
( ( nil @ ( A @ rearsegP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
thf(283,plain,
! [A: $i] :
( ( nil @ ( A @ rearsegP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(719,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf72 @ ssList )
!= ( B @ ssList ) )
| ~ $true
| ~ ( B @ ( B @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[244,228]) ).
thf(720,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf72 @ ssList )
!= ( B @ ssList ) )
| ~ ( B @ ( B @ neq ) ) ),
inference(simp,[status(thm)],[719]) ).
thf(721,plain,
! [A: $i] :
~ ( A @ skaf72 @ ( A @ skaf72 @ neq ) ),
inference(pattern_uni,[status(thm)],[720:[bind(A,$thf( C )),bind(B,$thf( C @ skaf72 ))]]) ).
thf(728,plain,
! [A: $i] :
~ ( A @ skaf72 @ ( A @ skaf72 @ neq ) ),
inference(simp,[status(thm)],[721]) ).
thf(1361,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf83 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[566,430]) ).
thf(1362,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf83 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1361]) ).
thf(1363,plain,
! [A: $i] :
~ ( A @ skaf83 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1362:[bind(A,$thf( C )),bind(B,$thf( C @ skaf83 ))]]) ).
thf(1384,plain,
! [A: $i] :
~ ( A @ skaf83 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1363]) ).
thf(146,axiom,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderP )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
thf(528,plain,
! [A: $i] :
( ( nil @ ( A @ cons ) @ strictorderP )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(818,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf44 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[353,430]) ).
thf(819,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf44 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[818]) ).
thf(820,plain,
! [A: $i] :
~ ( A @ skaf44 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[819:[bind(A,$thf( C )),bind(B,$thf( C @ skaf44 ))]]) ).
thf(822,plain,
! [A: $i] :
~ ( A @ skaf44 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[820]) ).
thf(2268,plain,
! [A: $i] :
( ( ( A @ skaf72 @ ( A @ skaf72 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[202,728]) ).
thf(2269,plain,
! [A: $i] :
( ( A @ skaf72 @ ( A @ skaf72 @ neq ) )
!= ( nil @ ( sk2 @ neq ) ) ),
inference(simp,[status(thm)],[2268]) ).
thf(2270,plain,
! [A: $i] :
( ( ( A @ skaf72 )
!= nil )
| ( ( A @ skaf72 )
!= sk2 ) ),
inference(simp,[status(thm)],[2269]) ).
thf(89,axiom,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
!= ( B @ ( C @ app ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
thf(395,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ~ ( C @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ( ( B @ ( A @ app ) )
!= ( B @ ( C @ app ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(13260,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[530,278]) ).
thf(13261,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[13260]) ).
thf(13262,plain,
~ ( skac3 @ ( skac3 @ neq ) ),
inference(pattern_uni,[status(thm)],[13261:[bind(A,$thf( skac3 ))]]) ).
thf(190,axiom,
! [A: $i] :
( ( A @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
thf(624,plain,
! [A: $i] :
( ( A @ ( A @ segmentP ) )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(76,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ app ) @ rearsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ rearsegP ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
thf(369,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( C @ app ) @ rearsegP ) )
| ~ ( A @ ssList )
| ~ ( B @ ssList )
| ~ ( C @ ssList )
| ~ ( B @ ( A @ rearsegP ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(254,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( A @ ssItem )
| ~ ( B @ ssItem )
| ~ ( B @ ( A @ geq ) ) ),
inference(cnf,[status(esa)],[253]) ).
thf(58,axiom,
! [A: $i] :
( ( ( A @ skaf58 @ ( A @ skaf55 @ cons ) @ ( A @ skaf57 @ ( A @ skaf54 @ cons ) @ ( A @ skaf56 @ app ) @ app ) )
= A )
| ( A @ totalorderP )
| ~ ( A @ ssList ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
thf(322,plain,
! [A: $i] :
( ( ( A @ skaf58 @ ( A @ skaf55 @ cons ) @ ( A @ skaf57 @ ( A @ skaf54 @ cons ) @ ( A @ skaf56 @ app ) @ app ) )
= A )
| ( A @ totalorderP )
| ~ ( A @ ssList ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(71,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ~ ( E @ ssList )
| ~ ( E @ equalelemsP )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( D @ ssList )
| ( ( D @ ( C @ cons ) @ ( B @ cons ) @ ( A @ app ) )
!= E ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
thf(354,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ~ ( E @ ssList )
| ~ ( E @ equalelemsP )
| ~ ( B @ ssItem )
| ~ ( C @ ssItem )
| ~ ( A @ ssList )
| ~ ( D @ ssList )
| ( ( D @ ( C @ cons ) @ ( B @ cons ) @ ( A @ app ) )
!= E ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(214,plain,
skac3 != skac2,
inference(polarity_switch,[status(thm)],[213]) ).
thf(215,plain,
skac2 != skac3,
inference(lifteq,[status(thm)],[214]) ).
thf(674,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ~ $true
| ~ ( A @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[530,430]) ).
thf(675,plain,
! [A: $i] :
( ( ( skac3 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[674]) ).
thf(676,plain,
~ ( skac3 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[675:[bind(A,$thf( skac3 ))]]) ).
thf(135,axiom,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ segmentP ) )
| ~ ( D @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ( ( C @ ( B @ ( A @ app ) @ app ) )
!= D ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
thf(496,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ segmentP ) )
| ~ ( D @ ssList )
| ~ ( B @ ssList )
| ~ ( A @ ssList )
| ~ ( C @ ssList )
| ( ( C @ ( B @ ( A @ app ) @ app ) )
!= D ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(74,axiom,
! [A: $i] :
( ( A @ ( A @ geq ) )
| ~ ( A @ ssItem ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
thf(364,plain,
! [A: $i] :
( ( A @ ( A @ geq ) )
| ~ ( A @ ssItem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(13287,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ~ $true
| ~ ( A @ ( A @ neq ) ) ),
inference(paramod_ordered,[status(thm)],[517,278]) ).
thf(13288,plain,
! [A: $i] :
( ( ( skac2 @ ssItem )
!= ( A @ ssItem ) )
| ~ ( A @ ( A @ neq ) ) ),
inference(simp,[status(thm)],[13287]) ).
thf(13289,plain,
~ ( skac2 @ ( skac2 @ neq ) ),
inference(pattern_uni,[status(thm)],[13288:[bind(A,$thf( skac2 ))]]) ).
thf(1000,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf49 @ ssItem )
!= ( B @ ssItem ) )
| ~ $true
| ~ ( B @ ( nil @ memberP ) ) ),
inference(paramod_ordered,[status(thm)],[419,430]) ).
thf(1001,plain,
! [B: $i,A: $i] :
( ( ( A @ skaf49 @ ssItem )
!= ( B @ ssItem ) )
| ~ ( B @ ( nil @ memberP ) ) ),
inference(simp,[status(thm)],[1000]) ).
thf(1002,plain,
! [A: $i] :
~ ( A @ skaf49 @ ( nil @ memberP ) ),
inference(pattern_uni,[status(thm)],[1001:[bind(A,$thf( C )),bind(B,$thf( C @ skaf49 ))]]) ).
thf(1009,plain,
! [A: $i] :
~ ( A @ skaf49 @ ( nil @ memberP ) ),
inference(simp,[status(thm)],[1002]) ).
thf(23240,plain,
$false,
inference(e,[status(thm)],[645,1322,2306,12564,479,1840,518,468,234,6014,249,333,628,582,217,1728,449,379,614,269,202,597,2607,1310,550,500,472,3616,814,340,670,404,417,288,2010,6754,257,570,751,6434,196,542,460,902,559,1147,325,228,261,969,606,1347,12621,416,492,4018,443,253,485,238,10602,2222,216,3966,4583,321,2469,1020,574,353,966,602,280,734,774,1351,988,243,428,265,2154,527,206,307,292,248,380,201,366,534,233,452,952,349,561,392,297,407,429,275,2032,6620,6582,467,252,197,435,11980,1159,9291,456,229,566,484,583,522,285,224,6709,6795,3704,388,593,1755,420,989,328,225,339,686,642,489,590,547,679,970,2153,654,6450,4069,371,605,237,244,266,633,205,311,6716,398,530,586,425,3607,264,279,296,444,1135,412,965,1727,618,2413,513,430,732,579,291,1124,204,391,445,572,236,1897,11841,11900,466,6638,764,2346,219,274,784,419,736,245,303,271,2065,377,1933,230,9185,362,567,477,631,345,535,609,213,621,483,626,387,6004,240,251,2410,198,6692,399,278,223,394,6704,2101,438,431,241,4965,473,490,589,531,663,374,255,342,2597,553,648,209,968,458,1798,872,414,327,263,310,331,441,585,463,808,11969,1336,6715,544,199,673,502,1869,470,576,744,336,613,600,1797,571,595,386,2511,1839,627,556,203,524,495,218,250,231,931,539,1010,9141,517,319,401,6694,1385,2594,946,258,2009,478,272,383,536,716,235,246,433,510,300,2102,315,262,422,410,967,564,305,918,2186,358,9250,886,210,4146,506,268,1172,2417,796,283,728,575,1384,528,822,200,2270,395,13262,624,11794,596,11803,369,254,322,940,354,309,215,676,496,364,232,13289,1009]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC088-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.40 % Computer : n016.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sat Sep 26 12:18:01 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.26/1.26 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.53/1.71 % [INFO] Parsing done (450ms).
% 2.53/1.73 % [INFO] Running in sequential loop mode.
% 3.82/2.33 % [INFO] eprover registered as external prover.
% 3.82/2.35 % [INFO] Scanning for conjecture ...
% 4.21/2.56 % [INFO] Found a conjecture (or negated_conjecture) and 185 axioms. Running axiom selection ...
% 4.67/2.77 % [INFO] Axiom selection finished. Selected 185 axioms (removed 0 axioms).
% 5.27/2.99 % [INFO] Problem is propositional (TPTP CNF).
% 5.27/3.02 % [INFO] Type checking passed.
% 5.27/3.03 % [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 ...
% 106.66/24.03 % External prover 'e' found a proof!
% 106.66/24.03 % [INFO] Killing All external provers ...
% 106.66/24.03 % Time passed: 23421ms (effective reasoning time: 22290ms)
% 106.66/24.04 % Axioms used in derivation (185): clause144, clause82, clause60, clause65, clause128, clause171, clause71, clause113, clause139, clause3, clause29, clause160, clause43, clause32, clause18, clause54, clause117, clause88, clause59, clause99, clause48, clause146, clause37, clause165, clause108, clause93, clause105, clause185, clause77, clause135, clause95, clause101, clause168, clause129, clause81, clause55, clause164, clause154, clause66, clause17, clause70, clause118, clause181, clause22, clause124, clause92, clause157, clause87, clause84, clause7, clause25, clause11, clause14, clause112, clause76, clause130, clause49, clause169, clause13, clause31, clause24, clause132, clause121, clause42, clause109, clause104, clause2, clause158, clause141, clause143, clause64, clause166, clause38, clause16, clause28, clause98, clause53, clause176, clause152, clause170, clause155, clause136, clause12, clause179, clause111, clause79, clause97, clause147, clause180, clause163, clause75, clause125, clause100, clause23, clause114, clause6, clause174, clause86, clause184, clause133, clause122, clause103, clause1, clause151, clause167, clause34, clause159, clause140, clause177, clause5, clause69, clause68, clause148, clause134, clause27, clause110, clause41, clause39, clause173, clause57, clause162, clause137, clause35, clause8, clause183, clause30, clause145, clause20, clause52, clause46, clause156, clause90, clause126, clause115, clause63, clause89, clause44, clause50, clause150, clause102, clause182, clause72, clause33, clause94, clause73, clause83, clause175, clause107, clause19, clause123, clause178, clause78, clause116, clause4, clause26, clause149, clause58, clause96, clause172, clause142, clause9, clause131, clause120, clause80, clause56, clause10, clause161, clause67, clause138, clause21, clause127, clause119, clause15, clause153, clause45, clause40, clause85, clause91, clause51, clause106, clause61, clause62, clause74, clause47, clause36
% 106.66/24.04 % No. of inferences in proof: 878
% 106.66/24.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 23421 ms resp. 22290 ms w/o parsing
% 112.58/24.40 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 112.58/24.41 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------