%------------------------------------------------------------------------------
% File : DarwinFM---1.4.5
% Problem : HWV076-1 : TPTP v8.1.0. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 13:35:41 EDT 2022
% Result : Satisfiable 1.32s 1.51s
% Output : FiniteModel 1.37s
% Verified :
% SZS Type : FiniteModel
% Domain size : 2
% Comments :
%------------------------------------------------------------------------------
fof(interpretation_domain,fi_domain,
! [X] :
( X = e1
| X = e2 ) ).
fof(interpretation_domain_distinct,fi_domain,
e1 != e2 ).
fof(interpretation_terms,fi_functors,
( false = e1
& true = e2 ) ).
fof(interpretation_atoms,fi_predicates,
( ! [X0,X1,X2,X3] : esk1000_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1003_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1006_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1007_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1008_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1009_4(X0,X1,X2,X3)
& ( esk100_0
<=> $false )
& ! [X0,X1,X2,X3] : esk1012_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1015_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1016_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1019_4(X0,X1,X2,X3)
& ( esk101_0
<=> $false )
& ! [X0,X1,X2,X3] : esk1022_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1023_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1024_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1027_4(X0,X1,X2,X3)
& ( esk102_0
<=> $false )
& ! [X0,X1,X2,X3] : esk1030_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1031_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1034_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk1036_4(X0,X1,X2,X3)
& esk103_0
& ( esk104_0
<=> $false )
& ( esk105_0
<=> $false )
& ( esk106_0
<=> $false )
& ( esk107_0
<=> $false )
& ( esk108_0
<=> $false )
& ( esk109_0
<=> $false )
& ( esk10_0
<=> $false )
& ( esk110_0
<=> $false )
& ( esk111_0
<=> $false )
& ( esk112_0
<=> $false )
& esk113_0
& ( esk114_0
<=> $false )
& esk115_0
& esk116_0
& ( esk117_0
<=> $false )
& ( esk118_0
<=> $false )
& ( esk119_0
<=> $false )
& esk11_0
& ( esk120_0
<=> $false )
& ( esk121_0
<=> $false )
& ( esk122_0
<=> $false )
& ( esk123_0
<=> $false )
& ( esk124_0
<=> $false )
& ( esk125_0
<=> $false )
& ( esk126_0
<=> $false )
& ( esk127_0
<=> $false )
& ( esk128_0
<=> $false )
& ( esk129_0
<=> $false )
& ( esk12_0
<=> $false )
& ( esk130_0
<=> $false )
& ( esk131_0
<=> $false )
& ( esk132_0
<=> $false )
& ( esk133_0
<=> $false )
& esk134_0
& ( esk135_0
<=> $false )
& esk136_0
& esk137_0
& ( esk138_0
<=> $false )
& ( esk139_0
<=> $false )
& ( esk13_0
<=> $false )
& esk140_0
& ( esk141_0
<=> $false )
& ( esk142_0
<=> $false )
& ( esk143_0
<=> $false )
& ( esk144_0
<=> $false )
& ( esk145_0
<=> $false )
& ( esk146_0
<=> $false )
& ( esk147_0
<=> $false )
& ( esk148_0
<=> $false )
& ( esk149_0
<=> $false )
& ( esk14_0
<=> $false )
& ( esk150_0
<=> $false )
& esk151_0
& ( esk152_0
<=> $false )
& esk153_0
& ( esk154_0
<=> $false )
& esk155_0
& ( esk156_0
<=> $false )
& esk157_0
& ( esk158_0
<=> $false )
& ( esk159_0
<=> $false )
& ( esk15_0
<=> $false )
& ( esk160_0
<=> $false )
& ( esk161_0
<=> $false )
& ( esk162_0
<=> $false )
& ( esk163_0
<=> $false )
& ( esk164_0
<=> $false )
& ( esk165_0
<=> $false )
& ( esk166_0
<=> $false )
& ( esk167_0
<=> $false )
& ( esk168_0
<=> $false )
& ( esk169_0
<=> $false )
& esk16_0
& ( esk170_0
<=> $false )
& ( esk171_0
<=> $false )
& ( esk172_0
<=> $false )
& ( esk173_0
<=> $false )
& ( esk174_0
<=> $false )
& ( esk175_0
<=> $false )
& esk176_0
& ( esk177_0
<=> $false )
& ( esk178_0
<=> $false )
& esk179_0
& esk17_0
& ( esk180_0
<=> $false )
& ( esk181_0
<=> $false )
& ( esk182_0
<=> $false )
& ( esk183_0
<=> $false )
& ( esk184_0
<=> $false )
& esk185_0
& ( esk186_0
<=> $false )
& esk187_0
& esk188_0
& ( esk189_0
<=> $false )
& ( esk18_0
<=> $false )
& ( esk190_0
<=> $false )
& ( esk191_0
<=> $false )
& ( esk192_0
<=> $false )
& ( esk193_0
<=> $false )
& ( esk194_0
<=> $false )
& ( esk195_0
<=> $false )
& ( esk196_0
<=> $false )
& ( esk197_0
<=> $false )
& ( esk198_0
<=> $false )
& ( esk199_0
<=> $false )
& esk19_0
& esk1_0
& ( esk200_0
<=> $false )
& ( esk201_0
<=> $false )
& ( esk202_0
<=> $false )
& ( esk203_0
<=> $false )
& ( esk204_0
<=> $false )
& ( esk205_0
<=> $false )
& ( esk206_0
<=> $false )
& esk207_0
& ( esk208_0
<=> $false )
& ( esk209_0
<=> $false )
& esk20_0
& esk210_0
& ( esk211_0
<=> $false )
& esk212_0
& ( esk213_0
<=> $false )
& ( esk214_0
<=> $false )
& ( esk215_0
<=> $false )
& ( esk216_0
<=> $false )
& ( esk217_0
<=> $false )
& ( esk218_0
<=> $false )
& ( esk219_0
<=> $false )
& ( esk21_0
<=> $false )
& ( esk220_0
<=> $false )
& ( esk221_0
<=> $false )
& ( esk222_0
<=> $false )
& esk223_0
& ( esk224_0
<=> $false )
& ( esk225_0
<=> $false )
& ( esk226_0
<=> $false )
& ( esk227_0
<=> $false )
& ( esk228_0
<=> $false )
& ( esk229_0
<=> $false )
& ( esk22_0
<=> $false )
& ( esk230_0
<=> $false )
& ( esk231_0
<=> $false )
& ( esk232_0
<=> $false )
& esk233_0
& ( esk234_0
<=> $false )
& esk235_0
& ( esk236_0
<=> $false )
& ( esk237_0
<=> $false )
& ( esk238_0
<=> $false )
& esk239_0
& ( esk23_0
<=> $false )
& ( esk240_0
<=> $false )
& ( esk241_0
<=> $false )
& ( esk242_0
<=> $false )
& esk243_0
& ( esk244_0
<=> $false )
& ( esk245_0
<=> $false )
& ( esk246_0
<=> $false )
& ( esk247_0
<=> $false )
& ( esk248_0
<=> $false )
& esk249_0
& ( esk24_0
<=> $false )
& ( esk250_0
<=> $false )
& ( esk251_0
<=> $false )
& ( esk252_0
<=> $false )
& ( esk253_0
<=> $false )
& ( esk254_0
<=> $false )
& ( esk255_0
<=> $false )
& ( esk256_0
<=> $false )
& ( esk257_0
<=> $false )
& esk258_0
& ( esk259_0
<=> $false )
& ( esk25_0
<=> $false )
& esk260_0
& ( esk261_0
<=> $false )
& esk262_0
& ( esk263_0
<=> $false )
& ( esk264_0
<=> $false )
& ( esk265_0
<=> $false )
& ( esk266_0
<=> $false )
& ( esk267_0
<=> $false )
& ( esk268_0
<=> $false )
& ( esk269_0
<=> $false )
& esk26_0
& ( esk270_0
<=> $false )
& ( esk271_0
<=> $false )
& esk272_0
& ( esk273_0
<=> $false )
& esk274_0
& ( esk275_0
<=> $false )
& ( esk276_0
<=> $false )
& ( esk277_0
<=> $false )
& ( esk278_0
<=> $false )
& ( esk279_0
<=> $false )
& ( esk27_0
<=> $false )
& ( esk280_0
<=> $false )
& ( esk281_0
<=> $false )
& ( esk282_0
<=> $false )
& esk283_0
& ( esk284_0
<=> $false )
& ( esk285_0
<=> $false )
& ( esk286_0
<=> $false )
& ( esk287_0
<=> $false )
& ( esk288_0
<=> $false )
& ( esk289_0
<=> $false )
& esk28_0
& ( esk290_0
<=> $false )
& esk291_0
& ( esk292_0
<=> $false )
& ( esk293_0
<=> $false )
& ( esk294_0
<=> $false )
& ( esk295_0
<=> $false )
& ( esk296_0
<=> $false )
& ( esk297_0
<=> $false )
& ( esk298_0
<=> $false )
& esk299_0
& ( esk29_0
<=> $false )
& ( esk2_0
<=> $false )
& ( esk300_0
<=> $false )
& ( esk301_0
<=> $false )
& ( esk302_0
<=> $false )
& ( esk303_0
<=> $false )
& ( esk304_0
<=> $false )
& ( esk305_0
<=> $false )
& ( esk306_0
<=> $false )
& ( esk307_0
<=> $false )
& ( esk308_0
<=> $false )
& ( esk309_0
<=> $false )
& ( esk30_0
<=> $false )
& esk310_0
& ( esk311_0
<=> $false )
& ( esk312_0
<=> $false )
& ( esk313_0
<=> $false )
& ( esk314_0
<=> $false )
& ( esk315_0
<=> $false )
& ( esk316_0
<=> $false )
& ( esk317_0
<=> $false )
& esk318_0
& ( esk319_0
<=> $false )
& esk31_0
& esk320_0
& ( esk321_0
<=> $false )
& ( esk322_0
<=> $false )
& ( esk323_0
<=> $false )
& esk324_0
& ! [X0,X1,X2,X3] :
( esk325_4(X0,X1,X2,X3)
<=> X0 != e2 )
& ! [X0,X1,X2,X3] :
( esk326_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk327_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk328_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk329_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2 )
| X2 = e2 ) )
& ( esk32_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk330_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk333_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk336_4(X0,X1,X2,X3)
<=> X0 != e2 )
& ! [X0,X1,X2,X3] :
( esk337_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk338_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk339_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ( esk33_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk340_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk341_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk344_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ! [X0,X1,X2,X3] :
( esk347_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] : esk348_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk349_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| ( X1 = e2
& X3 = e2 )
| ( X2 = e2
& X3 = e2 ) ) )
& ( esk34_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk350_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk351_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk352_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk353_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ! [X0,X1,X2,X3] :
( esk354_4(X0,X1,X2,X3)
<=> ( X2 = e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk355_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk358_4(X0,X1,X2,X3)
<=> ( X2 = e2
| X3 = e2 ) )
& ( esk35_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk361_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk362_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk363_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk364_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk365_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk366_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk369_4(X0,X1,X2,X3)
<=> $false )
& ( esk36_0
<=> $false )
& ! [X0,X1,X2,X3] : esk372_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk373_4(X0,X1,X2,X3)
<=> ( X2 = e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk374_4(X0,X1,X2,X3)
<=> ( X1 = e2
| X2 = e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk375_4(X0,X1,X2,X3)
<=> X0 != e2 )
& ! [X0,X1,X2,X3] :
( esk376_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk377_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk378_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk379_4(X0,X1,X2,X3)
<=> ( X0 != e2
| X2 = e2 ) )
& esk37_0
& ! [X0,X1,X2,X3] :
( esk380_4(X0,X1,X2,X3)
<=> X0 != e2 )
& ! [X0,X1,X2,X3] :
( esk383_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk386_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk387_4(X0,X1,X2,X3)
<=> X1 = e2 )
& ! [X0,X1,X2,X3] :
( esk388_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk389_4(X0,X1,X2,X3)
<=> X3 != e2 )
& esk38_0
& ! [X0,X1,X2,X3] :
( esk390_4(X0,X1,X2,X3)
<=> ( X3 != e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk391_4(X0,X1,X2,X3)
<=> X1 = e2 )
& ! [X0,X1,X2,X3] :
( esk394_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk397_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] : esk398_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk399_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X2 != e2 )
| ( X0 = e1
& X1 = e2 )
| X3 != e2
| ( X1 = e2
& X2 = e2 )
| ( X1 = e2
& X3 = e2 ) ) )
& ( esk39_0
<=> $false )
& esk3_0
& ! [X0,X1,X2,X3] :
( esk400_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk401_4(X0,X1,X2,X3)
<=> X1 = e2 )
& ! [X0,X1,X2,X3] :
( esk402_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk403_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk404_4(X0,X1,X2,X3)
<=> ( X3 != e2
| X1 = e2
| X2 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk405_4(X0,X1,X2,X3)
<=> X1 = e2 )
& ! [X0,X1,X2,X3] :
( esk408_4(X0,X1,X2,X3)
<=> ( X3 != e2
| X2 = e2 ) )
& esk40_0
& ! [X0,X1,X2,X3] :
( esk411_4(X0,X1,X2,X3)
<=> X0 = e2 )
& ! [X0,X1,X2,X3] :
( esk412_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk413_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk414_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk415_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk416_4(X0,X1,X2,X3)
<=> X0 = e2 )
& ! [X0,X1,X2,X3] :
( esk419_4(X0,X1,X2,X3)
<=> X3 != e2 )
& esk41_0
& ! [X0,X1,X2,X3] :
( esk422_4(X0,X1,X2,X3)
<=> ( X3 = e2
& X1 != e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk423_4(X0,X1,X2,X3)
<=> ( X3 != e2
| X1 = e2
| X2 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk424_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e2
& X2 = e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 )
& ~ ( X2 = e2
& X3 = e2 ) )
| ( X1 = e2
& X3 != e2 )
| ( X2 = e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk425_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk426_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk427_4(X0,X1,X2,X3)
<=> X2 != e2 )
& ! [X0,X1,X2,X3] :
( esk428_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk429_4(X0,X1,X2,X3)
<=> $false )
& ( esk42_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk430_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk431_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk432_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk433_4(X0,X1,X2,X3)
<=> ~ ( X2 = e2
& X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk434_4(X0,X1,X2,X3)
<=> ~ ( X2 = e2
& X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk435_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk438_4(X0,X1,X2,X3)
<=> ~ ( X2 = e2
& X3 = e2 ) )
& ( esk43_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk441_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk442_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk445_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk448_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk449_4(X0,X1,X2,X3)
<=> $false )
& ( esk44_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk450_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk451_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk452_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk453_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk454_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk455_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk456_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk457_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk458_4(X0,X1,X2,X3)
<=> $false )
& ( esk45_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk461_4(X0,X1,X2,X3)
<=> X3 != e2 )
& ! [X0,X1,X2,X3] :
( esk464_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk465_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk468_4(X0,X1,X2,X3)
<=> $false )
& esk46_0
& ! [X0,X1,X2,X3] :
( esk471_4(X0,X1,X2,X3)
<=> ( X2 = e2
& X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk472_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk473_4(X0,X1,X2,X3)
<=> ( ( X0 = e1
& X2 = e2 )
| X3 != e2
| ( X1 = e1
& X2 = e2 )
| ( X2 = e2
& X3 = e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk474_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk475_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk476_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk477_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk478_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk479_4(X0,X1,X2,X3)
<=> $false )
& ( esk47_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk480_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk481_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk482_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk483_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk484_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk487_4(X0,X1,X2,X3)
<=> $false )
& ( esk48_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk490_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk491_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk494_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk497_4(X0,X1,X2,X3)
<=> X0 = e2 )
& ! [X0,X1,X2,X3] :
( esk498_4(X0,X1,X2,X3)
<=> X1 = e2 )
& ! [X0,X1,X2,X3] :
( esk499_4(X0,X1,X2,X3)
<=> X2 != e2 )
& ( esk49_0
<=> $false )
& ( esk4_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk500_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ! [X0,X1,X2,X3] :
( esk501_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk502_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk503_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk504_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk505_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk506_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk507_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ( esk50_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk510_4(X0,X1,X2,X3)
<=> ( X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk513_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk514_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk517_4(X0,X1,X2,X3)
<=> $false )
& ( esk51_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk520_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] : esk521_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk522_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2 )
| ( X0 = e1
& X1 = e2
& X3 = e1 )
| ( X1 = e2
& X2 = e2 )
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk523_4(X0,X1,X2,X3)
<=> X0 != e2 )
& ! [X0,X1,X2,X3] :
( esk524_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk525_4(X0,X1,X2,X3)
<=> X2 != e2 )
& ! [X0,X1,X2,X3] :
( esk526_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk527_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk528_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk529_4(X0,X1,X2,X3)
<=> $false )
& esk52_0
& ! [X0,X1,X2,X3] :
( esk530_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk531_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk532_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk533_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk536_4(X0,X1,X2,X3)
<=> X2 != e2 )
& ! [X0,X1,X2,X3] :
( esk539_4(X0,X1,X2,X3)
<=> $false )
& ( esk53_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk540_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk543_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk546_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk547_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk548_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk549_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ( esk54_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk550_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk551_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk552_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk553_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk554_4(X0,X1,X2,X3)
<=> ( ( X1 != e2
& X2 != e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk555_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ! [X0,X1,X2,X3] :
( esk556_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk559_4(X0,X1,X2,X3)
<=> X3 = e2 )
& esk55_0
& ! [X0,X1,X2,X3] :
( esk562_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk563_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk566_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk569_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2 ) )
& ( esk56_0
<=> $false )
& ! [X0,X1,X2,X3] : esk570_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk571_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| ( X1 != e2
& X2 != e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk572_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk573_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk574_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk575_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk576_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk577_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk578_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk579_4(X0,X1,X2,X3)
<=> $false )
& esk57_0
& ! [X0,X1,X2,X3] :
( esk580_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk581_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk582_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk585_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk588_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk589_4(X0,X1,X2,X3)
<=> $false )
& ( esk58_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk592_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk595_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk596_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk597_4(X0,X1,X2,X3)
<=> X2 = e2 )
& ! [X0,X1,X2,X3] :
( esk598_4(X0,X1,X2,X3)
<=> X3 = e2 )
& ! [X0,X1,X2,X3] :
( esk599_4(X0,X1,X2,X3)
<=> $false )
& esk59_0
& ( esk5_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk600_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk601_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk602_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk603_4(X0,X1,X2,X3)
<=> ( X1 != e2
| X2 = e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk604_4(X0,X1,X2,X3)
<=> ( X1 != e2
| X2 = e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk605_4(X0,X1,X2,X3)
<=> X1 != e2 )
& ! [X0,X1,X2,X3] :
( esk608_4(X0,X1,X2,X3)
<=> ( X2 = e2
| X3 = e2 ) )
& esk60_0
& ! [X0,X1,X2,X3] :
( esk611_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk612_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk615_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk618_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] : esk619_4(X0,X1,X2,X3)
& ( esk61_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk620_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e1
& X3 = e2 )
| ( X0 = e1
& X2 = e2
& X3 = e1 )
| ( X1 = e2
& X2 = e2 )
| X1 != e2
| ( X1 = e2
& X3 = e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk621_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk622_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk623_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk624_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk625_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk626_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk627_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk628_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk629_4(X0,X1,X2,X3)
<=> $false )
& ( esk62_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk630_4(X0,X1,X2,X3)
<=> ( X2 = e2
& X0 != e2
& X1 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk631_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk632_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk633_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X0 = e2
& X1 = e1
& X2 = e1 )
| ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X1 = e2
& X2 = e2
& X3 = e2
& X0 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X0 != e2
& X1 != e2 )
| ( ~ ( X0 = e2
& X2 = e2 )
& X1 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk634_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk635_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk637_4(X0,X1,X2,X3)
<=> $false )
& ( esk63_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk640_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk642_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk645_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X1 = e2
& X2 = e2
& X3 = e2
& X0 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X0 != e2
& X1 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk646_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk648_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 ) ) )
& esk64_0
& ! [X0,X1,X2,X3] :
( esk651_4(X0,X1,X2,X3)
<=> ( X2 = e2
& X0 != e2
& X1 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk653_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk656_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 != e2 )
| ( X0 = e2
& X1 = e2
& X3 = e2 )
| ( X0 = e2
& X2 = e2
& X3 = e2 )
| ( X0 = e2
& X2 = e2
& X1 != e2 )
| ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2
& X2 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk657_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk658_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk659_4(X0,X1,X2,X3)
<=> $false )
& ( esk65_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk660_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk661_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk662_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk663_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk664_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk665_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk666_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk667_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk668_4(X0,X1,X2,X3)
<=> ( X1 = e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk669_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X0 = e2
& X1 = e2
& X3 = e1 )
| ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X1 = e2
& X2 != e2
& X3 != e2 )
| ( X2 = e2
& X3 = e2
& X1 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 )
& X2 != e2 ) ) )
& esk66_0
& ! [X0,X1,X2,X3] :
( esk670_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk671_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk673_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk676_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk678_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X1 != e2
& X2 != e2
& X3 != e2 ) ) )
& esk67_0
& ! [X0,X1,X2,X3] :
( esk681_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X1 = e2
& X2 != e2
& X3 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk682_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk684_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk687_4(X0,X1,X2,X3)
<=> ( X1 = e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk689_4(X0,X1,X2,X3)
<=> ( X1 = e2
& X2 != e2
& X3 != e2 ) )
& ( esk68_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk692_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X2 != e2 )
| ( X0 = e1
& X1 = e2
& X2 = e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 )
| ( X1 = e2
& X3 = e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk693_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk694_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk695_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk696_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk697_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk698_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk699_4(X0,X1,X2,X3)
<=> $false )
& ( esk69_0
<=> $false )
& esk6_0
& ! [X0,X1,X2,X3] :
( esk700_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk701_4(X0,X1,X2,X3)
<=> ( X3 = e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk702_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk703_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk704_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk705_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X3 = e2
& X2 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk706_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk707_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk709_4(X0,X1,X2,X3)
<=> $false )
& esk70_0
& ! [X0,X1,X2,X3] :
( esk712_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk714_4(X0,X1,X2,X3)
<=> ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk717_4(X0,X1,X2,X3)
<=> ( X3 = e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk718_4(X0,X1,X2,X3)
<=> ( X3 = e2
& X2 != e2 ) )
& ( esk71_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk720_4(X0,X1,X2,X3)
<=> ( X3 = e2
& X2 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk723_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk725_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk728_4(X0,X1,X2,X3)
<=> ( ( X0 = e1
& X2 = e2 )
| ( X3 = e1
& ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) )
| ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
& X3 != e2 )
| ( X1 = e1
& X2 = e2 )
| ( X2 = e2
& X3 = e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk729_4(X0,X1,X2,X3)
<=> $false )
& ( esk72_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk730_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk731_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk732_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk733_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk734_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk735_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk736_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk737_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk738_4(X0,X1,X2,X3)
<=> ( X2 = e2
& X0 != e2
& X1 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk739_4(X0,X1,X2,X3)
<=> ( ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 ) ) )
& ( esk73_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk740_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk741_4(X0,X1,X2,X3)
<=> ( ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 )
| ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk742_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk743_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk745_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk748_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ( esk74_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk750_4(X0,X1,X2,X3)
<=> ( X1 != e2
& X2 != e2
& X3 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk753_4(X0,X1,X2,X3)
<=> ( ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk754_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk756_4(X0,X1,X2,X3)
<=> $false )
& ! [X0,X1,X2,X3] :
( esk759_4(X0,X1,X2,X3)
<=> ( ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 ) ) )
& esk75_0
& ! [X0,X1,X2,X3] :
( esk761_4(X0,X1,X2,X3)
<=> ( ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 )
& X3 != e2 )
| ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 )
& X3 != e2 ) ) )
& ! [X0,X1,X2,X3] :
( esk764_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk765_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk766_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk769_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| ( ~ ( X0 = e2
& X2 = e2 )
& X1 != e2 )
| X3 = e2 ) )
& ( esk76_0
<=> $false )
& ! [X0,X1,X2,X3] : esk772_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk774_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk777_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk779_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& esk77_0
& ! [X0,X1,X2,X3] : esk782_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk783_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk786_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e1 )
| ( X0 = e2
& X1 = e2
& X3 = e2 )
| X2 = e2
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 ) ) ) )
& ! [X0,X1,X2,X3] :
( esk788_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e1 )
| ( X0 = e2
& X1 = e2
& X3 = e2 )
| ( X0 = e2
& X1 = e1
& X2 = e2 )
| ( X0 = e2
& X2 = e2
& X3 = e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 )
& ~ ( X2 = e2
& X3 = e2 ) ) ) )
& ( esk78_0
<=> $false )
& ! [X0,X1,X2,X3] : esk791_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk793_4(X0,X1,X2,X3)
<=> ~ ( X2 = e2
& X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk796_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk799_4(X0,X1,X2,X3)
& ( esk79_0
<=> $false )
& ( esk7_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk800_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk803_4(X0,X1,X2,X3)
<=> ( ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 ) )
| X2 = e2 ) )
& ! [X0,X1,X2,X3] : esk806_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk807_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X2 != e2 ) )
& esk80_0
& ! [X0,X1,X2,X3] :
( esk810_4(X0,X1,X2,X3)
<=> ( ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 ) )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk813_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk814_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk817_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X1 = e1
& X2 = e2
& X3 = e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 ) ) ) )
& ( esk81_0
<=> $false )
& ! [X0,X1,X2,X3] : esk820_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk821_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk824_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2
& X3 != e2 )
| ( X0 = e1
& X1 = e2
& X3 = e2 )
| ( X1 = e2
& X2 = e2
& X3 = e2
& X0 != e2 )
| ( ~ ( X0 = e2
& X2 = e2 )
& ~ ( X1 = e2
& X2 = e2 ) ) ) )
& ! [X0,X1,X2,X3] : esk827_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk829_4(X0,X1,X2,X3)
<=> ( ( X2 = e2
& X3 = e2 )
| ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) ) )
& ( esk82_0
<=> $false )
& ! [X0,X1,X2,X3] : esk832_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk833_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk836_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X1 != e2 )
| ( X1 = e2
& ~ ( X0 = e2
& X2 = e2 ) )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk839_4(X0,X1,X2,X3)
& ( esk83_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk841_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| ( X0 = e2
& X1 = e2
& X3 = e1 )
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk844_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk845_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk848_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e1
& X2 = e1 )
| ( X0 = e2
& X3 = e2
& X1 != e2
& X2 != e2 )
| ( X0 = e1
& X1 = e2 )
| ( X0 = e1
& X1 = e1
& X2 = e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X2 = e2
& X3 = e2
& X0 != e2 )
| X3 != e2 ) )
& ( esk84_0
<=> $false )
& ! [X0,X1,X2,X3] : esk851_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk853_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X2 != e2 )
| X1 = e2
| X3 != e2 ) )
& ! [X0,X1,X2,X3] : esk856_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk857_4(X0,X1,X2,X3)
<=> ( X0 = e2
| X1 != e2 ) )
& esk85_0
& ! [X0,X1,X2,X3] :
( esk860_4(X0,X1,X2,X3)
<=> ( ( X0 = e1
& X1 = e2 )
| ( X1 = e2
& X3 = e2 )
| ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
& ~ ( X2 = e2
& X3 = e2 ) ) ) )
& ! [X0,X1,X2,X3] : esk863_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk865_4(X0,X1,X2,X3)
<=> ( ( X3 = e1
& ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) )
| ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk868_4(X0,X1,X2,X3)
& ( esk86_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk870_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk873_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk874_4(X0,X1,X2,X3)
<=> ( X0 != e2
| X2 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk877_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X3 = e2
& X2 != e2 )
| ( X0 = e2
& X2 = e1 )
| ( X0 = e1
& X1 = e2
& X2 = e2 )
| ( X1 = e2
& X3 = e2 )
| X3 != e2 ) )
& esk87_0
& ! [X0,X1,X2,X3] : esk880_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk881_4(X0,X1,X2,X3)
<=> ( X0 != e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk884_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 != e2 )
| ( X1 = e2
& X3 = e2
& X0 != e2 )
| ( X1 != e2
& X3 != e2 )
| X2 = e2 ) )
& ! [X0,X1,X2,X3] : esk887_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk888_4(X0,X1,X2,X3)
<=> ( X1 = e2
| X2 != e2 ) )
& ( esk88_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk891_4(X0,X1,X2,X3)
<=> ( ( X2 = e2
& ~ ( X0 = e2
& X1 = e2 ) )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk894_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk895_4(X0,X1,X2,X3)
<=> ( X1 = e2
| X2 != e2 ) )
& ! [X0,X1,X2,X3] :
( esk898_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X2 = e2
& X3 = e2
& X1 != e2 )
| ( X1 = e1
& X2 = e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 ) ) ) )
& ( esk89_0
<=> $false )
& ( esk8_0
<=> $false )
& ! [X0,X1,X2,X3] : esk901_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk902_4(X0,X1,X2,X3)
<=> ( X0 != e2
| X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk905_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X3 = e2 )
| ( X0 = e2
& X1 = e1 )
| ( X0 = e2
& X2 = e2
& X1 != e2 )
| ( X0 = e1
& X1 = e2
& X3 = e1 )
| ( X1 = e2
& X2 = e2
& X0 != e2
& X3 != e2 )
| X2 != e2 ) )
& ! [X0,X1,X2,X3] : esk908_4(X0,X1,X2,X3)
& ( esk90_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk910_4(X0,X1,X2,X3)
<=> ( ( X2 = e2
& X3 = e2 )
| ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) ) )
& ! [X0,X1,X2,X3] : esk913_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk914_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk917_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| X2 != e2
| X3 = e2 ) )
& ( esk91_0
<=> $false )
& ! [X0,X1,X2,X3] : esk920_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk922_4(X0,X1,X2,X3)
<=> ( ( X3 = e1
& ~ ( X0 = e2
& X1 = e2
& X2 = e2 ) )
| ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk925_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk927_4(X0,X1,X2,X3)
<=> ( ~ ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ( esk92_0
<=> $false )
& ! [X0,X1,X2,X3] : esk930_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk931_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk934_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X1 = e2
& X3 != e2 )
| ( X3 = e2
& X0 != e2
& X1 != e2 )
| X2 = e2 ) )
& ! [X0,X1,X2,X3] : esk937_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk938_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ( esk93_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk941_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| ( ~ ( X0 = e2
& X2 = e2 )
& ~ ( X1 = e2
& X2 = e2 ) )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk943_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| ( ~ ( X0 = e2
& X2 = e2 )
& X1 != e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk946_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk947_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ( esk94_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk950_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk952_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2
& X2 = e2 )
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk955_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk956_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ! [X0,X1,X2,X3] :
( esk959_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e2
& X1 = e1
& X2 = e2 )
| ( X0 = e2
& X2 = e2
& X3 = e2 )
| ( ~ ( X0 = e2
& X3 = e2 )
& ~ ( X1 = e2
& X3 = e2 )
& ~ ( X2 = e2
& X3 = e2 ) ) ) )
& ( esk95_0
<=> $false )
& ! [X0,X1,X2,X3] : esk962_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk964_4(X0,X1,X2,X3)
<=> ( X2 = e2
| X3 != e2 ) )
& ! [X0,X1,X2,X3] : esk967_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] :
( esk968_4(X0,X1,X2,X3)
<=> ~ ( X0 = e2
& X1 = e2 ) )
& ( esk96_0
<=> $false )
& ! [X0,X1,X2,X3] :
( esk971_4(X0,X1,X2,X3)
<=> ( ( X0 = e2
& X1 = e2 )
| X2 != e2
| X3 = e2 ) )
& ! [X0,X1,X2,X3] : esk974_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk975_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk976_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk977_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk978_4(X0,X1,X2,X3)
& ( esk97_0
<=> $false )
& ! [X0,X1,X2,X3] : esk981_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk984_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk985_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk988_4(X0,X1,X2,X3)
& ( esk98_0
<=> $false )
& ! [X0,X1,X2,X3] : esk991_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk992_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk993_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk996_4(X0,X1,X2,X3)
& ! [X0,X1,X2,X3] : esk999_4(X0,X1,X2,X3)
& ( esk99_0
<=> $false )
& esk9_0
& ! [X0] :
( p(X0)
<=> X0 = e2 ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : HWV076-1 : TPTP v8.1.0. Bugfixed v5.5.1.
% 0.05/0.12 % Command : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Fri Jun 17 07:56:42 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 Defaulting to tptp format.
% 1.32/1.51 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.32/1.51
% 1.32/1.51 MODEL (TPTP):
% 1.32/1.51 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------