%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO903^10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:37 AM UTC 2026
% Result : ContradictoryAxioms 0.21s 0.35s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 34
% Syntax : Number of formulae : 376 ( 70 unt; 0 typ; 19 def)
% Number of atoms : 4433 ( 918 equ; 0 cnn)
% Maximal formula atoms : 17 ( 11 avg)
% Number of connectives : 5653 ( 346 ~; 921 |; 0 &;3583 @)
% ( 19 <=>; 459 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 148 ( 148 >; 0 *; 0 +; 0 <<)
% Number of symbols : 51 ( 47 usr; 25 con; 0-4 aty)
% ( 325 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 995 ( 0 sgn 355 !; 0 ?; 995 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
mworld: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
mrel: mworld > mworld > $o ).
thf(func_def_1,type,
mactual: mworld ).
thf(func_def_2,type,
mlocal: ( mworld > $o ) > $o ).
thf(func_def_4,type,
mnot: ( mworld > $o ) > mworld > $o ).
thf(func_def_5,type,
mand: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_6,type,
mor: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_7,type,
mimplies: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_8,type,
mequiv: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(func_def_9,type,
mbox: ( mworld > $o ) > mworld > $o ).
thf(func_def_10,type,
mdia: ( mworld > $o ) > mworld > $o ).
thf(func_def_11,type,
v1: mworld > $o ).
thf(func_def_12,type,
v2: mworld > $o ).
thf(func_def_13,type,
v3: mworld > $o ).
thf(func_def_14,type,
v4: mworld > $o ).
thf(func_def_15,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_16,type,
vAND: $o > $o > $o ).
thf(func_def_17,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_18,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_19,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_20,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_23,type,
vIFF: $o > $o > $o ).
thf(func_def_24,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_25,type,
vIMP: $o > $o > $o ).
thf(func_def_26,type,
vOR: $o > $o > $o ).
thf(func_def_27,type,
vNOT: $o > $o ).
thf(func_def_28,type,
sF0: $o ).
thf(func_def_29,type,
sK1: mworld ).
thf(f1,axiom,
( mlocal
= ( ^ [X0: mworld > $o] : ( X0 @ mactual ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mlocal_def) ).
thf(f2,axiom,
( mnot
= ( ^ [X0: mworld > $o,X1: mworld] :
~ ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mnot_def) ).
thf(f4,axiom,
( ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X0 @ X2 )
| ( X1 @ X2 ) ) )
= mor ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mor_def) ).
thf(f7,axiom,
( ( ^ [X0: mworld > $o,X1: mworld] :
! [X2: mworld] :
( ( mrel @ X1 @ X2 )
=> ( X0 @ X2 ) ) )
= mbox ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mbox_def) ).
thf(f9,axiom,
! [X0: mworld] : ( mrel @ X0 @ X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mrel_reflexive) ).
thf(f13,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat3) ).
thf(f15,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat5) ).
thf(f28,axiom,
mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat18) ).
thf(f36,axiom,
mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat26) ).
thf(f39,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat29) ).
thf(f41,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat31) ).
thf(f45,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat35) ).
thf(f48,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat38) ).
thf(f55,axiom,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat45) ).
thf(f56,axiom,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',persat46) ).
thf(f76,plain,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
inference(rectify,[],[f45]) ).
thf(f77,plain,
( ( mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f76]) ).
thf(f80,plain,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
inference(rectify,[],[f41]) ).
thf(f81,plain,
( ( mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f80]) ).
thf(f84,plain,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
inference(rectify,[],[f55]) ).
thf(f85,plain,
( ( mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f84]) ).
thf(f88,plain,
( mlocal
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual ) ) ),
inference(fool_elimination,[],[f1]) ).
thf(f95,plain,
( ( ^ [X0: mworld > $o,X1: mworld] :
! [X2: mworld] :
( ( mrel @ X1 @ X2 )
=> ( X0 @ X2 ) ) )
= mbox ),
inference(rectify,[],[f7]) ).
thf(f96,plain,
( mbox
= ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(fool_elimination,[],[f95]) ).
thf(f101,plain,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
inference(rectify,[],[f56]) ).
thf(f102,plain,
( ( mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f101]) ).
thf(f107,plain,
mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
inference(rectify,[],[f15]) ).
thf(f108,plain,
( ( mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f107]) ).
thf(f111,plain,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
inference(rectify,[],[f39]) ).
thf(f112,plain,
( ( mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f111]) ).
thf(f117,plain,
! [X0: mworld] : ( mrel @ X0 @ X0 ),
inference(rectify,[],[f9]) ).
thf(f118,plain,
! [X0: mworld] :
( ( mrel @ X0 @ X0 )
= $true ),
inference(fool_elimination,[],[f117]) ).
thf(f129,plain,
( ( ^ [X0: mworld > $o,X1: mworld > $o,X2: mworld] :
( ( X0 @ X2 )
| ( X1 @ X2 ) ) )
= mor ),
inference(rectify,[],[f4]) ).
thf(f130,plain,
( mor
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f129]) ).
thf(f149,plain,
mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
inference(rectify,[],[f36]) ).
thf(f150,plain,
( ( mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f149]) ).
thf(f151,plain,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
inference(rectify,[],[f48]) ).
thf(f152,plain,
( ( mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f151]) ).
thf(f173,plain,
mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
inference(rectify,[],[f28]) ).
thf(f174,plain,
( ( mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f173]) ).
thf(f175,plain,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
inference(rectify,[],[f13]) ).
thf(f176,plain,
( ( mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f175]) ).
thf(f185,plain,
( mnot
= ( ^ [X0: mworld > $o,X1: mworld] :
~ ( X0 @ X1 ) ) ),
inference(rectify,[],[f2]) ).
thf(f186,plain,
( mnot
= ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 ) ) ),
inference(fool_elimination,[],[f185]) ).
thf(f193,plain,
( ( mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f85]) ).
thf(f194,plain,
( ( mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f102]) ).
thf(f201,plain,
( mnot
= ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 ) ) ),
inference(cnf_transformation,[],[f186]) ).
thf(f218,plain,
( ( mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f81]) ).
thf(f220,plain,
( ( mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f176]) ).
thf(f228,plain,
( mlocal
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual ) ) ),
inference(cnf_transformation,[],[f88]) ).
thf(f231,plain,
( ( mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f150]) ).
thf(f232,plain,
( mor
= ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f130]) ).
thf(f233,plain,
( ( mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f152]) ).
thf(f234,plain,
( mbox
= ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f96]) ).
thf(f235,plain,
( ( mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f112]) ).
thf(f237,plain,
( ( mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f77]) ).
thf(f240,plain,
( ( mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f174]) ).
thf(f247,plain,
! [X0: mworld] :
( ( mrel @ X0 @ X0 )
= $true ),
inference(cnf_transformation,[],[f118]) ).
thf(f250,plain,
( ( mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f108]) ).
thf(f257,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v3 ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f193,f228,f232,f201,f232,f234,f232,f234,f201,f234,f234]) ).
thf(f258,plain,
( ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f194,f228,f232,f201,f232,f234,f201,f232,f234,f234,f201,f234,f234,f201]) ).
thf(f278,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v4
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v1 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v4 ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f218,f228,f232,f232,f201,f232,f234,f234,f234,f234]) ).
thf(f280,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v1
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v2
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f220,f228,f232,f232,f232,f201,f234,f234,f201]) ).
thf(f290,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v3
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v3 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f231,f228,f232,f232,f201,f232,f234,f234,f234,f234,f201]) ).
thf(f291,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v4 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v4 ) ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f233,f228,f232,f201,f232,f234,f201,f232,f234,f234,f234,f234,f201]) ).
thf(f292,plain,
( ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v4
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v3 ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f235,f228,f232,f232,f201,f232,f234,f201,f234,f234]) ).
thf(f294,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v4 ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f237,f228,f232,f201,f232,f201,f232,f234,f201,f234,f234]) ).
thf(f297,plain,
( ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v2
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v3 )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
~ ( Y0 @ Y1 )
@ v1 ) ) ) ) ) ) )
= $true ),
inference(definition_unfolding,[],[f240,f228,f232,f232,f201,f232,f234,f201,f234,f234,f201]) ).
thf(f304,plain,
( $true
= ( ^ [Y0: mworld > $o] : ( Y0 @ mactual )
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v1
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ v3
@ ( ^ [Y0: mworld > $o,Y1: mworld > $o,Y2: mworld] :
( ( Y1 @ Y2 )
| ( Y0 @ Y2 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v3 ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ ( ^ [Y0: mworld > $o,Y1: mworld] :
( !! @ mworld
@ ^ [Y2: mworld] :
( ( mrel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) )
@ v4 ) ) ) ) ) ) ),
inference(definition_unfolding,[],[f250,f228,f232,f232,f232,f234,f234,f234,f234]) ).
thf(f310,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) )
| ~ ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f257]) ).
thf(f311,plain,
( ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f310]) ).
thf(f312,plain,
( ( $false
= ( v3 @ mactual ) )
| ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true ) ),
inference(not_proxy_clausification,[],[f311]) ).
thf(f313,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f312]) ).
thf(f314,plain,
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f313]) ).
thf(f315,plain,
! [X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X1 ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f314]) ).
thf(f316,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) )
@ X2 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f315]) ).
thf(f317,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( v3 @ Y0 ) )
@ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X3 ) ) ),
inference(pi_proxy_clausification,[],[f316]) ).
thf(f318,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X1 )
=> ~ ( v4 @ X1 ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( ( mrel @ mactual @ X3 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( v3 @ X2 ) ) ) ),
inference(beta-eta_normalization,[],[f317]) ).
thf(f319,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ~ ( v4 @ X1 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( v3 @ X2 ) ) )
| ( ( ( mrel @ mactual @ X3 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f318]) ).
thf(f320,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( v4 @ X1 ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( v3 @ X2 ) ) )
| ( ( ( mrel @ mactual @ X3 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f319]) ).
thf(f321,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v3 @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( ( mrel @ mactual @ X3 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
= $true )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v4 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f320]) ).
thf(f322,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v3 @ X2 ) )
| ( $false
= ( v4 @ X1 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f321]) ).
thf(f323,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v4 @ X1 ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( ^ [Y0: mworld] :
( ( mrel @ X3 @ Y0 )
=> ( v3 @ Y0 ) )
@ X4 )
= $true )
| ( $true
= ( v3 @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(pi_proxy_clausification,[],[f322]) ).
thf(f324,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( ( mrel @ X3 @ X4 )
=> ( v3 @ X4 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v3 @ X2 ) )
| ( $false
= ( v4 @ X1 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f323]) ).
thf(f325,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( mrel @ X3 @ X4 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v4 @ X1 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( v3 @ X4 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v3 @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f324]) ).
thf(f363,plain,
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) )
| ~ ( v1 @ mactual )
| ( v4 @ mactual ) )
= $true ),
inference(beta-eta_normalization,[],[f292]) ).
thf(f364,plain,
( ( $true
= ( v4 @ mactual ) )
| ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) )
| ~ ( v1 @ mactual ) )
= $true ) ),
inference(or_proxy_clausification,[],[f363]) ).
thf(f365,plain,
( ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ~ ( v1 @ mactual ) ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f364]) ).
thf(f366,plain,
( ( $true
= ( v4 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f365]) ).
thf(f367,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( v4 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f366]) ).
thf(f368,plain,
! [X1: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( v4 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f367]) ).
thf(f369,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) )
@ X2 ) )
| ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X1 ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(pi_proxy_clausification,[],[f368]) ).
thf(f370,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ~ ( v1 @ X2 ) ) )
| ( $true
= ( v4 @ mactual ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(beta-eta_normalization,[],[f369]) ).
thf(f371,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v4 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ~ ( v1 @ X2 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f370]) ).
thf(f372,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) )
@ X3 ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ~ ( v1 @ X2 ) ) )
| ( $true
= ( v4 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(pi_proxy_clausification,[],[f371]) ).
thf(f373,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) )
@ X3 ) )
| ( $true
= ( ~ ( v1 @ X2 ) ) )
| ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v4 @ mactual ) ) ),
inference(imp_proxy_clausification,[],[f372]) ).
thf(f374,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) )
@ X3 ) )
| ( $false
= ( v1 @ X2 ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( v4 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(not_proxy_clausification,[],[f373]) ).
thf(f375,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( ( mrel @ X1 @ X3 )
=> ( v3 @ X3 ) ) )
| ( $false
= ( v1 @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v4 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f374]) ).
thf(f376,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( v4 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ X1 @ X3 ) )
| ( $true
= ( v3 @ X3 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v1 @ X2 ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(imp_proxy_clausification,[],[f375]) ).
thf(f377,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) )
| ~ ( v3 @ mactual )
| ( v2 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f297]) ).
thf(f378,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) )
| ~ ( v3 @ mactual ) ) )
| ( $true
= ( v2 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f377]) ).
thf(f379,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( v2 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f378]) ).
thf(f380,plain,
( ( $true
= ( v2 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f379]) ).
thf(f381,plain,
! [X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) )
@ X1 ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) ) ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( v2 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f380]) ).
thf(f382,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) )
@ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) )
@ X1 ) )
| ( $true
= ( v2 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f381]) ).
thf(f383,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v1 @ Y1 ) ) ) )
@ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v1 @ Y0 ) )
@ X1 ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f382]) ).
thf(f384,plain,
! [X2: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) ) )
| ( $true
= ( v2 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ~ ( v1 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f383]) ).
thf(f385,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X1 )
=> ~ ( v1 @ X1 ) ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f384]) ).
thf(f386,plain,
! [X2: mworld,X1: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( ~ ( v1 @ X1 ) )
= $true )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f385]) ).
thf(f387,plain,
! [X2: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v1 @ X1 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v1 @ Y0 ) ) ) )
| ( $true
= ( v2 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f386]) ).
thf(f388,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( v2 @ mactual ) )
| ( ( v1 @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v1 @ Y0 ) )
@ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f387]) ).
thf(f389,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v1 @ X1 )
= $false )
| ( $true
= ( v2 @ mactual ) )
| ( $true
= ( ( mrel @ X2 @ X3 )
=> ~ ( v1 @ X3 ) ) ) ),
inference(beta-eta_normalization,[],[f388]) ).
thf(f390,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ~ ( v1 @ X3 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v1 @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( mrel @ X2 @ X3 ) ) ),
inference(imp_proxy_clausification,[],[f389]) ).
thf(f391,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( mrel @ X2 @ X3 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( ( v1 @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v1 @ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(not_proxy_clausification,[],[f390]) ).
thf(f442,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) ) )
| ~ ( v3 @ mactual )
| ( v4 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f278]) ).
thf(f443,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) ) )
| ~ ( v3 @ mactual ) ) )
| ( $true
= ( v4 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f442]) ).
thf(f444,plain,
( ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) ) ) ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f443]) ).
thf(f445,plain,
( ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) ) ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( v4 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f444]) ).
thf(f446,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) ) ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( v4 @ mactual ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f445]) ).
thf(f447,plain,
! [X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( v4 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f446]) ).
thf(f448,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) )
@ X2 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v1 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( v4 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f447]) ).
thf(f449,plain,
! [X2: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v1 @ Y0 ) ) ) ) )
| ( $true
= ( v4 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f448]) ).
thf(f450,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v1 @ Y0 ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(imp_proxy_clausification,[],[f449]) ).
thf(f451,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v1 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v4 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f450]) ).
thf(f452,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v1 @ Y0 ) )
@ X3 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f451]) ).
thf(f453,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v4 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v1 @ Y0 ) )
@ X3 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f452]) ).
thf(f454,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v4 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v4 @ X4 ) ) )
| ( $true
= ( ( mrel @ X1 @ X3 )
=> ( v1 @ X3 ) ) ) ),
inference(beta-eta_normalization,[],[f453]) ).
thf(f455,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( ( mrel @ X1 @ X3 )
=> ( v1 @ X3 ) ) )
| ( $true
= ( v4 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v4 @ X4 ) ) ),
inference(imp_proxy_clausification,[],[f454]) ).
thf(f456,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( v4 @ mactual ) )
| ( $true
= ( v1 @ X3 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ X1 @ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v4 @ X4 ) ) ),
inference(imp_proxy_clausification,[],[f455]) ).
thf(f491,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( v3 @ mactual )
| ( v1 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f304]) ).
thf(f492,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ( v3 @ mactual ) ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f491]) ).
thf(f493,plain,
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f492]) ).
thf(f494,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f493]) ).
thf(f495,plain,
! [X1: mworld] :
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f494]) ).
thf(f496,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) )
@ X2 ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f495]) ).
thf(f497,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) ) ) ) )
| ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f496]) ).
thf(f498,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(imp_proxy_clausification,[],[f497]) ).
thf(f499,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f498]) ).
thf(f500,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) )
@ X3 ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f499]) ).
thf(f501,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ( v3 @ Y0 ) )
@ X3 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( $true
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(pi_proxy_clausification,[],[f500]) ).
thf(f502,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v4 @ X4 ) ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ( mrel @ X1 @ X3 )
=> ( v3 @ X3 ) ) )
| ( $true
= ( v1 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(beta-eta_normalization,[],[f501]) ).
thf(f503,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v4 @ X4 ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ X1 @ X3 )
=> ( v3 @ X3 ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( v1 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f502]) ).
thf(f504,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( mrel @ X1 @ X3 ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v1 @ mactual ) )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( v4 @ X4 ) )
| ( $true
= ( v3 @ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f503]) ).
thf(f733,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
| ~ ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f258]) ).
thf(f734,plain,
( ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f733]) ).
thf(f735,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f734]) ).
thf(f736,plain,
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) ) ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f735]) ).
thf(f737,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f736]) ).
thf(f738,plain,
! [X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) ) ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true ) ),
inference(pi_proxy_clausification,[],[f737]) ).
thf(f739,plain,
! [X2: mworld,X1: mworld] :
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) )
@ X2 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f738]) ).
thf(f740,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v2 @ Y1 ) ) ) )
@ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f739]) ).
thf(f741,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X3 )
=> ~ ( v4 @ X3 ) ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f740]) ).
thf(f742,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( ( ~ ( v4 @ X3 ) )
= $true )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f741]) ).
thf(f743,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( v4 @ X3 )
= $false )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f742]) ).
thf(f744,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v4 @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f743]) ).
thf(f745,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) )
@ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( ( v4 @ X3 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f744]) ).
thf(f746,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) )
@ X4 ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( v4 @ X3 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f745]) ).
thf(f747,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X5 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ~ ( v2 @ Y0 ) )
@ X4 ) ) ),
inference(pi_proxy_clausification,[],[f746]) ).
thf(f748,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( $true
= ( ( mrel @ X2 @ X4 )
=> ~ ( v2 @ X4 ) ) )
| ( $true
= ( ( mrel @ X1 @ X5 )
=> ~ ( v4 @ X5 ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( ( v4 @ X3 )
= $false )
| ( ( mrel @ mactual @ X3 )
= $false ) ),
inference(beta-eta_normalization,[],[f747]) ).
thf(f749,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( ~ ( v2 @ X4 ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v4 @ X3 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ( mrel @ X1 @ X5 )
=> ~ ( v4 @ X5 ) ) ) ),
inference(imp_proxy_clausification,[],[f748]) ).
thf(f750,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( v4 @ X3 )
= $false )
| ( $true
= ( ( mrel @ X1 @ X5 )
=> ~ ( v4 @ X5 ) ) )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v2 @ X4 )
= $false )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f749]) ).
thf(f751,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ~ ( v4 @ X5 ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v4 @ X3 )
= $false )
| ( ( v2 @ X4 )
= $false )
| ( $false
= ( mrel @ X1 @ X5 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) ) ),
inference(imp_proxy_clausification,[],[f750]) ).
thf(f752,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( v2 @ X4 )
= $false )
| ( ( v4 @ X5 )
= $false )
| ( $false
= ( mrel @ X1 @ X5 ) )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( ( mrel @ mactual @ X3 )
= $false ) ),
inference(not_proxy_clausification,[],[f751]) ).
thf(f896,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ~ ( v3 @ mactual )
| ( v2 @ mactual )
| ( v1 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f280]) ).
thf(f897,plain,
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ~ ( v3 @ mactual )
| ( v2 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f896]) ).
thf(f898,plain,
( ( $true
= ( v2 @ mactual ) )
| ( $true
= ( v1 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ~ ( v3 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f897]) ).
thf(f899,plain,
( ( $true
= ( v2 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f898]) ).
thf(f900,plain,
! [X1: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( v2 @ mactual ) )
| ( $true
= ( ~ ( v3 @ mactual ) ) ) ),
inference(pi_proxy_clausification,[],[f899]) ).
thf(f901,plain,
! [X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( $true
= ( v1 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f900]) ).
thf(f902,plain,
! [X1: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f901]) ).
thf(f903,plain,
! [X1: mworld] :
( ( $true
= ( v2 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v1 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f902]) ).
thf(f904,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X2 ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(pi_proxy_clausification,[],[f903]) ).
thf(f905,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ X1 @ X2 )
=> ~ ( v4 @ X2 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f904]) ).
thf(f906,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v1 @ mactual ) )
| ( $true
= ( v2 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ X1 @ X2 )
= $false )
| ( ( ~ ( v4 @ X2 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f905]) ).
thf(f907,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v2 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( mrel @ X1 @ X2 )
= $false )
| ( $true
= ( v1 @ mactual ) )
| ( $false
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ X2 ) ) ),
inference(not_proxy_clausification,[],[f906]) ).
thf(f1004,plain,
( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) ) )
| ~ ( v3 @ mactual )
| ~ ( v1 @ mactual ) )
= $true ),
inference(beta-eta_normalization,[],[f294]) ).
thf(f1005,plain,
( ( $true
= ( ~ ( v1 @ mactual ) ) )
| ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) ) )
| ~ ( v3 @ mactual ) )
= $true ) ),
inference(or_proxy_clausification,[],[f1004]) ).
thf(f1006,plain,
( ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) ) )
| ~ ( v3 @ mactual ) )
= $true )
| ( ( v1 @ mactual )
= $false ) ),
inference(not_proxy_clausification,[],[f1005]) ).
thf(f1007,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) ) ) ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( ~ ( v3 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f1006]) ).
thf(f1008,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) ) ) )
| ( ( v1 @ mactual )
= $false )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( ~ ( v3 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f1007]) ).
thf(f1009,plain,
! [X1: mworld] :
( ( $true
= ( ~ ( v3 @ mactual ) ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) )
@ X1 ) )
| ( ( v1 @ mactual )
= $false )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true ) ),
inference(pi_proxy_clausification,[],[f1008]) ).
thf(f1010,plain,
! [X1: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f1009]) ).
thf(f1011,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v3 @ Y0 ) )
@ X1 ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f1010]) ).
thf(f1012,plain,
! [X2: mworld,X1: mworld] :
( ( ( ( mrel @ mactual @ X1 )
=> ~ ( v3 @ X1 ) )
= $true )
| ( $false
= ( v3 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1011]) ).
thf(f1013,plain,
! [X2: mworld,X1: mworld] :
( ( ( ~ ( v3 @ X1 ) )
= $true )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1012]) ).
thf(f1014,plain,
! [X2: mworld,X1: mworld] :
( ( ( v3 @ X1 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v1 @ mactual )
= $false )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) )
| ( $false
= ( v3 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f1013]) ).
thf(f1015,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v3 @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v1 @ mactual )
= $false ) ),
inference(imp_proxy_clausification,[],[f1014]) ).
thf(f1016,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( v3 @ X1 )
= $false )
| ( $false
= ( v3 @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X3 )
= $true )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f1015]) ).
thf(f1017,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ X2 @ X3 )
=> ( v4 @ X3 ) ) )
| ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v3 @ X1 )
= $false ) ),
inference(beta-eta_normalization,[],[f1016]) ).
thf(f1018,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v4 @ X3 ) )
| ( ( v3 @ X1 )
= $false )
| ( $false
= ( mrel @ X2 @ X3 ) )
| ( ( v1 @ mactual )
= $false )
| ( $false
= ( v3 @ mactual ) ) ),
inference(imp_proxy_clausification,[],[f1017]) ).
thf(f1019,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ~ ( v4 @ mactual )
| ( v3 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f290]) ).
thf(f1020,plain,
( ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) )
| ~ ( v4 @ mactual ) ) ) ),
inference(or_proxy_clausification,[],[f1019]) ).
thf(f1021,plain,
( ( $true
= ( ~ ( v4 @ mactual ) ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f1020]) ).
thf(f1022,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ mactual ) ) ),
inference(not_proxy_clausification,[],[f1021]) ).
thf(f1023,plain,
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( v3 @ mactual ) ) ),
inference(or_proxy_clausification,[],[f1022]) ).
thf(f1024,plain,
! [X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) ) ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( v3 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f1023]) ).
thf(f1025,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ mactual ) )
| ( ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v3 @ Y1 ) ) ) )
@ X2 )
= $true ) ),
inference(pi_proxy_clausification,[],[f1024]) ).
thf(f1026,plain,
! [X2: mworld,X1: mworld] :
( ( $false
= ( v4 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( v3 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v3 @ Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1025]) ).
thf(f1027,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v3 @ Y0 ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1026]) ).
thf(f1028,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v3 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1027]) ).
thf(f1029,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X3 ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v3 @ Y0 ) ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v4 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v3 @ mactual ) ) ),
inference(pi_proxy_clausification,[],[f1028]) ).
thf(f1030,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v3 @ Y0 ) )
@ X4 ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X3 ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(pi_proxy_clausification,[],[f1029]) ).
thf(f1031,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v4 @ mactual ) )
| ( ( ( mrel @ X1 @ X3 )
=> ~ ( v4 @ X3 ) )
= $true )
| ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v3 @ X4 ) ) ) ),
inference(beta-eta_normalization,[],[f1030]) ).
thf(f1032,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v3 @ X4 ) ) )
| ( ( ~ ( v4 @ X3 ) )
= $true )
| ( $false
= ( mrel @ X1 @ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ mactual ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f1031]) ).
thf(f1033,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $true
= ( v3 @ mactual ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X1 @ X3 ) )
| ( $false
= ( v4 @ mactual ) )
| ( ( ~ ( v4 @ X3 ) )
= $true )
| ( $true
= ( v3 @ X4 ) ) ),
inference(imp_proxy_clausification,[],[f1032]) ).
thf(f1034,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( v4 @ X3 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X1 @ X3 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( $true
= ( v3 @ mactual ) )
| ( $false
= ( v4 @ mactual ) )
| ( $true
= ( v3 @ X4 ) ) ),
inference(not_proxy_clausification,[],[f1033]) ).
thf(f1048,plain,
( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
| ~ ( v1 @ mactual ) ) ),
inference(beta-eta_normalization,[],[f291]) ).
thf(f1049,plain,
( ( $true
= ( ~ ( v1 @ mactual ) ) )
| ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f1048]) ).
thf(f1050,plain,
( ( $true
= ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(not_proxy_clausification,[],[f1049]) ).
thf(f1051,plain,
( ( ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) )
| ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) ) )
= $true )
| ( ( v1 @ mactual )
= $false )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f1050]) ).
thf(f1052,plain,
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) ) ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f1051]) ).
thf(f1053,plain,
! [X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) ) )
= $true )
| ( ( v1 @ mactual )
= $false )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true ) ),
inference(pi_proxy_clausification,[],[f1052]) ).
thf(f1054,plain,
! [X2: mworld,X1: mworld] :
( ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) )
@ X2 ) )
| ( ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) ) )
= $true )
| ( ( v1 @ mactual )
= $false ) ),
inference(pi_proxy_clausification,[],[f1053]) ).
thf(f1055,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ( v4 @ Y1 ) ) ) )
@ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ( !! @ mworld
@ ^ [Y1: mworld] :
( ( mrel @ Y0 @ Y1 )
=> ~ ( v4 @ Y1 ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ mactual @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X3 ) ) ),
inference(pi_proxy_clausification,[],[f1054]) ).
thf(f1056,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $true
= ( ( mrel @ mactual @ X2 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X3 )
=> ~ ( v4 @ X3 ) ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(beta-eta_normalization,[],[f1055]) ).
thf(f1057,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ( mrel @ mactual @ X1 )
=> ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X3 )
=> ~ ( v4 @ X3 ) ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(imp_proxy_clausification,[],[f1056]) ).
thf(f1058,plain,
! [X2: mworld,X3: mworld,X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) ) ) )
| ( $true
= ( ( mrel @ mactual @ X3 )
=> ~ ( v4 @ X3 ) ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) )
| ( ( v1 @ mactual )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(imp_proxy_clausification,[],[f1057]) ).
thf(f1059,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( $true
= ( ( mrel @ mactual @ X3 )
=> ~ ( v4 @ X3 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f1058]) ).
thf(f1060,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( ~ ( v4 @ X3 ) )
= $true )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) )
| ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1059]) ).
thf(f1061,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( ( v1 @ mactual )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( $true
= ( !! @ mworld
@ ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) ) ) ) ),
inference(not_proxy_clausification,[],[f1060]) ).
thf(f1062,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( v4 @ X3 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X1 @ Y0 )
=> ~ ( v4 @ Y0 ) )
@ X5 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ^ [Y0: mworld] :
( ( mrel @ X2 @ Y0 )
=> ( v4 @ Y0 ) )
@ X4 ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(pi_proxy_clausification,[],[f1061]) ).
thf(f1063,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( v1 @ mactual )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( $true
= ( ( mrel @ X1 @ X5 )
=> ~ ( v4 @ X5 ) ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v4 @ X4 ) ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ),
inference(beta-eta_normalization,[],[f1062]) ).
thf(f1064,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( $false
= ( mrel @ X1 @ X5 ) )
| ( $true
= ( ( mrel @ X2 @ X4 )
=> ( v4 @ X4 ) ) )
| ( $true
= ( ~ ( v4 @ X5 ) ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v1 @ mactual )
= $false ) ),
inference(imp_proxy_clausification,[],[f1063]) ).
thf(f1065,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( ~ ( v4 @ X5 ) ) )
| ( $false
= ( mrel @ X1 @ X5 ) )
| ( $true
= ( v4 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v1 @ mactual )
= $false )
| ( ( v4 @ X3 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1064]) ).
thf(f1066,plain,
! [X2: mworld,X3: mworld,X1: mworld,X4: mworld,X5: mworld] :
( ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ X2 @ X4 ) )
| ( ( v4 @ X5 )
= $false )
| ( ( v4 @ X3 )
= $false )
| ( ( v1 @ mactual )
= $false )
| ( $false
= ( mrel @ X1 @ X5 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( $true
= ( v4 @ X4 ) ) ),
inference(not_proxy_clausification,[],[f1065]) ).
thf(f1096,definition,
( spl2_1
<=> ! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v4 @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
thf(f1097,plain,
( ! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v4 @ X1 ) ) )
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f1096]) ).
thf(f1099,definition,
( spl2_2
<=> ! [X2: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v3 @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
thf(f1100,plain,
( ! [X2: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v3 @ X2 ) ) )
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f1099]) ).
thf(f1102,definition,
( spl2_3
<=> ( $false
= ( v3 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
thf(f1103,plain,
( ( $false
!= ( v3 @ mactual ) )
| spl2_3 ),
inference(avatar_component_clause,[],[f1102]) ).
thf(f1104,plain,
( ( $false
= ( v3 @ mactual ) )
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f1102]) ).
thf(f1106,definition,
( spl2_4
<=> ! [X4: mworld,X3: mworld] :
( ( $false
= ( mrel @ X3 @ X4 ) )
| ( $true
= ( v3 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
thf(f1107,plain,
( ! [X3: mworld,X4: mworld] :
( ( $false
= ( mrel @ X3 @ X4 ) )
| ( $true
= ( v3 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false ) )
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f1106]) ).
thf(f1108,plain,
( spl2_1
| spl2_2
| spl2_3
| spl2_4 ),
inference(avatar_split_clause,[],[f325,f1106,f1102,f1099,f1096]) ).
thf(f1110,definition,
( spl2_5
<=> ( $false
= ( v4 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
thf(f1112,plain,
( ( $false
= ( v4 @ mactual ) )
| ~ spl2_5 ),
inference(avatar_component_clause,[],[f1110]) ).
thf(f1114,definition,
( spl2_6
<=> ( $true
= ( v1 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
thf(f1115,plain,
( ( $true
!= ( v1 @ mactual ) )
| spl2_6 ),
inference(avatar_component_clause,[],[f1114]) ).
thf(f1116,plain,
( ( $true
= ( v1 @ mactual ) )
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f1114]) ).
thf(f1118,definition,
( spl2_7
<=> ! [X2: mworld,X1: mworld] :
( ( $false
= ( v2 @ X2 ) )
| ( ( mrel @ mactual @ X1 )
= $false )
| ( ( mrel @ X1 @ X2 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
thf(f1119,plain,
( ! [X2: mworld,X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( $false
= ( v2 @ X2 ) )
| ( ( mrel @ X1 @ X2 )
= $false ) )
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f1118]) ).
thf(f1121,definition,
( spl2_8
<=> ( $false
= ( v2 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
thf(f1123,plain,
( ( $false
= ( v2 @ mactual ) )
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f1121]) ).
thf(f1126,definition,
( spl2_9
<=> ! [X2: mworld,X5: mworld] :
( ( $false
= ( mrel @ X2 @ X5 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v4 @ X5 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
thf(f1127,plain,
( ! [X2: mworld,X5: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( ( v4 @ X5 )
= $true )
| ( $false
= ( mrel @ X2 @ X5 ) ) )
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f1126]) ).
thf(f1129,definition,
( spl2_10
<=> ! [X4: mworld,X3: mworld] :
( ( $false
= ( v4 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( mrel @ X3 @ X4 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
thf(f1130,plain,
( ! [X3: mworld,X4: mworld] :
( ( $false
= ( mrel @ X3 @ X4 ) )
| ( ( mrel @ mactual @ X3 )
= $false )
| ( $false
= ( v4 @ X4 ) ) )
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f1129]) ).
thf(f1132,definition,
( spl2_11
<=> ! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v2 @ X1 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
thf(f1133,plain,
( ! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v2 @ X1 )
= $false ) )
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f1132]) ).
thf(f1136,definition,
( spl2_12
<=> ( $true
= ( v4 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
thf(f1138,plain,
( ( $true
= ( v4 @ mactual ) )
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f1136]) ).
thf(f1140,definition,
( spl2_13
<=> ! [X2: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v1 @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_13])],[avatar_definition]) ).
thf(f1141,plain,
( ! [X2: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( v1 @ X2 ) ) )
| ~ spl2_13 ),
inference(avatar_component_clause,[],[f1140]) ).
thf(f1143,definition,
( spl2_14
<=> ( ( v1 @ mactual )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
thf(f1145,plain,
( ( ( v1 @ mactual )
= $false )
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f1143]) ).
thf(f1146,plain,
( spl2_12
| spl2_13
| spl2_14
| spl2_4 ),
inference(avatar_split_clause,[],[f376,f1106,f1143,f1140,f1136]) ).
thf(f1148,definition,
( spl2_15
<=> ( $true
= ( v2 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
thf(f1150,plain,
( ( $true
= ( v2 @ mactual ) )
| ~ spl2_15 ),
inference(avatar_component_clause,[],[f1148]) ).
thf(f1152,definition,
( spl2_16
<=> ! [X2: mworld,X3: mworld] :
( ( $false
= ( mrel @ X2 @ X3 ) )
| ( $false
= ( v1 @ X3 ) )
| ( $false
= ( mrel @ mactual @ X2 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
thf(f1153,plain,
( ! [X2: mworld,X3: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X2 @ X3 ) )
| ( $false
= ( v1 @ X3 ) ) )
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f1152]) ).
thf(f1154,plain,
( spl2_13
| spl2_3
| spl2_15
| spl2_16 ),
inference(avatar_split_clause,[],[f391,f1152,f1148,f1102,f1140]) ).
thf(f1156,definition,
( spl2_17
<=> ! [X4: mworld,X2: mworld] :
( ( $true
= ( v1 @ X4 ) )
| ( $false
= ( mrel @ mactual @ X2 ) )
| ( $false
= ( mrel @ X2 @ X4 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
thf(f1157,plain,
( ! [X2: mworld,X4: mworld] :
( ( $false
= ( mrel @ mactual @ X2 ) )
| ( $true
= ( v1 @ X4 ) )
| ( $false
= ( mrel @ X2 @ X4 ) ) )
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f1156]) ).
thf(f1159,definition,
( spl2_18
<=> ( $true
= ( v3 @ mactual ) ) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
thf(f1161,plain,
( ( $true
= ( v3 @ mactual ) )
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f1159]) ).
thf(f1171,plain,
( spl2_17
| spl2_3
| spl2_12
| spl2_9 ),
inference(avatar_split_clause,[],[f456,f1126,f1136,f1102,f1156]) ).
thf(f1177,plain,
( spl2_6
| spl2_4
| spl2_18
| spl2_9 ),
inference(avatar_split_clause,[],[f504,f1126,f1159,f1106,f1114]) ).
thf(f1181,definition,
( spl2_22
<=> ! [X1: mworld] :
( ( ( v3 @ X1 )
= $false )
| ( ( mrel @ mactual @ X1 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
thf(f1182,plain,
( ! [X1: mworld] :
( ( ( mrel @ mactual @ X1 )
= $false )
| ( ( v3 @ X1 )
= $false ) )
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f1181]) ).
thf(f1202,plain,
( spl2_7
| spl2_1
| spl2_3
| spl2_10 ),
inference(avatar_split_clause,[],[f752,f1129,f1102,f1096,f1118]) ).
thf(f1212,plain,
( spl2_6
| spl2_10
| spl2_15
| spl2_3 ),
inference(avatar_split_clause,[],[f907,f1102,f1148,f1129,f1114]) ).
thf(f1219,plain,
( spl2_14
| spl2_9
| spl2_3
| spl2_22 ),
inference(avatar_split_clause,[],[f1018,f1181,f1102,f1126,f1143]) ).
thf(f1220,plain,
( spl2_4
| spl2_18
| spl2_10
| spl2_5 ),
inference(avatar_split_clause,[],[f1034,f1110,f1129,f1159,f1106]) ).
thf(f1222,plain,
( spl2_10
| spl2_14
| spl2_1
| spl2_9 ),
inference(avatar_split_clause,[],[f1066,f1126,f1096,f1143,f1129]) ).
thf(f1243,plain,
( ( $true = $false )
| ~ spl2_5
| ~ spl2_12 ),
inference(forward_demodulation,[],[f1138,f1112]) ).
thf(f1244,plain,
( $false
| ~ spl2_5
| ~ spl2_12 ),
inference(trivial_inequality_removal,[],[f1243]) ).
thf(f1245,plain,
( ~ spl2_5
| ~ spl2_12 ),
inference(avatar_contradiction_clause,[],[f1244]) ).
thf(f1248,plain,
( ( $true = $false )
| ~ spl2_6
| ~ spl2_14 ),
inference(forward_demodulation,[],[f1145,f1116]) ).
thf(f1249,plain,
( $false
| ~ spl2_6
| ~ spl2_14 ),
inference(trivial_inequality_removal,[],[f1248]) ).
thf(f1250,plain,
( ~ spl2_6
| ~ spl2_14 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
thf(f1251,plain,
( ( $true = $false )
| ~ spl2_8
| ~ spl2_15 ),
inference(forward_demodulation,[],[f1150,f1123]) ).
thf(f1252,plain,
( $false
| ~ spl2_8
| ~ spl2_15 ),
inference(trivial_inequality_removal,[],[f1251]) ).
thf(f1253,plain,
( ~ spl2_8
| ~ spl2_15 ),
inference(avatar_contradiction_clause,[],[f1252]) ).
thf(f1261,plain,
( ( $true = $false )
| ( ( v1 @ mactual )
= $false )
| ~ spl2_13 ),
inference(constrained_superposition,[],[f1141,f247]) ).
thf(f1267,plain,
( ( ( v1 @ mactual )
= $false )
| ~ spl2_13 ),
inference(trivial_inequality_removal,[],[f1261]) ).
thf(f1276,plain,
( ! [X0: mworld] :
( ( $false
= ( mrel @ mactual @ X0 ) )
| ( $true
= ( v3 @ X0 ) )
| ( $true = $false ) )
| ~ spl2_4 ),
inference(constrained_superposition,[],[f247,f1107]) ).
thf(f1278,plain,
( ( $false != $false )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ( $true
= ( v3 @ mactual ) )
| ~ spl2_4 ),
inference(equality_factoring,[],[f1107]) ).
thf(f1279,plain,
( ! [X0: mworld] :
( ( $true
= ( v3 @ X0 ) )
| ( $false
= ( mrel @ mactual @ X0 ) ) )
| ~ spl2_4 ),
inference(trivial_inequality_removal,[],[f1276]) ).
thf(f1284,plain,
( ( $true
= ( v3 @ mactual ) )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ~ spl2_4 ),
inference(trivial_inequality_removal,[],[f1278]) ).
thf(f1285,plain,
( spl2_2
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f1279,f1106,f1099]) ).
thf(f1290,plain,
( ( $false
= ( mrel @ mactual @ mactual ) )
| ( $true = $false )
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_demodulation,[],[f1284,f1104]) ).
thf(f1291,plain,
( ( $false
= ( mrel @ mactual @ mactual ) )
| ~ spl2_3
| ~ spl2_4 ),
inference(trivial_inequality_removal,[],[f1290]) ).
thf(f1292,plain,
( ( $true = $false )
| ~ spl2_3
| ~ spl2_4 ),
inference(forward_demodulation,[],[f1291,f247]) ).
thf(f1293,plain,
( $false
| ~ spl2_3
| ~ spl2_4 ),
inference(trivial_inequality_removal,[],[f1292]) ).
thf(f1294,plain,
( ~ spl2_3
| ~ spl2_4 ),
inference(avatar_contradiction_clause,[],[f1293]) ).
thf(f1299,plain,
( ( $true = $false )
| ( $true
= ( v3 @ mactual ) )
| ~ spl2_2 ),
inference(constrained_superposition,[],[f1100,f247]) ).
thf(f1304,plain,
( ( $true
= ( v3 @ mactual ) )
| ~ spl2_2 ),
inference(trivial_inequality_removal,[],[f1299]) ).
thf(f1309,plain,
( spl2_18
| ~ spl2_2 ),
inference(avatar_split_clause,[],[f1304,f1099,f1159]) ).
thf(f1327,plain,
( ( $true
= ( v4 @ mactual ) )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ( $false != $false )
| ~ spl2_9 ),
inference(equality_factoring,[],[f1127]) ).
thf(f1331,plain,
( ( $true
= ( v4 @ mactual ) )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ~ spl2_9 ),
inference(trivial_inequality_removal,[],[f1327]) ).
thf(f1340,plain,
( ! [X0: mworld] :
( ( $true = $false )
| ( $false
= ( v4 @ X0 ) )
| ( $false
= ( mrel @ mactual @ X0 ) ) )
| ~ spl2_10 ),
inference(constrained_superposition,[],[f1130,f247]) ).
thf(f1346,plain,
( ! [X0: mworld] :
( ( $false
= ( mrel @ mactual @ X0 ) )
| ( $false
= ( v4 @ X0 ) ) )
| ~ spl2_10 ),
inference(trivial_inequality_removal,[],[f1340]) ).
thf(f1352,plain,
( spl2_1
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f1346,f1129,f1096]) ).
thf(f1370,plain,
( ( $true = $false )
| ( $true
= ( v4 @ mactual ) )
| ~ spl2_9 ),
inference(forward_demodulation,[],[f1331,f247]) ).
thf(f1371,plain,
( ( $true
= ( v4 @ mactual ) )
| ~ spl2_9 ),
inference(trivial_inequality_removal,[],[f1370]) ).
thf(f1373,plain,
( spl2_12
| ~ spl2_9 ),
inference(avatar_split_clause,[],[f1371,f1126,f1136]) ).
thf(f1374,plain,
( spl2_14
| ~ spl2_13 ),
inference(avatar_split_clause,[],[f1267,f1140,f1143]) ).
thf(f1375,plain,
( ( $true = $false )
| ~ spl2_3
| ~ spl2_18 ),
inference(forward_demodulation,[],[f1161,f1104]) ).
thf(f1376,plain,
( $false
| ~ spl2_3
| ~ spl2_18 ),
inference(trivial_inequality_removal,[],[f1375]) ).
thf(f1377,plain,
( ~ spl2_3
| ~ spl2_18 ),
inference(avatar_contradiction_clause,[],[f1376]) ).
thf(f1393,plain,
( ( $false
= ( v4 @ mactual ) )
| ( $true = $false )
| ~ spl2_1 ),
inference(constrained_superposition,[],[f247,f1097]) ).
thf(f1396,plain,
( ( $false
= ( v4 @ mactual ) )
| ~ spl2_1 ),
inference(trivial_inequality_removal,[],[f1393]) ).
thf(f1402,plain,
( ( $true = $false )
| ( $false
= ( v3 @ mactual ) )
| ~ spl2_22 ),
inference(constrained_superposition,[],[f1182,f247]) ).
thf(f1409,plain,
( ( $false
= ( v3 @ mactual ) )
| ~ spl2_22 ),
inference(trivial_inequality_removal,[],[f1402]) ).
thf(f1414,plain,
( $false
| spl2_3
| ~ spl2_22 ),
inference(forward_subsumption_resolution,[],[f1409,f1103]) ).
thf(f1415,plain,
( spl2_3
| ~ spl2_22 ),
inference(avatar_contradiction_clause,[],[f1414]) ).
thf(f1422,plain,
( ! [X0: mworld] :
( ( $false
= ( mrel @ mactual @ X0 ) )
| ( $true = $false )
| ( ( v2 @ X0 )
= $false ) )
| ~ spl2_7 ),
inference(constrained_superposition,[],[f247,f1119]) ).
thf(f1429,plain,
( ! [X0: mworld] :
( ( ( v2 @ X0 )
= $false )
| ( $false
= ( mrel @ mactual @ X0 ) ) )
| ~ spl2_7 ),
inference(trivial_inequality_removal,[],[f1422]) ).
thf(f1431,plain,
( spl2_11
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f1429,f1118,f1132]) ).
thf(f1435,plain,
( ( $false
= ( v2 @ mactual ) )
| ( $true = $false )
| ~ spl2_11 ),
inference(constrained_superposition,[],[f247,f1133]) ).
thf(f1437,plain,
( ( $false
= ( v2 @ mactual ) )
| ~ spl2_11 ),
inference(trivial_inequality_removal,[],[f1435]) ).
thf(f1467,plain,
( ( $false != $false )
| ( ( v1 @ mactual )
= $false )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ~ spl2_16 ),
inference(equality_factoring,[],[f1153]) ).
thf(f1468,plain,
( ( $false
= ( mrel @ mactual @ mactual ) )
| ( ( v1 @ mactual )
= $false )
| ~ spl2_16 ),
inference(trivial_inequality_removal,[],[f1467]) ).
thf(f1485,plain,
( ( $false != $false )
| ( $true
= ( v1 @ mactual ) )
| ( $false
= ( mrel @ mactual @ mactual ) )
| ~ spl2_17 ),
inference(equality_factoring,[],[f1157]) ).
thf(f1487,plain,
( ( $false
= ( mrel @ mactual @ mactual ) )
| ( $true
= ( v1 @ mactual ) )
| ~ spl2_17 ),
inference(trivial_inequality_removal,[],[f1485]) ).
thf(f1492,plain,
( ( $false
= ( mrel @ mactual @ mactual ) )
| spl2_6
| ~ spl2_17 ),
inference(forward_subsumption_resolution,[],[f1487,f1115]) ).
thf(f1494,plain,
( ( $true = $false )
| spl2_6
| ~ spl2_17 ),
inference(forward_demodulation,[],[f1492,f247]) ).
thf(f1495,plain,
( $false
| spl2_6
| ~ spl2_17 ),
inference(trivial_inequality_removal,[],[f1494]) ).
thf(f1496,plain,
( spl2_6
| ~ spl2_17 ),
inference(avatar_contradiction_clause,[],[f1495]) ).
thf(f1497,plain,
( spl2_8
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f1437,f1132,f1121]) ).
thf(f1499,plain,
( spl2_5
| ~ spl2_1 ),
inference(avatar_split_clause,[],[f1396,f1096,f1110]) ).
thf(f1500,plain,
( ( $true = $false )
| ( ( v1 @ mactual )
= $false )
| ~ spl2_16 ),
inference(forward_demodulation,[],[f1468,f247]) ).
thf(f1501,plain,
( ( ( v1 @ mactual )
= $false )
| ~ spl2_16 ),
inference(trivial_inequality_removal,[],[f1500]) ).
thf(f1502,plain,
( spl2_14
| ~ spl2_16 ),
inference(avatar_split_clause,[],[f1501,f1152,f1143]) ).
cnf(s1,plain,
( spl2_1
| spl2_2
| spl2_3
| spl2_4 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s4,plain,
( spl2_4
| spl2_12
| spl2_13
| spl2_14 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s5,plain,
( spl2_3
| spl2_13
| spl2_15
| spl2_16 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s9,plain,
( spl2_3
| spl2_9
| spl2_12
| spl2_17 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s12,plain,
( spl2_4
| spl2_6
| spl2_9
| spl2_18 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s28,plain,
( spl2_1
| spl2_3
| spl2_7
| spl2_10 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s38,plain,
( spl2_3
| spl2_6
| spl2_10
| spl2_15 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s45,plain,
( spl2_3
| spl2_9
| spl2_14
| spl2_22 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s46,plain,
( spl2_4
| spl2_5
| spl2_10
| spl2_18 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s48,plain,
( spl2_1
| spl2_9
| spl2_10
| spl2_14 ),
inference(sat_conversion,[],[f1222]) ).
cnf(s51,plain,
( ~ spl2_5
| ~ spl2_12 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s52,plain,
( ~ spl2_6
| ~ spl2_14 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s53,plain,
( ~ spl2_8
| ~ spl2_15 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s55,plain,
( spl2_2
| ~ spl2_4 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s57,plain,
( ~ spl2_3
| ~ spl2_4 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s59,plain,
( ~ spl2_2
| spl2_18 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s61,plain,
( spl2_1
| ~ spl2_10 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s69,plain,
( ~ spl2_9
| spl2_12 ),
inference(sat_conversion,[],[f1373]) ).
cnf(s70,plain,
( ~ spl2_13
| spl2_14 ),
inference(sat_conversion,[],[f1374]) ).
cnf(s72,plain,
( ~ spl2_3
| ~ spl2_18 ),
inference(sat_conversion,[],[f1377]) ).
cnf(s75,plain,
( spl2_3
| ~ spl2_22 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s76,plain,
( ~ spl2_7
| spl2_11 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s80,plain,
( spl2_6
| ~ spl2_17 ),
inference(sat_conversion,[],[f1496]) ).
cnf(s81,plain,
( spl2_8
| ~ spl2_11 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s85,plain,
( ~ spl2_1
| spl2_5 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s87,plain,
( spl2_14
| ~ spl2_16 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s88,plain,
( spl2_2
| spl2_1 ),
inference(rat,[],[s52,s12,s48,s69,s51,s46,s72,s1,s55,s61]) ).
cnf(s89,plain,
( spl2_15
| spl2_3
| spl2_10 ),
inference(rat,[],[s5,s70,s87,s52,s38]) ).
cnf(s90,plain,
( spl2_3
| spl2_10
| spl2_1 ),
inference(rat,[],[s89,s53,s81,s76,s28]) ).
cnf(s91,plain,
spl2_1,
inference(rat,[],[s90,s72,s59,s88,s61]) ).
cnf(s92,plain,
spl2_5,
inference(rat,[],[s85,s91]) ).
cnf(s93,plain,
~ spl2_12,
inference(rat,[],[s51,s92]) ).
cnf(s94,plain,
~ spl2_9,
inference(rat,[],[s69,s93]) ).
cnf(s95,plain,
( spl2_4
| spl2_18 ),
inference(rat,[],[s4,s70,s52,s12,s94,s93]) ).
cnf(s96,plain,
~ spl2_3,
inference(rat,[],[s95,s57,s72]) ).
cnf(s97,plain,
~ spl2_22,
inference(rat,[],[s75,s96]) ).
cnf(s98,plain,
spl2_17,
inference(rat,[],[s9,s94,s93,s96]) ).
cnf(s99,plain,
spl2_14,
inference(rat,[],[s45,s97,s94,s96]) ).
cnf(s100,plain,
spl2_6,
inference(rat,[],[s80,s98]) ).
cnf(s102,plain,
$false,
inference(rat,[],[s52,s99,s100]) ).
thf(f1503,plain,
$false,
inference(avatar_sat_refutation,[],[s102]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO903^10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n014.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 17:26:30 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.35 % (2960865)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.35 % (2960875)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=613774665:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.35 % (2960876)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.35 % (2960876)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.35 % (2960871)lrs+10_16_si=on:nwc=1.5:random_seed=3375154015:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.35 % (2960870)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3774060523:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.35 % (2960872)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2974524088:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.35 % (2960874)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2571941253:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.35 % (2960873)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=4018455057:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.35 % (2960876)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3515156892:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.35 % (2960872)Instruction limit reached!
% 0.21/0.35 % (2960872)------------------------------
% 0.21/0.35 % (2960872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960872)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960872)Termination reason: Instruction limit
% 0.21/0.35 % (2960872)Termination phase: shuffling
% 0.21/0.35 % (2960872)Time elapsed: 0.003 s
% 0.21/0.35 % (2960872)Peak memory usage: 9 MB
% 0.21/0.35 % (2960872)Instructions burned: 9 (million)
% 0.21/0.35 % (2960871)Instruction limit reached!
% 0.21/0.35 % (2960871)------------------------------
% 0.21/0.35 % (2960871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960871)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960871)Termination reason: Instruction limit
% 0.21/0.35 % (2960871)Termination phase: Function definition elimination
% 0.21/0.35 % (2960871)Time elapsed: 0.008 s
% 0.21/0.35 % (2960871)Peak memory usage: 10 MB
% 0.21/0.35 % (2960871)Instructions burned: 20 (million)
% 0.21/0.35 % (2960875)Instruction limit reached!
% 0.21/0.35 % (2960875)------------------------------
% 0.21/0.35 % (2960875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960875)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960875)Termination reason: Instruction limit
% 0.21/0.35 % (2960875)Termination phase: Saturation
% 0.21/0.35 % (2960875)Time elapsed: 0.017 s
% 0.21/0.35 % (2960875)Peak memory usage: 12 MB
% 0.21/0.35 % (2960875)Instructions burned: 79 (million)
% 0.21/0.35 % (2960874)Instruction limit reached!
% 0.21/0.35 % (2960874)------------------------------
% 0.21/0.35 % (2960874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960874)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960874)Termination reason: Instruction limit
% 0.21/0.35 % (2960874)Termination phase: Saturation
% 0.21/0.35 % (2960874)Time elapsed: 0.010 s
% 0.21/0.35 % (2960874)Peak memory usage: 11 MB
% 0.21/0.35 % (2960874)Instructions burned: 24 (million)
% 0.21/0.35 % (2960886)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.35 % (2960886)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=910442543:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.35 % (2960886)Instruction limit reached!
% 0.21/0.35 % (2960886)------------------------------
% 0.21/0.35 % (2960886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960886)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960886)Termination reason: Instruction limit
% 0.21/0.35 % (2960886)Termination phase: Property scanning
% 0.21/0.35 % (2960886)Time elapsed: 0.001 s
% 0.21/0.35 % (2960886)Peak memory usage: 9 MB
% 0.21/0.35 % (2960886)Instructions burned: 7 (million)
% 0.21/0.35 % (2960884)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=678011846:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.35 % (2960884)Instruction limit reached!
% 0.21/0.35 % (2960884)------------------------------
% 0.21/0.35 % (2960884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960884)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960884)Termination reason: Instruction limit
% 0.21/0.35 % (2960884)Termination phase: shuffling
% 0.21/0.35 % (2960884)Time elapsed: 0.001 s
% 0.21/0.35 % (2960884)Peak memory usage: 9 MB
% 0.21/0.35 % (2960884)Instructions burned: 2 (million)
% 0.21/0.35 % (2960887)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3307318140:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.21/0.35 % (2960885)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=4194561279:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.35 % (2960885)Instruction limit reached!
% 0.21/0.35 % (2960885)------------------------------
% 0.21/0.35 % (2960885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960885)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960885)Termination reason: Instruction limit
% 0.21/0.35 % (2960885)Termination phase: Property scanning
% 0.21/0.35 % (2960885)Time elapsed: 0.003 s
% 0.21/0.35 % (2960885)Peak memory usage: 10 MB
% 0.21/0.35 % (2960885)Instructions burned: 9 (million)
% 0.21/0.35 % (2960887)Instruction limit reached!
% 0.21/0.35 % (2960887)------------------------------
% 0.21/0.35 % (2960887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960887)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960887)Termination reason: Instruction limit
% 0.21/0.35 % (2960887)Termination phase: Property scanning
% 0.21/0.35 % (2960887)Time elapsed: 0.005 s
% 0.21/0.35 % (2960887)Peak memory usage: 10 MB
% 0.21/0.35 % (2960887)Instructions burned: 12 (million)
% 0.21/0.35 % (2960889)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.35 % (2960889)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.35 % (2960889)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=402865280:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.21/0.35 % (2960870)Instruction limit reached!
% 0.21/0.35 % (2960870)------------------------------
% 0.21/0.35 % (2960870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960870)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960870)Termination reason: Instruction limit
% 0.21/0.35 % (2960870)Termination phase: Saturation
% 0.21/0.35 % (2960870)Time elapsed: 0.038 s
% 0.21/0.35 % (2960870)Peak memory usage: 12 MB
% 0.21/0.35 % (2960870)Instructions burned: 89 (million)
% 0.21/0.35 % (2960876) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2960865-2960876"...
% 0.21/0.35 % (2960889)Instruction limit reached!
% 0.21/0.35 % (2960889)------------------------------
% 0.21/0.35 % (2960889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960889)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960889)Termination reason: Instruction limit
% 0.21/0.35 % (2960889)Termination phase: Property scanning
% 0.21/0.35 % (2960889)Time elapsed: 0.006 s
% 0.21/0.35 % (2960889)Peak memory usage: 10 MB
% 0.21/0.35 % (2960889)Instructions burned: 32 (million)
% 0.21/0.35 % (2960895)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.21/0.35 % (2960894)lrs+10_1_si=on:cs=on:random_seed=2260393257:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.21/0.35 % (2960895)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=833775927:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.35 % (2960898)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=597756863:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.21/0.35 % (2960876)...printing done.
% 0.21/0.35 % (2960894)Instruction limit reached!
% 0.21/0.35 % (2960894)------------------------------
% 0.21/0.35 % (2960894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960895)Instruction limit reached!
% 0.21/0.35 % (2960895)------------------------------
% 0.21/0.35 % (2960895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960894)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960894)Termination reason: Instruction limit
% 0.21/0.35 % (2960894)Termination phase: shuffling
% 0.21/0.35 % (2960894)Time elapsed: 0.003 s
% 0.21/0.35 % (2960895)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960894)Peak memory usage: 9 MB
% 0.21/0.35 % (2960895)Termination reason: Instruction limit
% 0.21/0.35 % (2960895)Termination phase: Property scanning
% 0.21/0.35 % (2960895)Time elapsed: 0.002 s
% 0.21/0.35 % (2960895)Peak memory usage: 9 MB
% 0.21/0.35 % (2960894)Instructions burned: 8 (million)
% 0.21/0.35 % (2960895)Instructions burned: 5 (million)
% 0.21/0.35 % (2960876)Refutation found. Thanks to Tanya!
% 0.21/0.35 % SZS status ContradictoryAxioms for theBenchmark
% 0.21/0.35 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.35 % (2960876)------------------------------
% 0.21/0.35 % (2960876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2960876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2960876)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2960876)Termination reason: Refutation
% 0.21/0.35 % (2960876)Time elapsed: 0.053 s
% 0.21/0.35 % (2960876)Peak memory usage: 14 MB
% 0.21/0.35 % (2960876)Instructions burned: 121 (million)
% 0.21/0.35 % (2960865)Success in time 0.1 s
% 0.21/0.35 % Vampire exiting
%------------------------------------------------------------------------------