%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SYO505^1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n022.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:24 AM UTC 2026
% Result : Theorem 1.80s 1.57s
% Output : Refutation 1.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 83
% Syntax : Number of formulae : 421 ( 41 unt; 0 typ; 63 def)
% Number of atoms : 2264 ( 464 equ; 0 cnn)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 1393 ( 338 ~; 624 |; 0 &; 368 @)
% ( 63 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 104 ( 101 usr; 77 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_0,type,
a: $o > $o ).
thf(func_def_1,type,
b: $o > $o ).
thf(func_def_2,type,
c: $o > $o ).
thf(func_def_3,type,
d: $o > $o ).
thf(func_def_4,type,
e: $o > $o ).
thf(func_def_5,type,
f0: ( $o > $o ) > $i ).
thf(func_def_6,type,
g0: ( $o > $o ) > $i ).
thf(func_def_7,type,
f1: ( $o > $o ) > $i ).
thf(func_def_8,type,
g1: ( $o > $o ) > $i ).
thf(func_def_9,type,
f2: ( $o > $o ) > $i ).
thf(func_def_10,type,
g2: ( $o > $o ) > $i ).
thf(func_def_11,type,
f3: ( $o > $o ) > $i ).
thf(func_def_12,type,
g3: ( $o > $o ) > $i ).
thf(func_def_13,type,
f4: ( $o > $o ) > $i ).
thf(func_def_14,type,
g4: ( $o > $o ) > $i ).
thf(func_def_15,type,
f5: ( $o > $o ) > $i ).
thf(func_def_16,type,
g5: ( $o > $o ) > $i ).
thf(func_def_17,type,
f6: ( $o > $o ) > $i ).
thf(func_def_18,type,
g6: ( $o > $o ) > $i ).
thf(func_def_19,type,
f7: ( $o > $o ) > $i ).
thf(func_def_20,type,
g7: ( $o > $o ) > $i ).
thf(func_def_21,type,
f8: ( $o > $o ) > $i ).
thf(func_def_22,type,
g8: ( $o > $o ) > $i ).
thf(func_def_23,type,
f9: ( $o > $o ) > $i ).
thf(func_def_24,type,
g9: ( $o > $o ) > $i ).
thf(func_def_29,type,
ph1:
!>[X0: $tType] : X0 ).
thf(f558,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f52,f76,f93,f101,f109,f117,f125,f162,f170,f181,f182,f186,f195,f203,f206,f214,f257,f270,f274,f275,f278,f280,f291,f292,f296,f297,f299,f312,f316,f317,f318,f319,f322,f324,f335,f336,f340,f341,f343,f356,f360,f361,f363,f374,f375,f379,f380,f382,f395,f399,f400,f403,f404,f407,f411,f413,f426,f430,f431,f433,f444,f445,f449,f450,f457,f460,f465,f471,f476,f478,f500,f503,f509,f514,f517,f520,f523,f526,f529,f532,f535,f538,f541,f544,f545,f547,f549,f553,f554,f557]) ).
thf(f557,plain,
( spl0_5
| spl0_21
| spl0_19
| ~ spl0_58 ),
inference(avatar_split_clause,[status(thm)],[f556,f358,f120,f134,f67]) ).
thf(f67,definition,
( spl0_5
<=> ( $true
= ( a @ $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition]) ).
thf(f134,definition,
( spl0_21
<=> ( $true
= ( e @ $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_21])],[avatar_definition]) ).
thf(f120,definition,
( spl0_19
<=> ( a = e ) ),
introduced(definition,[new_symbols(naming,[spl0_19])],[avatar_definition]) ).
thf(f358,definition,
( spl0_58
<=> ( $true = sK10 ) ),
introduced(definition,[new_symbols(naming,[spl0_58])],[avatar_definition]) ).
thf(f556,plain,
( ( $true
= ( a @ $true ) )
| ( $true
= ( e @ $true ) )
| spl0_19
| ~ spl0_58 ),
inference(trivial_inequality_removal,[status(thm)],[f555]) ).
thf(f555,plain,
( ( $true
= ( a @ $true ) )
| ( $true
= ( e @ $true ) )
| ( $true = $false )
| spl0_19
| ~ spl0_58 ),
inference(forward_demodulation,[status(thm)],[f349,f359]) ).
thf(f359,plain,
( ( $true = sK10 )
| ~ spl0_58 ),
inference(avatar_component_clause,[status(thm)],[f358]) ).
thf(f349,plain,
( ( $true
= ( a @ $true ) )
| ( sK10 = $false )
| ( $true
= ( e @ $true ) )
| spl0_19 ),
inference(binary_proxy_clausification,[status(thm)],[f345]) ).
thf(f345,plain,
( ( sK10 = $false )
| ( ( e @ $true )
!= ( a @ $true ) )
| spl0_19 ),
inference(cases_simplifying,[status(thm)],[f344]) ).
thf(f344,plain,
( ( ( a @ sK10 )
!= ( e @ sK10 ) )
| spl0_19 ),
inference(negative_extensionality,[status(thm)],[f121]) ).
thf(f121,plain,
( ( a != e )
| spl0_19 ),
inference(avatar_component_clause,[status(thm)],[f120]) ).
thf(f554,plain,
( spl0_67
| spl0_21
| spl0_3
| spl0_27 ),
inference(avatar_split_clause,[status(thm)],[f484,f157,f61,f134,f489]) ).
thf(f489,definition,
( spl0_67
<=> ( sK15 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_67])],[avatar_definition]) ).
thf(f61,definition,
( spl0_3
<=> ( ( d @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition]) ).
thf(f157,definition,
( spl0_27
<=> ( d = e ) ),
introduced(definition,[new_symbols(naming,[spl0_27])],[avatar_definition]) ).
thf(f484,plain,
( ( $true
= ( e @ $true ) )
| ( ( d @ $true )
= $true )
| ( sK15 = $false )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f480]) ).
thf(f480,plain,
( ( ( d @ $true )
!= ( e @ $true ) )
| ( sK15 = $false )
| spl0_27 ),
inference(cases_simplifying,[status(thm)],[f479]) ).
thf(f479,plain,
( ( ( d @ sK15 )
!= ( e @ sK15 ) )
| spl0_27 ),
inference(negative_extensionality,[status(thm)],[f158]) ).
thf(f158,plain,
( ( d != e )
| spl0_27 ),
inference(avatar_component_clause,[status(thm)],[f157]) ).
thf(f553,plain,
( spl0_23
| spl0_7
| spl0_19
| ~ spl0_58 ),
inference(avatar_split_clause,[status(thm)],[f552,f358,f120,f74,f141]) ).
thf(f141,definition,
( spl0_23
<=> ( ( e @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_23])],[avatar_definition]) ).
thf(f74,definition,
( spl0_7
<=> ( ( a @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_7])],[avatar_definition]) ).
thf(f552,plain,
( ( ( e @ $true )
= $false )
| ( ( a @ $true )
= $false )
| spl0_19
| ~ spl0_58 ),
inference(trivial_inequality_removal,[status(thm)],[f551]) ).
thf(f551,plain,
( ( $true = $false )
| ( ( a @ $true )
= $false )
| ( ( e @ $true )
= $false )
| spl0_19
| ~ spl0_58 ),
inference(forward_demodulation,[status(thm)],[f350,f359]) ).
thf(f350,plain,
( ( ( e @ $true )
= $false )
| ( sK10 = $false )
| ( ( a @ $true )
= $false )
| spl0_19 ),
inference(binary_proxy_clausification,[status(thm)],[f345]) ).
thf(f549,plain,
( spl0_43
| spl0_7
| spl0_63
| spl0_36 ),
inference(avatar_split_clause,[status(thm)],[f420,f201,f424,f74,f236]) ).
thf(f236,definition,
( spl0_43
<=> ( ( c @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_43])],[avatar_definition]) ).
thf(f424,definition,
( spl0_63
<=> ( sK13 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_63])],[avatar_definition]) ).
thf(f201,definition,
( spl0_36
<=> ( a = c ) ),
introduced(definition,[new_symbols(naming,[spl0_36])],[avatar_definition]) ).
thf(f420,plain,
( ( sK13 = $false )
| ( ( c @ $true )
= $false )
| ( ( a @ $true )
= $false )
| spl0_36 ),
inference(binary_proxy_clausification,[status(thm)],[f415]) ).
thf(f415,plain,
( ( sK13 = $false )
| ( ( c @ $true )
!= ( a @ $true ) )
| spl0_36 ),
inference(cases_simplifying,[status(thm)],[f414]) ).
thf(f414,plain,
( ( ( a @ sK13 )
!= ( c @ sK13 ) )
| spl0_36 ),
inference(negative_extensionality,[status(thm)],[f202]) ).
thf(f202,plain,
( ( a != c )
| spl0_36 ),
inference(avatar_component_clause,[status(thm)],[f201]) ).
thf(f547,plain,
( spl0_6
| spl0_7
| spl0_49
| spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f264,f47,f268,f74,f71]) ).
thf(f71,definition,
( spl0_6
<=> ( ( d @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition]) ).
thf(f268,definition,
( spl0_49
<=> ( sK6 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_49])],[avatar_definition]) ).
thf(f47,definition,
( spl0_1
<=> ( a = d ) ),
introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition]) ).
thf(f264,plain,
( ( sK6 = $false )
| ( ( d @ $true )
= $false )
| ( ( a @ $true )
= $false )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f259]) ).
thf(f259,plain,
( ( sK6 = $false )
| ( ( d @ $true )
!= ( a @ $true ) )
| spl0_1 ),
inference(cases_simplifying,[status(thm)],[f258]) ).
thf(f258,plain,
( ( ( a @ sK6 )
!= ( d @ sK6 ) )
| spl0_1 ),
inference(negative_extensionality,[status(thm)],[f48]) ).
thf(f48,plain,
( ( a != d )
| spl0_1 ),
inference(avatar_component_clause,[status(thm)],[f47]) ).
thf(f545,plain,
( spl0_6
| spl0_67
| spl0_23
| spl0_27 ),
inference(avatar_split_clause,[status(thm)],[f485,f157,f141,f489,f71]) ).
thf(f485,plain,
( ( ( d @ $true )
= $false )
| ( ( e @ $true )
= $false )
| ( sK15 = $false )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f480]) ).
thf(f544,plain,
( ~ spl0_31
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[status(thm)],[f543]) ).
thf(f543,plain,
( $false
| ~ spl0_31
| ~ spl0_32 ),
inference(trivial_inequality_removal,[status(thm)],[f542]) ).
thf(f542,plain,
( ( $true = $false )
| ~ spl0_31
| ~ spl0_32 ),
inference(forward_demodulation,[status(thm)],[f185,f180]) ).
thf(f180,plain,
( ( sK4 = $false )
| ~ spl0_31 ),
inference(avatar_component_clause,[status(thm)],[f179]) ).
thf(f179,definition,
( spl0_31
<=> ( sK4 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_31])],[avatar_definition]) ).
thf(f185,plain,
( ( sK4 = $true )
| ~ spl0_32 ),
inference(avatar_component_clause,[status(thm)],[f184]) ).
thf(f184,definition,
( spl0_32
<=> ( sK4 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_32])],[avatar_definition]) ).
thf(f541,plain,
( spl0_26
| spl0_11
| spl0_27
| ~ spl0_67 ),
inference(avatar_split_clause,[status(thm)],[f540,f489,f157,f88,f152]) ).
thf(f152,definition,
( spl0_26
<=> ( ( e @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_26])],[avatar_definition]) ).
thf(f88,definition,
( spl0_11
<=> ( ( d @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_11])],[avatar_definition]) ).
thf(f540,plain,
( ( ( e @ $false )
= $false )
| ( ( d @ $false )
= $false )
| spl0_27
| ~ spl0_67 ),
inference(trivial_inequality_removal,[status(thm)],[f539]) ).
thf(f539,plain,
( ( ( d @ $false )
= $false )
| ( ( e @ $false )
= $false )
| ( $true = $false )
| spl0_27
| ~ spl0_67 ),
inference(forward_demodulation,[status(thm)],[f483,f490]) ).
thf(f490,plain,
( ( sK15 = $false )
| ~ spl0_67 ),
inference(avatar_component_clause,[status(thm)],[f489]) ).
thf(f483,plain,
( ( $true = sK15 )
| ( ( d @ $false )
= $false )
| ( ( e @ $false )
= $false )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f481]) ).
thf(f481,plain,
( ( $true = sK15 )
| ( ( d @ $false )
!= ( e @ $false ) )
| spl0_27 ),
inference(cases_simplifying,[status(thm)],[f479]) ).
thf(f538,plain,
( ~ spl0_49
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[status(thm)],[f537]) ).
thf(f537,plain,
( $false
| ~ spl0_49
| ~ spl0_50 ),
inference(trivial_inequality_removal,[status(thm)],[f536]) ).
thf(f536,plain,
( ( $true = $false )
| ~ spl0_49
| ~ spl0_50 ),
inference(forward_demodulation,[status(thm)],[f273,f269]) ).
thf(f269,plain,
( ( sK6 = $false )
| ~ spl0_49 ),
inference(avatar_component_clause,[status(thm)],[f268]) ).
thf(f273,plain,
( ( sK6 = $true )
| ~ spl0_50 ),
inference(avatar_component_clause,[status(thm)],[f272]) ).
thf(f272,definition,
( spl0_50
<=> ( sK6 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_50])],[avatar_definition]) ).
thf(f535,plain,
( ~ spl0_55
| ~ spl0_56 ),
inference(avatar_contradiction_clause,[status(thm)],[f534]) ).
thf(f534,plain,
( $false
| ~ spl0_55
| ~ spl0_56 ),
inference(trivial_inequality_removal,[status(thm)],[f533]) ).
thf(f533,plain,
( ( $true = $false )
| ~ spl0_55
| ~ spl0_56 ),
inference(backward_demodulation,[status(thm)],[f339,f334]) ).
thf(f334,plain,
( ( sK9 = $false )
| ~ spl0_55 ),
inference(avatar_component_clause,[status(thm)],[f333]) ).
thf(f333,definition,
( spl0_55
<=> ( sK9 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_55])],[avatar_definition]) ).
thf(f339,plain,
( ( $true = sK9 )
| ~ spl0_56 ),
inference(avatar_component_clause,[status(thm)],[f338]) ).
thf(f338,definition,
( spl0_56
<=> ( $true = sK9 ) ),
introduced(definition,[new_symbols(naming,[spl0_56])],[avatar_definition]) ).
thf(f532,plain,
( ~ spl0_51
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[status(thm)],[f531]) ).
thf(f531,plain,
( $false
| ~ spl0_51
| ~ spl0_52 ),
inference(trivial_inequality_removal,[status(thm)],[f530]) ).
thf(f530,plain,
( ( $true = $false )
| ~ spl0_51
| ~ spl0_52 ),
inference(forward_demodulation,[status(thm)],[f295,f290]) ).
thf(f290,plain,
( ( sK7 = $false )
| ~ spl0_51 ),
inference(avatar_component_clause,[status(thm)],[f289]) ).
thf(f289,definition,
( spl0_51
<=> ( sK7 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_51])],[avatar_definition]) ).
thf(f295,plain,
( ( $true = sK7 )
| ~ spl0_52 ),
inference(avatar_component_clause,[status(thm)],[f294]) ).
thf(f294,definition,
( spl0_52
<=> ( $true = sK7 ) ),
introduced(definition,[new_symbols(naming,[spl0_52])],[avatar_definition]) ).
thf(f529,plain,
( ~ spl0_53
| ~ spl0_54 ),
inference(avatar_contradiction_clause,[status(thm)],[f528]) ).
thf(f528,plain,
( $false
| ~ spl0_53
| ~ spl0_54 ),
inference(trivial_inequality_removal,[status(thm)],[f527]) ).
thf(f527,plain,
( ( $true = $false )
| ~ spl0_53
| ~ spl0_54 ),
inference(backward_demodulation,[status(thm)],[f315,f311]) ).
thf(f311,plain,
( ( sK8 = $false )
| ~ spl0_53 ),
inference(avatar_component_clause,[status(thm)],[f310]) ).
thf(f310,definition,
( spl0_53
<=> ( sK8 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_53])],[avatar_definition]) ).
thf(f315,plain,
( ( sK8 = $true )
| ~ spl0_54 ),
inference(avatar_component_clause,[status(thm)],[f314]) ).
thf(f314,definition,
( spl0_54
<=> ( sK8 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_54])],[avatar_definition]) ).
thf(f526,plain,
( ~ spl0_61
| ~ spl0_62 ),
inference(avatar_contradiction_clause,[status(thm)],[f525]) ).
thf(f525,plain,
( $false
| ~ spl0_61
| ~ spl0_62 ),
inference(trivial_inequality_removal,[status(thm)],[f524]) ).
thf(f524,plain,
( ( $true = $false )
| ~ spl0_61
| ~ spl0_62 ),
inference(backward_demodulation,[status(thm)],[f398,f394]) ).
thf(f394,plain,
( ( sK12 = $false )
| ~ spl0_61 ),
inference(avatar_component_clause,[status(thm)],[f393]) ).
thf(f393,definition,
( spl0_61
<=> ( sK12 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_61])],[avatar_definition]) ).
thf(f398,plain,
( ( sK12 = $true )
| ~ spl0_62 ),
inference(avatar_component_clause,[status(thm)],[f397]) ).
thf(f397,definition,
( spl0_62
<=> ( sK12 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_62])],[avatar_definition]) ).
thf(f523,plain,
( ~ spl0_63
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[status(thm)],[f522]) ).
thf(f522,plain,
( $false
| ~ spl0_63
| ~ spl0_64 ),
inference(trivial_inequality_removal,[status(thm)],[f521]) ).
thf(f521,plain,
( ( $true = $false )
| ~ spl0_63
| ~ spl0_64 ),
inference(forward_demodulation,[status(thm)],[f429,f425]) ).
thf(f425,plain,
( ( sK13 = $false )
| ~ spl0_63 ),
inference(avatar_component_clause,[status(thm)],[f424]) ).
thf(f429,plain,
( ( sK13 = $true )
| ~ spl0_64 ),
inference(avatar_component_clause,[status(thm)],[f428]) ).
thf(f428,definition,
( spl0_64
<=> ( sK13 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_64])],[avatar_definition]) ).
thf(f520,plain,
( ~ spl0_44
| ~ spl0_47 ),
inference(avatar_contradiction_clause,[status(thm)],[f519]) ).
thf(f519,plain,
( $false
| ~ spl0_44
| ~ spl0_47 ),
inference(trivial_inequality_removal,[status(thm)],[f518]) ).
thf(f518,plain,
( ( $true = $false )
| ~ spl0_44
| ~ spl0_47 ),
inference(forward_demodulation,[status(thm)],[f241,f251]) ).
thf(f251,plain,
( ( ( c @ $false )
= $false )
| ~ spl0_47 ),
inference(avatar_component_clause,[status(thm)],[f250]) ).
thf(f250,definition,
( spl0_47
<=> ( ( c @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_47])],[avatar_definition]) ).
thf(f241,plain,
( ( ( c @ $false )
= $true )
| ~ spl0_44 ),
inference(avatar_component_clause,[status(thm)],[f240]) ).
thf(f240,definition,
( spl0_44
<=> ( ( c @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_44])],[avatar_definition]) ).
thf(f517,plain,
( ~ spl0_59
| ~ spl0_60 ),
inference(avatar_contradiction_clause,[status(thm)],[f516]) ).
thf(f516,plain,
( $false
| ~ spl0_59
| ~ spl0_60 ),
inference(trivial_inequality_removal,[status(thm)],[f515]) ).
thf(f515,plain,
( ( $true = $false )
| ~ spl0_59
| ~ spl0_60 ),
inference(backward_demodulation,[status(thm)],[f378,f373]) ).
thf(f373,plain,
( ( sK11 = $false )
| ~ spl0_59 ),
inference(avatar_component_clause,[status(thm)],[f372]) ).
thf(f372,definition,
( spl0_59
<=> ( sK11 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_59])],[avatar_definition]) ).
thf(f378,plain,
( ( sK11 = $true )
| ~ spl0_60 ),
inference(avatar_component_clause,[status(thm)],[f377]) ).
thf(f377,definition,
( spl0_60
<=> ( sK11 = $true ) ),
introduced(definition,[new_symbols(naming,[spl0_60])],[avatar_definition]) ).
thf(f514,plain,
( ~ spl0_45
| ~ spl0_48 ),
inference(avatar_contradiction_clause,[status(thm)],[f513]) ).
thf(f513,plain,
( $false
| ~ spl0_45
| ~ spl0_48 ),
inference(trivial_inequality_removal,[status(thm)],[f512]) ).
thf(f512,plain,
( ( $true = $false )
| ~ spl0_45
| ~ spl0_48 ),
inference(backward_demodulation,[status(thm)],[f244,f254]) ).
thf(f254,plain,
( ( ( b @ $false )
= $false )
| ~ spl0_48 ),
inference(avatar_component_clause,[status(thm)],[f253]) ).
thf(f253,definition,
( spl0_48
<=> ( ( b @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_48])],[avatar_definition]) ).
thf(f244,plain,
( ( ( b @ $false )
= $true )
| ~ spl0_45 ),
inference(avatar_component_clause,[status(thm)],[f243]) ).
thf(f243,definition,
( spl0_45
<=> ( ( b @ $false )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_45])],[avatar_definition]) ).
thf(f509,plain,
( ~ spl0_65
| ~ spl0_66 ),
inference(avatar_contradiction_clause,[status(thm)],[f508]) ).
thf(f508,plain,
( $false
| ~ spl0_65
| ~ spl0_66 ),
inference(trivial_inequality_removal,[status(thm)],[f507]) ).
thf(f507,plain,
( ( $true = $false )
| ~ spl0_65
| ~ spl0_66 ),
inference(backward_demodulation,[status(thm)],[f448,f443]) ).
thf(f443,plain,
( ( sK14 = $false )
| ~ spl0_65 ),
inference(avatar_component_clause,[status(thm)],[f442]) ).
thf(f442,definition,
( spl0_65
<=> ( sK14 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_65])],[avatar_definition]) ).
thf(f448,plain,
( ( $true = sK14 )
| ~ spl0_66 ),
inference(avatar_component_clause,[status(thm)],[f447]) ).
thf(f447,definition,
( spl0_66
<=> ( $true = sK14 ) ),
introduced(definition,[new_symbols(naming,[spl0_66])],[avatar_definition]) ).
thf(f503,plain,
( ~ spl0_41
| ~ spl0_43 ),
inference(avatar_contradiction_clause,[status(thm)],[f502]) ).
thf(f502,plain,
( $false
| ~ spl0_41
| ~ spl0_43 ),
inference(trivial_inequality_removal,[status(thm)],[f501]) ).
thf(f501,plain,
( ( $true = $false )
| ~ spl0_41
| ~ spl0_43 ),
inference(backward_demodulation,[status(thm)],[f230,f237]) ).
thf(f237,plain,
( ( ( c @ $true )
= $false )
| ~ spl0_43 ),
inference(avatar_component_clause,[status(thm)],[f236]) ).
thf(f230,plain,
( ( $true
= ( c @ $true ) )
| ~ spl0_41 ),
inference(avatar_component_clause,[status(thm)],[f229]) ).
thf(f229,definition,
( spl0_41
<=> ( $true
= ( c @ $true ) ) ),
introduced(definition,[new_symbols(naming,[spl0_41])],[avatar_definition]) ).
thf(f500,plain,
( ~ spl0_40
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[status(thm)],[f499]) ).
thf(f499,plain,
( $false
| ~ spl0_40
| ~ spl0_42 ),
inference(trivial_inequality_removal,[status(thm)],[f498]) ).
thf(f498,plain,
( ( $true = $false )
| ~ spl0_40
| ~ spl0_42 ),
inference(backward_demodulation,[status(thm)],[f227,f234]) ).
thf(f234,plain,
( ( ( b @ $true )
= $false )
| ~ spl0_42 ),
inference(avatar_component_clause,[status(thm)],[f233]) ).
thf(f233,definition,
( spl0_42
<=> ( ( b @ $true )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_42])],[avatar_definition]) ).
thf(f227,plain,
( ( ( b @ $true )
= $true )
| ~ spl0_40 ),
inference(avatar_component_clause,[status(thm)],[f226]) ).
thf(f226,definition,
( spl0_40
<=> ( ( b @ $true )
= $true ) ),
introduced(definition,[new_symbols(naming,[spl0_40])],[avatar_definition]) ).
thf(f478,plain,
( ~ spl0_27
| spl0_28 ),
inference(avatar_split_clause,[status(thm)],[f477,f160,f157]) ).
thf(f160,definition,
( spl0_28
<=> ( ( f9 @ d )
= ( f9 @ e ) ) ),
introduced(definition,[new_symbols(naming,[spl0_28])],[avatar_definition]) ).
thf(f477,plain,
( ( d != e )
| spl0_28 ),
inference(equality_resolution,[status(thm)],[f161]) ).
thf(f161,plain,
( ( ( f9 @ d )
!= ( f9 @ e ) )
| spl0_28 ),
inference(avatar_component_clause,[status(thm)],[f160]) ).
thf(f476,plain,
( ~ spl0_24
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[status(thm)],[f475]) ).
thf(f475,plain,
( $false
| ~ spl0_24
| ~ spl0_26 ),
inference(trivial_inequality_removal,[status(thm)],[f474]) ).
thf(f474,plain,
( ( $true = $false )
| ~ spl0_24
| ~ spl0_26 ),
inference(backward_demodulation,[status(thm)],[f146,f153]) ).
thf(f153,plain,
( ( ( e @ $false )
= $false )
| ~ spl0_26 ),
inference(avatar_component_clause,[status(thm)],[f152]) ).
thf(f146,plain,
( ( $true
= ( e @ $false ) )
| ~ spl0_24 ),
inference(avatar_component_clause,[status(thm)],[f145]) ).
thf(f145,definition,
( spl0_24
<=> ( $true
= ( e @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl0_24])],[avatar_definition]) ).
thf(f471,plain,
( ~ spl0_57
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[status(thm)],[f470]) ).
thf(f470,plain,
( $false
| ~ spl0_57
| ~ spl0_58 ),
inference(trivial_inequality_removal,[status(thm)],[f469]) ).
thf(f469,plain,
( ( $true = $false )
| ~ spl0_57
| ~ spl0_58 ),
inference(backward_demodulation,[status(thm)],[f359,f355]) ).
thf(f355,plain,
( ( sK10 = $false )
| ~ spl0_57 ),
inference(avatar_component_clause,[status(thm)],[f354]) ).
thf(f354,definition,
( spl0_57
<=> ( sK10 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_57])],[avatar_definition]) ).
thf(f465,plain,
( ~ spl0_21
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[status(thm)],[f464]) ).
thf(f464,plain,
( $false
| ~ spl0_21
| ~ spl0_23 ),
inference(trivial_inequality_removal,[status(thm)],[f463]) ).
thf(f463,plain,
( ( $true = $false )
| ~ spl0_21
| ~ spl0_23 ),
inference(backward_demodulation,[status(thm)],[f135,f142]) ).
thf(f142,plain,
( ( ( e @ $true )
= $false )
| ~ spl0_23 ),
inference(avatar_component_clause,[status(thm)],[f141]) ).
thf(f135,plain,
( ( $true
= ( e @ $true ) )
| ~ spl0_21 ),
inference(avatar_component_clause,[status(thm)],[f134]) ).
thf(f460,plain,
( ~ spl0_10
| ~ spl0_12 ),
inference(avatar_contradiction_clause,[status(thm)],[f459]) ).
thf(f459,plain,
( $false
| ~ spl0_10
| ~ spl0_12 ),
inference(trivial_inequality_removal,[status(thm)],[f458]) ).
thf(f458,plain,
( ( $true = $false )
| ~ spl0_10
| ~ spl0_12 ),
inference(backward_demodulation,[status(thm)],[f85,f92]) ).
thf(f92,plain,
( ( ( a @ $false )
= $false )
| ~ spl0_12 ),
inference(avatar_component_clause,[status(thm)],[f91]) ).
thf(f91,definition,
( spl0_12
<=> ( ( a @ $false )
= $false ) ),
introduced(definition,[new_symbols(naming,[spl0_12])],[avatar_definition]) ).
thf(f85,plain,
( ( $true
= ( a @ $false ) )
| ~ spl0_10 ),
inference(avatar_component_clause,[status(thm)],[f84]) ).
thf(f84,definition,
( spl0_10
<=> ( $true
= ( a @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition]) ).
thf(f457,plain,
( ~ spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[status(thm)],[f456]) ).
thf(f456,plain,
( $false
| ~ spl0_9
| ~ spl0_11 ),
inference(trivial_inequality_removal,[status(thm)],[f453]) ).
thf(f453,plain,
( ( $true = $false )
| ~ spl0_9
| ~ spl0_11 ),
inference(backward_demodulation,[status(thm)],[f82,f89]) ).
thf(f89,plain,
( ( ( d @ $false )
= $false )
| ~ spl0_11 ),
inference(avatar_component_clause,[status(thm)],[f88]) ).
thf(f82,plain,
( ( $true
= ( d @ $false ) )
| ~ spl0_9 ),
inference(avatar_component_clause,[status(thm)],[f81]) ).
thf(f81,definition,
( spl0_9
<=> ( $true
= ( d @ $false ) ) ),
introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition]) ).
thf(f450,plain,
( spl0_66
| spl0_48
| spl0_47
| spl0_37 ),
inference(avatar_split_clause,[status(thm)],[f438,f209,f250,f253,f447]) ).
thf(f209,definition,
( spl0_37
<=> ( b = c ) ),
introduced(definition,[new_symbols(naming,[spl0_37])],[avatar_definition]) ).
thf(f438,plain,
( ( ( c @ $false )
= $false )
| ( $true = sK14 )
| ( ( b @ $false )
= $false )
| spl0_37 ),
inference(binary_proxy_clausification,[status(thm)],[f436]) ).
thf(f436,plain,
( ( $true = sK14 )
| ( ( c @ $false )
!= ( b @ $false ) )
| spl0_37 ),
inference(cases_simplifying,[status(thm)],[f434]) ).
thf(f434,plain,
( ( ( b @ sK14 )
!= ( c @ sK14 ) )
| spl0_37 ),
inference(negative_extensionality,[status(thm)],[f210]) ).
thf(f210,plain,
( ( b != c )
| spl0_37 ),
inference(avatar_component_clause,[status(thm)],[f209]) ).
thf(f449,plain,
( spl0_45
| spl0_66
| spl0_44
| spl0_37 ),
inference(avatar_split_clause,[status(thm)],[f437,f209,f240,f447,f243]) ).
thf(f437,plain,
( ( ( b @ $false )
= $true )
| ( ( c @ $false )
= $true )
| ( $true = sK14 )
| spl0_37 ),
inference(binary_proxy_clausification,[status(thm)],[f436]) ).
thf(f445,plain,
( spl0_43
| spl0_42
| spl0_65
| spl0_37 ),
inference(avatar_split_clause,[status(thm)],[f440,f209,f442,f233,f236]) ).
thf(f440,plain,
( ( ( b @ $true )
= $false )
| ( sK14 = $false )
| ( ( c @ $true )
= $false )
| spl0_37 ),
inference(binary_proxy_clausification,[status(thm)],[f435]) ).
thf(f435,plain,
( ( ( b @ $true )
!= ( c @ $true ) )
| ( sK14 = $false )
| spl0_37 ),
inference(cases_simplifying,[status(thm)],[f434]) ).
thf(f444,plain,
( spl0_40
| spl0_65
| spl0_41
| spl0_37 ),
inference(avatar_split_clause,[status(thm)],[f439,f209,f229,f442,f226]) ).
thf(f439,plain,
( ( sK14 = $false )
| ( ( b @ $true )
= $true )
| ( $true
= ( c @ $true ) )
| spl0_37 ),
inference(binary_proxy_clausification,[status(thm)],[f435]) ).
thf(f433,plain,
( ~ spl0_37
| spl0_38 ),
inference(avatar_split_clause,[status(thm)],[f432,f212,f209]) ).
thf(f212,definition,
( spl0_38
<=> ( ( f4 @ b )
= ( f4 @ c ) ) ),
introduced(definition,[new_symbols(naming,[spl0_38])],[avatar_definition]) ).
thf(f432,plain,
( ( b != c )
| spl0_38 ),
inference(equality_resolution,[status(thm)],[f213]) ).
thf(f213,plain,
( ( ( f4 @ b )
!= ( f4 @ c ) )
| spl0_38 ),
inference(avatar_component_clause,[status(thm)],[f212]) ).
thf(f431,plain,
( spl0_47
| spl0_64
| spl0_12
| spl0_36 ),
inference(avatar_split_clause,[status(thm)],[f418,f201,f91,f428,f250]) ).
thf(f418,plain,
( ( ( c @ $false )
= $false )
| ( sK13 = $true )
| ( ( a @ $false )
= $false )
| spl0_36 ),
inference(binary_proxy_clausification,[status(thm)],[f416]) ).
thf(f416,plain,
( ( sK13 = $true )
| ( ( c @ $false )
!= ( a @ $false ) )
| spl0_36 ),
inference(cases_simplifying,[status(thm)],[f414]) ).
thf(f430,plain,
( spl0_44
| spl0_10
| spl0_64
| spl0_36 ),
inference(avatar_split_clause,[status(thm)],[f417,f201,f428,f84,f240]) ).
thf(f417,plain,
( ( $true
= ( a @ $false ) )
| ( sK13 = $true )
| ( ( c @ $false )
= $true )
| spl0_36 ),
inference(binary_proxy_clausification,[status(thm)],[f416]) ).
thf(f426,plain,
( spl0_41
| spl0_63
| ~ spl0_7
| spl0_36 ),
inference(avatar_split_clause,[status(thm)],[f422,f201,f74,f424,f229]) ).
thf(f422,plain,
( ( sK13 = $false )
| ( $true
= ( c @ $true ) )
| ~ spl0_7
| spl0_36 ),
inference(trivial_inequality_removal,[status(thm)],[f421]) ).
thf(f421,plain,
( ( $true = $false )
| ( $true
= ( c @ $true ) )
| ( sK13 = $false )
| ~ spl0_7
| spl0_36 ),
inference(forward_demodulation,[status(thm)],[f419,f75]) ).
thf(f75,plain,
( ( ( a @ $true )
= $false )
| ~ spl0_7 ),
inference(avatar_component_clause,[status(thm)],[f74]) ).
thf(f419,plain,
( ( $true
= ( a @ $true ) )
| ( $true
= ( c @ $true ) )
| ( sK13 = $false )
| spl0_36 ),
inference(binary_proxy_clausification,[status(thm)],[f415]) ).
thf(f413,plain,
( ~ spl0_36
| spl0_35 ),
inference(avatar_split_clause,[status(thm)],[f412,f198,f201]) ).
thf(f198,definition,
( spl0_35
<=> ( ( f1 @ a )
= ( f1 @ c ) ) ),
introduced(definition,[new_symbols(naming,[spl0_35])],[avatar_definition]) ).
thf(f412,plain,
( ( a != c )
| spl0_35 ),
inference(equality_resolution,[status(thm)],[f199]) ).
thf(f199,plain,
( ( ( f1 @ a )
!= ( f1 @ c ) )
| spl0_35 ),
inference(avatar_component_clause,[status(thm)],[f198]) ).
thf(f411,plain,
( spl0_49
| spl0_3
| spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[status(thm)],[f410,f74,f47,f61,f268]) ).
thf(f410,plain,
( ( ( d @ $true )
= $true )
| ( sK6 = $false )
| spl0_1
| ~ spl0_7 ),
inference(trivial_inequality_removal,[status(thm)],[f409]) ).
thf(f409,plain,
( ( $true = $false )
| ( sK6 = $false )
| ( ( d @ $true )
= $true )
| spl0_1
| ~ spl0_7 ),
inference(forward_demodulation,[status(thm)],[f263,f75]) ).
thf(f263,plain,
( ( ( d @ $true )
= $true )
| ( $true
= ( a @ $true ) )
| ( sK6 = $false )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f259]) ).
thf(f407,plain,
( spl0_57
| spl0_21
| ~ spl0_7
| spl0_19 ),
inference(avatar_split_clause,[status(thm)],[f406,f120,f74,f134,f354]) ).
thf(f406,plain,
( ( $true
= ( e @ $true ) )
| ( sK10 = $false )
| ~ spl0_7
| spl0_19 ),
inference(trivial_inequality_removal,[status(thm)],[f405]) ).
thf(f405,plain,
( ( $true = $false )
| ( $true
= ( e @ $true ) )
| ( sK10 = $false )
| ~ spl0_7
| spl0_19 ),
inference(forward_demodulation,[status(thm)],[f349,f75]) ).
thf(f404,plain,
( spl0_6
| spl0_43
| spl0_61
| spl0_34 ),
inference(avatar_split_clause,[status(thm)],[f389,f193,f393,f236,f71]) ).
thf(f193,definition,
( spl0_34
<=> ( c = d ) ),
introduced(definition,[new_symbols(naming,[spl0_34])],[avatar_definition]) ).
thf(f389,plain,
( ( ( d @ $true )
= $false )
| ( sK12 = $false )
| ( ( c @ $true )
= $false )
| spl0_34 ),
inference(binary_proxy_clausification,[status(thm)],[f384]) ).
thf(f384,plain,
( ( sK12 = $false )
| ( ( d @ $true )
!= ( c @ $true ) )
| spl0_34 ),
inference(cases_simplifying,[status(thm)],[f383]) ).
thf(f383,plain,
( ( ( d @ sK12 )
!= ( c @ sK12 ) )
| spl0_34 ),
inference(negative_extensionality,[status(thm)],[f194]) ).
thf(f194,plain,
( ( c != d )
| spl0_34 ),
inference(avatar_component_clause,[status(thm)],[f193]) ).
thf(f403,plain,
( ~ spl0_5
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[status(thm)],[f402]) ).
thf(f402,plain,
( $false
| ~ spl0_5
| ~ spl0_7 ),
inference(trivial_inequality_removal,[status(thm)],[f401]) ).
thf(f401,plain,
( ( $true = $false )
| ~ spl0_5
| ~ spl0_7 ),
inference(backward_demodulation,[status(thm)],[f68,f75]) ).
thf(f68,plain,
( ( $true
= ( a @ $true ) )
| ~ spl0_5 ),
inference(avatar_component_clause,[status(thm)],[f67]) ).
thf(f400,plain,
( spl0_62
| spl0_11
| spl0_47
| spl0_34 ),
inference(avatar_split_clause,[status(thm)],[f387,f193,f250,f88,f397]) ).
thf(f387,plain,
( ( ( d @ $false )
= $false )
| ( ( c @ $false )
= $false )
| ( sK12 = $true )
| spl0_34 ),
inference(binary_proxy_clausification,[status(thm)],[f385]) ).
thf(f385,plain,
( ( ( c @ $false )
!= ( d @ $false ) )
| ( sK12 = $true )
| spl0_34 ),
inference(cases_simplifying,[status(thm)],[f383]) ).
thf(f399,plain,
( spl0_44
| spl0_62
| spl0_9
| spl0_34 ),
inference(avatar_split_clause,[status(thm)],[f386,f193,f81,f397,f240]) ).
thf(f386,plain,
( ( $true
= ( d @ $false ) )
| ( sK12 = $true )
| ( ( c @ $false )
= $true )
| spl0_34 ),
inference(binary_proxy_clausification,[status(thm)],[f385]) ).
thf(f395,plain,
( spl0_41
| spl0_61
| ~ spl0_6
| spl0_34 ),
inference(avatar_split_clause,[status(thm)],[f391,f193,f71,f393,f229]) ).
thf(f391,plain,
( ( sK12 = $false )
| ( $true
= ( c @ $true ) )
| ~ spl0_6
| spl0_34 ),
inference(trivial_inequality_removal,[status(thm)],[f390]) ).
thf(f390,plain,
( ( $true
= ( c @ $true ) )
| ( sK12 = $false )
| ( $true = $false )
| ~ spl0_6
| spl0_34 ),
inference(forward_demodulation,[status(thm)],[f388,f72]) ).
thf(f72,plain,
( ( ( d @ $true )
= $false )
| ~ spl0_6 ),
inference(avatar_component_clause,[status(thm)],[f71]) ).
thf(f388,plain,
( ( ( d @ $true )
= $true )
| ( sK12 = $false )
| ( $true
= ( c @ $true ) )
| spl0_34 ),
inference(binary_proxy_clausification,[status(thm)],[f384]) ).
thf(f382,plain,
( ~ spl0_34
| spl0_33 ),
inference(avatar_split_clause,[status(thm)],[f381,f190,f193]) ).
thf(f190,definition,
( spl0_33
<=> ( ( f7 @ c )
= ( f7 @ d ) ) ),
introduced(definition,[new_symbols(naming,[spl0_33])],[avatar_definition]) ).
thf(f381,plain,
( ( c != d )
| spl0_33 ),
inference(equality_resolution,[status(thm)],[f191]) ).
thf(f191,plain,
( ( ( f7 @ c )
!= ( f7 @ d ) )
| spl0_33 ),
inference(avatar_component_clause,[status(thm)],[f190]) ).
thf(f380,plain,
( spl0_47
| spl0_26
| spl0_60
| spl0_30 ),
inference(avatar_split_clause,[status(thm)],[f368,f168,f377,f152,f250]) ).
thf(f168,definition,
( spl0_30
<=> ( c = e ) ),
introduced(definition,[new_symbols(naming,[spl0_30])],[avatar_definition]) ).
thf(f368,plain,
( ( sK11 = $true )
| ( ( e @ $false )
= $false )
| ( ( c @ $false )
= $false )
| spl0_30 ),
inference(binary_proxy_clausification,[status(thm)],[f366]) ).
thf(f366,plain,
( ( sK11 = $true )
| ( ( c @ $false )
!= ( e @ $false ) )
| spl0_30 ),
inference(cases_simplifying,[status(thm)],[f364]) ).
thf(f364,plain,
( ( ( e @ sK11 )
!= ( c @ sK11 ) )
| spl0_30 ),
inference(negative_extensionality,[status(thm)],[f169]) ).
thf(f169,plain,
( ( c != e )
| spl0_30 ),
inference(avatar_component_clause,[status(thm)],[f168]) ).
thf(f379,plain,
( spl0_60
| spl0_24
| spl0_44
| spl0_30 ),
inference(avatar_split_clause,[status(thm)],[f367,f168,f240,f145,f377]) ).
thf(f367,plain,
( ( sK11 = $true )
| ( ( c @ $false )
= $true )
| ( $true
= ( e @ $false ) )
| spl0_30 ),
inference(binary_proxy_clausification,[status(thm)],[f366]) ).
thf(f375,plain,
( spl0_43
| spl0_59
| spl0_23
| spl0_30 ),
inference(avatar_split_clause,[status(thm)],[f370,f168,f141,f372,f236]) ).
thf(f370,plain,
( ( ( c @ $true )
= $false )
| ( ( e @ $true )
= $false )
| ( sK11 = $false )
| spl0_30 ),
inference(binary_proxy_clausification,[status(thm)],[f365]) ).
thf(f365,plain,
( ( sK11 = $false )
| ( ( e @ $true )
!= ( c @ $true ) )
| spl0_30 ),
inference(cases_simplifying,[status(thm)],[f364]) ).
thf(f374,plain,
( spl0_59
| spl0_41
| spl0_21
| spl0_30 ),
inference(avatar_split_clause,[status(thm)],[f369,f168,f134,f229,f372]) ).
thf(f369,plain,
( ( sK11 = $false )
| ( $true
= ( c @ $true ) )
| ( $true
= ( e @ $true ) )
| spl0_30 ),
inference(binary_proxy_clausification,[status(thm)],[f365]) ).
thf(f363,plain,
( ~ spl0_30
| spl0_29 ),
inference(avatar_split_clause,[status(thm)],[f362,f165,f168]) ).
thf(f165,definition,
( spl0_29
<=> ( ( f8 @ c )
= ( f8 @ e ) ) ),
introduced(definition,[new_symbols(naming,[spl0_29])],[avatar_definition]) ).
thf(f362,plain,
( ( c != e )
| spl0_29 ),
inference(equality_resolution,[status(thm)],[f166]) ).
thf(f166,plain,
( ( ( f8 @ c )
!= ( f8 @ e ) )
| spl0_29 ),
inference(avatar_component_clause,[status(thm)],[f165]) ).
thf(f361,plain,
( spl0_26
| spl0_12
| spl0_58
| spl0_19 ),
inference(avatar_split_clause,[status(thm)],[f348,f120,f358,f91,f152]) ).
thf(f348,plain,
( ( ( e @ $false )
= $false )
| ( $true = sK10 )
| ( ( a @ $false )
= $false )
| spl0_19 ),
inference(binary_proxy_clausification,[status(thm)],[f346]) ).
thf(f346,plain,
( ( $true = sK10 )
| ( ( e @ $false )
!= ( a @ $false ) )
| spl0_19 ),
inference(cases_simplifying,[status(thm)],[f344]) ).
thf(f360,plain,
( spl0_58
| spl0_10
| spl0_24
| spl0_19 ),
inference(avatar_split_clause,[status(thm)],[f347,f120,f145,f84,f358]) ).
thf(f347,plain,
( ( $true
= ( e @ $false ) )
| ( $true = sK10 )
| ( $true
= ( a @ $false ) )
| spl0_19 ),
inference(binary_proxy_clausification,[status(thm)],[f346]) ).
thf(f356,plain,
( spl0_57
| spl0_23
| ~ spl0_5
| spl0_19 ),
inference(avatar_split_clause,[status(thm)],[f352,f120,f67,f141,f354]) ).
thf(f352,plain,
( ( sK10 = $false )
| ( ( e @ $true )
= $false )
| ~ spl0_5
| spl0_19 ),
inference(trivial_inequality_removal,[status(thm)],[f351]) ).
thf(f351,plain,
( ( ( e @ $true )
= $false )
| ( $true = $false )
| ( sK10 = $false )
| ~ spl0_5
| spl0_19 ),
inference(forward_demodulation,[status(thm)],[f350,f68]) ).
thf(f343,plain,
( ~ spl0_19
| spl0_20 ),
inference(avatar_split_clause,[status(thm)],[f342,f123,f120]) ).
thf(f123,definition,
( spl0_20
<=> ( ( f3 @ a )
= ( f3 @ e ) ) ),
introduced(definition,[new_symbols(naming,[spl0_20])],[avatar_definition]) ).
thf(f342,plain,
( ( a != e )
| spl0_20 ),
inference(equality_resolution,[status(thm)],[f124]) ).
thf(f124,plain,
( ( ( f3 @ a )
!= ( f3 @ e ) )
| spl0_20 ),
inference(avatar_component_clause,[status(thm)],[f123]) ).
thf(f341,plain,
( spl0_48
| spl0_56
| spl0_26
| spl0_18 ),
inference(avatar_split_clause,[status(thm)],[f329,f115,f152,f338,f253]) ).
thf(f115,definition,
( spl0_18
<=> ( b = e ) ),
introduced(definition,[new_symbols(naming,[spl0_18])],[avatar_definition]) ).
thf(f329,plain,
( ( ( b @ $false )
= $false )
| ( $true = sK9 )
| ( ( e @ $false )
= $false )
| spl0_18 ),
inference(binary_proxy_clausification,[status(thm)],[f327]) ).
thf(f327,plain,
( ( $true = sK9 )
| ( ( b @ $false )
!= ( e @ $false ) )
| spl0_18 ),
inference(cases_simplifying,[status(thm)],[f325]) ).
thf(f325,plain,
( ( ( e @ sK9 )
!= ( b @ sK9 ) )
| spl0_18 ),
inference(negative_extensionality,[status(thm)],[f116]) ).
thf(f116,plain,
( ( b != e )
| spl0_18 ),
inference(avatar_component_clause,[status(thm)],[f115]) ).
thf(f340,plain,
( spl0_24
| spl0_56
| spl0_45
| spl0_18 ),
inference(avatar_split_clause,[status(thm)],[f328,f115,f243,f338,f145]) ).
thf(f328,plain,
( ( $true
= ( e @ $false ) )
| ( ( b @ $false )
= $true )
| ( $true = sK9 )
| spl0_18 ),
inference(binary_proxy_clausification,[status(thm)],[f327]) ).
thf(f336,plain,
( spl0_42
| spl0_55
| spl0_23
| spl0_18 ),
inference(avatar_split_clause,[status(thm)],[f331,f115,f141,f333,f233]) ).
thf(f331,plain,
( ( ( e @ $true )
= $false )
| ( sK9 = $false )
| ( ( b @ $true )
= $false )
| spl0_18 ),
inference(binary_proxy_clausification,[status(thm)],[f326]) ).
thf(f326,plain,
( ( sK9 = $false )
| ( ( b @ $true )
!= ( e @ $true ) )
| spl0_18 ),
inference(cases_simplifying,[status(thm)],[f325]) ).
thf(f335,plain,
( spl0_55
| spl0_21
| spl0_40
| spl0_18 ),
inference(avatar_split_clause,[status(thm)],[f330,f115,f226,f134,f333]) ).
thf(f330,plain,
( ( $true
= ( e @ $true ) )
| ( sK9 = $false )
| ( ( b @ $true )
= $true )
| spl0_18 ),
inference(binary_proxy_clausification,[status(thm)],[f326]) ).
thf(f324,plain,
( ~ spl0_18
| spl0_17 ),
inference(avatar_split_clause,[status(thm)],[f323,f112,f115]) ).
thf(f112,definition,
( spl0_17
<=> ( ( f6 @ b )
= ( f6 @ e ) ) ),
introduced(definition,[new_symbols(naming,[spl0_17])],[avatar_definition]) ).
thf(f323,plain,
( ( b != e )
| spl0_17 ),
inference(equality_resolution,[status(thm)],[f113]) ).
thf(f113,plain,
( ( ( f6 @ b )
!= ( f6 @ e ) )
| spl0_17 ),
inference(avatar_component_clause,[status(thm)],[f112]) ).
thf(f322,plain,
( spl0_6
| spl0_49
| spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[status(thm)],[f321,f67,f47,f268,f71]) ).
thf(f321,plain,
( ( sK6 = $false )
| ( ( d @ $true )
= $false )
| spl0_1
| ~ spl0_5 ),
inference(trivial_inequality_removal,[status(thm)],[f320]) ).
thf(f320,plain,
( ( sK6 = $false )
| ( $true = $false )
| ( ( d @ $true )
= $false )
| spl0_1
| ~ spl0_5 ),
inference(forward_demodulation,[status(thm)],[f264,f68]) ).
thf(f319,plain,
( spl0_42
| spl0_53
| spl0_6
| spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f306,f107,f71,f310,f233]) ).
thf(f107,definition,
( spl0_16
<=> ( b = d ) ),
introduced(definition,[new_symbols(naming,[spl0_16])],[avatar_definition]) ).
thf(f306,plain,
( ( ( d @ $true )
= $false )
| ( ( b @ $true )
= $false )
| ( sK8 = $false )
| spl0_16 ),
inference(binary_proxy_clausification,[status(thm)],[f301]) ).
thf(f301,plain,
( ( sK8 = $false )
| ( ( b @ $true )
!= ( d @ $true ) )
| spl0_16 ),
inference(cases_simplifying,[status(thm)],[f300]) ).
thf(f300,plain,
( ( ( d @ sK8 )
!= ( b @ sK8 ) )
| spl0_16 ),
inference(negative_extensionality,[status(thm)],[f108]) ).
thf(f108,plain,
( ( b != d )
| spl0_16 ),
inference(avatar_component_clause,[status(thm)],[f107]) ).
thf(f318,plain,
( spl0_3
| spl0_40
| spl0_53
| spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f305,f107,f310,f226,f61]) ).
thf(f305,plain,
( ( ( d @ $true )
= $true )
| ( ( b @ $true )
= $true )
| ( sK8 = $false )
| spl0_16 ),
inference(binary_proxy_clausification,[status(thm)],[f301]) ).
thf(f317,plain,
( spl0_11
| spl0_48
| spl0_54
| spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f304,f107,f314,f253,f88]) ).
thf(f304,plain,
( ( sK8 = $true )
| ( ( b @ $false )
= $false )
| ( ( d @ $false )
= $false )
| spl0_16 ),
inference(binary_proxy_clausification,[status(thm)],[f302]) ).
thf(f302,plain,
( ( sK8 = $true )
| ( ( b @ $false )
!= ( d @ $false ) )
| spl0_16 ),
inference(cases_simplifying,[status(thm)],[f300]) ).
thf(f316,plain,
( spl0_54
| spl0_45
| spl0_9
| spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f303,f107,f81,f243,f314]) ).
thf(f303,plain,
( ( sK8 = $true )
| ( ( b @ $false )
= $true )
| ( $true
= ( d @ $false ) )
| spl0_16 ),
inference(binary_proxy_clausification,[status(thm)],[f302]) ).
thf(f312,plain,
( spl0_53
| spl0_40
| ~ spl0_6
| spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f308,f107,f71,f226,f310]) ).
thf(f308,plain,
( ( ( b @ $true )
= $true )
| ( sK8 = $false )
| ~ spl0_6
| spl0_16 ),
inference(trivial_inequality_removal,[status(thm)],[f307]) ).
thf(f307,plain,
( ( sK8 = $false )
| ( ( b @ $true )
= $true )
| ( $true = $false )
| ~ spl0_6
| spl0_16 ),
inference(forward_demodulation,[status(thm)],[f305,f72]) ).
thf(f299,plain,
( ~ spl0_16
| spl0_15 ),
inference(avatar_split_clause,[status(thm)],[f298,f104,f107]) ).
thf(f104,definition,
( spl0_15
<=> ( ( f5 @ b )
= ( f5 @ d ) ) ),
introduced(definition,[new_symbols(naming,[spl0_15])],[avatar_definition]) ).
thf(f298,plain,
( ( b != d )
| spl0_15 ),
inference(equality_resolution,[status(thm)],[f105]) ).
thf(f105,plain,
( ( ( f5 @ b )
!= ( f5 @ d ) )
| spl0_15 ),
inference(avatar_component_clause,[status(thm)],[f104]) ).
thf(f297,plain,
( spl0_48
| spl0_52
| spl0_12
| spl0_14 ),
inference(avatar_split_clause,[status(thm)],[f285,f99,f91,f294,f253]) ).
thf(f99,definition,
( spl0_14
<=> ( a = b ) ),
introduced(definition,[new_symbols(naming,[spl0_14])],[avatar_definition]) ).
thf(f285,plain,
( ( $true = sK7 )
| ( ( a @ $false )
= $false )
| ( ( b @ $false )
= $false )
| spl0_14 ),
inference(binary_proxy_clausification,[status(thm)],[f283]) ).
thf(f283,plain,
( ( ( b @ $false )
!= ( a @ $false ) )
| ( $true = sK7 )
| spl0_14 ),
inference(cases_simplifying,[status(thm)],[f281]) ).
thf(f281,plain,
( ( ( a @ sK7 )
!= ( b @ sK7 ) )
| spl0_14 ),
inference(negative_extensionality,[status(thm)],[f100]) ).
thf(f100,plain,
( ( a != b )
| spl0_14 ),
inference(avatar_component_clause,[status(thm)],[f99]) ).
thf(f296,plain,
( spl0_45
| spl0_10
| spl0_52
| spl0_14 ),
inference(avatar_split_clause,[status(thm)],[f284,f99,f294,f84,f243]) ).
thf(f284,plain,
( ( $true = sK7 )
| ( $true
= ( a @ $false ) )
| ( ( b @ $false )
= $true )
| spl0_14 ),
inference(binary_proxy_clausification,[status(thm)],[f283]) ).
thf(f292,plain,
( spl0_7
| spl0_42
| spl0_51
| spl0_14 ),
inference(avatar_split_clause,[status(thm)],[f287,f99,f289,f233,f74]) ).
thf(f287,plain,
( ( ( b @ $true )
= $false )
| ( sK7 = $false )
| ( ( a @ $true )
= $false )
| spl0_14 ),
inference(binary_proxy_clausification,[status(thm)],[f282]) ).
thf(f282,plain,
( ( ( b @ $true )
!= ( a @ $true ) )
| ( sK7 = $false )
| spl0_14 ),
inference(cases_simplifying,[status(thm)],[f281]) ).
thf(f291,plain,
( spl0_51
| spl0_40
| spl0_5
| spl0_14 ),
inference(avatar_split_clause,[status(thm)],[f286,f99,f67,f226,f289]) ).
thf(f286,plain,
( ( sK7 = $false )
| ( $true
= ( a @ $true ) )
| ( ( b @ $true )
= $true )
| spl0_14 ),
inference(binary_proxy_clausification,[status(thm)],[f282]) ).
thf(f280,plain,
( ~ spl0_14
| spl0_13 ),
inference(avatar_split_clause,[status(thm)],[f279,f96,f99]) ).
thf(f96,definition,
( spl0_13
<=> ( ( f0 @ a )
= ( f0 @ b ) ) ),
introduced(definition,[new_symbols(naming,[spl0_13])],[avatar_definition]) ).
thf(f279,plain,
( ( a != b )
| spl0_13 ),
inference(equality_resolution,[status(thm)],[f97]) ).
thf(f97,plain,
( ( ( f0 @ a )
!= ( f0 @ b ) )
| spl0_13 ),
inference(avatar_component_clause,[status(thm)],[f96]) ).
thf(f278,plain,
( ~ spl0_4
| ~ spl0_8 ),
inference(avatar_contradiction_clause,[status(thm)],[f277]) ).
thf(f277,plain,
( $false
| ~ spl0_4
| ~ spl0_8 ),
inference(trivial_inequality_removal,[status(thm)],[f276]) ).
thf(f276,plain,
( ( $true = $false )
| ~ spl0_4
| ~ spl0_8 ),
inference(forward_demodulation,[status(thm)],[f79,f65]) ).
thf(f65,plain,
( ( sK2 = $false )
| ~ spl0_4 ),
inference(avatar_component_clause,[status(thm)],[f64]) ).
thf(f64,definition,
( spl0_4
<=> ( sK2 = $false ) ),
introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition]) ).
thf(f79,plain,
( ( $true = sK2 )
| ~ spl0_8 ),
inference(avatar_component_clause,[status(thm)],[f78]) ).
thf(f78,definition,
( spl0_8
<=> ( $true = sK2 ) ),
introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition]) ).
thf(f275,plain,
( spl0_11
| spl0_50
| spl0_12
| spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f262,f47,f91,f272,f88]) ).
thf(f262,plain,
( ( ( a @ $false )
= $false )
| ( sK6 = $true )
| ( ( d @ $false )
= $false )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f260]) ).
thf(f260,plain,
( ( sK6 = $true )
| ( ( d @ $false )
!= ( a @ $false ) )
| spl0_1 ),
inference(cases_simplifying,[status(thm)],[f258]) ).
thf(f274,plain,
( spl0_9
| spl0_50
| spl0_10
| spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f261,f47,f84,f272,f81]) ).
thf(f261,plain,
( ( sK6 = $true )
| ( $true
= ( a @ $false ) )
| ( $true
= ( d @ $false ) )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f260]) ).
thf(f270,plain,
( spl0_5
| spl0_49
| spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[status(thm)],[f266,f71,f47,f268,f67]) ).
thf(f266,plain,
( ( sK6 = $false )
| ( $true
= ( a @ $true ) )
| spl0_1
| ~ spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f265]) ).
thf(f265,plain,
( ( sK6 = $false )
| ( $true = $false )
| ( $true
= ( a @ $true ) )
| spl0_1
| ~ spl0_6 ),
inference(forward_demodulation,[status(thm)],[f263,f72]) ).
thf(f257,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f256,f50,f47]) ).
thf(f50,definition,
( spl0_2
<=> ( ( f2 @ a )
= ( f2 @ d ) ) ),
introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition]) ).
thf(f256,plain,
( ( a != d )
| spl0_2 ),
inference(equality_resolution,[status(thm)],[f51]) ).
thf(f51,plain,
( ( ( f2 @ a )
!= ( f2 @ d ) )
| spl0_2 ),
inference(avatar_component_clause,[status(thm)],[f50]) ).
thf(f214,plain,
( ~ spl0_37
| ~ spl0_38 ),
inference(avatar_split_clause,[status(thm)],[f207,f212,f209]) ).
thf(f207,plain,
( ( b != c )
| ( ( f4 @ b )
!= ( f4 @ c ) ) ),
inference(constrained_superposition,[status(thm)],[f32,f44]) ).
thf(f44,plain,
( ( f4 @ b )
= ( g4 @ c ) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
thf(f9,axiom,
( ( f4 @ b )
= ( g4 @ c ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotc1) ).
thf(f32,plain,
( ( f4 @ c )
!= ( g4 @ b ) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
thf(f10,axiom,
( ( f4 @ c )
!= ( g4 @ b ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotc2) ).
thf(f206,plain,
( ~ spl0_3
| ~ spl0_6 ),
inference(avatar_contradiction_clause,[status(thm)],[f205]) ).
thf(f205,plain,
( $false
| ~ spl0_3
| ~ spl0_6 ),
inference(trivial_inequality_removal,[status(thm)],[f204]) ).
thf(f204,plain,
( ( $true = $false )
| ~ spl0_3
| ~ spl0_6 ),
inference(backward_demodulation,[status(thm)],[f62,f72]) ).
thf(f62,plain,
( ( ( d @ $true )
= $true )
| ~ spl0_3 ),
inference(avatar_component_clause,[status(thm)],[f61]) ).
thf(f203,plain,
( ~ spl0_35
| ~ spl0_36 ),
inference(avatar_split_clause,[status(thm)],[f196,f201,f198]) ).
thf(f196,plain,
( ( ( f1 @ a )
!= ( f1 @ c ) )
| ( a != c ) ),
inference(constrained_superposition,[status(thm)],[f28,f43]) ).
thf(f43,plain,
( ( f1 @ a )
= ( g1 @ c ) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
thf(f3,axiom,
( ( f1 @ a )
= ( g1 @ c ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotc1) ).
thf(f28,plain,
( ( f1 @ c )
!= ( g1 @ a ) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
thf(f4,axiom,
( ( f1 @ c )
!= ( g1 @ a ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotc2) ).
thf(f195,plain,
( ~ spl0_33
| ~ spl0_34 ),
inference(avatar_split_clause,[status(thm)],[f188,f193,f190]) ).
thf(f188,plain,
( ( c != d )
| ( ( f7 @ c )
!= ( f7 @ d ) ) ),
inference(constrained_superposition,[status(thm)],[f42,f31]) ).
thf(f31,plain,
( ( f7 @ c )
= ( g7 @ d ) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f15,axiom,
( ( f7 @ c )
= ( g7 @ d ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnotd1) ).
thf(f42,plain,
( ( f7 @ d )
!= ( g7 @ c ) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
thf(f16,axiom,
( ( f7 @ d )
!= ( g7 @ c ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnotd2) ).
thf(f186,plain,
( spl0_9
| spl0_24
| spl0_32
| spl0_27 ),
inference(avatar_split_clause,[status(thm)],[f174,f157,f184,f145,f81]) ).
thf(f174,plain,
( ( sK4 = $true )
| ( $true
= ( e @ $false ) )
| ( $true
= ( d @ $false ) )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f173]) ).
thf(f173,plain,
( ( sK4 = $true )
| ( ( d @ $false )
!= ( e @ $false ) )
| spl0_27 ),
inference(cases_simplifying,[status(thm)],[f171]) ).
thf(f171,plain,
( ( ( e @ sK4 )
!= ( d @ sK4 ) )
| spl0_27 ),
inference(negative_extensionality,[status(thm)],[f158]) ).
thf(f182,plain,
( spl0_31
| spl0_23
| spl0_6
| spl0_27 ),
inference(avatar_split_clause,[status(thm)],[f177,f157,f71,f141,f179]) ).
thf(f177,plain,
( ( ( d @ $true )
= $false )
| ( ( e @ $true )
= $false )
| ( sK4 = $false )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f172]) ).
thf(f172,plain,
( ( sK4 = $false )
| ( ( d @ $true )
!= ( e @ $true ) )
| spl0_27 ),
inference(cases_simplifying,[status(thm)],[f171]) ).
thf(f181,plain,
( spl0_21
| spl0_31
| spl0_3
| spl0_27 ),
inference(avatar_split_clause,[status(thm)],[f176,f157,f61,f179,f134]) ).
thf(f176,plain,
( ( ( d @ $true )
= $true )
| ( $true
= ( e @ $true ) )
| ( sK4 = $false )
| spl0_27 ),
inference(binary_proxy_clausification,[status(thm)],[f172]) ).
thf(f170,plain,
( ~ spl0_29
| ~ spl0_30 ),
inference(avatar_split_clause,[status(thm)],[f163,f168,f165]) ).
thf(f163,plain,
( ( ( f8 @ c )
!= ( f8 @ e ) )
| ( c != e ) ),
inference(constrained_superposition,[status(thm)],[f38,f41]) ).
thf(f41,plain,
( ( f8 @ c )
= ( g8 @ e ) ),
inference(cnf_transformation,[status(thm)],[f17]) ).
thf(f17,axiom,
( ( f8 @ c )
= ( g8 @ e ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnote1) ).
thf(f38,plain,
( ( f8 @ e )
!= ( g8 @ c ) ),
inference(cnf_transformation,[status(thm)],[f18]) ).
thf(f18,axiom,
( ( f8 @ e )
!= ( g8 @ c ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnote2) ).
thf(f162,plain,
( ~ spl0_27
| ~ spl0_28 ),
inference(avatar_split_clause,[status(thm)],[f155,f160,f157]) ).
thf(f155,plain,
( ( d != e )
| ( ( f9 @ d )
!= ( f9 @ e ) ) ),
inference(constrained_superposition,[status(thm)],[f40,f39]) ).
thf(f39,plain,
( ( f9 @ d )
= ( g9 @ e ) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
thf(f19,axiom,
( ( f9 @ d )
= ( g9 @ e ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',dnote1) ).
thf(f40,plain,
( ( f9 @ e )
!= ( g9 @ d ) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
thf(f20,axiom,
( ( f9 @ e )
!= ( g9 @ d ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',dnote2) ).
thf(f125,plain,
( ~ spl0_19
| ~ spl0_20 ),
inference(avatar_split_clause,[status(thm)],[f118,f123,f120]) ).
thf(f118,plain,
( ( a != e )
| ( ( f3 @ a )
!= ( f3 @ e ) ) ),
inference(constrained_superposition,[status(thm)],[f37,f34]) ).
thf(f34,plain,
( ( f3 @ a )
= ( g3 @ e ) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
thf(f7,axiom,
( ( f3 @ a )
= ( g3 @ e ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anote1) ).
thf(f37,plain,
( ( f3 @ e )
!= ( g3 @ a ) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
thf(f8,axiom,
( ( f3 @ e )
!= ( g3 @ a ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anote2) ).
thf(f117,plain,
( ~ spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[status(thm)],[f110,f115,f112]) ).
thf(f110,plain,
( ( ( f6 @ b )
!= ( f6 @ e ) )
| ( b != e ) ),
inference(constrained_superposition,[status(thm)],[f35,f36]) ).
thf(f36,plain,
( ( f6 @ b )
= ( g6 @ e ) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f13,axiom,
( ( f6 @ b )
= ( g6 @ e ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnote1) ).
thf(f35,plain,
( ( f6 @ e )
!= ( g6 @ b ) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
thf(f14,axiom,
( ( f6 @ e )
!= ( g6 @ b ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnote2) ).
thf(f109,plain,
( ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[status(thm)],[f102,f107,f104]) ).
thf(f102,plain,
( ( ( f5 @ b )
!= ( f5 @ d ) )
| ( b != d ) ),
inference(constrained_superposition,[status(thm)],[f33,f26]) ).
thf(f26,plain,
( ( f5 @ b )
= ( g5 @ d ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,axiom,
( ( f5 @ b )
= ( g5 @ d ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotd1) ).
thf(f33,plain,
( ( f5 @ d )
!= ( g5 @ b ) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
thf(f12,axiom,
( ( f5 @ d )
!= ( g5 @ b ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotd2) ).
thf(f101,plain,
( ~ spl0_13
| ~ spl0_14 ),
inference(avatar_split_clause,[status(thm)],[f94,f99,f96]) ).
thf(f94,plain,
( ( ( f0 @ a )
!= ( f0 @ b ) )
| ( a != b ) ),
inference(constrained_superposition,[status(thm)],[f30,f29]) ).
thf(f29,plain,
( ( f0 @ a )
= ( g0 @ b ) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
thf(f1,axiom,
( ( f0 @ a )
= ( g0 @ b ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotb1) ).
thf(f30,plain,
( ( f0 @ b )
!= ( g0 @ a ) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
thf(f2,axiom,
( ( f0 @ b )
!= ( g0 @ a ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotb2) ).
thf(f93,plain,
( spl0_11
| spl0_8
| spl0_12
| spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f57,f47,f91,f78,f88]) ).
thf(f57,plain,
( ( ( d @ $false )
= $false )
| ( $true = sK2 )
| ( ( a @ $false )
= $false )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f55]) ).
thf(f55,plain,
( ( $true = sK2 )
| ( ( d @ $false )
!= ( a @ $false ) )
| spl0_1 ),
inference(cases_simplifying,[status(thm)],[f53]) ).
thf(f53,plain,
( ( ( a @ sK2 )
!= ( d @ sK2 ) )
| spl0_1 ),
inference(negative_extensionality,[status(thm)],[f48]) ).
thf(f76,plain,
( spl0_6
| spl0_4
| spl0_7
| spl0_1 ),
inference(avatar_split_clause,[status(thm)],[f59,f47,f74,f64,f71]) ).
thf(f59,plain,
( ( ( a @ $true )
= $false )
| ( ( d @ $true )
= $false )
| ( sK2 = $false )
| spl0_1 ),
inference(binary_proxy_clausification,[status(thm)],[f54]) ).
thf(f54,plain,
( ( sK2 = $false )
| ( ( d @ $true )
!= ( a @ $true ) )
| spl0_1 ),
inference(cases_simplifying,[status(thm)],[f53]) ).
thf(f52,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[status(thm)],[f45,f50,f47]) ).
thf(f45,plain,
( ( ( f2 @ a )
!= ( f2 @ d ) )
| ( a != d ) ),
inference(constrained_superposition,[status(thm)],[f27,f25]) ).
thf(f25,plain,
( ( f2 @ a )
= ( g2 @ d ) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
thf(f5,axiom,
( ( f2 @ a )
= ( g2 @ d ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotd1) ).
thf(f27,plain,
( ( f2 @ d )
!= ( g2 @ a ) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
thf(f6,axiom,
( ( f2 @ d )
!= ( g2 @ a ) ),
file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotd2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO505^1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.34 % Computer : n022.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue Feb 24 14:32:51 EST 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.31/0.46 ---- Original DTF file ---
% 0.31/0.46 thf(spec,logic,$$dhol).
% 0.31/0.46 %------------------------------------------------------------------------------
% 0.31/0.46 % File : SYO505^1 : TPTP v9.2.1. Released v4.1.0.
% 0.31/0.46 % Domain : Syntactic
% 0.31/0.46 % Problem : Explosive confrontation
% 0.31/0.46 % Version : Especial.
% 0.31/0.46 % English : The Mensa Example at type oo: There are not 5 distinct values of
% 0.31/0.46 % type oo.
% 0.31/0.46
% 0.31/0.46 % Refs : [Bro09] Brown E. (2009), Email to Geoff Sutcliffe
% 0.31/0.46 % : [Hoe09] Hoeschele (2009), Towards a Semi-Automatic Higher-Orde
% 0.31/0.46 % Source : [Bro09]
% 0.31/0.46 % Names : basic18 [Bro09]
% 0.31/0.46
% 0.31/0.46 % Status : ContradictoryAxioms
% 0.31/0.46 % Rating : 0.33 v9.1.0, 0.38 v9.0.0, 0.40 v8.2.0, 0.54 v8.1.0, 0.55 v7.5.0, 0.71 v7.4.0, 0.78 v7.2.0, 0.75 v7.0.0, 0.71 v6.4.0, 0.67 v6.3.0, 0.80 v6.2.0, 0.86 v5.5.0, 0.83 v5.4.0, 0.80 v4.1.0
% 0.31/0.46 % Syntax : Number of formulae : 46 ( 21 unt; 25 typ; 0 def)
% 0.31/0.46 % Number of atoms : 61 ( 20 equ; 0 cnn)
% 0.31/0.46 % Maximal formula atoms : 1 ( 2 avg)
% 0.31/0.46 % Number of connectives : 50 ( 10 ~; 0 |; 0 &; 40 @)
% 0.31/0.46 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.31/0.46 % Maximal formula depth : 2 ( 1 avg)
% 0.31/0.46 % Number of types : 2 ( 0 usr)
% 0.31/0.46 % Number of type conns : 45 ( 45 >; 0 *; 0 +; 0 <<)
% 0.31/0.46 % Number of symbols : 27 ( 25 usr; 1 con; 0-2 aty)
% 0.31/0.46 % Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% 0.31/0.46 % SPC : TH0_THM_EQU_NAR
% 0.31/0.46
% 0.31/0.46 % Comments :
% 0.31/0.46 %------------------------------------------------------------------------------
% 0.31/0.46 thf(a,type,
% 0.31/0.46 a: $o > $o ).
% 0.31/0.46
% 0.31/0.46 thf(b,type,
% 0.31/0.46 b: $o > $o ).
% 0.31/0.46
% 0.31/0.46 thf(c,type,
% 0.31/0.46 c: $o > $o ).
% 0.31/0.46
% 0.31/0.46 thf(d,type,
% 0.31/0.46 d: $o > $o ).
% 0.31/0.46
% 0.31/0.46 thf(e,type,
% 0.31/0.46 e: $o > $o ).
% 0.31/0.46
% 0.31/0.46 thf(f0,type,
% 0.31/0.46 f0: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g0,type,
% 0.31/0.46 g0: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f1,type,
% 0.31/0.46 f1: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g1,type,
% 0.31/0.46 g1: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f2,type,
% 0.31/0.46 f2: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g2,type,
% 0.31/0.46 g2: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f3,type,
% 0.31/0.46 f3: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g3,type,
% 0.31/0.46 g3: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f4,type,
% 0.31/0.46 f4: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g4,type,
% 0.31/0.46 g4: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f5,type,
% 0.31/0.46 f5: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g5,type,
% 0.31/0.46 g5: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f6,type,
% 0.31/0.46 f6: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g6,type,
% 0.31/0.46 g6: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f7,type,
% 0.31/0.46 f7: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g7,type,
% 0.31/0.46 g7: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f8,type,
% 0.31/0.46 f8: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g8,type,
% 0.31/0.46 g8: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(f9,type,
% 0.31/0.46 f9: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(g9,type,
% 0.31/0.46 g9: ( $o > $o ) > $i ).
% 0.31/0.46
% 0.31/0.46 thf(anotb1,axiom,
% 0.31/0.46 ( ( f0 @ a )
% 0.31/0.46 = ( g0 @ b ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anotb2,axiom,
% 0.31/0.46 ( ( f0 @ b )
% 0.31/0.46 != ( g0 @ a ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anotc1,axiom,
% 0.31/0.46 ( ( f1 @ a )
% 0.31/0.46 = ( g1 @ c ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anotc2,axiom,
% 0.31/0.46 ( ( f1 @ c )
% 0.31/0.46 != ( g1 @ a ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anotd1,axiom,
% 0.31/0.46 ( ( f2 @ a )
% 0.31/0.46 = ( g2 @ d ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anotd2,axiom,
% 0.31/0.46 ( ( f2 @ d )
% 0.31/0.46 != ( g2 @ a ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anote1,axiom,
% 0.31/0.46 ( ( f3 @ a )
% 0.31/0.46 = ( g3 @ e ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(anote2,axiom,
% 0.31/0.46 ( ( f3 @ e )
% 0.31/0.46 != ( g3 @ a ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnotc1,axiom,
% 0.31/0.46 ( ( f4 @ b )
% 0.31/0.46 = ( g4 @ c ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnotc2,axiom,
% 0.31/0.46 ( ( f4 @ c )
% 0.31/0.46 != ( g4 @ b ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnotd1,axiom,
% 0.31/0.46 ( ( f5 @ b )
% 0.31/0.46 = ( g5 @ d ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnotd2,axiom,
% 0.31/0.46 ( ( f5 @ d )
% 0.31/0.46 != ( g5 @ b ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnote1,axiom,
% 0.31/0.46 ( ( f6 @ b )
% 0.31/0.46 = ( g6 @ e ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(bnote2,axiom,
% 0.31/0.46 ( ( f6 @ e )
% 0.31/0.46 != ( g6 @ b ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(cnotd1,axiom,
% 0.31/0.46 ( ( f7 @ c )
% 0.31/0.46 = ( g7 @ d ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(cnotd2,axiom,
% 0.31/0.46 ( ( f7 @ d )
% 0.31/0.46 != ( g7 @ c ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(cnote1,axiom,
% 0.31/0.46 ( ( f8 @ c )
% 0.31/0.46 = ( g8 @ e ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(cnote2,axiom,
% 0.31/0.46 ( ( f8 @ e )
% 0.31/0.46 != ( g8 @ c ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(dnote1,axiom,
% 0.31/0.46 ( ( f9 @ d )
% 0.31/0.46 = ( g9 @ e ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(dnote2,axiom,
% 0.31/0.46 ( ( f9 @ e )
% 0.31/0.46 != ( g9 @ d ) ) ).
% 0.31/0.46
% 0.31/0.46 thf(mensaoo,conjecture,
% 0.31/0.46 $false ).
% 0.31/0.46
% 0.31/0.46 %------------------------------------------------------------------------------
% 0.31/0.46 ------------------------
% 1.61/1.39 ---- Embedded in THF ---
% 1.61/1.39 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.61/1.39 %%% Generated on Tue Feb 24 14:32:52 EST 2026
% 1.61/1.39 %%% using '$$dhol' embedding, version 1.3.0.
% 1.61/1.39 %%% Logic specification used:
% 1.61/1.39 %%% thf(spec, logic, $$dhol).
% 1.61/1.39
% 1.61/1.39 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2DTF17938.p
% See solution above
% 1.61/1.39 ------------------------
% 1.78/1.40 ---- Cleaned THF ---
% 1.78/1.40 thf(a,type,
% 1.78/1.40 a: $o > $o ).
% 1.78/1.40
% 1.78/1.40 thf(b,type,
% 1.78/1.40 b: $o > $o ).
% 1.78/1.40
% 1.78/1.40 thf(c,type,
% 1.78/1.40 c: $o > $o ).
% 1.78/1.40
% 1.78/1.40 thf(d,type,
% 1.78/1.40 d: $o > $o ).
% 1.78/1.40
% 1.78/1.40 thf(e,type,
% 1.78/1.40 e: $o > $o ).
% 1.78/1.40
% 1.78/1.40 thf(f0,type,
% 1.78/1.40 f0: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g0,type,
% 1.78/1.40 g0: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f1,type,
% 1.78/1.40 f1: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g1,type,
% 1.78/1.40 g1: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f2,type,
% 1.78/1.40 f2: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g2,type,
% 1.78/1.40 g2: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f3,type,
% 1.78/1.40 f3: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g3,type,
% 1.78/1.40 g3: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f4,type,
% 1.78/1.40 f4: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g4,type,
% 1.78/1.40 g4: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f5,type,
% 1.78/1.40 f5: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g5,type,
% 1.78/1.40 g5: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f6,type,
% 1.78/1.40 f6: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g6,type,
% 1.78/1.40 g6: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f7,type,
% 1.78/1.40 f7: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g7,type,
% 1.78/1.40 g7: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f8,type,
% 1.78/1.40 f8: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g8,type,
% 1.78/1.40 g8: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(f9,type,
% 1.78/1.40 f9: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(g9,type,
% 1.78/1.40 g9: ( $o > $o ) > $i ).
% 1.78/1.40
% 1.78/1.40 thf(anotb1,axiom,
% 1.78/1.40 ( ( f0 @ a )
% 1.78/1.40 = ( g0 @ b ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anotb2,axiom,
% 1.78/1.40 ( ( f0 @ b )
% 1.78/1.40 != ( g0 @ a ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anotc1,axiom,
% 1.78/1.40 ( ( f1 @ a )
% 1.78/1.40 = ( g1 @ c ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anotc2,axiom,
% 1.78/1.40 ( ( f1 @ c )
% 1.78/1.40 != ( g1 @ a ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anotd1,axiom,
% 1.78/1.40 ( ( f2 @ a )
% 1.78/1.40 = ( g2 @ d ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anotd2,axiom,
% 1.78/1.40 ( ( f2 @ d )
% 1.78/1.40 != ( g2 @ a ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anote1,axiom,
% 1.78/1.40 ( ( f3 @ a )
% 1.78/1.40 = ( g3 @ e ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(anote2,axiom,
% 1.78/1.40 ( ( f3 @ e )
% 1.78/1.40 != ( g3 @ a ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnotc1,axiom,
% 1.78/1.40 ( ( f4 @ b )
% 1.78/1.40 = ( g4 @ c ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnotc2,axiom,
% 1.78/1.40 ( ( f4 @ c )
% 1.78/1.40 != ( g4 @ b ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnotd1,axiom,
% 1.78/1.40 ( ( f5 @ b )
% 1.78/1.40 = ( g5 @ d ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnotd2,axiom,
% 1.78/1.40 ( ( f5 @ d )
% 1.78/1.40 != ( g5 @ b ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnote1,axiom,
% 1.78/1.40 ( ( f6 @ b )
% 1.78/1.40 = ( g6 @ e ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(bnote2,axiom,
% 1.78/1.40 ( ( f6 @ e )
% 1.78/1.40 != ( g6 @ b ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(cnotd1,axiom,
% 1.78/1.40 ( ( f7 @ c )
% 1.78/1.40 = ( g7 @ d ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(cnotd2,axiom,
% 1.78/1.40 ( ( f7 @ d )
% 1.78/1.40 != ( g7 @ c ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(cnote1,axiom,
% 1.78/1.40 ( ( f8 @ c )
% 1.78/1.40 = ( g8 @ e ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(cnote2,axiom,
% 1.78/1.40 ( ( f8 @ e )
% 1.78/1.40 != ( g8 @ c ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(dnote1,axiom,
% 1.78/1.40 ( ( f9 @ d )
% 1.78/1.40 = ( g9 @ e ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(dnote2,axiom,
% 1.78/1.40 ( ( f9 @ e )
% 1.78/1.40 != ( g9 @ d ) ) ).
% 1.78/1.40
% 1.78/1.40 thf(mensaoo,conjecture,
% 1.78/1.40 $false ).
% 1.78/1.40 ------------------------
% 1.78/1.41 % (18215)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/18Mi)
% 1.78/1.42 % (18210)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_17938 for (2999ds/4Mi)
% 1.78/1.42 % (18209)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/183Mi)
% 1.78/1.42 % (18211)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_17938 for (2999ds/27Mi)
% 1.78/1.42 % (18212)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/2Mi)
% 1.78/1.42 % (18213)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_17938 for (2999ds/2Mi)
% 1.78/1.42 % (18214)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_17938 for (2999ds/275Mi)
% 1.78/1.42 % (18212)Instruction limit reached!
% 1.78/1.42 % (18212)------------------------------
% 1.78/1.42 % (18212)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18212)Termination reason: Unknown
% 1.78/1.42 % (18212)Termination phase: Saturation
% 1.78/1.42
% 1.78/1.42 % (18212)Memory used [KB]: 1023
% 1.78/1.42 % (18212)Time elapsed: 0.003 s
% 1.78/1.42 % (18212)Instructions burned: 2 (million)
% 1.78/1.42 % (18212)------------------------------
% 1.78/1.42 % (18212)------------------------------
% 1.78/1.42 % (18213)Instruction limit reached!
% 1.78/1.42 % (18213)------------------------------
% 1.78/1.42 % (18213)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18213)Termination reason: Unknown
% 1.78/1.42 % (18213)Termination phase: Saturation
% 1.78/1.42
% 1.78/1.42 % (18213)Memory used [KB]: 1023
% 1.78/1.42 % (18213)Time elapsed: 0.003 s
% 1.78/1.42 % (18213)Instructions burned: 2 (million)
% 1.78/1.42 % (18213)------------------------------
% 1.78/1.42 % (18213)------------------------------
% 1.78/1.42 % (18215)Instruction limit reached!
% 1.78/1.42 % (18215)------------------------------
% 1.78/1.42 % (18215)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18215)Termination reason: Unknown
% 1.78/1.42 % (18215)Termination phase: Saturation
% 1.78/1.42
% 1.78/1.42 % (18215)Memory used [KB]: 5628
% 1.78/1.42 % (18215)Time elapsed: 0.009 s
% 1.78/1.42 % (18214)Refutation not found, incomplete strategy
% 1.78/1.42 % (18214)------------------------------
% 1.78/1.42 % (18214)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18215)Instructions burned: 19 (million)
% 1.78/1.42 % (18215)------------------------------
% 1.78/1.42 % (18215)------------------------------
% 1.78/1.42 % (18214)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.42
% 1.78/1.42
% 1.78/1.42 % (18214)Memory used [KB]: 5500
% 1.78/1.42 % (18214)Time elapsed: 0.003 s
% 1.78/1.42 % (18214)Instructions burned: 1 (million)
% 1.78/1.42 % (18214)------------------------------
% 1.78/1.42 % (18214)------------------------------
% 1.78/1.42 % (18210)Instruction limit reached!
% 1.78/1.42 % (18210)------------------------------
% 1.78/1.42 % (18210)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18210)Termination reason: Unknown
% 1.78/1.42 % (18210)Termination phase: Saturation
% 1.78/1.42
% 1.78/1.42 % (18210)Memory used [KB]: 5500
% 1.78/1.42 % (18210)Time elapsed: 0.005 s
% 1.78/1.42 % (18210)Instructions burned: 4 (million)
% 1.78/1.42 % (18210)------------------------------
% 1.78/1.42 % (18210)------------------------------
% 1.78/1.42 % (18211)Refutation not found, incomplete strategy
% 1.78/1.42 % (18211)------------------------------
% 1.78/1.42 % (18211)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.42 % (18211)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.42
% 1.78/1.42
% 1.78/1.42 % (18211)Memory used [KB]: 5500
% 1.78/1.42 % (18211)Time elapsed: 0.005 s
% 1.78/1.42 % (18211)Instructions burned: 4 (million)
% 1.78/1.42 % (18211)------------------------------
% 1.78/1.42 % (18211)------------------------------
% 1.78/1.43 % (18216)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/3Mi)
% 1.78/1.43 % (18216)Instruction limit reached!
% 1.78/1.43 % (18216)------------------------------
% 1.78/1.43 % (18216)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.43 % (18216)Termination reason: Unknown
% 1.78/1.43 % (18216)Termination phase: Saturation
% 1.78/1.43
% 1.78/1.43 % (18216)Memory used [KB]: 5500
% 1.78/1.43 % (18216)Time elapsed: 0.003 s
% 1.78/1.43 % (18216)Instructions burned: 3 (million)
% 1.78/1.43 % (18216)------------------------------
% 1.78/1.43 % (18216)------------------------------
% 1.78/1.44 % (18217)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_17938 for (2999ds/37Mi)
% 1.78/1.44 % (18218)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_17938 for (2999ds/15Mi)
% 1.78/1.44 % (18219)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_17938 for (2999ds/3Mi)
% 1.78/1.44 % (18218)Refutation not found, incomplete strategy
% 1.78/1.44 % (18218)------------------------------
% 1.78/1.44 % (18218)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.44 % (18218)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.44
% 1.78/1.44
% 1.78/1.44 % (18218)Memory used [KB]: 5500
% 1.78/1.44 % (18218)Time elapsed: 0.003 s
% 1.78/1.44 % (18218)Instructions burned: 2 (million)
% 1.78/1.44 % (18218)------------------------------
% 1.78/1.44 % (18218)------------------------------
% 1.78/1.44 % (18220)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_17938 for (2999ds/1041Mi)
% 1.78/1.44 % (18219)Instruction limit reached!
% 1.78/1.44 % (18219)------------------------------
% 1.78/1.44 % (18219)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.44 % (18219)Termination reason: Unknown
% 1.78/1.44 % (18219)Termination phase: Saturation
% 1.78/1.44
% 1.78/1.44 % (18219)Memory used [KB]: 5500
% 1.78/1.44 % (18219)Time elapsed: 0.004 s
% 1.78/1.44 % (18219)Instructions burned: 3 (million)
% 1.78/1.44 % (18219)------------------------------
% 1.78/1.44 % (18219)------------------------------
% 1.78/1.44 % (18221)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/7Mi)
% 1.78/1.44 % (18222)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/16Mi)
% 1.78/1.44 % (18220)Refutation not found, incomplete strategy
% 1.78/1.44 % (18220)------------------------------
% 1.78/1.44 % (18220)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.44 % (18220)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.44
% 1.78/1.44
% 1.78/1.44 % (18220)Memory used [KB]: 5500
% 1.78/1.44 % (18220)Time elapsed: 0.005 s
% 1.78/1.44 % (18220)Instructions burned: 5 (million)
% 1.78/1.44 % (18220)------------------------------
% 1.78/1.44 % (18220)------------------------------
% 1.78/1.45 % (18221)Instruction limit reached!
% 1.78/1.45 % (18221)------------------------------
% 1.78/1.45 % (18221)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.45 % (18221)Termination reason: Unknown
% 1.78/1.45 % (18221)Termination phase: Saturation
% 1.78/1.45
% 1.78/1.45 % (18221)Memory used [KB]: 1023
% 1.78/1.45 % (18221)Time elapsed: 0.006 s
% 1.78/1.45 % (18221)Instructions burned: 7 (million)
% 1.78/1.45 % (18221)------------------------------
% 1.78/1.45 % (18221)------------------------------
% 1.78/1.45 % (18222)Instruction limit reached!
% 1.78/1.45 % (18222)------------------------------
% 1.78/1.45 % (18222)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.45 % (18222)Termination reason: Unknown
% 1.78/1.45 % (18222)Termination phase: Saturation
% 1.78/1.45
% 1.78/1.45 % (18222)Memory used [KB]: 5756
% 1.78/1.45 % (18222)Time elapsed: 0.008 s
% 1.78/1.45 % (18222)Instructions burned: 16 (million)
% 1.78/1.45 % (18222)------------------------------
% 1.78/1.45 % (18222)------------------------------
% 1.78/1.46 % (18223)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_17938 for (2999ds/3Mi)
% 1.78/1.46 % (18224)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_17938 for (2999ds/3Mi)
% 1.78/1.46 % (18227)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/4Mi)
% 1.78/1.46 % (18223)Instruction limit reached!
% 1.78/1.46 % (18223)------------------------------
% 1.78/1.46 % (18223)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18223)Termination reason: Unknown
% 1.78/1.46 % (18223)Termination phase: Saturation
% 1.78/1.46
% 1.78/1.46 % (18223)Memory used [KB]: 5500
% 1.78/1.46 % (18223)Time elapsed: 0.004 s
% 1.78/1.46 % (18223)Instructions burned: 3 (million)
% 1.78/1.46 % (18223)------------------------------
% 1.78/1.46 % (18223)------------------------------
% 1.78/1.46 % (18224)Instruction limit reached!
% 1.78/1.46 % (18224)------------------------------
% 1.78/1.46 % (18224)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18224)Termination reason: Unknown
% 1.78/1.46 % (18224)Termination phase: Saturation
% 1.78/1.46
% 1.78/1.46 % (18224)Memory used [KB]: 1023
% 1.78/1.46 % (18224)Time elapsed: 0.004 s
% 1.78/1.46 % (18224)Instructions burned: 4 (million)
% 1.78/1.46 % (18224)------------------------------
% 1.78/1.46 % (18224)------------------------------
% 1.78/1.46 % (18226)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/3Mi)
% 1.78/1.46 % (18227)Instruction limit reached!
% 1.78/1.46 % (18227)------------------------------
% 1.78/1.46 % (18227)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18227)Termination reason: Unknown
% 1.78/1.46 % (18227)Termination phase: Saturation
% 1.78/1.46
% 1.78/1.46 % (18227)Memory used [KB]: 5500
% 1.78/1.46 % (18227)Time elapsed: 0.004 s
% 1.78/1.46 % (18227)Instructions burned: 6 (million)
% 1.78/1.46 % (18227)------------------------------
% 1.78/1.46 % (18227)------------------------------
% 1.78/1.46 % (18225)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/7Mi)
% 1.78/1.46 % (18217)Instruction limit reached!
% 1.78/1.46 % (18217)------------------------------
% 1.78/1.46 % (18217)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18217)Termination reason: Unknown
% 1.78/1.46 % (18217)Termination phase: Saturation
% 1.78/1.46
% 1.78/1.46 % (18217)Memory used [KB]: 5756
% 1.78/1.46 % (18217)Time elapsed: 0.025 s
% 1.78/1.46 % (18217)Instructions burned: 37 (million)
% 1.78/1.46 % (18217)------------------------------
% 1.78/1.46 % (18217)------------------------------
% 1.78/1.46 % (18226)Instruction limit reached!
% 1.78/1.46 % (18226)------------------------------
% 1.78/1.46 % (18226)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18226)Termination reason: Unknown
% 1.78/1.46 % (18226)Termination phase: Saturation
% 1.78/1.46
% 1.78/1.46 % (18226)Memory used [KB]: 5500
% 1.78/1.46 % (18226)Time elapsed: 0.003 s
% 1.78/1.46 % (18226)Instructions burned: 3 (million)
% 1.78/1.46 % (18226)------------------------------
% 1.78/1.46 % (18226)------------------------------
% 1.78/1.46 % (18225)Refutation not found, incomplete strategy
% 1.78/1.46 % (18225)------------------------------
% 1.78/1.46 % (18225)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.46 % (18225)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.46
% 1.78/1.46
% 1.78/1.46 % (18225)Memory used [KB]: 5500
% 1.78/1.46 % (18225)Time elapsed: 0.004 s
% 1.78/1.46 % (18225)Instructions burned: 3 (million)
% 1.78/1.46 % (18225)------------------------------
% 1.78/1.46 % (18225)------------------------------
% 1.78/1.47 % (18232)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/21Mi)
% 1.78/1.47 % (18232)Refutation not found, incomplete strategy
% 1.78/1.47 % (18232)------------------------------
% 1.78/1.47 % (18232)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.47 % (18232)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.47
% 1.78/1.47
% 1.78/1.47 % (18232)Memory used [KB]: 5500
% 1.78/1.47 % (18232)Time elapsed: 0.002 s
% 1.78/1.47 % (18232)Instructions burned: 1 (million)
% 1.78/1.47 % (18232)------------------------------
% 1.78/1.47 % (18232)------------------------------
% 1.78/1.47 % (18231)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/902Mi)
% 1.78/1.47 % (18231)Refutation not found, incomplete strategy
% 1.78/1.47 % (18231)------------------------------
% 1.78/1.47 % (18231)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.47 % (18231)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.47
% 1.78/1.47
% 1.78/1.47 % (18231)Memory used [KB]: 5500
% 1.78/1.47 % (18231)Time elapsed: 0.001 s
% 1.78/1.47 % (18231)Instructions burned: 1 (million)
% 1.78/1.47 % (18231)------------------------------
% 1.78/1.47 % (18231)------------------------------
% 1.78/1.48 % (18228)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/18Mi)
% 1.78/1.48 % (18229)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/710Mi)
% 1.78/1.48 % (18229)Refutation not found, incomplete strategy
% 1.78/1.48 % (18229)------------------------------
% 1.78/1.48 % (18229)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.48 % (18229)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.48
% 1.78/1.48
% 1.78/1.48 % (18229)Memory used [KB]: 5500
% 1.78/1.48 % (18229)Time elapsed: 0.002 s
% 1.78/1.48 % (18229)Instructions burned: 1 (million)
% 1.78/1.48 % (18229)------------------------------
% 1.78/1.48 % (18229)------------------------------
% 1.78/1.48 % (18230)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/6Mi)
% 1.78/1.48 % (18228)Refutation not found, incomplete strategy
% 1.78/1.48 % (18228)------------------------------
% 1.78/1.48 % (18228)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.48 % (18228)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.48
% 1.78/1.48
% 1.78/1.48 % (18228)Memory used [KB]: 5500
% 1.78/1.48 % (18228)Time elapsed: 0.005 s
% 1.78/1.48 % (18228)Instructions burned: 4 (million)
% 1.78/1.48 % (18228)------------------------------
% 1.78/1.48 % (18228)------------------------------
% 1.78/1.48 % (18233)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/5Mi)
% 1.78/1.48 % (18230)Instruction limit reached!
% 1.78/1.48 % (18230)------------------------------
% 1.78/1.48 % (18230)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.48 % (18230)Termination reason: Unknown
% 1.78/1.48 % (18230)Termination phase: Saturation
% 1.78/1.48
% 1.78/1.48 % (18230)Memory used [KB]: 5500
% 1.78/1.48 % (18230)Time elapsed: 0.006 s
% 1.78/1.48 % (18230)Instructions burned: 6 (million)
% 1.78/1.48 % (18230)------------------------------
% 1.78/1.48 % (18230)------------------------------
% 1.78/1.48 % (18234)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/6Mi)
% 1.78/1.48 % (18234)Refutation not found, incomplete strategy
% 1.78/1.48 % (18234)------------------------------
% 1.78/1.48 % (18234)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.48 % (18234)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.48
% 1.78/1.48
% 1.78/1.48 % (18234)Memory used [KB]: 5500
% 1.78/1.48 % (18234)Time elapsed: 0.002 s
% 1.78/1.48 % (18234)Instructions burned: 1 (million)
% 1.78/1.48 % (18234)------------------------------
% 1.78/1.48 % (18234)------------------------------
% 1.78/1.48 % (18235)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/377Mi)
% 1.78/1.49 % (18233)Instruction limit reached!
% 1.78/1.49 % (18233)------------------------------
% 1.78/1.49 % (18233)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.49 % (18233)Termination reason: Unknown
% 1.78/1.49 % (18233)Termination phase: Saturation
% 1.78/1.49
% 1.78/1.49 % (18233)Memory used [KB]: 5500
% 1.78/1.49 % (18233)Time elapsed: 0.005 s
% 1.78/1.49 % (18233)Instructions burned: 5 (million)
% 1.78/1.49 % (18233)------------------------------
% 1.78/1.49 % (18233)------------------------------
% 1.78/1.49 % (18235)Refutation not found, incomplete strategy
% 1.78/1.49 % (18235)------------------------------
% 1.78/1.49 % (18235)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.78/1.49 % (18235)Termination reason: Refutation not found, incomplete strategy
% 1.78/1.49
% 1.78/1.49
% 1.78/1.49 % (18235)Memory used [KB]: 5500
% 1.78/1.49 % (18235)Time elapsed: 0.003 s
% 1.78/1.49 % (18235)Instructions burned: 3 (million)
% 1.78/1.49 % (18235)------------------------------
% 1.78/1.49 % (18235)------------------------------
% 1.78/1.49 % (18239)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/17Mi)
% 1.80/1.50 % (18241)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/30Mi)
% 1.80/1.50 % (18236)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/779Mi)
% 1.80/1.50 % (18236)Refutation not found, incomplete strategy
% 1.80/1.50 % (18236)------------------------------
% 1.80/1.50 % (18236)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18236)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.50
% 1.80/1.50
% 1.80/1.50 % (18236)Memory used [KB]: 5500
% 1.80/1.50 % (18236)Time elapsed: 0.003 s
% 1.80/1.50 % (18236)Instructions burned: 2 (million)
% 1.80/1.50 % (18236)------------------------------
% 1.80/1.50 % (18236)------------------------------
% 1.80/1.50 % (18237)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/19Mi)
% 1.80/1.50 % (18237)Refutation not found, incomplete strategy
% 1.80/1.50 % (18237)------------------------------
% 1.80/1.50 % (18237)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18237)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.50
% 1.80/1.50
% 1.80/1.50 % (18237)Memory used [KB]: 5500
% 1.80/1.50 % (18237)Time elapsed: 0.003 s
% 1.80/1.50 % (18237)Instructions burned: 1 (million)
% 1.80/1.50 % (18237)------------------------------
% 1.80/1.50 % (18237)------------------------------
% 1.80/1.50 % (18241)Refutation not found, incomplete strategy
% 1.80/1.50 % (18241)------------------------------
% 1.80/1.50 % (18241)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18241)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.50
% 1.80/1.50
% 1.80/1.50 % (18241)Memory used [KB]: 5628
% 1.80/1.50 % (18241)Time elapsed: 0.005 s
% 1.80/1.50 % (18241)Instructions burned: 8 (million)
% 1.80/1.50 % (18241)------------------------------
% 1.80/1.50 % (18241)------------------------------
% 1.80/1.50 % (18238)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/879Mi)
% 1.80/1.50 % (18209)Instruction limit reached!
% 1.80/1.50 % (18209)------------------------------
% 1.80/1.50 % (18209)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18209)Termination reason: Unknown
% 1.80/1.50 % (18209)Termination phase: Saturation
% 1.80/1.50
% 1.80/1.50 % (18209)Memory used [KB]: 7291
% 1.80/1.50 % (18209)Time elapsed: 0.083 s
% 1.80/1.50 % (18209)Instructions burned: 184 (million)
% 1.80/1.50 % (18209)------------------------------
% 1.80/1.50 % (18209)------------------------------
% 1.80/1.50 % (18238)Refutation not found, incomplete strategy
% 1.80/1.50 % (18238)------------------------------
% 1.80/1.50 % (18238)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18238)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.50
% 1.80/1.50
% 1.80/1.50 % (18238)Memory used [KB]: 5500
% 1.80/1.50 % (18238)Time elapsed: 0.003 s
% 1.80/1.50 % (18238)Instructions burned: 2 (million)
% 1.80/1.50 % (18238)------------------------------
% 1.80/1.50 % (18238)------------------------------
% 1.80/1.50 % (18239)Instruction limit reached!
% 1.80/1.50 % (18239)------------------------------
% 1.80/1.50 % (18239)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18239)Termination reason: Unknown
% 1.80/1.50 % (18239)Termination phase: Saturation
% 1.80/1.50
% 1.80/1.50 % (18239)Memory used [KB]: 5756
% 1.80/1.50 % (18239)Time elapsed: 0.009 s
% 1.80/1.50 % (18239)Instructions burned: 18 (million)
% 1.80/1.50 % (18239)------------------------------
% 1.80/1.50 % (18239)------------------------------
% 1.80/1.50 % (18240)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/3Mi)
% 1.80/1.50 % (18240)Instruction limit reached!
% 1.80/1.50 % (18240)------------------------------
% 1.80/1.50 % (18240)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.50 % (18240)Termination reason: Unknown
% 1.80/1.50 % (18240)Termination phase: Saturation
% 1.80/1.50
% 1.80/1.50 % (18240)Memory used [KB]: 1023
% 1.80/1.50 % (18240)Time elapsed: 0.004 s
% 1.80/1.50 % (18240)Instructions burned: 4 (million)
% 1.80/1.50 % (18240)------------------------------
% 1.80/1.50 % (18240)------------------------------
% 1.80/1.51 % (18244)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/3Mi)
% 1.80/1.51 % (18245)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/20Mi)
% 1.80/1.51 % (18245)Refutation not found, incomplete strategy
% 1.80/1.51 % (18245)------------------------------
% 1.80/1.51 % (18245)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.51 % (18245)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.51
% 1.80/1.51
% 1.80/1.51 % (18245)Memory used [KB]: 5500
% 1.80/1.51 % (18245)Time elapsed: 0.002 s
% 1.80/1.51 % (18245)Instructions burned: 1 (million)
% 1.80/1.51 % (18245)------------------------------
% 1.80/1.51 % (18245)------------------------------
% 1.80/1.51 % (18246)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/86Mi)
% 1.80/1.51 % (18244)Instruction limit reached!
% 1.80/1.51 % (18244)------------------------------
% 1.80/1.51 % (18244)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.51 % (18244)Termination reason: Unknown
% 1.80/1.51 % (18244)Termination phase: Saturation
% 1.80/1.51
% 1.80/1.51 % (18244)Memory used [KB]: 5500
% 1.80/1.51 % (18244)Time elapsed: 0.003 s
% 1.80/1.51 % (18244)Instructions burned: 3 (million)
% 1.80/1.51 % (18244)------------------------------
% 1.80/1.51 % (18244)------------------------------
% 1.80/1.52 % (18242)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/127Mi)
% 1.80/1.52 % (18243)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/100Mi)
% 1.80/1.52 % (18247)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/107Mi)
% 1.80/1.52 % (18247)Refutation not found, incomplete strategy
% 1.80/1.52 % (18247)------------------------------
% 1.80/1.52 % (18247)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.52 % (18247)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.52
% 1.80/1.52
% 1.80/1.52 % (18247)Memory used [KB]: 5500
% 1.80/1.52 % (18247)Time elapsed: 0.002 s
% 1.80/1.52 % (18247)Instructions burned: 1 (million)
% 1.80/1.52 % (18247)------------------------------
% 1.80/1.52 % (18247)------------------------------
% 1.80/1.52 % (18243)Refutation not found, incomplete strategy
% 1.80/1.52 % (18243)------------------------------
% 1.80/1.52 % (18243)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.52 % (18243)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.52
% 1.80/1.52
% 1.80/1.52 % (18243)Memory used [KB]: 5500
% 1.80/1.52 % (18243)Time elapsed: 0.005 s
% 1.80/1.52 % (18243)Instructions burned: 5 (million)
% 1.80/1.52 % (18243)------------------------------
% 1.80/1.52 % (18243)------------------------------
% 1.80/1.52 % (18248)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/39Mi)
% 1.80/1.52 % (18249)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/448Mi)
% 1.80/1.52 % (18250)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_17938 for (2999ds/46Mi)
% 1.80/1.52 % (18250)Refutation not found, incomplete strategy
% 1.80/1.52 % (18250)------------------------------
% 1.80/1.52 % (18250)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.52 % (18250)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.52
% 1.80/1.52
% 1.80/1.52 % (18250)Memory used [KB]: 5500
% 1.80/1.52 % (18250)Time elapsed: 0.002 s
% 1.80/1.52 % (18250)Instructions burned: 1 (million)
% 1.80/1.52 % (18250)------------------------------
% 1.80/1.52 % (18250)------------------------------
% 1.80/1.52 % (18249)Refutation not found, incomplete strategy
% 1.80/1.52 % (18249)------------------------------
% 1.80/1.52 % (18249)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.52 % (18249)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.52
% 1.80/1.52
% 1.80/1.52 % (18249)Memory used [KB]: 5500
% 1.80/1.52 % (18249)Time elapsed: 0.002 s
% 1.80/1.52 % (18249)Instructions burned: 1 (million)
% 1.80/1.52 % (18249)------------------------------
% 1.80/1.52 % (18249)------------------------------
% 1.80/1.52 % (18248)Refutation not found, incomplete strategy
% 1.80/1.52 % (18248)------------------------------
% 1.80/1.52 % (18248)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.52 % (18248)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.52
% 1.80/1.52
% 1.80/1.52 % (18248)Memory used [KB]: 5500
% 1.80/1.52 % (18248)Time elapsed: 0.004 s
% 1.80/1.52 % (18248)Instructions burned: 4 (million)
% 1.80/1.52 % (18248)------------------------------
% 1.80/1.52 % (18248)------------------------------
% 1.80/1.53 % (18253)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/149Mi)
% 1.80/1.53 % (18254)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/39Mi)
% 1.80/1.53 % (18254)Refutation not found, incomplete strategy
% 1.80/1.53 % (18254)------------------------------
% 1.80/1.53 % (18254)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.53 % (18254)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.53
% 1.80/1.53
% 1.80/1.53 % (18254)Memory used [KB]: 5500
% 1.80/1.53 % (18254)Time elapsed: 0.003 s
% 1.80/1.53 % (18254)Instructions burned: 4 (million)
% 1.80/1.53 % (18254)------------------------------
% 1.80/1.53 % (18254)------------------------------
% 1.80/1.54 % (18255)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/6Mi)
% 1.80/1.54 % (18252)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/507Mi)
% 1.80/1.54 % (18255)Refutation not found, incomplete strategy
% 1.80/1.54 % (18255)------------------------------
% 1.80/1.54 % (18255)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.54 % (18255)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.54
% 1.80/1.54
% 1.80/1.54 % (18255)Memory used [KB]: 9978
% 1.80/1.54 % (18255)Time elapsed: 0.029 s
% 1.80/1.54 % (18255)Instructions burned: 4 (million)
% 1.80/1.54 % (18255)------------------------------
% 1.80/1.54 % (18255)------------------------------
% 1.80/1.54 % (18252)Refutation not found, incomplete strategy
% 1.80/1.54 % (18252)------------------------------
% 1.80/1.54 % (18252)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.54 % (18252)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.54
% 1.80/1.54
% 1.80/1.54 % (18252)Memory used [KB]: 5500
% 1.80/1.54 % (18252)Time elapsed: 0.003 s
% 1.80/1.54 % (18252)Instructions burned: 4 (million)
% 1.80/1.54 % (18252)------------------------------
% 1.80/1.54 % (18252)------------------------------
% 1.80/1.54 % (18251)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/98Mi)
% 1.80/1.54 % (18251)Refutation not found, incomplete strategy
% 1.80/1.54 % (18251)------------------------------
% 1.80/1.54 % (18251)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.54 % (18251)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.54
% 1.80/1.54
% 1.80/1.54 % (18251)Memory used [KB]: 1023
% 1.80/1.54 % (18251)Time elapsed: 0.005 s
% 1.80/1.54 % (18251)Instructions burned: 5 (million)
% 1.80/1.54 % (18251)------------------------------
% 1.80/1.54 % (18251)------------------------------
% 1.80/1.54 % (18256)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/1087Mi)
% 1.80/1.54 % (18246)Instruction limit reached!
% 1.80/1.54 % (18246)------------------------------
% 1.80/1.54 % (18246)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.54 % (18246)Termination reason: Unknown
% 1.80/1.54 % (18246)Termination phase: Saturation
% 1.80/1.54
% 1.80/1.54 % (18246)Memory used [KB]: 6652
% 1.80/1.54 % (18246)Time elapsed: 0.056 s
% 1.80/1.54 % (18246)Instructions burned: 88 (million)
% 1.80/1.54 % (18246)------------------------------
% 1.80/1.54 % (18246)------------------------------
% 1.80/1.55 % (18256)Refutation not found, incomplete strategy
% 1.80/1.55 % (18256)------------------------------
% 1.80/1.55 % (18256)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.55 % (18256)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.55
% 1.80/1.55
% 1.80/1.55 % (18256)Memory used [KB]: 5500
% 1.80/1.55 % (18256)Time elapsed: 0.002 s
% 1.80/1.55 % (18256)Instructions burned: 1 (million)
% 1.80/1.55 % (18256)------------------------------
% 1.80/1.55 % (18256)------------------------------
% 1.80/1.55 % (18257)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/47Mi)
% 1.80/1.55 % (18258)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/44Mi)
% 1.80/1.55 % (18258)Refutation not found, incomplete strategy
% 1.80/1.55 % (18258)------------------------------
% 1.80/1.55 % (18258)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.55 % (18258)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.55
% 1.80/1.55
% 1.80/1.55 % (18258)Memory used [KB]: 1023
% 1.80/1.55 % (18258)Time elapsed: 0.002 s
% 1.80/1.55 % (18258)Instructions burned: 2 (million)
% 1.80/1.55 % (18258)------------------------------
% 1.80/1.55 % (18258)------------------------------
% 1.80/1.56 % (18260)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/62Mi)
% 1.80/1.56 % (18261)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/31Mi)
% 1.80/1.56 % (18260)Refutation not found, incomplete strategy
% 1.80/1.56 % (18260)------------------------------
% 1.80/1.56 % (18260)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.56 % (18260)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.56
% 1.80/1.56
% 1.80/1.56 % (18260)Memory used [KB]: 5500
% 1.80/1.56 % (18260)Time elapsed: 0.003 s
% 1.80/1.56 % (18260)Instructions burned: 4 (million)
% 1.80/1.56 % (18260)------------------------------
% 1.80/1.56 % (18260)------------------------------
% 1.80/1.56 % (18259)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/432Mi)
% 1.80/1.56 % (18262)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_17938 for (2998ds/96Mi)
% 1.80/1.56 % (18259)Refutation not found, incomplete strategy
% 1.80/1.56 % (18259)------------------------------
% 1.80/1.56 % (18259)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.56 % (18259)Termination reason: Refutation not found, incomplete strategy
% 1.80/1.56
% 1.80/1.56
% 1.80/1.56 % (18259)Memory used [KB]: 1023
% 1.80/1.56 % (18259)Time elapsed: 0.005 s
% 1.80/1.56 % (18259)Instructions burned: 5 (million)
% 1.80/1.56 % (18259)------------------------------
% 1.80/1.56 % (18259)------------------------------
% 1.80/1.56 % (18257)First to succeed.
% 1.80/1.57 % (18257)Refutation found. Thanks to Tanya!
% 1.80/1.57 % SZS status Theorem for DTF2THF_17938
% 1.80/1.57 % SZS output start Proof for DTF2THF_17938
% 1.80/1.57 thf(func_def_0, type, a: $o > $o).
% 1.80/1.57 thf(func_def_1, type, b: $o > $o).
% 1.80/1.57 thf(func_def_2, type, c: $o > $o).
% 1.80/1.57 thf(func_def_3, type, d: $o > $o).
% 1.80/1.57 thf(func_def_4, type, e: $o > $o).
% 1.80/1.57 thf(func_def_5, type, f0: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_6, type, g0: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_7, type, f1: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_8, type, g1: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_9, type, f2: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_10, type, g2: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_11, type, f3: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_12, type, g3: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_13, type, f4: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_14, type, g4: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_15, type, f5: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_16, type, g5: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_17, type, f6: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_18, type, g6: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_19, type, f7: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_20, type, g7: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_21, type, f8: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_22, type, g8: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_23, type, f9: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_24, type, g9: ($o > $o) > $i).
% 1.80/1.57 thf(func_def_29, type, ph1: !>[X0: $tType]:(X0)).
% 1.80/1.57 thf(f558,plain,(
% 1.80/1.57 $false),
% 1.80/1.57 inference(avatar_sat_refutation,[status(thm)],[f52,f76,f93,f101,f109,f117,f125,f162,f170,f181,f182,f186,f195,f203,f206,f214,f257,f270,f274,f275,f278,f280,f291,f292,f296,f297,f299,f312,f316,f317,f318,f319,f322,f324,f335,f336,f340,f341,f343,f356,f360,f361,f363,f374,f375,f379,f380,f382,f395,f399,f400,f403,f404,f407,f411,f413,f426,f430,f431,f433,f444,f445,f449,f450,f457,f460,f465,f471,f476,f478,f500,f503,f509,f514,f517,f520,f523,f526,f529,f532,f535,f538,f541,f544,f545,f547,f549,f553,f554,f557])).
% 1.80/1.57 thf(f557,plain,(
% 1.80/1.57 spl0_5 | spl0_21 | spl0_19 | ~spl0_58),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f556,f358,f120,f134,f67])).
% 1.80/1.57 thf(f67,definition,(
% 1.80/1.57 spl0_5 <=> ($true = (a @ $true))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_5])],[avatar_definition])).
% 1.80/1.57 thf(f134,definition,(
% 1.80/1.57 spl0_21 <=> ($true = (e @ $true))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_21])],[avatar_definition])).
% 1.80/1.57 thf(f120,definition,(
% 1.80/1.57 spl0_19 <=> (a = e)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_19])],[avatar_definition])).
% 1.80/1.57 thf(f358,definition,(
% 1.80/1.57 spl0_58 <=> ($true = sK10)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_58])],[avatar_definition])).
% 1.80/1.57 thf(f556,plain,(
% 1.80/1.57 ($true = (a @ $true)) | ($true = (e @ $true)) | (spl0_19 | ~spl0_58)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f555])).
% 1.80/1.57 thf(f555,plain,(
% 1.80/1.57 ($true = (a @ $true)) | ($true = (e @ $true)) | ($true = $false) | (spl0_19 | ~spl0_58)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f349,f359])).
% 1.80/1.57 thf(f359,plain,(
% 1.80/1.57 ($true = sK10) | ~spl0_58),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f358])).
% 1.80/1.57 thf(f349,plain,(
% 1.80/1.57 ($true = (a @ $true)) | (sK10 = $false) | ($true = (e @ $true)) | spl0_19),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f345])).
% 1.80/1.57 thf(f345,plain,(
% 1.80/1.57 (sK10 = $false) | ((e @ $true) != (a @ $true)) | spl0_19),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f344])).
% 1.80/1.57 thf(f344,plain,(
% 1.80/1.57 ((a @ sK10) != (e @ sK10)) | spl0_19),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f121])).
% 1.80/1.57 thf(f121,plain,(
% 1.80/1.57 (a != e) | spl0_19),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f120])).
% 1.80/1.57 thf(f554,plain,(
% 1.80/1.57 spl0_67 | spl0_21 | spl0_3 | spl0_27),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f484,f157,f61,f134,f489])).
% 1.80/1.57 thf(f489,definition,(
% 1.80/1.57 spl0_67 <=> (sK15 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_67])],[avatar_definition])).
% 1.80/1.57 thf(f61,definition,(
% 1.80/1.57 spl0_3 <=> ((d @ $true) = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_3])],[avatar_definition])).
% 1.80/1.57 thf(f157,definition,(
% 1.80/1.57 spl0_27 <=> (d = e)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_27])],[avatar_definition])).
% 1.80/1.57 thf(f484,plain,(
% 1.80/1.57 ($true = (e @ $true)) | ((d @ $true) = $true) | (sK15 = $false) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f480])).
% 1.80/1.57 thf(f480,plain,(
% 1.80/1.57 ((d @ $true) != (e @ $true)) | (sK15 = $false) | spl0_27),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f479])).
% 1.80/1.57 thf(f479,plain,(
% 1.80/1.57 ((d @ sK15) != (e @ sK15)) | spl0_27),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f158])).
% 1.80/1.57 thf(f158,plain,(
% 1.80/1.57 (d != e) | spl0_27),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f157])).
% 1.80/1.57 thf(f553,plain,(
% 1.80/1.57 spl0_23 | spl0_7 | spl0_19 | ~spl0_58),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f552,f358,f120,f74,f141])).
% 1.80/1.57 thf(f141,definition,(
% 1.80/1.57 spl0_23 <=> ((e @ $true) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_23])],[avatar_definition])).
% 1.80/1.57 thf(f74,definition,(
% 1.80/1.57 spl0_7 <=> ((a @ $true) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_7])],[avatar_definition])).
% 1.80/1.57 thf(f552,plain,(
% 1.80/1.57 ((e @ $true) = $false) | ((a @ $true) = $false) | (spl0_19 | ~spl0_58)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f551])).
% 1.80/1.57 thf(f551,plain,(
% 1.80/1.57 ($true = $false) | ((a @ $true) = $false) | ((e @ $true) = $false) | (spl0_19 | ~spl0_58)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f350,f359])).
% 1.80/1.57 thf(f350,plain,(
% 1.80/1.57 ((e @ $true) = $false) | (sK10 = $false) | ((a @ $true) = $false) | spl0_19),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f345])).
% 1.80/1.57 thf(f549,plain,(
% 1.80/1.57 spl0_43 | spl0_7 | spl0_63 | spl0_36),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f420,f201,f424,f74,f236])).
% 1.80/1.57 thf(f236,definition,(
% 1.80/1.57 spl0_43 <=> ((c @ $true) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_43])],[avatar_definition])).
% 1.80/1.57 thf(f424,definition,(
% 1.80/1.57 spl0_63 <=> (sK13 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_63])],[avatar_definition])).
% 1.80/1.57 thf(f201,definition,(
% 1.80/1.57 spl0_36 <=> (a = c)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_36])],[avatar_definition])).
% 1.80/1.57 thf(f420,plain,(
% 1.80/1.57 (sK13 = $false) | ((c @ $true) = $false) | ((a @ $true) = $false) | spl0_36),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f415])).
% 1.80/1.57 thf(f415,plain,(
% 1.80/1.57 (sK13 = $false) | ((c @ $true) != (a @ $true)) | spl0_36),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f414])).
% 1.80/1.57 thf(f414,plain,(
% 1.80/1.57 ((a @ sK13) != (c @ sK13)) | spl0_36),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f202])).
% 1.80/1.57 thf(f202,plain,(
% 1.80/1.57 (a != c) | spl0_36),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f201])).
% 1.80/1.57 thf(f547,plain,(
% 1.80/1.57 spl0_6 | spl0_7 | spl0_49 | spl0_1),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f264,f47,f268,f74,f71])).
% 1.80/1.57 thf(f71,definition,(
% 1.80/1.57 spl0_6 <=> ((d @ $true) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_6])],[avatar_definition])).
% 1.80/1.57 thf(f268,definition,(
% 1.80/1.57 spl0_49 <=> (sK6 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_49])],[avatar_definition])).
% 1.80/1.57 thf(f47,definition,(
% 1.80/1.57 spl0_1 <=> (a = d)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_1])],[avatar_definition])).
% 1.80/1.57 thf(f264,plain,(
% 1.80/1.57 (sK6 = $false) | ((d @ $true) = $false) | ((a @ $true) = $false) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f259])).
% 1.80/1.57 thf(f259,plain,(
% 1.80/1.57 (sK6 = $false) | ((d @ $true) != (a @ $true)) | spl0_1),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f258])).
% 1.80/1.57 thf(f258,plain,(
% 1.80/1.57 ((a @ sK6) != (d @ sK6)) | spl0_1),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f48])).
% 1.80/1.57 thf(f48,plain,(
% 1.80/1.57 (a != d) | spl0_1),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f47])).
% 1.80/1.57 thf(f545,plain,(
% 1.80/1.57 spl0_6 | spl0_67 | spl0_23 | spl0_27),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f485,f157,f141,f489,f71])).
% 1.80/1.57 thf(f485,plain,(
% 1.80/1.57 ((d @ $true) = $false) | ((e @ $true) = $false) | (sK15 = $false) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f480])).
% 1.80/1.57 thf(f544,plain,(
% 1.80/1.57 ~spl0_31 | ~spl0_32),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f543])).
% 1.80/1.57 thf(f543,plain,(
% 1.80/1.57 $false | (~spl0_31 | ~spl0_32)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f542])).
% 1.80/1.57 thf(f542,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_31 | ~spl0_32)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f185,f180])).
% 1.80/1.57 thf(f180,plain,(
% 1.80/1.57 (sK4 = $false) | ~spl0_31),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f179])).
% 1.80/1.57 thf(f179,definition,(
% 1.80/1.57 spl0_31 <=> (sK4 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_31])],[avatar_definition])).
% 1.80/1.57 thf(f185,plain,(
% 1.80/1.57 (sK4 = $true) | ~spl0_32),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f184])).
% 1.80/1.57 thf(f184,definition,(
% 1.80/1.57 spl0_32 <=> (sK4 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_32])],[avatar_definition])).
% 1.80/1.57 thf(f541,plain,(
% 1.80/1.57 spl0_26 | spl0_11 | spl0_27 | ~spl0_67),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f540,f489,f157,f88,f152])).
% 1.80/1.57 thf(f152,definition,(
% 1.80/1.57 spl0_26 <=> ((e @ $false) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_26])],[avatar_definition])).
% 1.80/1.57 thf(f88,definition,(
% 1.80/1.57 spl0_11 <=> ((d @ $false) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_11])],[avatar_definition])).
% 1.80/1.57 thf(f540,plain,(
% 1.80/1.57 ((e @ $false) = $false) | ((d @ $false) = $false) | (spl0_27 | ~spl0_67)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f539])).
% 1.80/1.57 thf(f539,plain,(
% 1.80/1.57 ((d @ $false) = $false) | ((e @ $false) = $false) | ($true = $false) | (spl0_27 | ~spl0_67)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f483,f490])).
% 1.80/1.57 thf(f490,plain,(
% 1.80/1.57 (sK15 = $false) | ~spl0_67),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f489])).
% 1.80/1.57 thf(f483,plain,(
% 1.80/1.57 ($true = sK15) | ((d @ $false) = $false) | ((e @ $false) = $false) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f481])).
% 1.80/1.57 thf(f481,plain,(
% 1.80/1.57 ($true = sK15) | ((d @ $false) != (e @ $false)) | spl0_27),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f479])).
% 1.80/1.57 thf(f538,plain,(
% 1.80/1.57 ~spl0_49 | ~spl0_50),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f537])).
% 1.80/1.57 thf(f537,plain,(
% 1.80/1.57 $false | (~spl0_49 | ~spl0_50)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f536])).
% 1.80/1.57 thf(f536,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_49 | ~spl0_50)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f273,f269])).
% 1.80/1.57 thf(f269,plain,(
% 1.80/1.57 (sK6 = $false) | ~spl0_49),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f268])).
% 1.80/1.57 thf(f273,plain,(
% 1.80/1.57 (sK6 = $true) | ~spl0_50),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f272])).
% 1.80/1.57 thf(f272,definition,(
% 1.80/1.57 spl0_50 <=> (sK6 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_50])],[avatar_definition])).
% 1.80/1.57 thf(f535,plain,(
% 1.80/1.57 ~spl0_55 | ~spl0_56),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f534])).
% 1.80/1.57 thf(f534,plain,(
% 1.80/1.57 $false | (~spl0_55 | ~spl0_56)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f533])).
% 1.80/1.57 thf(f533,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_55 | ~spl0_56)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f339,f334])).
% 1.80/1.57 thf(f334,plain,(
% 1.80/1.57 (sK9 = $false) | ~spl0_55),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f333])).
% 1.80/1.57 thf(f333,definition,(
% 1.80/1.57 spl0_55 <=> (sK9 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_55])],[avatar_definition])).
% 1.80/1.57 thf(f339,plain,(
% 1.80/1.57 ($true = sK9) | ~spl0_56),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f338])).
% 1.80/1.57 thf(f338,definition,(
% 1.80/1.57 spl0_56 <=> ($true = sK9)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_56])],[avatar_definition])).
% 1.80/1.57 thf(f532,plain,(
% 1.80/1.57 ~spl0_51 | ~spl0_52),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f531])).
% 1.80/1.57 thf(f531,plain,(
% 1.80/1.57 $false | (~spl0_51 | ~spl0_52)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f530])).
% 1.80/1.57 thf(f530,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_51 | ~spl0_52)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f295,f290])).
% 1.80/1.57 thf(f290,plain,(
% 1.80/1.57 (sK7 = $false) | ~spl0_51),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f289])).
% 1.80/1.57 thf(f289,definition,(
% 1.80/1.57 spl0_51 <=> (sK7 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_51])],[avatar_definition])).
% 1.80/1.57 thf(f295,plain,(
% 1.80/1.57 ($true = sK7) | ~spl0_52),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f294])).
% 1.80/1.57 thf(f294,definition,(
% 1.80/1.57 spl0_52 <=> ($true = sK7)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_52])],[avatar_definition])).
% 1.80/1.57 thf(f529,plain,(
% 1.80/1.57 ~spl0_53 | ~spl0_54),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f528])).
% 1.80/1.57 thf(f528,plain,(
% 1.80/1.57 $false | (~spl0_53 | ~spl0_54)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f527])).
% 1.80/1.57 thf(f527,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_53 | ~spl0_54)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f315,f311])).
% 1.80/1.57 thf(f311,plain,(
% 1.80/1.57 (sK8 = $false) | ~spl0_53),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f310])).
% 1.80/1.57 thf(f310,definition,(
% 1.80/1.57 spl0_53 <=> (sK8 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_53])],[avatar_definition])).
% 1.80/1.57 thf(f315,plain,(
% 1.80/1.57 (sK8 = $true) | ~spl0_54),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f314])).
% 1.80/1.57 thf(f314,definition,(
% 1.80/1.57 spl0_54 <=> (sK8 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_54])],[avatar_definition])).
% 1.80/1.57 thf(f526,plain,(
% 1.80/1.57 ~spl0_61 | ~spl0_62),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f525])).
% 1.80/1.57 thf(f525,plain,(
% 1.80/1.57 $false | (~spl0_61 | ~spl0_62)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f524])).
% 1.80/1.57 thf(f524,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_61 | ~spl0_62)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f398,f394])).
% 1.80/1.57 thf(f394,plain,(
% 1.80/1.57 (sK12 = $false) | ~spl0_61),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f393])).
% 1.80/1.57 thf(f393,definition,(
% 1.80/1.57 spl0_61 <=> (sK12 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_61])],[avatar_definition])).
% 1.80/1.57 thf(f398,plain,(
% 1.80/1.57 (sK12 = $true) | ~spl0_62),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f397])).
% 1.80/1.57 thf(f397,definition,(
% 1.80/1.57 spl0_62 <=> (sK12 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_62])],[avatar_definition])).
% 1.80/1.57 thf(f523,plain,(
% 1.80/1.57 ~spl0_63 | ~spl0_64),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f522])).
% 1.80/1.57 thf(f522,plain,(
% 1.80/1.57 $false | (~spl0_63 | ~spl0_64)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f521])).
% 1.80/1.57 thf(f521,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_63 | ~spl0_64)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f429,f425])).
% 1.80/1.57 thf(f425,plain,(
% 1.80/1.57 (sK13 = $false) | ~spl0_63),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f424])).
% 1.80/1.57 thf(f429,plain,(
% 1.80/1.57 (sK13 = $true) | ~spl0_64),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f428])).
% 1.80/1.57 thf(f428,definition,(
% 1.80/1.57 spl0_64 <=> (sK13 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_64])],[avatar_definition])).
% 1.80/1.57 thf(f520,plain,(
% 1.80/1.57 ~spl0_44 | ~spl0_47),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f519])).
% 1.80/1.57 thf(f519,plain,(
% 1.80/1.57 $false | (~spl0_44 | ~spl0_47)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f518])).
% 1.80/1.57 thf(f518,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_44 | ~spl0_47)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f241,f251])).
% 1.80/1.57 thf(f251,plain,(
% 1.80/1.57 ((c @ $false) = $false) | ~spl0_47),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f250])).
% 1.80/1.57 thf(f250,definition,(
% 1.80/1.57 spl0_47 <=> ((c @ $false) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_47])],[avatar_definition])).
% 1.80/1.57 thf(f241,plain,(
% 1.80/1.57 ((c @ $false) = $true) | ~spl0_44),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f240])).
% 1.80/1.57 thf(f240,definition,(
% 1.80/1.57 spl0_44 <=> ((c @ $false) = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_44])],[avatar_definition])).
% 1.80/1.57 thf(f517,plain,(
% 1.80/1.57 ~spl0_59 | ~spl0_60),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f516])).
% 1.80/1.57 thf(f516,plain,(
% 1.80/1.57 $false | (~spl0_59 | ~spl0_60)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f515])).
% 1.80/1.57 thf(f515,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_59 | ~spl0_60)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f378,f373])).
% 1.80/1.57 thf(f373,plain,(
% 1.80/1.57 (sK11 = $false) | ~spl0_59),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f372])).
% 1.80/1.57 thf(f372,definition,(
% 1.80/1.57 spl0_59 <=> (sK11 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_59])],[avatar_definition])).
% 1.80/1.57 thf(f378,plain,(
% 1.80/1.57 (sK11 = $true) | ~spl0_60),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f377])).
% 1.80/1.57 thf(f377,definition,(
% 1.80/1.57 spl0_60 <=> (sK11 = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_60])],[avatar_definition])).
% 1.80/1.57 thf(f514,plain,(
% 1.80/1.57 ~spl0_45 | ~spl0_48),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f513])).
% 1.80/1.57 thf(f513,plain,(
% 1.80/1.57 $false | (~spl0_45 | ~spl0_48)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f512])).
% 1.80/1.57 thf(f512,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_45 | ~spl0_48)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f244,f254])).
% 1.80/1.57 thf(f254,plain,(
% 1.80/1.57 ((b @ $false) = $false) | ~spl0_48),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f253])).
% 1.80/1.57 thf(f253,definition,(
% 1.80/1.57 spl0_48 <=> ((b @ $false) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_48])],[avatar_definition])).
% 1.80/1.57 thf(f244,plain,(
% 1.80/1.57 ((b @ $false) = $true) | ~spl0_45),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f243])).
% 1.80/1.57 thf(f243,definition,(
% 1.80/1.57 spl0_45 <=> ((b @ $false) = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_45])],[avatar_definition])).
% 1.80/1.57 thf(f509,plain,(
% 1.80/1.57 ~spl0_65 | ~spl0_66),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f508])).
% 1.80/1.57 thf(f508,plain,(
% 1.80/1.57 $false | (~spl0_65 | ~spl0_66)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f507])).
% 1.80/1.57 thf(f507,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_65 | ~spl0_66)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f448,f443])).
% 1.80/1.57 thf(f443,plain,(
% 1.80/1.57 (sK14 = $false) | ~spl0_65),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f442])).
% 1.80/1.57 thf(f442,definition,(
% 1.80/1.57 spl0_65 <=> (sK14 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_65])],[avatar_definition])).
% 1.80/1.57 thf(f448,plain,(
% 1.80/1.57 ($true = sK14) | ~spl0_66),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f447])).
% 1.80/1.57 thf(f447,definition,(
% 1.80/1.57 spl0_66 <=> ($true = sK14)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_66])],[avatar_definition])).
% 1.80/1.57 thf(f503,plain,(
% 1.80/1.57 ~spl0_41 | ~spl0_43),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f502])).
% 1.80/1.57 thf(f502,plain,(
% 1.80/1.57 $false | (~spl0_41 | ~spl0_43)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f501])).
% 1.80/1.57 thf(f501,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_41 | ~spl0_43)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f230,f237])).
% 1.80/1.57 thf(f237,plain,(
% 1.80/1.57 ((c @ $true) = $false) | ~spl0_43),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f236])).
% 1.80/1.57 thf(f230,plain,(
% 1.80/1.57 ($true = (c @ $true)) | ~spl0_41),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f229])).
% 1.80/1.57 thf(f229,definition,(
% 1.80/1.57 spl0_41 <=> ($true = (c @ $true))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_41])],[avatar_definition])).
% 1.80/1.57 thf(f500,plain,(
% 1.80/1.57 ~spl0_40 | ~spl0_42),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f499])).
% 1.80/1.57 thf(f499,plain,(
% 1.80/1.57 $false | (~spl0_40 | ~spl0_42)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f498])).
% 1.80/1.57 thf(f498,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_40 | ~spl0_42)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f227,f234])).
% 1.80/1.57 thf(f234,plain,(
% 1.80/1.57 ((b @ $true) = $false) | ~spl0_42),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f233])).
% 1.80/1.57 thf(f233,definition,(
% 1.80/1.57 spl0_42 <=> ((b @ $true) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_42])],[avatar_definition])).
% 1.80/1.57 thf(f227,plain,(
% 1.80/1.57 ((b @ $true) = $true) | ~spl0_40),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f226])).
% 1.80/1.57 thf(f226,definition,(
% 1.80/1.57 spl0_40 <=> ((b @ $true) = $true)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_40])],[avatar_definition])).
% 1.80/1.57 thf(f478,plain,(
% 1.80/1.57 ~spl0_27 | spl0_28),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f477,f160,f157])).
% 1.80/1.57 thf(f160,definition,(
% 1.80/1.57 spl0_28 <=> ((f9 @ d) = (f9 @ e))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_28])],[avatar_definition])).
% 1.80/1.57 thf(f477,plain,(
% 1.80/1.57 (d != e) | spl0_28),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f161])).
% 1.80/1.57 thf(f161,plain,(
% 1.80/1.57 ((f9 @ d) != (f9 @ e)) | spl0_28),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f160])).
% 1.80/1.57 thf(f476,plain,(
% 1.80/1.57 ~spl0_24 | ~spl0_26),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f475])).
% 1.80/1.57 thf(f475,plain,(
% 1.80/1.57 $false | (~spl0_24 | ~spl0_26)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f474])).
% 1.80/1.57 thf(f474,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_24 | ~spl0_26)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f146,f153])).
% 1.80/1.57 thf(f153,plain,(
% 1.80/1.57 ((e @ $false) = $false) | ~spl0_26),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f152])).
% 1.80/1.57 thf(f146,plain,(
% 1.80/1.57 ($true = (e @ $false)) | ~spl0_24),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f145])).
% 1.80/1.57 thf(f145,definition,(
% 1.80/1.57 spl0_24 <=> ($true = (e @ $false))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_24])],[avatar_definition])).
% 1.80/1.57 thf(f471,plain,(
% 1.80/1.57 ~spl0_57 | ~spl0_58),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f470])).
% 1.80/1.57 thf(f470,plain,(
% 1.80/1.57 $false | (~spl0_57 | ~spl0_58)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f469])).
% 1.80/1.57 thf(f469,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_57 | ~spl0_58)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f359,f355])).
% 1.80/1.57 thf(f355,plain,(
% 1.80/1.57 (sK10 = $false) | ~spl0_57),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f354])).
% 1.80/1.57 thf(f354,definition,(
% 1.80/1.57 spl0_57 <=> (sK10 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_57])],[avatar_definition])).
% 1.80/1.57 thf(f465,plain,(
% 1.80/1.57 ~spl0_21 | ~spl0_23),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f464])).
% 1.80/1.57 thf(f464,plain,(
% 1.80/1.57 $false | (~spl0_21 | ~spl0_23)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f463])).
% 1.80/1.57 thf(f463,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_21 | ~spl0_23)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f135,f142])).
% 1.80/1.57 thf(f142,plain,(
% 1.80/1.57 ((e @ $true) = $false) | ~spl0_23),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f141])).
% 1.80/1.57 thf(f135,plain,(
% 1.80/1.57 ($true = (e @ $true)) | ~spl0_21),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f134])).
% 1.80/1.57 thf(f460,plain,(
% 1.80/1.57 ~spl0_10 | ~spl0_12),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f459])).
% 1.80/1.57 thf(f459,plain,(
% 1.80/1.57 $false | (~spl0_10 | ~spl0_12)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f458])).
% 1.80/1.57 thf(f458,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_10 | ~spl0_12)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f85,f92])).
% 1.80/1.57 thf(f92,plain,(
% 1.80/1.57 ((a @ $false) = $false) | ~spl0_12),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f91])).
% 1.80/1.57 thf(f91,definition,(
% 1.80/1.57 spl0_12 <=> ((a @ $false) = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_12])],[avatar_definition])).
% 1.80/1.57 thf(f85,plain,(
% 1.80/1.57 ($true = (a @ $false)) | ~spl0_10),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f84])).
% 1.80/1.57 thf(f84,definition,(
% 1.80/1.57 spl0_10 <=> ($true = (a @ $false))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_10])],[avatar_definition])).
% 1.80/1.57 thf(f457,plain,(
% 1.80/1.57 ~spl0_9 | ~spl0_11),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f456])).
% 1.80/1.57 thf(f456,plain,(
% 1.80/1.57 $false | (~spl0_9 | ~spl0_11)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f453])).
% 1.80/1.57 thf(f453,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_9 | ~spl0_11)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f82,f89])).
% 1.80/1.57 thf(f89,plain,(
% 1.80/1.57 ((d @ $false) = $false) | ~spl0_11),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f88])).
% 1.80/1.57 thf(f82,plain,(
% 1.80/1.57 ($true = (d @ $false)) | ~spl0_9),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f81])).
% 1.80/1.57 thf(f81,definition,(
% 1.80/1.57 spl0_9 <=> ($true = (d @ $false))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_9])],[avatar_definition])).
% 1.80/1.57 thf(f450,plain,(
% 1.80/1.57 spl0_66 | spl0_48 | spl0_47 | spl0_37),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f438,f209,f250,f253,f447])).
% 1.80/1.57 thf(f209,definition,(
% 1.80/1.57 spl0_37 <=> (b = c)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_37])],[avatar_definition])).
% 1.80/1.57 thf(f438,plain,(
% 1.80/1.57 ((c @ $false) = $false) | ($true = sK14) | ((b @ $false) = $false) | spl0_37),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f436])).
% 1.80/1.57 thf(f436,plain,(
% 1.80/1.57 ($true = sK14) | ((c @ $false) != (b @ $false)) | spl0_37),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f434])).
% 1.80/1.57 thf(f434,plain,(
% 1.80/1.57 ((b @ sK14) != (c @ sK14)) | spl0_37),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f210])).
% 1.80/1.57 thf(f210,plain,(
% 1.80/1.57 (b != c) | spl0_37),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f209])).
% 1.80/1.57 thf(f449,plain,(
% 1.80/1.57 spl0_45 | spl0_66 | spl0_44 | spl0_37),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f437,f209,f240,f447,f243])).
% 1.80/1.57 thf(f437,plain,(
% 1.80/1.57 ((b @ $false) = $true) | ((c @ $false) = $true) | ($true = sK14) | spl0_37),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f436])).
% 1.80/1.57 thf(f445,plain,(
% 1.80/1.57 spl0_43 | spl0_42 | spl0_65 | spl0_37),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f440,f209,f442,f233,f236])).
% 1.80/1.57 thf(f440,plain,(
% 1.80/1.57 ((b @ $true) = $false) | (sK14 = $false) | ((c @ $true) = $false) | spl0_37),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f435])).
% 1.80/1.57 thf(f435,plain,(
% 1.80/1.57 ((b @ $true) != (c @ $true)) | (sK14 = $false) | spl0_37),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f434])).
% 1.80/1.57 thf(f444,plain,(
% 1.80/1.57 spl0_40 | spl0_65 | spl0_41 | spl0_37),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f439,f209,f229,f442,f226])).
% 1.80/1.57 thf(f439,plain,(
% 1.80/1.57 (sK14 = $false) | ((b @ $true) = $true) | ($true = (c @ $true)) | spl0_37),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f435])).
% 1.80/1.57 thf(f433,plain,(
% 1.80/1.57 ~spl0_37 | spl0_38),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f432,f212,f209])).
% 1.80/1.57 thf(f212,definition,(
% 1.80/1.57 spl0_38 <=> ((f4 @ b) = (f4 @ c))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_38])],[avatar_definition])).
% 1.80/1.57 thf(f432,plain,(
% 1.80/1.57 (b != c) | spl0_38),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f213])).
% 1.80/1.57 thf(f213,plain,(
% 1.80/1.57 ((f4 @ b) != (f4 @ c)) | spl0_38),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f212])).
% 1.80/1.57 thf(f431,plain,(
% 1.80/1.57 spl0_47 | spl0_64 | spl0_12 | spl0_36),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f418,f201,f91,f428,f250])).
% 1.80/1.57 thf(f418,plain,(
% 1.80/1.57 ((c @ $false) = $false) | (sK13 = $true) | ((a @ $false) = $false) | spl0_36),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f416])).
% 1.80/1.57 thf(f416,plain,(
% 1.80/1.57 (sK13 = $true) | ((c @ $false) != (a @ $false)) | spl0_36),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f414])).
% 1.80/1.57 thf(f430,plain,(
% 1.80/1.57 spl0_44 | spl0_10 | spl0_64 | spl0_36),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f417,f201,f428,f84,f240])).
% 1.80/1.57 thf(f417,plain,(
% 1.80/1.57 ($true = (a @ $false)) | (sK13 = $true) | ((c @ $false) = $true) | spl0_36),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f416])).
% 1.80/1.57 thf(f426,plain,(
% 1.80/1.57 spl0_41 | spl0_63 | ~spl0_7 | spl0_36),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f422,f201,f74,f424,f229])).
% 1.80/1.57 thf(f422,plain,(
% 1.80/1.57 (sK13 = $false) | ($true = (c @ $true)) | (~spl0_7 | spl0_36)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f421])).
% 1.80/1.57 thf(f421,plain,(
% 1.80/1.57 ($true = $false) | ($true = (c @ $true)) | (sK13 = $false) | (~spl0_7 | spl0_36)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f419,f75])).
% 1.80/1.57 thf(f75,plain,(
% 1.80/1.57 ((a @ $true) = $false) | ~spl0_7),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f74])).
% 1.80/1.57 thf(f419,plain,(
% 1.80/1.57 ($true = (a @ $true)) | ($true = (c @ $true)) | (sK13 = $false) | spl0_36),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f415])).
% 1.80/1.57 thf(f413,plain,(
% 1.80/1.57 ~spl0_36 | spl0_35),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f412,f198,f201])).
% 1.80/1.57 thf(f198,definition,(
% 1.80/1.57 spl0_35 <=> ((f1 @ a) = (f1 @ c))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_35])],[avatar_definition])).
% 1.80/1.57 thf(f412,plain,(
% 1.80/1.57 (a != c) | spl0_35),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f199])).
% 1.80/1.57 thf(f199,plain,(
% 1.80/1.57 ((f1 @ a) != (f1 @ c)) | spl0_35),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f198])).
% 1.80/1.57 thf(f411,plain,(
% 1.80/1.57 spl0_49 | spl0_3 | spl0_1 | ~spl0_7),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f410,f74,f47,f61,f268])).
% 1.80/1.57 thf(f410,plain,(
% 1.80/1.57 ((d @ $true) = $true) | (sK6 = $false) | (spl0_1 | ~spl0_7)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f409])).
% 1.80/1.57 thf(f409,plain,(
% 1.80/1.57 ($true = $false) | (sK6 = $false) | ((d @ $true) = $true) | (spl0_1 | ~spl0_7)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f263,f75])).
% 1.80/1.57 thf(f263,plain,(
% 1.80/1.57 ((d @ $true) = $true) | ($true = (a @ $true)) | (sK6 = $false) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f259])).
% 1.80/1.57 thf(f407,plain,(
% 1.80/1.57 spl0_57 | spl0_21 | ~spl0_7 | spl0_19),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f406,f120,f74,f134,f354])).
% 1.80/1.57 thf(f406,plain,(
% 1.80/1.57 ($true = (e @ $true)) | (sK10 = $false) | (~spl0_7 | spl0_19)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f405])).
% 1.80/1.57 thf(f405,plain,(
% 1.80/1.57 ($true = $false) | ($true = (e @ $true)) | (sK10 = $false) | (~spl0_7 | spl0_19)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f349,f75])).
% 1.80/1.57 thf(f404,plain,(
% 1.80/1.57 spl0_6 | spl0_43 | spl0_61 | spl0_34),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f389,f193,f393,f236,f71])).
% 1.80/1.57 thf(f193,definition,(
% 1.80/1.57 spl0_34 <=> (c = d)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_34])],[avatar_definition])).
% 1.80/1.57 thf(f389,plain,(
% 1.80/1.57 ((d @ $true) = $false) | (sK12 = $false) | ((c @ $true) = $false) | spl0_34),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f384])).
% 1.80/1.57 thf(f384,plain,(
% 1.80/1.57 (sK12 = $false) | ((d @ $true) != (c @ $true)) | spl0_34),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f383])).
% 1.80/1.57 thf(f383,plain,(
% 1.80/1.57 ((d @ sK12) != (c @ sK12)) | spl0_34),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f194])).
% 1.80/1.57 thf(f194,plain,(
% 1.80/1.57 (c != d) | spl0_34),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f193])).
% 1.80/1.57 thf(f403,plain,(
% 1.80/1.57 ~spl0_5 | ~spl0_7),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f402])).
% 1.80/1.57 thf(f402,plain,(
% 1.80/1.57 $false | (~spl0_5 | ~spl0_7)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f401])).
% 1.80/1.57 thf(f401,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_5 | ~spl0_7)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f68,f75])).
% 1.80/1.57 thf(f68,plain,(
% 1.80/1.57 ($true = (a @ $true)) | ~spl0_5),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f67])).
% 1.80/1.57 thf(f400,plain,(
% 1.80/1.57 spl0_62 | spl0_11 | spl0_47 | spl0_34),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f387,f193,f250,f88,f397])).
% 1.80/1.57 thf(f387,plain,(
% 1.80/1.57 ((d @ $false) = $false) | ((c @ $false) = $false) | (sK12 = $true) | spl0_34),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f385])).
% 1.80/1.57 thf(f385,plain,(
% 1.80/1.57 ((c @ $false) != (d @ $false)) | (sK12 = $true) | spl0_34),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f383])).
% 1.80/1.57 thf(f399,plain,(
% 1.80/1.57 spl0_44 | spl0_62 | spl0_9 | spl0_34),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f386,f193,f81,f397,f240])).
% 1.80/1.57 thf(f386,plain,(
% 1.80/1.57 ($true = (d @ $false)) | (sK12 = $true) | ((c @ $false) = $true) | spl0_34),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f385])).
% 1.80/1.57 thf(f395,plain,(
% 1.80/1.57 spl0_41 | spl0_61 | ~spl0_6 | spl0_34),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f391,f193,f71,f393,f229])).
% 1.80/1.57 thf(f391,plain,(
% 1.80/1.57 (sK12 = $false) | ($true = (c @ $true)) | (~spl0_6 | spl0_34)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f390])).
% 1.80/1.57 thf(f390,plain,(
% 1.80/1.57 ($true = (c @ $true)) | (sK12 = $false) | ($true = $false) | (~spl0_6 | spl0_34)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f388,f72])).
% 1.80/1.57 thf(f72,plain,(
% 1.80/1.57 ((d @ $true) = $false) | ~spl0_6),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f71])).
% 1.80/1.57 thf(f388,plain,(
% 1.80/1.57 ((d @ $true) = $true) | (sK12 = $false) | ($true = (c @ $true)) | spl0_34),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f384])).
% 1.80/1.57 thf(f382,plain,(
% 1.80/1.57 ~spl0_34 | spl0_33),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f381,f190,f193])).
% 1.80/1.57 thf(f190,definition,(
% 1.80/1.57 spl0_33 <=> ((f7 @ c) = (f7 @ d))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_33])],[avatar_definition])).
% 1.80/1.57 thf(f381,plain,(
% 1.80/1.57 (c != d) | spl0_33),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f191])).
% 1.80/1.57 thf(f191,plain,(
% 1.80/1.57 ((f7 @ c) != (f7 @ d)) | spl0_33),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f190])).
% 1.80/1.57 thf(f380,plain,(
% 1.80/1.57 spl0_47 | spl0_26 | spl0_60 | spl0_30),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f368,f168,f377,f152,f250])).
% 1.80/1.57 thf(f168,definition,(
% 1.80/1.57 spl0_30 <=> (c = e)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_30])],[avatar_definition])).
% 1.80/1.57 thf(f368,plain,(
% 1.80/1.57 (sK11 = $true) | ((e @ $false) = $false) | ((c @ $false) = $false) | spl0_30),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f366])).
% 1.80/1.57 thf(f366,plain,(
% 1.80/1.57 (sK11 = $true) | ((c @ $false) != (e @ $false)) | spl0_30),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f364])).
% 1.80/1.57 thf(f364,plain,(
% 1.80/1.57 ((e @ sK11) != (c @ sK11)) | spl0_30),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f169])).
% 1.80/1.57 thf(f169,plain,(
% 1.80/1.57 (c != e) | spl0_30),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f168])).
% 1.80/1.57 thf(f379,plain,(
% 1.80/1.57 spl0_60 | spl0_24 | spl0_44 | spl0_30),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f367,f168,f240,f145,f377])).
% 1.80/1.57 thf(f367,plain,(
% 1.80/1.57 (sK11 = $true) | ((c @ $false) = $true) | ($true = (e @ $false)) | spl0_30),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f366])).
% 1.80/1.57 thf(f375,plain,(
% 1.80/1.57 spl0_43 | spl0_59 | spl0_23 | spl0_30),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f370,f168,f141,f372,f236])).
% 1.80/1.57 thf(f370,plain,(
% 1.80/1.57 ((c @ $true) = $false) | ((e @ $true) = $false) | (sK11 = $false) | spl0_30),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f365])).
% 1.80/1.57 thf(f365,plain,(
% 1.80/1.57 (sK11 = $false) | ((e @ $true) != (c @ $true)) | spl0_30),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f364])).
% 1.80/1.57 thf(f374,plain,(
% 1.80/1.57 spl0_59 | spl0_41 | spl0_21 | spl0_30),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f369,f168,f134,f229,f372])).
% 1.80/1.57 thf(f369,plain,(
% 1.80/1.57 (sK11 = $false) | ($true = (c @ $true)) | ($true = (e @ $true)) | spl0_30),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f365])).
% 1.80/1.57 thf(f363,plain,(
% 1.80/1.57 ~spl0_30 | spl0_29),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f362,f165,f168])).
% 1.80/1.57 thf(f165,definition,(
% 1.80/1.57 spl0_29 <=> ((f8 @ c) = (f8 @ e))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_29])],[avatar_definition])).
% 1.80/1.57 thf(f362,plain,(
% 1.80/1.57 (c != e) | spl0_29),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f166])).
% 1.80/1.57 thf(f166,plain,(
% 1.80/1.57 ((f8 @ c) != (f8 @ e)) | spl0_29),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f165])).
% 1.80/1.57 thf(f361,plain,(
% 1.80/1.57 spl0_26 | spl0_12 | spl0_58 | spl0_19),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f348,f120,f358,f91,f152])).
% 1.80/1.57 thf(f348,plain,(
% 1.80/1.57 ((e @ $false) = $false) | ($true = sK10) | ((a @ $false) = $false) | spl0_19),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f346])).
% 1.80/1.57 thf(f346,plain,(
% 1.80/1.57 ($true = sK10) | ((e @ $false) != (a @ $false)) | spl0_19),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f344])).
% 1.80/1.57 thf(f360,plain,(
% 1.80/1.57 spl0_58 | spl0_10 | spl0_24 | spl0_19),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f347,f120,f145,f84,f358])).
% 1.80/1.57 thf(f347,plain,(
% 1.80/1.57 ($true = (e @ $false)) | ($true = sK10) | ($true = (a @ $false)) | spl0_19),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f346])).
% 1.80/1.57 thf(f356,plain,(
% 1.80/1.57 spl0_57 | spl0_23 | ~spl0_5 | spl0_19),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f352,f120,f67,f141,f354])).
% 1.80/1.57 thf(f352,plain,(
% 1.80/1.57 (sK10 = $false) | ((e @ $true) = $false) | (~spl0_5 | spl0_19)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f351])).
% 1.80/1.57 thf(f351,plain,(
% 1.80/1.57 ((e @ $true) = $false) | ($true = $false) | (sK10 = $false) | (~spl0_5 | spl0_19)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f350,f68])).
% 1.80/1.57 thf(f343,plain,(
% 1.80/1.57 ~spl0_19 | spl0_20),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f342,f123,f120])).
% 1.80/1.57 thf(f123,definition,(
% 1.80/1.57 spl0_20 <=> ((f3 @ a) = (f3 @ e))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_20])],[avatar_definition])).
% 1.80/1.57 thf(f342,plain,(
% 1.80/1.57 (a != e) | spl0_20),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f124])).
% 1.80/1.57 thf(f124,plain,(
% 1.80/1.57 ((f3 @ a) != (f3 @ e)) | spl0_20),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f123])).
% 1.80/1.57 thf(f341,plain,(
% 1.80/1.57 spl0_48 | spl0_56 | spl0_26 | spl0_18),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f329,f115,f152,f338,f253])).
% 1.80/1.57 thf(f115,definition,(
% 1.80/1.57 spl0_18 <=> (b = e)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_18])],[avatar_definition])).
% 1.80/1.57 thf(f329,plain,(
% 1.80/1.57 ((b @ $false) = $false) | ($true = sK9) | ((e @ $false) = $false) | spl0_18),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f327])).
% 1.80/1.57 thf(f327,plain,(
% 1.80/1.57 ($true = sK9) | ((b @ $false) != (e @ $false)) | spl0_18),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f325])).
% 1.80/1.57 thf(f325,plain,(
% 1.80/1.57 ((e @ sK9) != (b @ sK9)) | spl0_18),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f116])).
% 1.80/1.57 thf(f116,plain,(
% 1.80/1.57 (b != e) | spl0_18),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f115])).
% 1.80/1.57 thf(f340,plain,(
% 1.80/1.57 spl0_24 | spl0_56 | spl0_45 | spl0_18),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f328,f115,f243,f338,f145])).
% 1.80/1.57 thf(f328,plain,(
% 1.80/1.57 ($true = (e @ $false)) | ((b @ $false) = $true) | ($true = sK9) | spl0_18),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f327])).
% 1.80/1.57 thf(f336,plain,(
% 1.80/1.57 spl0_42 | spl0_55 | spl0_23 | spl0_18),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f331,f115,f141,f333,f233])).
% 1.80/1.57 thf(f331,plain,(
% 1.80/1.57 ((e @ $true) = $false) | (sK9 = $false) | ((b @ $true) = $false) | spl0_18),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f326])).
% 1.80/1.57 thf(f326,plain,(
% 1.80/1.57 (sK9 = $false) | ((b @ $true) != (e @ $true)) | spl0_18),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f325])).
% 1.80/1.57 thf(f335,plain,(
% 1.80/1.57 spl0_55 | spl0_21 | spl0_40 | spl0_18),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f330,f115,f226,f134,f333])).
% 1.80/1.57 thf(f330,plain,(
% 1.80/1.57 ($true = (e @ $true)) | (sK9 = $false) | ((b @ $true) = $true) | spl0_18),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f326])).
% 1.80/1.57 thf(f324,plain,(
% 1.80/1.57 ~spl0_18 | spl0_17),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f323,f112,f115])).
% 1.80/1.57 thf(f112,definition,(
% 1.80/1.57 spl0_17 <=> ((f6 @ b) = (f6 @ e))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_17])],[avatar_definition])).
% 1.80/1.57 thf(f323,plain,(
% 1.80/1.57 (b != e) | spl0_17),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f113])).
% 1.80/1.57 thf(f113,plain,(
% 1.80/1.57 ((f6 @ b) != (f6 @ e)) | spl0_17),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f112])).
% 1.80/1.57 thf(f322,plain,(
% 1.80/1.57 spl0_6 | spl0_49 | spl0_1 | ~spl0_5),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f321,f67,f47,f268,f71])).
% 1.80/1.57 thf(f321,plain,(
% 1.80/1.57 (sK6 = $false) | ((d @ $true) = $false) | (spl0_1 | ~spl0_5)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f320])).
% 1.80/1.57 thf(f320,plain,(
% 1.80/1.57 (sK6 = $false) | ($true = $false) | ((d @ $true) = $false) | (spl0_1 | ~spl0_5)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f264,f68])).
% 1.80/1.57 thf(f319,plain,(
% 1.80/1.57 spl0_42 | spl0_53 | spl0_6 | spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f306,f107,f71,f310,f233])).
% 1.80/1.57 thf(f107,definition,(
% 1.80/1.57 spl0_16 <=> (b = d)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_16])],[avatar_definition])).
% 1.80/1.57 thf(f306,plain,(
% 1.80/1.57 ((d @ $true) = $false) | ((b @ $true) = $false) | (sK8 = $false) | spl0_16),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f301])).
% 1.80/1.57 thf(f301,plain,(
% 1.80/1.57 (sK8 = $false) | ((b @ $true) != (d @ $true)) | spl0_16),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f300])).
% 1.80/1.57 thf(f300,plain,(
% 1.80/1.57 ((d @ sK8) != (b @ sK8)) | spl0_16),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f108])).
% 1.80/1.57 thf(f108,plain,(
% 1.80/1.57 (b != d) | spl0_16),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f107])).
% 1.80/1.57 thf(f318,plain,(
% 1.80/1.57 spl0_3 | spl0_40 | spl0_53 | spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f305,f107,f310,f226,f61])).
% 1.80/1.57 thf(f305,plain,(
% 1.80/1.57 ((d @ $true) = $true) | ((b @ $true) = $true) | (sK8 = $false) | spl0_16),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f301])).
% 1.80/1.57 thf(f317,plain,(
% 1.80/1.57 spl0_11 | spl0_48 | spl0_54 | spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f304,f107,f314,f253,f88])).
% 1.80/1.57 thf(f304,plain,(
% 1.80/1.57 (sK8 = $true) | ((b @ $false) = $false) | ((d @ $false) = $false) | spl0_16),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f302])).
% 1.80/1.57 thf(f302,plain,(
% 1.80/1.57 (sK8 = $true) | ((b @ $false) != (d @ $false)) | spl0_16),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f300])).
% 1.80/1.57 thf(f316,plain,(
% 1.80/1.57 spl0_54 | spl0_45 | spl0_9 | spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f303,f107,f81,f243,f314])).
% 1.80/1.57 thf(f303,plain,(
% 1.80/1.57 (sK8 = $true) | ((b @ $false) = $true) | ($true = (d @ $false)) | spl0_16),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f302])).
% 1.80/1.57 thf(f312,plain,(
% 1.80/1.57 spl0_53 | spl0_40 | ~spl0_6 | spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f308,f107,f71,f226,f310])).
% 1.80/1.57 thf(f308,plain,(
% 1.80/1.57 ((b @ $true) = $true) | (sK8 = $false) | (~spl0_6 | spl0_16)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f307])).
% 1.80/1.57 thf(f307,plain,(
% 1.80/1.57 (sK8 = $false) | ((b @ $true) = $true) | ($true = $false) | (~spl0_6 | spl0_16)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f305,f72])).
% 1.80/1.57 thf(f299,plain,(
% 1.80/1.57 ~spl0_16 | spl0_15),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f298,f104,f107])).
% 1.80/1.57 thf(f104,definition,(
% 1.80/1.57 spl0_15 <=> ((f5 @ b) = (f5 @ d))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_15])],[avatar_definition])).
% 1.80/1.57 thf(f298,plain,(
% 1.80/1.57 (b != d) | spl0_15),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f105])).
% 1.80/1.57 thf(f105,plain,(
% 1.80/1.57 ((f5 @ b) != (f5 @ d)) | spl0_15),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f104])).
% 1.80/1.57 thf(f297,plain,(
% 1.80/1.57 spl0_48 | spl0_52 | spl0_12 | spl0_14),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f285,f99,f91,f294,f253])).
% 1.80/1.57 thf(f99,definition,(
% 1.80/1.57 spl0_14 <=> (a = b)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_14])],[avatar_definition])).
% 1.80/1.57 thf(f285,plain,(
% 1.80/1.57 ($true = sK7) | ((a @ $false) = $false) | ((b @ $false) = $false) | spl0_14),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f283])).
% 1.80/1.57 thf(f283,plain,(
% 1.80/1.57 ((b @ $false) != (a @ $false)) | ($true = sK7) | spl0_14),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f281])).
% 1.80/1.57 thf(f281,plain,(
% 1.80/1.57 ((a @ sK7) != (b @ sK7)) | spl0_14),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f100])).
% 1.80/1.57 thf(f100,plain,(
% 1.80/1.57 (a != b) | spl0_14),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f99])).
% 1.80/1.57 thf(f296,plain,(
% 1.80/1.57 spl0_45 | spl0_10 | spl0_52 | spl0_14),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f284,f99,f294,f84,f243])).
% 1.80/1.57 thf(f284,plain,(
% 1.80/1.57 ($true = sK7) | ($true = (a @ $false)) | ((b @ $false) = $true) | spl0_14),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f283])).
% 1.80/1.57 thf(f292,plain,(
% 1.80/1.57 spl0_7 | spl0_42 | spl0_51 | spl0_14),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f287,f99,f289,f233,f74])).
% 1.80/1.57 thf(f287,plain,(
% 1.80/1.57 ((b @ $true) = $false) | (sK7 = $false) | ((a @ $true) = $false) | spl0_14),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f282])).
% 1.80/1.57 thf(f282,plain,(
% 1.80/1.57 ((b @ $true) != (a @ $true)) | (sK7 = $false) | spl0_14),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f281])).
% 1.80/1.57 thf(f291,plain,(
% 1.80/1.57 spl0_51 | spl0_40 | spl0_5 | spl0_14),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f286,f99,f67,f226,f289])).
% 1.80/1.57 thf(f286,plain,(
% 1.80/1.57 (sK7 = $false) | ($true = (a @ $true)) | ((b @ $true) = $true) | spl0_14),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f282])).
% 1.80/1.57 thf(f280,plain,(
% 1.80/1.57 ~spl0_14 | spl0_13),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f279,f96,f99])).
% 1.80/1.57 thf(f96,definition,(
% 1.80/1.57 spl0_13 <=> ((f0 @ a) = (f0 @ b))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_13])],[avatar_definition])).
% 1.80/1.57 thf(f279,plain,(
% 1.80/1.57 (a != b) | spl0_13),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f97])).
% 1.80/1.57 thf(f97,plain,(
% 1.80/1.57 ((f0 @ a) != (f0 @ b)) | spl0_13),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f96])).
% 1.80/1.57 thf(f278,plain,(
% 1.80/1.57 ~spl0_4 | ~spl0_8),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f277])).
% 1.80/1.57 thf(f277,plain,(
% 1.80/1.57 $false | (~spl0_4 | ~spl0_8)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f276])).
% 1.80/1.57 thf(f276,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_4 | ~spl0_8)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f79,f65])).
% 1.80/1.57 thf(f65,plain,(
% 1.80/1.57 (sK2 = $false) | ~spl0_4),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f64])).
% 1.80/1.57 thf(f64,definition,(
% 1.80/1.57 spl0_4 <=> (sK2 = $false)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_4])],[avatar_definition])).
% 1.80/1.57 thf(f79,plain,(
% 1.80/1.57 ($true = sK2) | ~spl0_8),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f78])).
% 1.80/1.57 thf(f78,definition,(
% 1.80/1.57 spl0_8 <=> ($true = sK2)),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_8])],[avatar_definition])).
% 1.80/1.57 thf(f275,plain,(
% 1.80/1.57 spl0_11 | spl0_50 | spl0_12 | spl0_1),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f262,f47,f91,f272,f88])).
% 1.80/1.57 thf(f262,plain,(
% 1.80/1.57 ((a @ $false) = $false) | (sK6 = $true) | ((d @ $false) = $false) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f260])).
% 1.80/1.57 thf(f260,plain,(
% 1.80/1.57 (sK6 = $true) | ((d @ $false) != (a @ $false)) | spl0_1),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f258])).
% 1.80/1.57 thf(f274,plain,(
% 1.80/1.57 spl0_9 | spl0_50 | spl0_10 | spl0_1),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f261,f47,f84,f272,f81])).
% 1.80/1.57 thf(f261,plain,(
% 1.80/1.57 (sK6 = $true) | ($true = (a @ $false)) | ($true = (d @ $false)) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f260])).
% 1.80/1.57 thf(f270,plain,(
% 1.80/1.57 spl0_5 | spl0_49 | spl0_1 | ~spl0_6),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f266,f71,f47,f268,f67])).
% 1.80/1.57 thf(f266,plain,(
% 1.80/1.57 (sK6 = $false) | ($true = (a @ $true)) | (spl0_1 | ~spl0_6)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f265])).
% 1.80/1.57 thf(f265,plain,(
% 1.80/1.57 (sK6 = $false) | ($true = $false) | ($true = (a @ $true)) | (spl0_1 | ~spl0_6)),
% 1.80/1.57 inference(forward_demodulation,[status(thm)],[f263,f72])).
% 1.80/1.57 thf(f257,plain,(
% 1.80/1.57 ~spl0_1 | spl0_2),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f256,f50,f47])).
% 1.80/1.57 thf(f50,definition,(
% 1.80/1.57 spl0_2 <=> ((f2 @ a) = (f2 @ d))),
% 1.80/1.57 introduced(definition,[new_symbols(naming,[spl0_2])],[avatar_definition])).
% 1.80/1.57 thf(f256,plain,(
% 1.80/1.57 (a != d) | spl0_2),
% 1.80/1.57 inference(equality_resolution,[status(thm)],[f51])).
% 1.80/1.57 thf(f51,plain,(
% 1.80/1.57 ((f2 @ a) != (f2 @ d)) | spl0_2),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f50])).
% 1.80/1.57 thf(f214,plain,(
% 1.80/1.57 ~spl0_37 | ~spl0_38),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f207,f212,f209])).
% 1.80/1.57 thf(f207,plain,(
% 1.80/1.57 (b != c) | ((f4 @ b) != (f4 @ c))),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f32,f44])).
% 1.80/1.57 thf(f44,plain,(
% 1.80/1.57 ((f4 @ b) = (g4 @ c))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f9])).
% 1.80/1.57 thf(f9,axiom,(
% 1.80/1.57 ((f4 @ b) = (g4 @ c))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotc1)).
% 1.80/1.57 thf(f32,plain,(
% 1.80/1.57 ((f4 @ c) != (g4 @ b))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f10])).
% 1.80/1.57 thf(f10,axiom,(
% 1.80/1.57 ((f4 @ c) != (g4 @ b))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotc2)).
% 1.80/1.57 thf(f206,plain,(
% 1.80/1.57 ~spl0_3 | ~spl0_6),
% 1.80/1.57 inference(avatar_contradiction_clause,[status(thm)],[f205])).
% 1.80/1.57 thf(f205,plain,(
% 1.80/1.57 $false | (~spl0_3 | ~spl0_6)),
% 1.80/1.57 inference(trivial_inequality_removal,[status(thm)],[f204])).
% 1.80/1.57 thf(f204,plain,(
% 1.80/1.57 ($true = $false) | (~spl0_3 | ~spl0_6)),
% 1.80/1.57 inference(backward_demodulation,[status(thm)],[f62,f72])).
% 1.80/1.57 thf(f62,plain,(
% 1.80/1.57 ((d @ $true) = $true) | ~spl0_3),
% 1.80/1.57 inference(avatar_component_clause,[status(thm)],[f61])).
% 1.80/1.57 thf(f203,plain,(
% 1.80/1.57 ~spl0_35 | ~spl0_36),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f196,f201,f198])).
% 1.80/1.57 thf(f196,plain,(
% 1.80/1.57 ((f1 @ a) != (f1 @ c)) | (a != c)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f28,f43])).
% 1.80/1.57 thf(f43,plain,(
% 1.80/1.57 ((f1 @ a) = (g1 @ c))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f3])).
% 1.80/1.57 thf(f3,axiom,(
% 1.80/1.57 ((f1 @ a) = (g1 @ c))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotc1)).
% 1.80/1.57 thf(f28,plain,(
% 1.80/1.57 ((f1 @ c) != (g1 @ a))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f4])).
% 1.80/1.57 thf(f4,axiom,(
% 1.80/1.57 ((f1 @ c) != (g1 @ a))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotc2)).
% 1.80/1.57 thf(f195,plain,(
% 1.80/1.57 ~spl0_33 | ~spl0_34),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f188,f193,f190])).
% 1.80/1.57 thf(f188,plain,(
% 1.80/1.57 (c != d) | ((f7 @ c) != (f7 @ d))),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f42,f31])).
% 1.80/1.57 thf(f31,plain,(
% 1.80/1.57 ((f7 @ c) = (g7 @ d))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f15])).
% 1.80/1.57 thf(f15,axiom,(
% 1.80/1.57 ((f7 @ c) = (g7 @ d))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnotd1)).
% 1.80/1.57 thf(f42,plain,(
% 1.80/1.57 ((f7 @ d) != (g7 @ c))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f16])).
% 1.80/1.57 thf(f16,axiom,(
% 1.80/1.57 ((f7 @ d) != (g7 @ c))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnotd2)).
% 1.80/1.57 thf(f186,plain,(
% 1.80/1.57 spl0_9 | spl0_24 | spl0_32 | spl0_27),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f174,f157,f184,f145,f81])).
% 1.80/1.57 thf(f174,plain,(
% 1.80/1.57 (sK4 = $true) | ($true = (e @ $false)) | ($true = (d @ $false)) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f173])).
% 1.80/1.57 thf(f173,plain,(
% 1.80/1.57 (sK4 = $true) | ((d @ $false) != (e @ $false)) | spl0_27),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f171])).
% 1.80/1.57 thf(f171,plain,(
% 1.80/1.57 ((e @ sK4) != (d @ sK4)) | spl0_27),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f158])).
% 1.80/1.57 thf(f182,plain,(
% 1.80/1.57 spl0_31 | spl0_23 | spl0_6 | spl0_27),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f177,f157,f71,f141,f179])).
% 1.80/1.57 thf(f177,plain,(
% 1.80/1.57 ((d @ $true) = $false) | ((e @ $true) = $false) | (sK4 = $false) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f172])).
% 1.80/1.57 thf(f172,plain,(
% 1.80/1.57 (sK4 = $false) | ((d @ $true) != (e @ $true)) | spl0_27),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f171])).
% 1.80/1.57 thf(f181,plain,(
% 1.80/1.57 spl0_21 | spl0_31 | spl0_3 | spl0_27),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f176,f157,f61,f179,f134])).
% 1.80/1.57 thf(f176,plain,(
% 1.80/1.57 ((d @ $true) = $true) | ($true = (e @ $true)) | (sK4 = $false) | spl0_27),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f172])).
% 1.80/1.57 thf(f170,plain,(
% 1.80/1.57 ~spl0_29 | ~spl0_30),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f163,f168,f165])).
% 1.80/1.57 thf(f163,plain,(
% 1.80/1.57 ((f8 @ c) != (f8 @ e)) | (c != e)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f38,f41])).
% 1.80/1.57 thf(f41,plain,(
% 1.80/1.57 ((f8 @ c) = (g8 @ e))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f17])).
% 1.80/1.57 thf(f17,axiom,(
% 1.80/1.57 ((f8 @ c) = (g8 @ e))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnote1)).
% 1.80/1.57 thf(f38,plain,(
% 1.80/1.57 ((f8 @ e) != (g8 @ c))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f18])).
% 1.80/1.57 thf(f18,axiom,(
% 1.80/1.57 ((f8 @ e) != (g8 @ c))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',cnote2)).
% 1.80/1.57 thf(f162,plain,(
% 1.80/1.57 ~spl0_27 | ~spl0_28),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f155,f160,f157])).
% 1.80/1.57 thf(f155,plain,(
% 1.80/1.57 (d != e) | ((f9 @ d) != (f9 @ e))),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f40,f39])).
% 1.80/1.57 thf(f39,plain,(
% 1.80/1.57 ((f9 @ d) = (g9 @ e))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f19])).
% 1.80/1.57 thf(f19,axiom,(
% 1.80/1.57 ((f9 @ d) = (g9 @ e))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',dnote1)).
% 1.80/1.57 thf(f40,plain,(
% 1.80/1.57 ((f9 @ e) != (g9 @ d))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f20])).
% 1.80/1.57 thf(f20,axiom,(
% 1.80/1.57 ((f9 @ e) != (g9 @ d))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',dnote2)).
% 1.80/1.57 thf(f125,plain,(
% 1.80/1.57 ~spl0_19 | ~spl0_20),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f118,f123,f120])).
% 1.80/1.57 thf(f118,plain,(
% 1.80/1.57 (a != e) | ((f3 @ a) != (f3 @ e))),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f37,f34])).
% 1.80/1.57 thf(f34,plain,(
% 1.80/1.57 ((f3 @ a) = (g3 @ e))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f7])).
% 1.80/1.57 thf(f7,axiom,(
% 1.80/1.57 ((f3 @ a) = (g3 @ e))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anote1)).
% 1.80/1.57 thf(f37,plain,(
% 1.80/1.57 ((f3 @ e) != (g3 @ a))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f8])).
% 1.80/1.57 thf(f8,axiom,(
% 1.80/1.57 ((f3 @ e) != (g3 @ a))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anote2)).
% 1.80/1.57 thf(f117,plain,(
% 1.80/1.57 ~spl0_17 | ~spl0_18),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f110,f115,f112])).
% 1.80/1.57 thf(f110,plain,(
% 1.80/1.57 ((f6 @ b) != (f6 @ e)) | (b != e)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f35,f36])).
% 1.80/1.57 thf(f36,plain,(
% 1.80/1.57 ((f6 @ b) = (g6 @ e))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f13])).
% 1.80/1.57 thf(f13,axiom,(
% 1.80/1.57 ((f6 @ b) = (g6 @ e))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnote1)).
% 1.80/1.57 thf(f35,plain,(
% 1.80/1.57 ((f6 @ e) != (g6 @ b))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f14])).
% 1.80/1.57 thf(f14,axiom,(
% 1.80/1.57 ((f6 @ e) != (g6 @ b))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnote2)).
% 1.80/1.57 thf(f109,plain,(
% 1.80/1.57 ~spl0_15 | ~spl0_16),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f102,f107,f104])).
% 1.80/1.57 thf(f102,plain,(
% 1.80/1.57 ((f5 @ b) != (f5 @ d)) | (b != d)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f33,f26])).
% 1.80/1.57 thf(f26,plain,(
% 1.80/1.57 ((f5 @ b) = (g5 @ d))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f11])).
% 1.80/1.57 thf(f11,axiom,(
% 1.80/1.57 ((f5 @ b) = (g5 @ d))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotd1)).
% 1.80/1.57 thf(f33,plain,(
% 1.80/1.57 ((f5 @ d) != (g5 @ b))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f12])).
% 1.80/1.57 thf(f12,axiom,(
% 1.80/1.57 ((f5 @ d) != (g5 @ b))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',bnotd2)).
% 1.80/1.57 thf(f101,plain,(
% 1.80/1.57 ~spl0_13 | ~spl0_14),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f94,f99,f96])).
% 1.80/1.57 thf(f94,plain,(
% 1.80/1.57 ((f0 @ a) != (f0 @ b)) | (a != b)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f30,f29])).
% 1.80/1.57 thf(f29,plain,(
% 1.80/1.57 ((f0 @ a) = (g0 @ b))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f1])).
% 1.80/1.57 thf(f1,axiom,(
% 1.80/1.57 ((f0 @ a) = (g0 @ b))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotb1)).
% 1.80/1.57 thf(f30,plain,(
% 1.80/1.57 ((f0 @ b) != (g0 @ a))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f2])).
% 1.80/1.57 thf(f2,axiom,(
% 1.80/1.57 ((f0 @ b) != (g0 @ a))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotb2)).
% 1.80/1.57 thf(f93,plain,(
% 1.80/1.57 spl0_11 | spl0_8 | spl0_12 | spl0_1),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f57,f47,f91,f78,f88])).
% 1.80/1.57 thf(f57,plain,(
% 1.80/1.57 ((d @ $false) = $false) | ($true = sK2) | ((a @ $false) = $false) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f55])).
% 1.80/1.57 thf(f55,plain,(
% 1.80/1.57 ($true = sK2) | ((d @ $false) != (a @ $false)) | spl0_1),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f53])).
% 1.80/1.57 thf(f53,plain,(
% 1.80/1.57 ((a @ sK2) != (d @ sK2)) | spl0_1),
% 1.80/1.57 inference(negative_extensionality,[status(thm)],[f48])).
% 1.80/1.57 thf(f76,plain,(
% 1.80/1.57 spl0_6 | spl0_4 | spl0_7 | spl0_1),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f59,f47,f74,f64,f71])).
% 1.80/1.57 thf(f59,plain,(
% 1.80/1.57 ((a @ $true) = $false) | ((d @ $true) = $false) | (sK2 = $false) | spl0_1),
% 1.80/1.57 inference(binary_proxy_clausification,[status(thm)],[f54])).
% 1.80/1.57 thf(f54,plain,(
% 1.80/1.57 (sK2 = $false) | ((d @ $true) != (a @ $true)) | spl0_1),
% 1.80/1.57 inference(cases_simplifying,[status(thm)],[f53])).
% 1.80/1.57 thf(f52,plain,(
% 1.80/1.57 ~spl0_1 | ~spl0_2),
% 1.80/1.57 inference(avatar_split_clause,[status(thm)],[f45,f50,f47])).
% 1.80/1.57 thf(f45,plain,(
% 1.80/1.57 ((f2 @ a) != (f2 @ d)) | (a != d)),
% 1.80/1.57 inference(constrained_superposition,[status(thm)],[f27,f25])).
% 1.80/1.57 thf(f25,plain,(
% 1.80/1.57 ((f2 @ a) = (g2 @ d))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f5])).
% 1.80/1.57 thf(f5,axiom,(
% 1.80/1.57 ((f2 @ a) = (g2 @ d))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotd1)).
% 1.80/1.57 thf(f27,plain,(
% 1.80/1.57 ((f2 @ d) != (g2 @ a))),
% 1.80/1.57 inference(cnf_transformation,[status(thm)],[f6])).
% 1.80/1.57 thf(f6,axiom,(
% 1.80/1.57 ((f2 @ d) != (g2 @ a))),
% 1.80/1.57 file('/export/starexec/sandbox2/tmp/tmp.nnRNQRA4hG/DTF2THF_17938.p',anotd2)).
% 1.80/1.57 % SZS output end Proof for DTF2THF_17938
% 1.80/1.57 % (18257)------------------------------
% 1.80/1.57 % (18257)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.80/1.57 % (18257)Termination reason: Refutation
% 1.80/1.57
% 1.80/1.57 % (18257)Memory used [KB]: 5884
% 1.80/1.57 % (18257)Time elapsed: 0.019 s
% 1.80/1.57 % (18257)Instructions burned: 36 (million)
% 1.80/1.57 % (18257)------------------------------
% 1.80/1.57 % (18257)------------------------------
% 1.80/1.57 % (18208)Success in time 0.165 s
%------------------------------------------------------------------------------