%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU997^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 02:53:04 PM UTC 2025
% Result : Theorem 23.84s 24.10s
% Output : Proof 23.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 98 ( 58 unt; 0 typ; 0 def)
% Number of atoms : 1058 ( 297 equ; 0 cnn)
% Maximal formula atoms : 42 ( 10 avg)
% Number of connectives : 1677 ( 278 ~; 113 |; 80 &;1062 @)
% ( 0 <=>; 140 =>; 4 <=; 0 <~>)
% Maximal formula depth : 50 ( 7 avg)
% Number of types : 0 ( 0 usr)
% Number of type conns : 14 ( 14 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 32 usr; 33 con; 0-2 aty)
% Number of variables : 404 ( 0 ^; 404 !; 0 ?; 404 :)
% Comments :
%------------------------------------------------------------------------------
thf(cCD_LATTICE_THM_pme,conjecture,
! [X1: a > a > a,X2: a > a > a,X3: a,X4: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X5: a] :
( ( X1 @ X5 @ X5 )
= X5 )
=> ~ ! [X5: a] :
( ( X2 @ X5 @ X5 )
= X5 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ ( X1 @ X5 @ X6 ) @ X7 )
= ( X1 @ X5 @ ( X1 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ ( X2 @ X5 @ X6 ) @ X7 )
= ( X2 @ X5 @ ( X2 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ X5 @ X6 )
= ( X1 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ X5 @ X6 )
= ( X2 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ ( X2 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ ( X1 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ X5 @ ( X1 @ X6 @ X7 ) )
= ( X1 @ ( X2 @ X5 @ X6 ) @ ( X2 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ X5 @ ( X2 @ X6 @ X7 ) )
= ( X2 @ ( X1 @ X5 @ X6 ) @ ( X1 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a] :
( ( X2 @ X3 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
( ( X1 @ X3 @ X5 )
= X3 ) )
=> ~ ! [X5: a] :
( ( X2 @ X4 @ X5 )
= X4 ) )
=> ~ ! [X5: a] :
( ( X1 @ X4 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
~ ! [X6: a] :
( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) ) )
=> ! [X5: a,X6: a,X7: a] :
( ~ ( ~ ( ~ ( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) )
=> ( ( X1 @ X5 @ X7 )
!= X3 ) )
=> ( ( X2 @ X5 @ X7 )
!= X4 ) )
=> ( X6 = X7 ) ) ) ).
thf(h0,negated_conjecture,
~ ! [X1: a > a > a,X2: a > a > a,X3: a,X4: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X5: a] :
( ( X1 @ X5 @ X5 )
= X5 )
=> ~ ! [X5: a] :
( ( X2 @ X5 @ X5 )
= X5 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ ( X1 @ X5 @ X6 ) @ X7 )
= ( X1 @ X5 @ ( X1 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ ( X2 @ X5 @ X6 ) @ X7 )
= ( X2 @ X5 @ ( X2 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ X5 @ X6 )
= ( X1 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ X5 @ X6 )
= ( X2 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ ( X2 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ ( X1 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ X5 @ ( X1 @ X6 @ X7 ) )
= ( X1 @ ( X2 @ X5 @ X6 ) @ ( X2 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ X5 @ ( X2 @ X6 @ X7 ) )
= ( X2 @ ( X1 @ X5 @ X6 ) @ ( X1 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a] :
( ( X2 @ X3 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
( ( X1 @ X3 @ X5 )
= X3 ) )
=> ~ ! [X5: a] :
( ( X2 @ X4 @ X5 )
= X4 ) )
=> ~ ! [X5: a] :
( ( X1 @ X4 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
~ ! [X6: a] :
( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) ) )
=> ! [X5: a,X6: a,X7: a] :
( ~ ( ~ ( ~ ( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) )
=> ( ( X1 @ X5 @ X7 )
!= X3 ) )
=> ( ( X2 @ X5 @ X7 )
!= X4 ) )
=> ( X6 = X7 ) ) ),
inference(assume_negation,[status(cth)],[cCD_LATTICE_THM_pme]) ).
thf(ax7,axiom,
( p1
| ~ p2 ),
file('<stdin>',ax7) ).
thf(ax8,axiom,
~ p1,
file('<stdin>',ax8) ).
thf(ax6,axiom,
( p2
| ~ p3 ),
file('<stdin>',ax6) ).
thf(nax3,axiom,
( p3
<= ! [X1: a,X2: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X3: a] :
( ( f__0 @ X3 @ X3 )
= X3 )
=> ~ ! [X3: a] :
( ( f__1 @ X3 @ X3 )
= X3 ) )
=> ~ ! [X3: a,X4: a,X5: a] :
( ( f__0 @ ( f__0 @ X3 @ X4 ) @ X5 )
= ( f__0 @ X3 @ ( f__0 @ X4 @ X5 ) ) ) )
=> ~ ! [X3: a,X4: a,X5: a] :
( ( f__1 @ ( f__1 @ X3 @ X4 ) @ X5 )
= ( f__1 @ X3 @ ( f__1 @ X4 @ X5 ) ) ) )
=> ~ ! [X3: a,X4: a] :
( ( f__0 @ X3 @ X4 )
= ( f__0 @ X4 @ X3 ) ) )
=> ~ ! [X3: a,X4: a] :
( ( f__1 @ X3 @ X4 )
= ( f__1 @ X4 @ X3 ) ) )
=> ~ ! [X3: a,X4: a] :
( ( f__0 @ ( f__1 @ X3 @ X4 ) @ X4 )
= X4 ) )
=> ~ ! [X3: a,X4: a] :
( ( f__1 @ ( f__0 @ X3 @ X4 ) @ X4 )
= X4 ) )
=> ~ ! [X3: a,X4: a,X5: a] :
( ( f__1 @ X3 @ ( f__0 @ X4 @ X5 ) )
= ( f__0 @ ( f__1 @ X3 @ X4 ) @ ( f__1 @ X3 @ X5 ) ) ) )
=> ~ ! [X3: a,X4: a,X5: a] :
( ( f__0 @ X3 @ ( f__1 @ X4 @ X5 ) )
= ( f__1 @ ( f__0 @ X3 @ X4 ) @ ( f__0 @ X3 @ X5 ) ) ) )
=> ~ ! [X3: a] :
( ( f__1 @ X1 @ X3 )
= X3 ) )
=> ~ ! [X3: a] :
( ( f__0 @ X1 @ X3 )
= X1 ) )
=> ~ ! [X3: a] :
( ( f__1 @ X2 @ X3 )
= X2 ) )
=> ~ ! [X3: a] :
( ( f__0 @ X2 @ X3 )
= X3 ) )
=> ~ ! [X3: a] :
~ ! [X4: a] :
( ( ( f__0 @ X3 @ X4 )
= X1 )
=> ( ( f__1 @ X3 @ X4 )
!= X2 ) ) )
=> ! [X3: a,X4: a,X5: a] :
( ~ ( ~ ( ~ ( ( ( f__0 @ X3 @ X4 )
= X1 )
=> ( ( f__1 @ X3 @ X4 )
!= X2 ) )
=> ( ( f__0 @ X3 @ X5 )
!= X1 ) )
=> ( ( f__1 @ X3 @ X5 )
!= X2 ) )
=> ( X4 = X5 ) ) ) ),
file('<stdin>',nax3) ).
thf(nax2,axiom,
( p2
<= ! [X6: a > a > a,X2: a,X3: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X4: a] :
( ( f__0 @ X4 @ X4 )
= X4 )
=> ~ ! [X4: a] :
( ( X6 @ X4 @ X4 )
= X4 ) )
=> ~ ! [X4: a,X5: a,X7: a] :
( ( f__0 @ ( f__0 @ X4 @ X5 ) @ X7 )
= ( f__0 @ X4 @ ( f__0 @ X5 @ X7 ) ) ) )
=> ~ ! [X4: a,X5: a,X7: a] :
( ( X6 @ ( X6 @ X4 @ X5 ) @ X7 )
= ( X6 @ X4 @ ( X6 @ X5 @ X7 ) ) ) )
=> ~ ! [X4: a,X5: a] :
( ( f__0 @ X4 @ X5 )
= ( f__0 @ X5 @ X4 ) ) )
=> ~ ! [X4: a,X5: a] :
( ( X6 @ X4 @ X5 )
= ( X6 @ X5 @ X4 ) ) )
=> ~ ! [X4: a,X5: a] :
( ( f__0 @ ( X6 @ X4 @ X5 ) @ X5 )
= X5 ) )
=> ~ ! [X4: a,X5: a] :
( ( X6 @ ( f__0 @ X4 @ X5 ) @ X5 )
= X5 ) )
=> ~ ! [X4: a,X5: a,X7: a] :
( ( X6 @ X4 @ ( f__0 @ X5 @ X7 ) )
= ( f__0 @ ( X6 @ X4 @ X5 ) @ ( X6 @ X4 @ X7 ) ) ) )
=> ~ ! [X4: a,X5: a,X7: a] :
( ( f__0 @ X4 @ ( X6 @ X5 @ X7 ) )
= ( X6 @ ( f__0 @ X4 @ X5 ) @ ( f__0 @ X4 @ X7 ) ) ) )
=> ~ ! [X4: a] :
( ( X6 @ X2 @ X4 )
= X4 ) )
=> ~ ! [X4: a] :
( ( f__0 @ X2 @ X4 )
= X2 ) )
=> ~ ! [X4: a] :
( ( X6 @ X3 @ X4 )
= X3 ) )
=> ~ ! [X4: a] :
( ( f__0 @ X3 @ X4 )
= X4 ) )
=> ~ ! [X4: a] :
~ ! [X5: a] :
( ( ( f__0 @ X4 @ X5 )
= X2 )
=> ( ( X6 @ X4 @ X5 )
!= X3 ) ) )
=> ! [X4: a,X5: a,X7: a] :
( ~ ( ~ ( ~ ( ( ( f__0 @ X4 @ X5 )
= X2 )
=> ( ( X6 @ X4 @ X5 )
!= X3 ) )
=> ( ( f__0 @ X4 @ X7 )
!= X2 ) )
=> ( ( X6 @ X4 @ X7 )
!= X3 ) )
=> ( X5 = X7 ) ) ) ),
file('<stdin>',nax2) ).
thf(ax5,axiom,
( p3
| ~ p4 ),
file('<stdin>',ax5) ).
thf(ax4,axiom,
( p4
| ~ p5 ),
file('<stdin>',ax4) ).
thf(nax5,axiom,
( p5
<= ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X1: a] :
( ( f__0 @ X1 @ X1 )
= X1 )
=> ~ ! [X1: a] :
( ( f__1 @ X1 @ X1 )
= X1 ) )
=> ~ ! [X1: a,X2: a,X3: a] :
( ( f__0 @ ( f__0 @ X1 @ X2 ) @ X3 )
= ( f__0 @ X1 @ ( f__0 @ X2 @ X3 ) ) ) )
=> ~ ! [X1: a,X2: a,X3: a] :
( ( f__1 @ ( f__1 @ X1 @ X2 ) @ X3 )
= ( f__1 @ X1 @ ( f__1 @ X2 @ X3 ) ) ) )
=> ~ ! [X1: a,X2: a] :
( ( f__0 @ X1 @ X2 )
= ( f__0 @ X2 @ X1 ) ) )
=> ~ ! [X1: a,X2: a] :
( ( f__1 @ X1 @ X2 )
= ( f__1 @ X2 @ X1 ) ) )
=> ~ ! [X1: a,X2: a] :
( ( f__0 @ ( f__1 @ X1 @ X2 ) @ X2 )
= X2 ) )
=> ~ ! [X1: a,X2: a] :
( ( f__1 @ ( f__0 @ X1 @ X2 ) @ X2 )
= X2 ) )
=> ~ ! [X1: a,X2: a,X3: a] :
( ( f__1 @ X1 @ ( f__0 @ X2 @ X3 ) )
= ( f__0 @ ( f__1 @ X1 @ X2 ) @ ( f__1 @ X1 @ X3 ) ) ) )
=> ~ ! [X1: a,X2: a,X3: a] :
( ( f__0 @ X1 @ ( f__1 @ X2 @ X3 ) )
= ( f__1 @ ( f__0 @ X1 @ X2 ) @ ( f__0 @ X1 @ X3 ) ) ) )
=> ~ ! [X1: a] :
( ( f__1 @ f__2 @ X1 )
= X1 ) )
=> ~ ! [X1: a] :
( ( f__0 @ f__2 @ X1 )
= f__2 ) )
=> ~ ! [X1: a] :
( ( f__1 @ f__3 @ X1 )
= f__3 ) )
=> ~ ! [X1: a] :
( ( f__0 @ f__3 @ X1 )
= X1 ) )
=> ~ ! [X1: a] :
~ ! [X2: a] :
( ( ( f__0 @ X1 @ X2 )
= f__2 )
=> ( ( f__1 @ X1 @ X2 )
!= f__3 ) ) )
=> ! [X1: a,X2: a,X3: a] :
( ~ ( ~ ( ~ ( ( ( f__0 @ X1 @ X2 )
= f__2 )
=> ( ( f__1 @ X1 @ X2 )
!= f__3 ) )
=> ( ( f__0 @ X1 @ X3 )
!= f__2 ) )
=> ( ( f__1 @ X1 @ X3 )
!= f__3 ) )
=> ( X2 = X3 ) ) ) ),
file('<stdin>',nax5) ).
thf(nax4,axiom,
( p4
<= ! [X1: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X2: a] :
( ( f__0 @ X2 @ X2 )
= X2 )
=> ~ ! [X2: a] :
( ( f__1 @ X2 @ X2 )
= X2 ) )
=> ~ ! [X2: a,X3: a,X4: a] :
( ( f__0 @ ( f__0 @ X2 @ X3 ) @ X4 )
= ( f__0 @ X2 @ ( f__0 @ X3 @ X4 ) ) ) )
=> ~ ! [X2: a,X3: a,X4: a] :
( ( f__1 @ ( f__1 @ X2 @ X3 ) @ X4 )
= ( f__1 @ X2 @ ( f__1 @ X3 @ X4 ) ) ) )
=> ~ ! [X2: a,X3: a] :
( ( f__0 @ X2 @ X3 )
= ( f__0 @ X3 @ X2 ) ) )
=> ~ ! [X2: a,X3: a] :
( ( f__1 @ X2 @ X3 )
= ( f__1 @ X3 @ X2 ) ) )
=> ~ ! [X2: a,X3: a] :
( ( f__0 @ ( f__1 @ X2 @ X3 ) @ X3 )
= X3 ) )
=> ~ ! [X2: a,X3: a] :
( ( f__1 @ ( f__0 @ X2 @ X3 ) @ X3 )
= X3 ) )
=> ~ ! [X2: a,X3: a,X4: a] :
( ( f__1 @ X2 @ ( f__0 @ X3 @ X4 ) )
= ( f__0 @ ( f__1 @ X2 @ X3 ) @ ( f__1 @ X2 @ X4 ) ) ) )
=> ~ ! [X2: a,X3: a,X4: a] :
( ( f__0 @ X2 @ ( f__1 @ X3 @ X4 ) )
= ( f__1 @ ( f__0 @ X2 @ X3 ) @ ( f__0 @ X2 @ X4 ) ) ) )
=> ~ ! [X2: a] :
( ( f__1 @ f__2 @ X2 )
= X2 ) )
=> ~ ! [X2: a] :
( ( f__0 @ f__2 @ X2 )
= f__2 ) )
=> ~ ! [X2: a] :
( ( f__1 @ X1 @ X2 )
= X1 ) )
=> ~ ! [X2: a] :
( ( f__0 @ X1 @ X2 )
= X2 ) )
=> ~ ! [X2: a] :
~ ! [X3: a] :
( ( ( f__0 @ X2 @ X3 )
= f__2 )
=> ( ( f__1 @ X2 @ X3 )
!= X1 ) ) )
=> ! [X2: a,X3: a,X4: a] :
( ~ ( ~ ( ~ ( ( ( f__0 @ X2 @ X3 )
= f__2 )
=> ( ( f__1 @ X2 @ X3 )
!= X1 ) )
=> ( ( f__0 @ X2 @ X4 )
!= f__2 ) )
=> ( ( f__1 @ X2 @ X4 )
!= X1 ) )
=> ( X3 = X4 ) ) ) ),
file('<stdin>',nax4) ).
thf(c_0_9,plain,
( p1
| ~ p2 ),
inference(fof_simplification,[status(thm)],[ax7]) ).
thf(c_0_10,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax8]) ).
thf(c_0_11,plain,
( p2
| ~ p3 ),
inference(fof_simplification,[status(thm)],[ax6]) ).
thf(c_0_12,plain,
( p1
| ~ p2 ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
thf(c_0_13,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_14,plain,
! [X293: a,X294: a,X295: a,X296: a,X297: a,X298: a,X299: a,X300: a,X301: a,X302: a,X303: a,X304: a,X305: a,X306: a,X307: a,X308: a,X309: a,X310: a,X311: a,X312: a,X313: a,X314: a,X315: a,X316: a,X317: a,X318: a,X319: a] :
( ( ( ( f__0 @ X293 @ X293 )
= X293 )
| p3 )
& ( ( ( f__1 @ X294 @ X294 )
= X294 )
| p3 )
& ( ( ( f__0 @ ( f__0 @ X295 @ X296 ) @ X297 )
= ( f__0 @ X295 @ ( f__0 @ X296 @ X297 ) ) )
| p3 )
& ( ( ( f__1 @ ( f__1 @ X298 @ X299 ) @ X300 )
= ( f__1 @ X298 @ ( f__1 @ X299 @ X300 ) ) )
| p3 )
& ( ( ( f__0 @ X301 @ X302 )
= ( f__0 @ X302 @ X301 ) )
| p3 )
& ( ( ( f__1 @ X303 @ X304 )
= ( f__1 @ X304 @ X303 ) )
| p3 )
& ( ( ( f__0 @ ( f__1 @ X305 @ X306 ) @ X306 )
= X306 )
| p3 )
& ( ( ( f__1 @ ( f__0 @ X307 @ X308 ) @ X308 )
= X308 )
| p3 )
& ( ( ( f__1 @ X309 @ ( f__0 @ X310 @ X311 ) )
= ( f__0 @ ( f__1 @ X309 @ X310 ) @ ( f__1 @ X309 @ X311 ) ) )
| p3 )
& ( ( ( f__0 @ X312 @ ( f__1 @ X313 @ X314 ) )
= ( f__1 @ ( f__0 @ X312 @ X313 ) @ ( f__0 @ X312 @ X314 ) ) )
| p3 )
& ( ( ( f__1 @ esk152_0 @ X315 )
= X315 )
| p3 )
& ( ( ( f__0 @ esk152_0 @ X316 )
= esk152_0 )
| p3 )
& ( ( ( f__1 @ esk153_0 @ X317 )
= esk153_0 )
| p3 )
& ( ( ( f__0 @ esk153_0 @ X318 )
= X318 )
| p3 )
& ( ( ( f__0 @ X319 @ ( esk154_1 @ X319 ) )
= esk152_0 )
| p3 )
& ( ( ( f__1 @ X319 @ ( esk154_1 @ X319 ) )
= esk153_0 )
| p3 )
& ( ( ( f__0 @ esk155_0 @ esk156_0 )
= esk152_0 )
| p3 )
& ( ( ( f__1 @ esk155_0 @ esk156_0 )
= esk153_0 )
| p3 )
& ( ( ( f__0 @ esk155_0 @ esk157_0 )
= esk152_0 )
| p3 )
& ( ( ( f__1 @ esk155_0 @ esk157_0 )
= esk153_0 )
| p3 )
& ( ( esk156_0 != esk157_0 )
| p3 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])])])])]) ).
thf(c_0_15,plain,
( p2
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
thf(c_0_16,plain,
~ p2,
inference(sr,[status(thm)],[c_0_12,c_0_13]) ).
thf(c_0_17,plain,
! [X361: a,X362: a,X363: a,X364: a,X365: a,X366: a,X367: a,X368: a,X369: a,X370: a,X371: a,X372: a,X373: a,X374: a,X375: a,X376: a,X377: a,X378: a,X379: a,X380: a,X381: a,X382: a,X383: a,X384: a,X385: a,X386: a,X387: a] :
( ( ( ( f__0 @ X361 @ X361 )
= X361 )
| p2 )
& ( ( ( esk185_0 @ X362 @ X362 )
= X362 )
| p2 )
& ( ( ( f__0 @ ( f__0 @ X363 @ X364 ) @ X365 )
= ( f__0 @ X363 @ ( f__0 @ X364 @ X365 ) ) )
| p2 )
& ( ( ( esk185_0 @ ( esk185_0 @ X366 @ X367 ) @ X368 )
= ( esk185_0 @ X366 @ ( esk185_0 @ X367 @ X368 ) ) )
| p2 )
& ( ( ( f__0 @ X369 @ X370 )
= ( f__0 @ X370 @ X369 ) )
| p2 )
& ( ( ( esk185_0 @ X371 @ X372 )
= ( esk185_0 @ X372 @ X371 ) )
| p2 )
& ( ( ( f__0 @ ( esk185_0 @ X373 @ X374 ) @ X374 )
= X374 )
| p2 )
& ( ( ( esk185_0 @ ( f__0 @ X375 @ X376 ) @ X376 )
= X376 )
| p2 )
& ( ( ( esk185_0 @ X377 @ ( f__0 @ X378 @ X379 ) )
= ( f__0 @ ( esk185_0 @ X377 @ X378 ) @ ( esk185_0 @ X377 @ X379 ) ) )
| p2 )
& ( ( ( f__0 @ X380 @ ( esk185_0 @ X381 @ X382 ) )
= ( esk185_0 @ ( f__0 @ X380 @ X381 ) @ ( f__0 @ X380 @ X382 ) ) )
| p2 )
& ( ( ( esk185_0 @ esk186_0 @ X383 )
= X383 )
| p2 )
& ( ( ( f__0 @ esk186_0 @ X384 )
= esk186_0 )
| p2 )
& ( ( ( esk185_0 @ esk187_0 @ X385 )
= esk187_0 )
| p2 )
& ( ( ( f__0 @ esk187_0 @ X386 )
= X386 )
| p2 )
& ( ( ( f__0 @ X387 @ ( esk188_1 @ X387 ) )
= esk186_0 )
| p2 )
& ( ( ( esk185_0 @ X387 @ ( esk188_1 @ X387 ) )
= esk187_0 )
| p2 )
& ( ( ( f__0 @ esk189_0 @ esk190_0 )
= esk186_0 )
| p2 )
& ( ( ( esk185_0 @ esk189_0 @ esk190_0 )
= esk187_0 )
| p2 )
& ( ( ( f__0 @ esk189_0 @ esk191_0 )
= esk186_0 )
| p2 )
& ( ( ( esk185_0 @ esk189_0 @ esk191_0 )
= esk187_0 )
| p2 )
& ( ( esk190_0 != esk191_0 )
| p2 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax2])])])])])]) ).
thf(c_0_18,plain,
( p3
| ~ p4 ),
inference(fof_simplification,[status(thm)],[ax5]) ).
thf(c_0_19,plain,
! [X1: a,X2: a] :
( ( ( f__0 @ ( f__1 @ X1 @ X2 ) @ X2 )
= X2 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_20,plain,
~ p3,
inference(sr,[status(thm)],[c_0_15,c_0_16]) ).
thf(c_0_21,plain,
! [X2: a,X1: a] :
( ( ( f__0 @ X1 @ X2 )
= ( f__0 @ X2 @ X1 ) )
| p2 ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
thf(c_0_22,plain,
( p4
| ~ p5 ),
inference(fof_simplification,[status(thm)],[ax4]) ).
thf(c_0_23,plain,
( p3
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
thf(c_0_24,plain,
! [X1: a,X2: a] :
( ( f__0 @ ( f__1 @ X1 @ X2 ) @ X2 )
= X2 ),
inference(sr,[status(thm)],[c_0_19,c_0_20]) ).
thf(c_0_25,plain,
! [X2: a,X1: a] :
( ( f__0 @ X1 @ X2 )
= ( f__0 @ X2 @ X1 ) ),
inference(sr,[status(thm)],[c_0_21,c_0_16]) ).
thf(c_0_26,plain,
! [X1: a] :
( ( ( f__1 @ esk153_0 @ X1 )
= esk153_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_27,plain,
! [X163: a,X164: a,X165: a,X166: a,X167: a,X168: a,X169: a,X170: a,X171: a,X172: a,X173: a,X174: a,X175: a,X176: a,X177: a,X178: a,X179: a,X180: a,X181: a,X182: a,X183: a,X184: a,X185: a,X186: a,X187: a,X188: a,X189: a] :
( ( ( ( f__0 @ X163 @ X163 )
= X163 )
| p5 )
& ( ( ( f__1 @ X164 @ X164 )
= X164 )
| p5 )
& ( ( ( f__0 @ ( f__0 @ X165 @ X166 ) @ X167 )
= ( f__0 @ X165 @ ( f__0 @ X166 @ X167 ) ) )
| p5 )
& ( ( ( f__1 @ ( f__1 @ X168 @ X169 ) @ X170 )
= ( f__1 @ X168 @ ( f__1 @ X169 @ X170 ) ) )
| p5 )
& ( ( ( f__0 @ X171 @ X172 )
= ( f__0 @ X172 @ X171 ) )
| p5 )
& ( ( ( f__1 @ X173 @ X174 )
= ( f__1 @ X174 @ X173 ) )
| p5 )
& ( ( ( f__0 @ ( f__1 @ X175 @ X176 ) @ X176 )
= X176 )
| p5 )
& ( ( ( f__1 @ ( f__0 @ X177 @ X178 ) @ X178 )
= X178 )
| p5 )
& ( ( ( f__1 @ X179 @ ( f__0 @ X180 @ X181 ) )
= ( f__0 @ ( f__1 @ X179 @ X180 ) @ ( f__1 @ X179 @ X181 ) ) )
| p5 )
& ( ( ( f__0 @ X182 @ ( f__1 @ X183 @ X184 ) )
= ( f__1 @ ( f__0 @ X182 @ X183 ) @ ( f__0 @ X182 @ X184 ) ) )
| p5 )
& ( ( ( f__1 @ f__2 @ X185 )
= X185 )
| p5 )
& ( ( ( f__0 @ f__2 @ X186 )
= f__2 )
| p5 )
& ( ( ( f__1 @ f__3 @ X187 )
= f__3 )
| p5 )
& ( ( ( f__0 @ f__3 @ X188 )
= X188 )
| p5 )
& ( ( ( f__0 @ X189 @ ( esk89_1 @ X189 ) )
= f__2 )
| p5 )
& ( ( ( f__1 @ X189 @ ( esk89_1 @ X189 ) )
= f__3 )
| p5 )
& ( ( ( f__0 @ esk90_0 @ esk91_0 )
= f__2 )
| p5 )
& ( ( ( f__1 @ esk90_0 @ esk91_0 )
= f__3 )
| p5 )
& ( ( ( f__0 @ esk90_0 @ esk92_0 )
= f__2 )
| p5 )
& ( ( ( f__1 @ esk90_0 @ esk92_0 )
= f__3 )
| p5 )
& ( ( esk91_0 != esk92_0 )
| p5 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax5])])])])])]) ).
thf(c_0_28,plain,
( p4
| ~ p5 ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
thf(c_0_29,plain,
~ p4,
inference(sr,[status(thm)],[c_0_23,c_0_20]) ).
thf(c_0_30,plain,
! [X1: a,X2: a] :
( ( ( f__1 @ ( f__0 @ X1 @ X2 ) @ X2 )
= X2 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_31,plain,
! [X2: a,X1: a] :
( ( ( f__1 @ X1 @ X2 )
= ( f__1 @ X2 @ X1 ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_32,plain,
! [X2: a,X1: a] :
( ( f__0 @ X1 @ ( f__1 @ X2 @ X1 ) )
= X1 ),
inference(rw,[status(thm)],[c_0_24,c_0_25]) ).
thf(c_0_33,plain,
! [X1: a] :
( ( f__1 @ esk153_0 @ X1 )
= esk153_0 ),
inference(sr,[status(thm)],[c_0_26,c_0_20]) ).
thf(c_0_34,plain,
! [X1: a] :
( ( ( f__0 @ f__3 @ X1 )
= X1 )
| p5 ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
thf(c_0_35,plain,
~ p5,
inference(sr,[status(thm)],[c_0_28,c_0_29]) ).
thf(c_0_36,plain,
! [X227: a,X228: a,X229: a,X230: a,X231: a,X232: a,X233: a,X234: a,X235: a,X236: a,X237: a,X238: a,X239: a,X240: a,X241: a,X242: a,X243: a,X244: a,X245: a,X246: a,X247: a,X248: a,X249: a,X250: a,X251: a,X252: a,X253: a] :
( ( ( ( f__0 @ X227 @ X227 )
= X227 )
| p4 )
& ( ( ( f__1 @ X228 @ X228 )
= X228 )
| p4 )
& ( ( ( f__0 @ ( f__0 @ X229 @ X230 ) @ X231 )
= ( f__0 @ X229 @ ( f__0 @ X230 @ X231 ) ) )
| p4 )
& ( ( ( f__1 @ ( f__1 @ X232 @ X233 ) @ X234 )
= ( f__1 @ X232 @ ( f__1 @ X233 @ X234 ) ) )
| p4 )
& ( ( ( f__0 @ X235 @ X236 )
= ( f__0 @ X236 @ X235 ) )
| p4 )
& ( ( ( f__1 @ X237 @ X238 )
= ( f__1 @ X238 @ X237 ) )
| p4 )
& ( ( ( f__0 @ ( f__1 @ X239 @ X240 ) @ X240 )
= X240 )
| p4 )
& ( ( ( f__1 @ ( f__0 @ X241 @ X242 ) @ X242 )
= X242 )
| p4 )
& ( ( ( f__1 @ X243 @ ( f__0 @ X244 @ X245 ) )
= ( f__0 @ ( f__1 @ X243 @ X244 ) @ ( f__1 @ X243 @ X245 ) ) )
| p4 )
& ( ( ( f__0 @ X246 @ ( f__1 @ X247 @ X248 ) )
= ( f__1 @ ( f__0 @ X246 @ X247 ) @ ( f__0 @ X246 @ X248 ) ) )
| p4 )
& ( ( ( f__1 @ f__2 @ X249 )
= X249 )
| p4 )
& ( ( ( f__0 @ f__2 @ X250 )
= f__2 )
| p4 )
& ( ( ( f__1 @ esk120_0 @ X251 )
= esk120_0 )
| p4 )
& ( ( ( f__0 @ esk120_0 @ X252 )
= X252 )
| p4 )
& ( ( ( f__0 @ X253 @ ( esk121_1 @ X253 ) )
= f__2 )
| p4 )
& ( ( ( f__1 @ X253 @ ( esk121_1 @ X253 ) )
= esk120_0 )
| p4 )
& ( ( ( f__0 @ esk122_0 @ esk123_0 )
= f__2 )
| p4 )
& ( ( ( f__1 @ esk122_0 @ esk123_0 )
= esk120_0 )
| p4 )
& ( ( ( f__0 @ esk122_0 @ esk124_0 )
= f__2 )
| p4 )
& ( ( ( f__1 @ esk122_0 @ esk124_0 )
= esk120_0 )
| p4 )
& ( ( esk123_0 != esk124_0 )
| p4 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax4])])])])])]) ).
thf(c_0_37,plain,
! [X1: a,X2: a] :
( ( f__1 @ ( f__0 @ X1 @ X2 ) @ X2 )
= X2 ),
inference(sr,[status(thm)],[c_0_30,c_0_20]) ).
thf(c_0_38,plain,
! [X2: a,X1: a] :
( ( f__1 @ X1 @ X2 )
= ( f__1 @ X2 @ X1 ) ),
inference(sr,[status(thm)],[c_0_31,c_0_20]) ).
thf(c_0_39,plain,
! [X1: a] :
( ( ( f__0 @ esk152_0 @ X1 )
= esk152_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_40,plain,
( ( ( f__1 @ esk155_0 @ esk157_0 )
= esk153_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_41,plain,
! [X1: a] :
( ( f__0 @ X1 @ esk153_0 )
= X1 ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
thf(c_0_42,plain,
! [X1: a] :
( ( f__0 @ f__3 @ X1 )
= X1 ),
inference(sr,[status(thm)],[c_0_34,c_0_35]) ).
thf(c_0_43,plain,
! [X1: a] :
( ( ( f__1 @ f__2 @ X1 )
= X1 )
| p4 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_44,plain,
! [X2: a,X1: a] :
( ( f__1 @ X1 @ ( f__0 @ X2 @ X1 ) )
= X1 ),
inference(rw,[status(thm)],[c_0_37,c_0_38]) ).
thf(c_0_45,plain,
! [X1: a] :
( ( f__0 @ esk152_0 @ X1 )
= esk152_0 ),
inference(sr,[status(thm)],[c_0_39,c_0_20]) ).
thf(c_0_46,plain,
! [X1: a,X2: a,X3: a] :
( ( ( f__1 @ X1 @ ( f__0 @ X2 @ X3 ) )
= ( f__0 @ ( f__1 @ X1 @ X2 ) @ ( f__1 @ X1 @ X3 ) ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_47,plain,
( ( f__1 @ esk155_0 @ esk157_0 )
= esk153_0 ),
inference(sr,[status(thm)],[c_0_40,c_0_20]) ).
thf(c_0_48,plain,
esk153_0 = f__3,
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
thf(c_0_49,plain,
! [X1: a] :
( ( ( f__0 @ X1 @ ( esk154_1 @ X1 ) )
= esk152_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_50,plain,
! [X1: a] :
( ( f__1 @ f__2 @ X1 )
= X1 ),
inference(sr,[status(thm)],[c_0_43,c_0_29]) ).
thf(c_0_51,plain,
! [X1: a] :
( ( f__1 @ X1 @ esk152_0 )
= X1 ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
thf(c_0_52,plain,
! [X1: a] :
( ( ( f__1 @ X1 @ ( esk154_1 @ X1 ) )
= esk153_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_53,plain,
( ( ( f__0 @ esk155_0 @ esk157_0 )
= esk152_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_54,plain,
! [X1: a,X2: a,X3: a] :
( ( f__0 @ ( f__1 @ X1 @ X2 ) @ ( f__1 @ X1 @ X3 ) )
= ( f__1 @ X1 @ ( f__0 @ X2 @ X3 ) ) ),
inference(sr,[status(thm)],[c_0_46,c_0_20]) ).
thf(c_0_55,plain,
( ( f__1 @ esk155_0 @ esk157_0 )
= f__3 ),
inference(rw,[status(thm)],[c_0_47,c_0_48]) ).
thf(c_0_56,plain,
! [X1: a] :
( ( f__0 @ X1 @ ( esk154_1 @ X1 ) )
= esk152_0 ),
inference(sr,[status(thm)],[c_0_49,c_0_20]) ).
thf(c_0_57,plain,
esk152_0 = f__2,
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
thf(c_0_58,plain,
( ( ( f__1 @ esk155_0 @ esk156_0 )
= esk153_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_59,plain,
! [X1: a] :
( ( f__1 @ X1 @ ( esk154_1 @ X1 ) )
= esk153_0 ),
inference(sr,[status(thm)],[c_0_52,c_0_20]) ).
thf(c_0_60,plain,
! [X1: a,X2: a,X3: a] :
( ( ( f__0 @ X1 @ ( f__1 @ X2 @ X3 ) )
= ( f__1 @ ( f__0 @ X1 @ X2 ) @ ( f__0 @ X1 @ X3 ) ) )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_61,plain,
( ( f__0 @ esk155_0 @ esk157_0 )
= esk152_0 ),
inference(sr,[status(thm)],[c_0_53,c_0_20]) ).
thf(c_0_62,plain,
! [X1: a] :
( ( f__1 @ esk155_0 @ ( f__0 @ esk157_0 @ X1 ) )
= ( f__1 @ esk155_0 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_42]) ).
thf(c_0_63,plain,
! [X1: a] :
( ( f__0 @ X1 @ ( esk154_1 @ X1 ) )
= f__2 ),
inference(rw,[status(thm)],[c_0_56,c_0_57]) ).
thf(c_0_64,plain,
! [X1: a] :
( ( f__1 @ X1 @ f__2 )
= X1 ),
inference(rw,[status(thm)],[c_0_51,c_0_57]) ).
thf(c_0_65,plain,
( ( f__1 @ esk155_0 @ esk156_0 )
= esk153_0 ),
inference(sr,[status(thm)],[c_0_58,c_0_20]) ).
thf(c_0_66,plain,
! [X1: a] :
( ( f__1 @ X1 @ ( esk154_1 @ X1 ) )
= f__3 ),
inference(rw,[status(thm)],[c_0_59,c_0_48]) ).
thf(c_0_67,plain,
! [X1: a,X2: a,X3: a] :
( ( f__1 @ ( f__0 @ X1 @ X2 ) @ ( f__0 @ X1 @ X3 ) )
= ( f__0 @ X1 @ ( f__1 @ X2 @ X3 ) ) ),
inference(sr,[status(thm)],[c_0_60,c_0_20]) ).
thf(c_0_68,plain,
( ( f__0 @ esk155_0 @ esk157_0 )
= f__2 ),
inference(rw,[status(thm)],[c_0_61,c_0_57]) ).
thf(c_0_69,plain,
( ( f__1 @ esk155_0 @ ( esk154_1 @ esk157_0 ) )
= esk155_0 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63]),c_0_64]) ).
thf(c_0_70,plain,
( ( ( f__0 @ esk155_0 @ esk156_0 )
= esk152_0 )
| p3 ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_71,plain,
( ( f__1 @ esk155_0 @ esk156_0 )
= f__3 ),
inference(rw,[status(thm)],[c_0_65,c_0_48]) ).
thf(c_0_72,plain,
! [X1: a,X2: a] :
( ( f__1 @ X1 @ ( f__0 @ ( esk154_1 @ X1 ) @ X2 ) )
= ( f__1 @ X1 @ X2 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_66]),c_0_42]) ).
thf(c_0_73,plain,
! [X1: a] :
( ( f__0 @ esk155_0 @ ( f__1 @ esk157_0 @ X1 ) )
= ( f__0 @ esk155_0 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_68]),c_0_50]) ).
thf(c_0_74,plain,
! [X1: a] :
( ( f__0 @ X1 @ f__3 )
= X1 ),
inference(rw,[status(thm)],[c_0_41,c_0_48]) ).
thf(c_0_75,plain,
( ( f__0 @ esk155_0 @ ( esk154_1 @ esk157_0 ) )
= ( esk154_1 @ esk157_0 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_69]),c_0_25]) ).
thf(c_0_76,plain,
( ( f__0 @ esk155_0 @ esk156_0 )
= esk152_0 ),
inference(sr,[status(thm)],[c_0_70,c_0_20]) ).
thf(c_0_77,plain,
! [X1: a] :
( ( f__1 @ esk155_0 @ ( f__0 @ esk156_0 @ X1 ) )
= ( f__1 @ esk155_0 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_71]),c_0_42]) ).
thf(c_0_78,plain,
! [X1: a] :
( ( f__1 @ X1 @ ( esk154_1 @ ( esk154_1 @ X1 ) ) )
= X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_63]),c_0_64]) ).
thf(c_0_79,plain,
( ( esk154_1 @ esk157_0 )
= esk155_0 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_66]),c_0_74]),c_0_75]) ).
thf(c_0_80,plain,
! [X1: a,X2: a] :
( ( f__0 @ X1 @ ( f__1 @ ( esk154_1 @ X1 ) @ X2 ) )
= ( f__0 @ X1 @ X2 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_63]),c_0_50]) ).
thf(c_0_81,plain,
( ( f__0 @ esk155_0 @ esk156_0 )
= f__2 ),
inference(rw,[status(thm)],[c_0_76,c_0_57]) ).
thf(c_0_82,plain,
( ( f__1 @ esk155_0 @ ( esk154_1 @ esk156_0 ) )
= esk155_0 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_63]),c_0_64]) ).
thf(c_0_83,plain,
( ( f__1 @ esk157_0 @ ( esk154_1 @ esk155_0 ) )
= esk157_0 ),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
thf(c_0_84,plain,
! [X1: a] :
( ( f__0 @ X1 @ ( esk154_1 @ ( esk154_1 @ X1 ) ) )
= X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_66]),c_0_74]) ).
thf(c_0_85,plain,
! [X1: a] :
( ( f__0 @ esk155_0 @ ( f__1 @ esk156_0 @ X1 ) )
= ( f__0 @ esk155_0 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_81]),c_0_50]) ).
thf(c_0_86,plain,
( ( f__0 @ esk155_0 @ ( esk154_1 @ esk156_0 ) )
= ( esk154_1 @ esk156_0 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_82]),c_0_25]) ).
thf(c_0_87,plain,
( ( f__0 @ esk157_0 @ ( esk154_1 @ esk155_0 ) )
= ( esk154_1 @ esk155_0 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_83]),c_0_25]) ).
thf(c_0_88,plain,
( p3
| ( esk156_0 != esk157_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
thf(c_0_89,plain,
! [X1: a] :
( ( esk154_1 @ ( esk154_1 @ X1 ) )
= X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_84]),c_0_38]),c_0_78]) ).
thf(c_0_90,plain,
( ( esk154_1 @ esk156_0 )
= esk155_0 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_66]),c_0_74]),c_0_86]) ).
thf(c_0_91,plain,
( ( esk154_1 @ esk155_0 )
= esk157_0 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_79]),c_0_87]) ).
thf(c_0_92,plain,
esk157_0 != esk156_0,
inference(sr,[status(thm)],[c_0_88,c_0_20]) ).
thf(c_0_93,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_90]),c_0_91]),c_0_92]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
! [X1: a > a > a,X2: a > a > a,X3: a,X4: a] :
( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ~ ( ! [X5: a] :
( ( X1 @ X5 @ X5 )
= X5 )
=> ~ ! [X5: a] :
( ( X2 @ X5 @ X5 )
= X5 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ ( X1 @ X5 @ X6 ) @ X7 )
= ( X1 @ X5 @ ( X1 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ ( X2 @ X5 @ X6 ) @ X7 )
= ( X2 @ X5 @ ( X2 @ X6 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ X5 @ X6 )
= ( X1 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ X5 @ X6 )
= ( X2 @ X6 @ X5 ) ) )
=> ~ ! [X5: a,X6: a] :
( ( X1 @ ( X2 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a] :
( ( X2 @ ( X1 @ X5 @ X6 ) @ X6 )
= X6 ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X2 @ X5 @ ( X1 @ X6 @ X7 ) )
= ( X1 @ ( X2 @ X5 @ X6 ) @ ( X2 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a,X6: a,X7: a] :
( ( X1 @ X5 @ ( X2 @ X6 @ X7 ) )
= ( X2 @ ( X1 @ X5 @ X6 ) @ ( X1 @ X5 @ X7 ) ) ) )
=> ~ ! [X5: a] :
( ( X2 @ X3 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
( ( X1 @ X3 @ X5 )
= X3 ) )
=> ~ ! [X5: a] :
( ( X2 @ X4 @ X5 )
= X4 ) )
=> ~ ! [X5: a] :
( ( X1 @ X4 @ X5 )
= X5 ) )
=> ~ ! [X5: a] :
~ ! [X6: a] :
( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) ) )
=> ! [X5: a,X6: a,X7: a] :
( ~ ( ~ ( ~ ( ( ( X1 @ X5 @ X6 )
= X3 )
=> ( ( X2 @ X5 @ X6 )
!= X4 ) )
=> ( ( X1 @ X5 @ X7 )
!= X3 ) )
=> ( ( X2 @ X5 @ X7 )
!= X4 ) )
=> ( X6 = X7 ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SEU997^5 : TPTP v9.2.0. Released v4.0.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 21:41:08 EDT 2025
% 0.13/0.35 % CPUTime :
% 23.84/24.10 % SZS status Theorem
% 23.84/24.10 % Mode: mode371
% 23.84/24.10 % Inferences: 7
% 23.84/24.10 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------