%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 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 : n007.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:00:52 AM UTC 2026
% Result : Theorem 89.23s 19.46s
% Output : Refutation 75.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 39
% Syntax : Number of formulae : 587 ( 95 unt; 0 typ; 6 def)
% Number of atoms : 1930 ( 464 equ; 0 cnn)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 5325 ( 999 ~; 872 |; 125 &;3271 @)
% ( 8 <=>; 50 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 24 ( 21 usr; 10 con; 0-4 aty)
% Number of variables : 831 ( 12 ^; 787 !; 26 ?; 831 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% Comments :
%------------------------------------------------------------------------------
thf(in_lopen_decl,type,
in_lopen: $i > $i > $i > $o ).
thf(v0_decl,type,
v0: $i ).
thf(v200_decl,type,
v200: $i ).
thf(v100_decl,type,
v100: $i ).
thf(v50_decl,type,
v50: $i ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(v400_decl,type,
v400: $i ).
thf(axis_conflict_decl,type,
axis_conflict: $i > $i > $i > $i > $o ).
thf(in_closed_decl,type,
in_closed: $i > $i > $i > $o ).
thf(less_decl,type,
less: $i > $i > $o ).
thf(axis_compatible_decl,type,
axis_compatible: $i > $i > $i > $i > $o ).
thf(axis_subsumes_decl,type,
axis_subsumes: $i > $i > $i > $i > $o ).
thf(in_open_decl,type,
in_open: $i > $i > $i > $o ).
thf(in_ropen_decl,type,
in_ropen: $i > $i > $i > $o ).
thf(val_decl,type,
val: $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 > $i > $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
? [B: $i,C: $i] :
( ( C @ ( v100 @ leq ) )
& ( B @ ( v200 @ leq ) )
& ( A @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( C @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( A @ in_lopen ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
? [B: $i] :
( ( B @ ( v100 @ leq ) )
& ( A @ ( v200 @ leq ) )
& ( sk1 @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( A @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
( ( A @ ( v100 @ leq ) )
& ( sk2 @ ( v200 @ leq ) )
& ( sk1 @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( A @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ( A @ ( B @ ( E @ in_closed ) ) )
& ( C @ ( D @ ( E @ in_closed ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ( A @ ( B @ ( E @ in_closed ) ) )
& ( C @ ( D @ ( E @ in_closed ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
~ ( ( C @ ( D @ ( E @ in_closed ) ) )
=> ( A @ ( B @ ( E @ in_closed ) ) ) ) ) ) ).
thf(7,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
<=> ! [E: $i] :
( ( B @ ( A @ ( E @ in_closed ) ) )
=> ( D @ ( C @ ( E @ in_closed ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axis_subsumes_def) ).
thf(63,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ! [E: $i] :
( ( B @ ( A @ ( E @ in_closed ) ) )
=> ( D @ ( C @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
=> ! [E: $i] :
( ( B @ ( A @ ( E @ in_closed ) ) )
=> ( D @ ( C @ ( E @ in_closed ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(64,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ! [E: $i] :
( ( B @ ( A @ ( E @ in_closed ) ) )
=> ( D @ ( C @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
=> ! [E: $i] :
( ( B @ ( A @ ( E @ in_closed ) ) )
=> ( D @ ( C @ ( E @ in_closed ) ) ) ) ) ),
inference(miniscope,[status(thm)],[63]) ).
thf(65,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( I @ ( H @ ( G @ ( F @ axis_subsumes ) ) ) )
| ~ ( I @ ( H @ ( F @ ( G @ ( H @ ( I @ sk6 ) ) ) @ in_closed ) ) ) )
& ( ( I @ ( H @ ( G @ ( F @ axis_subsumes ) ) ) )
| ( G @ ( F @ ( F @ ( G @ ( H @ ( I @ sk6 ) ) ) @ in_closed ) ) ) )
& ( ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) ) ),
inference(cnf,[status(esa)],[64]) ).
thf(67,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[65]) ).
thf(69,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(1,conjecture,
~ ? [A: $i,B: $i,C: $i] :
( ( C @ ( v100 @ leq ) )
& ( B @ ( v200 @ leq ) )
& ( A @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( C @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( A @ in_lopen ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',odrl445) ).
thf(2,negated_conjecture,
~ ~ ? [A: $i,B: $i,C: $i] :
( ( C @ ( v100 @ leq ) )
& ( B @ ( v200 @ leq ) )
& ( A @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( C @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( A @ in_lopen ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(35,plain,
~ ~ ? [A: $i,B: $i,C: $i] :
( ( C @ ( v100 @ leq ) )
& ( B @ ( v200 @ leq ) )
& ( A @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( C @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( A @ in_lopen ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(36,plain,
? [A: $i,B: $i,C: $i] :
( ( C @ ( v100 @ leq ) )
& ( B @ ( v200 @ leq ) )
& ( A @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( C @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( B @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( A @ in_lopen ) ) ) ) ),
inference(polarity_switch,[status(thm)],[35]) ).
thf(37,plain,
( ( sk3 @ ( v100 @ leq ) )
& ( sk2 @ ( v200 @ leq ) )
& ( sk1 @ ( v400 @ leq ) )
& ( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ) ),
inference(cnf,[status(esa)],[36]) ).
thf(39,plain,
sk1 @ ( v400 @ leq ),
inference(cnfConj,[status(thm)],[37]) ).
thf(16,axiom,
! [A: $i,B: $i] :
( ( ( A @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_antisym) ).
thf(108,plain,
! [A: $i,B: $i] :
( ( ( A @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[108]) ).
thf(110,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[109]) ).
thf(12,axiom,
( ( v200 != v400 )
& ( v100 != v400 )
& ( v100 != v200 )
& ( v50 != v400 )
& ( v50 != v200 )
& ( v50 != v100 )
& ( v0 != v400 )
& ( v0 != v200 )
& ( v0 != v100 )
& ( v0 != v50 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distinct) ).
thf(83,plain,
( ( v200 != v400 )
& ( v100 != v400 )
& ( v100 != v200 )
& ( v50 != v400 )
& ( v50 != v200 )
& ( v50 != v100 )
& ( v0 != v400 )
& ( v0 != v200 )
& ( v0 != v100 )
& ( v0 != v50 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(84,plain,
( ( v200 != v400 )
& ( v100 != v400 )
& ( v100 != v200 )
& ( v50 != v400 )
& ( v50 != v200 )
& ( v50 != v100 )
& ( v0 != v400 )
& ( v0 != v200 )
& ( v0 != v100 )
& ( v0 != v50 ) ),
inference(cnf,[status(esa)],[83]) ).
thf(88,plain,
v200 != v400,
inference(cnfConj,[status(thm)],[84]) ).
thf(95,plain,
v400 != v200,
inference(lifteq,[status(thm)],[88]) ).
thf(290,plain,
! [B: $i,A: $i] :
( ( A != v400 )
| ( B != v200 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,95]) ).
thf(291,plain,
! [A: $i] :
( ( A != v200 )
| ~ ( v400 @ ( A @ leq ) )
| ~ ( A @ ( v400 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[290:[bind(A,$thf( v400 ))]]) ).
thf(331,plain,
( ~ ( v400 @ ( v200 @ leq ) )
| ~ ( v200 @ ( v400 @ leq ) ) ),
inference(simp,[status(thm)],[291]) ).
thf(1083,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v200 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v200 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39,331]) ).
thf(1084,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v200 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v200 @ leq ) ) ),
inference(simp,[status(thm)],[1083]) ).
thf(1110,plain,
( ( sk1 != v200 )
| ( v400 != v400 )
| ~ ( v400 @ ( v200 @ leq ) ) ),
inference(simp,[status(thm)],[1084]) ).
thf(1122,plain,
( ( sk1 != v200 )
| ~ ( v400 @ ( v200 @ leq ) ) ),
inference(simp,[status(thm)],[1110]) ).
thf(10,axiom,
v400 @ ( v200 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v200_v400) ).
thf(80,plain,
v400 @ ( v200 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( B @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_implies_leq) ).
thf(81,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
=> ( B @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(82,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[81]) ).
thf(2764,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v200 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[80,82]) ).
thf(2765,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v200 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2764]) ).
thf(2766,plain,
v400 @ ( v200 @ leq ),
inference(pattern_uni,[status(thm)],[2765:[bind(A,$thf( v200 )),bind(B,$thf( v400 ))]]) ).
thf(3943,plain,
( ( sk1 != v200 )
| ~ $true ),
inference(rewrite,[status(thm)],[1122,2766]) ).
thf(3944,plain,
sk1 != v200,
inference(simp,[status(thm)],[3943]) ).
thf(91,plain,
v100 != v400,
inference(cnfConj,[status(thm)],[84]) ).
thf(101,plain,
v400 != v100,
inference(lifteq,[status(thm)],[91]) ).
thf(27,axiom,
v100 @ ( v50 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v50_v100) ).
thf(136,plain,
v100 @ ( v50 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(2776,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[136,82]) ).
thf(2777,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2776]) ).
thf(2778,plain,
v100 @ ( v50 @ leq ),
inference(pattern_uni,[status(thm)],[2777:[bind(A,$thf( v50 )),bind(B,$thf( v100 ))]]) ).
thf(38,plain,
( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ),
inference(cnfConj,[status(thm)],[37]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( B != v50 )
| ( A @ ( v0 @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,38]) ).
thf(217,plain,
! [A: $i] :
( ( A @ ( v0 @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( v50 @ leq ) )
| ~ ( v50 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[216:[bind(A,$thf( A )),bind(B,$thf( v50 ))]]) ).
thf(41,plain,
sk3 @ ( v100 @ leq ),
inference(cnfConj,[status(thm)],[37]) ).
thf(89,plain,
v50 != v100,
inference(cnfConj,[status(thm)],[84]) ).
thf(97,plain,
v50 != v100,
inference(lifteq,[status(thm)],[89]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( A != v50 )
| ( B != v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,97]) ).
thf(219,plain,
! [A: $i] :
( ( A != v100 )
| ~ ( v50 @ ( A @ leq ) )
| ~ ( A @ ( v50 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[218:[bind(A,$thf( v50 ))]]) ).
thf(349,plain,
( ~ ( v50 @ ( v100 @ leq ) )
| ~ ( v100 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[219]) ).
thf(2155,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( v50 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( v50 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[41,349]) ).
thf(2156,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( v50 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2155]) ).
thf(2205,plain,
( ( sk3 != v50 )
| ( v100 != v100 )
| ~ ( v100 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2156]) ).
thf(2217,plain,
( ( sk3 != v50 )
| ~ ( v100 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2205]) ).
thf(4225,plain,
( ( sk3 != v50 )
| ~ $true ),
inference(rewrite,[status(thm)],[2217,2778]) ).
thf(4226,plain,
sk3 != v50,
inference(simp,[status(thm)],[4225]) ).
thf(4292,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != v50 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,4226]) ).
thf(4293,plain,
! [A: $i] :
( ( A != v50 )
| ~ ( sk3 @ ( A @ leq ) )
| ~ ( A @ ( sk3 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4292:[bind(A,$thf( sk3 ))]]) ).
thf(4302,plain,
( ~ ( sk3 @ ( v50 @ leq ) )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[4293]) ).
thf(16686,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v100 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2778,4302]) ).
thf(16687,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v100 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16686]) ).
thf(16827,plain,
( ( sk3 != v100 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16687]) ).
thf(16862,plain,
( ( sk3 != v100 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16827]) ).
thf(18,axiom,
v200 @ ( v50 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v50_v200) ).
thf(113,plain,
v200 @ ( v50 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(2761,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[113,82]) ).
thf(2762,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2761]) ).
thf(2763,plain,
v200 @ ( v50 @ leq ),
inference(pattern_uni,[status(thm)],[2762:[bind(A,$thf( v50 )),bind(B,$thf( v200 ))]]) ).
thf(40,plain,
sk2 @ ( v200 @ leq ),
inference(cnfConj,[status(thm)],[37]) ).
thf(94,plain,
v50 != v200,
inference(cnfConj,[status(thm)],[84]) ).
thf(103,plain,
v50 != v200,
inference(lifteq,[status(thm)],[94]) ).
thf(236,plain,
! [B: $i,A: $i] :
( ( A != v50 )
| ( B != v200 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,103]) ).
thf(237,plain,
! [A: $i] :
( ( A != v200 )
| ~ ( v50 @ ( A @ leq ) )
| ~ ( A @ ( v50 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( v50 ))]]) ).
thf(353,plain,
( ~ ( v50 @ ( v200 @ leq ) )
| ~ ( v200 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[237]) ).
thf(2298,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v50 @ ( v200 @ leq ) ) )
| ~ $true
| ~ ( v200 @ ( v50 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[40,353]) ).
thf(2299,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v50 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2298]) ).
thf(2327,plain,
( ( sk2 != v50 )
| ( v200 != v200 )
| ~ ( v200 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2299]) ).
thf(2335,plain,
( ( sk2 != v50 )
| ~ ( v200 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2327]) ).
thf(3841,plain,
( ( sk2 != v50 )
| ~ $true ),
inference(rewrite,[status(thm)],[2335,2763]) ).
thf(3842,plain,
sk2 != v50,
inference(simp,[status(thm)],[3841]) ).
thf(3927,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( B != v50 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3842]) ).
thf(3928,plain,
! [A: $i] :
( ( A != v50 )
| ~ ( sk2 @ ( A @ leq ) )
| ~ ( A @ ( sk2 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3927:[bind(A,$thf( sk2 ))]]) ).
thf(3938,plain,
( ~ ( sk2 @ ( v50 @ leq ) )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[3928]) ).
thf(14793,plain,
( ( ( sk2 @ ( v50 @ leq ) )
!= ( v200 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2763,3938]) ).
thf(14794,plain,
( ( ( sk2 @ ( v50 @ leq ) )
!= ( v200 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14793]) ).
thf(14940,plain,
( ( sk2 != v200 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14794]) ).
thf(14976,plain,
( ( sk2 != v200 )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14940]) ).
thf(85,plain,
v0 != v100,
inference(cnfConj,[status(thm)],[84]) ).
thf(98,plain,
v100 != v0,
inference(lifteq,[status(thm)],[85]) ).
thf(270,plain,
! [B: $i,A: $i] :
( ( A != v100 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,98]) ).
thf(271,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( v100 @ ( A @ leq ) )
| ~ ( A @ ( v100 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[270:[bind(A,$thf( v100 ))]]) ).
thf(324,plain,
( ~ ( v100 @ ( v0 @ leq ) )
| ~ ( v0 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[271]) ).
thf(13,axiom,
v100 @ ( v0 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v0_v100) ).
thf(105,plain,
v100 @ ( v0 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(2755,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[105,82]) ).
thf(2756,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2755]) ).
thf(2757,plain,
v100 @ ( v0 @ leq ),
inference(pattern_uni,[status(thm)],[2756:[bind(A,$thf( v0 )),bind(B,$thf( v100 ))]]) ).
thf(3508,plain,
( ~ $true
| ~ ( v0 @ ( v100 @ leq ) ) ),
inference(rewrite,[status(thm)],[324,2757]) ).
thf(3509,plain,
~ ( v0 @ ( v100 @ leq ) ),
inference(simp,[status(thm)],[3508]) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ less ) )
| ( A = B )
| ( B @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trichotomy) ).
thf(53,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ less ) )
| ( A = B )
| ( B @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( A = B )
| ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[53]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ( B @ ( A @ less ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[54]) ).
thf(87,plain,
v100 != v200,
inference(cnfConj,[status(thm)],[84]) ).
thf(102,plain,
v100 != v200,
inference(lifteq,[status(thm)],[87]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( A != v100 )
| ( B != v200 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,102]) ).
thf(203,plain,
! [A: $i] :
( ( A != v200 )
| ~ ( v100 @ ( A @ leq ) )
| ~ ( A @ ( v100 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[202:[bind(A,$thf( v100 ))]]) ).
thf(344,plain,
( ~ ( v100 @ ( v200 @ leq ) )
| ~ ( v200 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(1840,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v100 @ ( v200 @ leq ) ) )
| ~ $true
| ~ ( v200 @ ( v100 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[40,344]) ).
thf(1841,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v100 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1840]) ).
thf(1864,plain,
( ( sk2 != v100 )
| ( v200 != v200 )
| ~ ( v200 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1841]) ).
thf(1873,plain,
( ( sk2 != v100 )
| ~ ( v200 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1864]) ).
thf(29,axiom,
v200 @ ( v100 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v100_v200) ).
thf(147,plain,
v200 @ ( v100 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(2749,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[147,82]) ).
thf(2750,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2749]) ).
thf(2751,plain,
v200 @ ( v100 @ leq ),
inference(pattern_uni,[status(thm)],[2750:[bind(A,$thf( v100 )),bind(B,$thf( v200 ))]]) ).
thf(3156,plain,
( ( sk2 != v100 )
| ~ $true ),
inference(rewrite,[status(thm)],[1873,2751]) ).
thf(3157,plain,
sk2 != v100,
inference(simp,[status(thm)],[3156]) ).
thf(3281,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( B != v100 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3157]) ).
thf(3282,plain,
! [A: $i] :
( ( A != v100 )
| ( sk2 @ ( A @ less ) )
| ( A @ ( sk2 @ less ) ) ),
inference(pattern_uni,[status(thm)],[3281:[bind(A,$thf( sk2 ))]]) ).
thf(3285,plain,
( ( sk2 @ ( v100 @ less ) )
| ( v100 @ ( sk2 @ less ) ) ),
inference(simp,[status(thm)],[3282]) ).
thf(22,axiom,
v400 @ val,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',val_v400) ).
thf(124,plain,
v400 @ val,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(250,plain,
! [B: $i,A: $i] :
( ( B != v400 )
| ( A @ val )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,124]) ).
thf(251,plain,
! [A: $i] :
( ( A @ val )
| ~ ( A @ ( v400 @ leq ) )
| ~ ( v400 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[250:[bind(A,$thf( A )),bind(B,$thf( v400 ))]]) ).
thf(8680,plain,
! [A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( A @ ( v400 @ leq ) ) )
| ( A @ val )
| ~ $true
| ~ ( v400 @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[39,251]) ).
thf(8681,plain,
! [A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( A @ ( v400 @ leq ) ) )
| ( A @ val )
| ~ ( v400 @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[8680]) ).
thf(8682,plain,
( ( sk1 @ val )
| ~ ( v400 @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[8681:[bind(A,$thf( sk1 ))]]) ).
thf(93,plain,
v0 != v400,
inference(cnfConj,[status(thm)],[84]) ).
thf(96,plain,
v400 != v0,
inference(lifteq,[status(thm)],[93]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ( A != v400 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,96]) ).
thf(253,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( v400 @ ( A @ leq ) )
| ~ ( A @ ( v400 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[252:[bind(A,$thf( v400 ))]]) ).
thf(359,plain,
( ~ ( v400 @ ( v0 @ leq ) )
| ~ ( v0 @ ( v400 @ leq ) ) ),
inference(simp,[status(thm)],[253]) ).
thf(2641,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v0 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v0 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39,359]) ).
thf(2642,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v0 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[2641]) ).
thf(2676,plain,
( ( sk1 != v0 )
| ( v400 != v400 )
| ~ ( v400 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[2642]) ).
thf(2688,plain,
( ( sk1 != v0 )
| ~ ( v400 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[2676]) ).
thf(33,axiom,
v400 @ ( v0 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v0_v400) ).
thf(157,plain,
v400 @ ( v0 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(2743,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[157,82]) ).
thf(2744,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2743]) ).
thf(2745,plain,
v400 @ ( v0 @ leq ),
inference(pattern_uni,[status(thm)],[2744:[bind(A,$thf( v0 )),bind(B,$thf( v400 ))]]) ).
thf(2779,plain,
( ( sk1 != v0 )
| ~ $true ),
inference(rewrite,[status(thm)],[2688,2745]) ).
thf(2780,plain,
sk1 != v0,
inference(simp,[status(thm)],[2779]) ).
thf(2923,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v0 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,2780]) ).
thf(2924,plain,
! [A: $i] :
( ( A != v0 )
| ( sk1 @ ( A @ less ) )
| ( A @ ( sk1 @ less ) ) ),
inference(pattern_uni,[status(thm)],[2923:[bind(A,$thf( sk1 ))]]) ).
thf(2929,plain,
( ( sk1 @ ( v0 @ less ) )
| ( v0 @ ( sk1 @ less ) ) ),
inference(simp,[status(thm)],[2924]) ).
thf(8116,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v0 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[2929,82]) ).
thf(8117,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v0 @ less ) ) ),
inference(simp,[status(thm)],[8116]) ).
thf(8118,plain,
( ( v0 @ ( sk1 @ leq ) )
| ( sk1 @ ( v0 @ less ) ) ),
inference(pattern_uni,[status(thm)],[8117:[bind(A,$thf( sk1 )),bind(B,$thf( v0 ))]]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_ropen ) ) )
<=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ leq ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in_ropen) ).
thf(114,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ less ) )
& ( A @ ( B @ leq ) ) )
=> ( C @ ( B @ ( A @ in_ropen ) ) ) )
& ( ( C @ ( B @ ( A @ in_ropen ) ) )
=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ leq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(115,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ less ) )
& ( A @ ( B @ leq ) ) )
=> ( C @ ( B @ ( A @ in_ropen ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_ropen ) ) )
=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ leq ) ) ) ) ),
inference(miniscope,[status(thm)],[114]) ).
thf(116,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ in_ropen ) ) )
| ~ ( F @ ( D @ less ) )
| ~ ( D @ ( E @ leq ) ) )
& ( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ ( A @ in_ropen ) ) ) )
& ( ( A @ ( B @ leq ) )
| ~ ( C @ ( B @ ( A @ in_ropen ) ) ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(119,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_ropen ) ) )
| ~ ( C @ ( A @ less ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(120,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_ropen ) ) )
| ~ ( C @ ( A @ less ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(23,axiom,
v200 @ val,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',val_v200) ).
thf(125,plain,
v200 @ val,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(246,plain,
! [B: $i,A: $i] :
( ( B != v200 )
| ( A @ val )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,125]) ).
thf(247,plain,
! [A: $i] :
( ( A @ val )
| ~ ( A @ ( v200 @ leq ) )
| ~ ( v200 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[246:[bind(A,$thf( A )),bind(B,$thf( v200 ))]]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) )
<=> ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axis_compatible_def) ).
thf(56,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) )
=> ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(3941,plain,
( ~ $true
| ~ ( v200 @ ( v400 @ leq ) ) ),
inference(rewrite,[status(thm)],[331,2766]) ).
thf(3942,plain,
~ ( v200 @ ( v400 @ leq ) ),
inference(simp,[status(thm)],[3941]) ).
thf(8383,plain,
! [A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( A @ ( v200 @ leq ) ) )
| ( A @ val )
| ~ $true
| ~ ( v200 @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[40,247]) ).
thf(8384,plain,
! [A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( A @ ( v200 @ leq ) ) )
| ( A @ val )
| ~ ( v200 @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[8383]) ).
thf(8385,plain,
( ( sk2 @ val )
| ~ ( v200 @ ( sk2 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[8384:[bind(A,$thf( sk2 ))]]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_closed ) ) )
<=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in_closed) ).
thf(149,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( C @ ( B @ ( A @ in_closed ) ) ) )
& ( ( C @ ( B @ ( A @ in_closed ) ) )
=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(150,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) )
=> ( C @ ( B @ ( A @ in_closed ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_closed ) ) )
=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ leq ) ) ) ) ),
inference(miniscope,[status(thm)],[149]) ).
thf(151,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ in_closed ) ) )
| ~ ( F @ ( D @ leq ) )
| ~ ( D @ ( E @ leq ) ) )
& ( ( C @ ( A @ leq ) )
| ~ ( C @ ( B @ ( A @ in_closed ) ) ) )
& ( ( A @ ( B @ leq ) )
| ~ ( C @ ( B @ ( A @ in_closed ) ) ) ) ),
inference(cnf,[status(esa)],[150]) ).
thf(153,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( C @ ( B @ ( A @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[151]) ).
thf(26,axiom,
v100 @ val,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',val_v100) ).
thf(135,plain,
v100 @ val,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(276,plain,
! [B: $i,A: $i] :
( ( B != v100 )
| ( A @ val )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,135]) ).
thf(277,plain,
! [A: $i] :
( ( A @ val )
| ~ ( A @ ( v100 @ leq ) )
| ~ ( v100 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[276:[bind(A,$thf( A )),bind(B,$thf( v100 ))]]) ).
thf(9670,plain,
! [A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( A @ ( v100 @ leq ) ) )
| ( A @ val )
| ~ $true
| ~ ( v100 @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[41,277]) ).
thf(9671,plain,
! [A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( A @ ( v100 @ leq ) ) )
| ( A @ val )
| ~ ( v100 @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[9670]) ).
thf(9672,plain,
( ( sk3 @ val )
| ~ ( v100 @ ( sk3 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[9671:[bind(A,$thf( sk3 ))]]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
<=> ~ ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axis_conflict_def) ).
thf(42,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) )
& ( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
=> ~ ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(4024,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v200 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3944]) ).
thf(4025,plain,
! [A: $i] :
( ( A != v200 )
| ( sk1 @ ( A @ less ) )
| ( A @ ( sk1 @ less ) ) ),
inference(pattern_uni,[status(thm)],[4024:[bind(A,$thf( sk1 ))]]) ).
thf(4030,plain,
( ( sk1 @ ( v200 @ less ) )
| ( v200 @ ( sk1 @ less ) ) ),
inference(simp,[status(thm)],[4025]) ).
thf(4296,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != v50 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,4226]) ).
thf(4297,plain,
! [A: $i] :
( ( A != v50 )
| ( sk3 @ ( A @ less ) )
| ( A @ ( sk3 @ less ) ) ),
inference(pattern_uni,[status(thm)],[4296:[bind(A,$thf( sk3 ))]]) ).
thf(4304,plain,
( ( sk3 @ ( v50 @ less ) )
| ( v50 @ ( sk3 @ less ) ) ),
inference(simp,[status(thm)],[4297]) ).
thf(13256,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk3 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk3 @ ( v50 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[4304,82]) ).
thf(13257,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk3 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk3 @ ( v50 @ less ) ) ),
inference(simp,[status(thm)],[13256]) ).
thf(13258,plain,
( ( v50 @ ( sk3 @ leq ) )
| ( sk3 @ ( v50 @ less ) ) ),
inference(pattern_uni,[status(thm)],[13257:[bind(A,$thf( sk3 )),bind(B,$thf( v50 ))]]) ).
thf(4,axiom,
! [A: $i] :
~ ( A @ ( A @ less ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',irreflexive) ).
thf(50,plain,
! [A: $i] :
~ ( A @ ( A @ less ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(51,plain,
~ ? [A: $i] : ( A @ ( A @ less ) ),
inference(miniscope,[status(thm)],[50]) ).
thf(52,plain,
! [A: $i] :
~ ( A @ ( A @ less ) ),
inference(cnf,[status(esa)],[51]) ).
thf(3839,plain,
( ~ ( v50 @ ( v200 @ leq ) )
| ~ $true ),
inference(rewrite,[status(thm)],[353,2763]) ).
thf(3840,plain,
~ ( v50 @ ( v200 @ leq ) ),
inference(simp,[status(thm)],[3839]) ).
thf(152,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( C @ ( B @ ( A @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[151]) ).
thf(86,plain,
v50 != v400,
inference(cnfConj,[status(thm)],[84]) ).
thf(100,plain,
v400 != v50,
inference(lifteq,[status(thm)],[86]) ).
thf(240,plain,
! [B: $i,A: $i] :
( ( A != v400 )
| ( B != v50 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,100]) ).
thf(241,plain,
! [A: $i] :
( ( A != v50 )
| ~ ( v400 @ ( A @ leq ) )
| ~ ( A @ ( v400 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( v400 ))]]) ).
thf(355,plain,
( ~ ( v400 @ ( v50 @ leq ) )
| ~ ( v50 @ ( v400 @ leq ) ) ),
inference(simp,[status(thm)],[241]) ).
thf(2411,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v50 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v50 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39,355]) ).
thf(2412,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v50 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2411]) ).
thf(2440,plain,
( ( sk1 != v50 )
| ( v400 != v400 )
| ~ ( v400 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2412]) ).
thf(2450,plain,
( ( sk1 != v50 )
| ~ ( v400 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[2440]) ).
thf(30,axiom,
v400 @ ( v50 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v50_v400) ).
thf(148,plain,
v400 @ ( v50 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(2758,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[148,82]) ).
thf(2759,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v50 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2758]) ).
thf(2760,plain,
v400 @ ( v50 @ leq ),
inference(pattern_uni,[status(thm)],[2759:[bind(A,$thf( v50 )),bind(B,$thf( v400 ))]]) ).
thf(3726,plain,
( ( sk1 != v50 )
| ~ $true ),
inference(rewrite,[status(thm)],[2450,2760]) ).
thf(3727,plain,
sk1 != v50,
inference(simp,[status(thm)],[3726]) ).
thf(3825,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v50 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3727]) ).
thf(3826,plain,
! [A: $i] :
( ( A != v50 )
| ~ ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3825:[bind(A,$thf( sk1 ))]]) ).
thf(3835,plain,
( ~ ( sk1 @ ( v50 @ leq ) )
| ~ ( v50 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[3826]) ).
thf(260,plain,
! [B: $i,A: $i] :
( ( B != v400 )
| ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,39]) ).
thf(261,plain,
! [A: $i] :
( ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( v400 @ leq ) )
| ~ ( v400 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[260:[bind(A,$thf( A )),bind(B,$thf( v400 ))]]) ).
thf(43,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ~ ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
=> ~ ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ) ),
inference(miniscope,[status(thm)],[42]) ).
thf(44,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( I @ ( H @ ( G @ ( F @ axis_conflict ) ) ) )
| ( I @ ( H @ ( F @ ( G @ ( H @ ( I @ sk4 ) ) ) @ in_closed ) ) ) )
& ( ( I @ ( H @ ( G @ ( F @ axis_conflict ) ) ) )
| ( G @ ( F @ ( F @ ( G @ ( H @ ( I @ sk4 ) ) ) @ in_closed ) ) ) )
& ( ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(46,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(48,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[46]) ).
thf(45,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(176,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) ) )
| ~ ( H @ ( G @ ( I @ in_closed ) ) )
| ~ ( F @ ( E @ ( I @ in_closed ) ) )
| ~ $true
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,45]) ).
thf(177,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) ) )
| ~ ( H @ ( G @ ( I @ in_closed ) ) )
| ~ ( F @ ( E @ ( I @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(178,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(pattern_uni,[status(thm)],[177:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( B )),bind(G,$thf( C )),bind(H,$thf( D ))]]) ).
thf(179,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(2781,plain,
( ~ $true
| ~ ( v0 @ ( v400 @ leq ) ) ),
inference(rewrite,[status(thm)],[359,2745]) ).
thf(2782,plain,
~ ( v0 @ ( v400 @ leq ) ),
inference(simp,[status(thm)],[2781]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[41,110]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ( A = B ) ),
inference(simp,[status(thm)],[230]) ).
thf(232,plain,
( ~ ( v100 @ ( sk3 @ leq ) )
| ( sk3 = v100 ) ),
inference(pattern_uni,[status(thm)],[231:[bind(A,$thf( v100 )),bind(B,$thf( sk3 ))]]) ).
thf(375,plain,
( ( sk3 != sk3 )
| ( v50 @ ( v0 @ ( v100 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( v100 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[232,38]) ).
thf(376,plain,
( ( v50 @ ( v0 @ ( v100 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( v100 @ ( sk3 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[375:[]]) ).
thf(14,axiom,
v400 @ ( v100 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v100_v400) ).
thf(106,plain,
v400 @ ( v100 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(488,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( v0 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( v0 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,324]) ).
thf(489,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( v0 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[488]) ).
thf(518,plain,
( ( sk3 != v0 )
| ( v100 != v100 )
| ~ ( v100 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[489]) ).
thf(525,plain,
( ( sk3 != v0 )
| ~ ( v100 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[518]) ).
thf(3510,plain,
( ( sk3 != v0 )
| ~ $true ),
inference(rewrite,[status(thm)],[525,2757]) ).
thf(3511,plain,
sk3 != v0,
inference(simp,[status(thm)],[3510]) ).
thf(3615,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != v0 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3511]) ).
thf(3616,plain,
! [A: $i] :
( ( A != v0 )
| ( sk3 @ ( A @ less ) )
| ( A @ ( sk3 @ less ) ) ),
inference(pattern_uni,[status(thm)],[3615:[bind(A,$thf( sk3 ))]]) ).
thf(3621,plain,
( ( sk3 @ ( v0 @ less ) )
| ( v0 @ ( sk3 @ less ) ) ),
inference(simp,[status(thm)],[3616]) ).
thf(20,axiom,
v50 @ val,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',val_v50) ).
thf(121,plain,
v50 @ val,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( A != v400 )
| ( B != v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,101]) ).
thf(195,plain,
! [A: $i] :
( ( A != v100 )
| ~ ( v400 @ ( A @ leq ) )
| ~ ( A @ ( v400 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[194:[bind(A,$thf( v400 ))]]) ).
thf(341,plain,
( ~ ( v400 @ ( v100 @ leq ) )
| ~ ( v100 @ ( v400 @ leq ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(1601,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v100 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v100 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39,341]) ).
thf(1602,plain,
( ( ( sk1 @ ( v400 @ leq ) )
!= ( v100 @ ( v400 @ leq ) ) )
| ~ ( v400 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1601]) ).
thf(1631,plain,
( ( sk1 != v100 )
| ( v400 != v400 )
| ~ ( v400 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1602]) ).
thf(1642,plain,
( ( sk1 != v100 )
| ~ ( v400 @ ( v100 @ leq ) ) ),
inference(simp,[status(thm)],[1631]) ).
thf(2746,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[106,82]) ).
thf(2747,plain,
! [B: $i,A: $i] :
( ( ( v400 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2746]) ).
thf(2748,plain,
v400 @ ( v100 @ leq ),
inference(pattern_uni,[status(thm)],[2747:[bind(A,$thf( v100 )),bind(B,$thf( v400 ))]]) ).
thf(2931,plain,
( ( sk1 != v100 )
| ~ $true ),
inference(rewrite,[status(thm)],[1642,2748]) ).
thf(2932,plain,
sk1 != v100,
inference(simp,[status(thm)],[2931]) ).
thf(3058,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,2932]) ).
thf(3059,plain,
! [A: $i] :
( ( A != v100 )
| ~ ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3058:[bind(A,$thf( sk1 ))]]) ).
thf(3068,plain,
( ~ ( sk1 @ ( v100 @ leq ) )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[3059]) ).
thf(28,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( ( A = B )
| ( B @ ( A @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_def) ).
thf(137,plain,
! [A: $i,B: $i] :
( ( ( ( A = B )
| ( B @ ( A @ less ) ) )
=> ( B @ ( A @ leq ) ) )
& ( ( B @ ( A @ leq ) )
=> ( ( A = B )
| ( B @ ( A @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(138,plain,
( ! [A: $i,B: $i] :
( ( ( A = B )
| ( B @ ( A @ less ) ) )
=> ( B @ ( A @ leq ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( ( A = B )
| ( B @ ( A @ less ) ) ) ) ),
inference(miniscope,[status(thm)],[137]) ).
thf(139,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ leq ) )
| ( C != D ) )
& ( ( D @ ( C @ leq ) )
| ~ ( D @ ( C @ less ) ) )
& ( ( A = B )
| ( B @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) ) ) ),
inference(cnf,[status(esa)],[138]) ).
thf(140,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnfConj,[status(thm)],[139]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ less ) )
| ~ ( B @ ( A @ leq ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[140]) ).
thf(5550,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[40,143]) ).
thf(5551,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ( A = B ) ),
inference(simp,[status(thm)],[5550]) ).
thf(5552,plain,
( ( sk2 @ ( v200 @ less ) )
| ( sk2 = v200 ) ),
inference(pattern_uni,[status(thm)],[5551:[bind(A,$thf( v200 )),bind(B,$thf( sk2 ))]]) ).
thf(142,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[139]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[142]) ).
thf(146,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[145]) ).
thf(8607,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( v200 @ ( sk2 @ leq ) ) )
| ( sk2 @ val )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[146,8385]) ).
thf(8608,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( v200 @ ( sk2 @ leq ) ) )
| ( sk2 @ val ) ),
inference(simp,[status(thm)],[8607]) ).
thf(8616,plain,
! [A: $i] :
( ( A != v200 )
| ( A != sk2 )
| ( sk2 @ val ) ),
inference(simp,[status(thm)],[8608]) ).
thf(8636,plain,
( ( sk2 != v200 )
| ( sk2 @ val ) ),
inference(simp,[status(thm)],[8616]) ).
thf(8815,plain,
( ( sk2 != sk2 )
| ( v200 != v200 )
| ( sk2 @ val )
| ( sk2 @ ( v200 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[5552,8636]) ).
thf(8816,plain,
( ( sk2 != sk2 )
| ( sk2 @ val )
| ( sk2 @ ( v200 @ less ) ) ),
inference(simp,[status(thm)],[8815]) ).
thf(8817,plain,
( ( sk2 @ val )
| ( sk2 @ ( v200 @ less ) ) ),
inference(pattern_uni,[status(thm)],[8816:[]]) ).
thf(25,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ less ) ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_leq_trans) ).
thf(133,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ less ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(24,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_lopen ) ) )
<=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in_lopen) ).
thf(126,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ less ) ) )
=> ( C @ ( B @ ( A @ in_lopen ) ) ) )
& ( ( C @ ( B @ ( A @ in_lopen ) ) )
=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(127,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ leq ) )
& ( A @ ( B @ less ) ) )
=> ( C @ ( B @ ( A @ in_lopen ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_lopen ) ) )
=> ( ( C @ ( A @ leq ) )
& ( A @ ( B @ less ) ) ) ) ),
inference(miniscope,[status(thm)],[126]) ).
thf(128,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ in_lopen ) ) )
| ~ ( F @ ( D @ leq ) )
| ~ ( D @ ( E @ less ) ) )
& ( ( C @ ( A @ leq ) )
| ~ ( C @ ( B @ ( A @ in_lopen ) ) ) )
& ( ( A @ ( B @ less ) )
| ~ ( C @ ( B @ ( A @ in_lopen ) ) ) ) ),
inference(cnf,[status(esa)],[127]) ).
thf(131,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_lopen ) ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[128]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_lopen ) ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ less ) ) ),
inference(simp,[status(thm)],[131]) ).
thf(11411,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk3 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk3 @ ( v0 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3621,82]) ).
thf(11412,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk3 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk3 @ ( v0 @ less ) ) ),
inference(simp,[status(thm)],[11411]) ).
thf(11413,plain,
( ( v0 @ ( sk3 @ leq ) )
| ( sk3 @ ( v0 @ less ) ) ),
inference(pattern_uni,[status(thm)],[11412:[bind(A,$thf( sk3 )),bind(B,$thf( v0 ))]]) ).
thf(32,axiom,
v200 @ ( v0 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v0_v200) ).
thf(156,plain,
v200 @ ( v0 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(2752,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[156,82]) ).
thf(2753,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2752]) ).
thf(2754,plain,
v200 @ ( v0 @ leq ),
inference(pattern_uni,[status(thm)],[2753:[bind(A,$thf( v0 )),bind(B,$thf( v200 ))]]) ).
thf(3611,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3511]) ).
thf(3612,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( sk3 @ ( A @ leq ) )
| ~ ( A @ ( sk3 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3611:[bind(A,$thf( sk3 ))]]) ).
thf(3623,plain,
( ~ ( sk3 @ ( v0 @ leq ) )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[3612]) ).
thf(13838,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v200 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2754,3623]) ).
thf(13839,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v200 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13838]) ).
thf(13861,plain,
( ( sk3 != v200 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13839]) ).
thf(13891,plain,
( ( sk3 != v200 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13861]) ).
thf(310,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[40,110]) ).
thf(311,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v200 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ( A = B ) ),
inference(simp,[status(thm)],[310]) ).
thf(312,plain,
( ~ ( v200 @ ( sk2 @ leq ) )
| ( sk2 = v200 ) ),
inference(pattern_uni,[status(thm)],[311:[bind(A,$thf( v200 )),bind(B,$thf( sk2 ))]]) ).
thf(306,plain,
! [B: $i,A: $i] :
( ( B != v200 )
| ( sk2 @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,40]) ).
thf(307,plain,
! [A: $i] :
( ( sk2 @ ( A @ leq ) )
| ~ ( A @ ( v200 @ leq ) )
| ~ ( v200 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[306:[bind(A,$thf( A )),bind(B,$thf( v200 ))]]) ).
thf(90,plain,
v0 != v200,
inference(cnfConj,[status(thm)],[84]) ).
thf(104,plain,
v200 != v0,
inference(lifteq,[status(thm)],[90]) ).
thf(298,plain,
! [B: $i,A: $i] :
( ( A != v200 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,104]) ).
thf(299,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( v200 @ ( A @ leq ) )
| ~ ( A @ ( v200 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[298:[bind(A,$thf( v200 ))]]) ).
thf(335,plain,
( ~ ( v200 @ ( v0 @ leq ) )
| ~ ( v0 @ ( v200 @ leq ) ) ),
inference(simp,[status(thm)],[299]) ).
thf(1449,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v0 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( v0 @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,335]) ).
thf(1450,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( v0 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[1449]) ).
thf(1471,plain,
( ( sk2 != v0 )
| ( v200 != v200 )
| ~ ( v200 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[1450]) ).
thf(1491,plain,
( ( sk2 != v0 )
| ~ ( v200 @ ( v0 @ leq ) ) ),
inference(simp,[status(thm)],[1471]) ).
thf(3382,plain,
( ( sk2 != v0 )
| ~ $true ),
inference(rewrite,[status(thm)],[1491,2754]) ).
thf(3383,plain,
sk2 != v0,
inference(simp,[status(thm)],[3382]) ).
thf(3500,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( B != v0 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3383]) ).
thf(3501,plain,
! [A: $i] :
( ( A != v0 )
| ( sk2 @ ( A @ less ) )
| ( A @ ( sk2 @ less ) ) ),
inference(pattern_uni,[status(thm)],[3500:[bind(A,$thf( sk2 ))]]) ).
thf(3506,plain,
( ( sk2 @ ( v0 @ less ) )
| ( v0 @ ( sk2 @ less ) ) ),
inference(simp,[status(thm)],[3501]) ).
thf(11157,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk2 @ ( v0 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3506,82]) ).
thf(11158,plain,
! [B: $i,A: $i] :
( ( ( v0 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk2 @ ( v0 @ less ) ) ),
inference(simp,[status(thm)],[11157]) ).
thf(11159,plain,
( ( v0 @ ( sk2 @ leq ) )
| ( sk2 @ ( v0 @ less ) ) ),
inference(pattern_uni,[status(thm)],[11158:[bind(A,$thf( sk2 )),bind(B,$thf( v0 ))]]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( B != v50 )
| ( A @ val )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,121]) ).
thf(201,plain,
! [A: $i] :
( ( A @ val )
| ~ ( A @ ( v50 @ leq ) )
| ~ ( v50 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[200:[bind(A,$thf( A )),bind(B,$thf( v50 ))]]) ).
thf(57,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) )
=> ? [E: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
& ( B @ ( A @ ( E @ in_closed ) ) ) ) ) ),
inference(miniscope,[status(thm)],[56]) ).
thf(58,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( G @ ( F @ ( E @ axis_compatible ) ) ) )
| ~ ( H @ ( G @ ( I @ in_closed ) ) )
| ~ ( F @ ( E @ ( I @ in_closed ) ) ) )
& ( ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) )
& ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(60,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(117,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ leq ) )
| ~ ( C @ ( B @ ( A @ in_ropen ) ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(10501,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk2 @ ( v100 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3285,82]) ).
thf(10502,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk2 @ ( v100 @ less ) ) ),
inference(simp,[status(thm)],[10501]) ).
thf(10503,plain,
( ( v100 @ ( sk2 @ leq ) )
| ( sk2 @ ( v100 @ less ) ) ),
inference(pattern_uni,[status(thm)],[10502:[bind(A,$thf( sk2 )),bind(B,$thf( v100 ))]]) ).
thf(14764,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( v100 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[10503,82]) ).
thf(14765,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14764]) ).
thf(14766,plain,
( ( sk2 @ ( v100 @ leq ) )
| ( v100 @ ( sk2 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[14765:[bind(A,$thf( v100 )),bind(B,$thf( sk2 ))]]) ).
thf(68,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
| ~ ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[65]) ).
thf(70,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) )
| ~ ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(167,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( C @ ( E @ in_closed ) ) )
!= ( B @ ( A @ ( E @ in_closed ) ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[45]) ).
thf(168,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( C @ in_closed ) ) )
| ~ ( B @ ( A @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(pattern_uni,[status(thm)],[167:[bind(A,$thf( C )),bind(B,$thf( D ))]]) ).
thf(169,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( C @ in_closed ) ) )
| ~ ( B @ ( A @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[168]) ).
thf(186,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( F @ ( E @ ( G @ in_closed ) ) ) )
| ~ $true
| ~ ( F @ ( E @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,169]) ).
thf(187,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( F @ ( E @ ( G @ in_closed ) ) ) )
| ~ ( F @ ( E @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(188,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ ( C @ ( D @ axis_conflict ) ) ) )
| ( A @ ( B @ ( C @ ( D @ axis_conflict ) ) ) ) ),
inference(pattern_uni,[status(thm)],[187:[bind(A,$thf( K )),bind(B,$thf( J )),bind(C,$thf( I )),bind(D,$thf( H )),bind(E,$thf( K )),bind(F,$thf( J )),bind(G,$thf( K @ ( J @ ( I @ ( H @ sk4 ) ) ) ))]]) ).
thf(192,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ ( C @ ( D @ axis_conflict ) ) ) )
| ( A @ ( B @ ( C @ ( D @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[188]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( A @ ( v100 @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,41]) ).
thf(229,plain,
! [A: $i] :
( ( A @ ( v100 @ leq ) )
| ~ ( A @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[228:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(284,plain,
! [B: $i,A: $i] :
( ( B != v400 )
| ( A @ ( v200 @ less ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,80]) ).
thf(285,plain,
! [A: $i] :
( ( A @ ( v200 @ less ) )
| ~ ( A @ ( v400 @ leq ) )
| ~ ( v400 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[284:[bind(A,$thf( A )),bind(B,$thf( v400 ))]]) ).
thf(286,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( D @ ( E @ ( F @ sk4 ) ) ) ) )
| ( F @ ( E @ ( D @ ( C @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ in_closed ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,48]) ).
thf(287,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( D @ ( E @ axis_conflict ) ) ) )
| ( D @ ( E @ ( A @ in_closed ) ) )
| ~ ( E @ ( D @ ( C @ ( B @ sk4 ) ) ) @ ( A @ leq ) )
| ~ ( A @ ( E @ ( D @ ( C @ ( B @ sk4 ) ) ) @ leq ) ) ),
inference(pattern_uni,[status(thm)],[286:[bind(A,$thf( J @ ( I @ ( H @ ( G @ sk4 ) ) ) )),bind(B,$thf( B )),bind(C,$thf( J )),bind(D,$thf( I )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(329,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( D @ ( E @ axis_conflict ) ) ) )
| ( D @ ( E @ ( A @ in_closed ) ) )
| ~ ( E @ ( D @ ( C @ ( B @ sk4 ) ) ) @ ( A @ leq ) )
| ~ ( A @ ( E @ ( D @ ( C @ ( B @ sk4 ) ) ) @ leq ) ) ),
inference(simp,[status(thm)],[287]) ).
thf(3275,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( B != v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3157]) ).
thf(3276,plain,
! [A: $i] :
( ( A != v100 )
| ~ ( sk2 @ ( A @ leq ) )
| ~ ( A @ ( sk2 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3275:[bind(A,$thf( sk2 ))]]) ).
thf(3287,plain,
( ~ ( sk2 @ ( v100 @ leq ) )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[3276]) ).
thf(12635,plain,
( ( ( sk2 @ ( v100 @ leq ) )
!= ( v400 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2748,3287]) ).
thf(12636,plain,
( ( ( sk2 @ ( v100 @ leq ) )
!= ( v400 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12635]) ).
thf(12739,plain,
( ( sk2 != v400 )
| ( v100 != v100 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12636]) ).
thf(12769,plain,
( ( sk2 != v400 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12739]) ).
thf(9827,plain,
( ( ( v100 @ ( sk3 @ leq ) )
!= ( sk3 @ ( v100 @ leq ) ) )
| ( sk3 @ val )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,9672]) ).
thf(9828,plain,
( ( ( v100 @ ( sk3 @ leq ) )
!= ( sk3 @ ( v100 @ leq ) ) )
| ( sk3 @ val ) ),
inference(simp,[status(thm)],[9827]) ).
thf(9872,plain,
( ( sk3 != v100 )
| ( sk3 != v100 )
| ( sk3 @ val ) ),
inference(simp,[status(thm)],[9828]) ).
thf(9889,plain,
( ( sk3 != v100 )
| ( sk3 @ val ) ),
inference(simp,[status(thm)],[9872]) ).
thf(3380,plain,
( ~ $true
| ~ ( v0 @ ( v200 @ leq ) ) ),
inference(rewrite,[status(thm)],[335,2754]) ).
thf(3381,plain,
~ ( v0 @ ( v200 @ leq ) ),
inference(simp,[status(thm)],[3380]) ).
thf(5426,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[39,143]) ).
thf(5427,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ( A = B ) ),
inference(simp,[status(thm)],[5426]) ).
thf(5428,plain,
( ( sk1 @ ( v400 @ less ) )
| ( sk1 = v400 ) ),
inference(pattern_uni,[status(thm)],[5427:[bind(A,$thf( v400 )),bind(B,$thf( sk1 ))]]) ).
thf(14310,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( v0 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[8118,82]) ).
thf(14311,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( v0 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[14310]) ).
thf(14312,plain,
( ( sk1 @ ( v0 @ leq ) )
| ( v0 @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[14311:[bind(A,$thf( v0 )),bind(B,$thf( sk1 ))]]) ).
thf(3494,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3383]) ).
thf(3495,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( sk2 @ ( A @ leq ) )
| ~ ( A @ ( sk2 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[3494:[bind(A,$thf( sk2 ))]]) ).
thf(3504,plain,
( ~ ( sk2 @ ( v0 @ leq ) )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[3495]) ).
thf(13413,plain,
( ( ( sk2 @ ( v0 @ leq ) )
!= ( v200 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2754,3504]) ).
thf(13414,plain,
( ( ( sk2 @ ( v0 @ leq ) )
!= ( v200 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13413]) ).
thf(13422,plain,
( ( sk2 != v200 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13414]) ).
thf(13468,plain,
( ( sk2 != v200 )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13422]) ).
thf(387,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ~ ( v100 @ ( sk3 @ leq ) )
| ( A = v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,232]) ).
thf(388,plain,
! [A: $i] :
( ~ ( v100 @ ( sk3 @ leq ) )
| ( A = v100 )
| ~ ( A @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[387:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(3831,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v50 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3727]) ).
thf(3832,plain,
! [A: $i] :
( ( A != v50 )
| ( sk1 @ ( A @ less ) )
| ( A @ ( sk1 @ less ) ) ),
inference(pattern_uni,[status(thm)],[3831:[bind(A,$thf( sk1 ))]]) ).
thf(3837,plain,
( ( sk1 @ ( v50 @ less ) )
| ( v50 @ ( sk1 @ less ) ) ),
inference(simp,[status(thm)],[3832]) ).
thf(11799,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v50 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3837,82]) ).
thf(11800,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v50 @ less ) ) ),
inference(simp,[status(thm)],[11799]) ).
thf(11801,plain,
( ( v50 @ ( sk1 @ leq ) )
| ( sk1 @ ( v50 @ less ) ) ),
inference(pattern_uni,[status(thm)],[11800:[bind(A,$thf( sk1 )),bind(B,$thf( v50 ))]]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_open ) ) )
<=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',in_open) ).
thf(73,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( A @ less ) )
& ( A @ ( B @ less ) ) )
=> ( C @ ( B @ ( A @ in_open ) ) ) )
& ( ( C @ ( B @ ( A @ in_open ) ) )
=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(74,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ less ) )
& ( A @ ( B @ less ) ) )
=> ( C @ ( B @ ( A @ in_open ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ in_open ) ) )
=> ( ( C @ ( A @ less ) )
& ( A @ ( B @ less ) ) ) ) ),
inference(miniscope,[status(thm)],[73]) ).
thf(75,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ in_open ) ) )
| ~ ( F @ ( D @ less ) )
| ~ ( D @ ( E @ less ) ) )
& ( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ ( A @ in_open ) ) ) )
& ( ( A @ ( B @ less ) )
| ~ ( C @ ( B @ ( A @ in_open ) ) ) ) ),
inference(cnf,[status(esa)],[74]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ ( A @ in_open ) ) ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(189,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
!= ( F @ ( E @ ( F @ ( E @ axis_conflict ) ) ) ) )
| ~ ( F @ ( E @ ( G @ in_closed ) ) )
| ~ $true
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,169]) ).
thf(190,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
!= ( F @ ( E @ ( F @ ( E @ axis_conflict ) ) ) ) )
| ~ ( F @ ( E @ ( G @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[189]) ).
thf(191,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( C @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( A @ ( B @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(pattern_uni,[status(thm)],[190:[bind(A,$thf( C )),bind(B,$thf( D )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( C )),bind(F,$thf( D ))]]) ).
thf(193,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( C @ in_closed ) ) )
| ( B @ ( A @ ( A @ ( B @ ( A @ ( B @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[191]) ).
thf(1935,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) )
!= ( H @ ( G @ ( E @ ( F @ ( G @ ( H @ sk6 ) ) ) @ in_closed ) ) ) )
| ( H @ ( G @ ( F @ ( E @ axis_subsumes ) ) ) )
| ~ $true
| ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[69,70]) ).
thf(1936,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in_closed ) ) )
!= ( H @ ( G @ ( E @ ( F @ ( G @ ( H @ sk6 ) ) ) @ in_closed ) ) ) )
| ( H @ ( G @ ( F @ ( E @ axis_subsumes ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) ),
inference(simp,[status(thm)],[1935]) ).
thf(1937,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( A @ axis_subsumes ) ) ) )
| ( B @ ( A @ ( B @ ( A @ axis_subsumes ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1936:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( A )),bind(F,$thf( B )),bind(G,$thf( A )),bind(H,$thf( B ))]]) ).
thf(1964,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ ( A @ axis_subsumes ) ) ) ),
inference(simp,[status(thm)],[1937]) ).
thf(12631,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( sk2 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[41,3287]) ).
thf(12632,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( sk2 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12631]) ).
thf(12717,plain,
( ( sk3 != sk2 )
| ( v100 != v100 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12632]) ).
thf(12756,plain,
( ( sk3 != sk2 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12717]) ).
thf(3935,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( A != v50 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,3842]) ).
thf(3936,plain,
! [A: $i] :
( ( A != v50 )
| ( A @ ( sk2 @ less ) )
| ( sk2 @ ( A @ less ) ) ),
inference(pattern_uni,[status(thm)],[3935:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(3937,plain,
( ( v50 @ ( sk2 @ less ) )
| ( sk2 @ ( v50 @ less ) ) ),
inference(simp,[status(thm)],[3936]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( C @ ( B @ ( A @ in_lopen ) ) ) ),
inference(cnfConj,[status(thm)],[128]) ).
thf(12944,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v200 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[4030,82]) ).
thf(12945,plain,
! [B: $i,A: $i] :
( ( ( v200 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v200 @ less ) ) ),
inference(simp,[status(thm)],[12944]) ).
thf(12946,plain,
( ( v200 @ ( sk1 @ leq ) )
| ( sk1 @ ( v200 @ less ) ) ),
inference(pattern_uni,[status(thm)],[12945:[bind(A,$thf( sk1 )),bind(B,$thf( v200 ))]]) ).
thf(134,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ leq ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[133]) ).
thf(5361,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[41,143]) ).
thf(5362,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( v100 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ( B @ ( A @ less ) )
| ( A = B ) ),
inference(simp,[status(thm)],[5361]) ).
thf(5363,plain,
( ( sk3 @ ( v100 @ less ) )
| ( sk3 = v100 ) ),
inference(pattern_uni,[status(thm)],[5362:[bind(A,$thf( v100 )),bind(B,$thf( sk3 ))]]) ).
thf(9911,plain,
( ( sk3 != sk3 )
| ( v100 != v100 )
| ( sk3 @ val )
| ( sk3 @ ( v100 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[5363,9889]) ).
thf(9912,plain,
( ( sk3 != sk3 )
| ( sk3 @ val )
| ( sk3 @ ( v100 @ less ) ) ),
inference(simp,[status(thm)],[9911]) ).
thf(9913,plain,
( ( sk3 @ val )
| ( sk3 @ ( v100 @ less ) ) ),
inference(pattern_uni,[status(thm)],[9912:[]]) ).
thf(264,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[39,110]) ).
thf(265,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v400 @ leq ) )
!= ( B @ ( A @ leq ) ) )
| ~ ( A @ ( B @ leq ) )
| ( A = B ) ),
inference(simp,[status(thm)],[264]) ).
thf(266,plain,
( ~ ( v400 @ ( sk1 @ leq ) )
| ( sk1 = v400 ) ),
inference(pattern_uni,[status(thm)],[265:[bind(A,$thf( v400 )),bind(B,$thf( sk1 ))]]) ).
thf(159,plain,
( ~ $true
| ( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
!= ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(161,plain,
( ( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
!= ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(170,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( F @ ( E @ ( I @ in_closed ) ) ) )
| ~ ( H @ ( G @ ( I @ in_closed ) ) )
| ~ $true
| ~ ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,45]) ).
thf(171,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( F @ ( E @ ( I @ in_closed ) ) ) )
| ~ ( H @ ( G @ ( I @ in_closed ) ) )
| ~ ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(172,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ sk4 ) ) ) @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ ( F @ axis_conflict ) ) ) )
| ( C @ ( D @ ( E @ ( F @ axis_conflict ) ) ) ) ),
inference(pattern_uni,[status(thm)],[171:[bind(A,$thf( M )),bind(B,$thf( L )),bind(C,$thf( K )),bind(D,$thf( J )),bind(E,$thf( M )),bind(F,$thf( L )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( M @ ( L @ ( K @ ( J @ sk4 ) ) ) ))]]) ).
thf(180,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ sk4 ) ) ) @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ ( F @ axis_conflict ) ) ) )
| ( C @ ( D @ ( E @ ( F @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(13311,plain,
( ( ( sk2 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2745,3504]) ).
thf(13312,plain,
( ( ( sk2 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13311]) ).
thf(13425,plain,
( ( sk2 != v400 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13312]) ).
thf(13471,plain,
( ( sk2 != v400 )
| ~ ( v0 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[13425]) ).
thf(3064,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v100 )
| ( A @ ( B @ less ) )
| ( B @ ( A @ less ) ) ),
inference(paramod_ordered,[status(thm)],[55,2932]) ).
thf(3065,plain,
! [A: $i] :
( ( A != v100 )
| ( sk1 @ ( A @ less ) )
| ( A @ ( sk1 @ less ) ) ),
inference(pattern_uni,[status(thm)],[3064:[bind(A,$thf( sk1 ))]]) ).
thf(3070,plain,
( ( sk1 @ ( v100 @ less ) )
| ( v100 @ ( sk1 @ less ) ) ),
inference(simp,[status(thm)],[3065]) ).
thf(16768,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2760,4302]) ).
thf(16769,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16768]) ).
thf(16834,plain,
( ( sk3 != v400 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16769]) ).
thf(16866,plain,
( ( sk3 != v400 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16834]) ).
thf(59,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(118,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ ( A @ in_ropen ) ) ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(8,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less ) )
& ( B @ ( A @ less ) ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitive) ).
thf(71,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less ) )
& ( B @ ( A @ less ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(47,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
| ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(49,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) )
| ( D @ ( C @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(173,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( H @ ( G @ ( I @ in_closed ) ) ) )
| ~ $true
| ~ ( F @ ( E @ ( I @ in_closed ) ) )
| ~ ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,45]) ).
thf(174,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( A @ ( B @ ( C @ ( D @ sk4 ) ) ) @ in_closed ) ) )
!= ( H @ ( G @ ( I @ in_closed ) ) ) )
| ~ ( F @ ( E @ ( I @ in_closed ) ) )
| ~ ( H @ ( G @ ( F @ ( E @ axis_conflict ) ) ) )
| ( D @ ( C @ ( B @ ( A @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[173]) ).
thf(175,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ sk4 ) ) ) @ in_closed ) ) )
| ~ ( E @ ( F @ ( B @ ( A @ axis_conflict ) ) ) )
| ( C @ ( D @ ( E @ ( F @ axis_conflict ) ) ) ) ),
inference(pattern_uni,[status(thm)],[174:[bind(A,$thf( M )),bind(B,$thf( L )),bind(C,$thf( K )),bind(D,$thf( J )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( M )),bind(H,$thf( L )),bind(I,$thf( M @ ( L @ ( K @ ( J @ sk4 ) ) ) ))]]) ).
thf(181,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ sk4 ) ) ) @ in_closed ) ) )
| ~ ( E @ ( F @ ( B @ ( A @ axis_conflict ) ) ) )
| ( C @ ( D @ ( E @ ( F @ axis_conflict ) ) ) ) ),
inference(simp,[status(thm)],[175]) ).
thf(11880,plain,
( ( ( sk1 @ ( v100 @ leq ) )
!= ( v400 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2748,3068]) ).
thf(11881,plain,
( ( ( sk1 @ ( v100 @ leq ) )
!= ( v400 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11880]) ).
thf(11957,plain,
( ( sk1 != v400 )
| ( v100 != v100 )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11881]) ).
thf(11996,plain,
( ( sk1 != v400 )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11957]) ).
thf(3154,plain,
( ~ ( v100 @ ( v200 @ leq ) )
| ~ $true ),
inference(rewrite,[status(thm)],[344,2751]) ).
thf(3155,plain,
~ ( v100 @ ( v200 @ leq ) ),
inference(simp,[status(thm)],[3154]) ).
thf(76,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ less ) )
| ~ ( C @ ( B @ ( A @ in_open ) ) ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(4227,plain,
( ~ ( v50 @ ( v100 @ leq ) )
| ~ $true ),
inference(rewrite,[status(thm)],[349,2778]) ).
thf(4228,plain,
~ ( v50 @ ( v100 @ leq ) ),
inference(simp,[status(thm)],[4227]) ).
thf(14876,plain,
( ( ( sk2 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2760,3938]) ).
thf(14877,plain,
( ( ( sk2 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14876]) ).
thf(14951,plain,
( ( sk2 != v400 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14877]) ).
thf(14979,plain,
( ( sk2 != v400 )
| ~ ( v50 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[14951]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( v50 @ ( v0 @ ( A @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,38]) ).
thf(213,plain,
! [A: $i] :
( ( v50 @ ( v0 @ ( A @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[212:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(8527,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk1 @ ( v100 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3070,82]) ).
thf(8528,plain,
! [B: $i,A: $i] :
( ( ( v100 @ ( sk1 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk1 @ ( v100 @ less ) ) ),
inference(simp,[status(thm)],[8527]) ).
thf(8529,plain,
( ( v100 @ ( sk1 @ leq ) )
| ( sk1 @ ( v100 @ less ) ) ),
inference(pattern_uni,[status(thm)],[8528:[bind(A,$thf( sk1 )),bind(B,$thf( v100 ))]]) ).
thf(14574,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( v100 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[8529,82]) ).
thf(14575,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( v100 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[14574]) ).
thf(14576,plain,
( ( sk1 @ ( v100 @ leq ) )
| ( v100 @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[14575:[bind(A,$thf( v100 )),bind(B,$thf( sk1 ))]]) ).
thf(154,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_closed ) ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(cnfConj,[status(thm)],[151]) ).
thf(155,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_closed ) ) )
| ~ ( C @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(4018,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v200 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,3944]) ).
thf(4019,plain,
! [A: $i] :
( ( A != v200 )
| ~ ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[4018:[bind(A,$thf( sk1 ))]]) ).
thf(4028,plain,
( ~ ( sk1 @ ( v200 @ leq ) )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[4019]) ).
thf(66,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ axis_subsumes ) ) ) ) ),
inference(cnfConj,[status(thm)],[65]) ).
thf(130,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( C @ ( B @ ( A @ in_lopen ) ) ) ),
inference(cnfConj,[status(thm)],[128]) ).
thf(12705,plain,
( ( ( sk2 @ ( v100 @ leq ) )
!= ( v200 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2751,3287]) ).
thf(12706,plain,
( ( ( sk2 @ ( v100 @ leq ) )
!= ( v200 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12705]) ).
thf(12727,plain,
( ( sk2 != v200 )
| ( v100 != v100 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12706]) ).
thf(12765,plain,
( ( sk2 != v200 )
| ~ ( v100 @ ( sk2 @ leq ) ) ),
inference(simp,[status(thm)],[12727]) ).
thf(15917,plain,
( ( ( sk1 @ ( v200 @ leq ) )
!= ( v400 @ ( v200 @ leq ) ) )
| ~ $true
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2766,4028]) ).
thf(15918,plain,
( ( ( sk1 @ ( v200 @ leq ) )
!= ( v400 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[15917]) ).
thf(16008,plain,
( ( sk1 != v400 )
| ( v200 != v200 )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[15918]) ).
thf(16042,plain,
( ( sk1 != v400 )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[16008]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ less ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_less_trans) ).
thf(111,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ less ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ less ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(112,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ less ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[111]) ).
thf(2917,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,2780]) ).
thf(2918,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( sk1 @ ( A @ leq ) )
| ~ ( A @ ( sk1 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[2917:[bind(A,$thf( sk1 ))]]) ).
thf(2927,plain,
( ~ ( sk1 @ ( v0 @ leq ) )
| ~ ( v0 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[2918]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leq_trans) ).
thf(122,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ leq ) )
& ( B @ ( A @ leq ) ) )
=> ( C @ ( A @ leq ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(123,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ leq ) )
| ~ ( C @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnf,[status(esa)],[122]) ).
thf(262,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( A @ ( v400 @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,39]) ).
thf(263,plain,
! [A: $i] :
( ( A @ ( v400 @ leq ) )
| ~ ( A @ ( sk1 @ leq ) )
| ~ ( sk1 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[262:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(13740,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2745,3623]) ).
thf(13741,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13740]) ).
thf(13864,plain,
( ( sk3 != v400 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13741]) ).
thf(13893,plain,
( ( sk3 != v400 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13864]) ).
thf(369,plain,
! [B: $i,A: $i] :
( ( B != v100 )
| ( A @ ( v0 @ less ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,105]) ).
thf(370,plain,
! [A: $i] :
( ( A @ ( v0 @ less ) )
| ~ ( A @ ( v100 @ leq ) )
| ~ ( v100 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[369:[bind(A,$thf( A )),bind(B,$thf( v100 ))]]) ).
thf(14421,plain,
( ( ( sk1 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2760,3835]) ).
thf(14422,plain,
( ( ( sk1 @ ( v50 @ leq ) )
!= ( v400 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[14421]) ).
thf(14494,plain,
( ( sk1 != v400 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[14422]) ).
thf(14513,plain,
( ( sk1 != v400 )
| ~ ( v50 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[14494]) ).
thf(13772,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v100 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2757,3623]) ).
thf(13773,plain,
( ( ( sk3 @ ( v0 @ leq ) )
!= ( v100 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13772]) ).
thf(13848,plain,
( ( sk3 != v100 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13773]) ).
thf(13880,plain,
( ( sk3 != v100 )
| ~ ( v0 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[13848]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less ) )
| ~ ( C @ ( B @ less ) )
| ~ ( B @ ( A @ less ) ) ),
inference(cnf,[status(esa)],[71]) ).
thf(15971,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( sk1 @ ( v200 @ leq ) ) )
| ~ $true
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[40,4028]) ).
thf(15972,plain,
( ( ( sk2 @ ( v200 @ leq ) )
!= ( sk1 @ ( v200 @ leq ) ) )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[15971]) ).
thf(16019,plain,
( ( sk2 != sk1 )
| ( v200 != v200 )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[15972]) ).
thf(16049,plain,
( ( sk2 != sk1 )
| ~ ( v200 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[16019]) ).
thf(92,plain,
v0 != v50,
inference(cnfConj,[status(thm)],[84]) ).
thf(99,plain,
v50 != v0,
inference(lifteq,[status(thm)],[92]) ).
thf(367,plain,
! [B: $i,A: $i] :
( ( B != v0 )
| ( v100 @ ( A @ less ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,105]) ).
thf(368,plain,
! [A: $i] :
( ( v100 @ ( A @ less ) )
| ~ ( A @ ( v0 @ leq ) )
| ~ ( v0 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[367:[bind(A,$thf( A )),bind(B,$thf( v0 ))]]) ).
thf(15,axiom,
v50 @ ( v0 @ less ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ord_v0_v50) ).
thf(107,plain,
v50 @ ( v0 @ less ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(2773,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[107,82]) ).
thf(2774,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( v0 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) ) ),
inference(simp,[status(thm)],[2773]) ).
thf(2775,plain,
v50 @ ( v0 @ leq ),
inference(pattern_uni,[status(thm)],[2774:[bind(A,$thf( v0 )),bind(B,$thf( v50 ))]]) ).
thf(3728,plain,
( ~ $true
| ~ ( v50 @ ( v400 @ leq ) ) ),
inference(rewrite,[status(thm)],[355,2760]) ).
thf(3729,plain,
~ ( v50 @ ( v400 @ leq ) ),
inference(simp,[status(thm)],[3728]) ).
thf(34,axiom,
v0 @ val,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',val_v0) ).
thf(158,plain,
v0 @ val,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(318,plain,
! [B: $i,A: $i] :
( ( B != v0 )
| ( A @ val )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,158]) ).
thf(319,plain,
! [A: $i] :
( ( A @ val )
| ~ ( A @ ( v0 @ leq ) )
| ~ ( v0 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[318:[bind(A,$thf( A )),bind(B,$thf( v0 ))]]) ).
thf(389,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ~ ( v100 @ ( A @ leq ) )
| ( sk3 = v100 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,232]) ).
thf(390,plain,
! [A: $i] :
( ~ ( v100 @ ( A @ leq ) )
| ( sk3 = v100 )
| ~ ( A @ ( sk3 @ leq ) )
| ~ ( sk3 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[389:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(16690,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v200 @ ( v50 @ leq ) ) )
| ~ $true
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2763,4302]) ).
thf(16691,plain,
( ( ( sk3 @ ( v50 @ leq ) )
!= ( v200 @ ( v50 @ leq ) ) )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16690]) ).
thf(16837,plain,
( ( sk3 != v200 )
| ( v50 != v50 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16691]) ).
thf(16867,plain,
( ( sk3 != v200 )
| ~ ( v50 @ ( sk3 @ leq ) ) ),
inference(simp,[status(thm)],[16837]) ).
thf(2933,plain,
( ~ $true
| ~ ( v100 @ ( v400 @ leq ) ) ),
inference(rewrite,[status(thm)],[341,2748]) ).
thf(2934,plain,
~ ( v100 @ ( v400 @ leq ) ),
inference(simp,[status(thm)],[2933]) ).
thf(294,plain,
! [B: $i,A: $i] :
( ( A != v50 )
| ( B != v0 )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,99]) ).
thf(295,plain,
! [A: $i] :
( ( A != v0 )
| ~ ( v50 @ ( A @ leq ) )
| ~ ( A @ ( v50 @ leq ) ) ),
inference(pattern_uni,[status(thm)],[294:[bind(A,$thf( v50 ))]]) ).
thf(333,plain,
( ~ ( v50 @ ( v0 @ leq ) )
| ~ ( v0 @ ( v50 @ leq ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(4152,plain,
( ~ $true
| ~ ( v0 @ ( v50 @ leq ) ) ),
inference(rewrite,[status(thm)],[333,2775]) ).
thf(4153,plain,
~ ( v0 @ ( v50 @ leq ) ),
inference(simp,[status(thm)],[4152]) ).
thf(9310,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( v400 @ ( sk1 @ leq ) ) )
| ( sk1 @ val )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[146,8682]) ).
thf(9311,plain,
! [A: $i] :
( ( ( A @ ( A @ leq ) )
!= ( v400 @ ( sk1 @ leq ) ) )
| ( sk1 @ val ) ),
inference(simp,[status(thm)],[9310]) ).
thf(9330,plain,
! [A: $i] :
( ( A != v400 )
| ( A != sk1 )
| ( sk1 @ val ) ),
inference(simp,[status(thm)],[9311]) ).
thf(9346,plain,
( ( sk1 != v400 )
| ( sk1 @ val ) ),
inference(simp,[status(thm)],[9330]) ).
thf(11466,plain,
( ( ( sk1 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ $true
| ~ ( v0 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[2745,2927]) ).
thf(11467,plain,
( ( ( sk1 @ ( v0 @ leq ) )
!= ( v400 @ ( v0 @ leq ) ) )
| ~ ( v0 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11466]) ).
thf(11574,plain,
( ( sk1 != v400 )
| ( v0 != v0 )
| ~ ( v0 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11467]) ).
thf(11612,plain,
( ( sk1 != v400 )
| ~ ( v0 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11574]) ).
thf(282,plain,
! [B: $i,A: $i] :
( ( B != v200 )
| ( v400 @ ( A @ less ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,80]) ).
thf(283,plain,
! [A: $i] :
( ( v400 @ ( A @ less ) )
| ~ ( A @ ( v200 @ leq ) )
| ~ ( v200 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[282:[bind(A,$thf( A )),bind(B,$thf( v200 ))]]) ).
thf(78,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_open ) ) )
| ~ ( C @ ( A @ less ) )
| ~ ( A @ ( B @ less ) ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(79,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ in_open ) ) )
| ~ ( C @ ( A @ less ) )
| ~ ( A @ ( B @ less ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(12305,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ~ $true
| ( sk2 @ ( v50 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[3937,82]) ).
thf(12306,plain,
! [B: $i,A: $i] :
( ( ( v50 @ ( sk2 @ less ) )
!= ( B @ ( A @ less ) ) )
| ( B @ ( A @ leq ) )
| ( sk2 @ ( v50 @ less ) ) ),
inference(simp,[status(thm)],[12305]) ).
thf(12307,plain,
( ( v50 @ ( sk2 @ leq ) )
| ( sk2 @ ( v50 @ less ) ) ),
inference(pattern_uni,[status(thm)],[12306:[bind(A,$thf( sk2 )),bind(B,$thf( v50 ))]]) ).
thf(160,plain,
( ~ $true
| ( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
!= ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[38]) ).
thf(163,plain,
( ( ( v50 @ ( v0 @ ( sk3 @ in_lopen ) ) )
!= ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(61,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) )
| ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(62,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ axis_compatible ) ) ) )
| ~ ( D @ ( C @ ( E @ in_closed ) ) )
| ~ ( B @ ( A @ ( E @ in_closed ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(11872,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( sk1 @ ( v100 @ leq ) ) )
| ~ $true
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[41,3068]) ).
thf(11873,plain,
( ( ( sk3 @ ( v100 @ leq ) )
!= ( sk1 @ ( v100 @ leq ) ) )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11872]) ).
thf(11974,plain,
( ( sk3 != sk1 )
| ( v100 != v100 )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11873]) ).
thf(12007,plain,
( ( sk3 != sk1 )
| ~ ( v100 @ ( sk1 @ leq ) ) ),
inference(simp,[status(thm)],[11974]) ).
thf(226,plain,
! [B: $i,A: $i] :
( ( B != v100 )
| ( sk3 @ ( A @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,41]) ).
thf(227,plain,
! [A: $i] :
( ( sk3 @ ( A @ leq ) )
| ~ ( A @ ( v100 @ leq ) )
| ~ ( v100 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[226:[bind(A,$thf( A )),bind(B,$thf( v100 ))]]) ).
thf(9534,plain,
( ( sk1 != sk1 )
| ( v400 != v400 )
| ( sk1 @ val )
| ( sk1 @ ( v400 @ less ) ) ),
inference(paramod_ordered,[status(thm)],[5428,9346]) ).
thf(9535,plain,
( ( sk1 != sk1 )
| ( sk1 @ val )
| ( sk1 @ ( v400 @ less ) ) ),
inference(simp,[status(thm)],[9534]) ).
thf(9536,plain,
( ( sk1 @ val )
| ( sk1 @ ( v400 @ less ) ) ),
inference(pattern_uni,[status(thm)],[9535:[]]) ).
thf(308,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( A @ ( v200 @ leq ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,40]) ).
thf(309,plain,
! [A: $i] :
( ( A @ ( v200 @ leq ) )
| ~ ( A @ ( sk2 @ leq ) )
| ~ ( sk2 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[308:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(214,plain,
! [B: $i,A: $i] :
( ( B != v0 )
| ( v50 @ ( A @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( B @ leq ) )
| ~ ( B @ ( A @ leq ) ) ),
inference(paramod_ordered,[status(thm)],[110,38]) ).
thf(215,plain,
! [A: $i] :
( ( v50 @ ( A @ ( sk3 @ in_lopen ) ) )
| ( v100 @ ( v0 @ ( sk2 @ in_lopen ) ) )
| ( v200 @ ( v0 @ ( sk1 @ in_lopen ) ) )
| ~ ( A @ ( v0 @ leq ) )
| ~ ( v0 @ ( A @ leq ) ) ),
inference(pattern_uni,[status(thm)],[214:[bind(A,$thf( A )),bind(B,$thf( v0 ))]]) ).
thf(31250,plain,
$false,
inference(e,[status(thm)],[69,3944,101,2778,217,16862,14976,4226,3509,3285,8682,8118,120,247,56,3942,8385,153,9672,2763,42,4030,13258,52,3938,110,125,2745,157,3840,2929,152,3835,4302,261,179,2782,376,106,3621,121,147,3068,8817,3157,133,132,11413,13891,312,307,11159,201,102,60,117,14766,38,70,192,137,229,3727,285,97,329,12769,156,9889,3381,5428,14312,13468,388,53,169,8636,11801,77,193,96,124,1964,12756,2932,3937,129,12946,2766,41,134,73,105,9913,266,2748,10503,148,45,161,180,149,13471,3070,16866,3504,59,118,71,5363,49,181,11996,3155,76,39,98,113,4228,3287,81,5552,14979,103,213,2757,14576,251,155,108,2780,4028,66,8529,130,135,12765,4304,80,35,16042,112,2927,123,48,63,3842,95,263,13893,50,370,14513,13880,3623,72,16049,143,2760,99,104,368,2775,3729,319,40,3383,158,390,16867,2934,55,114,4153,82,9346,3511,146,3837,11612,3506,283,2751,107,126,136,79,12307,163,62,277,12007,111,227,2754,122,83,9536,309,215,232,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT085+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 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.13/0.38 % Computer : n007.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sat Sep 26 00:10:38 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 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.19/1.11 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.84/1.44 % [INFO] Parsing done (326ms).
% 1.84/1.46 % [INFO] Running in sequential loop mode.
% 2.69/2.05 % [INFO] eprover registered as external prover.
% 3.01/2.06 % [INFO] Scanning for conjecture ...
% 3.28/2.22 % [INFO] Found a conjecture (or negated_conjecture) and 43 axioms. Running axiom selection ...
% 3.47/2.33 % [INFO] Axiom selection finished. Selected 32 axioms (removed 11 axioms).
% 3.72/2.40 % [INFO] Problem is first-order (TPTP FOF).
% 3.72/2.41 % [INFO] Type checking passed.
% 3.72/2.42 % [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 ...
% 89.23/19.45 % External prover 'e' found a proof!
% 89.23/19.46 % [INFO] Killing All external provers ...
% 89.23/19.46 % Time passed: 18858ms (effective reasoning time: 17991ms)
% 89.23/19.46 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 89.23/19.46 % Axioms used in derivation (32): ord_v0_v400, ord_v50_v400, leq_antisym, ord_v0_v50, ord_v100_v200, val_v0, ord_v200_v400, axis_conflict_def, irreflexive, ord_v0_v200, in_open, ord_v50_v100, ord_v50_v200, val_v100, leq_def, axis_subsumes_def, less_implies_leq, in_ropen, leq_trans, leq_less_trans, val_v400, in_closed, val_v50, in_lopen, ord_v100_v400, distinct, less_leq_trans, axis_compatible_def, val_v200, trichotomy, transitive, ord_v0_v100
% 89.23/19.46 % No. of inferences in proof: 581
% 89.23/19.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18858 ms resp. 17991 ms w/o parsing
% 75.79/19.75 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 75.79/19.76 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------