%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SYO041^1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 : Wed Oct 7 11:07:27 AM UTC 2026
% Result : Unsatisfiable 35.13s 6.10s
% Output : CNFRefutation 35.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 1
% Syntax : Number of formulae : 712 ( 36 unt; 0 typ; 0 def)
% Number of atoms : 11907 (2843 equ; 0 cnn)
% Maximal formula atoms : 6 ( 16 avg)
% Number of connectives : 5653 ( 144 ~;1918 |; 12 &;3579 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 8 ( 5 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $o ).
thf(tp_f,type,
f: $o > $o ).
thf(tp_g,type,
g: $o > $o ).
thf(tp_x,type,
x: $o ).
thf(tp_y,type,
y: $o ).
thf(1,axiom,
( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',3) ).
thf(5,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[1]) ).
thf(7,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(extcnf_combined,[status(esa)],[5]) ).
thf(8,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(copy,[status(thm)],[7]) ).
thf(10,plain,
( ( ~ ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
| ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[8]) ).
thf(12,plain,
( ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
| ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[10]) ).
thf(13,plain,
( ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[12]) ).
thf(14,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[12]) ).
thf(15,plain,
( ( ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[13]) ).
thf(16,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[14]) ).
thf(17,plain,
( ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[15]) ).
thf(18,plain,
( ( ~ ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) )
| ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[16]) ).
thf(19,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[16]) ).
thf(20,plain,
( ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[17]) ).
thf(21,plain,
( ( ( g @ y )
!= x )
= $false ),
inference(extcnf_or_neg,[status(thm)],[17]) ).
thf(22,plain,
( ( ( ~ ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) ) )
= $true )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[18]) ).
thf(23,plain,
( ( ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[20]) ).
thf(24,plain,
( ( ( g @ y )
= x )
= $true ),
inference(extcnf_not_neg,[status(thm)],[21]) ).
thf(25,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[22]) ).
thf(26,plain,
( ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[23]) ).
thf(27,plain,
( ( ~ ( ( g @ y )
| x )
| ~ ( ~ ( g @ y )
| ~ x ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[24]) ).
thf(28,plain,
( ( ( g @ y )
= x )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[24]) ).
thf(29,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[25]) ).
thf(30,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[25]) ).
thf(31,plain,
( ( ~ ( ( x != y ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[26]) ).
thf(32,plain,
( ( ( g @ x )
!= y )
= $false ),
inference(extcnf_or_neg,[status(thm)],[26]) ).
thf(33,plain,
( ( ( ~ ( ( g @ y )
| x ) )
= $true )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[27]) ).
thf(34,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[29]) ).
thf(35,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[30]) ).
thf(36,plain,
( ( x != y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[31]) ).
thf(37,plain,
( ( ( g @ x )
= y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[32]) ).
thf(38,plain,
( ( ( ( g @ y )
| x )
= $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[33]) ).
thf(40,plain,
( ( ( ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[34]) ).
thf(41,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[35]) ).
thf(43,plain,
( ( x = y )
= $false ),
inference(extcnf_not_pos,[status(thm)],[36]) ).
thf(44,plain,
( ( ~ ( ( g @ x )
| y )
| ~ ( ~ ( g @ x )
| ~ y ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[37]) ).
thf(45,plain,
( ( ( g @ x )
= y )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[37]) ).
thf(46,plain,
( ( ( g @ y )
= $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[38]) ).
thf(47,plain,
( ( x = $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[38]) ).
thf(49,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[40]) ).
thf(50,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[41]) ).
thf(52,plain,
( ( ~ ( x
| y )
| ~ ( ~ x
| ~ y ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[43]) ).
thf(53,plain,
( ( x = y )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[43]) ).
thf(54,plain,
( ( ( ~ ( ( g @ x )
| y ) )
= $true )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[44]) ).
thf(55,plain,
( ( ( ~ ( g @ y )
| ~ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[46]) ).
thf(56,plain,
( ( ( ~ ( g @ y )
| ~ x )
= $false )
| ( x = $false ) ),
inference(extcnf_not_pos,[status(thm)],[47]) ).
thf(57,plain,
( ( ~ ( x
| y ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[52]) ).
thf(58,plain,
( ( ~ ( ~ x
| ~ y ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[52]) ).
thf(59,plain,
( ( ( ( g @ x )
| y )
= $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[54]) ).
thf(61,plain,
( ( ( ~ x ) = $false )
| ( ( g @ y )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[55]) ).
thf(62,plain,
( ( ( ~ ( g @ y ) )
= $false )
| ( x = $false ) ),
inference(extcnf_or_neg,[status(thm)],[56]) ).
thf(64,plain,
( ( x
| y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[57]) ).
thf(65,plain,
( ( ~ x
| ~ y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[58]) ).
thf(66,plain,
( ( ( g @ x )
= $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[59]) ).
thf(67,plain,
( ( y = $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[59]) ).
thf(69,plain,
( ( x = $true )
| ( ( g @ y )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[61]) ).
thf(70,plain,
( ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(extcnf_not_neg,[status(thm)],[62]) ).
thf(72,plain,
( ( x = $true )
| ( y = $true ) ),
inference(extcnf_or_pos,[status(thm)],[64]) ).
thf(73,plain,
( ( ( ~ x ) = $true )
| ( ( ~ y ) = $true ) ),
inference(extcnf_or_pos,[status(thm)],[65]) ).
thf(74,plain,
( ( ( ~ ( g @ x )
| ~ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[66]) ).
thf(75,plain,
( ( ( ~ ( g @ x )
| ~ y )
= $false )
| ( y = $false ) ),
inference(extcnf_not_pos,[status(thm)],[67]) ).
thf(76,plain,
( ( x = $false )
| ( ( ~ y ) = $true ) ),
inference(extcnf_not_pos,[status(thm)],[73]) ).
thf(78,plain,
( ( ( ~ y ) = $false )
| ( ( g @ x )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[74]) ).
thf(79,plain,
( ( ( ~ ( g @ x ) )
= $false )
| ( y = $false ) ),
inference(extcnf_or_neg,[status(thm)],[75]) ).
thf(81,plain,
( ( y = $false )
| ( x = $false ) ),
inference(extcnf_not_pos,[status(thm)],[76]) ).
thf(83,plain,
( ( y = $true )
| ( ( g @ x )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[78]) ).
thf(84,plain,
( ( ( g @ x )
= $true )
| ( y = $false ) ),
inference(extcnf_not_neg,[status(thm)],[79]) ).
thf(122,plain,
( ( ( x = y )
= ( ( g @ x )
= y ) )
= $false ),
inference(res,[status(thm)],[53,45]) ).
thf(123,plain,
( ( ( x = y )
= ( ( g @ y )
= x ) )
= $false ),
inference(res,[status(thm)],[53,28]) ).
thf(133,plain,
( ( y = $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[123]) ).
thf(134,plain,
( ( y = $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[123]) ).
thf(143,plain,
( ( x = $true )
| ( ( g @ x )
= $true ) ),
inference(extuni,[status(esa)],[122]) ).
thf(144,plain,
( ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[122]) ).
thf(278,plain,
( ( ( y = y )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[133,84]) ).
thf(291,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[133,50]) ).
thf(296,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[291]) ).
thf(302,plain,
( ( ( g @ x )
= $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[278]) ).
thf(303,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[296]) ).
thf(312,plain,
( ( ( y = y )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[134,83]) ).
thf(323,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[134,49]) ).
thf(333,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[323]) ).
thf(336,plain,
( ( ( g @ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[312]) ).
thf(341,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[333]) ).
thf(361,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[143,50]) ).
thf(366,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[361]) ).
thf(375,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[366]) ).
thf(399,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[144,49]) ).
thf(409,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[399]) ).
thf(419,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[409]) ).
thf(561,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[303,81]) ).
thf(577,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[303,49]) ).
thf(578,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[577]) ).
thf(581,plain,
( ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[561]) ).
thf(618,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[341,72]) ).
thf(629,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[341,50]) ).
thf(631,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[341,50]) ).
thf(644,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[631]) ).
thf(645,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[629]) ).
thf(646,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[629]) ).
thf(647,plain,
( ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[618]) ).
thf(659,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[375,341]) ).
thf(663,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[375,341]) ).
thf(708,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[375,49]) ).
thf(712,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[708]) ).
thf(718,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[663]) ).
thf(720,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[659]) ).
thf(723,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[712]) ).
thf(724,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[718]) ).
thf(725,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[720]) ).
thf(737,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[419,303]) ).
thf(741,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[419,303]) ).
thf(780,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[419,50]) ).
thf(797,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[780]) ).
thf(803,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[741]) ).
thf(805,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[737]) ).
thf(814,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[797]) ).
thf(815,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[803]) ).
thf(816,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[805]) ).
thf(818,plain,
( ( ( ( f @ x )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[578,419]) ).
thf(824,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[578,419]) ).
thf(840,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( y = $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[578,336]) ).
thf(878,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[578,49]) ).
thf(880,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[878]) ).
thf(881,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[878]) ).
thf(894,plain,
( ( ( g @ y )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[840]) ).
thf(903,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[824]) ).
thf(904,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[818]) ).
thf(905,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[881]) ).
thf(906,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[880]) ).
thf(909,plain,
( ( ( g @ y )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[894]) ).
thf(911,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[903]) ).
thf(919,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[581,419]) ).
thf(924,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[581,419]) ).
thf(926,plain,
( ( ( x = x )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[581,375]) ).
thf(928,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[581,341]) ).
thf(933,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[581,341]) ).
thf(979,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[581,49]) ).
thf(985,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[979]) ).
thf(991,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[933]) ).
thf(995,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[928]) ).
thf(996,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[926]) ).
thf(998,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[924]) ).
thf(1002,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[919]) ).
thf(1003,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[985]) ).
thf(1004,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[991]) ).
thf(1005,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[995]) ).
thf(1006,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(sim,[status(thm)],[996]) ).
thf(1007,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[998]) ).
thf(1008,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1002]) ).
thf(1009,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1006,419]) ).
thf(1014,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1006,419]) ).
thf(1015,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1006,341]) ).
thf(1020,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1006,341]) ).
thf(1049,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1006,49]) ).
thf(1050,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1006,49]) ).
thf(1051,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false ) ),
inference(fac_restr,[status(thm)],[1006]) ).
thf(1052,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1050]) ).
thf(1053,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1050]) ).
thf(1054,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1049]) ).
thf(1055,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1020]) ).
thf(1056,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1020]) ).
thf(1059,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1015]) ).
thf(1060,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1015]) ).
thf(1062,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1014]) ).
thf(1066,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1009]) ).
thf(1067,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[1051]) ).
thf(1068,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[1051]) ).
thf(1069,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1062]) ).
thf(1070,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1066]) ).
thf(1075,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1054,419]) ).
thf(1081,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1054,341]) ).
thf(1111,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1054,49]) ).
thf(1114,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1111]) ).
thf(1115,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1111]) ).
thf(1129,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1081]) ).
thf(1130,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1081]) ).
thf(1133,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1075]) ).
thf(1135,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1115]) ).
thf(1136,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1114]) ).
thf(1141,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1133]) ).
thf(1149,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[644,1006]) ).
thf(1159,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[644,302]) ).
thf(1191,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[644,50]) ).
thf(1206,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1191]) ).
thf(1207,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1191]) ).
thf(1220,plain,
( ( ( g @ y )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1159]) ).
thf(1224,plain,
( ( ( f @ x )
= $true )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1149]) ).
thf(1225,plain,
( ( ( f @ x )
= $true )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1149]) ).
thf(1228,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1207]) ).
thf(1229,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1206]) ).
thf(1232,plain,
( ( ( g @ y )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1220]) ).
thf(1234,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[647,1054]) ).
thf(1239,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[647,1006]) ).
thf(1240,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[647,1006]) ).
thf(1250,plain,
( ( ( x = x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[647,419]) ).
thf(1294,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[647,50]) ).
thf(1304,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1294]) ).
thf(1310,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1250]) ).
thf(1312,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1240]) ).
thf(1314,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1239]) ).
thf(1318,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1234]) ).
thf(1320,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1304]) ).
thf(1321,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(sim,[status(thm)],[1310]) ).
thf(1322,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1312]) ).
thf(1323,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1314]) ).
thf(1324,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1318]) ).
thf(1325,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1321,1054]) ).
thf(1330,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1321,1006]) ).
thf(1331,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1321,1006]) ).
thf(1357,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1321,50]) ).
thf(1358,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1321,50]) ).
thf(1367,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false ) ),
inference(fac_restr,[status(thm)],[1321]) ).
thf(1368,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1358]) ).
thf(1369,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1358]) ).
thf(1370,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1357]) ).
thf(1372,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1331]) ).
thf(1373,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1331]) ).
thf(1374,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1330]) ).
thf(1375,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1330]) ).
thf(1378,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1325]) ).
thf(1379,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1325]) ).
thf(1380,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[1367]) ).
thf(1381,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[1367]) ).
thf(1386,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1370,1006]) ).
thf(1391,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1370,302]) ).
thf(1393,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1370,302]) ).
thf(1403,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1370,84]) ).
thf(1411,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1370,70]) ).
thf(1414,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1370,50]) ).
thf(1426,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1414]) ).
thf(1427,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1414]) ).
thf(1429,plain,
( ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1411]) ).
thf(1431,plain,
( ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1403]) ).
thf(1437,plain,
( ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1393]) ).
thf(1439,plain,
( ( ( g @ x )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1391]) ).
thf(1441,plain,
( ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1386]) ).
thf(1442,plain,
( ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1386]) ).
thf(1445,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1427]) ).
thf(1446,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1426]) ).
thf(1447,plain,
( ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1429]) ).
thf(1448,plain,
( ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1431]) ).
thf(1449,plain,
( ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1437]) ).
thf(1450,plain,
( ( ( g @ x )
= $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1439]) ).
thf(1451,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1067,1370]) ).
thf(1452,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1067,1370]) ).
thf(1457,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1067,1321]) ).
thf(1458,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1067,1321]) ).
thf(1460,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1067,1321]) ).
thf(1474,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1067,144]) ).
thf(1489,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1067,81]) ).
thf(1495,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1067,70]) ).
thf(1505,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1067,49]) ).
thf(1506,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1067,49]) ).
thf(1508,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1506]) ).
thf(1510,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1506]) ).
thf(1511,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1506]) ).
thf(1512,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1505]) ).
thf(1513,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1495]) ).
thf(1514,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1489]) ).
thf(1515,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1474]) ).
thf(1518,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1460]) ).
thf(1523,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1458]) ).
thf(1524,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1457]) ).
thf(1525,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1452]) ).
thf(1527,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1451]) ).
thf(1529,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1508]) ).
thf(1530,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1518]) ).
thf(1531,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1523]) ).
thf(1532,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1525]) ).
thf(1533,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1527]) ).
thf(1534,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1068,1370]) ).
thf(1536,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1068,1321]) ).
thf(1537,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1068,1321]) ).
thf(1538,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1068,1068]) ).
thf(1540,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1068,1068]) ).
thf(1548,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1068,1054]) ).
thf(1552,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1068,1006]) ).
thf(1554,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1068,1006]) ).
thf(1567,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1068,143]) ).
thf(1585,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[1068,72]) ).
thf(1591,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1068,69]) ).
thf(1594,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1068,50]) ).
thf(1596,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1068,49]) ).
thf(1605,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1596]) ).
thf(1607,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1594]) ).
thf(1608,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1594]) ).
thf(1609,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1594]) ).
thf(1610,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1591]) ).
thf(1611,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1585]) ).
thf(1612,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1567]) ).
thf(1614,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1554]) ).
thf(1617,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1552]) ).
thf(1620,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1548]) ).
thf(1628,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1540]) ).
thf(1630,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1540]) ).
thf(1632,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1538]) ).
thf(1634,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1538]) ).
thf(1636,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1537]) ).
thf(1637,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1536]) ).
thf(1639,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1534]) ).
thf(1640,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1607]) ).
thf(1641,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1614]) ).
thf(1642,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1617]) ).
thf(1643,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1620]) ).
thf(1644,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1630]) ).
thf(1645,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1628]) ).
thf(1646,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1634]) ).
thf(1647,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1632]) ).
thf(1648,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1636]) ).
thf(1649,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1639]) ).
thf(1651,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1135,1370]) ).
thf(1658,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1135,1068]) ).
thf(1668,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1135,1054]) ).
thf(1672,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1135,1006]) ).
thf(1674,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1135,1006]) ).
thf(1676,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1135,336]) ).
thf(1677,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1135,336]) ).
thf(1682,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1135,144]) ).
thf(1687,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1135,143]) ).
thf(1688,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1135,134]) ).
thf(1697,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1135,83]) ).
thf(1705,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1135,72]) ).
thf(1711,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1135,69]) ).
thf(1713,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1135,50]) ).
thf(1729,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1713]) ).
thf(1730,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1711]) ).
thf(1733,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1705]) ).
thf(1735,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1697]) ).
thf(1737,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1688]) ).
thf(1738,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1687]) ).
thf(1740,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1682]) ).
thf(1742,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1677]) ).
thf(1743,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1676]) ).
thf(1744,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1676]) ).
thf(1746,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1674]) ).
thf(1749,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1672]) ).
thf(1752,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1668]) ).
thf(1760,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1658]) ).
thf(1762,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1658]) ).
thf(1763,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1651]) ).
thf(1764,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1735]) ).
thf(1765,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1737]) ).
thf(1766,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1740]) ).
thf(1767,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1742]) ).
thf(1768,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1746]) ).
thf(1769,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1749]) ).
thf(1770,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1752]) ).
thf(1771,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1762]) ).
thf(1772,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1760]) ).
thf(1778,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1136,1370]) ).
thf(1779,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1136,1321]) ).
thf(1782,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1136,1321]) ).
thf(1799,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1136,336]) ).
thf(1802,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1136,336]) ).
thf(1807,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1136,144]) ).
thf(1811,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1136,134]) ).
thf(1820,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[1136,83]) ).
thf(1822,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1136,81]) ).
thf(1828,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1136,70]) ).
thf(1832,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(res,[status(thm)],[1136,69]) ).
thf(1838,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1136,50]) ).
thf(1839,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1136,49]) ).
thf(1842,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1839]) ).
thf(1844,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1839]) ).
thf(1845,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1839]) ).
thf(1846,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1838]) ).
thf(1847,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1832]) ).
thf(1848,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1832]) ).
thf(1849,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1828]) ).
thf(1850,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1822]) ).
thf(1851,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1820]) ).
thf(1854,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1811]) ).
thf(1855,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1807]) ).
thf(1858,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1802]) ).
thf(1860,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1799]) ).
thf(1861,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1799]) ).
thf(1866,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1782]) ).
thf(1871,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1779]) ).
thf(1872,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1778]) ).
thf(1875,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1845]) ).
thf(1876,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1844]) ).
thf(1877,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1842]) ).
thf(1878,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1848]) ).
thf(1879,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(sim,[status(thm)],[1847]) ).
thf(1880,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1851]) ).
thf(1881,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1854]) ).
thf(1882,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1858]) ).
thf(1883,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1866]) ).
thf(1884,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1871]) ).
thf(1885,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1380,1380]) ).
thf(1887,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1380,1380]) ).
thf(1889,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1380,1370]) ).
thf(1893,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1380,1321]) ).
thf(1895,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1380,1321]) ).
thf(1897,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(res,[status(thm)],[1380,1136]) ).
thf(1910,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1380,1067]) ).
thf(1911,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1380,1067]) ).
thf(1913,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1380,1054]) ).
thf(1915,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1380,1006]) ).
thf(1916,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1380,1006]) ).
thf(1926,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1380,144]) ).
thf(1942,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1380,81]) ).
thf(1948,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1380,70]) ).
thf(1957,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1380,50]) ).
thf(1958,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1380,49]) ).
thf(1964,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1958]) ).
thf(1966,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1958]) ).
thf(1967,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1958]) ).
thf(1968,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1957]) ).
thf(1969,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1948]) ).
thf(1970,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1942]) ).
thf(1971,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1926]) ).
thf(1972,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1916]) ).
thf(1974,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1915]) ).
thf(1975,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1913]) ).
thf(1977,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1911]) ).
thf(1979,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1911]) ).
thf(1981,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1910]) ).
thf(1987,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1897]) ).
thf(1989,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1897]) ).
thf(1991,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1895]) ).
thf(1996,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1893]) ).
thf(1997,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1889]) ).
thf(1999,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1887]) ).
thf(2001,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1887]) ).
thf(2003,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1885]) ).
thf(2005,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1885]) ).
thf(2007,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1964]) ).
thf(2008,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1972]) ).
thf(2009,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1975]) ).
thf(2010,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1979]) ).
thf(2011,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1977]) ).
thf(2012,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1981]) ).
thf(2013,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1989]) ).
thf(2014,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1987]) ).
thf(2015,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1991]) ).
thf(2016,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1996]) ).
thf(2017,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1997]) ).
thf(2018,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2001]) ).
thf(2019,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1999]) ).
thf(2020,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2005]) ).
thf(2021,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2003]) ).
thf(2023,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2012,1370]) ).
thf(2027,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2012,1321]) ).
thf(2029,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2012,1321]) ).
thf(2044,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2012,144]) ).
thf(2054,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[2012,81]) ).
thf(2058,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2012,70]) ).
thf(2067,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2012,49]) ).
thf(2069,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2067]) ).
thf(2071,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2067]) ).
thf(2072,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2067]) ).
thf(2073,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2058]) ).
thf(2074,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2054]) ).
thf(2075,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2044]) ).
thf(2080,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2029]) ).
thf(2085,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2027]) ).
thf(2086,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2023]) ).
thf(2088,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2069]) ).
thf(2089,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2080]) ).
thf(2090,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2085]) ).
thf(2091,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2086]) ).
thf(2092,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2073,1370]) ).
thf(2095,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2073,1370]) ).
thf(2096,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2073,1321]) ).
thf(2098,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2073,1321]) ).
thf(2100,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2073,1135]) ).
thf(2104,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2073,1068]) ).
thf(2111,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2073,336]) ).
thf(2113,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2073,144]) ).
thf(2123,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[2073,83]) ).
thf(2135,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2073,50]) ).
thf(2136,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2073,49]) ).
thf(2139,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2136]) ).
thf(2140,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2136]) ).
thf(2141,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2136]) ).
thf(2142,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2136]) ).
thf(2143,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2135]) ).
thf(2144,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2135]) ).
thf(2146,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2123]) ).
thf(2150,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2113]) ).
thf(2151,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2111]) ).
thf(2152,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2111]) ).
thf(2154,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[2104]) ).
thf(2155,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[2100]) ).
thf(2156,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2098]) ).
thf(2157,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2098]) ).
thf(2159,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2096]) ).
thf(2161,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2096]) ).
thf(2163,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2095]) ).
thf(2164,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2092]) ).
thf(2165,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2092]) ).
thf(2166,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2146]) ).
thf(2167,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2150]) ).
thf(2168,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2161]) ).
thf(2169,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(sim,[status(thm)],[2159]) ).
thf(2170,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2163]) ).
thf(2177,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2074,1370]) ).
thf(2179,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2074,1321]) ).
thf(2180,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2074,1321]) ).
thf(2181,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2074,1135]) ).
thf(2185,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2074,1068]) ).
thf(2218,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2074,49]) ).
thf(2223,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2218]) ).
thf(2224,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2218]) ).
thf(2225,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2218]) ).
thf(2226,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2218]) ).
thf(2230,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2185]) ).
thf(2231,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2181]) ).
thf(2232,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2180]) ).
thf(2233,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2180]) ).
thf(2235,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2179]) ).
thf(2237,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2179]) ).
thf(2238,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2177]) ).
thf(2239,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2177]) ).
thf(2240,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2237]) ).
thf(2241,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2235]) ).
thf(2247,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2075,2073]) ).
thf(2250,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2075,1370]) ).
thf(2252,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2075,1321]) ).
thf(2253,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2075,1321]) ).
thf(2254,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2075,1135]) ).
thf(2258,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2075,1068]) ).
thf(2261,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2075,1054]) ).
thf(2266,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2075,302]) ).
thf(2274,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[2075,133]) ).
thf(2285,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2075,70]) ).
thf(2291,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2075,49]) ).
thf(2292,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2075,49]) ).
thf(2296,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2292]) ).
thf(2297,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2292]) ).
thf(2298,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2291]) ).
thf(2299,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2291]) ).
thf(2300,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2291]) ).
thf(2301,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2291]) ).
thf(2303,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2285]) ).
thf(2305,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2274]) ).
thf(2309,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2266]) ).
thf(2310,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2266]) ).
thf(2311,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2261]) ).
thf(2313,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[2258]) ).
thf(2316,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[2254]) ).
thf(2317,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2253]) ).
thf(2318,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2253]) ).
thf(2320,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2252]) ).
thf(2322,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2252]) ).
thf(2323,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2250]) ).
thf(2324,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2250]) ).
thf(2325,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2247]) ).
thf(2326,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2247]) ).
thf(2327,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2303]) ).
thf(2328,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2305]) ).
thf(2329,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2311]) ).
thf(2330,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2322]) ).
thf(2331,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2320]) ).
thf(2332,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[2326]) ).
thf(2333,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(sim,[status(thm)],[2325]) ).
thf(2334,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1381,2075]) ).
thf(2335,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1381,2075]) ).
thf(2337,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1381,2074]) ).
thf(2338,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1381,2074]) ).
thf(2340,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1381,2073]) ).
thf(2341,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1381,2073]) ).
thf(2355,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1381,1068]) ).
thf(2356,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1381,1068]) ).
thf(2358,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1381,1054]) ).
thf(2359,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1381,1054]) ).
thf(2364,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1381,1006]) ).
thf(2365,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1381,1006]) ).
thf(2367,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1381,1006]) ).
thf(2381,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1381,143]) ).
thf(2399,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1381,72]) ).
thf(2405,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1381,69]) ).
thf(2406,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1381,50]) ).
thf(2407,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1381,50]) ).
thf(2422,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2407]) ).
thf(2423,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2407]) ).
thf(2424,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2407]) ).
thf(2425,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2406]) ).
thf(2426,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2405]) ).
thf(2427,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2399]) ).
thf(2428,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2381]) ).
thf(2432,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2367]) ).
thf(2435,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2365]) ).
thf(2437,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2364]) ).
thf(2439,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2359]) ).
thf(2441,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2358]) ).
thf(2443,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2356]) ).
thf(2445,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2356]) ).
thf(2446,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2355]) ).
thf(2453,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2341]) ).
thf(2455,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2340]) ).
thf(2457,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2340]) ).
thf(2458,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2338]) ).
thf(2460,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2337]) ).
thf(2462,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2337]) ).
thf(2463,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2335]) ).
thf(2465,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2334]) ).
thf(2467,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2334]) ).
thf(2468,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2422]) ).
thf(2469,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2432]) ).
thf(2470,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2435]) ).
thf(2471,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2439]) ).
thf(2472,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2441]) ).
thf(2473,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2445]) ).
thf(2474,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2443]) ).
thf(2475,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2446]) ).
thf(2476,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2457]) ).
thf(2477,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2455]) ).
thf(2478,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2462]) ).
thf(2479,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2460]) ).
thf(2480,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2467]) ).
thf(2481,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2465]) ).
thf(2483,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2475,2075]) ).
thf(2485,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2475,2074]) ).
thf(2487,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2475,2073]) ).
thf(2495,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2475,1054]) ).
thf(2499,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2475,1006]) ).
thf(2501,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2475,1006]) ).
thf(2508,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2475,143]) ).
thf(2520,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[2475,72]) ).
thf(2524,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2475,69]) ).
thf(2527,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2475,50]) ).
thf(2538,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2527]) ).
thf(2539,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2527]) ).
thf(2540,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2527]) ).
thf(2541,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2524]) ).
thf(2542,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2520]) ).
thf(2543,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2508]) ).
thf(2545,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2501]) ).
thf(2548,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2499]) ).
thf(2551,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2495]) ).
thf(2554,plain,
( ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2487]) ).
thf(2555,plain,
( ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2485]) ).
thf(2556,plain,
( ( ( g @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2483]) ).
thf(2557,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2538]) ).
thf(2558,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2545]) ).
thf(2559,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2548]) ).
thf(2560,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2551]) ).
thf(2561,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2541,2075]) ).
thf(2563,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2541,2074]) ).
thf(2571,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[2541,2012]) ).
thf(2573,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2541,1054]) ).
thf(2576,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2541,1054]) ).
thf(2577,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2541,1006]) ).
thf(2579,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2541,1006]) ).
thf(2582,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2541,302]) ).
thf(2584,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2541,302]) ).
thf(2586,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[2541,143]) ).
thf(2590,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[2541,133]) ).
thf(2594,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2541,84]) ).
thf(2602,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[2541,70]) ).
thf(2605,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2541,50]) ).
thf(2608,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2541,49]) ).
thf(2616,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2608]) ).
thf(2617,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2608]) ).
thf(2618,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2605]) ).
thf(2619,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2605]) ).
thf(2620,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2605]) ).
thf(2621,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2605]) ).
thf(2622,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2602]) ).
thf(2624,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2594]) ).
thf(2625,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2590]) ).
thf(2626,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2586]) ).
thf(2628,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2584]) ).
thf(2629,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2584]) ).
thf(2630,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2582]) ).
thf(2631,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2579]) ).
thf(2632,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2579]) ).
thf(2633,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2577]) ).
thf(2635,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2577]) ).
thf(2637,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2576]) ).
thf(2639,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2573]) ).
thf(2640,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2573]) ).
thf(2641,plain,
( ( x = $true )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2571]) ).
thf(2644,plain,
( ( y = $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2563]) ).
thf(2645,plain,
( ( ( g @ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2561]) ).
thf(2646,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2624]) ).
thf(2647,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(sim,[status(thm)],[2626]) ).
thf(2648,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2635]) ).
thf(2649,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( x = $true ) ),
inference(sim,[status(thm)],[2633]) ).
thf(2650,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(sim,[status(thm)],[2637]) ).
thf(2657,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2542,2075]) ).
thf(2661,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2542,2073]) ).
thf(2664,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(res,[status(thm)],[2542,2012]) ).
thf(2669,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2542,1054]) ).
thf(2671,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2542,1006]) ).
thf(2672,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2542,1006]) ).
thf(2682,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2542,134]) ).
thf(2685,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2542,84]) ).
thf(2690,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[2542,81]) ).
thf(2699,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2542,50]) ).
thf(2705,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2699]) ).
thf(2706,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2699]) ).
thf(2707,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2699]) ).
thf(2708,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2699]) ).
thf(2709,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2690]) ).
thf(2710,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2685]) ).
thf(2711,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2682]) ).
thf(2712,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2672]) ).
thf(2713,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2672]) ).
thf(2714,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2671]) ).
thf(2716,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2671]) ).
thf(2718,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2669]) ).
thf(2719,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2669]) ).
thf(2720,plain,
( ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2664]) ).
thf(2721,plain,
( ( ( g @ y )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2661]) ).
thf(2724,plain,
( ( ( g @ x )
= $false )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2657]) ).
thf(2725,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2716]) ).
thf(2726,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2714]) ).
thf(2727,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[19,2726,2725,2724,2721,2720,2719,2718,2713,2712,2711,2710,2709,2708,2707,2706,2705,2650,2649,2648,2647,2646,2645,2644,2641,2640,2639,2632,2631,2630,2629,2628,2625,2622,2621,2620,2619,2618,2617,2616,2560,2559,2558,2557,2556,2555,2554,2543,2542,2541,2540,2539,2481,2480,2479,2478,2477,2476,2475,2474,2473,2472,2471,2470,2469,2468,2463,2458,2453,2437,2428,2427,2426,2425,2424,2423,2333,2332,2331,2330,2329,2328,2327,2324,2323,2318,2317,2316,2313,2310,2309,2301,2300,2299,2298,2297,2296,2241,2240,2239,2238,2233,2232,2231,2230,2226,2225,2224,2223,2170,2169,2168,2167,2166,2165,2164,2157,2156,2155,2154,2152,2151,2144,2143,2142,2141,2140,2139,2091,2090,2089,2088,2075,2074,2073,2072,2071,2021,2020,2019,2018,2017,2016,2015,2014,2013,2012,2011,2010,2009,2008,2007,1974,1971,1970,1969,1968,1967,1966,1884,1883,1882,1881,1880,1879,1878,1877,1876,1875,1872,1861,1860,1855,1850,1849,1846,1772,1771,1770,1769,1768,1767,1766,1765,1764,1763,1744,1743,1738,1733,1730,1729,1649,1648,1647,1646,1645,1644,1643,1642,1641,1640,1637,1612,1611,1610,1609,1608,1605,1533,1532,1531,1530,1529,1524,1515,1514,1513,1512,1511,1510,1450,1449,1448,1447,1446,1445,1442,1441,1379,1378,1375,1374,1373,1372,1370,1369,1368,1324,1323,1322,1321,1320,1232,1229,1228,1225,1224,1141,1130,1129,1070,1069,1060,1059,1056,1055,1054,1053,1052,1008,1007,1006,1005,1004,1003,911,909,906,905,904,816,815,814,725,724,723,646,645,336,302,144,143,134,133,84,83,81,72,70,69,53,50,49,45,28]) ).
thf(2728,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[2727]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO041^1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.16 % Computer : n002.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Tue Oct 6 17:33:57 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.13/6.10
% 35.13/6.10 No.of.Axioms: 1
% 35.13/6.10
% 35.13/6.10 Length.of.Defs: 0
% 35.13/6.10
% 35.13/6.10 Contains.Choice.Funs: false
% 35.13/6.10 ...............................................................
% 35.13/6.10
% 35.13/6.10 ********************************
% 35.13/6.10 * All subproblems solved! *
% 35.13/6.10 ********************************
% 35.13/6.10 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:2727,loop_count:185,foatp_calls:39,translation:fof_full)
% 35.13/6.10
% 35.13/6.10 %**** Beginning of derivation protocol ****
% 35.13/6.10 % SZS output start CNFRefutation
% See solution above
% 35.13/6.10
% 35.13/6.10 %**** End of derivation protocol ****
% 35.13/6.10 %**** no. of clauses in derivation: 712 ****
% 35.13/6.10 %**** clause counter: 2727 ****
% 35.13/6.10
% 35.13/6.10 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:2727,loop_count:185,foatp_calls:39,translation:fof_full)
%------------------------------------------------------------------------------