%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SYO041^2 : TPTP v9.3.1. Released v4.1.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 : n019.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 : Theorem 38.63s 6.63s
% Output : CNFRefutation 38.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 1
% Syntax : Number of formulae : 714 ( 38 unt; 0 typ; 0 def)
% Number of atoms : 11949 (2853 equ; 0 cnn)
% Maximal formula atoms : 6 ( 16 avg)
% Number of connectives : 5678 ( 149 ~;1918 |; 18 &;3593 @)
% ( 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,conjecture,
~ ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',3) ).
thf(2,negated_conjecture,
( ( ~ ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( ~ ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) ) )
= $false ),
inference(unfold_def,[status(thm)],[2]) ).
thf(4,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[3]) ).
thf(5,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(extcnf_combined,[status(esa)],[4]) ).
thf(6,plain,
( ( ( x != y )
& ( ( g @ x )
= y )
& ( ( g @ y )
= x )
& ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) ) )
= $true ),
inference(copy,[status(thm)],[5]) ).
thf(7,plain,
( ( ~ ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
| ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[6]) ).
thf(8,plain,
( ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
| ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[7]) ).
thf(9,plain,
( ( ~ ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[8]) ).
thf(10,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
!= ( g @ ( f @ x ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[8]) ).
thf(11,plain,
( ( ~ ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[9]) ).
thf(12,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[10]) ).
thf(13,plain,
( ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
| ( ( g @ y )
!= x ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[11]) ).
thf(14,plain,
( ( ~ ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) )
| ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[12]) ).
thf(15,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= ( g @ ( f @ x ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[12]) ).
thf(16,plain,
( ( ~ ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[13]) ).
thf(17,plain,
( ( ( g @ y )
!= x )
= $false ),
inference(extcnf_or_neg,[status(thm)],[13]) ).
thf(18,plain,
( ( ( ~ ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) ) )
= $true )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[14]) ).
thf(19,plain,
( ( ~ ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[16]) ).
thf(20,plain,
( ( ( g @ y )
= x )
= $true ),
inference(extcnf_not_neg,[status(thm)],[17]) ).
thf(21,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
| ( g @ ( f @ x ) ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[18]) ).
thf(22,plain,
( ( ~ ( ( x != y ) )
| ( ( g @ x )
!= y ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[19]) ).
thf(23,plain,
( ( ~ ( ( g @ y )
| x )
| ~ ( ~ ( g @ y )
| ~ x ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[20]) ).
thf(24,plain,
( ( ( g @ y )
= x )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[20]) ).
thf(25,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[21]) ).
thf(26,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( ~ ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[21]) ).
thf(27,plain,
( ( ~ ( ( x != y ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[22]) ).
thf(28,plain,
( ( ( g @ x )
!= y )
= $false ),
inference(extcnf_or_neg,[status(thm)],[22]) ).
thf(29,plain,
( ( ( ~ ( ( g @ y )
| x ) )
= $true )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[23]) ).
thf(30,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[25]) ).
thf(31,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) )
| ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[26]) ).
thf(32,plain,
( ( x != y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[27]) ).
thf(33,plain,
( ( ( g @ x )
= y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[28]) ).
thf(34,plain,
( ( ( ( g @ y )
| x )
= $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[29]) ).
thf(36,plain,
( ( ( ~ ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[30]) ).
thf(37,plain,
( ( ( ~ ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[31]) ).
thf(39,plain,
( ( x = y )
= $false ),
inference(extcnf_not_pos,[status(thm)],[32]) ).
thf(40,plain,
( ( ~ ( ( g @ x )
| y )
| ~ ( ~ ( g @ x )
| ~ y ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[33]) ).
thf(41,plain,
( ( ( g @ x )
= y )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[33]) ).
thf(42,plain,
( ( ( g @ y )
= $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[34]) ).
thf(43,plain,
( ( x = $false )
| ( ( ~ ( ~ ( g @ y )
| ~ x ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[34]) ).
thf(45,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[36]) ).
thf(46,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[37]) ).
thf(48,plain,
( ( ~ ( x
| y )
| ~ ( ~ x
| ~ y ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[39]) ).
thf(49,plain,
( ( x = y )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[39]) ).
thf(50,plain,
( ( ( ~ ( ( g @ x )
| y ) )
= $true )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[40]) ).
thf(51,plain,
( ( ( ~ ( g @ y )
| ~ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[42]) ).
thf(52,plain,
( ( ( ~ ( g @ y )
| ~ x )
= $false )
| ( x = $false ) ),
inference(extcnf_not_pos,[status(thm)],[43]) ).
thf(53,plain,
( ( ~ ( x
| y ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[48]) ).
thf(54,plain,
( ( ~ ( ~ x
| ~ y ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[48]) ).
thf(55,plain,
( ( ( ( g @ x )
| y )
= $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[50]) ).
thf(57,plain,
( ( ( ~ x ) = $false )
| ( ( g @ y )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[51]) ).
thf(58,plain,
( ( ( ~ ( g @ y ) )
= $false )
| ( x = $false ) ),
inference(extcnf_or_neg,[status(thm)],[52]) ).
thf(60,plain,
( ( x
| y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[53]) ).
thf(61,plain,
( ( ~ x
| ~ y )
= $true ),
inference(extcnf_not_neg,[status(thm)],[54]) ).
thf(62,plain,
( ( ( g @ x )
= $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[55]) ).
thf(63,plain,
( ( y = $false )
| ( ( ~ ( ~ ( g @ x )
| ~ y ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[55]) ).
thf(65,plain,
( ( x = $true )
| ( ( g @ y )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[57]) ).
thf(66,plain,
( ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(extcnf_not_neg,[status(thm)],[58]) ).
thf(68,plain,
( ( x = $true )
| ( y = $true ) ),
inference(extcnf_or_pos,[status(thm)],[60]) ).
thf(69,plain,
( ( ( ~ x ) = $true )
| ( ( ~ y ) = $true ) ),
inference(extcnf_or_pos,[status(thm)],[61]) ).
thf(70,plain,
( ( ( ~ ( g @ x )
| ~ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[62]) ).
thf(71,plain,
( ( ( ~ ( g @ x )
| ~ y )
= $false )
| ( y = $false ) ),
inference(extcnf_not_pos,[status(thm)],[63]) ).
thf(72,plain,
( ( x = $false )
| ( ( ~ y ) = $true ) ),
inference(extcnf_not_pos,[status(thm)],[69]) ).
thf(74,plain,
( ( ( ~ y ) = $false )
| ( ( g @ x )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[70]) ).
thf(75,plain,
( ( ( ~ ( g @ x ) )
= $false )
| ( y = $false ) ),
inference(extcnf_or_neg,[status(thm)],[71]) ).
thf(77,plain,
( ( y = $false )
| ( x = $false ) ),
inference(extcnf_not_pos,[status(thm)],[72]) ).
thf(79,plain,
( ( y = $true )
| ( ( g @ x )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[74]) ).
thf(80,plain,
( ( ( g @ x )
= $true )
| ( y = $false ) ),
inference(extcnf_not_neg,[status(thm)],[75]) ).
thf(118,plain,
( ( ( x = y )
= ( ( g @ x )
= y ) )
= $false ),
inference(res,[status(thm)],[49,41]) ).
thf(119,plain,
( ( ( x = y )
= ( ( g @ y )
= x ) )
= $false ),
inference(res,[status(thm)],[49,24]) ).
thf(129,plain,
( ( y = $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[119]) ).
thf(130,plain,
( ( y = $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[119]) ).
thf(139,plain,
( ( x = $true )
| ( ( g @ x )
= $true ) ),
inference(extuni,[status(esa)],[118]) ).
thf(140,plain,
( ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[118]) ).
thf(274,plain,
( ( ( y = y )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[129,80]) ).
thf(287,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[129,46]) ).
thf(292,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[287]) ).
thf(298,plain,
( ( ( g @ x )
= $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[274]) ).
thf(299,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[292]) ).
thf(308,plain,
( ( ( y = y )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[130,79]) ).
thf(319,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[130,45]) ).
thf(329,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[319]) ).
thf(332,plain,
( ( ( g @ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[308]) ).
thf(337,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[329]) ).
thf(357,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[139,46]) ).
thf(362,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[357]) ).
thf(371,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[362]) ).
thf(395,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[140,45]) ).
thf(405,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[395]) ).
thf(415,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[405]) ).
thf(557,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[299,77]) ).
thf(573,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[299,45]) ).
thf(574,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[573]) ).
thf(577,plain,
( ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[557]) ).
thf(614,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[337,68]) ).
thf(625,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[337,46]) ).
thf(627,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[337,46]) ).
thf(640,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[627]) ).
thf(641,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[625]) ).
thf(642,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[625]) ).
thf(643,plain,
( ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[614]) ).
thf(655,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[371,337]) ).
thf(659,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[371,337]) ).
thf(704,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[371,45]) ).
thf(708,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[704]) ).
thf(714,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[659]) ).
thf(716,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[655]) ).
thf(719,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[708]) ).
thf(720,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[714]) ).
thf(721,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[716]) ).
thf(733,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[415,299]) ).
thf(737,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[415,299]) ).
thf(776,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[415,46]) ).
thf(793,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[776]) ).
thf(799,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[737]) ).
thf(801,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[733]) ).
thf(810,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[793]) ).
thf(811,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[799]) ).
thf(812,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[801]) ).
thf(814,plain,
( ( ( ( f @ x )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[574,415]) ).
thf(820,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[574,415]) ).
thf(836,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( y = $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[574,332]) ).
thf(874,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[574,45]) ).
thf(876,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[874]) ).
thf(877,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[874]) ).
thf(890,plain,
( ( ( g @ y )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[836]) ).
thf(899,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[820]) ).
thf(900,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[814]) ).
thf(901,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[877]) ).
thf(902,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[876]) ).
thf(905,plain,
( ( ( g @ y )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[890]) ).
thf(907,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[899]) ).
thf(915,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[577,415]) ).
thf(920,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[577,415]) ).
thf(922,plain,
( ( ( x = x )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[577,371]) ).
thf(924,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[577,337]) ).
thf(929,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[577,337]) ).
thf(975,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[577,45]) ).
thf(981,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[975]) ).
thf(987,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[929]) ).
thf(991,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[924]) ).
thf(992,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[922]) ).
thf(994,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[920]) ).
thf(998,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[915]) ).
thf(999,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[981]) ).
thf(1000,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[987]) ).
thf(1001,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[991]) ).
thf(1002,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(sim,[status(thm)],[992]) ).
thf(1003,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[994]) ).
thf(1004,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[998]) ).
thf(1005,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1002,415]) ).
thf(1010,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1002,415]) ).
thf(1011,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1002,337]) ).
thf(1016,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1002,337]) ).
thf(1045,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1002,45]) ).
thf(1046,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1002,45]) ).
thf(1047,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false ) ),
inference(fac_restr,[status(thm)],[1002]) ).
thf(1048,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1046]) ).
thf(1049,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1046]) ).
thf(1050,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1045]) ).
thf(1051,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1016]) ).
thf(1052,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1016]) ).
thf(1055,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1011]) ).
thf(1056,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1011]) ).
thf(1058,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1010]) ).
thf(1062,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1005]) ).
thf(1063,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[1047]) ).
thf(1064,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(extuni,[status(esa)],[1047]) ).
thf(1065,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1058]) ).
thf(1066,plain,
( ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1062]) ).
thf(1071,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1050,415]) ).
thf(1077,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1050,337]) ).
thf(1107,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1050,45]) ).
thf(1110,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1107]) ).
thf(1111,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1107]) ).
thf(1125,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1077]) ).
thf(1126,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1077]) ).
thf(1129,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1071]) ).
thf(1131,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1111]) ).
thf(1132,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1110]) ).
thf(1137,plain,
( ( ( f @ x )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1129]) ).
thf(1145,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[640,1002]) ).
thf(1155,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[640,298]) ).
thf(1187,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[640,46]) ).
thf(1202,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1187]) ).
thf(1203,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1187]) ).
thf(1216,plain,
( ( ( g @ y )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1155]) ).
thf(1220,plain,
( ( ( f @ x )
= $true )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1145]) ).
thf(1221,plain,
( ( ( f @ x )
= $true )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1145]) ).
thf(1224,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1203]) ).
thf(1225,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1202]) ).
thf(1228,plain,
( ( ( g @ y )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1216]) ).
thf(1230,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[643,1050]) ).
thf(1235,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[643,1002]) ).
thf(1236,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[643,1002]) ).
thf(1246,plain,
( ( ( x = x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[643,415]) ).
thf(1290,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[643,46]) ).
thf(1300,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1290]) ).
thf(1306,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1246]) ).
thf(1308,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1236]) ).
thf(1310,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1235]) ).
thf(1314,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1230]) ).
thf(1316,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1300]) ).
thf(1317,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(sim,[status(thm)],[1306]) ).
thf(1318,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1308]) ).
thf(1319,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1310]) ).
thf(1320,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1314]) ).
thf(1321,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1317,1050]) ).
thf(1326,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1317,1002]) ).
thf(1327,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1317,1002]) ).
thf(1353,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1317,46]) ).
thf(1354,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1317,46]) ).
thf(1363,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false ) ),
inference(fac_restr,[status(thm)],[1317]) ).
thf(1364,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1354]) ).
thf(1365,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1354]) ).
thf(1366,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1353]) ).
thf(1368,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1327]) ).
thf(1369,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1327]) ).
thf(1370,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1326]) ).
thf(1371,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1326]) ).
thf(1374,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1321]) ).
thf(1375,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1321]) ).
thf(1376,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[1363]) ).
thf(1377,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(extuni,[status(esa)],[1363]) ).
thf(1382,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1366,1002]) ).
thf(1387,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1366,298]) ).
thf(1389,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1366,298]) ).
thf(1399,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1366,80]) ).
thf(1407,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1366,66]) ).
thf(1410,plain,
( ( ( ( f @ x )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1366,46]) ).
thf(1422,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1410]) ).
thf(1423,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1410]) ).
thf(1425,plain,
( ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1407]) ).
thf(1427,plain,
( ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1399]) ).
thf(1433,plain,
( ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1389]) ).
thf(1435,plain,
( ( ( g @ x )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1387]) ).
thf(1437,plain,
( ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1382]) ).
thf(1438,plain,
( ( ( f @ x )
= $true )
| ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1382]) ).
thf(1441,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1423]) ).
thf(1442,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1422]) ).
thf(1443,plain,
( ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1425]) ).
thf(1444,plain,
( ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1427]) ).
thf(1445,plain,
( ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1433]) ).
thf(1446,plain,
( ( ( g @ x )
= $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1435]) ).
thf(1447,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1063,1366]) ).
thf(1448,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1063,1366]) ).
thf(1453,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1063,1317]) ).
thf(1454,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1063,1317]) ).
thf(1456,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1063,1317]) ).
thf(1470,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1063,140]) ).
thf(1485,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1063,77]) ).
thf(1491,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1063,66]) ).
thf(1501,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1063,45]) ).
thf(1502,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1063,45]) ).
thf(1504,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1502]) ).
thf(1506,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1502]) ).
thf(1507,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1502]) ).
thf(1508,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1501]) ).
thf(1509,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1491]) ).
thf(1510,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1485]) ).
thf(1511,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1470]) ).
thf(1514,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1456]) ).
thf(1519,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1454]) ).
thf(1520,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1453]) ).
thf(1521,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1448]) ).
thf(1523,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1447]) ).
thf(1525,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1504]) ).
thf(1526,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1514]) ).
thf(1527,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1519]) ).
thf(1528,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1521]) ).
thf(1529,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1523]) ).
thf(1530,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1064,1366]) ).
thf(1532,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1064,1317]) ).
thf(1533,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1064,1317]) ).
thf(1534,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)],[1064,1064]) ).
thf(1536,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)],[1064,1064]) ).
thf(1544,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1064,1050]) ).
thf(1548,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1064,1002]) ).
thf(1550,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1064,1002]) ).
thf(1563,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1064,139]) ).
thf(1581,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[1064,68]) ).
thf(1587,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1064,65]) ).
thf(1590,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1064,46]) ).
thf(1592,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1064,45]) ).
thf(1601,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1592]) ).
thf(1603,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1590]) ).
thf(1604,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1590]) ).
thf(1605,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1590]) ).
thf(1606,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1587]) ).
thf(1607,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1581]) ).
thf(1608,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1563]) ).
thf(1610,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1550]) ).
thf(1613,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1548]) ).
thf(1616,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1544]) ).
thf(1624,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1536]) ).
thf(1626,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)],[1536]) ).
thf(1628,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1534]) ).
thf(1630,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)],[1534]) ).
thf(1632,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1533]) ).
thf(1633,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1532]) ).
thf(1635,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1530]) ).
thf(1636,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1603]) ).
thf(1637,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1610]) ).
thf(1638,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1613]) ).
thf(1639,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1616]) ).
thf(1640,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1626]) ).
thf(1641,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1624]) ).
thf(1642,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1630]) ).
thf(1643,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1628]) ).
thf(1644,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1632]) ).
thf(1645,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[1635]) ).
thf(1647,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1131,1366]) ).
thf(1654,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)],[1131,1064]) ).
thf(1664,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1131,1050]) ).
thf(1668,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1131,1002]) ).
thf(1670,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1131,1002]) ).
thf(1672,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1131,332]) ).
thf(1673,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1131,332]) ).
thf(1678,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[1131,140]) ).
thf(1683,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1131,139]) ).
thf(1684,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1131,130]) ).
thf(1693,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1131,79]) ).
thf(1701,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1131,68]) ).
thf(1707,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1131,65]) ).
thf(1709,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1131,46]) ).
thf(1725,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1709]) ).
thf(1726,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1707]) ).
thf(1729,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1701]) ).
thf(1731,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1693]) ).
thf(1733,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1684]) ).
thf(1734,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1683]) ).
thf(1736,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1678]) ).
thf(1738,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1673]) ).
thf(1739,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1672]) ).
thf(1740,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1672]) ).
thf(1742,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1670]) ).
thf(1745,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1668]) ).
thf(1748,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1664]) ).
thf(1756,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[1654]) ).
thf(1758,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1654]) ).
thf(1759,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[1647]) ).
thf(1760,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1731]) ).
thf(1761,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1733]) ).
thf(1762,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1736]) ).
thf(1763,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1738]) ).
thf(1764,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1742]) ).
thf(1765,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1745]) ).
thf(1766,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1748]) ).
thf(1767,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1758]) ).
thf(1768,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1756]) ).
thf(1774,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1132,1366]) ).
thf(1775,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1132,1317]) ).
thf(1778,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1132,1317]) ).
thf(1795,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1132,332]) ).
thf(1798,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1132,332]) ).
thf(1803,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1132,140]) ).
thf(1807,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1132,130]) ).
thf(1816,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[1132,79]) ).
thf(1818,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[1132,77]) ).
thf(1824,plain,
( ( ( x = x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1132,66]) ).
thf(1828,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ y ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(res,[status(thm)],[1132,65]) ).
thf(1834,plain,
( ( ( ( g @ ( f @ x ) )
= ( g @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1132,46]) ).
thf(1835,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1132,45]) ).
thf(1838,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1835]) ).
thf(1840,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1835]) ).
thf(1841,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1835]) ).
thf(1842,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1834]) ).
thf(1843,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1828]) ).
thf(1844,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1828]) ).
thf(1845,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1824]) ).
thf(1846,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1818]) ).
thf(1847,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1816]) ).
thf(1850,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1807]) ).
thf(1851,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1803]) ).
thf(1854,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1798]) ).
thf(1856,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[1795]) ).
thf(1857,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[1795]) ).
thf(1862,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1778]) ).
thf(1867,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1775]) ).
thf(1868,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1774]) ).
thf(1871,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1841]) ).
thf(1872,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[1840]) ).
thf(1873,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1838]) ).
thf(1874,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[1844]) ).
thf(1875,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true )
| ( y = $true ) ),
inference(sim,[status(thm)],[1843]) ).
thf(1876,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1847]) ).
thf(1877,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[1850]) ).
thf(1878,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1854]) ).
thf(1879,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1862]) ).
thf(1880,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1867]) ).
thf(1881,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)],[1376,1376]) ).
thf(1883,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)],[1376,1376]) ).
thf(1885,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1376,1366]) ).
thf(1889,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[1376,1317]) ).
thf(1891,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[1376,1317]) ).
thf(1893,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)],[1376,1132]) ).
thf(1906,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)],[1376,1063]) ).
thf(1907,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)],[1376,1063]) ).
thf(1909,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1376,1050]) ).
thf(1911,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1376,1002]) ).
thf(1912,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1376,1002]) ).
thf(1922,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1376,140]) ).
thf(1938,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1376,77]) ).
thf(1944,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1376,66]) ).
thf(1953,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1376,46]) ).
thf(1954,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1376,45]) ).
thf(1960,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1954]) ).
thf(1962,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1954]) ).
thf(1963,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1954]) ).
thf(1964,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1953]) ).
thf(1965,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1944]) ).
thf(1966,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1938]) ).
thf(1967,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[1922]) ).
thf(1968,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1912]) ).
thf(1970,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1911]) ).
thf(1971,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1909]) ).
thf(1973,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1907]) ).
thf(1975,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)],[1907]) ).
thf(1977,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1906]) ).
thf(1983,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1893]) ).
thf(1985,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1893]) ).
thf(1987,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1891]) ).
thf(1992,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[1889]) ).
thf(1993,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1885]) ).
thf(1995,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[1883]) ).
thf(1997,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)],[1883]) ).
thf(1999,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[1881]) ).
thf(2001,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)],[1881]) ).
thf(2003,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1960]) ).
thf(2004,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1968]) ).
thf(2005,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1971]) ).
thf(2006,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1975]) ).
thf(2007,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1973]) ).
thf(2008,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[1977]) ).
thf(2009,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1985]) ).
thf(2010,plain,
( ( x = $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1983]) ).
thf(2011,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1987]) ).
thf(2012,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[1992]) ).
thf(2013,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1993]) ).
thf(2014,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1997]) ).
thf(2015,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1995]) ).
thf(2016,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2001]) ).
thf(2017,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[1999]) ).
thf(2019,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2008,1366]) ).
thf(2023,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2008,1317]) ).
thf(2025,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2008,1317]) ).
thf(2040,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2008,140]) ).
thf(2050,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(res,[status(thm)],[2008,77]) ).
thf(2054,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2008,66]) ).
thf(2063,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2008,45]) ).
thf(2065,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2063]) ).
thf(2067,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2063]) ).
thf(2068,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2063]) ).
thf(2069,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2054]) ).
thf(2070,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2050]) ).
thf(2071,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2040]) ).
thf(2076,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2025]) ).
thf(2081,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2023]) ).
thf(2082,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2019]) ).
thf(2084,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2065]) ).
thf(2085,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2076]) ).
thf(2086,plain,
( ( ( f @ x )
= $false )
| ( x = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2081]) ).
thf(2087,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(sim,[status(thm)],[2082]) ).
thf(2088,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2069,1366]) ).
thf(2091,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2069,1366]) ).
thf(2092,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2069,1317]) ).
thf(2094,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2069,1317]) ).
thf(2096,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2069,1131]) ).
thf(2100,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2069,1064]) ).
thf(2107,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2069,332]) ).
thf(2109,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2069,140]) ).
thf(2119,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[2069,79]) ).
thf(2131,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2069,46]) ).
thf(2132,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2069,45]) ).
thf(2135,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2132]) ).
thf(2136,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2132]) ).
thf(2137,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2132]) ).
thf(2138,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2132]) ).
thf(2139,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2131]) ).
thf(2140,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2131]) ).
thf(2142,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2119]) ).
thf(2146,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2109]) ).
thf(2147,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2107]) ).
thf(2148,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2107]) ).
thf(2150,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[2100]) ).
thf(2151,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $true ) ),
inference(extuni,[status(esa)],[2096]) ).
thf(2152,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2094]) ).
thf(2153,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2094]) ).
thf(2155,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2092]) ).
thf(2157,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2092]) ).
thf(2159,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2091]) ).
thf(2160,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2088]) ).
thf(2161,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2088]) ).
thf(2162,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2142]) ).
thf(2163,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2146]) ).
thf(2164,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2157]) ).
thf(2165,plain,
( ( ( f @ x )
= $false )
| ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(sim,[status(thm)],[2155]) ).
thf(2166,plain,
( ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2159]) ).
thf(2173,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2070,1366]) ).
thf(2175,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2070,1317]) ).
thf(2176,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2070,1317]) ).
thf(2177,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2070,1131]) ).
thf(2181,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2070,1064]) ).
thf(2214,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2070,45]) ).
thf(2219,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2214]) ).
thf(2220,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2214]) ).
thf(2221,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2214]) ).
thf(2222,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2214]) ).
thf(2226,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2181]) ).
thf(2227,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2177]) ).
thf(2228,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2176]) ).
thf(2229,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2176]) ).
thf(2231,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2175]) ).
thf(2233,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2175]) ).
thf(2234,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2173]) ).
thf(2235,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2173]) ).
thf(2236,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2233]) ).
thf(2237,plain,
( ( ( f @ x )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2231]) ).
thf(2243,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2071,2069]) ).
thf(2246,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2071,1366]) ).
thf(2248,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false ) ),
inference(res,[status(thm)],[2071,1317]) ).
thf(2249,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2071,1317]) ).
thf(2250,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2071,1131]) ).
thf(2254,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2071,1064]) ).
thf(2257,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2071,1050]) ).
thf(2262,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2071,298]) ).
thf(2270,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $true ) ),
inference(res,[status(thm)],[2071,129]) ).
thf(2281,plain,
( ( ( ( g @ x )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false ) ),
inference(res,[status(thm)],[2071,66]) ).
thf(2287,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2071,45]) ).
thf(2288,plain,
( ( ( ( g @ x )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2071,45]) ).
thf(2292,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2288]) ).
thf(2293,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2288]) ).
thf(2294,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2287]) ).
thf(2295,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2287]) ).
thf(2296,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2287]) ).
thf(2297,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2287]) ).
thf(2299,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2281]) ).
thf(2301,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2270]) ).
thf(2305,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2262]) ).
thf(2306,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2262]) ).
thf(2307,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2257]) ).
thf(2309,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[2254]) ).
thf(2312,plain,
( ( x = $false )
| ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ x )
= $false ) ),
inference(extuni,[status(esa)],[2250]) ).
thf(2313,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2249]) ).
thf(2314,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2249]) ).
thf(2316,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2248]) ).
thf(2318,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2248]) ).
thf(2319,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2246]) ).
thf(2320,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2246]) ).
thf(2321,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2243]) ).
thf(2322,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(extuni,[status(esa)],[2243]) ).
thf(2323,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $true )
| ( y = $false ) ),
inference(sim,[status(thm)],[2299]) ).
thf(2324,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2301]) ).
thf(2325,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2307]) ).
thf(2326,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(sim,[status(thm)],[2318]) ).
thf(2327,plain,
( ( ( f @ x )
= $false )
| ( ( g @ x )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2316]) ).
thf(2328,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $false )
| ( y = $false ) ),
inference(sim,[status(thm)],[2322]) ).
thf(2329,plain,
( ( ( f @ ( f @ x ) )
= $true )
| ( x = $true )
| ( y = $true ) ),
inference(sim,[status(thm)],[2321]) ).
thf(2330,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1377,2071]) ).
thf(2331,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[1377,2071]) ).
thf(2333,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1377,2070]) ).
thf(2334,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[1377,2070]) ).
thf(2336,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1377,2069]) ).
thf(2337,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[1377,2069]) ).
thf(2351,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)],[1377,1064]) ).
thf(2352,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)],[1377,1064]) ).
thf(2354,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1377,1050]) ).
thf(2355,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[1377,1050]) ).
thf(2360,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1377,1002]) ).
thf(2361,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[1377,1002]) ).
thf(2363,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[1377,1002]) ).
thf(2377,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[1377,139]) ).
thf(2395,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[1377,68]) ).
thf(2401,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[1377,65]) ).
thf(2402,plain,
( ( ( ( f @ ( f @ ( f @ x ) ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1377,46]) ).
thf(2403,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[1377,46]) ).
thf(2418,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2403]) ).
thf(2419,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2403]) ).
thf(2420,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2403]) ).
thf(2421,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2402]) ).
thf(2422,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2401]) ).
thf(2423,plain,
( ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2395]) ).
thf(2424,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2377]) ).
thf(2428,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2363]) ).
thf(2431,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2361]) ).
thf(2433,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2360]) ).
thf(2435,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2355]) ).
thf(2437,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2354]) ).
thf(2439,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2352]) ).
thf(2441,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)],[2352]) ).
thf(2442,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2351]) ).
thf(2449,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2337]) ).
thf(2451,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2336]) ).
thf(2453,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2336]) ).
thf(2454,plain,
( ( y = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2334]) ).
thf(2456,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2333]) ).
thf(2458,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2333]) ).
thf(2459,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2331]) ).
thf(2461,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2330]) ).
thf(2463,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2330]) ).
thf(2464,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2418]) ).
thf(2465,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2428]) ).
thf(2466,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2431]) ).
thf(2467,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2435]) ).
thf(2468,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2437]) ).
thf(2469,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2441]) ).
thf(2470,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2439]) ).
thf(2471,plain,
( ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2442]) ).
thf(2472,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2453]) ).
thf(2473,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2451]) ).
thf(2474,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2458]) ).
thf(2475,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2456]) ).
thf(2476,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2463]) ).
thf(2477,plain,
( ( ( g @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2461]) ).
thf(2479,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2471,2071]) ).
thf(2481,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2471,2070]) ).
thf(2483,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( x = $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2471,2069]) ).
thf(2491,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2471,1050]) ).
thf(2495,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2471,1002]) ).
thf(2497,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2471,1002]) ).
thf(2504,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2471,139]) ).
thf(2516,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[2471,68]) ).
thf(2520,plain,
( ( ( x = x )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2471,65]) ).
thf(2523,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( x = $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2471,46]) ).
thf(2534,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2523]) ).
thf(2535,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2523]) ).
thf(2536,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2523]) ).
thf(2537,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2520]) ).
thf(2538,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2516]) ).
thf(2539,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2504]) ).
thf(2541,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2497]) ).
thf(2544,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2495]) ).
thf(2547,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2491]) ).
thf(2550,plain,
( ( ( g @ y )
= $true )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2483]) ).
thf(2551,plain,
( ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2481]) ).
thf(2552,plain,
( ( ( g @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2479]) ).
thf(2553,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2534]) ).
thf(2554,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2541]) ).
thf(2555,plain,
( ( ( f @ x )
= $true )
| ( x = $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2544]) ).
thf(2556,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(sim,[status(thm)],[2547]) ).
thf(2557,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2537,2071]) ).
thf(2559,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2537,2070]) ).
thf(2567,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[2537,2008]) ).
thf(2569,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2537,1050]) ).
thf(2572,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2537,1050]) ).
thf(2573,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2537,1002]) ).
thf(2575,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2537,1002]) ).
thf(2578,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2537,298]) ).
thf(2580,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2537,298]) ).
thf(2582,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $true ) ),
inference(res,[status(thm)],[2537,139]) ).
thf(2586,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(res,[status(thm)],[2537,129]) ).
thf(2590,plain,
( ( ( ( g @ y )
= ( g @ x ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false ) ),
inference(res,[status(thm)],[2537,80]) ).
thf(2598,plain,
( ( ( ( g @ y )
= ( g @ y ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[2537,66]) ).
thf(2601,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2537,46]) ).
thf(2604,plain,
( ( ( ( g @ y )
= ( g @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( f @ ( f @ ( f @ x ) ) )
= $false ) ),
inference(res,[status(thm)],[2537,45]) ).
thf(2612,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2604]) ).
thf(2613,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2604]) ).
thf(2614,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2601]) ).
thf(2615,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2601]) ).
thf(2616,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2601]) ).
thf(2617,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2601]) ).
thf(2618,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2598]) ).
thf(2620,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2590]) ).
thf(2621,plain,
( ( y = $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2586]) ).
thf(2622,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2582]) ).
thf(2624,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2580]) ).
thf(2625,plain,
( ( ( g @ y )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2580]) ).
thf(2626,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2578]) ).
thf(2627,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2575]) ).
thf(2628,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2575]) ).
thf(2629,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2573]) ).
thf(2631,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2573]) ).
thf(2633,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2572]) ).
thf(2635,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2569]) ).
thf(2636,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2569]) ).
thf(2637,plain,
( ( x = $true )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2567]) ).
thf(2640,plain,
( ( y = $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2559]) ).
thf(2641,plain,
( ( ( g @ x )
= $false )
| ( ( g @ y )
= $false ) ),
inference(extuni,[status(esa)],[2557]) ).
thf(2642,plain,
( ( y = $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(sim,[status(thm)],[2620]) ).
thf(2643,plain,
( ( x = $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(sim,[status(thm)],[2622]) ).
thf(2644,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2631]) ).
thf(2645,plain,
( ( ( f @ x )
= $true )
| ( ( g @ y )
= $false )
| ( x = $true ) ),
inference(sim,[status(thm)],[2629]) ).
thf(2646,plain,
( ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false )
| ( y = $true ) ),
inference(sim,[status(thm)],[2633]) ).
thf(2653,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ x )
= $false ) ),
inference(res,[status(thm)],[2538,2071]) ).
thf(2657,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( ( g @ y )
= $true ) ),
inference(res,[status(thm)],[2538,2069]) ).
thf(2660,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ x ) ) )
= $false )
| ( y = $true )
| ( x = $true ) ),
inference(res,[status(thm)],[2538,2008]) ).
thf(2665,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $true ) ),
inference(res,[status(thm)],[2538,1050]) ).
thf(2667,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true ) ),
inference(res,[status(thm)],[2538,1002]) ).
thf(2668,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ ( f @ ( f @ x ) ) )
= $true ) ),
inference(res,[status(thm)],[2538,1002]) ).
thf(2678,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ y )
= $false ) ),
inference(res,[status(thm)],[2538,130]) ).
thf(2681,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( ( g @ x )
= $true ) ),
inference(res,[status(thm)],[2538,80]) ).
thf(2686,plain,
( ( ( y = y )
= $false )
| ( ( f @ ( f @ x ) )
= $false )
| ( x = $false ) ),
inference(res,[status(thm)],[2538,77]) ).
thf(2695,plain,
( ( ( ( f @ ( f @ x ) )
= ( f @ ( f @ ( f @ x ) ) ) )
= $false )
| ( y = $true )
| ( ( g @ ( f @ x ) )
= $false ) ),
inference(res,[status(thm)],[2538,46]) ).
thf(2701,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2695]) ).
thf(2702,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( x = $false )
| ( ( f @ x )
= $false ) ),
inference(extuni,[status(esa)],[2695]) ).
thf(2703,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2695]) ).
thf(2704,plain,
( ( ( g @ ( f @ x ) )
= $false )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2695]) ).
thf(2705,plain,
( ( x = $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2686]) ).
thf(2706,plain,
( ( ( g @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2681]) ).
thf(2707,plain,
( ( ( g @ y )
= $false )
| ( ( f @ ( f @ x ) )
= $false ) ),
inference(extuni,[status(esa)],[2678]) ).
thf(2708,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2668]) ).
thf(2709,plain,
( ( ( f @ ( f @ ( f @ x ) ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2668]) ).
thf(2710,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $true )
| ( ( f @ x )
= $true ) ),
inference(extuni,[status(esa)],[2667]) ).
thf(2712,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(extuni,[status(esa)],[2667]) ).
thf(2714,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $true )
| ( x = $true ) ),
inference(extuni,[status(esa)],[2665]) ).
thf(2715,plain,
( ( ( g @ ( f @ x ) )
= $true )
| ( y = $true )
| ( ( f @ x )
= $false )
| ( x = $false ) ),
inference(extuni,[status(esa)],[2665]) ).
thf(2716,plain,
( ( x = $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2660]) ).
thf(2717,plain,
( ( ( g @ y )
= $true )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2657]) ).
thf(2720,plain,
( ( ( g @ x )
= $false )
| ( y = $true ) ),
inference(extuni,[status(esa)],[2653]) ).
thf(2721,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( ( f @ ( f @ x ) )
= $true ) ),
inference(sim,[status(thm)],[2712]) ).
thf(2722,plain,
( ( ( f @ x )
= $true )
| ( y = $true )
| ( x = $true ) ),
inference(sim,[status(thm)],[2710]) ).
thf(2723,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[15,2722,2721,2720,2717,2716,2715,2714,2709,2708,2707,2706,2705,2704,2703,2702,2701,2646,2645,2644,2643,2642,2641,2640,2637,2636,2635,2628,2627,2626,2625,2624,2621,2618,2617,2616,2615,2614,2613,2612,2556,2555,2554,2553,2552,2551,2550,2539,2538,2537,2536,2535,2477,2476,2475,2474,2473,2472,2471,2470,2469,2468,2467,2466,2465,2464,2459,2454,2449,2433,2424,2423,2422,2421,2420,2419,2329,2328,2327,2326,2325,2324,2323,2320,2319,2314,2313,2312,2309,2306,2305,2297,2296,2295,2294,2293,2292,2237,2236,2235,2234,2229,2228,2227,2226,2222,2221,2220,2219,2166,2165,2164,2163,2162,2161,2160,2153,2152,2151,2150,2148,2147,2140,2139,2138,2137,2136,2135,2087,2086,2085,2084,2071,2070,2069,2068,2067,2017,2016,2015,2014,2013,2012,2011,2010,2009,2008,2007,2006,2005,2004,2003,1970,1967,1966,1965,1964,1963,1962,1880,1879,1878,1877,1876,1875,1874,1873,1872,1871,1868,1857,1856,1851,1846,1845,1842,1768,1767,1766,1765,1764,1763,1762,1761,1760,1759,1740,1739,1734,1729,1726,1725,1645,1644,1643,1642,1641,1640,1639,1638,1637,1636,1633,1608,1607,1606,1605,1604,1601,1529,1528,1527,1526,1525,1520,1511,1510,1509,1508,1507,1506,1446,1445,1444,1443,1442,1441,1438,1437,1375,1374,1371,1370,1369,1368,1366,1365,1364,1320,1319,1318,1317,1316,1228,1225,1224,1221,1220,1137,1126,1125,1066,1065,1056,1055,1052,1051,1050,1049,1048,1004,1003,1002,1001,1000,999,907,905,902,901,900,812,811,810,721,720,719,642,641,332,298,140,139,130,129,80,79,77,68,66,65,49,46,45,41,24]) ).
thf(2724,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[2723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO041^2 : TPTP v9.3.1. Released v4.1.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 : n019.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:31:16 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.63/6.63
% 38.63/6.63 No.of.Axioms: 0
% 38.63/6.63
% 38.63/6.63 Length.of.Defs: 0
% 38.63/6.63
% 38.63/6.63 Contains.Choice.Funs: false
% 38.63/6.63 ...............................................................
% 38.63/6.63
% 38.63/6.63 ********************************
% 38.63/6.63 * All subproblems solved! *
% 38.63/6.63 ********************************
% 38.63/6.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:0,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:2723,loop_count:185,foatp_calls:39,translation:fof_full)
% 38.63/6.63
% 38.63/6.63 %**** Beginning of derivation protocol ****
% 38.63/6.63 % SZS output start CNFRefutation
% See solution above
% 38.63/6.63
% 38.63/6.63 %**** End of derivation protocol ****
% 38.63/6.63 %**** no. of clauses in derivation: 714 ****
% 38.63/6.63 %**** clause counter: 2723 ****
% 38.63/6.63
% 38.63/6.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:0,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:2723,loop_count:185,foatp_calls:39,translation:fof_full)
%------------------------------------------------------------------------------