diff options
Diffstat (limited to 'test/regress/regress2/ho/SYO362^5.p')
| -rw-r--r-- | test/regress/regress2/ho/SYO362^5.p | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress2/ho/SYO362^5.p b/test/regress/regress2/ho/SYO362^5.p new file mode 100644 index 000000000..c01d3f235 --- /dev/null +++ b/test/regress/regress2/ho/SYO362^5.p @@ -0,0 +1,22 @@ +% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% EXPECT: % SZS status Theorem for SYO362^5 + +thf(cK,type,( + cK: ( $i > $o ) > $i > $o )). + +thf(cTHM631A_pme,conjecture, + ( ! [X: $i > $o,Y: $i > $o] : + ( ( cK + @ ^ [Xz: $i] : + ( ( X @ Xz ) + | ( Y @ Xz ) ) ) + = ( ^ [Xw: $i] : + ( ( cK @ X @ Xw ) + | ( cK @ Y @ Xw ) ) ) ) + => ! [X: $i > $o,Y: $i > $o] : + ( ! [Xx: $i] : + ( ( X @ Xx ) + => ( Y @ Xx ) ) + => ! [Xx: $i] : + ( ( cK @ X @ Xx ) + => ( cK @ Y @ Xx ) ) ) )). |