%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SYO500^1.008 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : 300s
% DateTime : Wed Feb 25 09:54:23 AM UTC 2026
% Result : Theorem 1.58s 1.32s
% Output : Refutation 1.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 178
% Syntax : Number of formulae : 498 ( 39 unt; 0 typ; 128 def)
% Number of atoms : 3218 ( 778 equ; 0 cnn)
% Maximal formula atoms : 3 ( 6 avg)
% Number of connectives : 1266 ( 102 ~; 658 |; 0 &; 409 @)
% ( 97 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 140 ( 137 usr; 131 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_1,type,
f0: $o > $o ).
thf(func_def_2,type,
f1: $o > $o ).
thf(func_def_3,type,
f2: $o > $o ).
thf(func_def_4,type,
f3: $o > $o ).
thf(func_def_5,type,
f4: $o > $o ).
thf(func_def_6,type,
f5: $o > $o ).
thf(func_def_7,type,
f6: $o > $o ).
thf(func_def_8,type,
f7: $o > $o ).
thf(f789,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f238,f247,f256,f261,f274,f283,f292,f297,f306,f311,f316,f317,f330,f339,f348,f353,f366,f375,f384,f389,f394,f399,f400,f401,f414,f423,f432,f437,f450,f459,f468,f473,f478,f479,f484,f485,f498,f507,f516,f521,f526,f527,f532,f533,f538,f539,f544,f545,f550,f555,f556,f557,f562,f563,f568,f569,f570,f571,f572,f573,f578,f579,f584,f585,f590,f595,f596,f597,f606,f615,f620,f625,f630,f631,f636,f637,f642,f647,f648,f649,f650,f651,f652,f653,f658,f663,f664,f665,f674,f683,f684,f685,f686,f687,f688,f689,f690,f691,f696,f697,f702,f703,f708,f709,f714,f715,f716,f717,f718,f719,f720,f721,f722,f723,f724,f725,f726,f727,f728,f729,f730,f731,f732,f733,f734,f735,f740,f741,f742,f743,f744,f745,f746,f747,f748,f749,f750,f751,f752,f753,f754,f755,f756,f757,f758,f759,f760,f761,f762,f763,f764,f765,f766,f767,f768,f769,f770,f771,f772,f773,f774,f775,f776,f777,f778,f779,f780,f781,f782,f783,f784,f785,f786,f787,f788]) ).
thf(f788,plain,
( ( sF18 != $true )
| ( sF18 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f787,plain,
( ( sF24 != $true )
| ( sF24 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f786,plain,
( ( sF5 != $true )
| ( sF5 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f785,plain,
( ( sF19 != $true )
| ( sF19 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f784,plain,
( ( $true != sF21 )
| ( $false != sF21 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f783,plain,
( ( sF14 != $true )
| ( sF14 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f782,plain,
( ( sF26 != $true )
| ( sF26 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f781,plain,
( ( ( f0 @ $false )
!= $true )
| ( ( f0 @ $false )
!= $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f780,plain,
( ( ( f0 @ $true )
!= $true )
| ( ( f0 @ $true )
!= $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f779,plain,
( ( sF12 != $true )
| ( sF12 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f778,plain,
( ( sF27 != $true )
| ( sF27 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f777,plain,
( ( $true != sF9 )
| ( $false != sF9 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f776,plain,
( ( sF11 != $true )
| ( sF11 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f775,plain,
( ( sF30 != $true )
| ( sF30 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f774,plain,
( ( sF15 != $true )
| ( sF15 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f773,plain,
( ( $true != sF20 )
| ( $false != sF20 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f772,plain,
( ( sF13 != $true )
| ( sF13 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f771,plain,
( ( sF17 != $true )
| ( sF17 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f770,plain,
( ( x != $true )
| ( x != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f769,plain,
( ( $true != sF0 )
| ( $false != sF0 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f768,plain,
( ( sF1 != $true )
| ( sF1 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f767,plain,
( ( sF2 != $true )
| ( sF2 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f766,plain,
( ( sF6 != $true )
| ( sF6 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f765,plain,
( ( ( f6 @ $false )
!= $true )
| ( ( f6 @ $false )
!= $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f764,plain,
( ( sF3 != $true )
| ( sF3 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f763,plain,
( ( ( f6 @ $true )
!= $true )
| ( ( f6 @ $true )
!= $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f762,plain,
( ( sF23 != $true )
| ( sF23 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f761,plain,
( ( ( f1 @ $false )
!= $false )
| ( ( f1 @ $false )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f760,plain,
( ( sF28 != $false )
| ( sF28 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f759,plain,
( ( $false != sF29 )
| ( $true != sF29 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f758,plain,
( ( ( f1 @ $true )
!= $false )
| ( ( f1 @ $true )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f757,plain,
( ( ( f2 @ $false )
!= $false )
| ( ( f2 @ $false )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f756,plain,
( ( sF10 != $false )
| ( sF10 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f755,plain,
( ( ( f2 @ $true )
!= $false )
| ( ( f2 @ $true )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f754,plain,
( ( sF16 != $false )
| ( sF16 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f753,plain,
( ( $true
!= ( f5 @ $false ) )
| ( $false
!= ( f5 @ $false ) )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f752,plain,
( ( $true != sF22 )
| ( $false != sF22 )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f751,plain,
( ( sF4 != $false )
| ( sF4 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f750,plain,
( ( ( f5 @ $true )
!= $false )
| ( ( f5 @ $true )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f749,plain,
( ( $false
!= ( f4 @ $false ) )
| ( $true
!= ( f4 @ $false ) )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f748,plain,
( ( ( f4 @ $true )
!= $false )
| ( ( f4 @ $true )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f747,plain,
( ( sF7 != $false )
| ( sF7 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f746,plain,
( ( sF8 != $true )
| ( sF8 != $false )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f745,plain,
( ( ( f3 @ $false )
!= $false )
| ( ( f3 @ $false )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f744,plain,
( ( ( f3 @ $true )
!= $false )
| ( ( f3 @ $true )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f743,plain,
( ( sF25 != $false )
| ( sF25 != $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f742,plain,
( ( ( f7 @ $false )
!= $false )
| ( ( f7 @ $false )
!= $true )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f741,plain,
( ( $true
!= ( f7 @ $true ) )
| ( $false
!= ( f7 @ $true ) )
| ( $true = $false ) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
thf(f740,plain,
~ spl31_97,
inference(avatar_split_clause,[status(thm)],[f3,f737]) ).
thf(f737,definition,
( spl31_97
<=> ( $true = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_97])],[avatar_definition]) ).
thf(f3,plain,
$true != $false,
introduced(definition,[],[fool_axiom]) ).
thf(f735,plain,
( spl31_59
| spl31_93
| spl31_36 ),
inference(avatar_split_clause,[status(thm)],[f41,f386,f693,f495]) ).
thf(f495,definition,
( spl31_59
<=> ( sF18 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_59])],[avatar_definition]) ).
thf(f693,definition,
( spl31_93
<=> ( sF19 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_93])],[avatar_definition]) ).
thf(f386,definition,
( spl31_36
<=> ( $true
= ( f5 @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl31_36])],[avatar_definition]) ).
thf(f41,plain,
( ( $true
= ( f5 @ $false ) )
| ( sF19 = $false )
| ( sF18 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f39]) ).
thf(f39,plain,
( ( sF19
= ( f5 @ $false ) )
| ( sF18 = $true ) ),
inference(cases_simplifying,[status(thm)],[f25]) ).
thf(f25,definition,
( sF19
= ( f5 @ sF18 ) ),
introduced(definition,[],[function_definition]) ).
thf(f734,plain,
( spl31_59
| spl31_34
| spl31_94 ),
inference(avatar_split_clause,[status(thm)],[f40,f699,f377,f495]) ).
thf(f377,definition,
( spl31_34
<=> ( $false
= ( f5 @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl31_34])],[avatar_definition]) ).
thf(f699,definition,
( spl31_94
<=> ( sF19 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_94])],[avatar_definition]) ).
thf(f40,plain,
( ( sF19 = $true )
| ( sF18 = $true )
| ( $false
= ( f5 @ $false ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f39]) ).
thf(f733,plain,
( spl31_60
| spl31_32
| spl31_93 ),
inference(avatar_split_clause,[status(thm)],[f43,f693,f368,f500]) ).
thf(f500,definition,
( spl31_60
<=> ( sF18 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_60])],[avatar_definition]) ).
thf(f368,definition,
( spl31_32
<=> ( ( f5 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_32])],[avatar_definition]) ).
thf(f43,plain,
( ( sF19 = $false )
| ( ( f5 @ $true )
= $true )
| ( sF18 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f38]) ).
thf(f38,plain,
( ( sF19
= ( f5 @ $true ) )
| ( sF18 = $false ) ),
inference(cases_simplifying,[status(thm)],[f25]) ).
thf(f732,plain,
( spl31_94
| spl31_30
| spl31_60 ),
inference(avatar_split_clause,[status(thm)],[f42,f500,f359,f699]) ).
thf(f359,definition,
( spl31_30
<=> ( ( f5 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_30])],[avatar_definition]) ).
thf(f42,plain,
( ( sF19 = $true )
| ( sF18 = $false )
| ( ( f5 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f38]) ).
thf(f731,plain,
( spl31_24
| spl31_16
| spl31_55 ),
inference(avatar_split_clause,[status(thm)],[f47,f475,f294,f332]) ).
thf(f332,definition,
( spl31_24
<=> ( $true = sF22 ) ),
introduced(definition,[new_symbols(naming,[spl31_24])],[avatar_definition]) ).
thf(f294,definition,
( spl31_16
<=> ( ( f3 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_16])],[avatar_definition]) ).
thf(f475,definition,
( spl31_55
<=> ( sF23 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_55])],[avatar_definition]) ).
thf(f47,plain,
( ( sF23 = $false )
| ( ( f3 @ $false )
= $true )
| ( $true = sF22 ) ),
inference(binary_proxy_clausification,[status(thm)],[f45]) ).
thf(f45,plain,
( ( sF23
= ( f3 @ $false ) )
| ( $true = sF22 ) ),
inference(cases_simplifying,[status(thm)],[f29]) ).
thf(f29,definition,
( sF23
= ( f3 @ sF22 ) ),
introduced(definition,[],[function_definition]) ).
thf(f730,plain,
( spl31_24
| spl31_14
| spl31_56 ),
inference(avatar_split_clause,[status(thm)],[f46,f481,f285,f332]) ).
thf(f285,definition,
( spl31_14
<=> ( ( f3 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_14])],[avatar_definition]) ).
thf(f481,definition,
( spl31_56
<=> ( sF23 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_56])],[avatar_definition]) ).
thf(f46,plain,
( ( ( f3 @ $false )
= $false )
| ( sF23 = $true )
| ( $true = sF22 ) ),
inference(binary_proxy_clausification,[status(thm)],[f45]) ).
thf(f729,plain,
( spl31_10
| spl31_55
| spl31_21 ),
inference(avatar_split_clause,[status(thm)],[f49,f319,f475,f267]) ).
thf(f267,definition,
( spl31_10
<=> ( ( f3 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_10])],[avatar_definition]) ).
thf(f319,definition,
( spl31_21
<=> ( $false = sF22 ) ),
introduced(definition,[new_symbols(naming,[spl31_21])],[avatar_definition]) ).
thf(f49,plain,
( ( $false = sF22 )
| ( ( f3 @ $true )
= $true )
| ( sF23 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f44]) ).
thf(f44,plain,
( ( $false = sF22 )
| ( sF23
= ( f3 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f29]) ).
thf(f728,plain,
( spl31_13
| spl31_56
| spl31_21 ),
inference(avatar_split_clause,[status(thm)],[f48,f319,f481,f280]) ).
thf(f280,definition,
( spl31_13
<=> ( ( f3 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_13])],[avatar_definition]) ).
thf(f48,plain,
( ( ( f3 @ $true )
= $false )
| ( sF23 = $true )
| ( $false = sF22 ) ),
inference(binary_proxy_clausification,[status(thm)],[f44]) ).
thf(f727,plain,
( spl31_91
| spl31_87
| spl31_81 ),
inference(avatar_split_clause,[status(thm)],[f53,f617,f655,f676]) ).
thf(f676,definition,
( spl31_91
<=> ( sF15 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_91])],[avatar_definition]) ).
thf(f655,definition,
( spl31_87
<=> ( sF14 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_87])],[avatar_definition]) ).
thf(f617,definition,
( spl31_81
<=> ( ( f0 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_81])],[avatar_definition]) ).
thf(f53,plain,
( ( sF14 = $true )
| ( ( f0 @ $false )
= $true )
| ( sF15 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f51]) ).
thf(f51,plain,
( ( sF14 = $true )
| ( sF15
= ( f0 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f21]) ).
thf(f21,definition,
( sF15
= ( f0 @ sF14 ) ),
introduced(definition,[],[function_definition]) ).
thf(f726,plain,
( spl31_82
| spl31_87
| spl31_89 ),
inference(avatar_split_clause,[status(thm)],[f52,f667,f655,f622]) ).
thf(f622,definition,
( spl31_82
<=> ( ( f0 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_82])],[avatar_definition]) ).
thf(f667,definition,
( spl31_89
<=> ( sF15 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_89])],[avatar_definition]) ).
thf(f52,plain,
( ( sF14 = $true )
| ( ( f0 @ $false )
= $false )
| ( sF15 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f51]) ).
thf(f725,plain,
( spl31_88
| spl31_80
| spl31_91 ),
inference(avatar_split_clause,[status(thm)],[f55,f676,f612,f660]) ).
thf(f660,definition,
( spl31_88
<=> ( sF14 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_88])],[avatar_definition]) ).
thf(f612,definition,
( spl31_80
<=> ( ( f0 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_80])],[avatar_definition]) ).
thf(f55,plain,
( ( sF14 = $false )
| ( ( f0 @ $true )
= $true )
| ( sF15 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f50]) ).
thf(f50,plain,
( ( sF14 = $false )
| ( sF15
= ( f0 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f21]) ).
thf(f724,plain,
( spl31_89
| spl31_77
| spl31_88 ),
inference(avatar_split_clause,[status(thm)],[f54,f660,f599,f667]) ).
thf(f599,definition,
( spl31_77
<=> ( ( f0 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_77])],[avatar_definition]) ).
thf(f54,plain,
( ( sF15 = $true )
| ( sF14 = $false )
| ( ( f0 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f50]) ).
thf(f723,plain,
( spl31_81
| spl31_51
| spl31_92 ),
inference(avatar_split_clause,[status(thm)],[f59,f680,f456,f617]) ).
thf(f456,definition,
( spl31_51
<=> ( $true = sF29 ) ),
introduced(definition,[new_symbols(naming,[spl31_51])],[avatar_definition]) ).
thf(f680,definition,
( spl31_92
<=> ( sF30 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_92])],[avatar_definition]) ).
thf(f59,plain,
( ( ( f0 @ $false )
= $true )
| ( $true = sF29 )
| ( sF30 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f57]) ).
thf(f57,plain,
( ( $true = sF29 )
| ( sF30
= ( f0 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f36]) ).
thf(f36,definition,
( sF30
= ( f0 @ sF29 ) ),
introduced(definition,[],[function_definition]) ).
thf(f722,plain,
( spl31_51
| spl31_90
| spl31_82 ),
inference(avatar_split_clause,[status(thm)],[f58,f622,f671,f456]) ).
thf(f671,definition,
( spl31_90
<=> ( sF30 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_90])],[avatar_definition]) ).
thf(f58,plain,
( ( sF30 = $true )
| ( ( f0 @ $false )
= $false )
| ( $true = sF29 ) ),
inference(binary_proxy_clausification,[status(thm)],[f57]) ).
thf(f721,plain,
( spl31_80
| spl31_48
| spl31_92 ),
inference(avatar_split_clause,[status(thm)],[f61,f680,f443,f612]) ).
thf(f443,definition,
( spl31_48
<=> ( $false = sF29 ) ),
introduced(definition,[new_symbols(naming,[spl31_48])],[avatar_definition]) ).
thf(f61,plain,
( ( ( f0 @ $true )
= $true )
| ( $false = sF29 )
| ( sF30 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f56]) ).
thf(f56,plain,
( ( sF30
= ( f0 @ $true ) )
| ( $false = sF29 ) ),
inference(cases_simplifying,[status(thm)],[f36]) ).
thf(f720,plain,
( spl31_77
| spl31_90
| spl31_48 ),
inference(avatar_split_clause,[status(thm)],[f60,f443,f671,f599]) ).
thf(f60,plain,
( ( ( f0 @ $true )
= $false )
| ( $false = sF29 )
| ( sF30 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f56]) ).
thf(f719,plain,
( spl31_95
| spl31_31
| spl31_28 ),
inference(avatar_split_clause,[status(thm)],[f65,f350,f363,f705]) ).
thf(f705,definition,
( spl31_95
<=> ( sF5 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_95])],[avatar_definition]) ).
thf(f363,definition,
( spl31_31
<=> ( sF4 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_31])],[avatar_definition]) ).
thf(f350,definition,
( spl31_28
<=> ( $true
= ( f4 @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl31_28])],[avatar_definition]) ).
thf(f65,plain,
( ( sF5 = $false )
| ( $true
= ( f4 @ $false ) )
| ( sF4 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f63]) ).
thf(f63,plain,
( ( sF5
= ( f4 @ $false ) )
| ( sF4 = $true ) ),
inference(cases_simplifying,[status(thm)],[f11]) ).
thf(f11,definition,
( ( f4 @ sF4 )
= sF5 ),
introduced(definition,[],[function_definition]) ).
thf(f718,plain,
( spl31_31
| spl31_27
| spl31_96 ),
inference(avatar_split_clause,[status(thm)],[f64,f711,f345,f363]) ).
thf(f345,definition,
( spl31_27
<=> ( $false
= ( f4 @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl31_27])],[avatar_definition]) ).
thf(f711,definition,
( spl31_96
<=> ( sF5 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_96])],[avatar_definition]) ).
thf(f64,plain,
( ( sF5 = $true )
| ( $false
= ( f4 @ $false ) )
| ( sF4 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f63]) ).
thf(f717,plain,
( spl31_23
| spl31_33
| spl31_95 ),
inference(avatar_split_clause,[status(thm)],[f67,f705,f372,f327]) ).
thf(f327,definition,
( spl31_23
<=> ( ( f4 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_23])],[avatar_definition]) ).
thf(f372,definition,
( spl31_33
<=> ( sF4 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_33])],[avatar_definition]) ).
thf(f67,plain,
( ( ( f4 @ $true )
= $true )
| ( sF4 = $false )
| ( sF5 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f62]) ).
thf(f62,plain,
( ( sF4 = $false )
| ( sF5
= ( f4 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f11]) ).
thf(f716,plain,
( spl31_25
| spl31_96
| spl31_33 ),
inference(avatar_split_clause,[status(thm)],[f66,f372,f711,f336]) ).
thf(f336,definition,
( spl31_25
<=> ( ( f4 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_25])],[avatar_definition]) ).
thf(f66,plain,
( ( sF4 = $false )
| ( sF5 = $true )
| ( ( f4 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f62]) ).
thf(f715,plain,
( spl31_65
| spl31_96
| spl31_28 ),
inference(avatar_split_clause,[status(thm)],[f71,f350,f711,f523]) ).
thf(f523,definition,
( spl31_65
<=> ( sF6 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_65])],[avatar_definition]) ).
thf(f71,plain,
( ( sF6 = $false )
| ( $true
= ( f4 @ $false ) )
| ( sF5 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f69]) ).
thf(f69,plain,
( ( sF5 = $true )
| ( sF6
= ( f4 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f12]) ).
thf(f12,definition,
( sF6
= ( f4 @ sF5 ) ),
introduced(definition,[],[function_definition]) ).
thf(f714,plain,
( spl31_66
| spl31_96
| spl31_27 ),
inference(avatar_split_clause,[status(thm)],[f70,f345,f711,f529]) ).
thf(f529,definition,
( spl31_66
<=> ( sF6 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_66])],[avatar_definition]) ).
thf(f70,plain,
( ( $false
= ( f4 @ $false ) )
| ( sF5 = $true )
| ( sF6 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f69]) ).
thf(f709,plain,
( spl31_65
| spl31_95
| spl31_23 ),
inference(avatar_split_clause,[status(thm)],[f73,f327,f705,f523]) ).
thf(f73,plain,
( ( sF5 = $false )
| ( sF6 = $false )
| ( ( f4 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f68]) ).
thf(f68,plain,
( ( sF5 = $false )
| ( sF6
= ( f4 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f12]) ).
thf(f708,plain,
( spl31_25
| spl31_95
| spl31_66 ),
inference(avatar_split_clause,[status(thm)],[f72,f529,f705,f336]) ).
thf(f72,plain,
( ( sF5 = $false )
| ( ( f4 @ $true )
= $false )
| ( sF6 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f68]) ).
thf(f703,plain,
( spl31_83
| spl31_94
| spl31_36 ),
inference(avatar_split_clause,[status(thm)],[f77,f386,f699,f627]) ).
thf(f627,definition,
( spl31_83
<=> ( $false = sF20 ) ),
introduced(definition,[new_symbols(naming,[spl31_83])],[avatar_definition]) ).
thf(f77,plain,
( ( $false = sF20 )
| ( sF19 = $true )
| ( $true
= ( f5 @ $false ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f75]) ).
thf(f75,plain,
( ( sF20
= ( f5 @ $false ) )
| ( sF19 = $true ) ),
inference(cases_simplifying,[status(thm)],[f26]) ).
thf(f26,definition,
( ( f5 @ sF19 )
= sF20 ),
introduced(definition,[],[function_definition]) ).
thf(f702,plain,
( spl31_34
| spl31_94
| spl31_84 ),
inference(avatar_split_clause,[status(thm)],[f76,f633,f699,f377]) ).
thf(f633,definition,
( spl31_84
<=> ( $true = sF20 ) ),
introduced(definition,[new_symbols(naming,[spl31_84])],[avatar_definition]) ).
thf(f76,plain,
( ( sF19 = $true )
| ( $true = sF20 )
| ( $false
= ( f5 @ $false ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f75]) ).
thf(f697,plain,
( spl31_84
| spl31_30
| spl31_93 ),
inference(avatar_split_clause,[status(thm)],[f79,f693,f359,f633]) ).
thf(f79,plain,
( ( sF19 = $false )
| ( ( f5 @ $true )
= $false )
| ( $true = sF20 ) ),
inference(binary_proxy_clausification,[status(thm)],[f74]) ).
thf(f74,plain,
( ( sF19 = $false )
| ( ( f5 @ $true )
= sF20 ) ),
inference(cases_simplifying,[status(thm)],[f26]) ).
thf(f696,plain,
( spl31_83
| spl31_93
| spl31_32 ),
inference(avatar_split_clause,[status(thm)],[f78,f368,f693,f627]) ).
thf(f78,plain,
( ( ( f5 @ $true )
= $true )
| ( sF19 = $false )
| ( $false = sF20 ) ),
inference(binary_proxy_clausification,[status(thm)],[f74]) ).
thf(f691,plain,
( spl31_73
| spl31_53
| spl31_85 ),
inference(avatar_split_clause,[status(thm)],[f83,f639,f465,f575]) ).
thf(f575,definition,
( spl31_73
<=> ( sF27 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_73])],[avatar_definition]) ).
thf(f465,definition,
( spl31_53
<=> ( ( f1 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_53])],[avatar_definition]) ).
thf(f639,definition,
( spl31_85
<=> ( sF26 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_85])],[avatar_definition]) ).
thf(f83,plain,
( ( ( f1 @ $false )
= $true )
| ( sF26 = $true )
| ( sF27 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f81]) ).
thf(f81,plain,
( ( sF26 = $true )
| ( sF27
= ( f1 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f33]) ).
thf(f33,definition,
( sF27
= ( f1 @ sF26 ) ),
introduced(definition,[],[function_definition]) ).
thf(f690,plain,
( spl31_54
| spl31_74
| spl31_85 ),
inference(avatar_split_clause,[status(thm)],[f82,f639,f581,f470]) ).
thf(f470,definition,
( spl31_54
<=> ( ( f1 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_54])],[avatar_definition]) ).
thf(f581,definition,
( spl31_74
<=> ( sF27 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_74])],[avatar_definition]) ).
thf(f82,plain,
( ( sF26 = $true )
| ( ( f1 @ $false )
= $false )
| ( sF27 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f81]) ).
thf(f689,plain,
( spl31_73
| spl31_49
| spl31_86 ),
inference(avatar_split_clause,[status(thm)],[f85,f644,f447,f575]) ).
thf(f447,definition,
( spl31_49
<=> ( ( f1 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_49])],[avatar_definition]) ).
thf(f644,definition,
( spl31_86
<=> ( sF26 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_86])],[avatar_definition]) ).
thf(f85,plain,
( ( sF26 = $false )
| ( sF27 = $false )
| ( ( f1 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f80]) ).
thf(f80,plain,
( ( sF26 = $false )
| ( sF27
= ( f1 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f33]) ).
thf(f688,plain,
( spl31_86
| spl31_74
| spl31_50 ),
inference(avatar_split_clause,[status(thm)],[f84,f452,f581,f644]) ).
thf(f452,definition,
( spl31_50
<=> ( ( f1 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_50])],[avatar_definition]) ).
thf(f84,plain,
( ( ( f1 @ $true )
= $false )
| ( sF26 = $false )
| ( sF27 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f80]) ).
thf(f687,plain,
( spl31_72
| spl31_45
| spl31_19 ),
inference(avatar_split_clause,[status(thm)],[f89,f308,f429,f565]) ).
thf(f565,definition,
( spl31_72
<=> ( $true = sF9 ) ),
introduced(definition,[new_symbols(naming,[spl31_72])],[avatar_definition]) ).
thf(f429,definition,
( spl31_45
<=> ( ( f2 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_45])],[avatar_definition]) ).
thf(f308,definition,
( spl31_19
<=> ( sF8 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_19])],[avatar_definition]) ).
thf(f89,plain,
( ( ( f2 @ $false )
= $false )
| ( sF8 = $true )
| ( $true = sF9 ) ),
inference(binary_proxy_clausification,[status(thm)],[f87]) ).
thf(f87,plain,
( ( sF8 = $true )
| ( ( f2 @ $false )
= sF9 ) ),
inference(cases_simplifying,[status(thm)],[f15]) ).
thf(f15,definition,
( ( f2 @ sF8 )
= sF9 ),
introduced(definition,[],[function_definition]) ).
thf(f686,plain,
( spl31_19
| spl31_46
| spl31_71 ),
inference(avatar_split_clause,[status(thm)],[f88,f559,f434,f308]) ).
thf(f434,definition,
( spl31_46
<=> ( ( f2 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_46])],[avatar_definition]) ).
thf(f559,definition,
( spl31_71
<=> ( $false = sF9 ) ),
introduced(definition,[new_symbols(naming,[spl31_71])],[avatar_definition]) ).
thf(f88,plain,
( ( ( f2 @ $false )
= $true )
| ( $false = sF9 )
| ( sF8 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f87]) ).
thf(f685,plain,
( spl31_39
| spl31_72
| spl31_18 ),
inference(avatar_split_clause,[status(thm)],[f91,f303,f565,f403]) ).
thf(f403,definition,
( spl31_39
<=> ( ( f2 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_39])],[avatar_definition]) ).
thf(f303,definition,
( spl31_18
<=> ( sF8 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_18])],[avatar_definition]) ).
thf(f91,plain,
( ( ( f2 @ $true )
= $false )
| ( sF8 = $false )
| ( $true = sF9 ) ),
inference(binary_proxy_clausification,[status(thm)],[f86]) ).
thf(f86,plain,
( ( ( f2 @ $true )
= sF9 )
| ( sF8 = $false ) ),
inference(cases_simplifying,[status(thm)],[f15]) ).
thf(f684,plain,
( spl31_42
| spl31_71
| spl31_18 ),
inference(avatar_split_clause,[status(thm)],[f90,f303,f559,f416]) ).
thf(f416,definition,
( spl31_42
<=> ( ( f2 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_42])],[avatar_definition]) ).
thf(f90,plain,
( ( ( f2 @ $true )
= $true )
| ( $false = sF9 )
| ( sF8 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f86]) ).
thf(f683,plain,
( spl31_91
| spl31_92 ),
inference(avatar_split_clause,[status(thm)],[f93,f680,f676]) ).
thf(f93,plain,
( ( sF30 = $false )
| ( sF15 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f37,plain,
sF30 != sF15,
inference(definition_folding,[status(thm)],[f5,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f6,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6]) ).
thf(f7,definition,
( sF1
= ( f6 @ sF0 ) ),
introduced(definition,[],[function_definition]) ).
thf(f8,definition,
( sF2
= ( f6 @ sF1 ) ),
introduced(definition,[],[function_definition]) ).
thf(f9,definition,
( sF3
= ( f6 @ sF2 ) ),
introduced(definition,[],[function_definition]) ).
thf(f10,definition,
( ( f5 @ sF3 )
= sF4 ),
introduced(definition,[],[function_definition]) ).
thf(f13,definition,
( sF7
= ( f4 @ sF6 ) ),
introduced(definition,[],[function_definition]) ).
thf(f14,definition,
( sF8
= ( f3 @ sF7 ) ),
introduced(definition,[],[function_definition]) ).
thf(f16,definition,
( ( f2 @ sF9 )
= sF10 ),
introduced(definition,[],[function_definition]) ).
thf(f17,definition,
( sF11
= ( f2 @ sF10 ) ),
introduced(definition,[],[function_definition]) ).
thf(f18,definition,
( ( f1 @ sF11 )
= sF12 ),
introduced(definition,[],[function_definition]) ).
thf(f19,definition,
( sF13
= ( f0 @ sF12 ) ),
introduced(definition,[],[function_definition]) ).
thf(f20,definition,
( ( f0 @ sF13 )
= sF14 ),
introduced(definition,[],[function_definition]) ).
thf(f6,definition,
( ( f7 @ x )
= sF0 ),
introduced(definition,[],[function_definition]) ).
thf(f22,definition,
( sF16
= ( f7 @ sF0 ) ),
introduced(definition,[],[function_definition]) ).
thf(f23,definition,
( sF17
= ( f7 @ sF16 ) ),
introduced(definition,[],[function_definition]) ).
thf(f24,definition,
( sF18
= ( f6 @ sF17 ) ),
introduced(definition,[],[function_definition]) ).
thf(f27,definition,
( ( f5 @ sF20 )
= sF21 ),
introduced(definition,[],[function_definition]) ).
thf(f28,definition,
( ( f4 @ sF21 )
= sF22 ),
introduced(definition,[],[function_definition]) ).
thf(f30,definition,
( ( f3 @ sF23 )
= sF24 ),
introduced(definition,[],[function_definition]) ).
thf(f31,definition,
( ( f3 @ sF24 )
= sF25 ),
introduced(definition,[],[function_definition]) ).
thf(f32,definition,
( sF26
= ( f2 @ sF25 ) ),
introduced(definition,[],[function_definition]) ).
thf(f34,definition,
( sF28
= ( f1 @ sF27 ) ),
introduced(definition,[],[function_definition]) ).
thf(f35,definition,
( ( f1 @ sF28 )
= sF29 ),
introduced(definition,[],[function_definition]) ).
thf(f5,plain,
( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
!= ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
thf(f4,plain,
( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
!= ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(flattening,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
!= ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
= ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.Tk9QRBkYJG/DTF2THF_18236.p',kaminski8) ).
thf(f674,plain,
( spl31_89
| spl31_90 ),
inference(avatar_split_clause,[status(thm)],[f92,f671,f667]) ).
thf(f92,plain,
( ( sF15 = $true )
| ( sF30 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f37]) ).
thf(f665,plain,
( spl31_82
| spl31_87
| spl31_78 ),
inference(avatar_split_clause,[status(thm)],[f97,f603,f655,f622]) ).
thf(f603,definition,
( spl31_78
<=> ( sF13 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_78])],[avatar_definition]) ).
thf(f97,plain,
( ( sF14 = $true )
| ( ( f0 @ $false )
= $false )
| ( sF13 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f95]) ).
thf(f95,plain,
( ( ( f0 @ $false )
= sF14 )
| ( sF13 = $true ) ),
inference(cases_simplifying,[status(thm)],[f20]) ).
thf(f664,plain,
( spl31_81
| spl31_88
| spl31_78 ),
inference(avatar_split_clause,[status(thm)],[f96,f603,f660,f617]) ).
thf(f96,plain,
( ( sF14 = $false )
| ( sF13 = $true )
| ( ( f0 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f95]) ).
thf(f663,plain,
( spl31_80
| spl31_79
| spl31_88 ),
inference(avatar_split_clause,[status(thm)],[f99,f660,f608,f612]) ).
thf(f608,definition,
( spl31_79
<=> ( sF13 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_79])],[avatar_definition]) ).
thf(f99,plain,
( ( sF14 = $false )
| ( sF13 = $false )
| ( ( f0 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f94]) ).
thf(f94,plain,
( ( sF14
= ( f0 @ $true ) )
| ( sF13 = $false ) ),
inference(cases_simplifying,[status(thm)],[f20]) ).
thf(f658,plain,
( spl31_87
| spl31_79
| spl31_77 ),
inference(avatar_split_clause,[status(thm)],[f98,f599,f608,f655]) ).
thf(f98,plain,
( ( ( f0 @ $true )
= $false )
| ( sF14 = $true )
| ( sF13 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f94]) ).
thf(f653,plain,
( spl31_67
| spl31_69
| spl31_64 ),
inference(avatar_split_clause,[status(thm)],[f103,f518,f547,f535]) ).
thf(f535,definition,
( spl31_67
<=> ( sF2 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_67])],[avatar_definition]) ).
thf(f547,definition,
( spl31_69
<=> ( sF1 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_69])],[avatar_definition]) ).
thf(f518,definition,
( spl31_64
<=> ( ( f6 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_64])],[avatar_definition]) ).
thf(f103,plain,
( ( ( f6 @ $false )
= $true )
| ( sF1 = $true )
| ( sF2 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f101]) ).
thf(f101,plain,
( ( sF2
= ( f6 @ $false ) )
| ( sF1 = $true ) ),
inference(cases_simplifying,[status(thm)],[f8]) ).
thf(f652,plain,
( spl31_63
| spl31_68
| spl31_69 ),
inference(avatar_split_clause,[status(thm)],[f102,f547,f541,f513]) ).
thf(f513,definition,
( spl31_63
<=> ( ( f6 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_63])],[avatar_definition]) ).
thf(f541,definition,
( spl31_68
<=> ( sF2 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_68])],[avatar_definition]) ).
thf(f102,plain,
( ( sF2 = $true )
| ( sF1 = $true )
| ( ( f6 @ $false )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f101]) ).
thf(f651,plain,
( spl31_67
| spl31_70
| spl31_61 ),
inference(avatar_split_clause,[status(thm)],[f105,f504,f552,f535]) ).
thf(f552,definition,
( spl31_70
<=> ( sF1 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_70])],[avatar_definition]) ).
thf(f504,definition,
( spl31_61
<=> ( ( f6 @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_61])],[avatar_definition]) ).
thf(f105,plain,
( ( sF2 = $false )
| ( sF1 = $false )
| ( ( f6 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f100]) ).
thf(f100,plain,
( ( sF2
= ( f6 @ $true ) )
| ( sF1 = $false ) ),
inference(cases_simplifying,[status(thm)],[f8]) ).
thf(f650,plain,
( spl31_68
| spl31_57
| spl31_70 ),
inference(avatar_split_clause,[status(thm)],[f104,f552,f487,f541]) ).
thf(f487,definition,
( spl31_57
<=> ( ( f6 @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_57])],[avatar_definition]) ).
thf(f104,plain,
( ( ( f6 @ $true )
= $false )
| ( sF2 = $true )
| ( sF1 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f100]) ).
thf(f649,plain,
( spl31_12
| spl31_45
| spl31_85 ),
inference(avatar_split_clause,[status(thm)],[f109,f639,f429,f276]) ).
thf(f276,definition,
( spl31_12
<=> ( sF25 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_12])],[avatar_definition]) ).
thf(f109,plain,
( ( sF26 = $true )
| ( sF25 = $true )
| ( ( f2 @ $false )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f107]) ).
thf(f107,plain,
( ( ( f2 @ $false )
= sF26 )
| ( sF25 = $true ) ),
inference(cases_simplifying,[status(thm)],[f32]) ).
thf(f648,plain,
( spl31_12
| spl31_46
| spl31_86 ),
inference(avatar_split_clause,[status(thm)],[f108,f644,f434,f276]) ).
thf(f108,plain,
( ( sF25 = $true )
| ( ( f2 @ $false )
= $true )
| ( sF26 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f107]) ).
thf(f647,plain,
( spl31_86
| spl31_11
| spl31_42 ),
inference(avatar_split_clause,[status(thm)],[f111,f416,f271,f644]) ).
thf(f271,definition,
( spl31_11
<=> ( sF25 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_11])],[avatar_definition]) ).
thf(f111,plain,
( ( sF25 = $false )
| ( sF26 = $false )
| ( ( f2 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f106]) ).
thf(f106,plain,
( ( sF26
= ( f2 @ $true ) )
| ( sF25 = $false ) ),
inference(cases_simplifying,[status(thm)],[f32]) ).
thf(f642,plain,
( spl31_39
| spl31_85
| spl31_11 ),
inference(avatar_split_clause,[status(thm)],[f110,f271,f639,f403]) ).
thf(f110,plain,
( ( sF26 = $true )
| ( ( f2 @ $true )
= $false )
| ( sF25 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f106]) ).
thf(f637,plain,
( spl31_36
| spl31_22
| spl31_84 ),
inference(avatar_split_clause,[status(thm)],[f115,f633,f323,f386]) ).
thf(f323,definition,
( spl31_22
<=> ( $false = sF21 ) ),
introduced(definition,[new_symbols(naming,[spl31_22])],[avatar_definition]) ).
thf(f115,plain,
( ( $false = sF21 )
| ( $true = sF20 )
| ( $true
= ( f5 @ $false ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f113]) ).
thf(f113,plain,
( ( $true = sF20 )
| ( sF21
= ( f5 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f27]) ).
thf(f636,plain,
( spl31_84
| spl31_26
| spl31_34 ),
inference(avatar_split_clause,[status(thm)],[f114,f377,f341,f633]) ).
thf(f341,definition,
( spl31_26
<=> ( $true = sF21 ) ),
introduced(definition,[new_symbols(naming,[spl31_26])],[avatar_definition]) ).
thf(f114,plain,
( ( $false
= ( f5 @ $false ) )
| ( $true = sF20 )
| ( $true = sF21 ) ),
inference(binary_proxy_clausification,[status(thm)],[f113]) ).
thf(f631,plain,
( spl31_83
| spl31_26
| spl31_30 ),
inference(avatar_split_clause,[status(thm)],[f117,f359,f341,f627]) ).
thf(f117,plain,
( ( $true = sF21 )
| ( $false = sF20 )
| ( ( f5 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f112]) ).
thf(f112,plain,
( ( ( f5 @ $true )
= sF21 )
| ( $false = sF20 ) ),
inference(cases_simplifying,[status(thm)],[f27]) ).
thf(f630,plain,
( spl31_83
| spl31_22
| spl31_32 ),
inference(avatar_split_clause,[status(thm)],[f116,f368,f323,f627]) ).
thf(f116,plain,
( ( ( f5 @ $true )
= $true )
| ( $false = sF20 )
| ( $false = sF21 ) ),
inference(binary_proxy_clausification,[status(thm)],[f112]) ).
thf(f625,plain,
( spl31_78
| spl31_82
| spl31_75 ),
inference(avatar_split_clause,[status(thm)],[f121,f587,f622,f603]) ).
thf(f587,definition,
( spl31_75
<=> ( sF12 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_75])],[avatar_definition]) ).
thf(f121,plain,
( ( ( f0 @ $false )
= $false )
| ( sF13 = $true )
| ( sF12 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f119]) ).
thf(f119,plain,
( ( ( f0 @ $false )
= sF13 )
| ( sF12 = $true ) ),
inference(cases_simplifying,[status(thm)],[f19]) ).
thf(f620,plain,
( spl31_79
| spl31_75
| spl31_81 ),
inference(avatar_split_clause,[status(thm)],[f120,f617,f587,f608]) ).
thf(f120,plain,
( ( sF12 = $true )
| ( sF13 = $false )
| ( ( f0 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f119]) ).
thf(f615,plain,
( spl31_76
| spl31_79
| spl31_80 ),
inference(avatar_split_clause,[status(thm)],[f123,f612,f608,f592]) ).
thf(f592,definition,
( spl31_76
<=> ( sF12 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_76])],[avatar_definition]) ).
thf(f123,plain,
( ( sF13 = $false )
| ( sF12 = $false )
| ( ( f0 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f118]) ).
thf(f118,plain,
( ( sF12 = $false )
| ( sF13
= ( f0 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f19]) ).
thf(f606,plain,
( spl31_77
| spl31_78
| spl31_76 ),
inference(avatar_split_clause,[status(thm)],[f122,f592,f603,f599]) ).
thf(f122,plain,
( ( sF12 = $false )
| ( ( f0 @ $true )
= $false )
| ( sF13 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f118]) ).
thf(f597,plain,
( spl31_40
| spl31_76
| spl31_53 ),
inference(avatar_split_clause,[status(thm)],[f127,f465,f592,f407]) ).
thf(f407,definition,
( spl31_40
<=> ( sF11 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_40])],[avatar_definition]) ).
thf(f127,plain,
( ( sF12 = $false )
| ( sF11 = $true )
| ( ( f1 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f125]) ).
thf(f125,plain,
( ( sF11 = $true )
| ( sF12
= ( f1 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f18]) ).
thf(f596,plain,
( spl31_75
| spl31_40
| spl31_54 ),
inference(avatar_split_clause,[status(thm)],[f126,f470,f407,f587]) ).
thf(f126,plain,
( ( ( f1 @ $false )
= $false )
| ( sF12 = $true )
| ( sF11 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f125]) ).
thf(f595,plain,
( spl31_76
| spl31_43
| spl31_49 ),
inference(avatar_split_clause,[status(thm)],[f129,f447,f420,f592]) ).
thf(f420,definition,
( spl31_43
<=> ( sF11 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_43])],[avatar_definition]) ).
thf(f129,plain,
( ( sF11 = $false )
| ( ( f1 @ $true )
= $true )
| ( sF12 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f124]) ).
thf(f124,plain,
( ( sF12
= ( f1 @ $true ) )
| ( sF11 = $false ) ),
inference(cases_simplifying,[status(thm)],[f18]) ).
thf(f590,plain,
( spl31_75
| spl31_43
| spl31_50 ),
inference(avatar_split_clause,[status(thm)],[f128,f452,f420,f587]) ).
thf(f128,plain,
( ( sF11 = $false )
| ( sF12 = $true )
| ( ( f1 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f124]) ).
thf(f585,plain,
( spl31_53
| spl31_74
| spl31_47 ),
inference(avatar_split_clause,[status(thm)],[f133,f439,f581,f465]) ).
thf(f439,definition,
( spl31_47
<=> ( sF28 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_47])],[avatar_definition]) ).
thf(f133,plain,
( ( sF27 = $true )
| ( sF28 = $false )
| ( ( f1 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f131]) ).
thf(f131,plain,
( ( sF27 = $true )
| ( sF28
= ( f1 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f34]) ).
thf(f584,plain,
( spl31_74
| spl31_52
| spl31_54 ),
inference(avatar_split_clause,[status(thm)],[f132,f470,f461,f581]) ).
thf(f461,definition,
( spl31_52
<=> ( sF28 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_52])],[avatar_definition]) ).
thf(f132,plain,
( ( ( f1 @ $false )
= $false )
| ( sF27 = $true )
| ( sF28 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f131]) ).
thf(f579,plain,
( spl31_49
| spl31_73
| spl31_47 ),
inference(avatar_split_clause,[status(thm)],[f135,f439,f575,f447]) ).
thf(f135,plain,
( ( sF27 = $false )
| ( sF28 = $false )
| ( ( f1 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f130]) ).
thf(f130,plain,
( ( sF28
= ( f1 @ $true ) )
| ( sF27 = $false ) ),
inference(cases_simplifying,[status(thm)],[f34]) ).
thf(f578,plain,
( spl31_50
| spl31_52
| spl31_73 ),
inference(avatar_split_clause,[status(thm)],[f134,f575,f461,f452]) ).
thf(f134,plain,
( ( ( f1 @ $true )
= $false )
| ( sF28 = $true )
| ( sF27 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f130]) ).
thf(f573,plain,
( spl31_58
| spl31_37
| spl31_7 ),
inference(avatar_split_clause,[status(thm)],[f139,f253,f391,f491]) ).
thf(f491,definition,
( spl31_58
<=> ( sF17 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_58])],[avatar_definition]) ).
thf(f391,definition,
( spl31_37
<=> ( sF16 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_37])],[avatar_definition]) ).
thf(f253,definition,
( spl31_7
<=> ( ( f7 @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl31_7])],[avatar_definition]) ).
thf(f139,plain,
( ( ( f7 @ $false )
= $true )
| ( sF16 = $true )
| ( sF17 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f137]) ).
thf(f137,plain,
( ( sF16 = $true )
| ( sF17
= ( f7 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f23]) ).
thf(f572,plain,
( spl31_37
| spl31_62
| spl31_8 ),
inference(avatar_split_clause,[status(thm)],[f138,f258,f509,f391]) ).
thf(f509,definition,
( spl31_62
<=> ( sF17 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_62])],[avatar_definition]) ).
thf(f258,definition,
( spl31_8
<=> ( ( f7 @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl31_8])],[avatar_definition]) ).
thf(f138,plain,
( ( ( f7 @ $false )
= $false )
| ( sF17 = $true )
| ( sF16 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f137]) ).
thf(f571,plain,
( spl31_3
| spl31_58
| spl31_38 ),
inference(avatar_split_clause,[status(thm)],[f141,f396,f491,f235]) ).
thf(f235,definition,
( spl31_3
<=> ( $true
= ( f7 @ $true ) ) ),
introduced(definition,[new_symbols(naming,[spl31_3])],[avatar_definition]) ).
thf(f396,definition,
( spl31_38
<=> ( sF16 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_38])],[avatar_definition]) ).
thf(f141,plain,
( ( $true
= ( f7 @ $true ) )
| ( sF16 = $false )
| ( sF17 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f136]) ).
thf(f136,plain,
( ( sF17
= ( f7 @ $true ) )
| ( sF16 = $false ) ),
inference(cases_simplifying,[status(thm)],[f23]) ).
thf(f570,plain,
( spl31_38
| spl31_62
| spl31_4 ),
inference(avatar_split_clause,[status(thm)],[f140,f240,f509,f396]) ).
thf(f240,definition,
( spl31_4
<=> ( $false
= ( f7 @ $true ) ) ),
introduced(definition,[new_symbols(naming,[spl31_4])],[avatar_definition]) ).
thf(f140,plain,
( ( $false
= ( f7 @ $true ) )
| ( sF16 = $false )
| ( sF17 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f136]) ).
thf(f569,plain,
( spl31_72
| spl31_44
| spl31_45 ),
inference(avatar_split_clause,[status(thm)],[f145,f429,f425,f565]) ).
thf(f425,definition,
( spl31_44
<=> ( sF10 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_44])],[avatar_definition]) ).
thf(f145,plain,
( ( ( f2 @ $false )
= $false )
| ( $true = sF9 )
| ( sF10 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f143]) ).
thf(f143,plain,
( ( $true = sF9 )
| ( ( f2 @ $false )
= sF10 ) ),
inference(cases_simplifying,[status(thm)],[f16]) ).
thf(f568,plain,
( spl31_46
| spl31_72
| spl31_41 ),
inference(avatar_split_clause,[status(thm)],[f144,f411,f565,f434]) ).
thf(f411,definition,
( spl31_41
<=> ( sF10 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_41])],[avatar_definition]) ).
thf(f144,plain,
( ( $true = sF9 )
| ( ( f2 @ $false )
= $true )
| ( sF10 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f143]) ).
thf(f563,plain,
( spl31_42
| spl31_41
| spl31_71 ),
inference(avatar_split_clause,[status(thm)],[f147,f559,f411,f416]) ).
thf(f147,plain,
( ( sF10 = $false )
| ( $false = sF9 )
| ( ( f2 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f142]) ).
thf(f142,plain,
( ( sF10
= ( f2 @ $true ) )
| ( $false = sF9 ) ),
inference(cases_simplifying,[status(thm)],[f16]) ).
thf(f562,plain,
( spl31_44
| spl31_39
| spl31_71 ),
inference(avatar_split_clause,[status(thm)],[f146,f559,f403,f425]) ).
thf(f146,plain,
( ( sF10 = $true )
| ( ( f2 @ $true )
= $false )
| ( $false = sF9 ) ),
inference(binary_proxy_clausification,[status(thm)],[f142]) ).
thf(f557,plain,
( spl31_70
| spl31_5
| spl31_64 ),
inference(avatar_split_clause,[status(thm)],[f151,f518,f244,f552]) ).
thf(f244,definition,
( spl31_5
<=> ( $true = sF0 ) ),
introduced(definition,[new_symbols(naming,[spl31_5])],[avatar_definition]) ).
thf(f151,plain,
( ( $true = sF0 )
| ( sF1 = $false )
| ( ( f6 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f149]) ).
thf(f149,plain,
( ( sF1
= ( f6 @ $false ) )
| ( $true = sF0 ) ),
inference(cases_simplifying,[status(thm)],[f7]) ).
thf(f556,plain,
( spl31_69
| spl31_63
| spl31_5 ),
inference(avatar_split_clause,[status(thm)],[f150,f244,f513,f547]) ).
thf(f150,plain,
( ( sF1 = $true )
| ( ( f6 @ $false )
= $false )
| ( $true = sF0 ) ),
inference(binary_proxy_clausification,[status(thm)],[f149]) ).
thf(f555,plain,
( spl31_61
| spl31_70
| spl31_2 ),
inference(avatar_split_clause,[status(thm)],[f153,f231,f552,f504]) ).
thf(f231,definition,
( spl31_2
<=> ( $false = sF0 ) ),
introduced(definition,[new_symbols(naming,[spl31_2])],[avatar_definition]) ).
thf(f153,plain,
( ( ( f6 @ $true )
= $true )
| ( sF1 = $false )
| ( $false = sF0 ) ),
inference(binary_proxy_clausification,[status(thm)],[f148]) ).
thf(f148,plain,
( ( $false = sF0 )
| ( sF1
= ( f6 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f7]) ).
thf(f550,plain,
( spl31_57
| spl31_69
| spl31_2 ),
inference(avatar_split_clause,[status(thm)],[f152,f231,f547,f487]) ).
thf(f152,plain,
( ( $false = sF0 )
| ( sF1 = $true )
| ( ( f6 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f148]) ).
thf(f545,plain,
( spl31_29
| spl31_64
| spl31_68 ),
inference(avatar_split_clause,[status(thm)],[f157,f541,f518,f355]) ).
thf(f355,definition,
( spl31_29
<=> ( sF3 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_29])],[avatar_definition]) ).
thf(f157,plain,
( ( sF2 = $true )
| ( ( f6 @ $false )
= $true )
| ( sF3 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f155]) ).
thf(f155,plain,
( ( sF2 = $true )
| ( sF3
= ( f6 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f9]) ).
thf(f544,plain,
( spl31_63
| spl31_35
| spl31_68 ),
inference(avatar_split_clause,[status(thm)],[f156,f541,f381,f513]) ).
thf(f381,definition,
( spl31_35
<=> ( sF3 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_35])],[avatar_definition]) ).
thf(f156,plain,
( ( sF2 = $true )
| ( sF3 = $true )
| ( ( f6 @ $false )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f155]) ).
thf(f539,plain,
( spl31_29
| spl31_67
| spl31_61 ),
inference(avatar_split_clause,[status(thm)],[f159,f504,f535,f355]) ).
thf(f159,plain,
( ( sF2 = $false )
| ( ( f6 @ $true )
= $true )
| ( sF3 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f154]) ).
thf(f154,plain,
( ( sF2 = $false )
| ( sF3
= ( f6 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f9]) ).
thf(f538,plain,
( spl31_35
| spl31_67
| spl31_57 ),
inference(avatar_split_clause,[status(thm)],[f158,f487,f535,f381]) ).
thf(f158,plain,
( ( sF2 = $false )
| ( sF3 = $true )
| ( ( f6 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f154]) ).
thf(f533,plain,
( spl31_28
| spl31_17
| spl31_66 ),
inference(avatar_split_clause,[status(thm)],[f163,f529,f299,f350]) ).
thf(f299,definition,
( spl31_17
<=> ( sF7 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_17])],[avatar_definition]) ).
thf(f163,plain,
( ( $true
= ( f4 @ $false ) )
| ( sF6 = $true )
| ( sF7 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f161]) ).
thf(f161,plain,
( ( sF6 = $true )
| ( sF7
= ( f4 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f13]) ).
thf(f532,plain,
( spl31_20
| spl31_27
| spl31_66 ),
inference(avatar_split_clause,[status(thm)],[f162,f529,f345,f313]) ).
thf(f313,definition,
( spl31_20
<=> ( sF7 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_20])],[avatar_definition]) ).
thf(f162,plain,
( ( sF7 = $true )
| ( $false
= ( f4 @ $false ) )
| ( sF6 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f161]) ).
thf(f527,plain,
( spl31_23
| spl31_65
| spl31_17 ),
inference(avatar_split_clause,[status(thm)],[f165,f299,f523,f327]) ).
thf(f165,plain,
( ( ( f4 @ $true )
= $true )
| ( sF7 = $false )
| ( sF6 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f160]) ).
thf(f160,plain,
( ( sF7
= ( f4 @ $true ) )
| ( sF6 = $false ) ),
inference(cases_simplifying,[status(thm)],[f13]) ).
thf(f526,plain,
( spl31_25
| spl31_65
| spl31_20 ),
inference(avatar_split_clause,[status(thm)],[f164,f313,f523,f336]) ).
thf(f164,plain,
( ( sF7 = $true )
| ( ( f4 @ $true )
= $false )
| ( sF6 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f160]) ).
thf(f521,plain,
( spl31_62
| spl31_64
| spl31_60 ),
inference(avatar_split_clause,[status(thm)],[f169,f500,f518,f509]) ).
thf(f169,plain,
( ( sF18 = $false )
| ( ( f6 @ $false )
= $true )
| ( sF17 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f167]) ).
thf(f167,plain,
( ( sF17 = $true )
| ( sF18
= ( f6 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f24]) ).
thf(f516,plain,
( spl31_62
| spl31_59
| spl31_63 ),
inference(avatar_split_clause,[status(thm)],[f168,f513,f495,f509]) ).
thf(f168,plain,
( ( ( f6 @ $false )
= $false )
| ( sF18 = $true )
| ( sF17 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f167]) ).
thf(f507,plain,
( spl31_58
| spl31_60
| spl31_61 ),
inference(avatar_split_clause,[status(thm)],[f171,f504,f500,f491]) ).
thf(f171,plain,
( ( sF17 = $false )
| ( sF18 = $false )
| ( ( f6 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f166]) ).
thf(f166,plain,
( ( sF17 = $false )
| ( sF18
= ( f6 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f24]) ).
thf(f498,plain,
( spl31_57
| spl31_58
| spl31_59 ),
inference(avatar_split_clause,[status(thm)],[f170,f495,f491,f487]) ).
thf(f170,plain,
( ( sF17 = $false )
| ( sF18 = $true )
| ( ( f6 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f166]) ).
thf(f485,plain,
( spl31_9
| spl31_16
| spl31_56 ),
inference(avatar_split_clause,[status(thm)],[f175,f481,f294,f263]) ).
thf(f263,definition,
( spl31_9
<=> ( sF24 = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_9])],[avatar_definition]) ).
thf(f175,plain,
( ( sF23 = $true )
| ( ( f3 @ $false )
= $true )
| ( sF24 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f173]) ).
thf(f173,plain,
( ( sF24
= ( f3 @ $false ) )
| ( sF23 = $true ) ),
inference(cases_simplifying,[status(thm)],[f30]) ).
thf(f484,plain,
( spl31_15
| spl31_56
| spl31_14 ),
inference(avatar_split_clause,[status(thm)],[f174,f285,f481,f289]) ).
thf(f289,definition,
( spl31_15
<=> ( sF24 = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_15])],[avatar_definition]) ).
thf(f174,plain,
( ( sF23 = $true )
| ( ( f3 @ $false )
= $false )
| ( sF24 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f173]) ).
thf(f479,plain,
( spl31_55
| spl31_13
| spl31_15 ),
inference(avatar_split_clause,[status(thm)],[f177,f289,f280,f475]) ).
thf(f177,plain,
( ( ( f3 @ $true )
= $false )
| ( sF24 = $true )
| ( sF23 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f172]) ).
thf(f172,plain,
( ( ( f3 @ $true )
= sF24 )
| ( sF23 = $false ) ),
inference(cases_simplifying,[status(thm)],[f30]) ).
thf(f478,plain,
( spl31_10
| spl31_55
| spl31_9 ),
inference(avatar_split_clause,[status(thm)],[f176,f263,f475,f267]) ).
thf(f176,plain,
( ( sF24 = $false )
| ( sF23 = $false )
| ( ( f3 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f172]) ).
thf(f473,plain,
( spl31_51
| spl31_54
| spl31_52 ),
inference(avatar_split_clause,[status(thm)],[f181,f461,f470,f456]) ).
thf(f181,plain,
( ( ( f1 @ $false )
= $false )
| ( $true = sF29 )
| ( sF28 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f179]) ).
thf(f179,plain,
( ( sF28 = $true )
| ( ( f1 @ $false )
= sF29 ) ),
inference(cases_simplifying,[status(thm)],[f35]) ).
thf(f468,plain,
( spl31_52
| spl31_48
| spl31_53 ),
inference(avatar_split_clause,[status(thm)],[f180,f465,f443,f461]) ).
thf(f180,plain,
( ( sF28 = $true )
| ( $false = sF29 )
| ( ( f1 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f179]) ).
thf(f459,plain,
( spl31_50
| spl31_47
| spl31_51 ),
inference(avatar_split_clause,[status(thm)],[f183,f456,f439,f452]) ).
thf(f183,plain,
( ( sF28 = $false )
| ( ( f1 @ $true )
= $false )
| ( $true = sF29 ) ),
inference(binary_proxy_clausification,[status(thm)],[f178]) ).
thf(f178,plain,
( ( sF28 = $false )
| ( ( f1 @ $true )
= sF29 ) ),
inference(cases_simplifying,[status(thm)],[f35]) ).
thf(f450,plain,
( spl31_47
| spl31_48
| spl31_49 ),
inference(avatar_split_clause,[status(thm)],[f182,f447,f443,f439]) ).
thf(f182,plain,
( ( ( f1 @ $true )
= $true )
| ( $false = sF29 )
| ( sF28 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f178]) ).
thf(f437,plain,
( spl31_46
| spl31_44
| spl31_43 ),
inference(avatar_split_clause,[status(thm)],[f187,f420,f425,f434]) ).
thf(f187,plain,
( ( ( f2 @ $false )
= $true )
| ( sF11 = $false )
| ( sF10 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f185]) ).
thf(f185,plain,
( ( sF10 = $true )
| ( sF11
= ( f2 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f17]) ).
thf(f432,plain,
( spl31_44
| spl31_40
| spl31_45 ),
inference(avatar_split_clause,[status(thm)],[f186,f429,f407,f425]) ).
thf(f186,plain,
( ( sF10 = $true )
| ( ( f2 @ $false )
= $false )
| ( sF11 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f185]) ).
thf(f423,plain,
( spl31_42
| spl31_43
| spl31_41 ),
inference(avatar_split_clause,[status(thm)],[f189,f411,f420,f416]) ).
thf(f189,plain,
( ( sF10 = $false )
| ( ( f2 @ $true )
= $true )
| ( sF11 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f184]) ).
thf(f184,plain,
( ( sF11
= ( f2 @ $true ) )
| ( sF10 = $false ) ),
inference(cases_simplifying,[status(thm)],[f17]) ).
thf(f414,plain,
( spl31_39
| spl31_40
| spl31_41 ),
inference(avatar_split_clause,[status(thm)],[f188,f411,f407,f403]) ).
thf(f188,plain,
( ( sF10 = $false )
| ( sF11 = $true )
| ( ( f2 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f184]) ).
thf(f401,plain,
( spl31_5
| spl31_38
| spl31_7 ),
inference(avatar_split_clause,[status(thm)],[f193,f253,f396,f244]) ).
thf(f193,plain,
( ( sF16 = $false )
| ( $true = sF0 )
| ( ( f7 @ $false )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f191]) ).
thf(f191,plain,
( ( sF16
= ( f7 @ $false ) )
| ( $true = sF0 ) ),
inference(cases_simplifying,[status(thm)],[f22]) ).
thf(f400,plain,
( spl31_5
| spl31_37
| spl31_8 ),
inference(avatar_split_clause,[status(thm)],[f192,f258,f391,f244]) ).
thf(f192,plain,
( ( ( f7 @ $false )
= $false )
| ( $true = sF0 )
| ( sF16 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f191]) ).
thf(f399,plain,
( spl31_2
| spl31_38
| spl31_3 ),
inference(avatar_split_clause,[status(thm)],[f195,f235,f396,f231]) ).
thf(f195,plain,
( ( sF16 = $false )
| ( $false = sF0 )
| ( $true
= ( f7 @ $true ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f190]) ).
thf(f190,plain,
( ( sF16
= ( f7 @ $true ) )
| ( $false = sF0 ) ),
inference(cases_simplifying,[status(thm)],[f22]) ).
thf(f394,plain,
( spl31_2
| spl31_4
| spl31_37 ),
inference(avatar_split_clause,[status(thm)],[f194,f391,f240,f231]) ).
thf(f194,plain,
( ( $false = sF0 )
| ( sF16 = $true )
| ( $false
= ( f7 @ $true ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f190]) ).
thf(f389,plain,
( spl31_35
| spl31_36
| spl31_33 ),
inference(avatar_split_clause,[status(thm)],[f199,f372,f386,f381]) ).
thf(f199,plain,
( ( sF4 = $false )
| ( sF3 = $true )
| ( $true
= ( f5 @ $false ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f197]) ).
thf(f197,plain,
( ( sF3 = $true )
| ( sF4
= ( f5 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f10]) ).
thf(f384,plain,
( spl31_34
| spl31_31
| spl31_35 ),
inference(avatar_split_clause,[status(thm)],[f198,f381,f363,f377]) ).
thf(f198,plain,
( ( $false
= ( f5 @ $false ) )
| ( sF3 = $true )
| ( sF4 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f197]) ).
thf(f375,plain,
( spl31_32
| spl31_29
| spl31_33 ),
inference(avatar_split_clause,[status(thm)],[f201,f372,f355,f368]) ).
thf(f201,plain,
( ( sF3 = $false )
| ( sF4 = $false )
| ( ( f5 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f196]) ).
thf(f196,plain,
( ( sF3 = $false )
| ( sF4
= ( f5 @ $true ) ) ),
inference(cases_simplifying,[status(thm)],[f10]) ).
thf(f366,plain,
( spl31_29
| spl31_30
| spl31_31 ),
inference(avatar_split_clause,[status(thm)],[f200,f363,f359,f355]) ).
thf(f200,plain,
( ( sF3 = $false )
| ( ( f5 @ $true )
= $false )
| ( sF4 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f196]) ).
thf(f353,plain,
( spl31_28
| spl31_26
| spl31_21 ),
inference(avatar_split_clause,[status(thm)],[f205,f319,f341,f350]) ).
thf(f205,plain,
( ( $false = sF22 )
| ( $true
= ( f4 @ $false ) )
| ( $true = sF21 ) ),
inference(binary_proxy_clausification,[status(thm)],[f203]) ).
thf(f203,plain,
( ( $true = sF21 )
| ( sF22
= ( f4 @ $false ) ) ),
inference(cases_simplifying,[status(thm)],[f28]) ).
thf(f348,plain,
( spl31_24
| spl31_26
| spl31_27 ),
inference(avatar_split_clause,[status(thm)],[f204,f345,f341,f332]) ).
thf(f204,plain,
( ( $false
= ( f4 @ $false ) )
| ( $true = sF22 )
| ( $true = sF21 ) ),
inference(binary_proxy_clausification,[status(thm)],[f203]) ).
thf(f339,plain,
( spl31_22
| spl31_24
| spl31_25 ),
inference(avatar_split_clause,[status(thm)],[f207,f336,f332,f323]) ).
thf(f207,plain,
( ( $false = sF21 )
| ( ( f4 @ $true )
= $false )
| ( $true = sF22 ) ),
inference(binary_proxy_clausification,[status(thm)],[f202]) ).
thf(f202,plain,
( ( $false = sF21 )
| ( ( f4 @ $true )
= sF22 ) ),
inference(cases_simplifying,[status(thm)],[f28]) ).
thf(f330,plain,
( spl31_21
| spl31_22
| spl31_23 ),
inference(avatar_split_clause,[status(thm)],[f206,f327,f323,f319]) ).
thf(f206,plain,
( ( $false = sF22 )
| ( $false = sF21 )
| ( ( f4 @ $true )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f202]) ).
thf(f317,plain,
( spl31_16
| spl31_18
| spl31_20 ),
inference(avatar_split_clause,[status(thm)],[f211,f313,f303,f294]) ).
thf(f211,plain,
( ( ( f3 @ $false )
= $true )
| ( sF7 = $true )
| ( sF8 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f209]) ).
thf(f209,plain,
( ( sF8
= ( f3 @ $false ) )
| ( sF7 = $true ) ),
inference(cases_simplifying,[status(thm)],[f14]) ).
thf(f316,plain,
( spl31_14
| spl31_19
| spl31_20 ),
inference(avatar_split_clause,[status(thm)],[f210,f313,f308,f285]) ).
thf(f210,plain,
( ( sF8 = $true )
| ( ( f3 @ $false )
= $false )
| ( sF7 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f209]) ).
thf(f311,plain,
( spl31_19
| spl31_17
| spl31_13 ),
inference(avatar_split_clause,[status(thm)],[f213,f280,f299,f308]) ).
thf(f213,plain,
( ( sF7 = $false )
| ( ( f3 @ $true )
= $false )
| ( sF8 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f208]) ).
thf(f208,plain,
( ( ( f3 @ $true )
= sF8 )
| ( sF7 = $false ) ),
inference(cases_simplifying,[status(thm)],[f14]) ).
thf(f306,plain,
( spl31_10
| spl31_17
| spl31_18 ),
inference(avatar_split_clause,[status(thm)],[f212,f303,f299,f267]) ).
thf(f212,plain,
( ( sF8 = $false )
| ( ( f3 @ $true )
= $true )
| ( sF7 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f208]) ).
thf(f297,plain,
( spl31_11
| spl31_15
| spl31_16 ),
inference(avatar_split_clause,[status(thm)],[f217,f294,f289,f271]) ).
thf(f217,plain,
( ( ( f3 @ $false )
= $true )
| ( sF25 = $false )
| ( sF24 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f215]) ).
thf(f215,plain,
( ( sF25
= ( f3 @ $false ) )
| ( sF24 = $true ) ),
inference(cases_simplifying,[status(thm)],[f31]) ).
thf(f292,plain,
( spl31_14
| spl31_12
| spl31_15 ),
inference(avatar_split_clause,[status(thm)],[f216,f289,f276,f285]) ).
thf(f216,plain,
( ( ( f3 @ $false )
= $false )
| ( sF25 = $true )
| ( sF24 = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f215]) ).
thf(f283,plain,
( spl31_9
| spl31_12
| spl31_13 ),
inference(avatar_split_clause,[status(thm)],[f219,f280,f276,f263]) ).
thf(f219,plain,
( ( sF24 = $false )
| ( sF25 = $true )
| ( ( f3 @ $true )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f214]) ).
thf(f214,plain,
( ( ( f3 @ $true )
= sF25 )
| ( sF24 = $false ) ),
inference(cases_simplifying,[status(thm)],[f31]) ).
thf(f274,plain,
( spl31_9
| spl31_10
| spl31_11 ),
inference(avatar_split_clause,[status(thm)],[f218,f271,f267,f263]) ).
thf(f218,plain,
( ( sF24 = $false )
| ( ( f3 @ $true )
= $true )
| ( sF25 = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f214]) ).
thf(f261,plain,
( spl31_6
| spl31_8
| spl31_5 ),
inference(avatar_split_clause,[status(thm)],[f223,f244,f258,f249]) ).
thf(f249,definition,
( spl31_6
<=> ( x = $true ) ),
introduced(definition,[new_symbols(naming,[spl31_6])],[avatar_definition]) ).
thf(f223,plain,
( ( ( f7 @ $false )
= $false )
| ( x = $true )
| ( $true = sF0 ) ),
inference(binary_proxy_clausification,[status(thm)],[f221]) ).
thf(f221,plain,
( ( ( f7 @ $false )
= sF0 )
| ( x = $true ) ),
inference(cases_simplifying,[status(thm)],[f6]) ).
thf(f256,plain,
( spl31_6
| spl31_2
| spl31_7 ),
inference(avatar_split_clause,[status(thm)],[f222,f253,f231,f249]) ).
thf(f222,plain,
( ( ( f7 @ $false )
= $true )
| ( $false = sF0 )
| ( x = $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f221]) ).
thf(f247,plain,
( spl31_4
| spl31_5
| spl31_1 ),
inference(avatar_split_clause,[status(thm)],[f225,f227,f244,f240]) ).
thf(f227,definition,
( spl31_1
<=> ( x = $false ) ),
introduced(definition,[new_symbols(naming,[spl31_1])],[avatar_definition]) ).
thf(f225,plain,
( ( $true = sF0 )
| ( $false
= ( f7 @ $true ) )
| ( x = $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f220]) ).
thf(f220,plain,
( ( x = $false )
| ( ( f7 @ $true )
= sF0 ) ),
inference(cases_simplifying,[status(thm)],[f6]) ).
thf(f238,plain,
( spl31_1
| spl31_2
| spl31_3 ),
inference(avatar_split_clause,[status(thm)],[f224,f235,f231,f227]) ).
thf(f224,plain,
( ( x = $false )
| ( $true
= ( f7 @ $true ) )
| ( $false = sF0 ) ),
inference(binary_proxy_clausification,[status(thm)],[f220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYO500^1.008 : TPTP v9.2.1. Released v4.1.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n015.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Feb 24 14:33:01 EST 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.45 ---- Original DTF file ---
% 0.18/0.45 thf(spec,logic,$$dhol).
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 % File : SYO500^1.008 : TPTP v9.2.1. Released v4.1.0.
% 0.18/0.45 % Domain : Syntactic
% 0.18/0.45 % Problem : Eight function variant of the Kaminski equation
% 0.18/0.45 % Version : Especial.
% 0.18/0.45 % English :
% 0.18/0.45
% 0.18/0.45 % Refs : [Bro09] Brown E. (2009), Email to Geoff Sutcliffe
% 0.18/0.45 % : [Hoe09] Hoeschele (2009), Towards a Semi-Automatic Higher-Orde
% 0.18/0.45 % Source : [Bro09]
% 0.18/0.45 % Names : basic16 [Bro09]
% 0.18/0.45
% 0.18/0.45 % Status : Theorem
% 0.18/0.45 % Rating : 0.33 v9.1.0, 0.50 v9.0.0, 0.40 v8.2.0, 0.31 v8.1.0, 0.36 v7.5.0, 0.57 v7.4.0, 0.56 v7.2.0, 0.50 v7.0.0, 0.43 v6.4.0, 0.50 v6.3.0, 0.60 v6.2.0, 0.57 v5.5.0, 0.50 v5.4.0, 0.80 v4.1.0
% 0.18/0.45 % Syntax : Number of formulae : 10 ( 1 unt; 9 typ; 0 def)
% 0.18/0.45 % Number of atoms : 35 ( 1 equ; 0 cnn)
% 0.18/0.45 % Maximal formula atoms : 1 ( 35 avg)
% 0.18/0.45 % Number of connectives : 32 ( 0 ~; 0 |; 0 &; 32 @)
% 0.18/0.45 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.18/0.45 % Maximal formula depth : 1 ( 1 avg)
% 0.18/0.45 % Number of types : 1 ( 0 usr)
% 0.18/0.45 % Number of type conns : 8 ( 8 >; 0 *; 0 +; 0 <<)
% 0.18/0.45 % Number of symbols : 10 ( 9 usr; 1 con; 0-2 aty)
% 0.18/0.45 % Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% 0.18/0.45 % SPC : TH0_THM_EQU_NAR
% 0.18/0.45
% 0.18/0.45 % Comments :
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 thf(x,type,
% 0.18/0.45 x: $o ).
% 0.18/0.45
% 0.18/0.45 thf(f0,type,
% 0.18/0.45 f0: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f1,type,
% 0.18/0.45 f1: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f2,type,
% 0.18/0.45 f2: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f3,type,
% 0.18/0.45 f3: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f4,type,
% 0.18/0.45 f4: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f5,type,
% 0.18/0.45 f5: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f6,type,
% 0.18/0.45 f6: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(f7,type,
% 0.18/0.45 f7: $o > $o ).
% 0.18/0.45
% 0.18/0.45 thf(kaminski8,conjecture,
% 0.18/0.45 ( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
% 0.18/0.45 = ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
% 0.18/0.45
% 0.18/0.45 %------------------------------------------------------------------------------
% 0.18/0.45 ------------------------
% 1.48/1.24 ---- Embedded in THF ---
% 1.48/1.24 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.48/1.24 %%% Generated on Tue Feb 24 14:33:02 EST 2026
% 1.48/1.24 %%% using '$$dhol' embedding, version 1.3.0.
% 1.48/1.24 %%% Logic specification used:
% 1.48/1.24 %%% thf(spec, logic, $$dhol).
% 1.48/1.24
% 1.48/1.24 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.Tk9QRBkYJG/DTF2DTF18236.p
% See solution above
% 1.48/1.24 ------------------------
% 1.48/1.25 ---- Cleaned THF ---
% 1.48/1.26 thf(x,type,
% 1.48/1.26 x: $o ).
% 1.48/1.26
% 1.48/1.26 thf(f0,type,
% 1.48/1.26 f0: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f1,type,
% 1.48/1.26 f1: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f2,type,
% 1.48/1.26 f2: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f3,type,
% 1.48/1.26 f3: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f4,type,
% 1.48/1.26 f4: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f5,type,
% 1.48/1.26 f5: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f6,type,
% 1.48/1.26 f6: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(f7,type,
% 1.48/1.26 f7: $o > $o ).
% 1.48/1.26
% 1.48/1.26 thf(kaminski8,conjecture,
% 1.48/1.26 ( ( f0 @ ( f0 @ ( f0 @ ( f1 @ ( f2 @ ( f2 @ ( f2 @ ( f3 @ ( f4 @ ( f4 @ ( f4 @ ( f5 @ ( f6 @ ( f6 @ ( f6 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
% 1.48/1.26 = ( f0 @ ( f1 @ ( f1 @ ( f1 @ ( f2 @ ( f3 @ ( f3 @ ( f3 @ ( f4 @ ( f5 @ ( f5 @ ( f5 @ ( f6 @ ( f7 @ ( f7 @ ( f7 @ x ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
% 1.48/1.26 ------------------------
% 1.48/1.27 % (18569)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/275Mi)
% 1.48/1.27 % (18567)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/2Mi)
% 1.48/1.27 % (18569)Refutation not found, incomplete strategy
% 1.48/1.27 % (18569)------------------------------
% 1.48/1.27 % (18569)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.27 % (18569)Termination reason: Refutation not found, incomplete strategy
% 1.48/1.27
% 1.48/1.27
% 1.48/1.27 % (18569)Memory used [KB]: 5500
% 1.48/1.27 % (18569)Time elapsed: 0.002 s
% 1.48/1.27 % (18569)Instructions burned: 2 (million)
% 1.48/1.27 % (18569)------------------------------
% 1.48/1.27 % (18569)------------------------------
% 1.48/1.27 % (18567)Instruction limit reached!
% 1.48/1.27 % (18567)------------------------------
% 1.48/1.27 % (18567)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.27 % (18567)Termination reason: Unknown
% 1.48/1.27 % (18567)Termination phase: Saturation
% 1.48/1.27
% 1.48/1.27 % (18567)Memory used [KB]: 5500
% 1.48/1.27 % (18567)Time elapsed: 0.002 s
% 1.48/1.27 % (18567)Instructions burned: 2 (million)
% 1.48/1.27 % (18567)------------------------------
% 1.48/1.27 % (18567)------------------------------
% 1.48/1.28 % (18565)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/4Mi)
% 1.48/1.28 % (18564)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/183Mi)
% 1.48/1.28 % (18566)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/27Mi)
% 1.48/1.28 % (18568)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/2Mi)
% 1.48/1.28 % (18570)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/18Mi)
% 1.48/1.28 % (18568)Instruction limit reached!
% 1.48/1.28 % (18568)------------------------------
% 1.48/1.28 % (18568)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.28 % (18568)Termination reason: Unknown
% 1.48/1.28 % (18568)Termination phase: Saturation
% 1.48/1.28
% 1.48/1.28 % (18568)Memory used [KB]: 895
% 1.48/1.28 % (18568)Time elapsed: 0.003 s
% 1.48/1.28 % (18568)Instructions burned: 2 (million)
% 1.48/1.28 % (18568)------------------------------
% 1.48/1.28 % (18568)------------------------------
% 1.48/1.28 % (18565)Instruction limit reached!
% 1.48/1.28 % (18565)------------------------------
% 1.48/1.28 % (18565)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.28 % (18565)Termination reason: Unknown
% 1.48/1.28 % (18565)Termination phase: Saturation
% 1.48/1.28
% 1.48/1.28 % (18565)Memory used [KB]: 5500
% 1.48/1.28 % (18565)Time elapsed: 0.005 s
% 1.48/1.28 % (18565)Instructions burned: 5 (million)
% 1.48/1.28 % (18565)------------------------------
% 1.48/1.28 % (18565)------------------------------
% 1.48/1.28 % (18566)Refutation not found, incomplete strategy
% 1.48/1.28 % (18566)------------------------------
% 1.48/1.28 % (18566)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.28 % (18566)Termination reason: Refutation not found, incomplete strategy
% 1.48/1.28
% 1.48/1.28
% 1.48/1.28 % (18566)Memory used [KB]: 5500
% 1.48/1.28 % (18566)Time elapsed: 0.005 s
% 1.48/1.28 % (18566)Instructions burned: 4 (million)
% 1.48/1.28 % (18566)------------------------------
% 1.48/1.28 % (18566)------------------------------
% 1.48/1.28 % (18572)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/37Mi)
% 1.48/1.28 % (18571)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/3Mi)
% 1.48/1.28 % (18571)Refutation not found, incomplete strategy
% 1.48/1.28 % (18571)------------------------------
% 1.48/1.28 % (18571)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.28 % (18571)Termination reason: Refutation not found, incomplete strategy
% 1.48/1.28
% 1.48/1.28
% 1.48/1.28 % (18571)Memory used [KB]: 5500
% 1.48/1.28 % (18571)Time elapsed: 0.002 s
% 1.48/1.28 % (18571)Instructions burned: 1 (million)
% 1.48/1.28 % (18571)------------------------------
% 1.48/1.28 % (18571)------------------------------
% 1.48/1.29 % (18570)Instruction limit reached!
% 1.48/1.29 % (18570)------------------------------
% 1.48/1.29 % (18570)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.29 % (18570)Termination reason: Unknown
% 1.48/1.29 % (18570)Termination phase: Saturation
% 1.48/1.29
% 1.48/1.29 % (18570)Memory used [KB]: 5628
% 1.48/1.29 % (18570)Time elapsed: 0.013 s
% 1.48/1.29 % (18570)Instructions burned: 19 (million)
% 1.48/1.29 % (18570)------------------------------
% 1.48/1.29 % (18570)------------------------------
% 1.48/1.29 % (18572)Instruction limit reached!
% 1.48/1.29 % (18572)------------------------------
% 1.48/1.29 % (18572)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.29 % (18572)Termination reason: Unknown
% 1.48/1.29 % (18572)Termination phase: Saturation
% 1.48/1.29
% 1.48/1.29 % (18572)Memory used [KB]: 5628
% 1.48/1.29 % (18572)Time elapsed: 0.012 s
% 1.48/1.29 % (18572)Instructions burned: 37 (million)
% 1.48/1.29 % (18572)------------------------------
% 1.48/1.29 % (18572)------------------------------
% 1.48/1.29 % (18576)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/7Mi)
% 1.48/1.29 % (18576)Instruction limit reached!
% 1.48/1.29 % (18576)------------------------------
% 1.48/1.29 % (18576)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.48/1.29 % (18576)Termination reason: Unknown
% 1.48/1.29 % (18576)Termination phase: Saturation
% 1.48/1.29
% 1.48/1.29 % (18576)Memory used [KB]: 1023
% 1.48/1.29 % (18576)Time elapsed: 0.004 s
% 1.48/1.29 % (18576)Instructions burned: 7 (million)
% 1.48/1.29 % (18576)------------------------------
% 1.48/1.29 % (18576)------------------------------
% 1.48/1.30 % (18573)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/15Mi)
% 1.58/1.30 % (18574)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/3Mi)
% 1.58/1.30 % (18575)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/1041Mi)
% 1.58/1.30 % (18574)Refutation not found, incomplete strategy
% 1.58/1.30 % (18574)------------------------------
% 1.58/1.30 % (18574)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.30 % (18574)Termination reason: Refutation not found, incomplete strategy
% 1.58/1.30
% 1.58/1.30
% 1.58/1.30 % (18574)Memory used [KB]: 5500
% 1.58/1.30 % (18574)Time elapsed: 0.003 s
% 1.58/1.30 % (18574)Instructions burned: 2 (million)
% 1.58/1.30 % (18574)------------------------------
% 1.58/1.30 % (18574)------------------------------
% 1.58/1.30 % (18578)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/3Mi)
% 1.58/1.30 % (18578)Instruction limit reached!
% 1.58/1.30 % (18578)------------------------------
% 1.58/1.30 % (18578)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.30 % (18578)Termination reason: Unknown
% 1.58/1.30 % (18578)Termination phase: Saturation
% 1.58/1.30
% 1.58/1.30 % (18578)Memory used [KB]: 5500
% 1.58/1.30 % (18578)Time elapsed: 0.002 s
% 1.58/1.30 % (18578)Instructions burned: 3 (million)
% 1.58/1.30 % (18578)------------------------------
% 1.58/1.30 % (18578)------------------------------
% 1.58/1.30 % (18573)Instruction limit reached!
% 1.58/1.30 % (18573)------------------------------
% 1.58/1.30 % (18573)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.30 % (18573)Termination reason: Unknown
% 1.58/1.30 % (18573)Termination phase: Saturation
% 1.58/1.30
% 1.58/1.30 % (18573)Memory used [KB]: 5884
% 1.58/1.30 % (18573)Time elapsed: 0.011 s
% 1.58/1.30 % (18573)Instructions burned: 15 (million)
% 1.58/1.30 % (18573)------------------------------
% 1.58/1.30 % (18573)------------------------------
% 1.58/1.30 % (18575)Refutation not found, incomplete strategy
% 1.58/1.30 % (18575)------------------------------
% 1.58/1.30 % (18575)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.30 % (18575)Termination reason: Refutation not found, incomplete strategy
% 1.58/1.30
% 1.58/1.30
% 1.58/1.30 % (18575)Memory used [KB]: 5500
% 1.58/1.30 % (18575)Time elapsed: 0.008 s
% 1.58/1.30 % (18575)Instructions burned: 10 (million)
% 1.58/1.30 % (18575)------------------------------
% 1.58/1.30 % (18575)------------------------------
% 1.58/1.30 % (18579)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/3Mi)
% 1.58/1.31 % (18577)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/16Mi)
% 1.58/1.31 % (18579)Instruction limit reached!
% 1.58/1.31 % (18579)------------------------------
% 1.58/1.31 % (18579)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.31 % (18579)Termination reason: Unknown
% 1.58/1.31 % (18579)Termination phase: Saturation
% 1.58/1.31
% 1.58/1.31 % (18579)Memory used [KB]: 5500
% 1.58/1.31 % (18579)Time elapsed: 0.003 s
% 1.58/1.31 % (18579)Instructions burned: 4 (million)
% 1.58/1.31 % (18579)------------------------------
% 1.58/1.31 % (18579)------------------------------
% 1.58/1.31 % (18581)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/3Mi)
% 1.58/1.31 % (18581)Instruction limit reached!
% 1.58/1.31 % (18581)------------------------------
% 1.58/1.31 % (18581)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.31 % (18581)Termination reason: Unknown
% 1.58/1.31 % (18581)Termination phase: Saturation
% 1.58/1.31
% 1.58/1.31 % (18581)Memory used [KB]: 5500
% 1.58/1.31 % (18581)Time elapsed: 0.002 s
% 1.58/1.31 % (18581)Instructions burned: 3 (million)
% 1.58/1.31 % (18581)------------------------------
% 1.58/1.31 % (18581)------------------------------
% 1.58/1.31 % (18577)First to succeed.
% 1.58/1.32 % (18584)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/710Mi)
% 1.58/1.32 % (18580)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/7Mi)
% 1.58/1.32 % (18580)Instruction limit reached!
% 1.58/1.32 % (18580)------------------------------
% 1.58/1.32 % (18580)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.32 % (18580)Termination reason: Unknown
% 1.58/1.32 % (18580)Termination phase: Saturation
% 1.58/1.32
% 1.58/1.32 % (18580)Memory used [KB]: 5500
% 1.58/1.32 % (18580)Time elapsed: 0.006 s
% 1.58/1.32 % (18580)Instructions burned: 8 (million)
% 1.58/1.32 % (18580)------------------------------
% 1.58/1.32 % (18580)------------------------------
% 1.58/1.32 % (18585)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/6Mi)
% 1.58/1.32 % (18583)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/18Mi)
% 1.58/1.32 % (18582)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_18236 for (2999ds/4Mi)
% 1.58/1.32 % (18577)Refutation found. Thanks to Tanya!
% 1.58/1.32 % SZS status Theorem for DTF2THF_18236
% 1.58/1.32 % SZS output start Proof for DTF2THF_18236
% 1.58/1.32 thf(func_def_1, type, f0: $o > $o).
% 1.58/1.32 thf(func_def_2, type, f1: $o > $o).
% 1.58/1.32 thf(func_def_3, type, f2: $o > $o).
% 1.58/1.32 thf(func_def_4, type, f3: $o > $o).
% 1.58/1.32 thf(func_def_5, type, f4: $o > $o).
% 1.58/1.32 thf(func_def_6, type, f5: $o > $o).
% 1.58/1.32 thf(func_def_7, type, f6: $o > $o).
% 1.58/1.32 thf(func_def_8, type, f7: $o > $o).
% 1.58/1.32 thf(f789,plain,(
% 1.58/1.32 $false),
% 1.58/1.32 inference(avatar_sat_refutation,[status(thm)],[f238,f247,f256,f261,f274,f283,f292,f297,f306,f311,f316,f317,f330,f339,f348,f353,f366,f375,f384,f389,f394,f399,f400,f401,f414,f423,f432,f437,f450,f459,f468,f473,f478,f479,f484,f485,f498,f507,f516,f521,f526,f527,f532,f533,f538,f539,f544,f545,f550,f555,f556,f557,f562,f563,f568,f569,f570,f571,f572,f573,f578,f579,f584,f585,f590,f595,f596,f597,f606,f615,f620,f625,f630,f631,f636,f637,f642,f647,f648,f649,f650,f651,f652,f653,f658,f663,f664,f665,f674,f683,f684,f685,f686,f687,f688,f689,f690,f691,f696,f697,f702,f703,f708,f709,f714,f715,f716,f717,f718,f719,f720,f721,f722,f723,f724,f725,f726,f727,f728,f729,f730,f731,f732,f733,f734,f735,f740,f741,f742,f743,f744,f745,f746,f747,f748,f749,f750,f751,f752,f753,f754,f755,f756,f757,f758,f759,f760,f761,f762,f763,f764,f765,f766,f767,f768,f769,f770,f771,f772,f773,f774,f775,f776,f777,f778,f779,f780,f781,f782,f783,f784,f785,f786,f787,f788])).
% 1.58/1.32 thf(f788,plain,(
% 1.58/1.32 (sF18 != $true) | (sF18 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f787,plain,(
% 1.58/1.32 (sF24 != $true) | (sF24 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f786,plain,(
% 1.58/1.32 (sF5 != $true) | (sF5 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f785,plain,(
% 1.58/1.32 (sF19 != $true) | (sF19 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f784,plain,(
% 1.58/1.32 ($true != sF21) | ($false != sF21) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f783,plain,(
% 1.58/1.32 (sF14 != $true) | (sF14 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f782,plain,(
% 1.58/1.32 (sF26 != $true) | (sF26 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f781,plain,(
% 1.58/1.32 ((f0 @ $false) != $true) | ((f0 @ $false) != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f780,plain,(
% 1.58/1.32 ((f0 @ $true) != $true) | ((f0 @ $true) != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f779,plain,(
% 1.58/1.32 (sF12 != $true) | (sF12 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f778,plain,(
% 1.58/1.32 (sF27 != $true) | (sF27 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f777,plain,(
% 1.58/1.32 ($true != sF9) | ($false != sF9) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f776,plain,(
% 1.58/1.32 (sF11 != $true) | (sF11 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f775,plain,(
% 1.58/1.32 (sF30 != $true) | (sF30 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f774,plain,(
% 1.58/1.32 (sF15 != $true) | (sF15 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f773,plain,(
% 1.58/1.32 ($true != sF20) | ($false != sF20) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f772,plain,(
% 1.58/1.32 (sF13 != $true) | (sF13 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f771,plain,(
% 1.58/1.32 (sF17 != $true) | (sF17 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f770,plain,(
% 1.58/1.32 (x != $true) | (x != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f769,plain,(
% 1.58/1.32 ($true != sF0) | ($false != sF0) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f768,plain,(
% 1.58/1.32 (sF1 != $true) | (sF1 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f767,plain,(
% 1.58/1.32 (sF2 != $true) | (sF2 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f766,plain,(
% 1.58/1.32 (sF6 != $true) | (sF6 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f765,plain,(
% 1.58/1.32 ((f6 @ $false) != $true) | ((f6 @ $false) != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f764,plain,(
% 1.58/1.32 (sF3 != $true) | (sF3 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f763,plain,(
% 1.58/1.32 ((f6 @ $true) != $true) | ((f6 @ $true) != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f762,plain,(
% 1.58/1.32 (sF23 != $true) | (sF23 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f761,plain,(
% 1.58/1.32 ((f1 @ $false) != $false) | ((f1 @ $false) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f760,plain,(
% 1.58/1.32 (sF28 != $false) | (sF28 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f759,plain,(
% 1.58/1.32 ($false != sF29) | ($true != sF29) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f758,plain,(
% 1.58/1.32 ((f1 @ $true) != $false) | ((f1 @ $true) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f757,plain,(
% 1.58/1.32 ((f2 @ $false) != $false) | ((f2 @ $false) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f756,plain,(
% 1.58/1.32 (sF10 != $false) | (sF10 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f755,plain,(
% 1.58/1.32 ((f2 @ $true) != $false) | ((f2 @ $true) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f754,plain,(
% 1.58/1.32 (sF16 != $false) | (sF16 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f753,plain,(
% 1.58/1.32 ($true != (f5 @ $false)) | ($false != (f5 @ $false)) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f752,plain,(
% 1.58/1.32 ($true != sF22) | ($false != sF22) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f751,plain,(
% 1.58/1.32 (sF4 != $false) | (sF4 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f750,plain,(
% 1.58/1.32 ((f5 @ $true) != $false) | ((f5 @ $true) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f749,plain,(
% 1.58/1.32 ($false != (f4 @ $false)) | ($true != (f4 @ $false)) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f748,plain,(
% 1.58/1.32 ((f4 @ $true) != $false) | ((f4 @ $true) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f747,plain,(
% 1.58/1.32 (sF7 != $false) | (sF7 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f746,plain,(
% 1.58/1.32 (sF8 != $true) | (sF8 != $false) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f745,plain,(
% 1.58/1.32 ((f3 @ $false) != $false) | ((f3 @ $false) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f744,plain,(
% 1.58/1.32 ((f3 @ $true) != $false) | ((f3 @ $true) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f743,plain,(
% 1.58/1.32 (sF25 != $false) | (sF25 != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f742,plain,(
% 1.58/1.32 ((f7 @ $false) != $false) | ((f7 @ $false) != $true) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f741,plain,(
% 1.58/1.32 ($true != (f7 @ $true)) | ($false != (f7 @ $true)) | ($true = $false)),
% 1.58/1.32 introduced(definition,[],[theory_tautology_sat_conflict])).
% 1.58/1.32 thf(f740,plain,(
% 1.58/1.32 ~spl31_97),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f3,f737])).
% 1.58/1.32 thf(f737,definition,(
% 1.58/1.32 spl31_97 <=> ($true = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_97])],[avatar_definition])).
% 1.58/1.32 thf(f3,plain,(
% 1.58/1.32 ($true != $false)),
% 1.58/1.32 introduced(definition,[],[fool_axiom])).
% 1.58/1.32 thf(f735,plain,(
% 1.58/1.32 spl31_59 | spl31_93 | spl31_36),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f41,f386,f693,f495])).
% 1.58/1.32 thf(f495,definition,(
% 1.58/1.32 spl31_59 <=> (sF18 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_59])],[avatar_definition])).
% 1.58/1.32 thf(f693,definition,(
% 1.58/1.32 spl31_93 <=> (sF19 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_93])],[avatar_definition])).
% 1.58/1.32 thf(f386,definition,(
% 1.58/1.32 spl31_36 <=> ($true = (f5 @ $false))),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_36])],[avatar_definition])).
% 1.58/1.32 thf(f41,plain,(
% 1.58/1.32 ($true = (f5 @ $false)) | (sF19 = $false) | (sF18 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f39])).
% 1.58/1.32 thf(f39,plain,(
% 1.58/1.32 (sF19 = (f5 @ $false)) | (sF18 = $true)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f25])).
% 1.58/1.32 thf(f25,definition,(
% 1.58/1.32 (sF19 = (f5 @ sF18))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f734,plain,(
% 1.58/1.32 spl31_59 | spl31_34 | spl31_94),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f40,f699,f377,f495])).
% 1.58/1.32 thf(f377,definition,(
% 1.58/1.32 spl31_34 <=> ($false = (f5 @ $false))),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_34])],[avatar_definition])).
% 1.58/1.32 thf(f699,definition,(
% 1.58/1.32 spl31_94 <=> (sF19 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_94])],[avatar_definition])).
% 1.58/1.32 thf(f40,plain,(
% 1.58/1.32 (sF19 = $true) | (sF18 = $true) | ($false = (f5 @ $false))),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f39])).
% 1.58/1.32 thf(f733,plain,(
% 1.58/1.32 spl31_60 | spl31_32 | spl31_93),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f43,f693,f368,f500])).
% 1.58/1.32 thf(f500,definition,(
% 1.58/1.32 spl31_60 <=> (sF18 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_60])],[avatar_definition])).
% 1.58/1.32 thf(f368,definition,(
% 1.58/1.32 spl31_32 <=> ((f5 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_32])],[avatar_definition])).
% 1.58/1.32 thf(f43,plain,(
% 1.58/1.32 (sF19 = $false) | ((f5 @ $true) = $true) | (sF18 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f38])).
% 1.58/1.32 thf(f38,plain,(
% 1.58/1.32 (sF19 = (f5 @ $true)) | (sF18 = $false)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f25])).
% 1.58/1.32 thf(f732,plain,(
% 1.58/1.32 spl31_94 | spl31_30 | spl31_60),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f42,f500,f359,f699])).
% 1.58/1.32 thf(f359,definition,(
% 1.58/1.32 spl31_30 <=> ((f5 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_30])],[avatar_definition])).
% 1.58/1.32 thf(f42,plain,(
% 1.58/1.32 (sF19 = $true) | (sF18 = $false) | ((f5 @ $true) = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f38])).
% 1.58/1.32 thf(f731,plain,(
% 1.58/1.32 spl31_24 | spl31_16 | spl31_55),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f47,f475,f294,f332])).
% 1.58/1.32 thf(f332,definition,(
% 1.58/1.32 spl31_24 <=> ($true = sF22)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_24])],[avatar_definition])).
% 1.58/1.32 thf(f294,definition,(
% 1.58/1.32 spl31_16 <=> ((f3 @ $false) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_16])],[avatar_definition])).
% 1.58/1.32 thf(f475,definition,(
% 1.58/1.32 spl31_55 <=> (sF23 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_55])],[avatar_definition])).
% 1.58/1.32 thf(f47,plain,(
% 1.58/1.32 (sF23 = $false) | ((f3 @ $false) = $true) | ($true = sF22)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f45])).
% 1.58/1.32 thf(f45,plain,(
% 1.58/1.32 (sF23 = (f3 @ $false)) | ($true = sF22)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f29])).
% 1.58/1.32 thf(f29,definition,(
% 1.58/1.32 (sF23 = (f3 @ sF22))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f730,plain,(
% 1.58/1.32 spl31_24 | spl31_14 | spl31_56),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f46,f481,f285,f332])).
% 1.58/1.32 thf(f285,definition,(
% 1.58/1.32 spl31_14 <=> ((f3 @ $false) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_14])],[avatar_definition])).
% 1.58/1.32 thf(f481,definition,(
% 1.58/1.32 spl31_56 <=> (sF23 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_56])],[avatar_definition])).
% 1.58/1.32 thf(f46,plain,(
% 1.58/1.32 ((f3 @ $false) = $false) | (sF23 = $true) | ($true = sF22)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f45])).
% 1.58/1.32 thf(f729,plain,(
% 1.58/1.32 spl31_10 | spl31_55 | spl31_21),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f49,f319,f475,f267])).
% 1.58/1.32 thf(f267,definition,(
% 1.58/1.32 spl31_10 <=> ((f3 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_10])],[avatar_definition])).
% 1.58/1.32 thf(f319,definition,(
% 1.58/1.32 spl31_21 <=> ($false = sF22)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_21])],[avatar_definition])).
% 1.58/1.32 thf(f49,plain,(
% 1.58/1.32 ($false = sF22) | ((f3 @ $true) = $true) | (sF23 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f44])).
% 1.58/1.32 thf(f44,plain,(
% 1.58/1.32 ($false = sF22) | (sF23 = (f3 @ $true))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f29])).
% 1.58/1.32 thf(f728,plain,(
% 1.58/1.32 spl31_13 | spl31_56 | spl31_21),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f48,f319,f481,f280])).
% 1.58/1.32 thf(f280,definition,(
% 1.58/1.32 spl31_13 <=> ((f3 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_13])],[avatar_definition])).
% 1.58/1.32 thf(f48,plain,(
% 1.58/1.32 ((f3 @ $true) = $false) | (sF23 = $true) | ($false = sF22)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f44])).
% 1.58/1.32 thf(f727,plain,(
% 1.58/1.32 spl31_91 | spl31_87 | spl31_81),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f53,f617,f655,f676])).
% 1.58/1.32 thf(f676,definition,(
% 1.58/1.32 spl31_91 <=> (sF15 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_91])],[avatar_definition])).
% 1.58/1.32 thf(f655,definition,(
% 1.58/1.32 spl31_87 <=> (sF14 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_87])],[avatar_definition])).
% 1.58/1.32 thf(f617,definition,(
% 1.58/1.32 spl31_81 <=> ((f0 @ $false) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_81])],[avatar_definition])).
% 1.58/1.32 thf(f53,plain,(
% 1.58/1.32 (sF14 = $true) | ((f0 @ $false) = $true) | (sF15 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f51])).
% 1.58/1.32 thf(f51,plain,(
% 1.58/1.32 (sF14 = $true) | (sF15 = (f0 @ $false))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f21])).
% 1.58/1.32 thf(f21,definition,(
% 1.58/1.32 (sF15 = (f0 @ sF14))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f726,plain,(
% 1.58/1.32 spl31_82 | spl31_87 | spl31_89),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f52,f667,f655,f622])).
% 1.58/1.32 thf(f622,definition,(
% 1.58/1.32 spl31_82 <=> ((f0 @ $false) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_82])],[avatar_definition])).
% 1.58/1.32 thf(f667,definition,(
% 1.58/1.32 spl31_89 <=> (sF15 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_89])],[avatar_definition])).
% 1.58/1.32 thf(f52,plain,(
% 1.58/1.32 (sF14 = $true) | ((f0 @ $false) = $false) | (sF15 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f51])).
% 1.58/1.32 thf(f725,plain,(
% 1.58/1.32 spl31_88 | spl31_80 | spl31_91),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f55,f676,f612,f660])).
% 1.58/1.32 thf(f660,definition,(
% 1.58/1.32 spl31_88 <=> (sF14 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_88])],[avatar_definition])).
% 1.58/1.32 thf(f612,definition,(
% 1.58/1.32 spl31_80 <=> ((f0 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_80])],[avatar_definition])).
% 1.58/1.32 thf(f55,plain,(
% 1.58/1.32 (sF14 = $false) | ((f0 @ $true) = $true) | (sF15 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f50])).
% 1.58/1.32 thf(f50,plain,(
% 1.58/1.32 (sF14 = $false) | (sF15 = (f0 @ $true))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f21])).
% 1.58/1.32 thf(f724,plain,(
% 1.58/1.32 spl31_89 | spl31_77 | spl31_88),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f54,f660,f599,f667])).
% 1.58/1.32 thf(f599,definition,(
% 1.58/1.32 spl31_77 <=> ((f0 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_77])],[avatar_definition])).
% 1.58/1.32 thf(f54,plain,(
% 1.58/1.32 (sF15 = $true) | (sF14 = $false) | ((f0 @ $true) = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f50])).
% 1.58/1.32 thf(f723,plain,(
% 1.58/1.32 spl31_81 | spl31_51 | spl31_92),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f59,f680,f456,f617])).
% 1.58/1.32 thf(f456,definition,(
% 1.58/1.32 spl31_51 <=> ($true = sF29)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_51])],[avatar_definition])).
% 1.58/1.32 thf(f680,definition,(
% 1.58/1.32 spl31_92 <=> (sF30 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_92])],[avatar_definition])).
% 1.58/1.32 thf(f59,plain,(
% 1.58/1.32 ((f0 @ $false) = $true) | ($true = sF29) | (sF30 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f57])).
% 1.58/1.32 thf(f57,plain,(
% 1.58/1.32 ($true = sF29) | (sF30 = (f0 @ $false))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f36])).
% 1.58/1.32 thf(f36,definition,(
% 1.58/1.32 (sF30 = (f0 @ sF29))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f722,plain,(
% 1.58/1.32 spl31_51 | spl31_90 | spl31_82),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f58,f622,f671,f456])).
% 1.58/1.32 thf(f671,definition,(
% 1.58/1.32 spl31_90 <=> (sF30 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_90])],[avatar_definition])).
% 1.58/1.32 thf(f58,plain,(
% 1.58/1.32 (sF30 = $true) | ((f0 @ $false) = $false) | ($true = sF29)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f57])).
% 1.58/1.32 thf(f721,plain,(
% 1.58/1.32 spl31_80 | spl31_48 | spl31_92),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f61,f680,f443,f612])).
% 1.58/1.32 thf(f443,definition,(
% 1.58/1.32 spl31_48 <=> ($false = sF29)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_48])],[avatar_definition])).
% 1.58/1.32 thf(f61,plain,(
% 1.58/1.32 ((f0 @ $true) = $true) | ($false = sF29) | (sF30 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f56])).
% 1.58/1.32 thf(f56,plain,(
% 1.58/1.32 (sF30 = (f0 @ $true)) | ($false = sF29)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f36])).
% 1.58/1.32 thf(f720,plain,(
% 1.58/1.32 spl31_77 | spl31_90 | spl31_48),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f60,f443,f671,f599])).
% 1.58/1.32 thf(f60,plain,(
% 1.58/1.32 ((f0 @ $true) = $false) | ($false = sF29) | (sF30 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f56])).
% 1.58/1.32 thf(f719,plain,(
% 1.58/1.32 spl31_95 | spl31_31 | spl31_28),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f65,f350,f363,f705])).
% 1.58/1.32 thf(f705,definition,(
% 1.58/1.32 spl31_95 <=> (sF5 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_95])],[avatar_definition])).
% 1.58/1.32 thf(f363,definition,(
% 1.58/1.32 spl31_31 <=> (sF4 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_31])],[avatar_definition])).
% 1.58/1.32 thf(f350,definition,(
% 1.58/1.32 spl31_28 <=> ($true = (f4 @ $false))),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_28])],[avatar_definition])).
% 1.58/1.32 thf(f65,plain,(
% 1.58/1.32 (sF5 = $false) | ($true = (f4 @ $false)) | (sF4 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f63])).
% 1.58/1.32 thf(f63,plain,(
% 1.58/1.32 (sF5 = (f4 @ $false)) | (sF4 = $true)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f11])).
% 1.58/1.32 thf(f11,definition,(
% 1.58/1.32 ((f4 @ sF4) = sF5)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f718,plain,(
% 1.58/1.32 spl31_31 | spl31_27 | spl31_96),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f64,f711,f345,f363])).
% 1.58/1.32 thf(f345,definition,(
% 1.58/1.32 spl31_27 <=> ($false = (f4 @ $false))),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_27])],[avatar_definition])).
% 1.58/1.32 thf(f711,definition,(
% 1.58/1.32 spl31_96 <=> (sF5 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_96])],[avatar_definition])).
% 1.58/1.32 thf(f64,plain,(
% 1.58/1.32 (sF5 = $true) | ($false = (f4 @ $false)) | (sF4 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f63])).
% 1.58/1.32 thf(f717,plain,(
% 1.58/1.32 spl31_23 | spl31_33 | spl31_95),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f67,f705,f372,f327])).
% 1.58/1.32 thf(f327,definition,(
% 1.58/1.32 spl31_23 <=> ((f4 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_23])],[avatar_definition])).
% 1.58/1.32 thf(f372,definition,(
% 1.58/1.32 spl31_33 <=> (sF4 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_33])],[avatar_definition])).
% 1.58/1.32 thf(f67,plain,(
% 1.58/1.32 ((f4 @ $true) = $true) | (sF4 = $false) | (sF5 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f62])).
% 1.58/1.32 thf(f62,plain,(
% 1.58/1.32 (sF4 = $false) | (sF5 = (f4 @ $true))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f11])).
% 1.58/1.32 thf(f716,plain,(
% 1.58/1.32 spl31_25 | spl31_96 | spl31_33),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f66,f372,f711,f336])).
% 1.58/1.32 thf(f336,definition,(
% 1.58/1.32 spl31_25 <=> ((f4 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_25])],[avatar_definition])).
% 1.58/1.32 thf(f66,plain,(
% 1.58/1.32 (sF4 = $false) | (sF5 = $true) | ((f4 @ $true) = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f62])).
% 1.58/1.32 thf(f715,plain,(
% 1.58/1.32 spl31_65 | spl31_96 | spl31_28),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f71,f350,f711,f523])).
% 1.58/1.32 thf(f523,definition,(
% 1.58/1.32 spl31_65 <=> (sF6 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_65])],[avatar_definition])).
% 1.58/1.32 thf(f71,plain,(
% 1.58/1.32 (sF6 = $false) | ($true = (f4 @ $false)) | (sF5 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f69])).
% 1.58/1.32 thf(f69,plain,(
% 1.58/1.32 (sF5 = $true) | (sF6 = (f4 @ $false))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f12])).
% 1.58/1.32 thf(f12,definition,(
% 1.58/1.32 (sF6 = (f4 @ sF5))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f714,plain,(
% 1.58/1.32 spl31_66 | spl31_96 | spl31_27),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f70,f345,f711,f529])).
% 1.58/1.32 thf(f529,definition,(
% 1.58/1.32 spl31_66 <=> (sF6 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_66])],[avatar_definition])).
% 1.58/1.32 thf(f70,plain,(
% 1.58/1.32 ($false = (f4 @ $false)) | (sF5 = $true) | (sF6 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f69])).
% 1.58/1.32 thf(f709,plain,(
% 1.58/1.32 spl31_65 | spl31_95 | spl31_23),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f73,f327,f705,f523])).
% 1.58/1.32 thf(f73,plain,(
% 1.58/1.32 (sF5 = $false) | (sF6 = $false) | ((f4 @ $true) = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f68])).
% 1.58/1.32 thf(f68,plain,(
% 1.58/1.32 (sF5 = $false) | (sF6 = (f4 @ $true))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f12])).
% 1.58/1.32 thf(f708,plain,(
% 1.58/1.32 spl31_25 | spl31_95 | spl31_66),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f72,f529,f705,f336])).
% 1.58/1.32 thf(f72,plain,(
% 1.58/1.32 (sF5 = $false) | ((f4 @ $true) = $false) | (sF6 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f68])).
% 1.58/1.32 thf(f703,plain,(
% 1.58/1.32 spl31_83 | spl31_94 | spl31_36),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f77,f386,f699,f627])).
% 1.58/1.32 thf(f627,definition,(
% 1.58/1.32 spl31_83 <=> ($false = sF20)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_83])],[avatar_definition])).
% 1.58/1.32 thf(f77,plain,(
% 1.58/1.32 ($false = sF20) | (sF19 = $true) | ($true = (f5 @ $false))),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f75])).
% 1.58/1.32 thf(f75,plain,(
% 1.58/1.32 (sF20 = (f5 @ $false)) | (sF19 = $true)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f26])).
% 1.58/1.32 thf(f26,definition,(
% 1.58/1.32 ((f5 @ sF19) = sF20)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f702,plain,(
% 1.58/1.32 spl31_34 | spl31_94 | spl31_84),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f76,f633,f699,f377])).
% 1.58/1.32 thf(f633,definition,(
% 1.58/1.32 spl31_84 <=> ($true = sF20)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_84])],[avatar_definition])).
% 1.58/1.32 thf(f76,plain,(
% 1.58/1.32 (sF19 = $true) | ($true = sF20) | ($false = (f5 @ $false))),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f75])).
% 1.58/1.32 thf(f697,plain,(
% 1.58/1.32 spl31_84 | spl31_30 | spl31_93),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f79,f693,f359,f633])).
% 1.58/1.32 thf(f79,plain,(
% 1.58/1.32 (sF19 = $false) | ((f5 @ $true) = $false) | ($true = sF20)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f74])).
% 1.58/1.32 thf(f74,plain,(
% 1.58/1.32 (sF19 = $false) | ((f5 @ $true) = sF20)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f26])).
% 1.58/1.32 thf(f696,plain,(
% 1.58/1.32 spl31_83 | spl31_93 | spl31_32),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f78,f368,f693,f627])).
% 1.58/1.32 thf(f78,plain,(
% 1.58/1.32 ((f5 @ $true) = $true) | (sF19 = $false) | ($false = sF20)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f74])).
% 1.58/1.32 thf(f691,plain,(
% 1.58/1.32 spl31_73 | spl31_53 | spl31_85),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f83,f639,f465,f575])).
% 1.58/1.32 thf(f575,definition,(
% 1.58/1.32 spl31_73 <=> (sF27 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_73])],[avatar_definition])).
% 1.58/1.32 thf(f465,definition,(
% 1.58/1.32 spl31_53 <=> ((f1 @ $false) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_53])],[avatar_definition])).
% 1.58/1.32 thf(f639,definition,(
% 1.58/1.32 spl31_85 <=> (sF26 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_85])],[avatar_definition])).
% 1.58/1.32 thf(f83,plain,(
% 1.58/1.32 ((f1 @ $false) = $true) | (sF26 = $true) | (sF27 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f81])).
% 1.58/1.32 thf(f81,plain,(
% 1.58/1.32 (sF26 = $true) | (sF27 = (f1 @ $false))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f33])).
% 1.58/1.32 thf(f33,definition,(
% 1.58/1.32 (sF27 = (f1 @ sF26))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f690,plain,(
% 1.58/1.32 spl31_54 | spl31_74 | spl31_85),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f82,f639,f581,f470])).
% 1.58/1.32 thf(f470,definition,(
% 1.58/1.32 spl31_54 <=> ((f1 @ $false) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_54])],[avatar_definition])).
% 1.58/1.32 thf(f581,definition,(
% 1.58/1.32 spl31_74 <=> (sF27 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_74])],[avatar_definition])).
% 1.58/1.32 thf(f82,plain,(
% 1.58/1.32 (sF26 = $true) | ((f1 @ $false) = $false) | (sF27 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f81])).
% 1.58/1.32 thf(f689,plain,(
% 1.58/1.32 spl31_73 | spl31_49 | spl31_86),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f85,f644,f447,f575])).
% 1.58/1.32 thf(f447,definition,(
% 1.58/1.32 spl31_49 <=> ((f1 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_49])],[avatar_definition])).
% 1.58/1.32 thf(f644,definition,(
% 1.58/1.32 spl31_86 <=> (sF26 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_86])],[avatar_definition])).
% 1.58/1.32 thf(f85,plain,(
% 1.58/1.32 (sF26 = $false) | (sF27 = $false) | ((f1 @ $true) = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f80])).
% 1.58/1.32 thf(f80,plain,(
% 1.58/1.32 (sF26 = $false) | (sF27 = (f1 @ $true))),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f33])).
% 1.58/1.32 thf(f688,plain,(
% 1.58/1.32 spl31_86 | spl31_74 | spl31_50),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f84,f452,f581,f644])).
% 1.58/1.32 thf(f452,definition,(
% 1.58/1.32 spl31_50 <=> ((f1 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_50])],[avatar_definition])).
% 1.58/1.32 thf(f84,plain,(
% 1.58/1.32 ((f1 @ $true) = $false) | (sF26 = $false) | (sF27 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f80])).
% 1.58/1.32 thf(f687,plain,(
% 1.58/1.32 spl31_72 | spl31_45 | spl31_19),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f89,f308,f429,f565])).
% 1.58/1.32 thf(f565,definition,(
% 1.58/1.32 spl31_72 <=> ($true = sF9)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_72])],[avatar_definition])).
% 1.58/1.32 thf(f429,definition,(
% 1.58/1.32 spl31_45 <=> ((f2 @ $false) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_45])],[avatar_definition])).
% 1.58/1.32 thf(f308,definition,(
% 1.58/1.32 spl31_19 <=> (sF8 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_19])],[avatar_definition])).
% 1.58/1.32 thf(f89,plain,(
% 1.58/1.32 ((f2 @ $false) = $false) | (sF8 = $true) | ($true = sF9)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f87])).
% 1.58/1.32 thf(f87,plain,(
% 1.58/1.32 (sF8 = $true) | ((f2 @ $false) = sF9)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f15])).
% 1.58/1.32 thf(f15,definition,(
% 1.58/1.32 ((f2 @ sF8) = sF9)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f686,plain,(
% 1.58/1.32 spl31_19 | spl31_46 | spl31_71),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f88,f559,f434,f308])).
% 1.58/1.32 thf(f434,definition,(
% 1.58/1.32 spl31_46 <=> ((f2 @ $false) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_46])],[avatar_definition])).
% 1.58/1.32 thf(f559,definition,(
% 1.58/1.32 spl31_71 <=> ($false = sF9)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_71])],[avatar_definition])).
% 1.58/1.32 thf(f88,plain,(
% 1.58/1.32 ((f2 @ $false) = $true) | ($false = sF9) | (sF8 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f87])).
% 1.58/1.32 thf(f685,plain,(
% 1.58/1.32 spl31_39 | spl31_72 | spl31_18),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f91,f303,f565,f403])).
% 1.58/1.32 thf(f403,definition,(
% 1.58/1.32 spl31_39 <=> ((f2 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_39])],[avatar_definition])).
% 1.58/1.32 thf(f303,definition,(
% 1.58/1.32 spl31_18 <=> (sF8 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_18])],[avatar_definition])).
% 1.58/1.32 thf(f91,plain,(
% 1.58/1.32 ((f2 @ $true) = $false) | (sF8 = $false) | ($true = sF9)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f86])).
% 1.58/1.32 thf(f86,plain,(
% 1.58/1.32 ((f2 @ $true) = sF9) | (sF8 = $false)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f15])).
% 1.58/1.32 thf(f684,plain,(
% 1.58/1.32 spl31_42 | spl31_71 | spl31_18),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f90,f303,f559,f416])).
% 1.58/1.32 thf(f416,definition,(
% 1.58/1.32 spl31_42 <=> ((f2 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_42])],[avatar_definition])).
% 1.58/1.32 thf(f90,plain,(
% 1.58/1.32 ((f2 @ $true) = $true) | ($false = sF9) | (sF8 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f86])).
% 1.58/1.32 thf(f683,plain,(
% 1.58/1.32 spl31_91 | spl31_92),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f93,f680,f676])).
% 1.58/1.32 thf(f93,plain,(
% 1.58/1.32 (sF30 = $false) | (sF15 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.58/1.32 thf(f37,plain,(
% 1.58/1.32 (sF30 != sF15)),
% 1.58/1.32 inference(definition_folding,[status(thm)],[f5,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f6,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6])).
% 1.58/1.32 thf(f7,definition,(
% 1.58/1.32 (sF1 = (f6 @ sF0))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f8,definition,(
% 1.58/1.32 (sF2 = (f6 @ sF1))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f9,definition,(
% 1.58/1.32 (sF3 = (f6 @ sF2))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f10,definition,(
% 1.58/1.32 ((f5 @ sF3) = sF4)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f13,definition,(
% 1.58/1.32 (sF7 = (f4 @ sF6))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f14,definition,(
% 1.58/1.32 (sF8 = (f3 @ sF7))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f16,definition,(
% 1.58/1.32 ((f2 @ sF9) = sF10)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f17,definition,(
% 1.58/1.32 (sF11 = (f2 @ sF10))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f18,definition,(
% 1.58/1.32 ((f1 @ sF11) = sF12)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f19,definition,(
% 1.58/1.32 (sF13 = (f0 @ sF12))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f20,definition,(
% 1.58/1.32 ((f0 @ sF13) = sF14)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f6,definition,(
% 1.58/1.32 ((f7 @ x) = sF0)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f22,definition,(
% 1.58/1.32 (sF16 = (f7 @ sF0))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f23,definition,(
% 1.58/1.32 (sF17 = (f7 @ sF16))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f24,definition,(
% 1.58/1.32 (sF18 = (f6 @ sF17))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f27,definition,(
% 1.58/1.32 ((f5 @ sF20) = sF21)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f28,definition,(
% 1.58/1.32 ((f4 @ sF21) = sF22)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f30,definition,(
% 1.58/1.32 ((f3 @ sF23) = sF24)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f31,definition,(
% 1.58/1.32 ((f3 @ sF24) = sF25)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f32,definition,(
% 1.58/1.32 (sF26 = (f2 @ sF25))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f34,definition,(
% 1.58/1.32 (sF28 = (f1 @ sF27))),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f35,definition,(
% 1.58/1.32 ((f1 @ sF28) = sF29)),
% 1.58/1.32 introduced(definition,[],[function_definition])).
% 1.58/1.32 thf(f5,plain,(
% 1.58/1.32 ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ (f7 @ x)))))))))))))))) != (f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ (f7 @ (f7 @ (f7 @ x)))))))))))))))))),
% 1.58/1.32 inference(cnf_transformation,[status(thm)],[f4])).
% 1.58/1.32 thf(f4,plain,(
% 1.58/1.32 ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ (f7 @ x)))))))))))))))) != (f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ (f7 @ (f7 @ (f7 @ x)))))))))))))))))),
% 1.58/1.32 inference(flattening,[status(thm)],[f2])).
% 1.58/1.32 thf(f2,negated_conjecture,(
% 1.58/1.32 ~((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ (f7 @ x)))))))))))))))) = (f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ (f7 @ (f7 @ (f7 @ x)))))))))))))))))),
% 1.58/1.32 inference(negated_conjecture,[status(cth)],[f1])).
% 1.58/1.32 thf(f1,conjecture,(
% 1.58/1.32 ((f0 @ (f0 @ (f0 @ (f1 @ (f2 @ (f2 @ (f2 @ (f3 @ (f4 @ (f4 @ (f4 @ (f5 @ (f6 @ (f6 @ (f6 @ (f7 @ x)))))))))))))))) = (f0 @ (f1 @ (f1 @ (f1 @ (f2 @ (f3 @ (f3 @ (f3 @ (f4 @ (f5 @ (f5 @ (f5 @ (f6 @ (f7 @ (f7 @ (f7 @ x)))))))))))))))))),
% 1.58/1.32 file('/export/starexec/sandbox/tmp/tmp.Tk9QRBkYJG/DTF2THF_18236.p',kaminski8)).
% 1.58/1.32 thf(f674,plain,(
% 1.58/1.32 spl31_89 | spl31_90),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f92,f671,f667])).
% 1.58/1.32 thf(f92,plain,(
% 1.58/1.32 (sF15 = $true) | (sF30 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f37])).
% 1.58/1.32 thf(f665,plain,(
% 1.58/1.32 spl31_82 | spl31_87 | spl31_78),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f97,f603,f655,f622])).
% 1.58/1.32 thf(f603,definition,(
% 1.58/1.32 spl31_78 <=> (sF13 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_78])],[avatar_definition])).
% 1.58/1.32 thf(f97,plain,(
% 1.58/1.32 (sF14 = $true) | ((f0 @ $false) = $false) | (sF13 = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f95])).
% 1.58/1.32 thf(f95,plain,(
% 1.58/1.32 ((f0 @ $false) = sF14) | (sF13 = $true)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f20])).
% 1.58/1.32 thf(f664,plain,(
% 1.58/1.32 spl31_81 | spl31_88 | spl31_78),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f96,f603,f660,f617])).
% 1.58/1.32 thf(f96,plain,(
% 1.58/1.32 (sF14 = $false) | (sF13 = $true) | ((f0 @ $false) = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f95])).
% 1.58/1.32 thf(f663,plain,(
% 1.58/1.32 spl31_80 | spl31_79 | spl31_88),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f99,f660,f608,f612])).
% 1.58/1.32 thf(f608,definition,(
% 1.58/1.32 spl31_79 <=> (sF13 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_79])],[avatar_definition])).
% 1.58/1.32 thf(f99,plain,(
% 1.58/1.32 (sF14 = $false) | (sF13 = $false) | ((f0 @ $true) = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f94])).
% 1.58/1.32 thf(f94,plain,(
% 1.58/1.32 (sF14 = (f0 @ $true)) | (sF13 = $false)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f20])).
% 1.58/1.32 thf(f658,plain,(
% 1.58/1.32 spl31_87 | spl31_79 | spl31_77),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f98,f599,f608,f655])).
% 1.58/1.32 thf(f98,plain,(
% 1.58/1.32 ((f0 @ $true) = $false) | (sF14 = $true) | (sF13 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f94])).
% 1.58/1.32 thf(f653,plain,(
% 1.58/1.32 spl31_67 | spl31_69 | spl31_64),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f103,f518,f547,f535])).
% 1.58/1.32 thf(f535,definition,(
% 1.58/1.32 spl31_67 <=> (sF2 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_67])],[avatar_definition])).
% 1.58/1.32 thf(f547,definition,(
% 1.58/1.32 spl31_69 <=> (sF1 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_69])],[avatar_definition])).
% 1.58/1.32 thf(f518,definition,(
% 1.58/1.32 spl31_64 <=> ((f6 @ $false) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_64])],[avatar_definition])).
% 1.58/1.32 thf(f103,plain,(
% 1.58/1.32 ((f6 @ $false) = $true) | (sF1 = $true) | (sF2 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f101])).
% 1.58/1.32 thf(f101,plain,(
% 1.58/1.32 (sF2 = (f6 @ $false)) | (sF1 = $true)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f8])).
% 1.58/1.32 thf(f652,plain,(
% 1.58/1.32 spl31_63 | spl31_68 | spl31_69),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f102,f547,f541,f513])).
% 1.58/1.32 thf(f513,definition,(
% 1.58/1.32 spl31_63 <=> ((f6 @ $false) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_63])],[avatar_definition])).
% 1.58/1.32 thf(f541,definition,(
% 1.58/1.32 spl31_68 <=> (sF2 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_68])],[avatar_definition])).
% 1.58/1.32 thf(f102,plain,(
% 1.58/1.32 (sF2 = $true) | (sF1 = $true) | ((f6 @ $false) = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f101])).
% 1.58/1.32 thf(f651,plain,(
% 1.58/1.32 spl31_67 | spl31_70 | spl31_61),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f105,f504,f552,f535])).
% 1.58/1.32 thf(f552,definition,(
% 1.58/1.32 spl31_70 <=> (sF1 = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_70])],[avatar_definition])).
% 1.58/1.32 thf(f504,definition,(
% 1.58/1.32 spl31_61 <=> ((f6 @ $true) = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_61])],[avatar_definition])).
% 1.58/1.32 thf(f105,plain,(
% 1.58/1.32 (sF2 = $false) | (sF1 = $false) | ((f6 @ $true) = $true)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f100])).
% 1.58/1.32 thf(f100,plain,(
% 1.58/1.32 (sF2 = (f6 @ $true)) | (sF1 = $false)),
% 1.58/1.32 inference(cases_simplifying,[status(thm)],[f8])).
% 1.58/1.32 thf(f650,plain,(
% 1.58/1.32 spl31_68 | spl31_57 | spl31_70),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f104,f552,f487,f541])).
% 1.58/1.32 thf(f487,definition,(
% 1.58/1.32 spl31_57 <=> ((f6 @ $true) = $false)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_57])],[avatar_definition])).
% 1.58/1.32 thf(f104,plain,(
% 1.58/1.32 ((f6 @ $true) = $false) | (sF2 = $true) | (sF1 = $false)),
% 1.58/1.32 inference(binary_proxy_clausification,[status(thm)],[f100])).
% 1.58/1.32 thf(f649,plain,(
% 1.58/1.32 spl31_12 | spl31_45 | spl31_85),
% 1.58/1.32 inference(avatar_split_clause,[status(thm)],[f109,f639,f429,f276])).
% 1.58/1.32 thf(f276,definition,(
% 1.58/1.32 spl31_12 <=> (sF25 = $true)),
% 1.58/1.32 introduced(definition,[new_symbols(naming,[spl31_12])],[avatar_definition])).
% 1.58/1.32 thf(f109,plain,(
% 1.58/1.32 (sF26 = $true) | (sF25 = $true) | ((f2 @ $false) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f107])).
% 1.58/1.33 thf(f107,plain,(
% 1.58/1.33 ((f2 @ $false) = sF26) | (sF25 = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f32])).
% 1.58/1.33 thf(f648,plain,(
% 1.58/1.33 spl31_12 | spl31_46 | spl31_86),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f108,f644,f434,f276])).
% 1.58/1.33 thf(f108,plain,(
% 1.58/1.33 (sF25 = $true) | ((f2 @ $false) = $true) | (sF26 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f107])).
% 1.58/1.33 thf(f647,plain,(
% 1.58/1.33 spl31_86 | spl31_11 | spl31_42),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f111,f416,f271,f644])).
% 1.58/1.33 thf(f271,definition,(
% 1.58/1.33 spl31_11 <=> (sF25 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_11])],[avatar_definition])).
% 1.58/1.33 thf(f111,plain,(
% 1.58/1.33 (sF25 = $false) | (sF26 = $false) | ((f2 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f106])).
% 1.58/1.33 thf(f106,plain,(
% 1.58/1.33 (sF26 = (f2 @ $true)) | (sF25 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f32])).
% 1.58/1.33 thf(f642,plain,(
% 1.58/1.33 spl31_39 | spl31_85 | spl31_11),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f110,f271,f639,f403])).
% 1.58/1.33 thf(f110,plain,(
% 1.58/1.33 (sF26 = $true) | ((f2 @ $true) = $false) | (sF25 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f106])).
% 1.58/1.33 thf(f637,plain,(
% 1.58/1.33 spl31_36 | spl31_22 | spl31_84),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f115,f633,f323,f386])).
% 1.58/1.33 thf(f323,definition,(
% 1.58/1.33 spl31_22 <=> ($false = sF21)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_22])],[avatar_definition])).
% 1.58/1.33 thf(f115,plain,(
% 1.58/1.33 ($false = sF21) | ($true = sF20) | ($true = (f5 @ $false))),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f113])).
% 1.58/1.33 thf(f113,plain,(
% 1.58/1.33 ($true = sF20) | (sF21 = (f5 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f27])).
% 1.58/1.33 thf(f636,plain,(
% 1.58/1.33 spl31_84 | spl31_26 | spl31_34),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f114,f377,f341,f633])).
% 1.58/1.33 thf(f341,definition,(
% 1.58/1.33 spl31_26 <=> ($true = sF21)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_26])],[avatar_definition])).
% 1.58/1.33 thf(f114,plain,(
% 1.58/1.33 ($false = (f5 @ $false)) | ($true = sF20) | ($true = sF21)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f113])).
% 1.58/1.33 thf(f631,plain,(
% 1.58/1.33 spl31_83 | spl31_26 | spl31_30),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f117,f359,f341,f627])).
% 1.58/1.33 thf(f117,plain,(
% 1.58/1.33 ($true = sF21) | ($false = sF20) | ((f5 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f112])).
% 1.58/1.33 thf(f112,plain,(
% 1.58/1.33 ((f5 @ $true) = sF21) | ($false = sF20)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f27])).
% 1.58/1.33 thf(f630,plain,(
% 1.58/1.33 spl31_83 | spl31_22 | spl31_32),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f116,f368,f323,f627])).
% 1.58/1.33 thf(f116,plain,(
% 1.58/1.33 ((f5 @ $true) = $true) | ($false = sF20) | ($false = sF21)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f112])).
% 1.58/1.33 thf(f625,plain,(
% 1.58/1.33 spl31_78 | spl31_82 | spl31_75),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f121,f587,f622,f603])).
% 1.58/1.33 thf(f587,definition,(
% 1.58/1.33 spl31_75 <=> (sF12 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_75])],[avatar_definition])).
% 1.58/1.33 thf(f121,plain,(
% 1.58/1.33 ((f0 @ $false) = $false) | (sF13 = $true) | (sF12 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f119])).
% 1.58/1.33 thf(f119,plain,(
% 1.58/1.33 ((f0 @ $false) = sF13) | (sF12 = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f19])).
% 1.58/1.33 thf(f620,plain,(
% 1.58/1.33 spl31_79 | spl31_75 | spl31_81),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f120,f617,f587,f608])).
% 1.58/1.33 thf(f120,plain,(
% 1.58/1.33 (sF12 = $true) | (sF13 = $false) | ((f0 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f119])).
% 1.58/1.33 thf(f615,plain,(
% 1.58/1.33 spl31_76 | spl31_79 | spl31_80),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f123,f612,f608,f592])).
% 1.58/1.33 thf(f592,definition,(
% 1.58/1.33 spl31_76 <=> (sF12 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_76])],[avatar_definition])).
% 1.58/1.33 thf(f123,plain,(
% 1.58/1.33 (sF13 = $false) | (sF12 = $false) | ((f0 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f118])).
% 1.58/1.33 thf(f118,plain,(
% 1.58/1.33 (sF12 = $false) | (sF13 = (f0 @ $true))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f19])).
% 1.58/1.33 thf(f606,plain,(
% 1.58/1.33 spl31_77 | spl31_78 | spl31_76),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f122,f592,f603,f599])).
% 1.58/1.33 thf(f122,plain,(
% 1.58/1.33 (sF12 = $false) | ((f0 @ $true) = $false) | (sF13 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f118])).
% 1.58/1.33 thf(f597,plain,(
% 1.58/1.33 spl31_40 | spl31_76 | spl31_53),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f127,f465,f592,f407])).
% 1.58/1.33 thf(f407,definition,(
% 1.58/1.33 spl31_40 <=> (sF11 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_40])],[avatar_definition])).
% 1.58/1.33 thf(f127,plain,(
% 1.58/1.33 (sF12 = $false) | (sF11 = $true) | ((f1 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f125])).
% 1.58/1.33 thf(f125,plain,(
% 1.58/1.33 (sF11 = $true) | (sF12 = (f1 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f18])).
% 1.58/1.33 thf(f596,plain,(
% 1.58/1.33 spl31_75 | spl31_40 | spl31_54),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f126,f470,f407,f587])).
% 1.58/1.33 thf(f126,plain,(
% 1.58/1.33 ((f1 @ $false) = $false) | (sF12 = $true) | (sF11 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f125])).
% 1.58/1.33 thf(f595,plain,(
% 1.58/1.33 spl31_76 | spl31_43 | spl31_49),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f129,f447,f420,f592])).
% 1.58/1.33 thf(f420,definition,(
% 1.58/1.33 spl31_43 <=> (sF11 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_43])],[avatar_definition])).
% 1.58/1.33 thf(f129,plain,(
% 1.58/1.33 (sF11 = $false) | ((f1 @ $true) = $true) | (sF12 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f124])).
% 1.58/1.33 thf(f124,plain,(
% 1.58/1.33 (sF12 = (f1 @ $true)) | (sF11 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f18])).
% 1.58/1.33 thf(f590,plain,(
% 1.58/1.33 spl31_75 | spl31_43 | spl31_50),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f128,f452,f420,f587])).
% 1.58/1.33 thf(f128,plain,(
% 1.58/1.33 (sF11 = $false) | (sF12 = $true) | ((f1 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f124])).
% 1.58/1.33 thf(f585,plain,(
% 1.58/1.33 spl31_53 | spl31_74 | spl31_47),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f133,f439,f581,f465])).
% 1.58/1.33 thf(f439,definition,(
% 1.58/1.33 spl31_47 <=> (sF28 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_47])],[avatar_definition])).
% 1.58/1.33 thf(f133,plain,(
% 1.58/1.33 (sF27 = $true) | (sF28 = $false) | ((f1 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f131])).
% 1.58/1.33 thf(f131,plain,(
% 1.58/1.33 (sF27 = $true) | (sF28 = (f1 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f34])).
% 1.58/1.33 thf(f584,plain,(
% 1.58/1.33 spl31_74 | spl31_52 | spl31_54),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f132,f470,f461,f581])).
% 1.58/1.33 thf(f461,definition,(
% 1.58/1.33 spl31_52 <=> (sF28 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_52])],[avatar_definition])).
% 1.58/1.33 thf(f132,plain,(
% 1.58/1.33 ((f1 @ $false) = $false) | (sF27 = $true) | (sF28 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f131])).
% 1.58/1.33 thf(f579,plain,(
% 1.58/1.33 spl31_49 | spl31_73 | spl31_47),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f135,f439,f575,f447])).
% 1.58/1.33 thf(f135,plain,(
% 1.58/1.33 (sF27 = $false) | (sF28 = $false) | ((f1 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f130])).
% 1.58/1.33 thf(f130,plain,(
% 1.58/1.33 (sF28 = (f1 @ $true)) | (sF27 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f34])).
% 1.58/1.33 thf(f578,plain,(
% 1.58/1.33 spl31_50 | spl31_52 | spl31_73),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f134,f575,f461,f452])).
% 1.58/1.33 thf(f134,plain,(
% 1.58/1.33 ((f1 @ $true) = $false) | (sF28 = $true) | (sF27 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f130])).
% 1.58/1.33 thf(f573,plain,(
% 1.58/1.33 spl31_58 | spl31_37 | spl31_7),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f139,f253,f391,f491])).
% 1.58/1.33 thf(f491,definition,(
% 1.58/1.33 spl31_58 <=> (sF17 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_58])],[avatar_definition])).
% 1.58/1.33 thf(f391,definition,(
% 1.58/1.33 spl31_37 <=> (sF16 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_37])],[avatar_definition])).
% 1.58/1.33 thf(f253,definition,(
% 1.58/1.33 spl31_7 <=> ((f7 @ $false) = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_7])],[avatar_definition])).
% 1.58/1.33 thf(f139,plain,(
% 1.58/1.33 ((f7 @ $false) = $true) | (sF16 = $true) | (sF17 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f137])).
% 1.58/1.33 thf(f137,plain,(
% 1.58/1.33 (sF16 = $true) | (sF17 = (f7 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f23])).
% 1.58/1.33 thf(f572,plain,(
% 1.58/1.33 spl31_37 | spl31_62 | spl31_8),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f138,f258,f509,f391])).
% 1.58/1.33 thf(f509,definition,(
% 1.58/1.33 spl31_62 <=> (sF17 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_62])],[avatar_definition])).
% 1.58/1.33 thf(f258,definition,(
% 1.58/1.33 spl31_8 <=> ((f7 @ $false) = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_8])],[avatar_definition])).
% 1.58/1.33 thf(f138,plain,(
% 1.58/1.33 ((f7 @ $false) = $false) | (sF17 = $true) | (sF16 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f137])).
% 1.58/1.33 thf(f571,plain,(
% 1.58/1.33 spl31_3 | spl31_58 | spl31_38),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f141,f396,f491,f235])).
% 1.58/1.33 thf(f235,definition,(
% 1.58/1.33 spl31_3 <=> ($true = (f7 @ $true))),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_3])],[avatar_definition])).
% 1.58/1.33 thf(f396,definition,(
% 1.58/1.33 spl31_38 <=> (sF16 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_38])],[avatar_definition])).
% 1.58/1.33 thf(f141,plain,(
% 1.58/1.33 ($true = (f7 @ $true)) | (sF16 = $false) | (sF17 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f136])).
% 1.58/1.33 thf(f136,plain,(
% 1.58/1.33 (sF17 = (f7 @ $true)) | (sF16 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f23])).
% 1.58/1.33 thf(f570,plain,(
% 1.58/1.33 spl31_38 | spl31_62 | spl31_4),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f140,f240,f509,f396])).
% 1.58/1.33 thf(f240,definition,(
% 1.58/1.33 spl31_4 <=> ($false = (f7 @ $true))),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_4])],[avatar_definition])).
% 1.58/1.33 thf(f140,plain,(
% 1.58/1.33 ($false = (f7 @ $true)) | (sF16 = $false) | (sF17 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f136])).
% 1.58/1.33 thf(f569,plain,(
% 1.58/1.33 spl31_72 | spl31_44 | spl31_45),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f145,f429,f425,f565])).
% 1.58/1.33 thf(f425,definition,(
% 1.58/1.33 spl31_44 <=> (sF10 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_44])],[avatar_definition])).
% 1.58/1.33 thf(f145,plain,(
% 1.58/1.33 ((f2 @ $false) = $false) | ($true = sF9) | (sF10 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f143])).
% 1.58/1.33 thf(f143,plain,(
% 1.58/1.33 ($true = sF9) | ((f2 @ $false) = sF10)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f16])).
% 1.58/1.33 thf(f568,plain,(
% 1.58/1.33 spl31_46 | spl31_72 | spl31_41),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f144,f411,f565,f434])).
% 1.58/1.33 thf(f411,definition,(
% 1.58/1.33 spl31_41 <=> (sF10 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_41])],[avatar_definition])).
% 1.58/1.33 thf(f144,plain,(
% 1.58/1.33 ($true = sF9) | ((f2 @ $false) = $true) | (sF10 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f143])).
% 1.58/1.33 thf(f563,plain,(
% 1.58/1.33 spl31_42 | spl31_41 | spl31_71),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f147,f559,f411,f416])).
% 1.58/1.33 thf(f147,plain,(
% 1.58/1.33 (sF10 = $false) | ($false = sF9) | ((f2 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f142])).
% 1.58/1.33 thf(f142,plain,(
% 1.58/1.33 (sF10 = (f2 @ $true)) | ($false = sF9)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f16])).
% 1.58/1.33 thf(f562,plain,(
% 1.58/1.33 spl31_44 | spl31_39 | spl31_71),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f146,f559,f403,f425])).
% 1.58/1.33 thf(f146,plain,(
% 1.58/1.33 (sF10 = $true) | ((f2 @ $true) = $false) | ($false = sF9)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f142])).
% 1.58/1.33 thf(f557,plain,(
% 1.58/1.33 spl31_70 | spl31_5 | spl31_64),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f151,f518,f244,f552])).
% 1.58/1.33 thf(f244,definition,(
% 1.58/1.33 spl31_5 <=> ($true = sF0)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_5])],[avatar_definition])).
% 1.58/1.33 thf(f151,plain,(
% 1.58/1.33 ($true = sF0) | (sF1 = $false) | ((f6 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f149])).
% 1.58/1.33 thf(f149,plain,(
% 1.58/1.33 (sF1 = (f6 @ $false)) | ($true = sF0)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f7])).
% 1.58/1.33 thf(f556,plain,(
% 1.58/1.33 spl31_69 | spl31_63 | spl31_5),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f150,f244,f513,f547])).
% 1.58/1.33 thf(f150,plain,(
% 1.58/1.33 (sF1 = $true) | ((f6 @ $false) = $false) | ($true = sF0)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f149])).
% 1.58/1.33 thf(f555,plain,(
% 1.58/1.33 spl31_61 | spl31_70 | spl31_2),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f153,f231,f552,f504])).
% 1.58/1.33 thf(f231,definition,(
% 1.58/1.33 spl31_2 <=> ($false = sF0)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_2])],[avatar_definition])).
% 1.58/1.33 thf(f153,plain,(
% 1.58/1.33 ((f6 @ $true) = $true) | (sF1 = $false) | ($false = sF0)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f148])).
% 1.58/1.33 thf(f148,plain,(
% 1.58/1.33 ($false = sF0) | (sF1 = (f6 @ $true))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f7])).
% 1.58/1.33 thf(f550,plain,(
% 1.58/1.33 spl31_57 | spl31_69 | spl31_2),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f152,f231,f547,f487])).
% 1.58/1.33 thf(f152,plain,(
% 1.58/1.33 ($false = sF0) | (sF1 = $true) | ((f6 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f148])).
% 1.58/1.33 thf(f545,plain,(
% 1.58/1.33 spl31_29 | spl31_64 | spl31_68),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f157,f541,f518,f355])).
% 1.58/1.33 thf(f355,definition,(
% 1.58/1.33 spl31_29 <=> (sF3 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_29])],[avatar_definition])).
% 1.58/1.33 thf(f157,plain,(
% 1.58/1.33 (sF2 = $true) | ((f6 @ $false) = $true) | (sF3 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f155])).
% 1.58/1.33 thf(f155,plain,(
% 1.58/1.33 (sF2 = $true) | (sF3 = (f6 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f9])).
% 1.58/1.33 thf(f544,plain,(
% 1.58/1.33 spl31_63 | spl31_35 | spl31_68),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f156,f541,f381,f513])).
% 1.58/1.33 thf(f381,definition,(
% 1.58/1.33 spl31_35 <=> (sF3 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_35])],[avatar_definition])).
% 1.58/1.33 thf(f156,plain,(
% 1.58/1.33 (sF2 = $true) | (sF3 = $true) | ((f6 @ $false) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f155])).
% 1.58/1.33 thf(f539,plain,(
% 1.58/1.33 spl31_29 | spl31_67 | spl31_61),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f159,f504,f535,f355])).
% 1.58/1.33 thf(f159,plain,(
% 1.58/1.33 (sF2 = $false) | ((f6 @ $true) = $true) | (sF3 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f154])).
% 1.58/1.33 thf(f154,plain,(
% 1.58/1.33 (sF2 = $false) | (sF3 = (f6 @ $true))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f9])).
% 1.58/1.33 thf(f538,plain,(
% 1.58/1.33 spl31_35 | spl31_67 | spl31_57),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f158,f487,f535,f381])).
% 1.58/1.33 thf(f158,plain,(
% 1.58/1.33 (sF2 = $false) | (sF3 = $true) | ((f6 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f154])).
% 1.58/1.33 thf(f533,plain,(
% 1.58/1.33 spl31_28 | spl31_17 | spl31_66),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f163,f529,f299,f350])).
% 1.58/1.33 thf(f299,definition,(
% 1.58/1.33 spl31_17 <=> (sF7 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_17])],[avatar_definition])).
% 1.58/1.33 thf(f163,plain,(
% 1.58/1.33 ($true = (f4 @ $false)) | (sF6 = $true) | (sF7 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f161])).
% 1.58/1.33 thf(f161,plain,(
% 1.58/1.33 (sF6 = $true) | (sF7 = (f4 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f13])).
% 1.58/1.33 thf(f532,plain,(
% 1.58/1.33 spl31_20 | spl31_27 | spl31_66),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f162,f529,f345,f313])).
% 1.58/1.33 thf(f313,definition,(
% 1.58/1.33 spl31_20 <=> (sF7 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_20])],[avatar_definition])).
% 1.58/1.33 thf(f162,plain,(
% 1.58/1.33 (sF7 = $true) | ($false = (f4 @ $false)) | (sF6 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f161])).
% 1.58/1.33 thf(f527,plain,(
% 1.58/1.33 spl31_23 | spl31_65 | spl31_17),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f165,f299,f523,f327])).
% 1.58/1.33 thf(f165,plain,(
% 1.58/1.33 ((f4 @ $true) = $true) | (sF7 = $false) | (sF6 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f160])).
% 1.58/1.33 thf(f160,plain,(
% 1.58/1.33 (sF7 = (f4 @ $true)) | (sF6 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f13])).
% 1.58/1.33 thf(f526,plain,(
% 1.58/1.33 spl31_25 | spl31_65 | spl31_20),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f164,f313,f523,f336])).
% 1.58/1.33 thf(f164,plain,(
% 1.58/1.33 (sF7 = $true) | ((f4 @ $true) = $false) | (sF6 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f160])).
% 1.58/1.33 thf(f521,plain,(
% 1.58/1.33 spl31_62 | spl31_64 | spl31_60),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f169,f500,f518,f509])).
% 1.58/1.33 thf(f169,plain,(
% 1.58/1.33 (sF18 = $false) | ((f6 @ $false) = $true) | (sF17 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f167])).
% 1.58/1.33 thf(f167,plain,(
% 1.58/1.33 (sF17 = $true) | (sF18 = (f6 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f24])).
% 1.58/1.33 thf(f516,plain,(
% 1.58/1.33 spl31_62 | spl31_59 | spl31_63),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f168,f513,f495,f509])).
% 1.58/1.33 thf(f168,plain,(
% 1.58/1.33 ((f6 @ $false) = $false) | (sF18 = $true) | (sF17 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f167])).
% 1.58/1.33 thf(f507,plain,(
% 1.58/1.33 spl31_58 | spl31_60 | spl31_61),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f171,f504,f500,f491])).
% 1.58/1.33 thf(f171,plain,(
% 1.58/1.33 (sF17 = $false) | (sF18 = $false) | ((f6 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f166])).
% 1.58/1.33 thf(f166,plain,(
% 1.58/1.33 (sF17 = $false) | (sF18 = (f6 @ $true))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f24])).
% 1.58/1.33 thf(f498,plain,(
% 1.58/1.33 spl31_57 | spl31_58 | spl31_59),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f170,f495,f491,f487])).
% 1.58/1.33 thf(f170,plain,(
% 1.58/1.33 (sF17 = $false) | (sF18 = $true) | ((f6 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f166])).
% 1.58/1.33 thf(f485,plain,(
% 1.58/1.33 spl31_9 | spl31_16 | spl31_56),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f175,f481,f294,f263])).
% 1.58/1.33 thf(f263,definition,(
% 1.58/1.33 spl31_9 <=> (sF24 = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_9])],[avatar_definition])).
% 1.58/1.33 thf(f175,plain,(
% 1.58/1.33 (sF23 = $true) | ((f3 @ $false) = $true) | (sF24 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f173])).
% 1.58/1.33 thf(f173,plain,(
% 1.58/1.33 (sF24 = (f3 @ $false)) | (sF23 = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f30])).
% 1.58/1.33 thf(f484,plain,(
% 1.58/1.33 spl31_15 | spl31_56 | spl31_14),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f174,f285,f481,f289])).
% 1.58/1.33 thf(f289,definition,(
% 1.58/1.33 spl31_15 <=> (sF24 = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_15])],[avatar_definition])).
% 1.58/1.33 thf(f174,plain,(
% 1.58/1.33 (sF23 = $true) | ((f3 @ $false) = $false) | (sF24 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f173])).
% 1.58/1.33 thf(f479,plain,(
% 1.58/1.33 spl31_55 | spl31_13 | spl31_15),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f177,f289,f280,f475])).
% 1.58/1.33 thf(f177,plain,(
% 1.58/1.33 ((f3 @ $true) = $false) | (sF24 = $true) | (sF23 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f172])).
% 1.58/1.33 thf(f172,plain,(
% 1.58/1.33 ((f3 @ $true) = sF24) | (sF23 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f30])).
% 1.58/1.33 thf(f478,plain,(
% 1.58/1.33 spl31_10 | spl31_55 | spl31_9),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f176,f263,f475,f267])).
% 1.58/1.33 thf(f176,plain,(
% 1.58/1.33 (sF24 = $false) | (sF23 = $false) | ((f3 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f172])).
% 1.58/1.33 thf(f473,plain,(
% 1.58/1.33 spl31_51 | spl31_54 | spl31_52),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f181,f461,f470,f456])).
% 1.58/1.33 thf(f181,plain,(
% 1.58/1.33 ((f1 @ $false) = $false) | ($true = sF29) | (sF28 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f179])).
% 1.58/1.33 thf(f179,plain,(
% 1.58/1.33 (sF28 = $true) | ((f1 @ $false) = sF29)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f35])).
% 1.58/1.33 thf(f468,plain,(
% 1.58/1.33 spl31_52 | spl31_48 | spl31_53),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f180,f465,f443,f461])).
% 1.58/1.33 thf(f180,plain,(
% 1.58/1.33 (sF28 = $true) | ($false = sF29) | ((f1 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f179])).
% 1.58/1.33 thf(f459,plain,(
% 1.58/1.33 spl31_50 | spl31_47 | spl31_51),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f183,f456,f439,f452])).
% 1.58/1.33 thf(f183,plain,(
% 1.58/1.33 (sF28 = $false) | ((f1 @ $true) = $false) | ($true = sF29)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f178])).
% 1.58/1.33 thf(f178,plain,(
% 1.58/1.33 (sF28 = $false) | ((f1 @ $true) = sF29)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f35])).
% 1.58/1.33 thf(f450,plain,(
% 1.58/1.33 spl31_47 | spl31_48 | spl31_49),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f182,f447,f443,f439])).
% 1.58/1.33 thf(f182,plain,(
% 1.58/1.33 ((f1 @ $true) = $true) | ($false = sF29) | (sF28 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f178])).
% 1.58/1.33 thf(f437,plain,(
% 1.58/1.33 spl31_46 | spl31_44 | spl31_43),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f187,f420,f425,f434])).
% 1.58/1.33 thf(f187,plain,(
% 1.58/1.33 ((f2 @ $false) = $true) | (sF11 = $false) | (sF10 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f185])).
% 1.58/1.33 thf(f185,plain,(
% 1.58/1.33 (sF10 = $true) | (sF11 = (f2 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f17])).
% 1.58/1.33 thf(f432,plain,(
% 1.58/1.33 spl31_44 | spl31_40 | spl31_45),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f186,f429,f407,f425])).
% 1.58/1.33 thf(f186,plain,(
% 1.58/1.33 (sF10 = $true) | ((f2 @ $false) = $false) | (sF11 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f185])).
% 1.58/1.33 thf(f423,plain,(
% 1.58/1.33 spl31_42 | spl31_43 | spl31_41),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f189,f411,f420,f416])).
% 1.58/1.33 thf(f189,plain,(
% 1.58/1.33 (sF10 = $false) | ((f2 @ $true) = $true) | (sF11 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f184])).
% 1.58/1.33 thf(f184,plain,(
% 1.58/1.33 (sF11 = (f2 @ $true)) | (sF10 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f17])).
% 1.58/1.33 thf(f414,plain,(
% 1.58/1.33 spl31_39 | spl31_40 | spl31_41),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f188,f411,f407,f403])).
% 1.58/1.33 thf(f188,plain,(
% 1.58/1.33 (sF10 = $false) | (sF11 = $true) | ((f2 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f184])).
% 1.58/1.33 thf(f401,plain,(
% 1.58/1.33 spl31_5 | spl31_38 | spl31_7),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f193,f253,f396,f244])).
% 1.58/1.33 thf(f193,plain,(
% 1.58/1.33 (sF16 = $false) | ($true = sF0) | ((f7 @ $false) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f191])).
% 1.58/1.33 thf(f191,plain,(
% 1.58/1.33 (sF16 = (f7 @ $false)) | ($true = sF0)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f22])).
% 1.58/1.33 thf(f400,plain,(
% 1.58/1.33 spl31_5 | spl31_37 | spl31_8),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f192,f258,f391,f244])).
% 1.58/1.33 thf(f192,plain,(
% 1.58/1.33 ((f7 @ $false) = $false) | ($true = sF0) | (sF16 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f191])).
% 1.58/1.33 thf(f399,plain,(
% 1.58/1.33 spl31_2 | spl31_38 | spl31_3),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f195,f235,f396,f231])).
% 1.58/1.33 thf(f195,plain,(
% 1.58/1.33 (sF16 = $false) | ($false = sF0) | ($true = (f7 @ $true))),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f190])).
% 1.58/1.33 thf(f190,plain,(
% 1.58/1.33 (sF16 = (f7 @ $true)) | ($false = sF0)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f22])).
% 1.58/1.33 thf(f394,plain,(
% 1.58/1.33 spl31_2 | spl31_4 | spl31_37),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f194,f391,f240,f231])).
% 1.58/1.33 thf(f194,plain,(
% 1.58/1.33 ($false = sF0) | (sF16 = $true) | ($false = (f7 @ $true))),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f190])).
% 1.58/1.33 thf(f389,plain,(
% 1.58/1.33 spl31_35 | spl31_36 | spl31_33),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f199,f372,f386,f381])).
% 1.58/1.33 thf(f199,plain,(
% 1.58/1.33 (sF4 = $false) | (sF3 = $true) | ($true = (f5 @ $false))),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f197])).
% 1.58/1.33 thf(f197,plain,(
% 1.58/1.33 (sF3 = $true) | (sF4 = (f5 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f10])).
% 1.58/1.33 thf(f384,plain,(
% 1.58/1.33 spl31_34 | spl31_31 | spl31_35),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f198,f381,f363,f377])).
% 1.58/1.33 thf(f198,plain,(
% 1.58/1.33 ($false = (f5 @ $false)) | (sF3 = $true) | (sF4 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f197])).
% 1.58/1.33 thf(f375,plain,(
% 1.58/1.33 spl31_32 | spl31_29 | spl31_33),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f201,f372,f355,f368])).
% 1.58/1.33 thf(f201,plain,(
% 1.58/1.33 (sF3 = $false) | (sF4 = $false) | ((f5 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f196])).
% 1.58/1.33 thf(f196,plain,(
% 1.58/1.33 (sF3 = $false) | (sF4 = (f5 @ $true))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f10])).
% 1.58/1.33 thf(f366,plain,(
% 1.58/1.33 spl31_29 | spl31_30 | spl31_31),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f200,f363,f359,f355])).
% 1.58/1.33 thf(f200,plain,(
% 1.58/1.33 (sF3 = $false) | ((f5 @ $true) = $false) | (sF4 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f196])).
% 1.58/1.33 thf(f353,plain,(
% 1.58/1.33 spl31_28 | spl31_26 | spl31_21),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f205,f319,f341,f350])).
% 1.58/1.33 thf(f205,plain,(
% 1.58/1.33 ($false = sF22) | ($true = (f4 @ $false)) | ($true = sF21)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f203])).
% 1.58/1.33 thf(f203,plain,(
% 1.58/1.33 ($true = sF21) | (sF22 = (f4 @ $false))),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f28])).
% 1.58/1.33 thf(f348,plain,(
% 1.58/1.33 spl31_24 | spl31_26 | spl31_27),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f204,f345,f341,f332])).
% 1.58/1.33 thf(f204,plain,(
% 1.58/1.33 ($false = (f4 @ $false)) | ($true = sF22) | ($true = sF21)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f203])).
% 1.58/1.33 thf(f339,plain,(
% 1.58/1.33 spl31_22 | spl31_24 | spl31_25),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f207,f336,f332,f323])).
% 1.58/1.33 thf(f207,plain,(
% 1.58/1.33 ($false = sF21) | ((f4 @ $true) = $false) | ($true = sF22)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f202])).
% 1.58/1.33 thf(f202,plain,(
% 1.58/1.33 ($false = sF21) | ((f4 @ $true) = sF22)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f28])).
% 1.58/1.33 thf(f330,plain,(
% 1.58/1.33 spl31_21 | spl31_22 | spl31_23),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f206,f327,f323,f319])).
% 1.58/1.33 thf(f206,plain,(
% 1.58/1.33 ($false = sF22) | ($false = sF21) | ((f4 @ $true) = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f202])).
% 1.58/1.33 thf(f317,plain,(
% 1.58/1.33 spl31_16 | spl31_18 | spl31_20),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f211,f313,f303,f294])).
% 1.58/1.33 thf(f211,plain,(
% 1.58/1.33 ((f3 @ $false) = $true) | (sF7 = $true) | (sF8 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f209])).
% 1.58/1.33 thf(f209,plain,(
% 1.58/1.33 (sF8 = (f3 @ $false)) | (sF7 = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f14])).
% 1.58/1.33 thf(f316,plain,(
% 1.58/1.33 spl31_14 | spl31_19 | spl31_20),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f210,f313,f308,f285])).
% 1.58/1.33 thf(f210,plain,(
% 1.58/1.33 (sF8 = $true) | ((f3 @ $false) = $false) | (sF7 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f209])).
% 1.58/1.33 thf(f311,plain,(
% 1.58/1.33 spl31_19 | spl31_17 | spl31_13),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f213,f280,f299,f308])).
% 1.58/1.33 thf(f213,plain,(
% 1.58/1.33 (sF7 = $false) | ((f3 @ $true) = $false) | (sF8 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f208])).
% 1.58/1.33 thf(f208,plain,(
% 1.58/1.33 ((f3 @ $true) = sF8) | (sF7 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f14])).
% 1.58/1.33 thf(f306,plain,(
% 1.58/1.33 spl31_10 | spl31_17 | spl31_18),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f212,f303,f299,f267])).
% 1.58/1.33 thf(f212,plain,(
% 1.58/1.33 (sF8 = $false) | ((f3 @ $true) = $true) | (sF7 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f208])).
% 1.58/1.33 thf(f297,plain,(
% 1.58/1.33 spl31_11 | spl31_15 | spl31_16),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f217,f294,f289,f271])).
% 1.58/1.33 thf(f217,plain,(
% 1.58/1.33 ((f3 @ $false) = $true) | (sF25 = $false) | (sF24 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f215])).
% 1.58/1.33 thf(f215,plain,(
% 1.58/1.33 (sF25 = (f3 @ $false)) | (sF24 = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f31])).
% 1.58/1.33 thf(f292,plain,(
% 1.58/1.33 spl31_14 | spl31_12 | spl31_15),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f216,f289,f276,f285])).
% 1.58/1.33 thf(f216,plain,(
% 1.58/1.33 ((f3 @ $false) = $false) | (sF25 = $true) | (sF24 = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f215])).
% 1.58/1.33 thf(f283,plain,(
% 1.58/1.33 spl31_9 | spl31_12 | spl31_13),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f219,f280,f276,f263])).
% 1.58/1.33 thf(f219,plain,(
% 1.58/1.33 (sF24 = $false) | (sF25 = $true) | ((f3 @ $true) = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f214])).
% 1.58/1.33 thf(f214,plain,(
% 1.58/1.33 ((f3 @ $true) = sF25) | (sF24 = $false)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f31])).
% 1.58/1.33 thf(f274,plain,(
% 1.58/1.33 spl31_9 | spl31_10 | spl31_11),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f218,f271,f267,f263])).
% 1.58/1.33 thf(f218,plain,(
% 1.58/1.33 (sF24 = $false) | ((f3 @ $true) = $true) | (sF25 = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f214])).
% 1.58/1.33 thf(f261,plain,(
% 1.58/1.33 spl31_6 | spl31_8 | spl31_5),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f223,f244,f258,f249])).
% 1.58/1.33 thf(f249,definition,(
% 1.58/1.33 spl31_6 <=> (x = $true)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_6])],[avatar_definition])).
% 1.58/1.33 thf(f223,plain,(
% 1.58/1.33 ((f7 @ $false) = $false) | (x = $true) | ($true = sF0)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f221])).
% 1.58/1.33 thf(f221,plain,(
% 1.58/1.33 ((f7 @ $false) = sF0) | (x = $true)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f6])).
% 1.58/1.33 thf(f256,plain,(
% 1.58/1.33 spl31_6 | spl31_2 | spl31_7),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f222,f253,f231,f249])).
% 1.58/1.33 thf(f222,plain,(
% 1.58/1.33 ((f7 @ $false) = $true) | ($false = sF0) | (x = $true)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f221])).
% 1.58/1.33 thf(f247,plain,(
% 1.58/1.33 spl31_4 | spl31_5 | spl31_1),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f225,f227,f244,f240])).
% 1.58/1.33 thf(f227,definition,(
% 1.58/1.33 spl31_1 <=> (x = $false)),
% 1.58/1.33 introduced(definition,[new_symbols(naming,[spl31_1])],[avatar_definition])).
% 1.58/1.33 thf(f225,plain,(
% 1.58/1.33 ($true = sF0) | ($false = (f7 @ $true)) | (x = $false)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f220])).
% 1.58/1.33 thf(f220,plain,(
% 1.58/1.33 (x = $false) | ((f7 @ $true) = sF0)),
% 1.58/1.33 inference(cases_simplifying,[status(thm)],[f6])).
% 1.58/1.33 thf(f238,plain,(
% 1.58/1.33 spl31_1 | spl31_2 | spl31_3),
% 1.58/1.33 inference(avatar_split_clause,[status(thm)],[f224,f235,f231,f227])).
% 1.58/1.33 thf(f224,plain,(
% 1.58/1.33 (x = $false) | ($true = (f7 @ $true)) | ($false = sF0)),
% 1.58/1.33 inference(binary_proxy_clausification,[status(thm)],[f220])).
% 1.58/1.33 % SZS output end Proof for DTF2THF_18236
% 1.58/1.33 % (18577)------------------------------
% 1.58/1.33 % (18577)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.58/1.33 % (18577)Termination reason: Refutation
% 1.58/1.33
% 1.58/1.33 % (18577)Memory used [KB]: 6012
% 1.58/1.33 % (18577)Time elapsed: 0.017 s
% 1.58/1.33 % (18577)Instructions burned: 15 (million)
% 1.58/1.33 % (18577)------------------------------
% 1.58/1.33 % (18577)------------------------------
% 1.58/1.33 % (18563)Success in time 0.054 s
%------------------------------------------------------------------------------