%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : GRA028^1 : TPTP v9.2.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n021.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 08:48:48 AM UTC 2026
% Result : Theorem 1.70s 1.53s
% Output : Refutation 1.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 7
% Syntax : Number of formulae : 79 ( 4 unt; 0 typ; 4 def)
% Number of atoms : 1168 ( 602 equ; 4 cnn)
% Maximal formula atoms : 46 ( 14 avg)
% Number of connectives : 1386 ( 177 ~; 488 |; 107 &; 599 @)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 12 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 396 ( 396 >; 0 *; 0 +; 0 <<)
% Number of symbols : 11 ( 7 usr; 7 con; 0-2 aty)
% Number of variables : 418 ( 33 ^; 331 !; 54 ?; 418 :)
% Comments :
%------------------------------------------------------------------------------
thf(func_def_3,type,
sK0: ( $o > $o ) > ( $o > $o ) > $o ).
thf(func_def_9,type,
ph2:
!>[X0: $tType] : X0 ).
thf(func_def_10,type,
sK3: $o > $o ).
thf(f779,plain,
$false,
inference(avatar_sat_refutation,[status(thm)],[f379,f445,f482,f690,f778]) ).
thf(f778,plain,
~ spl1_1,
inference(avatar_contradiction_clause,[status(thm)],[f777]) ).
thf(f777,plain,
( $false
| ~ spl1_1 ),
inference(equality_resolution,[status(thm)],[f719]) ).
thf(f719,plain,
( ! [X0: $o] : ( $false != X0 )
| ~ spl1_1 ),
inference(superposition,[status(thm)],[f3,f290]) ).
thf(f290,plain,
( ! [X4: $o] : ( $true = X4 )
| ~ spl1_1 ),
inference(avatar_component_clause,[status(thm)],[f289]) ).
thf(f289,definition,
( spl1_1
<=> ! [X4: $o] : ( $true = X4 ) ),
introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition]) ).
thf(f3,plain,
$false != $true,
introduced(definition,[],[fool_axiom]) ).
thf(f690,plain,
( spl1_1
| spl1_3
| spl1_3
| ~ spl1_10 ),
inference(avatar_split_clause,[status(thm)],[f664,f480,f366,f366,f289]) ).
thf(f366,definition,
( spl1_3
<=> ! [X1: $o] : ( $false = X1 ) ),
introduced(definition,[new_symbols(naming,[spl1_3])],[avatar_definition]) ).
thf(f480,definition,
( spl1_10
<=> ! [X2: $o > $o,X4: $o,X3: $o] :
( ( ( X2 @ X3 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( $false = X4 )
| ( ( X2 @ X4 )
= $true ) ) ),
introduced(definition,[new_symbols(naming,[spl1_10])],[avatar_definition]) ).
thf(f664,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( $false = X2 )
| ( $false = X0 )
| ( $true = X1 ) )
| ~ spl1_10 ),
inference(duplicate_literal_removal,[status(thm)],[f662]) ).
thf(f662,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( $true = X1 )
| ( $true = X1 )
| ( $false = X0 )
| ( $false = X2 ) )
| ~ spl1_10 ),
inference(binary_proxy_clausification,[status(thm)],[f661]) ).
thf(f661,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( $true = X1 )
| ( X1 = X2 )
| ( $false = X0 ) )
| ~ spl1_10 ),
inference(equality_proxy_clausification,[status(thm)],[f660]) ).
thf(f660,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( $true = X1 )
| ( ( X1 = X2 )
= $true )
| ( $false = X0 ) )
| ~ spl1_10 ),
inference(duplicate_literal_removal,[status(thm)],[f659]) ).
thf(f659,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( $true = X1 )
| ( $false = X0 )
| ( ( X1 = X2 )
= $true )
| ( $false = X0 ) )
| ~ spl1_10 ),
inference(binary_proxy_clausification,[status(thm)],[f638]) ).
thf(f638,plain,
( ! [X2: $o,X0: $o,X1: $o] :
( ( X0 = X1 )
| ( ( X1 = X2 )
= $true )
| ( $false = X0 ) )
| ~ spl1_10 ),
inference(leibniz_equality_elimination,[status(thm)],[f620]) ).
thf(f620,plain,
( ! [X2: $o > $o,X3: $o,X4: $o,X5: $o] :
( ( $false
= ( X2 @ X5 ) )
| ( $false = X4 )
| ( ( X2 @ X4 )
= $true )
| ( ( X2 @ X3 )
= $true ) )
| ~ spl1_10 ),
inference(beta_eta_normalization,[status(thm)],[f616]) ).
thf(f616,plain,
( ! [X2: $o > $o,X3: $o,X4: $o,X5: $o] :
( ( $false = X4 )
| ( ( X2 @ X4 )
= $true )
| ( ( X2 @ X5 )
= ( ^ [Y0: $o] : $false
@ X5 ) )
| ( ( X2 @ X3 )
= $true ) )
| ~ spl1_10 ),
inference(argument_congruence,[status(thm)],[f481]) ).
thf(f481,plain,
( ! [X2: $o > $o,X3: $o,X4: $o] :
( ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( X2 @ X3 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( $false = X4 ) )
| ~ spl1_10 ),
inference(avatar_component_clause,[status(thm)],[f480]) ).
thf(f482,plain,
( spl1_10
| spl1_3
| ~ spl1_6 ),
inference(avatar_split_clause,[status(thm)],[f471,f377,f366,f480]) ).
thf(f377,definition,
( spl1_6
<=> ! [X2: $o > $o,X1: $o,X3: $o] :
( ( ( (=) @ X1 )
= X2 )
| ( ( X2 @ X3 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( $false = X1 ) ) ),
introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition]) ).
thf(f471,plain,
( ! [X2: $o > $o,X3: $o,X1: $o,X4: $o] :
( ( ( X2 @ X3 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( $false = X4 )
| ( $false = X1 )
| ( ( ^ [Y0: $o] : $false )
= X2 ) )
| ~ spl1_6 ),
inference(duplicate_literal_removal,[status(thm)],[f470]) ).
thf(f470,plain,
( ! [X2: $o > $o,X3: $o,X1: $o,X4: $o] :
( ( ( X2 @ X3 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( $false = X4 )
| ( $false = X1 )
| ( $false = X1 )
| ( ( X2 @ X4 )
= $true ) )
| ~ spl1_6 ),
inference(binary_proxy_clausification,[status(thm)],[f468]) ).
thf(f468,plain,
( ! [X2: $o > $o,X3: $o,X1: $o,X4: $o] :
( ( $false = X1 )
| ( ( X2 @ X4 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( X2 @ X3 )
= $true )
| ( X1 != X4 ) )
| ~ spl1_6 ),
inference(equality_proxy_clausification,[status(thm)],[f462]) ).
thf(f462,plain,
( ! [X2: $o > $o,X3: $o,X1: $o,X4: $o] :
( ( $false = X1 )
| ( $false
= ( X1 = X4 ) )
| ( ( X2 @ X4 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( X2 @ X3 )
= $true ) )
| ~ spl1_6 ),
inference(binary_proxy_clausification,[status(thm)],[f456]) ).
thf(f456,plain,
( ! [X2: $o > $o,X3: $o,X1: $o,X4: $o] :
( ( ( ^ [Y0: $o] : $false )
= X2 )
| ( $false = X1 )
| ( ( X2 @ X4 )
= ( X1 = X4 ) )
| ( ( X2 @ X3 )
= $true ) )
| ~ spl1_6 ),
inference(argument_congruence,[status(thm)],[f378]) ).
thf(f378,plain,
( ! [X2: $o > $o,X3: $o,X1: $o] :
( ( ( (=) @ X1 )
= X2 )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( X2 @ X3 )
= $true )
| ( $false = X1 ) )
| ~ spl1_6 ),
inference(avatar_component_clause,[status(thm)],[f377]) ).
thf(f445,plain,
~ spl1_3,
inference(avatar_contradiction_clause,[status(thm)],[f444]) ).
thf(f444,plain,
( $false
| ~ spl1_3 ),
inference(trivial_inequality_removal,[status(thm)],[f443]) ).
thf(f443,plain,
( ( $false != $false )
| ~ spl1_3 ),
inference(superposition,[status(thm)],[f3,f367]) ).
thf(f367,plain,
( ! [X1: $o] : ( $false = X1 )
| ~ spl1_3 ),
inference(avatar_component_clause,[status(thm)],[f366]) ).
thf(f379,plain,
( spl1_1
| spl1_6 ),
inference(avatar_split_clause,[status(thm)],[f360,f377,f289]) ).
thf(f360,plain,
! [X2: $o > $o,X3: $o,X0: $o,X1: $o] :
( ( ( (=) @ X1 )
= X2 )
| ( $true = X0 )
| ( $false = X1 )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( X2 @ X3 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f348]) ).
thf(f348,plain,
! [X2: $o > $o,X3: $o,X0: $o,X1: $o] :
( ( X0 = X1 )
| ( ( ^ [Y0: $o] : $false )
= X2 )
| ( ( (=) @ X1 )
= X2 )
| ( ( X2 @ X3 )
= $true ) ),
inference(leibniz_equality_elimination,[status(thm)],[f325]) ).
thf(f325,plain,
! [X0: $o > $o,X1: $o > $o,X6: $o,X7: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $false )
= X0 )
| ( ( X0 @ X6 )
= $true )
| ( ( X1 @ X5 )
= $true )
| ( $false
= ( X1 @ X7 ) )
| ( X0 = X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f317]) ).
thf(f317,plain,
! [X0: $o > $o,X1: $o > $o,X6: $o,X7: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $false )
= X0 )
| ( X0 = X1 )
| ( ( X1 @ X5 )
= $true )
| ( ( X0 @ X6 )
= $true )
| ( ( X1 @ X7 )
= ( ^ [Y0: $o] : $false
@ X7 ) ) ),
inference(argument_congruence,[status(thm)],[f285]) ).
thf(f285,plain,
! [X0: $o > $o,X1: $o > $o,X6: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $false )
= X1 )
| ( ( X1 @ X5 )
= $true )
| ( ( X0 @ X6 )
= $true )
| ( X0 = X1 )
| ( ( ^ [Y0: $o] : $false )
= X0 ) ),
inference(trivial_inequality_removal,[status(thm)],[f284]) ).
thf(f284,plain,
! [X0: $o > $o,X1: $o > $o,X6: $o,X5: $o] :
( ( ( X0 @ X6 )
= $true )
| ( X0 = X1 )
| ( ( X1 @ X5 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X0 )
| ( $false = $true )
| ( ( ^ [Y0: $o] : $false )
= X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f272]) ).
thf(f272,plain,
! [X0: $o > $o,X1: $o > $o,X6: $o,X4: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $false
@ X4 )
= $true )
| ( ( X1 @ X5 )
= $true )
| ( ( X0 @ X6 )
= $true )
| ( ( ^ [Y0: $o] : $false )
= X0 )
| ( X0 = X1 )
| ( ( ^ [Y0: $o] : $false )
= X1 ) ),
inference(primitive_instantiation,[status(thm)],[f241]) ).
thf(f241,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X6: $o,X4: $o,X5: $o] :
( ( ( X2 @ X4 )
= $true )
| ( X0 = X1 )
| ( X1 = X2 )
| ( ( X0 @ X6 )
= $true )
| ( X0 = X2 )
| ( ( X1 @ X5 )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f227]) ).
thf(f227,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X6: $o,X4: $o,X5: $o] :
( ( ( X2 @ X4 )
= $true )
| ( X0 = X2 )
| ( X1 = X2 )
| ( X0 = X1 )
| ( ( ^ [Y0: $o] : $true
@ X6 )
= ( X0 @ X6 ) )
| ( ( X1 @ X5 )
= $true ) ),
inference(argument_congruence,[status(thm)],[f210]) ).
thf(f210,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $true )
= X0 )
| ( X1 = X2 )
| ( X0 = X1 )
| ( X0 = X2 )
| ( ( X1 @ X5 )
= $true )
| ( ( X2 @ X4 )
= $true ) ),
inference(beta_eta_normalization,[status(thm)],[f191]) ).
thf(f191,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o,X5: $o] :
( ( ( ^ [Y0: $o] : $true )
= X0 )
| ( X0 = X2 )
| ( X0 = X1 )
| ( ( X2 @ X4 )
= $true )
| ( X1 = X2 )
| ( ( ^ [Y0: $o] : $true
@ X5 )
= ( X1 @ X5 ) ) ),
inference(argument_congruence,[status(thm)],[f167]) ).
thf(f167,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o] :
( ( ( ^ [Y0: $o] : $true )
= X1 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( X0 = X1 )
| ( ( ^ [Y0: $o] : $true )
= X0 )
| ( ( X2 @ X4 )
= $true ) ),
inference(trivial_inequality_removal,[status(thm)],[f166]) ).
thf(f166,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o] :
( ( ( ^ [Y0: $o] : $true )
= X1 )
| ( ( ^ [Y0: $o] : $true )
= X0 )
| ( X1 = X2 )
| ( X0 = X2 )
| ( ( X2 @ X4 )
= $true )
| ( $false = $true )
| ( X0 = X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f160]) ).
thf(f160,plain,
! [X2: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o] :
( ( ( ^ [Y0: $o] : $true )
= X0 )
| ( X0 = X1 )
| ( ( X2 @ X4 )
= $true )
| ( X0 = X2 )
| ( X1 = X2 )
| ( $false
= ( ^ [Y0: $o] : $true
@ X4 ) )
| ( ( ^ [Y0: $o] : $true )
= X1 ) ),
inference(primitive_instantiation,[status(thm)],[f129]) ).
thf(f129,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o] :
( ( $false
= ( X3 @ X4 ) )
| ( ( X2 @ X4 )
= $true )
| ( X0 = X1 )
| ( X0 = X3 )
| ( X1 = X2 )
| ( X1 = X3 )
| ( X0 = X2 ) ),
inference(binary_proxy_clausification,[status(thm)],[f115]) ).
thf(f115,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o,X4: $o] :
( ( ( X2 @ X4 )
= ( X3 @ X4 ) )
| ( X0 = X1 )
| ( X0 = X3 )
| ( X0 = X2 )
| ( X1 = X2 )
| ( X1 = X3 ) ),
inference(argument_congruence,[status(thm)],[f88]) ).
thf(f88,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o] :
( ( X2 = X3 )
| ( X0 = X1 )
| ( X0 = X2 )
| ( X0 = X3 )
| ( X1 = X2 )
| ( X1 = X3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f87]) ).
thf(f87,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o] :
( ( X0 = X2 )
| ( X1 = X2 )
| ( X0 = X3 )
| ( X2 = X3 )
| ( X0 = X1 )
| ( $true
= ( X1 = X3 ) ) ),
inference(duplicate_literal_removal,[status(thm)],[f86]) ).
thf(f86,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o] :
( ( X0 = X1 )
| ( X1 = X2 )
| ( X1 = X2 )
| ( X2 = X3 )
| ( $true
= ( X1 = X3 ) )
| ( X0 = X2 )
| ( X0 = X3 ) ),
inference(equality_proxy_clausification,[status(thm)],[f85]) ).
thf(f85,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o] :
( ( X0 = X3 )
| ( ( X1 = X2 )
= $true )
| ( X0 = X1 )
| ( X0 = X2 )
| ( X2 = X3 )
| ( $true
= ( X1 = X3 ) )
| ( X1 = X2 ) ),
inference(duplicate_literal_removal,[status(thm)],[f71]) ).
thf(f71,plain,
! [X2: $o > $o,X3: $o > $o,X0: $o > $o,X1: $o > $o] :
( ( ( X1 = X2 )
= $true )
| ( X0 = X1 )
| ( X0 = X3 )
| ( $true
= ( X1 = X3 ) )
| ( X0 = X2 )
| ( X1 = X2 )
| ( X2 = X3 )
| ( X0 = X1 ) ),
inference(leibniz_equality_elimination,[status(thm)],[f68]) ).
thf(f68,plain,
! [X2: $o > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o] :
( ( ( X3 @ X1 )
!= $true )
| ( X0 = X4 )
| ( X0 = X2 )
| ( $true
= ( X3 @ X2 ) )
| ( X0 = X1 )
| ( ( X3 @ X4 )
= $true )
| ( X2 = X4 )
| ( ( X3 @ X0 )
= $true )
| ( X1 = X2 ) ),
inference(duplicate_literal_removal,[status(thm)],[f67]) ).
thf(f67,plain,
! [X2: $o > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o] :
( ( X1 = X2 )
| ( ( X3 @ X0 )
= $true )
| ( X0 = X2 )
| ( X0 = X4 )
| ( ( X3 @ X1 )
!= $true )
| ( ( X3 @ X4 )
= $true )
| ( X0 = X1 )
| ( $true
= ( X3 @ X2 ) )
| ( X0 = X2 )
| ( X2 = X4 ) ),
inference(equality_proxy_clausification,[status(thm)],[f66]) ).
thf(f66,plain,
! [X2: $o > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o] :
( ( X0 = X4 )
| ( $true
= ( X0 = X2 ) )
| ( ( X3 @ X1 )
!= $true )
| ( X2 = X4 )
| ( $true
= ( X3 @ X2 ) )
| ( ( X3 @ X0 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( X0 = X1 )
| ( X0 = X2 )
| ( X1 = X2 ) ),
inference(equality_proxy_clausification,[status(thm)],[f51]) ).
thf(f51,plain,
! [X2: $o > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o] :
( ( $true
= ( X3 @ X2 ) )
| ( X1 = X2 )
| ( X0 = X2 )
| ( ( X3 @ X0 )
= $true )
| ( ( X0 = X4 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( ( X3 @ X1 )
!= $true )
| ( X2 = X4 )
| ( X0 = X1 )
| ( $true
= ( X0 = X2 ) ) ),
inference(leibniz_equality_elimination,[status(thm)],[f50]) ).
thf(f50,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( $true
!= ( X2 @ X0 ) )
| ( X1 = X5 )
| ( ( X2 @ X4 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( ( X3 @ X0 )
= $true )
| ( ( X2 @ X5 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( X0 = X1 )
| ( X1 = X4 ) ),
inference(subsumption_resolution,[status(thm)],[f49,f16]) ).
thf(f16,plain,
! [X0: $o > $o,X1: $o > $o] :
( ( ( sK0 @ X1 @ X0 )
!= $true )
| ( X0 = X1 ) ),
inference(leibniz_equality_elimination,[status(thm)],[f12]) ).
thf(f12,plain,
! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( sK0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true )
| ( ( X10 @ X11 )
!= $true ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
( ! [X1: $o > $o,X2: $o > $o,X3: ( $o > $o ) > $o,X4: $o > $o,X5: $o > $o,X6: ( $o > $o ) > $o,X7: ( $o > $o ) > $o] :
( ( ( X7 @ X4 )
= $true )
| ( $true
= ( sK0 @ X1 @ X2 ) )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X6 @ X5 )
!= $true )
| ( $true
!= ( X3 @ X2 ) )
| ( ( sK0 @ X4 @ X5 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( ( X6 @ X2 )
= $true )
| ( ( X7 @ X1 )
!= $true )
| ( ( X6 @ X1 )
= $true )
| ( ( sK0 @ X1 @ X5 )
= $true )
| ( $true
= ( sK0 @ X5 @ X2 ) )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X7 @ X5 )
= $true )
| ( ( sK0 @ X4 @ X2 )
= $true )
| ( ( X6 @ X4 )
= $true )
| ( $true
= ( X7 @ X2 ) ) )
& ! [X8: $o > $o,X9: $o > $o] :
( ( ( sK0 @ X8 @ X9 )
= $true )
| ( ( sK0 @ X9 @ X8 )
!= $true ) )
& ! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( sK0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f9,f10]) ).
thf(f10,plain,
( ? [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X1: $o > $o,X2: $o > $o,X3: ( $o > $o ) > $o,X4: $o > $o,X5: $o > $o,X6: ( $o > $o ) > $o,X7: ( $o > $o ) > $o] :
( ( ( X7 @ X4 )
= $true )
| ( ( X0 @ X1 @ X2 )
= $true )
| ( ( X0 @ X4 @ X1 )
= $true )
| ( ( X6 @ X5 )
!= $true )
| ( $true
!= ( X3 @ X2 ) )
| ( ( X0 @ X4 @ X5 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( ( X6 @ X2 )
= $true )
| ( ( X7 @ X1 )
!= $true )
| ( ( X6 @ X1 )
= $true )
| ( ( X0 @ X1 @ X5 )
= $true )
| ( ( X0 @ X5 @ X2 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X7 @ X5 )
= $true )
| ( ( X0 @ X4 @ X2 )
= $true )
| ( ( X6 @ X4 )
= $true )
| ( $true
= ( X7 @ X2 ) ) )
& ! [X8: $o > $o,X9: $o > $o] :
( ( ( X0 @ X8 @ X9 )
= $true )
| ( $true
!= ( X0 @ X9 @ X8 ) ) )
& ! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( X0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) ) )
=> ( ! [X7: ( $o > $o ) > $o,X6: ( $o > $o ) > $o,X5: $o > $o,X4: $o > $o,X3: ( $o > $o ) > $o,X2: $o > $o,X1: $o > $o] :
( ( ( X7 @ X4 )
= $true )
| ( $true
= ( sK0 @ X1 @ X2 ) )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X6 @ X5 )
!= $true )
| ( $true
!= ( X3 @ X2 ) )
| ( ( sK0 @ X4 @ X5 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( ( X6 @ X2 )
= $true )
| ( ( X7 @ X1 )
!= $true )
| ( ( X6 @ X1 )
= $true )
| ( ( sK0 @ X1 @ X5 )
= $true )
| ( $true
= ( sK0 @ X5 @ X2 ) )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X7 @ X5 )
= $true )
| ( ( sK0 @ X4 @ X2 )
= $true )
| ( ( X6 @ X4 )
= $true )
| ( $true
= ( X7 @ X2 ) ) )
& ! [X9: $o > $o,X8: $o > $o] :
( ( ( sK0 @ X8 @ X9 )
= $true )
| ( ( sK0 @ X9 @ X8 )
!= $true ) )
& ! [X12: $o > $o,X11: $o > $o,X10: ( $o > $o ) > $o] :
( ( ( sK0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f9,plain,
? [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X1: $o > $o,X2: $o > $o,X3: ( $o > $o ) > $o,X4: $o > $o,X5: $o > $o,X6: ( $o > $o ) > $o,X7: ( $o > $o ) > $o] :
( ( ( X7 @ X4 )
= $true )
| ( ( X0 @ X1 @ X2 )
= $true )
| ( ( X0 @ X4 @ X1 )
= $true )
| ( ( X6 @ X5 )
!= $true )
| ( $true
!= ( X3 @ X2 ) )
| ( ( X0 @ X4 @ X5 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( ( X6 @ X2 )
= $true )
| ( ( X7 @ X1 )
!= $true )
| ( ( X6 @ X1 )
= $true )
| ( ( X0 @ X1 @ X5 )
= $true )
| ( ( X0 @ X5 @ X2 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X7 @ X5 )
= $true )
| ( ( X0 @ X4 @ X2 )
= $true )
| ( ( X6 @ X4 )
= $true )
| ( $true
= ( X7 @ X2 ) ) )
& ! [X8: $o > $o,X9: $o > $o] :
( ( ( X0 @ X8 @ X9 )
= $true )
| ( $true
!= ( X0 @ X9 @ X8 ) ) )
& ! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( X0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) ) ),
inference(rectify,[status(thm)],[f8]) ).
thf(f8,plain,
? [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X6: $o > $o,X9: $o > $o,X3: ( $o > $o ) > $o,X8: $o > $o,X4: $o > $o,X5: ( $o > $o ) > $o,X7: ( $o > $o ) > $o] :
( ( $true
= ( X7 @ X8 ) )
| ( ( X0 @ X6 @ X9 )
= $true )
| ( ( X0 @ X8 @ X6 )
= $true )
| ( ( X5 @ X4 )
!= $true )
| ( ( X3 @ X9 )
!= $true )
| ( ( X0 @ X8 @ X4 )
= $true )
| ( ( X3 @ X8 )
= $true )
| ( ( X5 @ X9 )
= $true )
| ( ( X7 @ X6 )
!= $true )
| ( ( X5 @ X6 )
= $true )
| ( ( X0 @ X6 @ X4 )
= $true )
| ( ( X0 @ X4 @ X9 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( $true
= ( X3 @ X6 ) )
| ( ( X7 @ X4 )
= $true )
| ( ( X0 @ X8 @ X9 )
= $true )
| ( ( X5 @ X8 )
= $true )
| ( ( X7 @ X9 )
= $true ) )
& ! [X2: $o > $o,X1: $o > $o] :
( ( ( X0 @ X2 @ X1 )
= $true )
| ( ( X0 @ X1 @ X2 )
!= $true ) )
& ! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( X0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) ) ),
inference(flattening,[status(thm)],[f7]) ).
thf(f7,plain,
? [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( X0 @ X12 @ X11 )
!= $true )
| ( ( X10 @ X11 )
!= $true )
| ( ( X10 @ X12 )
= $true ) )
& ! [X6: $o > $o,X9: $o > $o,X3: ( $o > $o ) > $o,X8: $o > $o,X4: $o > $o,X5: ( $o > $o ) > $o,X7: ( $o > $o ) > $o] :
( ( $true
= ( X7 @ X8 ) )
| ( ( X0 @ X6 @ X9 )
= $true )
| ( ( X0 @ X8 @ X6 )
= $true )
| ( ( X5 @ X4 )
!= $true )
| ( ( X3 @ X9 )
!= $true )
| ( ( X0 @ X8 @ X4 )
= $true )
| ( ( X3 @ X8 )
= $true )
| ( ( X5 @ X9 )
= $true )
| ( ( X7 @ X6 )
!= $true )
| ( ( X5 @ X6 )
= $true )
| ( ( X0 @ X6 @ X4 )
= $true )
| ( ( X0 @ X4 @ X9 )
= $true )
| ( ( X3 @ X4 )
= $true )
| ( $true
= ( X3 @ X6 ) )
| ( ( X7 @ X4 )
= $true )
| ( ( X0 @ X8 @ X9 )
= $true )
| ( ( X5 @ X8 )
= $true )
| ( ( X7 @ X9 )
= $true ) )
& ! [X2: $o > $o,X1: $o > $o] :
( ( ( X0 @ X2 @ X1 )
= $true )
| ( ( X0 @ X1 @ X2 )
!= $true ) ) ),
inference(ennf_transformation,[status(thm)],[f6]) ).
thf(f6,plain,
~ ! [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X2: $o > $o,X1: $o > $o] :
( ( ( X0 @ X1 @ X2 )
= $true )
=> ( ( X0 @ X2 @ X1 )
= $true ) )
=> ( ? [X12: $o > $o,X11: $o > $o,X10: ( $o > $o ) > $o] :
( ( ( X0 @ X12 @ X11 )
= $true )
& ( ( X10 @ X12 )
!= $true )
& ( ( X10 @ X11 )
= $true ) )
| ? [X6: $o > $o,X5: ( $o > $o ) > $o,X8: $o > $o,X4: $o > $o,X3: ( $o > $o ) > $o,X7: ( $o > $o ) > $o,X9: $o > $o] :
( ( ( X3 @ X9 )
= $true )
& ( ( X0 @ X6 @ X4 )
!= $true )
& ( ( X0 @ X8 @ X9 )
!= $true )
& ( ( X5 @ X8 )
!= $true )
& ( ( X3 @ X4 )
!= $true )
& ( ( X7 @ X4 )
!= $true )
& ( ( X0 @ X4 @ X9 )
!= $true )
& ( ( X7 @ X9 )
!= $true )
& ( ( X3 @ X8 )
!= $true )
& ( ( X0 @ X8 @ X6 )
!= $true )
& ( $true
!= ( X3 @ X6 ) )
& ( ( X7 @ X6 )
= $true )
& ( ( X0 @ X6 @ X9 )
!= $true )
& ( ( X5 @ X9 )
!= $true )
& ( $true
!= ( X7 @ X8 ) )
& ( ( X5 @ X6 )
!= $true )
& ( ( X5 @ X4 )
= $true )
& ( ( X0 @ X8 @ X4 )
!= $true ) ) ) ),
inference(flattening,[status(thm)],[f5]) ).
thf(f5,plain,
~ ! [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X2: $o > $o,X1: $o > $o] :
( ( ( X0 @ X1 @ X2 )
= $true )
=> ( ( X0 @ X2 @ X1 )
= $true ) )
=> ( ? [X3: ( $o > $o ) > $o,X4: $o > $o,X5: ( $o > $o ) > $o,X6: $o > $o,X7: ( $o > $o ) > $o,X8: $o > $o,X9: $o > $o] :
( ( ( X5 @ X8 )
!= $true )
& ( ( X0 @ X6 @ X4 )
!= $true )
& ( ( X0 @ X6 @ X9 )
!= $true )
& ( ( X0 @ X8 @ X9 )
!= $true )
& ( ( X0 @ X8 @ X6 )
!= $true )
& ( ( X3 @ X8 )
!= $true )
& ( ( X5 @ X6 )
!= $true )
& ( $true
!= ( X3 @ X6 ) )
& ( ( X0 @ X8 @ X4 )
!= $true )
& ( ( X7 @ X9 )
!= $true )
& ( ( X3 @ X9 )
= $true )
& ( ( X7 @ X6 )
= $true )
& ( ( X3 @ X4 )
!= $true )
& ( ( X5 @ X9 )
!= $true )
& ( $true
!= ( X7 @ X8 ) )
& ( ( X5 @ X4 )
= $true )
& ( ( X0 @ X4 @ X9 )
!= $true )
& ( ( X7 @ X4 )
!= $true ) )
| ? [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ( ( X10 @ X12 )
!= $true )
& ( ( X10 @ X11 )
= $true )
& ( ( X0 @ X12 @ X11 )
= $true ) ) ) ),
inference(fool_elimination,[status(thm)],[f4]) ).
thf(f4,plain,
~ ! [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X1: $o > $o,X2: $o > $o] :
( ( X0 @ X1 @ X2 )
=> ( X0 @ X2 @ X1 ) )
=> ( ? [X3: ( $o > $o ) > $o,X4: $o > $o,X5: ( $o > $o ) > $o,X6: $o > $o,X7: ( $o > $o ) > $o,X8: $o > $o,X9: $o > $o] :
( ~ ( X5 @ X8 )
& ~ ( X0 @ X6 @ X4 )
& ~ ( X0 @ X6 @ X9 )
& ~ ( X0 @ X8 @ X9 )
& ~ ( X0 @ X8 @ X6 )
& ~ ( X3 @ X8 )
& ~ ( X5 @ X6 )
& ~ ( X3 @ X6 )
& ~ ( X0 @ X8 @ X4 )
& ~ ( X7 @ X9 )
& ( X3 @ X9 )
& ( X7 @ X6 )
& ~ ( X3 @ X4 )
& ~ ( X5 @ X9 )
& ~ ( X7 @ X8 )
& ( X5 @ X4 )
& ~ ( X0 @ X4 @ X9 )
& ~ ( X7 @ X4 ) )
| ? [X10: ( $o > $o ) > $o,X11: $o > $o,X12: $o > $o] :
( ~ ( X10 @ X12 )
& ( X10 @ X11 )
& ( X0 @ X12 @ X11 ) ) ) ),
inference(rectify,[status(thm)],[f2]) ).
thf(f2,negated_conjecture,
~ ! [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X1: $o > $o,X2: $o > $o] :
( ( X0 @ X1 @ X2 )
=> ( X0 @ X2 @ X1 ) )
=> ( ? [X5: ( $o > $o ) > $o,X4: $o > $o,X8: ( $o > $o ) > $o,X6: $o > $o,X9: ( $o > $o ) > $o,X7: $o > $o,X3: $o > $o] :
( ~ ( X8 @ X7 )
& ~ ( X0 @ X6 @ X4 )
& ~ ( X0 @ X6 @ X3 )
& ~ ( X0 @ X7 @ X3 )
& ~ ( X0 @ X7 @ X6 )
& ~ ( X5 @ X7 )
& ~ ( X8 @ X6 )
& ~ ( X5 @ X6 )
& ~ ( X0 @ X7 @ X4 )
& ~ ( X9 @ X3 )
& ( X5 @ X3 )
& ( X9 @ X6 )
& ~ ( X5 @ X4 )
& ~ ( X8 @ X3 )
& ~ ( X9 @ X7 )
& ( X8 @ X4 )
& ~ ( X0 @ X4 @ X3 )
& ~ ( X9 @ X4 ) )
| ? [X5: ( $o > $o ) > $o,X3: $o > $o,X4: $o > $o] :
( ~ ( X5 @ X4 )
& ( X5 @ X3 )
& ( X0 @ X4 @ X3 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
thf(f1,conjecture,
! [X0: ( $o > $o ) > ( $o > $o ) > $o] :
( ! [X1: $o > $o,X2: $o > $o] :
( ( X0 @ X1 @ X2 )
=> ( X0 @ X2 @ X1 ) )
=> ( ? [X5: ( $o > $o ) > $o,X4: $o > $o,X8: ( $o > $o ) > $o,X6: $o > $o,X9: ( $o > $o ) > $o,X7: $o > $o,X3: $o > $o] :
( ~ ( X8 @ X7 )
& ~ ( X0 @ X6 @ X4 )
& ~ ( X0 @ X6 @ X3 )
& ~ ( X0 @ X7 @ X3 )
& ~ ( X0 @ X7 @ X6 )
& ~ ( X5 @ X7 )
& ~ ( X8 @ X6 )
& ~ ( X5 @ X6 )
& ~ ( X0 @ X7 @ X4 )
& ~ ( X9 @ X3 )
& ( X5 @ X3 )
& ( X9 @ X6 )
& ~ ( X5 @ X4 )
& ~ ( X8 @ X3 )
& ~ ( X9 @ X7 )
& ( X8 @ X4 )
& ~ ( X0 @ X4 @ X3 )
& ~ ( X9 @ X4 ) )
| ? [X5: ( $o > $o ) > $o,X3: $o > $o,X4: $o > $o] :
( ~ ( X5 @ X4 )
& ( X5 @ X3 )
& ( X0 @ X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.MeJNLNMy44/DTF2THF_24996.p',ramsey_u_2_4_4) ).
thf(f49,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( X2 @ X1 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( X1 = X5 )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( X0 = X1 )
| ( ( X2 @ X5 )
= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X0 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( X1 = X4 )
| ( ( X3 @ X4 )
!= $true ) ),
inference(subsumption_resolution,[status(thm)],[f48,f12]) ).
thf(f48,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( X2 @ X5 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( X2 @ X4 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( X1 = X4 )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( X1 = X5 )
| ( X0 = X1 )
| ( ( X3 @ X0 )
= $true )
| ( ( X3 @ X1 )
= $true ) ),
inference(subsumption_resolution,[status(thm)],[f47,f16]) ).
thf(f47,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( X3 @ X5 )
= $true )
| ( X0 = X1 )
| ( X1 = X4 )
| ( X1 = X5 )
| ( ( X2 @ X4 )
= $true )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( ( X2 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( ( X3 @ X0 )
= $true ) ),
inference(subsumption_resolution,[status(thm)],[f46,f12]) ).
thf(f46,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( sK0 @ X5 @ X4 )
= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( X0 = X1 )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( X1 = X5 )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( ( X2 @ X5 )
= $true )
| ( ( X3 @ X0 )
= $true )
| ( X1 = X4 ) ),
inference(subsumption_resolution,[status(thm)],[f45,f12]) ).
thf(f45,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( X3 @ X5 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( ( sK0 @ X5 @ X0 )
= $true )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( X1 = X4 )
| ( ( X3 @ X4 )
!= $true )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( X2 @ X5 )
= $true )
| ( X0 = X1 )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( sK0 @ X5 @ X4 )
= $true )
| ( ( X3 @ X0 )
= $true )
| ( X1 = X5 ) ),
inference(subsumption_resolution,[status(thm)],[f27,f16]) ).
thf(f27,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( X1 = X5 )
| ( ( X3 @ X4 )
!= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( X3 @ X1 )
= $true )
| ( $true
= ( sK0 @ X5 @ X1 ) )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X3 @ X0 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( ( sK0 @ X5 @ X4 )
= $true )
| ( ( sK0 @ X5 @ X0 )
= $true )
| ( ( X2 @ X5 )
= $true )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( X0 = X1 )
| ( X1 = X4 ) ),
inference(equality_proxy_clausification,[status(thm)],[f26]) ).
thf(f26,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( sK0 @ X5 @ X0 )
= $true )
| ( ( X1 = X5 )
= $true )
| ( ( X2 @ X5 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( X1 = X4 )
| ( $true
= ( sK0 @ X5 @ X1 ) )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( X0 = X1 )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( ( X3 @ X0 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( sK0 @ X5 @ X4 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( $true
!= ( X2 @ X0 ) ) ),
inference(equality_proxy_clausification,[status(thm)],[f17]) ).
thf(f17,plain,
! [X2: ( $o > $o ) > $o,X3: ( $o > $o ) > $o,X0: $o > $o,X1: $o > $o,X4: $o > $o,X5: $o > $o] :
( ( ( X3 @ X1 )
= $true )
| ( $true
!= ( X2 @ X0 ) )
| ( ( sK0 @ X5 @ X4 )
= $true )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( sK0 @ X5 @ X0 )
= $true )
| ( ( X2 @ X1 )
= $true )
| ( ( X3 @ X4 )
!= $true )
| ( ( X3 @ X0 )
= $true )
| ( ( sK0 @ X4 @ X0 )
= $true )
| ( ( X2 @ X4 )
= $true )
| ( $true
= ( X1 = X4 ) )
| ( ( sK0 @ X1 @ X0 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X1 = X5 )
= $true )
| ( X0 = X1 )
| ( $true
= ( sK0 @ X5 @ X1 ) )
| ( ( X2 @ X5 )
= $true ) ),
inference(leibniz_equality_elimination,[status(thm)],[f14]) ).
thf(f14,plain,
! [X2: $o > $o,X3: ( $o > $o ) > $o,X1: $o > $o,X6: ( $o > $o ) > $o,X7: ( $o > $o ) > $o,X4: $o > $o,X5: $o > $o] :
( ( $true
!= ( X3 @ X2 ) )
| ( ( X7 @ X5 )
= $true )
| ( ( X6 @ X4 )
= $true )
| ( ( X3 @ X1 )
= $true )
| ( ( X3 @ X5 )
= $true )
| ( ( X6 @ X2 )
= $true )
| ( $true
= ( sK0 @ X1 @ X2 ) )
| ( ( X3 @ X4 )
= $true )
| ( ( sK0 @ X4 @ X2 )
= $true )
| ( $true
= ( X7 @ X2 ) )
| ( ( X7 @ X1 )
!= $true )
| ( ( X7 @ X4 )
= $true )
| ( ( sK0 @ X4 @ X1 )
= $true )
| ( ( X6 @ X5 )
!= $true )
| ( ( X6 @ X1 )
= $true )
| ( $true
= ( sK0 @ X5 @ X2 ) )
| ( ( sK0 @ X4 @ X5 )
= $true )
| ( ( sK0 @ X1 @ X5 )
= $true ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA028^1 : TPTP v9.2.1. Released v3.6.0.
% 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.34 % Computer : n021.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue Feb 24 07:25:23 EST 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.30/0.46 ---- Original DTF file ---
% 0.30/0.46 thf(spec,logic,$$dhol).
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 % File : GRA028^1 : TPTP v9.2.1. Released v3.6.0.
% 0.30/0.46 % Domain : Graph Theory
% 0.30/0.46 % Problem : R(2,4) <= 4
% 0.30/0.46 % Version : Especial.
% 0.30/0.46 % English :
% 0.30/0.46
% 0.30/0.46 % Refs : [Rad06] Radziszowski (2006), Small Ramsey Numbers
% 0.30/0.46 % : [Bro08] Brown (2008), Email to G. Sutcliffe
% 0.30/0.46 % Source : [Bro08]
% 0.30/0.46 % Names :
% 0.30/0.46
% 0.30/0.46 % Status : Theorem
% 0.30/0.46 % Rating : 0.58 v9.1.0, 0.50 v9.0.0, 0.58 v8.2.0, 0.64 v8.1.0, 0.67 v7.5.0, 0.75 v7.4.0, 0.78 v7.3.0, 0.70 v7.2.0, 0.75 v7.1.0, 0.86 v7.0.0, 0.75 v6.4.0, 0.86 v6.3.0, 0.83 v5.5.0, 0.80 v5.4.0, 1.00 v3.7.0
% 0.30/0.46 % Syntax : Number of formulae : 1 ( 0 unt; 0 typ; 0 def)
% 0.30/0.46 % Number of atoms : 0 ( 0 equ; 0 cnn)
% 0.30/0.46 % Maximal formula atoms : 0 ( 0 avg)
% 0.30/0.46 % Number of connectives : 70 ( 16 ~; 1 |; 19 &; 32 @)
% 0.30/0.46 % ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% 0.30/0.46 % Maximal formula depth : 31 ( 31 avg)
% 0.30/0.46 % Number of types : 1 ( 0 usr)
% 0.30/0.46 % Number of type conns : 20 ( 20 >; 0 *; 0 +; 0 <<)
% 0.30/0.46 % Number of symbols : 0 ( 0 usr; 0 con; --- aty)
% 0.30/0.46 % Number of variables : 13 ( 0 ^; 3 !; 10 ?; 13 :)
% 0.30/0.46 % SPC : TH0_THM_NEQ_NAR
% 0.30/0.46
% 0.30/0.46 % Comments : If a type alpha has exactly n elements, then we can prove
% 0.30/0.46 % R(k,l) > n by finding a graph (symmetric binary relation) on type
% 0.30/0.46 % alpha with no k-cliques and no l-independent sets. Likewise, we
% 0.30/0.46 % can prove R(k,l) <= n by proving every graph (symmetric binary
% 0.30/0.46 % relation) on alpha must have a k-clique or l-independent set.
% 0.30/0.46 % There is one type with 4 elements: o > o. There are two types
% 0.30/0.46 % with 16 elements: o > o > o and (o > o) > o. There are two types
% 0.30/0.46 % with 256 elements: o > o > o > o and o > (o > o) > o. This means
% 0.30/0.46 % we always have two formulations of R(k,l) >/<= 16 and two
% 0.30/0.46 % formulations of R(k,l) >/<= 256.
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 thf(ramsey_u_2_4_4,conjecture,
% 0.30/0.46 ! [G: ( $o > $o ) > ( $o > $o ) > $o] :
% 0.30/0.46 ( ! [Xx: $o > $o,Xy: $o > $o] :
% 0.30/0.46 ( ( G @ Xx @ Xy )
% 0.30/0.46 => ( G @ Xy @ Xx ) )
% 0.30/0.46 => ( ? [Xx0: $o > $o,Xx1: $o > $o,Xp0: ( $o > $o ) > $o] :
% 0.30/0.46 ( ( Xp0 @ Xx0 )
% 0.30/0.46 & ~ ( Xp0 @ Xx1 )
% 0.30/0.46 & ( G @ Xx1 @ Xx0 ) )
% 0.30/0.46 | ? [Xx0: $o > $o,Xx1: $o > $o,Xx2: $o > $o,Xx3: $o > $o,Xp0: ( $o > $o ) > $o,Xp1: ( $o > $o ) > $o,Xp2: ( $o > $o ) > $o] :
% 0.30/0.46 ( ( Xp0 @ Xx0 )
% 0.30/0.46 & ~ ( Xp0 @ Xx1 )
% 0.30/0.46 & ~ ( Xp0 @ Xx2 )
% 0.30/0.46 & ~ ( Xp0 @ Xx3 )
% 0.30/0.46 & ~ ( Xp1 @ Xx0 )
% 0.30/0.46 & ( Xp1 @ Xx1 )
% 0.30/0.46 & ~ ( Xp1 @ Xx2 )
% 0.30/0.46 & ~ ( Xp1 @ Xx3 )
% 0.30/0.46 & ~ ( Xp2 @ Xx0 )
% 0.30/0.46 & ~ ( Xp2 @ Xx1 )
% 0.30/0.46 & ( Xp2 @ Xx2 )
% 0.30/0.46 & ~ ( Xp2 @ Xx3 )
% 0.30/0.46 & ~ ( G @ Xx1 @ Xx0 )
% 0.30/0.46 & ~ ( G @ Xx2 @ Xx0 )
% 0.30/0.46 & ~ ( G @ Xx2 @ Xx1 )
% 0.30/0.46 & ~ ( G @ Xx3 @ Xx0 )
% 0.30/0.46 & ~ ( G @ Xx3 @ Xx1 )
% 0.30/0.46 & ~ ( G @ Xx3 @ Xx2 ) ) ) ) ).
% 0.30/0.46
% 0.30/0.46 %------------------------------------------------------------------------------
% 0.30/0.46 ------------------------
% 1.50/1.29 ---- Embedded in THF ---
% 1.50/1.29 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.50/1.29 %%% Generated on Tue Feb 24 07:25:24 EST 2026
% 1.50/1.29 %%% using '$$dhol' embedding, version 1.3.0.
% 1.50/1.29 %%% Logic specification used:
% 1.50/1.29 %%% thf(spec, logic, $$dhol).
% 1.50/1.29
% 1.50/1.29 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.MeJNLNMy44/DTF2DTF24996.p
% See solution above
% 1.50/1.29 ------------------------
% 1.68/1.31 ---- Cleaned THF ---
% 1.68/1.31 thf(ramsey_u_2_4_4,conjecture,
% 1.68/1.31 ! [G: ( $o > $o ) > ( $o > $o ) > $o] :
% 1.68/1.31 ( ! [Xx: $o > $o,Xy: $o > $o] :
% 1.68/1.31 ( ( G @ Xx @ Xy )
% 1.68/1.31 => ( G @ Xy @ Xx ) )
% 1.68/1.31 => ( ? [Xx0: $o > $o,Xx1: $o > $o,Xp0: ( $o > $o ) > $o] :
% 1.68/1.31 ( ( Xp0 @ Xx0 )
% 1.68/1.31 & ~ ( Xp0 @ Xx1 )
% 1.68/1.31 & ( G @ Xx1 @ Xx0 ) )
% 1.68/1.31 | ? [Xx0: $o > $o,Xx1: $o > $o,Xx2: $o > $o,Xx3: $o > $o,Xp0: ( $o > $o ) > $o,Xp1: ( $o > $o ) > $o,Xp2: ( $o > $o ) > $o] :
% 1.68/1.31 ( ( Xp0 @ Xx0 )
% 1.68/1.31 & ~ ( Xp0 @ Xx1 )
% 1.68/1.31 & ~ ( Xp0 @ Xx2 )
% 1.68/1.31 & ~ ( Xp0 @ Xx3 )
% 1.68/1.31 & ~ ( Xp1 @ Xx0 )
% 1.68/1.31 & ( Xp1 @ Xx1 )
% 1.68/1.31 & ~ ( Xp1 @ Xx2 )
% 1.68/1.31 & ~ ( Xp1 @ Xx3 )
% 1.68/1.31 & ~ ( Xp2 @ Xx0 )
% 1.68/1.31 & ~ ( Xp2 @ Xx1 )
% 1.68/1.31 & ( Xp2 @ Xx2 )
% 1.68/1.31 & ~ ( Xp2 @ Xx3 )
% 1.68/1.31 & ~ ( G @ Xx1 @ Xx0 )
% 1.68/1.31 & ~ ( G @ Xx2 @ Xx0 )
% 1.68/1.31 & ~ ( G @ Xx2 @ Xx1 )
% 1.68/1.31 & ~ ( G @ Xx3 @ Xx0 )
% 1.68/1.31 & ~ ( G @ Xx3 @ Xx1 )
% 1.68/1.31 & ~ ( G @ Xx3 @ Xx2 ) ) ) ) ).
% 1.68/1.31 ------------------------
% 1.68/1.32 % (25097)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_24996 for (2999ds/2Mi)
% 1.68/1.32 % (25097)Instruction limit reached!
% 1.68/1.32 % (25097)------------------------------
% 1.68/1.32 % (25097)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.32 % (25097)Termination reason: Unknown
% 1.68/1.32 % (25097)Termination phase: shuffling
% 1.68/1.32
% 1.68/1.32 % (25097)Memory used [KB]: 895
% 1.68/1.32 % (25097)Time elapsed: 0.002 s
% 1.68/1.32 % (25097)Instructions burned: 2 (million)
% 1.68/1.32 % (25097)------------------------------
% 1.68/1.32 % (25097)------------------------------
% 1.68/1.33 % (25098)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_24996 for (2999ds/275Mi)
% 1.68/1.33 % (25093)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/183Mi)
% 1.68/1.33 % (25094)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_24996 for (2999ds/4Mi)
% 1.68/1.33 % (25096)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/2Mi)
% 1.68/1.33 % (25095)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_24996 for (2999ds/27Mi)
% 1.68/1.33 % (25099)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/18Mi)
% 1.68/1.33 % (25096)Instruction limit reached!
% 1.68/1.33 % (25096)------------------------------
% 1.68/1.33 % (25096)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.33 % (25096)Termination reason: Unknown
% 1.68/1.33 % (25096)Termination phase: Preprocessing 3
% 1.68/1.33
% 1.68/1.33 % (25096)Memory used [KB]: 1023
% 1.68/1.33 % (25096)Time elapsed: 0.003 s
% 1.68/1.33 % (25096)Instructions burned: 2 (million)
% 1.68/1.33 % (25096)------------------------------
% 1.68/1.33 % (25096)------------------------------
% 1.68/1.33 % (25095)Refutation not found, incomplete strategy
% 1.68/1.33 % (25095)------------------------------
% 1.68/1.33 % (25095)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.33 % (25095)Termination reason: Refutation not found, incomplete strategy
% 1.68/1.33
% 1.68/1.33
% 1.68/1.33 % (25095)Memory used [KB]: 5500
% 1.68/1.33 % (25095)Time elapsed: 0.004 s
% 1.68/1.33 % (25095)Instructions burned: 3 (million)
% 1.68/1.33 % (25095)------------------------------
% 1.68/1.33 % (25095)------------------------------
% 1.68/1.33 % (25094)Instruction limit reached!
% 1.68/1.33 % (25094)------------------------------
% 1.68/1.33 % (25094)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.33 % (25094)Termination reason: Unknown
% 1.68/1.33 % (25094)Termination phase: Saturation
% 1.68/1.33
% 1.68/1.33 % (25094)Memory used [KB]: 5500
% 1.68/1.33 % (25094)Time elapsed: 0.005 s
% 1.68/1.33 % (25094)Instructions burned: 5 (million)
% 1.68/1.33 % (25094)------------------------------
% 1.68/1.33 % (25094)------------------------------
% 1.68/1.34 % (25100)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/3Mi)
% 1.68/1.34 % (25099)Instruction limit reached!
% 1.68/1.34 % (25099)------------------------------
% 1.68/1.34 % (25099)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.34 % (25099)Termination reason: Unknown
% 1.68/1.34 % (25099)Termination phase: Saturation
% 1.68/1.34
% 1.68/1.34 % (25099)Memory used [KB]: 5500
% 1.68/1.34 % (25099)Time elapsed: 0.012 s
% 1.68/1.34 % (25099)Instructions burned: 19 (million)
% 1.68/1.34 % (25099)------------------------------
% 1.68/1.34 % (25099)------------------------------
% 1.68/1.34 % (25100)Instruction limit reached!
% 1.68/1.34 % (25100)------------------------------
% 1.68/1.34 % (25100)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.34 % (25100)Termination reason: Unknown
% 1.68/1.34 % (25100)Termination phase: Saturation
% 1.68/1.34
% 1.68/1.34 % (25100)Memory used [KB]: 5500
% 1.68/1.34 % (25100)Time elapsed: 0.003 s
% 1.68/1.34 % (25100)Instructions burned: 4 (million)
% 1.68/1.34 % (25100)------------------------------
% 1.68/1.34 % (25100)------------------------------
% 1.68/1.35 % (25101)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_24996 for (2999ds/37Mi)
% 1.68/1.35 % (25102)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_24996 for (2999ds/15Mi)
% 1.68/1.35 % (25103)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_24996 for (2999ds/3Mi)
% 1.68/1.35 % (25105)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/7Mi)
% 1.68/1.35 % (25103)Instruction limit reached!
% 1.68/1.35 % (25103)------------------------------
% 1.68/1.35 % (25103)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (25103)Termination reason: Unknown
% 1.68/1.35 % (25103)Termination phase: Saturation
% 1.68/1.35
% 1.68/1.35 % (25103)Memory used [KB]: 5500
% 1.68/1.35 % (25103)Time elapsed: 0.004 s
% 1.68/1.35 % (25103)Instructions burned: 3 (million)
% 1.68/1.35 % (25103)------------------------------
% 1.68/1.35 % (25103)------------------------------
% 1.68/1.35 % (25105)Instruction limit reached!
% 1.68/1.35 % (25105)------------------------------
% 1.68/1.35 % (25105)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.35 % (25105)Termination reason: Unknown
% 1.68/1.35 % (25105)Termination phase: Saturation
% 1.68/1.35
% 1.68/1.35 % (25105)Memory used [KB]: 1023
% 1.68/1.35 % (25105)Time elapsed: 0.005 s
% 1.68/1.35 % (25105)Instructions burned: 8 (million)
% 1.68/1.35 % (25105)------------------------------
% 1.68/1.35 % (25105)------------------------------
% 1.68/1.35 % (25104)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_24996 for (2999ds/1041Mi)
% 1.68/1.36 % (25102)Instruction limit reached!
% 1.68/1.36 % (25102)------------------------------
% 1.68/1.36 % (25102)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.36 % (25102)Termination reason: Unknown
% 1.68/1.36 % (25102)Termination phase: Saturation
% 1.68/1.36
% 1.68/1.36 % (25102)Memory used [KB]: 5500
% 1.68/1.36 % (25102)Time elapsed: 0.011 s
% 1.68/1.36 % (25102)Instructions burned: 16 (million)
% 1.68/1.36 % (25102)------------------------------
% 1.68/1.36 % (25102)------------------------------
% 1.68/1.36 % (25101)Instruction limit reached!
% 1.68/1.36 % (25101)------------------------------
% 1.68/1.36 % (25101)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.36 % (25101)Termination reason: Unknown
% 1.68/1.36 % (25101)Termination phase: Saturation
% 1.68/1.36
% 1.68/1.36 % (25101)Memory used [KB]: 5628
% 1.68/1.36 % (25101)Time elapsed: 0.017 s
% 1.68/1.36 % (25101)Instructions burned: 38 (million)
% 1.68/1.36 % (25101)------------------------------
% 1.68/1.36 % (25101)------------------------------
% 1.68/1.36 % (25107)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_24996 for (2999ds/3Mi)
% 1.68/1.36 % (25107)Instruction limit reached!
% 1.68/1.36 % (25107)------------------------------
% 1.68/1.36 % (25107)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.36 % (25107)Termination reason: Unknown
% 1.68/1.36 % (25107)Termination phase: Saturation
% 1.68/1.36
% 1.68/1.36 % (25107)Memory used [KB]: 5500
% 1.68/1.36 % (25107)Time elapsed: 0.003 s
% 1.68/1.36 % (25107)Instructions burned: 4 (million)
% 1.68/1.36 % (25107)------------------------------
% 1.68/1.36 % (25107)------------------------------
% 1.68/1.37 % (25106)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/16Mi)
% 1.68/1.37 % (25109)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/7Mi)
% 1.68/1.37 % (25109)Instruction limit reached!
% 1.68/1.37 % (25109)------------------------------
% 1.68/1.37 % (25109)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.37 % (25109)Termination reason: Unknown
% 1.68/1.37 % (25109)Termination phase: Saturation
% 1.68/1.37
% 1.68/1.37 % (25109)Memory used [KB]: 5500
% 1.68/1.37 % (25109)Time elapsed: 0.005 s
% 1.68/1.37 % (25109)Instructions burned: 9 (million)
% 1.68/1.37 % (25109)------------------------------
% 1.68/1.37 % (25109)------------------------------
% 1.68/1.37 % (25110)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/3Mi)
% 1.68/1.38 % (25108)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_24996 for (2999ds/3Mi)
% 1.68/1.38 % (25110)Instruction limit reached!
% 1.68/1.38 % (25110)------------------------------
% 1.68/1.38 % (25110)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (25110)Termination reason: Unknown
% 1.68/1.38 % (25110)Termination phase: Saturation
% 1.68/1.38
% 1.68/1.38 % (25110)Memory used [KB]: 5500
% 1.68/1.38 % (25110)Time elapsed: 0.003 s
% 1.68/1.38 % (25110)Instructions burned: 4 (million)
% 1.68/1.38 % (25110)------------------------------
% 1.68/1.38 % (25110)------------------------------
% 1.68/1.38 % (25108)Instruction limit reached!
% 1.68/1.38 % (25108)------------------------------
% 1.68/1.38 % (25108)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (25108)Termination reason: Unknown
% 1.68/1.38 % (25108)Termination phase: Property scanning
% 1.68/1.38
% 1.68/1.38 % (25108)Memory used [KB]: 1023
% 1.68/1.38 % (25108)Time elapsed: 0.003 s
% 1.68/1.38 % (25108)Instructions burned: 3 (million)
% 1.68/1.38 % (25108)------------------------------
% 1.68/1.38 % (25108)------------------------------
% 1.68/1.38 % (25106)Instruction limit reached!
% 1.68/1.38 % (25106)------------------------------
% 1.68/1.38 % (25106)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (25106)Termination reason: Unknown
% 1.68/1.38 % (25106)Termination phase: Saturation
% 1.68/1.38
% 1.68/1.38 % (25106)Memory used [KB]: 5500
% 1.68/1.38 % (25106)Time elapsed: 0.011 s
% 1.68/1.38 % (25106)Instructions burned: 16 (million)
% 1.68/1.38 % (25106)------------------------------
% 1.68/1.38 % (25106)------------------------------
% 1.68/1.38 % (25111)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/4Mi)
% 1.68/1.39 % (25112)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/18Mi)
% 1.68/1.39 % (25111)Instruction limit reached!
% 1.68/1.39 % (25111)------------------------------
% 1.68/1.39 % (25111)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.39 % (25111)Termination reason: Unknown
% 1.68/1.39 % (25111)Termination phase: Saturation
% 1.68/1.39
% 1.68/1.39 % (25111)Memory used [KB]: 5500
% 1.68/1.39 % (25111)Time elapsed: 0.004 s
% 1.68/1.39 % (25111)Instructions burned: 6 (million)
% 1.68/1.39 % (25111)------------------------------
% 1.68/1.39 % (25111)------------------------------
% 1.68/1.39 % (25112)Instruction limit reached!
% 1.68/1.39 % (25112)------------------------------
% 1.68/1.39 % (25112)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.39 % (25112)Termination reason: Unknown
% 1.68/1.39 % (25112)Termination phase: Saturation
% 1.68/1.39
% 1.68/1.39 % (25112)Memory used [KB]: 5500
% 1.68/1.39 % (25112)Time elapsed: 0.007 s
% 1.68/1.39 % (25112)Instructions burned: 18 (million)
% 1.68/1.39 % (25112)------------------------------
% 1.68/1.39 % (25112)------------------------------
% 1.68/1.39 % (25113)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/710Mi)
% 1.68/1.39 % (25114)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/6Mi)
% 1.70/1.40 % (25115)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_24996 for (2999ds/902Mi)
% 1.70/1.40 % (25114)Instruction limit reached!
% 1.70/1.40 % (25114)------------------------------
% 1.70/1.40 % (25114)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.40 % (25114)Termination reason: Unknown
% 1.70/1.40 % (25114)Termination phase: Saturation
% 1.70/1.40
% 1.70/1.40 % (25114)Memory used [KB]: 5500
% 1.70/1.40 % (25114)Time elapsed: 0.005 s
% 1.70/1.40 % (25114)Instructions burned: 6 (million)
% 1.70/1.40 % (25114)------------------------------
% 1.70/1.40 % (25114)------------------------------
% 1.70/1.40 % (25116)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_24996 for (2999ds/21Mi)
% 1.70/1.41 % (25116)Instruction limit reached!
% 1.70/1.41 % (25116)------------------------------
% 1.70/1.41 % (25116)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.41 % (25116)Termination reason: Unknown
% 1.70/1.41 % (25116)Termination phase: Saturation
% 1.70/1.41
% 1.70/1.41 % (25116)Memory used [KB]: 5628
% 1.70/1.41 % (25116)Time elapsed: 0.010 s
% 1.70/1.41 % (25116)Instructions burned: 22 (million)
% 1.70/1.41 % (25116)------------------------------
% 1.70/1.41 % (25116)------------------------------
% 1.70/1.41 % (25117)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/5Mi)
% 1.70/1.41 % (25117)Instruction limit reached!
% 1.70/1.41 % (25117)------------------------------
% 1.70/1.41 % (25117)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.41 % (25117)Termination reason: Unknown
% 1.70/1.41 % (25117)Termination phase: Saturation
% 1.70/1.41
% 1.70/1.41 % (25117)Memory used [KB]: 5500
% 1.70/1.41 % (25117)Time elapsed: 0.004 s
% 1.70/1.41 % (25117)Instructions burned: 6 (million)
% 1.70/1.41 % (25117)------------------------------
% 1.70/1.41 % (25117)------------------------------
% 1.70/1.42 % (25118)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_24996 for (2999ds/6Mi)
% 1.70/1.42 % (25093)Instruction limit reached!
% 1.70/1.42 % (25093)------------------------------
% 1.70/1.42 % (25093)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.42 % (25093)Termination reason: Unknown
% 1.70/1.42 % (25093)Termination phase: Saturation
% 1.70/1.42
% 1.70/1.42 % (25093)Memory used [KB]: 5756
% 1.70/1.42 % (25093)Time elapsed: 0.095 s
% 1.70/1.42 % (25093)Instructions burned: 184 (million)
% 1.70/1.42 % (25093)------------------------------
% 1.70/1.42 % (25093)------------------------------
% 1.70/1.42 % (25118)Instruction limit reached!
% 1.70/1.42 % (25118)------------------------------
% 1.70/1.42 % (25118)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.42 % (25118)Termination reason: Unknown
% 1.70/1.42 % (25118)Termination phase: Saturation
% 1.70/1.42
% 1.70/1.42 % (25118)Memory used [KB]: 5500
% 1.70/1.42 % (25118)Time elapsed: 0.004 s
% 1.70/1.42 % (25118)Instructions burned: 8 (million)
% 1.70/1.42 % (25118)------------------------------
% 1.70/1.42 % (25118)------------------------------
% 1.70/1.43 % (25119)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_24996 for (2999ds/377Mi)
% 1.70/1.43 % (25098)Instruction limit reached!
% 1.70/1.43 % (25098)------------------------------
% 1.70/1.43 % (25098)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.43 % (25098)Termination reason: Unknown
% 1.70/1.43 % (25098)Termination phase: Saturation
% 1.70/1.43
% 1.70/1.43 % (25098)Memory used [KB]: 5756
% 1.70/1.43 % (25098)Time elapsed: 0.105 s
% 1.70/1.43 % (25098)Instructions burned: 277 (million)
% 1.70/1.43 % (25098)------------------------------
% 1.70/1.43 % (25098)------------------------------
% 1.70/1.43 % (25121)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_24996 for (2999ds/19Mi)
% 1.70/1.43 % (25120)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_24996 for (2999ds/779Mi)
% 1.70/1.44 % (25121)Instruction limit reached!
% 1.70/1.44 % (25121)------------------------------
% 1.70/1.44 % (25121)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.44 % (25121)Termination reason: Unknown
% 1.70/1.44 % (25121)Termination phase: Saturation
% 1.70/1.44
% 1.70/1.44 % (25121)Memory used [KB]: 5628
% 1.70/1.44 % (25121)Time elapsed: 0.008 s
% 1.70/1.44 % (25121)Instructions burned: 21 (million)
% 1.70/1.44 % (25121)------------------------------
% 1.70/1.44 % (25121)------------------------------
% 1.70/1.44 % (25122)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_24996 for (2998ds/879Mi)
% 1.70/1.45 % (25123)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_24996 for (2998ds/17Mi)
% 1.70/1.45 % (25123)Instruction limit reached!
% 1.70/1.45 % (25123)------------------------------
% 1.70/1.45 % (25123)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.45 % (25123)Termination reason: Unknown
% 1.70/1.45 % (25123)Termination phase: Saturation
% 1.70/1.46
% 1.70/1.46 % (25123)Memory used [KB]: 5628
% 1.70/1.46 % (25123)Time elapsed: 0.008 s
% 1.70/1.46 % (25123)Instructions burned: 18 (million)
% 1.70/1.46 % (25123)------------------------------
% 1.70/1.46 % (25123)------------------------------
% 1.70/1.47 % (25124)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_24996 for (2998ds/3Mi)
% 1.70/1.47 % (25124)Instruction limit reached!
% 1.70/1.47 % (25124)------------------------------
% 1.70/1.47 % (25124)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.47 % (25124)Termination reason: Unknown
% 1.70/1.47 % (25124)Termination phase: Saturation
% 1.70/1.47
% 1.70/1.47 % (25124)Memory used [KB]: 1023
% 1.70/1.47 % (25124)Time elapsed: 0.003 s
% 1.70/1.47 % (25124)Instructions burned: 3 (million)
% 1.70/1.47 % (25124)------------------------------
% 1.70/1.47 % (25124)------------------------------
% 1.70/1.48 % (25125)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_24996 for (2998ds/30Mi)
% 1.70/1.49 % (25125)Instruction limit reached!
% 1.70/1.49 % (25125)------------------------------
% 1.70/1.49 % (25125)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.49 % (25125)Termination reason: Unknown
% 1.70/1.49 % (25125)Termination phase: Saturation
% 1.70/1.49
% 1.70/1.49 % (25125)Memory used [KB]: 5628
% 1.70/1.49 % (25125)Time elapsed: 0.012 s
% 1.70/1.49 % (25125)Instructions burned: 31 (million)
% 1.70/1.49 % (25125)------------------------------
% 1.70/1.49 % (25125)------------------------------
% 1.70/1.50 % (25126)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_24996 for (2998ds/127Mi)
% 1.70/1.52 % (25122)First to succeed.
% 1.70/1.53 % (25122)Refutation found. Thanks to Tanya!
% 1.70/1.53 % SZS status Theorem for DTF2THF_24996
% 1.70/1.53 % SZS output start Proof for DTF2THF_24996
% 1.70/1.53 thf(func_def_3, type, sK0: ($o > $o) > ($o > $o) > $o).
% 1.70/1.53 thf(func_def_9, type, ph2: !>[X0: $tType]:(X0)).
% 1.70/1.53 thf(func_def_10, type, sK3: $o > $o).
% 1.70/1.53 thf(f779,plain,(
% 1.70/1.53 $false),
% 1.70/1.53 inference(avatar_sat_refutation,[status(thm)],[f379,f445,f482,f690,f778])).
% 1.70/1.53 thf(f778,plain,(
% 1.70/1.53 ~spl1_1),
% 1.70/1.53 inference(avatar_contradiction_clause,[status(thm)],[f777])).
% 1.70/1.53 thf(f777,plain,(
% 1.70/1.53 $false | ~spl1_1),
% 1.70/1.53 inference(equality_resolution,[status(thm)],[f719])).
% 1.70/1.53 thf(f719,plain,(
% 1.70/1.53 ( ! [X0 : $o] : (($false != X0)) ) | ~spl1_1),
% 1.70/1.53 inference(superposition,[status(thm)],[f3,f290])).
% 1.70/1.53 thf(f290,plain,(
% 1.70/1.53 ( ! [X4 : $o] : (($true = X4)) ) | ~spl1_1),
% 1.70/1.53 inference(avatar_component_clause,[status(thm)],[f289])).
% 1.70/1.53 thf(f289,definition,(
% 1.70/1.53 spl1_1 <=> ! [X4 : $o] : ($true = X4)),
% 1.70/1.53 introduced(definition,[new_symbols(naming,[spl1_1])],[avatar_definition])).
% 1.70/1.53 thf(f3,plain,(
% 1.70/1.53 ($false != $true)),
% 1.70/1.53 introduced(definition,[],[fool_axiom])).
% 1.70/1.53 thf(f690,plain,(
% 1.70/1.53 spl1_1 | spl1_3 | spl1_3 | ~spl1_10),
% 1.70/1.53 inference(avatar_split_clause,[status(thm)],[f664,f480,f366,f366,f289])).
% 1.70/1.53 thf(f366,definition,(
% 1.70/1.53 spl1_3 <=> ! [X1 : $o] : ($false = X1)),
% 1.70/1.53 introduced(definition,[new_symbols(naming,[spl1_3])],[avatar_definition])).
% 1.70/1.53 thf(f480,definition,(
% 1.70/1.53 spl1_10 <=> ! [X2 : $o > $o,X4 : $o,X3 : $o] : (((X2 @ X3) = $true) | ((^[Y0 : $o]: ($false)) = X2) | ($false = X4) | ((X2 @ X4) = $true))),
% 1.70/1.53 introduced(definition,[new_symbols(naming,[spl1_10])],[avatar_definition])).
% 1.70/1.53 thf(f664,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : (($false = X2) | ($false = X0) | ($true = X1)) ) | ~spl1_10),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f662])).
% 1.70/1.53 thf(f662,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : (($true = X1) | ($true = X1) | ($false = X0) | ($false = X2)) ) | ~spl1_10),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f661])).
% 1.70/1.53 thf(f661,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : (($true = X1) | (X1 = X2) | ($false = X0)) ) | ~spl1_10),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f660])).
% 1.70/1.53 thf(f660,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : (($true = X1) | ((X1 = X2) = $true) | ($false = X0)) ) | ~spl1_10),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f659])).
% 1.70/1.53 thf(f659,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : (($true = X1) | ($false = X0) | ((X1 = X2) = $true) | ($false = X0)) ) | ~spl1_10),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f638])).
% 1.70/1.53 thf(f638,plain,(
% 1.70/1.53 ( ! [X2 : $o,X0 : $o,X1 : $o] : ((X0 = X1) | ((X1 = X2) = $true) | ($false = X0)) ) | ~spl1_10),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f620])).
% 1.70/1.53 thf(f620,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X4 : $o,X5 : $o] : (($false = (X2 @ X5)) | ($false = X4) | ((X2 @ X4) = $true) | ((X2 @ X3) = $true)) ) | ~spl1_10),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f616])).
% 1.70/1.53 thf(f616,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X4 : $o,X5 : $o] : (($false = X4) | ((X2 @ X4) = $true) | ((X2 @ X5) = ((^[Y0 : $o]: ($false)) @ X5)) | ((X2 @ X3) = $true)) ) | ~spl1_10),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f481])).
% 1.70/1.53 thf(f481,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X4 : $o] : (((^[Y0 : $o]: ($false)) = X2) | ((X2 @ X3) = $true) | ((X2 @ X4) = $true) | ($false = X4)) ) | ~spl1_10),
% 1.70/1.53 inference(avatar_component_clause,[status(thm)],[f480])).
% 1.70/1.53 thf(f482,plain,(
% 1.70/1.53 spl1_10 | spl1_3 | ~spl1_6),
% 1.70/1.53 inference(avatar_split_clause,[status(thm)],[f471,f377,f366,f480])).
% 1.70/1.53 thf(f377,definition,(
% 1.70/1.53 spl1_6 <=> ! [X2 : $o > $o,X1 : $o,X3 : $o] : (((= @ X1) = X2) | ((X2 @ X3) = $true) | ((^[Y0 : $o]: ($false)) = X2) | ($false = X1))),
% 1.70/1.53 introduced(definition,[new_symbols(naming,[spl1_6])],[avatar_definition])).
% 1.70/1.53 thf(f471,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o,X4 : $o] : (((X2 @ X3) = $true) | ((X2 @ X4) = $true) | ($false = X4) | ($false = X1) | ((^[Y0 : $o]: ($false)) = X2)) ) | ~spl1_6),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f470])).
% 1.70/1.53 thf(f470,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o,X4 : $o] : (((X2 @ X3) = $true) | ((^[Y0 : $o]: ($false)) = X2) | ($false = X4) | ($false = X1) | ($false = X1) | ((X2 @ X4) = $true)) ) | ~spl1_6),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f468])).
% 1.70/1.53 thf(f468,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o,X4 : $o] : (($false = X1) | ((X2 @ X4) = $true) | ((^[Y0 : $o]: ($false)) = X2) | ((X2 @ X3) = $true) | (X1 != X4)) ) | ~spl1_6),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f462])).
% 1.70/1.53 thf(f462,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o,X4 : $o] : (($false = X1) | ($false = (X1 = X4)) | ((X2 @ X4) = $true) | ((^[Y0 : $o]: ($false)) = X2) | ((X2 @ X3) = $true)) ) | ~spl1_6),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f456])).
% 1.70/1.53 thf(f456,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o,X4 : $o] : (((^[Y0 : $o]: ($false)) = X2) | ($false = X1) | ((X2 @ X4) = (X1 = X4)) | ((X2 @ X3) = $true)) ) | ~spl1_6),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f378])).
% 1.70/1.53 thf(f378,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X1 : $o] : (((= @ X1) = X2) | ((^[Y0 : $o]: ($false)) = X2) | ((X2 @ X3) = $true) | ($false = X1)) ) | ~spl1_6),
% 1.70/1.53 inference(avatar_component_clause,[status(thm)],[f377])).
% 1.70/1.53 thf(f445,plain,(
% 1.70/1.53 ~spl1_3),
% 1.70/1.53 inference(avatar_contradiction_clause,[status(thm)],[f444])).
% 1.70/1.53 thf(f444,plain,(
% 1.70/1.53 $false | ~spl1_3),
% 1.70/1.53 inference(trivial_inequality_removal,[status(thm)],[f443])).
% 1.70/1.53 thf(f443,plain,(
% 1.70/1.53 ($false != $false) | ~spl1_3),
% 1.70/1.53 inference(superposition,[status(thm)],[f3,f367])).
% 1.70/1.53 thf(f367,plain,(
% 1.70/1.53 ( ! [X1 : $o] : (($false = X1)) ) | ~spl1_3),
% 1.70/1.53 inference(avatar_component_clause,[status(thm)],[f366])).
% 1.70/1.53 thf(f379,plain,(
% 1.70/1.53 spl1_1 | spl1_6),
% 1.70/1.53 inference(avatar_split_clause,[status(thm)],[f360,f377,f289])).
% 1.70/1.53 thf(f360,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X0 : $o,X1 : $o] : (((= @ X1) = X2) | ($true = X0) | ($false = X1) | ((^[Y0 : $o]: ($false)) = X2) | ((X2 @ X3) = $true)) )),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f348])).
% 1.70/1.53 thf(f348,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o,X0 : $o,X1 : $o] : ((X0 = X1) | ((^[Y0 : $o]: ($false)) = X2) | ((= @ X1) = X2) | ((X2 @ X3) = $true)) )),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f325])).
% 1.70/1.53 thf(f325,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o,X6 : $o,X7 : $o,X5 : $o] : (((^[Y0 : $o]: ($false)) = X0) | ((X0 @ X6) = $true) | ((X1 @ X5) = $true) | ($false = (X1 @ X7)) | (X0 = X1)) )),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f317])).
% 1.70/1.53 thf(f317,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o,X6 : $o,X7 : $o,X5 : $o] : (((^[Y0 : $o]: ($false)) = X0) | (X0 = X1) | ((X1 @ X5) = $true) | ((X0 @ X6) = $true) | ((X1 @ X7) = ((^[Y0 : $o]: ($false)) @ X7))) )),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f285])).
% 1.70/1.53 thf(f285,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o,X6 : $o,X5 : $o] : (((^[Y0 : $o]: ($false)) = X1) | ((X1 @ X5) = $true) | ((X0 @ X6) = $true) | (X0 = X1) | ((^[Y0 : $o]: ($false)) = X0)) )),
% 1.70/1.53 inference(trivial_inequality_removal,[status(thm)],[f284])).
% 1.70/1.53 thf(f284,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o,X6 : $o,X5 : $o] : (((X0 @ X6) = $true) | (X0 = X1) | ((X1 @ X5) = $true) | ((^[Y0 : $o]: ($false)) = X0) | ($false = $true) | ((^[Y0 : $o]: ($false)) = X1)) )),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f272])).
% 1.70/1.53 thf(f272,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o,X6 : $o,X4 : $o,X5 : $o] : ((((^[Y0 : $o]: ($false)) @ X4) = $true) | ((X1 @ X5) = $true) | ((X0 @ X6) = $true) | ((^[Y0 : $o]: ($false)) = X0) | (X0 = X1) | ((^[Y0 : $o]: ($false)) = X1)) )),
% 1.70/1.53 inference(primitive_instantiation,[status(thm)],[f241])).
% 1.70/1.53 thf(f241,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X6 : $o,X4 : $o,X5 : $o] : (((X2 @ X4) = $true) | (X0 = X1) | (X1 = X2) | ((X0 @ X6) = $true) | (X0 = X2) | ((X1 @ X5) = $true)) )),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f227])).
% 1.70/1.53 thf(f227,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X6 : $o,X4 : $o,X5 : $o] : (((X2 @ X4) = $true) | (X0 = X2) | (X1 = X2) | (X0 = X1) | (((^[Y0 : $o]: ($true)) @ X6) = (X0 @ X6)) | ((X1 @ X5) = $true)) )),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f210])).
% 1.70/1.53 thf(f210,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o,X5 : $o] : (((^[Y0 : $o]: ($true)) = X0) | (X1 = X2) | (X0 = X1) | (X0 = X2) | ((X1 @ X5) = $true) | ((X2 @ X4) = $true)) )),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f191])).
% 1.70/1.53 thf(f191,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o,X5 : $o] : (((^[Y0 : $o]: ($true)) = X0) | (X0 = X2) | (X0 = X1) | ((X2 @ X4) = $true) | (X1 = X2) | (((^[Y0 : $o]: ($true)) @ X5) = (X1 @ X5))) )),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f167])).
% 1.70/1.53 thf(f167,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o] : (((^[Y0 : $o]: ($true)) = X1) | (X1 = X2) | (X0 = X2) | (X0 = X1) | ((^[Y0 : $o]: ($true)) = X0) | ((X2 @ X4) = $true)) )),
% 1.70/1.53 inference(trivial_inequality_removal,[status(thm)],[f166])).
% 1.70/1.53 thf(f166,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o] : (((^[Y0 : $o]: ($true)) = X1) | ((^[Y0 : $o]: ($true)) = X0) | (X1 = X2) | (X0 = X2) | ((X2 @ X4) = $true) | ($false = $true) | (X0 = X1)) )),
% 1.70/1.53 inference(beta_eta_normalization,[status(thm)],[f160])).
% 1.70/1.53 thf(f160,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o] : (((^[Y0 : $o]: ($true)) = X0) | (X0 = X1) | ((X2 @ X4) = $true) | (X0 = X2) | (X1 = X2) | ($false = ((^[Y0 : $o]: ($true)) @ X4)) | ((^[Y0 : $o]: ($true)) = X1)) )),
% 1.70/1.53 inference(primitive_instantiation,[status(thm)],[f129])).
% 1.70/1.53 thf(f129,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o] : (($false = (X3 @ X4)) | ((X2 @ X4) = $true) | (X0 = X1) | (X0 = X3) | (X1 = X2) | (X1 = X3) | (X0 = X2)) )),
% 1.70/1.53 inference(binary_proxy_clausification,[status(thm)],[f115])).
% 1.70/1.53 thf(f115,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o] : (((X2 @ X4) = (X3 @ X4)) | (X0 = X1) | (X0 = X3) | (X0 = X2) | (X1 = X2) | (X1 = X3)) )),
% 1.70/1.53 inference(argument_congruence,[status(thm)],[f88])).
% 1.70/1.53 thf(f88,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o] : ((X2 = X3) | (X0 = X1) | (X0 = X2) | (X0 = X3) | (X1 = X2) | (X1 = X3)) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f87])).
% 1.70/1.53 thf(f87,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o] : ((X0 = X2) | (X1 = X2) | (X0 = X3) | (X2 = X3) | (X0 = X1) | ($true = (X1 = X3))) )),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f86])).
% 1.70/1.53 thf(f86,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o] : ((X0 = X1) | (X1 = X2) | (X1 = X2) | (X2 = X3) | ($true = (X1 = X3)) | (X0 = X2) | (X0 = X3)) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f85])).
% 1.70/1.53 thf(f85,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o] : ((X0 = X3) | ((X1 = X2) = $true) | (X0 = X1) | (X0 = X2) | (X2 = X3) | ($true = (X1 = X3)) | (X1 = X2)) )),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f71])).
% 1.70/1.53 thf(f71,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : $o > $o,X0 : $o > $o,X1 : $o > $o] : (((X1 = X2) = $true) | (X0 = X1) | (X0 = X3) | ($true = (X1 = X3)) | (X0 = X2) | (X1 = X2) | (X2 = X3) | (X0 = X1)) )),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f68])).
% 1.70/1.53 thf(f68,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o] : (((X3 @ X1) != $true) | (X0 = X4) | (X0 = X2) | ($true = (X3 @ X2)) | (X0 = X1) | ((X3 @ X4) = $true) | (X2 = X4) | ((X3 @ X0) = $true) | (X1 = X2)) )),
% 1.70/1.53 inference(duplicate_literal_removal,[status(thm)],[f67])).
% 1.70/1.53 thf(f67,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o] : ((X1 = X2) | ((X3 @ X0) = $true) | (X0 = X2) | (X0 = X4) | ((X3 @ X1) != $true) | ((X3 @ X4) = $true) | (X0 = X1) | ($true = (X3 @ X2)) | (X0 = X2) | (X2 = X4)) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f66])).
% 1.70/1.53 thf(f66,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o] : ((X0 = X4) | ($true = (X0 = X2)) | ((X3 @ X1) != $true) | (X2 = X4) | ($true = (X3 @ X2)) | ((X3 @ X0) = $true) | ((X3 @ X4) = $true) | (X0 = X1) | (X0 = X2) | (X1 = X2)) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f51])).
% 1.70/1.53 thf(f51,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o] : (($true = (X3 @ X2)) | (X1 = X2) | (X0 = X2) | ((X3 @ X0) = $true) | ((X0 = X4) = $true) | ((X3 @ X4) = $true) | ((X3 @ X1) != $true) | (X2 = X4) | (X0 = X1) | ($true = (X0 = X2))) )),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f50])).
% 1.70/1.53 thf(f50,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (($true != (X2 @ X0)) | (X1 = X5) | ((X2 @ X4) = $true) | ((X3 @ X1) = $true) | ((X3 @ X4) != $true) | ((X3 @ X0) = $true) | ((X2 @ X5) = $true) | ((X3 @ X5) = $true) | ((X2 @ X1) = $true) | (X0 = X1) | (X1 = X4)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f49,f16])).
% 1.70/1.53 thf(f16,plain,(
% 1.70/1.53 ( ! [X0 : $o > $o,X1 : $o > $o] : (((sK0 @ X1 @ X0) != $true) | (X0 = X1)) )),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f12])).
% 1.70/1.53 thf(f12,plain,(
% 1.70/1.53 ( ! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((sK0 @ X12 @ X11) != $true) | ((X10 @ X12) = $true) | ((X10 @ X11) != $true)) )),
% 1.70/1.53 inference(cnf_transformation,[status(thm)],[f11])).
% 1.70/1.53 thf(f11,plain,(
% 1.70/1.53 ! [X1 : $o > $o,X2 : $o > $o,X3 : ($o > $o) > $o,X4 : $o > $o,X5 : $o > $o,X6 : ($o > $o) > $o,X7 : ($o > $o) > $o] : (((X7 @ X4) = $true) | ($true = (sK0 @ X1 @ X2)) | ((sK0 @ X4 @ X1) = $true) | ((X6 @ X5) != $true) | ($true != (X3 @ X2)) | ((sK0 @ X4 @ X5) = $true) | ((X3 @ X4) = $true) | ((X6 @ X2) = $true) | ((X7 @ X1) != $true) | ((X6 @ X1) = $true) | ((sK0 @ X1 @ X5) = $true) | ($true = (sK0 @ X5 @ X2)) | ((X3 @ X5) = $true) | ((X3 @ X1) = $true) | ((X7 @ X5) = $true) | ((sK0 @ X4 @ X2) = $true) | ((X6 @ X4) = $true) | ($true = (X7 @ X2))) & ! [X8 : $o > $o,X9 : $o > $o] : (((sK0 @ X8 @ X9) = $true) | ((sK0 @ X9 @ X8) != $true)) & ! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((sK0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true))),
% 1.70/1.53 inference(skolemisation,[status(esa),new_symbols(skolem,[sK0])],[f9,f10])).
% 1.70/1.53 thf(f10,plain,(
% 1.70/1.53 ? [X0 : ($o > $o) > ($o > $o) > $o] : (! [X1 : $o > $o,X2 : $o > $o,X3 : ($o > $o) > $o,X4 : $o > $o,X5 : $o > $o,X6 : ($o > $o) > $o,X7 : ($o > $o) > $o] : (((X7 @ X4) = $true) | ((X0 @ X1 @ X2) = $true) | ((X0 @ X4 @ X1) = $true) | ((X6 @ X5) != $true) | ($true != (X3 @ X2)) | ((X0 @ X4 @ X5) = $true) | ((X3 @ X4) = $true) | ((X6 @ X2) = $true) | ((X7 @ X1) != $true) | ((X6 @ X1) = $true) | ((X0 @ X1 @ X5) = $true) | ((X0 @ X5 @ X2) = $true) | ((X3 @ X5) = $true) | ((X3 @ X1) = $true) | ((X7 @ X5) = $true) | ((X0 @ X4 @ X2) = $true) | ((X6 @ X4) = $true) | ($true = (X7 @ X2))) & ! [X8 : $o > $o,X9 : $o > $o] : (((X0 @ X8 @ X9) = $true) | ($true != (X0 @ X9 @ X8))) & ! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((X0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true))) => (! [X7 : ($o > $o) > $o,X6 : ($o > $o) > $o,X5 : $o > $o,X4 : $o > $o,X3 : ($o > $o) > $o,X2 : $o > $o,X1 : $o > $o] : (((X7 @ X4) = $true) | ($true = (sK0 @ X1 @ X2)) | ((sK0 @ X4 @ X1) = $true) | ((X6 @ X5) != $true) | ($true != (X3 @ X2)) | ((sK0 @ X4 @ X5) = $true) | ((X3 @ X4) = $true) | ((X6 @ X2) = $true) | ((X7 @ X1) != $true) | ((X6 @ X1) = $true) | ((sK0 @ X1 @ X5) = $true) | ($true = (sK0 @ X5 @ X2)) | ((X3 @ X5) = $true) | ((X3 @ X1) = $true) | ((X7 @ X5) = $true) | ((sK0 @ X4 @ X2) = $true) | ((X6 @ X4) = $true) | ($true = (X7 @ X2))) & ! [X9 : $o > $o,X8 : $o > $o] : (((sK0 @ X8 @ X9) = $true) | ((sK0 @ X9 @ X8) != $true)) & ! [X12 : $o > $o,X11 : $o > $o,X10 : ($o > $o) > $o] : (((sK0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true)))),
% 1.70/1.53 introduced(definition,[],[choice_axiom])).
% 1.70/1.53 thf(f9,plain,(
% 1.70/1.53 ? [X0 : ($o > $o) > ($o > $o) > $o] : (! [X1 : $o > $o,X2 : $o > $o,X3 : ($o > $o) > $o,X4 : $o > $o,X5 : $o > $o,X6 : ($o > $o) > $o,X7 : ($o > $o) > $o] : (((X7 @ X4) = $true) | ((X0 @ X1 @ X2) = $true) | ((X0 @ X4 @ X1) = $true) | ((X6 @ X5) != $true) | ($true != (X3 @ X2)) | ((X0 @ X4 @ X5) = $true) | ((X3 @ X4) = $true) | ((X6 @ X2) = $true) | ((X7 @ X1) != $true) | ((X6 @ X1) = $true) | ((X0 @ X1 @ X5) = $true) | ((X0 @ X5 @ X2) = $true) | ((X3 @ X5) = $true) | ((X3 @ X1) = $true) | ((X7 @ X5) = $true) | ((X0 @ X4 @ X2) = $true) | ((X6 @ X4) = $true) | ($true = (X7 @ X2))) & ! [X8 : $o > $o,X9 : $o > $o] : (((X0 @ X8 @ X9) = $true) | ($true != (X0 @ X9 @ X8))) & ! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((X0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true)))),
% 1.70/1.53 inference(rectify,[status(thm)],[f8])).
% 1.70/1.53 thf(f8,plain,(
% 1.70/1.53 ? [X0 : ($o > $o) > ($o > $o) > $o] : (! [X6 : $o > $o,X9 : $o > $o,X3 : ($o > $o) > $o,X8 : $o > $o,X4 : $o > $o,X5 : ($o > $o) > $o,X7 : ($o > $o) > $o] : (($true = (X7 @ X8)) | ((X0 @ X6 @ X9) = $true) | ((X0 @ X8 @ X6) = $true) | ((X5 @ X4) != $true) | ((X3 @ X9) != $true) | ((X0 @ X8 @ X4) = $true) | ((X3 @ X8) = $true) | ((X5 @ X9) = $true) | ((X7 @ X6) != $true) | ((X5 @ X6) = $true) | ((X0 @ X6 @ X4) = $true) | ((X0 @ X4 @ X9) = $true) | ((X3 @ X4) = $true) | ($true = (X3 @ X6)) | ((X7 @ X4) = $true) | ((X0 @ X8 @ X9) = $true) | ((X5 @ X8) = $true) | ((X7 @ X9) = $true)) & ! [X2 : $o > $o,X1 : $o > $o] : (((X0 @ X2 @ X1) = $true) | ((X0 @ X1 @ X2) != $true)) & ! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((X0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true)))),
% 1.70/1.53 inference(flattening,[status(thm)],[f7])).
% 1.70/1.53 thf(f7,plain,(
% 1.70/1.53 ? [X0 : ($o > $o) > ($o > $o) > $o] : ((! [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (((X0 @ X12 @ X11) != $true) | ((X10 @ X11) != $true) | ((X10 @ X12) = $true)) & ! [X6 : $o > $o,X9 : $o > $o,X3 : ($o > $o) > $o,X8 : $o > $o,X4 : $o > $o,X5 : ($o > $o) > $o,X7 : ($o > $o) > $o] : (($true = (X7 @ X8)) | ((X0 @ X6 @ X9) = $true) | ((X0 @ X8 @ X6) = $true) | ((X5 @ X4) != $true) | ((X3 @ X9) != $true) | ((X0 @ X8 @ X4) = $true) | ((X3 @ X8) = $true) | ((X5 @ X9) = $true) | ((X7 @ X6) != $true) | ((X5 @ X6) = $true) | ((X0 @ X6 @ X4) = $true) | ((X0 @ X4 @ X9) = $true) | ((X3 @ X4) = $true) | ($true = (X3 @ X6)) | ((X7 @ X4) = $true) | ((X0 @ X8 @ X9) = $true) | ((X5 @ X8) = $true) | ((X7 @ X9) = $true))) & ! [X2 : $o > $o,X1 : $o > $o] : (((X0 @ X2 @ X1) = $true) | ((X0 @ X1 @ X2) != $true)))),
% 1.70/1.53 inference(ennf_transformation,[status(thm)],[f6])).
% 1.70/1.53 thf(f6,plain,(
% 1.70/1.53 ~! [X0 : ($o > $o) > ($o > $o) > $o] : (! [X2 : $o > $o,X1 : $o > $o] : (((X0 @ X1 @ X2) = $true) => ((X0 @ X2 @ X1) = $true)) => (? [X12 : $o > $o,X11 : $o > $o,X10 : ($o > $o) > $o] : (((X0 @ X12 @ X11) = $true) & ((X10 @ X12) != $true) & ((X10 @ X11) = $true)) | ? [X6 : $o > $o,X5 : ($o > $o) > $o,X8 : $o > $o,X4 : $o > $o,X3 : ($o > $o) > $o,X7 : ($o > $o) > $o,X9 : $o > $o] : (((X3 @ X9) = $true) & ((X0 @ X6 @ X4) != $true) & ((X0 @ X8 @ X9) != $true) & ((X5 @ X8) != $true) & ((X3 @ X4) != $true) & ((X7 @ X4) != $true) & ((X0 @ X4 @ X9) != $true) & ((X7 @ X9) != $true) & ((X3 @ X8) != $true) & ((X0 @ X8 @ X6) != $true) & ($true != (X3 @ X6)) & ((X7 @ X6) = $true) & ((X0 @ X6 @ X9) != $true) & ((X5 @ X9) != $true) & ($true != (X7 @ X8)) & ((X5 @ X6) != $true) & ((X5 @ X4) = $true) & ((X0 @ X8 @ X4) != $true))))),
% 1.70/1.53 inference(flattening,[status(thm)],[f5])).
% 1.70/1.53 thf(f5,plain,(
% 1.70/1.53 ~! [X0 : ($o > $o) > ($o > $o) > $o] : (! [X2 : $o > $o,X1 : $o > $o] : (((X0 @ X1 @ X2) = $true) => ((X0 @ X2 @ X1) = $true)) => (? [X3 : ($o > $o) > $o,X4 : $o > $o,X5 : ($o > $o) > $o,X6 : $o > $o,X7 : ($o > $o) > $o,X8 : $o > $o,X9 : $o > $o] : (~((X5 @ X8) = $true) & ~((X0 @ X6 @ X4) = $true) & ~((X0 @ X6 @ X9) = $true) & ~((X0 @ X8 @ X9) = $true) & ~((X0 @ X8 @ X6) = $true) & ~((X3 @ X8) = $true) & ~((X5 @ X6) = $true) & ~($true = (X3 @ X6)) & ~((X0 @ X8 @ X4) = $true) & ~((X7 @ X9) = $true) & ((X3 @ X9) = $true) & ((X7 @ X6) = $true) & ~((X3 @ X4) = $true) & ~((X5 @ X9) = $true) & ~($true = (X7 @ X8)) & ((X5 @ X4) = $true) & ~((X0 @ X4 @ X9) = $true) & ~((X7 @ X4) = $true)) | ? [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (~((X10 @ X12) = $true) & ((X10 @ X11) = $true) & ((X0 @ X12 @ X11) = $true))))),
% 1.70/1.53 inference(fool_elimination,[status(thm)],[f4])).
% 1.70/1.53 thf(f4,plain,(
% 1.70/1.53 ~! [X0 : ($o > $o) > ($o > $o) > $o] : (! [X1 : $o > $o,X2 : $o > $o] : ((X0 @ X1 @ X2) => (X0 @ X2 @ X1)) => (? [X3 : ($o > $o) > $o,X4 : $o > $o,X5 : ($o > $o) > $o,X6 : $o > $o,X7 : ($o > $o) > $o,X8 : $o > $o,X9 : $o > $o] : (~(X5 @ X8) & ~(X0 @ X6 @ X4) & ~(X0 @ X6 @ X9) & ~(X0 @ X8 @ X9) & ~(X0 @ X8 @ X6) & ~(X3 @ X8) & ~(X5 @ X6) & ~(X3 @ X6) & ~(X0 @ X8 @ X4) & ~(X7 @ X9) & (X3 @ X9) & (X7 @ X6) & ~(X3 @ X4) & ~(X5 @ X9) & ~(X7 @ X8) & (X5 @ X4) & ~(X0 @ X4 @ X9) & ~(X7 @ X4)) | ? [X10 : ($o > $o) > $o,X11 : $o > $o,X12 : $o > $o] : (~(X10 @ X12) & (X10 @ X11) & (X0 @ X12 @ X11))))),
% 1.70/1.53 inference(rectify,[status(thm)],[f2])).
% 1.70/1.53 thf(f2,negated_conjecture,(
% 1.70/1.53 ~! [X0 : ($o > $o) > ($o > $o) > $o] : (! [X1 : $o > $o,X2 : $o > $o] : ((X0 @ X1 @ X2) => (X0 @ X2 @ X1)) => (? [X5 : ($o > $o) > $o,X4 : $o > $o,X8 : ($o > $o) > $o,X6 : $o > $o,X9 : ($o > $o) > $o,X7 : $o > $o,X3 : $o > $o] : (~(X8 @ X7) & ~(X0 @ X6 @ X4) & ~(X0 @ X6 @ X3) & ~(X0 @ X7 @ X3) & ~(X0 @ X7 @ X6) & ~(X5 @ X7) & ~(X8 @ X6) & ~(X5 @ X6) & ~(X0 @ X7 @ X4) & ~(X9 @ X3) & (X5 @ X3) & (X9 @ X6) & ~(X5 @ X4) & ~(X8 @ X3) & ~(X9 @ X7) & (X8 @ X4) & ~(X0 @ X4 @ X3) & ~(X9 @ X4)) | ? [X5 : ($o > $o) > $o,X3 : $o > $o,X4 : $o > $o] : (~(X5 @ X4) & (X5 @ X3) & (X0 @ X4 @ X3))))),
% 1.70/1.53 inference(negated_conjecture,[status(cth)],[f1])).
% 1.70/1.53 thf(f1,conjecture,(
% 1.70/1.53 ! [X0 : ($o > $o) > ($o > $o) > $o] : (! [X1 : $o > $o,X2 : $o > $o] : ((X0 @ X1 @ X2) => (X0 @ X2 @ X1)) => (? [X5 : ($o > $o) > $o,X4 : $o > $o,X8 : ($o > $o) > $o,X6 : $o > $o,X9 : ($o > $o) > $o,X7 : $o > $o,X3 : $o > $o] : (~(X8 @ X7) & ~(X0 @ X6 @ X4) & ~(X0 @ X6 @ X3) & ~(X0 @ X7 @ X3) & ~(X0 @ X7 @ X6) & ~(X5 @ X7) & ~(X8 @ X6) & ~(X5 @ X6) & ~(X0 @ X7 @ X4) & ~(X9 @ X3) & (X5 @ X3) & (X9 @ X6) & ~(X5 @ X4) & ~(X8 @ X3) & ~(X9 @ X7) & (X8 @ X4) & ~(X0 @ X4 @ X3) & ~(X9 @ X4)) | ? [X5 : ($o > $o) > $o,X3 : $o > $o,X4 : $o > $o] : (~(X5 @ X4) & (X5 @ X3) & (X0 @ X4 @ X3))))),
% 1.70/1.53 file('/export/starexec/sandbox/tmp/tmp.MeJNLNMy44/DTF2THF_24996.p',ramsey_u_2_4_4)).
% 1.70/1.53 thf(f49,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((X2 @ X1) = $true) | ((X3 @ X1) = $true) | (X1 = X5) | ((sK0 @ X4 @ X1) = $true) | (X0 = X1) | ((X2 @ X5) = $true) | ($true != (X2 @ X0)) | ((X3 @ X5) = $true) | ((X3 @ X0) = $true) | ((X2 @ X4) = $true) | (X1 = X4) | ((X3 @ X4) != $true)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f48,f12])).
% 1.70/1.53 thf(f48,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((X2 @ X5) = $true) | ((X3 @ X5) = $true) | ((X3 @ X4) != $true) | ($true != (X2 @ X0)) | ((X2 @ X4) = $true) | ((X2 @ X1) = $true) | (X1 = X4) | ((sK0 @ X4 @ X0) = $true) | ((sK0 @ X4 @ X1) = $true) | (X1 = X5) | (X0 = X1) | ((X3 @ X0) = $true) | ((X3 @ X1) = $true)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f47,f16])).
% 1.70/1.53 thf(f47,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((X3 @ X5) = $true) | (X0 = X1) | (X1 = X4) | (X1 = X5) | ((X2 @ X4) = $true) | ((sK0 @ X1 @ X0) = $true) | ((X3 @ X4) != $true) | ((X2 @ X5) = $true) | ((X3 @ X1) = $true) | ($true != (X2 @ X0)) | ((sK0 @ X4 @ X0) = $true) | ((sK0 @ X4 @ X1) = $true) | ((X2 @ X1) = $true) | ((X3 @ X0) = $true)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f46,f12])).
% 1.70/1.53 thf(f46,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((sK0 @ X5 @ X4) = $true) | ($true != (X2 @ X0)) | ((sK0 @ X4 @ X1) = $true) | ((X2 @ X4) = $true) | (X0 = X1) | ((sK0 @ X4 @ X0) = $true) | ((X2 @ X1) = $true) | (X1 = X5) | ((sK0 @ X1 @ X0) = $true) | ((X3 @ X5) = $true) | ((X3 @ X1) = $true) | ((X3 @ X4) != $true) | ((X2 @ X5) = $true) | ((X3 @ X0) = $true) | (X1 = X4)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f45,f12])).
% 1.70/1.53 thf(f45,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((X3 @ X5) = $true) | ((X2 @ X1) = $true) | ((sK0 @ X5 @ X0) = $true) | ((sK0 @ X1 @ X0) = $true) | (X1 = X4) | ((X3 @ X4) != $true) | ((sK0 @ X4 @ X0) = $true) | ((X2 @ X5) = $true) | (X0 = X1) | ((sK0 @ X4 @ X1) = $true) | ((X2 @ X4) = $true) | ((X3 @ X1) = $true) | ($true != (X2 @ X0)) | ((sK0 @ X5 @ X4) = $true) | ((X3 @ X0) = $true) | (X1 = X5)) )),
% 1.70/1.53 inference(subsumption_resolution,[status(thm)],[f27,f16])).
% 1.70/1.53 thf(f27,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : ((X1 = X5) | ((X3 @ X4) != $true) | ($true != (X2 @ X0)) | ((X3 @ X1) = $true) | ($true = (sK0 @ X5 @ X1)) | ((sK0 @ X4 @ X0) = $true) | ((X3 @ X5) = $true) | ((X3 @ X0) = $true) | ((X2 @ X1) = $true) | ((X2 @ X4) = $true) | ((sK0 @ X5 @ X4) = $true) | ((sK0 @ X5 @ X0) = $true) | ((X2 @ X5) = $true) | ((sK0 @ X4 @ X1) = $true) | ((sK0 @ X1 @ X0) = $true) | (X0 = X1) | (X1 = X4)) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f26])).
% 1.70/1.53 thf(f26,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((sK0 @ X5 @ X0) = $true) | ((X1 = X5) = $true) | ((X2 @ X5) = $true) | ((X3 @ X1) = $true) | (X1 = X4) | ($true = (sK0 @ X5 @ X1)) | ((sK0 @ X1 @ X0) = $true) | (X0 = X1) | ((sK0 @ X4 @ X1) = $true) | ((X2 @ X4) = $true) | ((sK0 @ X4 @ X0) = $true) | ((X2 @ X1) = $true) | ((X3 @ X0) = $true) | ((X3 @ X5) = $true) | ((sK0 @ X5 @ X4) = $true) | ((X3 @ X4) != $true) | ($true != (X2 @ X0))) )),
% 1.70/1.53 inference(equality_proxy_clausification,[status(thm)],[f17])).
% 1.70/1.53 thf(f17,plain,(
% 1.70/1.53 ( ! [X2 : ($o > $o) > $o,X3 : ($o > $o) > $o,X0 : $o > $o,X1 : $o > $o,X4 : $o > $o,X5 : $o > $o] : (((X3 @ X1) = $true) | ($true != (X2 @ X0)) | ((sK0 @ X5 @ X4) = $true) | ((sK0 @ X4 @ X1) = $true) | ((sK0 @ X5 @ X0) = $true) | ((X2 @ X1) = $true) | ((X3 @ X4) != $true) | ((X3 @ X0) = $true) | ((sK0 @ X4 @ X0) = $true) | ((X2 @ X4) = $true) | ($true = (X1 = X4)) | ((sK0 @ X1 @ X0) = $true) | ((X3 @ X5) = $true) | ((X1 = X5) = $true) | (X0 = X1) | ($true = (sK0 @ X5 @ X1)) | ((X2 @ X5) = $true)) )),
% 1.70/1.53 inference(leibniz_equality_elimination,[status(thm)],[f14])).
% 1.70/1.53 thf(f14,plain,(
% 1.70/1.53 ( ! [X2 : $o > $o,X3 : ($o > $o) > $o,X1 : $o > $o,X6 : ($o > $o) > $o,X7 : ($o > $o) > $o,X4 : $o > $o,X5 : $o > $o] : (($true != (X3 @ X2)) | ((X7 @ X5) = $true) | ((X6 @ X4) = $true) | ((X3 @ X1) = $true) | ((X3 @ X5) = $true) | ((X6 @ X2) = $true) | ($true = (sK0 @ X1 @ X2)) | ((X3 @ X4) = $true) | ((sK0 @ X4 @ X2) = $true) | ($true = (X7 @ X2)) | ((X7 @ X1) != $true) | ((X7 @ X4) = $true) | ((sK0 @ X4 @ X1) = $true) | ((X6 @ X5) != $true) | ((X6 @ X1) = $true) | ($true = (sK0 @ X5 @ X2)) | ((sK0 @ X4 @ X5) = $true) | ((sK0 @ X1 @ X5) = $true)) )),
% 1.70/1.53 inference(cnf_transformation,[status(thm)],[f11])).
% 1.70/1.53 % SZS output end Proof for DTF2THF_24996
% 1.70/1.53 % (25122)------------------------------
% 1.70/1.53 % (25122)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.70/1.53 % (25122)Termination reason: Refutation
% 1.70/1.53
% 1.70/1.53 % (25122)Memory used [KB]: 6012
% 1.70/1.53 % (25122)Time elapsed: 0.087 s
% 1.70/1.53 % (25122)Instructions burned: 286 (million)
% 1.70/1.53 % (25122)------------------------------
% 1.70/1.53 % (25122)------------------------------
% 1.70/1.53 % (25092)Success in time 0.199 s
%------------------------------------------------------------------------------