%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN045^4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:41:49 AM UTC 2026
% Result : Theorem 1.06s 0.49s
% Output : Refutation 1.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 52
% Syntax : Number of formulae : 543 ( 69 unt; 0 typ; 40 def)
% Number of atoms : 5451 ( 842 equ; 0 cnn)
% Maximal formula atoms : 21 ( 10 avg)
% Number of connectives : 5877 ( 387 ~;1170 |; 114 &;3348 @)
% ( 40 <=>; 492 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 167 ( 167 >; 0 *; 0 +; 0 <<)
% Number of symbols : 95 ( 91 usr; 60 con; 0-4 aty)
% ( 326 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 809 ( 0 sgn 181 !; 0 ?; 809 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
irel: $i > $i > $o ).
thf(func_def_2,type,
mnot: ( $i > $o ) > $i > $o ).
thf(func_def_3,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_4,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_5,type,
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_6,type,
mbox_s4: ( $i > $o ) > $i > $o ).
thf(func_def_7,type,
iatom: ( $i > $o ) > $i > $o ).
thf(func_def_8,type,
inot: ( $i > $o ) > $i > $o ).
thf(func_def_9,type,
itrue: $i > $o ).
thf(func_def_10,type,
ifalse: $i > $o ).
thf(func_def_11,type,
iand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_12,type,
ior: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_13,type,
iimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_14,type,
iimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_15,type,
iequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_16,type,
ixor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_17,type,
ivalid: ( $i > $o ) > $o ).
thf(func_def_18,type,
isatisfiable: ( $i > $o ) > $o ).
thf(func_def_19,type,
icountersatisfiable: ( $i > $o ) > $o ).
thf(func_def_20,type,
iinvalid: ( $i > $o ) > $o ).
thf(func_def_21,type,
p: $i > $o ).
thf(func_def_22,type,
q: $i > $o ).
thf(func_def_23,type,
r: $i > $o ).
thf(func_def_26,type,
vNOT: $o > $o ).
thf(func_def_27,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_28,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_29,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_30,type,
vOR: $o > $o > $o ).
thf(func_def_31,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_32,type,
vAND: $o > $o > $o ).
thf(func_def_33,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_34,type,
vIMP: $o > $o > $o ).
thf(func_def_35,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(f3,axiom,
( mnot
= ( ^ [X0: $i > $o,X1: $i] :
~ ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mnot) ).
thf(f4,axiom,
( mor
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
| ( X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mor) ).
thf(f5,axiom,
( mand
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
& ( X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mand) ).
thf(f6,axiom,
( mimplies
= ( ^ [X0: $i > $o,X1: $i > $o] : ( mor @ ( mnot @ X0 ) @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mimplies) ).
thf(f7,axiom,
( mbox_s4
= ( ^ [X0: $i > $o,X1: $i] :
! [X2: $i] :
( ( irel @ X1 @ X2 )
=> ( X0 @ X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',mbox_s4) ).
thf(f8,axiom,
( iatom
= ( ^ [X0: $i > $o] : X0 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iatom) ).
thf(f12,axiom,
( iand
= ( ^ [X0: $i > $o,X1: $i > $o] : ( mand @ X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iand) ).
thf(f13,axiom,
( ior
= ( ^ [X0: $i > $o,X1: $i > $o] : ( mor @ ( mbox_s4 @ X0 ) @ ( mbox_s4 @ X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',ior) ).
thf(f14,axiom,
( iimplies
= ( ^ [X0: $i > $o,X1: $i > $o] : ( mimplies @ ( mbox_s4 @ X0 ) @ ( mbox_s4 @ X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iimplies) ).
thf(f16,axiom,
( iequiv
= ( ^ [X0: $i > $o,X1: $i > $o] : ( iand @ ( iimplies @ X0 @ X1 ) @ ( iimplies @ X1 @ X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',iequiv) ).
thf(f18,axiom,
( ivalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL010^0.ax',ivalid) ).
thf(f22,conjecture,
ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel13) ).
thf(f23,negated_conjecture,
~ ( ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f22]) ).
thf(f28,plain,
( mnot
= ( ^ [X0: $i > $o,X1: $i] :
~ ( X0 @ X1 ) ) ),
inference(rectify,[],[f3]) ).
thf(f29,plain,
( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) ),
inference(fool_elimination,[],[f28]) ).
thf(f30,plain,
( mor
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
| ( X0 @ X2 ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f31,plain,
( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
| ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f30]) ).
thf(f32,plain,
( mand
= ( ^ [X0: $i > $o,X1: $i > $o,X2: $i] :
( ( X1 @ X2 )
& ( X0 @ X2 ) ) ) ),
inference(rectify,[],[f5]) ).
thf(f33,plain,
( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) ) ) ),
inference(fool_elimination,[],[f32]) ).
thf(f34,plain,
( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mnot @ Y0 ) @ Y1 ) ) ),
inference(fool_elimination,[],[f6]) ).
thf(f35,plain,
( mbox_s4
= ( ^ [X0: $i > $o,X1: $i] :
! [X2: $i] :
( ( irel @ X1 @ X2 )
=> ( X0 @ X2 ) ) ) ),
inference(rectify,[],[f7]) ).
thf(f36,plain,
( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(fool_elimination,[],[f35]) ).
thf(f37,plain,
( iatom
= ( ^ [Y0: $i > $o] : Y0 ) ),
inference(fool_elimination,[],[f8]) ).
thf(f40,plain,
( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mand @ Y0 @ Y1 ) ) ),
inference(fool_elimination,[],[f12]) ).
thf(f41,plain,
( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f13]) ).
thf(f42,plain,
( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mimplies @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f14]) ).
thf(f44,plain,
( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( iand @ ( iimplies @ Y0 @ Y1 ) @ ( iimplies @ Y1 @ Y0 ) ) ) ),
inference(fool_elimination,[],[f16]) ).
thf(f46,plain,
( ivalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
inference(rectify,[],[f18]) ).
thf(f47,plain,
( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f46]) ).
thf(f54,plain,
~ ( ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ) ),
inference(rectify,[],[f23]) ).
thf(f55,plain,
( ( ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ) )
!= $true ),
inference(fool_elimination,[],[f54]) ).
thf(f56,plain,
( ( ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ) )
!= $true ),
inference(flattening,[],[f55]) ).
thf(f61,plain,
( mnot
= ( ^ [Y0: $i > $o,Y1: $i] :
~ ( Y0 @ Y1 ) ) ),
inference(cnf_transformation,[],[f29]) ).
thf(f62,plain,
( mor
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
| ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f31]) ).
thf(f63,plain,
( mand
= ( ^ [Y0: $i > $o,Y1: $i > $o,Y2: $i] :
( ( Y0 @ Y2 )
& ( Y1 @ Y2 ) ) ) ),
inference(cnf_transformation,[],[f33]) ).
thf(f64,plain,
( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mnot @ Y0 ) @ Y1 ) ) ),
inference(cnf_transformation,[],[f34]) ).
thf(f65,plain,
( mbox_s4
= ( ^ [Y0: $i > $o,Y1: $i] :
( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( Y0 @ Y2 ) ) ) ) ),
inference(cnf_transformation,[],[f36]) ).
thf(f66,plain,
( iatom
= ( ^ [Y0: $i > $o] : Y0 ) ),
inference(cnf_transformation,[],[f37]) ).
thf(f70,plain,
( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mand @ Y0 @ Y1 ) ) ),
inference(cnf_transformation,[],[f40]) ).
thf(f71,plain,
( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mor @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f41]) ).
thf(f72,plain,
( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( mimplies @ ( mbox_s4 @ Y0 ) @ ( mbox_s4 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f42]) ).
thf(f74,plain,
( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o] : ( iand @ ( iimplies @ Y0 @ Y1 ) @ ( iimplies @ Y1 @ Y0 ) ) ) ),
inference(cnf_transformation,[],[f44]) ).
thf(f76,plain,
( ivalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f47]) ).
thf(f80,plain,
( ( ivalid @ ( iequiv @ ( ior @ ( iatom @ p ) @ ( iand @ ( iatom @ q ) @ ( iatom @ r ) ) ) @ ( iand @ ( ior @ ( iatom @ p ) @ ( iatom @ q ) ) @ ( ior @ ( iatom @ p ) @ ( iatom @ r ) ) ) ) )
!= $true ),
inference(cnf_transformation,[],[f56]) ).
thf(f83,plain,
( mimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
~ ( Y2 @ Y3 )
@ Y0 )
@ Y1 ) ) ),
inference(definition_unfolding,[],[f64,f62,f61]) ).
thf(f86,plain,
( iand
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
& ( Y3 @ Y4 ) )
@ Y0
@ Y1 ) ) ),
inference(definition_unfolding,[],[f70,f63]) ).
thf(f87,plain,
( ior
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y1 ) ) ) ),
inference(definition_unfolding,[],[f71,f62,f65,f65]) ).
thf(f88,plain,
( iimplies
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o,Y6: $i] :
( ( Y4 @ Y6 )
| ( Y5 @ Y6 ) )
@ ( ^ [Y4: $i > $o,Y5: $i] :
~ ( Y4 @ Y5 )
@ Y2 )
@ Y3 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y1 ) ) ) ),
inference(definition_unfolding,[],[f72,f83,f65,f65]) ).
thf(f90,plain,
( iequiv
= ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o,Y6: $i] :
( ( Y4 @ Y6 )
& ( Y5 @ Y6 ) )
@ Y2
@ Y3 )
@ ( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o] :
( ^ [Y6: $i > $o,Y7: $i > $o,Y8: $i] :
( ( Y6 @ Y8 )
| ( Y7 @ Y8 ) )
@ ( ^ [Y6: $i > $o,Y7: $i] :
~ ( Y6 @ Y7 )
@ Y4 )
@ Y5 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y2 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y3 ) )
@ Y0
@ Y1 )
@ ( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o] :
( ^ [Y6: $i > $o,Y7: $i > $o,Y8: $i] :
( ( Y6 @ Y8 )
| ( Y7 @ Y8 ) )
@ ( ^ [Y6: $i > $o,Y7: $i] :
~ ( Y6 @ Y7 )
@ Y4 )
@ Y5 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y2 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y3 ) )
@ Y1
@ Y0 ) ) ) ),
inference(definition_unfolding,[],[f74,f86,f88,f88]) ).
thf(f92,plain,
( $true
!= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o,Y6: $i] :
( ( Y4 @ Y6 )
& ( Y5 @ Y6 ) )
@ Y2
@ Y3 )
@ ( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o] :
( ^ [Y6: $i > $o,Y7: $i > $o,Y8: $i] :
( ( Y6 @ Y8 )
| ( Y7 @ Y8 ) )
@ ( ^ [Y6: $i > $o,Y7: $i] :
~ ( Y6 @ Y7 )
@ Y4 )
@ Y5 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y2 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y3 ) )
@ Y0
@ Y1 )
@ ( ^ [Y2: $i > $o,Y3: $i > $o] :
( ^ [Y4: $i > $o,Y5: $i > $o] :
( ^ [Y6: $i > $o,Y7: $i > $o,Y8: $i] :
( ( Y6 @ Y8 )
| ( Y7 @ Y8 ) )
@ ( ^ [Y6: $i > $o,Y7: $i] :
~ ( Y6 @ Y7 )
@ Y4 )
@ Y5 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y2 )
@ ( ^ [Y4: $i > $o,Y5: $i] :
( !! @ $i
@ ^ [Y6: $i] :
( ( irel @ Y5 @ Y6 )
=> ( Y4 @ Y6 ) ) )
@ Y3 ) )
@ Y1
@ Y0 ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y1 ) )
@ ( ^ [Y0: $i > $o] : Y0
@ p )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
& ( Y3 @ Y4 ) )
@ Y0
@ Y1 )
@ ( ^ [Y0: $i > $o] : Y0
@ q )
@ ( ^ [Y0: $i > $o] : Y0
@ r ) ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
& ( Y3 @ Y4 ) )
@ Y0
@ Y1 )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y1 ) )
@ ( ^ [Y0: $i > $o] : Y0
@ p )
@ ( ^ [Y0: $i > $o] : Y0
@ q ) )
@ ( ^ [Y0: $i > $o,Y1: $i > $o] :
( ^ [Y2: $i > $o,Y3: $i > $o,Y4: $i] :
( ( Y2 @ Y4 )
| ( Y3 @ Y4 ) )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y0 )
@ ( ^ [Y2: $i > $o,Y3: $i] :
( !! @ $i
@ ^ [Y4: $i] :
( ( irel @ Y3 @ Y4 )
=> ( Y2 @ Y4 ) ) )
@ Y1 ) )
@ ( ^ [Y0: $i > $o] : Y0
@ p )
@ ( ^ [Y0: $i > $o] : Y0
@ r ) ) ) ) ) ),
inference(definition_unfolding,[],[f80,f76,f90,f87,f66,f86,f66,f66,f86,f87,f66,f66,f87,f66,f66]) ).
thf(f93,plain,
( $true
!= ( !! @ $i
@ ^ [Y0: $i] :
( ( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( ( q @ Y2 )
& ( r @ Y2 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( q @ Y2 ) ) ) )
& ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( r @ Y2 ) ) ) ) ) ) ) )
& ( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( q @ Y2 ) ) ) )
& ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( r @ Y2 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( ( q @ Y2 )
& ( r @ Y2 ) ) ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f92]) ).
thf(f94,plain,
( $false
= ( ^ [Y0: $i] :
( ( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( ( q @ Y2 )
& ( r @ Y2 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( q @ Y2 ) ) ) )
& ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( r @ Y2 ) ) ) ) ) ) ) )
& ( ~ ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( q @ Y2 ) ) ) )
& ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( r @ Y2 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( p @ Y2 ) ) )
| ( !! @ $i
@ ^ [Y2: $i] :
( ( irel @ Y1 @ Y2 )
=> ( ( q @ Y2 )
& ( r @ Y2 ) ) ) ) ) ) ) ) )
@ sK0 ) ),
inference(sigma_proxy_clausification,[],[f93]) ).
thf(f95,plain,
( $false
= ( ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) )
& ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f94]) ).
thf(f96,plain,
( ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f95]) ).
thf(f97,plain,
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f96]) ).
thf(f98,plain,
( ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f96]) ).
thf(f99,plain,
( ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f98]) ).
thf(f100,plain,
! [X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) )
@ X1 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f99]) ).
thf(f102,plain,
! [X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) )
@ X1 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f100]) ).
thf(f103,plain,
! [X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) )
@ X1 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) ) ) ),
inference(not_proxy_clausification,[],[f102]) ).
thf(f104,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) )
@ X1 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) )
@ X2 ) ) ),
inference(pi_proxy_clausification,[],[f103]) ).
thf(f105,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ( irel @ sK0 @ X1 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) )
| ( $true
= ( ( irel @ sK0 @ X2 )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f104]) ).
thf(f106,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $true
= ( ( irel @ sK0 @ X2 )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) )
| ( $true
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f105]) ).
thf(f107,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f106]) ).
thf(f108,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) ) ) ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f107]) ).
thf(f109,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) ) ) ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f107]) ).
thf(f110,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) ) ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f109]) ).
thf(f111,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) )
@ X3 ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f110]) ).
thf(f112,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) )
@ X3 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f111]) ).
thf(f113,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f112]) ).
thf(f114,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) )
@ X5 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f113]) ).
thf(f115,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( q @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) )
@ X6 ) ) ),
inference(pi_proxy_clausification,[],[f114]) ).
thf(f116,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ( irel @ X1 @ X3 )
=> ( q @ X3 ) ) )
| ( $true
= ( ( irel @ X2 @ X4 )
=> ( ( q @ X4 )
& ( r @ X4 ) ) ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) ) ),
inference(beta-eta_normalization,[],[f115]) ).
thf(f117,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $true
= ( ( irel @ X2 @ X4 )
=> ( ( q @ X4 )
& ( r @ X4 ) ) ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( q @ X3 ) ) ),
inference(imp_proxy_clausification,[],[f116]) ).
thf(f118,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( q @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) ) ),
inference(imp_proxy_clausification,[],[f117]) ).
thf(f119,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( q @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) )
| ( $true
= ( p @ X5 ) ) ),
inference(imp_proxy_clausification,[],[f118]) ).
thf(f120,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $true
= ( q @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) )
| ( $true
= ( p @ X5 ) )
| ( $true
= ( p @ X6 ) ) ),
inference(imp_proxy_clausification,[],[f119]) ).
thf(f122,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $true
= ( q @ X3 ) )
| ( $true
= ( q @ X4 ) )
| ( $true
= ( p @ X5 ) )
| ( $true
= ( p @ X6 ) ) ),
inference(and_proxy_clausification,[],[f120]) ).
thf(f123,plain,
! [X2: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) ) ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f108]) ).
thf(f124,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) )
@ X3 ) )
| ( $true
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f123]) ).
thf(f125,plain,
! [X2: $i,X3: $i,X1: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) )
@ X3 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f124]) ).
thf(f126,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f125]) ).
thf(f127,plain,
! [X2: $i,X3: $i,X1: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) )
@ X5 ) )
| ( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(pi_proxy_clausification,[],[f126]) ).
thf(f128,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( r @ Y0 ) )
@ X3 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ X4 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X1 @ Y0 )
=> ( p @ Y0 ) )
@ X5 ) )
| ( $true
= ( ^ [Y0: $i] :
( ( irel @ X2 @ Y0 )
=> ( p @ Y0 ) )
@ X6 ) ) ),
inference(pi_proxy_clausification,[],[f127]) ).
thf(f129,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( ( irel @ X1 @ X3 )
=> ( r @ X3 ) ) )
| ( $true
= ( ( irel @ X2 @ X4 )
=> ( ( q @ X4 )
& ( r @ X4 ) ) ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) ) ),
inference(beta-eta_normalization,[],[f128]) ).
thf(f130,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $true
= ( ( irel @ X2 @ X4 )
=> ( ( q @ X4 )
& ( r @ X4 ) ) ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( r @ X3 ) ) ),
inference(imp_proxy_clausification,[],[f129]) ).
thf(f131,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $true
= ( ( irel @ X1 @ X5 )
=> ( p @ X5 ) ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( r @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) ) ),
inference(imp_proxy_clausification,[],[f130]) ).
thf(f132,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $true
= ( ( irel @ X2 @ X6 )
=> ( p @ X6 ) ) )
| ( $true
= ( r @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) )
| ( $true
= ( p @ X5 ) ) ),
inference(imp_proxy_clausification,[],[f131]) ).
thf(f133,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $true
= ( r @ X3 ) )
| ( $true
= ( ( q @ X4 )
& ( r @ X4 ) ) )
| ( $true
= ( p @ X5 ) )
| ( $true
= ( p @ X6 ) ) ),
inference(imp_proxy_clausification,[],[f132]) ).
thf(f134,plain,
! [X2: $i,X3: $i,X1: $i,X6: $i,X4: $i,X5: $i] :
( ( $false
= ( irel @ sK0 @ X1 ) )
| ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X1 @ X3 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $false
= ( irel @ X1 @ X5 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $true
= ( r @ X3 ) )
| ( $true
= ( r @ X4 ) )
| ( $true
= ( p @ X5 ) )
| ( $true
= ( p @ X6 ) ) ),
inference(and_proxy_clausification,[],[f133]) ).
thf(f300,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) )
@ sK12 ) )
| ( $false
= ( ~ ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f97]) ).
thf(f301,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) )
@ sK12 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f300]) ).
thf(f352,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( ( q @ Y1 )
& ( r @ Y1 ) ) ) ) ) )
@ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK0 @ Y0 )
=> ( ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( q @ Y1 ) ) ) )
& ( ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( p @ Y1 ) ) )
| ( !! @ $i
@ ^ [Y1: $i] :
( ( irel @ Y0 @ Y1 )
=> ( r @ Y1 ) ) ) ) ) )
@ sK15 ) ) ),
inference(sigma_proxy_clausification,[],[f301]) ).
thf(f353,plain,
( ( $false
= ( ( irel @ sK0 @ sK12 )
=> ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f352]) ).
thf(f354,plain,
( ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f353]) ).
thf(f355,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f353]) ).
thf(f356,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f355]) ).
thf(f357,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f355]) ).
thf(f358,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f356]) ).
thf(f359,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f358]) ).
thf(f360,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f358]) ).
thf(f361,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK16 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f360]) ).
thf(f363,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK16 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f361]) ).
thf(f364,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK16 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK17 ) ) ),
inference(sigma_proxy_clausification,[],[f363]) ).
thf(f365,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ( irel @ sK15 @ sK16 )
=> ( p @ sK16 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK17 )
=> ( p @ sK17 ) ) ) ),
inference(beta-eta_normalization,[],[f364]) ).
thf(f366,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( p @ sK16 ) )
| ( $false
= ( ( irel @ sK15 @ sK17 )
=> ( p @ sK17 ) ) ) ),
inference(imp_proxy_clausification,[],[f365]) ).
thf(f367,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK16 ) )
| ( $false
= ( ( irel @ sK15 @ sK17 )
=> ( p @ sK17 ) ) ) ),
inference(imp_proxy_clausification,[],[f365]) ).
thf(f368,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK16 ) )
| ( $false
= ( p @ sK17 ) ) ),
inference(imp_proxy_clausification,[],[f367]) ).
thf(f369,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK16 ) )
| ( $true
= ( irel @ sK15 @ sK17 ) ) ),
inference(imp_proxy_clausification,[],[f367]) ).
thf(f370,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( p @ sK16 ) )
| ( $false
= ( p @ sK17 ) ) ),
inference(imp_proxy_clausification,[],[f366]) ).
thf(f371,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( p @ sK16 ) )
| ( $true
= ( irel @ sK15 @ sK17 ) ) ),
inference(imp_proxy_clausification,[],[f366]) ).
thf(f380,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK19 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f359]) ).
thf(f381,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK19 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f380]) ).
thf(f391,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK19 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) )
@ sK21 ) ) ),
inference(sigma_proxy_clausification,[],[f381]) ).
thf(f392,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( ( irel @ sK15 @ sK19 )
=> ( r @ sK19 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK21 )
=> ( q @ sK21 ) ) ) ),
inference(beta-eta_normalization,[],[f391]) ).
thf(f393,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( r @ sK19 ) )
| ( $false
= ( ( irel @ sK15 @ sK21 )
=> ( q @ sK21 ) ) ) ),
inference(imp_proxy_clausification,[],[f392]) ).
thf(f394,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK19 ) )
| ( $false
= ( ( irel @ sK15 @ sK21 )
=> ( q @ sK21 ) ) ) ),
inference(imp_proxy_clausification,[],[f392]) ).
thf(f395,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK19 ) )
| ( $false
= ( q @ sK21 ) ) ),
inference(imp_proxy_clausification,[],[f394]) ).
thf(f396,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $true
= ( irel @ sK15 @ sK19 ) )
| ( $true
= ( irel @ sK15 @ sK21 ) ) ),
inference(imp_proxy_clausification,[],[f394]) ).
thf(f397,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( r @ sK19 ) )
| ( $false
= ( q @ sK21 ) ) ),
inference(imp_proxy_clausification,[],[f393]) ).
thf(f398,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( r @ sK19 ) )
| ( $true
= ( irel @ sK15 @ sK21 ) ) ),
inference(imp_proxy_clausification,[],[f393]) ).
thf(f399,plain,
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) ) ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f354]) ).
thf(f400,plain,
( ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f354]) ).
thf(f401,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f400]) ).
thf(f402,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f401]) ).
thf(f403,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f401]) ).
thf(f404,plain,
( ( $false
= ( ( irel @ sK12 @ sK22 )
=> ( p @ sK22 ) ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(beta-eta_normalization,[],[f403]) ).
thf(f405,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f404]) ).
thf(f406,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f404]) ).
thf(f407,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f402]) ).
thf(f408,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f407]) ).
thf(f409,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f407]) ).
thf(f410,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK23 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f409]) ).
thf(f412,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK23 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f410]) ).
thf(f413,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK23 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK24 ) ) ),
inference(sigma_proxy_clausification,[],[f412]) ).
thf(f414,plain,
( ( $false
= ( ( irel @ sK12 @ sK22 )
=> ( p @ sK22 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK23 )
=> ( p @ sK23 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(beta-eta_normalization,[],[f413]) ).
thf(f415,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( ( irel @ sK15 @ sK23 )
=> ( p @ sK23 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f414]) ).
thf(f416,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( ( irel @ sK15 @ sK23 )
=> ( p @ sK23 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f414]) ).
thf(f417,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f416]) ).
thf(f418,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f416]) ).
thf(f419,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $false
= ( p @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f418]) ).
thf(f420,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $true
= ( irel @ sK15 @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f418]) ).
thf(f421,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $false
= ( p @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f417]) ).
thf(f422,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $true
= ( irel @ sK15 @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f417]) ).
thf(f423,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f415]) ).
thf(f424,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $false
= ( ( irel @ sK15 @ sK24 )
=> ( p @ sK24 ) ) ) ),
inference(imp_proxy_clausification,[],[f415]) ).
thf(f425,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $false
= ( p @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f424]) ).
thf(f426,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK23 ) )
| ( $true
= ( irel @ sK15 @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f424]) ).
thf(f427,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $false
= ( p @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f423]) ).
thf(f428,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( p @ sK23 ) )
| ( $true
= ( irel @ sK15 @ sK24 ) ) ),
inference(imp_proxy_clausification,[],[f423]) ).
thf(f445,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK26 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f408]) ).
thf(f446,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK26 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f445]) ).
thf(f464,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( p @ Y0 ) )
@ sK22 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK26 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) )
@ sK28 ) ) ),
inference(sigma_proxy_clausification,[],[f446]) ).
thf(f465,plain,
( ( $false
= ( ( irel @ sK12 @ sK22 )
=> ( p @ sK22 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK26 )
=> ( r @ sK26 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(beta-eta_normalization,[],[f464]) ).
thf(f466,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( ( irel @ sK15 @ sK26 )
=> ( r @ sK26 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f465]) ).
thf(f467,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( ( irel @ sK15 @ sK26 )
=> ( r @ sK26 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f465]) ).
thf(f468,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f467]) ).
thf(f469,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f467]) ).
thf(f470,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $false
= ( q @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f469]) ).
thf(f471,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $true
= ( irel @ sK15 @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f469]) ).
thf(f472,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $false
= ( q @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f468]) ).
thf(f473,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $true
= ( irel @ sK15 @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f468]) ).
thf(f474,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f466]) ).
thf(f475,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $false
= ( ( irel @ sK15 @ sK28 )
=> ( q @ sK28 ) ) ) ),
inference(imp_proxy_clausification,[],[f466]) ).
thf(f476,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $false
= ( q @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f475]) ).
thf(f477,plain,
( ( $false
= ( p @ sK22 ) )
| ( $true
= ( irel @ sK15 @ sK26 ) )
| ( $true
= ( irel @ sK15 @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f475]) ).
thf(f478,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $false
= ( q @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f474]) ).
thf(f479,plain,
( ( $false
= ( p @ sK22 ) )
| ( $false
= ( r @ sK26 ) )
| ( $true
= ( irel @ sK15 @ sK28 ) ) ),
inference(imp_proxy_clausification,[],[f474]) ).
thf(f480,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ( irel @ sK0 @ sK15 )
=> ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f399]) ).
thf(f481,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) )
& ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f480]) ).
thf(f482,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f480]) ).
thf(f483,plain,
( ( $false
= ( ( irel @ sK12 @ sK29 )
=> ( ( q @ sK29 )
& ( r @ sK29 ) ) ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(beta-eta_normalization,[],[f482]) ).
thf(f484,plain,
( ( $false
= ( ( q @ sK29 )
& ( r @ sK29 ) ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f483]) ).
thf(f485,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) ) ),
inference(imp_proxy_clausification,[],[f483]) ).
thf(f486,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK0 @ sK15 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(and_proxy_clausification,[],[f484]) ).
thf(f487,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(and_proxy_clausification,[],[f481]) ).
thf(f488,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f487]) ).
thf(f489,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(or_proxy_clausification,[],[f487]) ).
thf(f490,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK30 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f489]) ).
thf(f492,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK30 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f490]) ).
thf(f493,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK30 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) )
@ sK31 ) ) ),
inference(sigma_proxy_clausification,[],[f492]) ).
thf(f494,plain,
( ( $false
= ( ( irel @ sK12 @ sK29 )
=> ( ( q @ sK29 )
& ( r @ sK29 ) ) ) )
| ( $false
= ( ( irel @ sK15 @ sK30 )
=> ( p @ sK30 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) ) ),
inference(beta-eta_normalization,[],[f493]) ).
thf(f495,plain,
( ( $false
= ( ( q @ sK29 )
& ( r @ sK29 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK30 )
=> ( p @ sK30 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) ) ),
inference(imp_proxy_clausification,[],[f494]) ).
thf(f496,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( ( irel @ sK15 @ sK30 )
=> ( p @ sK30 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) ) ),
inference(imp_proxy_clausification,[],[f494]) ).
thf(f497,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) ) ),
inference(imp_proxy_clausification,[],[f496]) ).
thf(f498,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) ) ),
inference(imp_proxy_clausification,[],[f496]) ).
thf(f499,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $false
= ( p @ sK31 ) ) ),
inference(imp_proxy_clausification,[],[f498]) ).
thf(f500,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $true
= ( irel @ sK15 @ sK31 ) ) ),
inference(imp_proxy_clausification,[],[f498]) ).
thf(f501,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $false
= ( p @ sK31 ) ) ),
inference(imp_proxy_clausification,[],[f497]) ).
thf(f502,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $true
= ( irel @ sK15 @ sK31 ) ) ),
inference(imp_proxy_clausification,[],[f497]) ).
thf(f503,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( ( irel @ sK15 @ sK30 )
=> ( p @ sK30 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(and_proxy_clausification,[],[f495]) ).
thf(f504,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f503]) ).
thf(f505,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $false
= ( ( irel @ sK15 @ sK31 )
=> ( p @ sK31 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f503]) ).
thf(f506,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $false
= ( p @ sK31 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f505]) ).
thf(f507,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK30 ) )
| ( $true
= ( irel @ sK15 @ sK31 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f505]) ).
thf(f508,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $false
= ( p @ sK31 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f504]) ).
thf(f509,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( p @ sK30 ) )
| ( $true
= ( irel @ sK15 @ sK31 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f504]) ).
thf(f527,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK33 ) )
| ( $false
= ( ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( p @ Y0 ) ) )
| ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f488]) ).
thf(f528,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK33 ) )
| ( $false
= ( !! @ $i
@ ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) ) ) ) ),
inference(or_proxy_clausification,[],[f527]) ).
thf(f547,plain,
( ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK12 @ Y0 )
=> ( ( q @ Y0 )
& ( r @ Y0 ) ) )
@ sK29 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( r @ Y0 ) )
@ sK33 ) )
| ( $false
= ( ^ [Y0: $i] :
( ( irel @ sK15 @ Y0 )
=> ( q @ Y0 ) )
@ sK35 ) ) ),
inference(sigma_proxy_clausification,[],[f528]) ).
thf(f548,plain,
( ( $false
= ( ( irel @ sK12 @ sK29 )
=> ( ( q @ sK29 )
& ( r @ sK29 ) ) ) )
| ( $false
= ( ( irel @ sK15 @ sK33 )
=> ( r @ sK33 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) ) ),
inference(beta-eta_normalization,[],[f547]) ).
thf(f549,plain,
( ( $false
= ( ( q @ sK29 )
& ( r @ sK29 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK33 )
=> ( r @ sK33 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) ) ),
inference(imp_proxy_clausification,[],[f548]) ).
thf(f550,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( ( irel @ sK15 @ sK33 )
=> ( r @ sK33 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) ) ),
inference(imp_proxy_clausification,[],[f548]) ).
thf(f551,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) ) ),
inference(imp_proxy_clausification,[],[f550]) ).
thf(f552,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) ) ),
inference(imp_proxy_clausification,[],[f550]) ).
thf(f553,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $false
= ( q @ sK35 ) ) ),
inference(imp_proxy_clausification,[],[f552]) ).
thf(f554,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $true
= ( irel @ sK15 @ sK35 ) ) ),
inference(imp_proxy_clausification,[],[f552]) ).
thf(f555,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $false
= ( q @ sK35 ) ) ),
inference(imp_proxy_clausification,[],[f551]) ).
thf(f556,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $true
= ( irel @ sK15 @ sK35 ) ) ),
inference(imp_proxy_clausification,[],[f551]) ).
thf(f557,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( ( irel @ sK15 @ sK33 )
=> ( r @ sK33 ) ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(and_proxy_clausification,[],[f549]) ).
thf(f558,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f557]) ).
thf(f559,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $false
= ( ( irel @ sK15 @ sK35 )
=> ( q @ sK35 ) ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f557]) ).
thf(f560,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $false
= ( q @ sK35 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f559]) ).
thf(f561,plain,
( ( $false
= ( r @ sK29 ) )
| ( $true
= ( irel @ sK15 @ sK33 ) )
| ( $true
= ( irel @ sK15 @ sK35 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f559]) ).
thf(f562,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $false
= ( q @ sK35 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f558]) ).
thf(f563,plain,
( ( $false
= ( r @ sK29 ) )
| ( $false
= ( r @ sK33 ) )
| ( $true
= ( irel @ sK15 @ sK35 ) )
| ( $false
= ( q @ sK29 ) ) ),
inference(imp_proxy_clausification,[],[f558]) ).
thf(f565,definition,
( spl36_1
<=> ! [X6: $i,X2: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( p @ X6 ) )
| ( $true
= ( q @ X4 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $false
= ( irel @ X2 @ X4 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
thf(f566,plain,
( ! [X2: $i,X6: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $true
= ( q @ X4 ) )
| ( $true
= ( p @ X6 ) ) )
| ~ spl36_1 ),
inference(avatar_component_clause,[],[f565]) ).
thf(f567,plain,
( spl36_1
| spl36_1 ),
inference(avatar_split_clause,[],[f122,f565,f565]) ).
thf(f569,definition,
( spl36_2
<=> ! [X6: $i,X2: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X2 ) )
| ( $true
= ( p @ X6 ) )
| ( $true
= ( r @ X4 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $false
= ( irel @ X2 @ X4 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
thf(f570,plain,
( ! [X2: $i,X6: $i,X4: $i] :
( ( $false
= ( irel @ sK0 @ X2 ) )
| ( $false
= ( irel @ X2 @ X6 ) )
| ( $false
= ( irel @ X2 @ X4 ) )
| ( $true
= ( r @ X4 ) )
| ( $true
= ( p @ X6 ) ) )
| ~ spl36_2 ),
inference(avatar_component_clause,[],[f569]) ).
thf(f573,plain,
( spl36_2
| spl36_2 ),
inference(avatar_split_clause,[],[f134,f569,f569]) ).
thf(f693,definition,
( spl36_24
<=> ( $true
= ( irel @ sK0 @ sK12 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_24])],[avatar_definition]) ).
thf(f695,plain,
( ( $true
= ( irel @ sK0 @ sK12 ) )
| ~ spl36_24 ),
inference(avatar_component_clause,[],[f693]) ).
thf(f727,definition,
( spl36_30
<=> ( $true
= ( irel @ sK0 @ sK15 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_30])],[avatar_definition]) ).
thf(f729,plain,
( ( $true
= ( irel @ sK0 @ sK15 ) )
| ~ spl36_30 ),
inference(avatar_component_clause,[],[f727]) ).
thf(f730,plain,
( spl36_30
| spl36_24 ),
inference(avatar_split_clause,[],[f357,f693,f727]) ).
thf(f732,definition,
( spl36_31
<=> ( $true
= ( irel @ sK15 @ sK17 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_31])],[avatar_definition]) ).
thf(f734,plain,
( ( $true
= ( irel @ sK15 @ sK17 ) )
| ~ spl36_31 ),
inference(avatar_component_clause,[],[f732]) ).
thf(f736,definition,
( spl36_32
<=> ( $true
= ( irel @ sK15 @ sK16 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_32])],[avatar_definition]) ).
thf(f738,plain,
( ( $true
= ( irel @ sK15 @ sK16 ) )
| ~ spl36_32 ),
inference(avatar_component_clause,[],[f736]) ).
thf(f739,plain,
( spl36_31
| spl36_32
| spl36_24 ),
inference(avatar_split_clause,[],[f369,f693,f736,f732]) ).
thf(f741,definition,
( spl36_33
<=> ( $false
= ( p @ sK17 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_33])],[avatar_definition]) ).
thf(f743,plain,
( ( $false
= ( p @ sK17 ) )
| ~ spl36_33 ),
inference(avatar_component_clause,[],[f741]) ).
thf(f744,plain,
( spl36_33
| spl36_32
| spl36_24 ),
inference(avatar_split_clause,[],[f368,f693,f736,f741]) ).
thf(f746,definition,
( spl36_34
<=> ( $false
= ( p @ sK16 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_34])],[avatar_definition]) ).
thf(f748,plain,
( ( $false
= ( p @ sK16 ) )
| ~ spl36_34 ),
inference(avatar_component_clause,[],[f746]) ).
thf(f749,plain,
( spl36_31
| spl36_34
| spl36_24 ),
inference(avatar_split_clause,[],[f371,f693,f746,f732]) ).
thf(f750,plain,
( spl36_33
| spl36_34
| spl36_24 ),
inference(avatar_split_clause,[],[f370,f693,f746,f741]) ).
thf(f768,definition,
( spl36_38
<=> ( $true
= ( irel @ sK15 @ sK19 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_38])],[avatar_definition]) ).
thf(f770,plain,
( ( $true
= ( irel @ sK15 @ sK19 ) )
| ~ spl36_38 ),
inference(avatar_component_clause,[],[f768]) ).
thf(f778,definition,
( spl36_40
<=> ( $false
= ( r @ sK19 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_40])],[avatar_definition]) ).
thf(f780,plain,
( ( $false
= ( r @ sK19 ) )
| ~ spl36_40 ),
inference(avatar_component_clause,[],[f778]) ).
thf(f784,definition,
( spl36_41
<=> ( $true
= ( irel @ sK15 @ sK21 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_41])],[avatar_definition]) ).
thf(f786,plain,
( ( $true
= ( irel @ sK15 @ sK21 ) )
| ~ spl36_41 ),
inference(avatar_component_clause,[],[f784]) ).
thf(f787,plain,
( spl36_41
| spl36_38
| spl36_24 ),
inference(avatar_split_clause,[],[f396,f693,f768,f784]) ).
thf(f789,definition,
( spl36_42
<=> ( $false
= ( q @ sK21 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_42])],[avatar_definition]) ).
thf(f791,plain,
( ( $false
= ( q @ sK21 ) )
| ~ spl36_42 ),
inference(avatar_component_clause,[],[f789]) ).
thf(f792,plain,
( spl36_42
| spl36_38
| spl36_24 ),
inference(avatar_split_clause,[],[f395,f693,f768,f789]) ).
thf(f793,plain,
( spl36_41
| spl36_40
| spl36_24 ),
inference(avatar_split_clause,[],[f398,f693,f778,f784]) ).
thf(f794,plain,
( spl36_42
| spl36_40
| spl36_24 ),
inference(avatar_split_clause,[],[f397,f693,f778,f789]) ).
thf(f796,definition,
( spl36_43
<=> ( $true
= ( irel @ sK12 @ sK22 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_43])],[avatar_definition]) ).
thf(f798,plain,
( ( $true
= ( irel @ sK12 @ sK22 ) )
| ~ spl36_43 ),
inference(avatar_component_clause,[],[f796]) ).
thf(f799,plain,
( spl36_30
| spl36_43 ),
inference(avatar_split_clause,[],[f406,f796,f727]) ).
thf(f801,definition,
( spl36_44
<=> ( $false
= ( p @ sK22 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_44])],[avatar_definition]) ).
thf(f803,plain,
( ( $false
= ( p @ sK22 ) )
| ~ spl36_44 ),
inference(avatar_component_clause,[],[f801]) ).
thf(f804,plain,
( spl36_30
| spl36_44 ),
inference(avatar_split_clause,[],[f405,f801,f727]) ).
thf(f806,definition,
( spl36_45
<=> ( $true
= ( irel @ sK15 @ sK24 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_45])],[avatar_definition]) ).
thf(f808,plain,
( ( $true
= ( irel @ sK15 @ sK24 ) )
| ~ spl36_45 ),
inference(avatar_component_clause,[],[f806]) ).
thf(f810,definition,
( spl36_46
<=> ( $true
= ( irel @ sK15 @ sK23 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_46])],[avatar_definition]) ).
thf(f812,plain,
( ( $true
= ( irel @ sK15 @ sK23 ) )
| ~ spl36_46 ),
inference(avatar_component_clause,[],[f810]) ).
thf(f813,plain,
( spl36_45
| spl36_46
| spl36_43 ),
inference(avatar_split_clause,[],[f420,f796,f810,f806]) ).
thf(f815,definition,
( spl36_47
<=> ( $false
= ( p @ sK24 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_47])],[avatar_definition]) ).
thf(f817,plain,
( ( $false
= ( p @ sK24 ) )
| ~ spl36_47 ),
inference(avatar_component_clause,[],[f815]) ).
thf(f818,plain,
( spl36_47
| spl36_46
| spl36_43 ),
inference(avatar_split_clause,[],[f419,f796,f810,f815]) ).
thf(f820,definition,
( spl36_48
<=> ( $false
= ( p @ sK23 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_48])],[avatar_definition]) ).
thf(f822,plain,
( ( $false
= ( p @ sK23 ) )
| ~ spl36_48 ),
inference(avatar_component_clause,[],[f820]) ).
thf(f823,plain,
( spl36_45
| spl36_48
| spl36_43 ),
inference(avatar_split_clause,[],[f422,f796,f820,f806]) ).
thf(f824,plain,
( spl36_47
| spl36_48
| spl36_43 ),
inference(avatar_split_clause,[],[f421,f796,f820,f815]) ).
thf(f825,plain,
( spl36_45
| spl36_46
| spl36_44 ),
inference(avatar_split_clause,[],[f426,f801,f810,f806]) ).
thf(f826,plain,
( spl36_47
| spl36_46
| spl36_44 ),
inference(avatar_split_clause,[],[f425,f801,f810,f815]) ).
thf(f827,plain,
( spl36_45
| spl36_48
| spl36_44 ),
inference(avatar_split_clause,[],[f428,f801,f820,f806]) ).
thf(f828,plain,
( spl36_47
| spl36_48
| spl36_44 ),
inference(avatar_split_clause,[],[f427,f801,f820,f815]) ).
thf(f850,definition,
( spl36_52
<=> ( $true
= ( irel @ sK15 @ sK26 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_52])],[avatar_definition]) ).
thf(f852,plain,
( ( $true
= ( irel @ sK15 @ sK26 ) )
| ~ spl36_52 ),
inference(avatar_component_clause,[],[f850]) ).
thf(f860,definition,
( spl36_54
<=> ( $false
= ( r @ sK26 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_54])],[avatar_definition]) ).
thf(f862,plain,
( ( $false
= ( r @ sK26 ) )
| ~ spl36_54 ),
inference(avatar_component_clause,[],[f860]) ).
thf(f870,definition,
( spl36_55
<=> ( $true
= ( irel @ sK15 @ sK28 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_55])],[avatar_definition]) ).
thf(f872,plain,
( ( $true
= ( irel @ sK15 @ sK28 ) )
| ~ spl36_55 ),
inference(avatar_component_clause,[],[f870]) ).
thf(f873,plain,
( spl36_55
| spl36_52
| spl36_43 ),
inference(avatar_split_clause,[],[f471,f796,f850,f870]) ).
thf(f875,definition,
( spl36_56
<=> ( $false
= ( q @ sK28 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_56])],[avatar_definition]) ).
thf(f877,plain,
( ( $false
= ( q @ sK28 ) )
| ~ spl36_56 ),
inference(avatar_component_clause,[],[f875]) ).
thf(f878,plain,
( spl36_56
| spl36_52
| spl36_43 ),
inference(avatar_split_clause,[],[f470,f796,f850,f875]) ).
thf(f879,plain,
( spl36_55
| spl36_54
| spl36_43 ),
inference(avatar_split_clause,[],[f473,f796,f860,f870]) ).
thf(f880,plain,
( spl36_56
| spl36_54
| spl36_43 ),
inference(avatar_split_clause,[],[f472,f796,f860,f875]) ).
thf(f881,plain,
( spl36_55
| spl36_52
| spl36_44 ),
inference(avatar_split_clause,[],[f477,f801,f850,f870]) ).
thf(f882,plain,
( spl36_56
| spl36_52
| spl36_44 ),
inference(avatar_split_clause,[],[f476,f801,f850,f875]) ).
thf(f883,plain,
( spl36_55
| spl36_54
| spl36_44 ),
inference(avatar_split_clause,[],[f479,f801,f860,f870]) ).
thf(f884,plain,
( spl36_56
| spl36_54
| spl36_44 ),
inference(avatar_split_clause,[],[f478,f801,f860,f875]) ).
thf(f886,definition,
( spl36_57
<=> ( $true
= ( irel @ sK12 @ sK29 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_57])],[avatar_definition]) ).
thf(f888,plain,
( ( $true
= ( irel @ sK12 @ sK29 ) )
| ~ spl36_57 ),
inference(avatar_component_clause,[],[f886]) ).
thf(f889,plain,
( spl36_30
| spl36_57 ),
inference(avatar_split_clause,[],[f485,f886,f727]) ).
thf(f891,definition,
( spl36_58
<=> ( $false
= ( q @ sK29 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_58])],[avatar_definition]) ).
thf(f893,plain,
( ( $false
= ( q @ sK29 ) )
| ~ spl36_58 ),
inference(avatar_component_clause,[],[f891]) ).
thf(f895,definition,
( spl36_59
<=> ( $false
= ( r @ sK29 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_59])],[avatar_definition]) ).
thf(f897,plain,
( ( $false
= ( r @ sK29 ) )
| ~ spl36_59 ),
inference(avatar_component_clause,[],[f895]) ).
thf(f898,plain,
( spl36_58
| spl36_30
| spl36_59 ),
inference(avatar_split_clause,[],[f486,f895,f727,f891]) ).
thf(f900,definition,
( spl36_60
<=> ( $true
= ( irel @ sK15 @ sK31 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_60])],[avatar_definition]) ).
thf(f902,plain,
( ( $true
= ( irel @ sK15 @ sK31 ) )
| ~ spl36_60 ),
inference(avatar_component_clause,[],[f900]) ).
thf(f904,definition,
( spl36_61
<=> ( $true
= ( irel @ sK15 @ sK30 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_61])],[avatar_definition]) ).
thf(f906,plain,
( ( $true
= ( irel @ sK15 @ sK30 ) )
| ~ spl36_61 ),
inference(avatar_component_clause,[],[f904]) ).
thf(f907,plain,
( spl36_60
| spl36_61
| spl36_57 ),
inference(avatar_split_clause,[],[f500,f886,f904,f900]) ).
thf(f909,definition,
( spl36_62
<=> ( $false
= ( p @ sK31 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_62])],[avatar_definition]) ).
thf(f911,plain,
( ( $false
= ( p @ sK31 ) )
| ~ spl36_62 ),
inference(avatar_component_clause,[],[f909]) ).
thf(f912,plain,
( spl36_62
| spl36_61
| spl36_57 ),
inference(avatar_split_clause,[],[f499,f886,f904,f909]) ).
thf(f914,definition,
( spl36_63
<=> ( $false
= ( p @ sK30 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_63])],[avatar_definition]) ).
thf(f916,plain,
( ( $false
= ( p @ sK30 ) )
| ~ spl36_63 ),
inference(avatar_component_clause,[],[f914]) ).
thf(f917,plain,
( spl36_60
| spl36_63
| spl36_57 ),
inference(avatar_split_clause,[],[f502,f886,f914,f900]) ).
thf(f918,plain,
( spl36_62
| spl36_63
| spl36_57 ),
inference(avatar_split_clause,[],[f501,f886,f914,f909]) ).
thf(f919,plain,
( spl36_58
| spl36_60
| spl36_61
| spl36_59 ),
inference(avatar_split_clause,[],[f507,f895,f904,f900,f891]) ).
thf(f920,plain,
( spl36_58
| spl36_62
| spl36_61
| spl36_59 ),
inference(avatar_split_clause,[],[f506,f895,f904,f909,f891]) ).
thf(f921,plain,
( spl36_58
| spl36_60
| spl36_63
| spl36_59 ),
inference(avatar_split_clause,[],[f509,f895,f914,f900,f891]) ).
thf(f922,plain,
( spl36_58
| spl36_62
| spl36_63
| spl36_59 ),
inference(avatar_split_clause,[],[f508,f895,f914,f909,f891]) ).
thf(f944,definition,
( spl36_67
<=> ( $true
= ( irel @ sK15 @ sK33 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_67])],[avatar_definition]) ).
thf(f946,plain,
( ( $true
= ( irel @ sK15 @ sK33 ) )
| ~ spl36_67 ),
inference(avatar_component_clause,[],[f944]) ).
thf(f954,definition,
( spl36_69
<=> ( $false
= ( r @ sK33 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_69])],[avatar_definition]) ).
thf(f956,plain,
( ( $false
= ( r @ sK33 ) )
| ~ spl36_69 ),
inference(avatar_component_clause,[],[f954]) ).
thf(f964,definition,
( spl36_70
<=> ( $true
= ( irel @ sK15 @ sK35 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_70])],[avatar_definition]) ).
thf(f966,plain,
( ( $true
= ( irel @ sK15 @ sK35 ) )
| ~ spl36_70 ),
inference(avatar_component_clause,[],[f964]) ).
thf(f967,plain,
( spl36_70
| spl36_67
| spl36_57 ),
inference(avatar_split_clause,[],[f554,f886,f944,f964]) ).
thf(f969,definition,
( spl36_71
<=> ( $false
= ( q @ sK35 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_71])],[avatar_definition]) ).
thf(f971,plain,
( ( $false
= ( q @ sK35 ) )
| ~ spl36_71 ),
inference(avatar_component_clause,[],[f969]) ).
thf(f972,plain,
( spl36_71
| spl36_67
| spl36_57 ),
inference(avatar_split_clause,[],[f553,f886,f944,f969]) ).
thf(f973,plain,
( spl36_70
| spl36_69
| spl36_57 ),
inference(avatar_split_clause,[],[f556,f886,f954,f964]) ).
thf(f974,plain,
( spl36_71
| spl36_69
| spl36_57 ),
inference(avatar_split_clause,[],[f555,f886,f954,f969]) ).
thf(f975,plain,
( spl36_58
| spl36_70
| spl36_67
| spl36_59 ),
inference(avatar_split_clause,[],[f561,f895,f944,f964,f891]) ).
thf(f976,plain,
( spl36_58
| spl36_71
| spl36_67
| spl36_59 ),
inference(avatar_split_clause,[],[f560,f895,f944,f969,f891]) ).
thf(f977,plain,
( spl36_58
| spl36_70
| spl36_69
| spl36_59 ),
inference(avatar_split_clause,[],[f563,f895,f954,f964,f891]) ).
thf(f978,plain,
( spl36_58
| spl36_71
| spl36_69
| spl36_59 ),
inference(avatar_split_clause,[],[f562,f895,f954,f969,f891]) ).
thf(f1060,definition,
( spl36_79
<=> ! [X1: $i] :
( ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( q @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_79])],[avatar_definition]) ).
thf(f1061,plain,
( ! [X1: $i] :
( ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( q @ X1 ) ) )
| ~ spl36_79 ),
inference(avatar_component_clause,[],[f1060]) ).
thf(f1063,definition,
( spl36_80
<=> ! [X0: $i] :
( ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( p @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_80])],[avatar_definition]) ).
thf(f1064,plain,
( ! [X0: $i] :
( ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_80 ),
inference(avatar_component_clause,[],[f1063]) ).
thf(f1117,plain,
( ( $true = $false )
| ( $true
= ( q @ sK29 ) )
| ~ spl36_57
| ~ spl36_79 ),
inference(constrained_superposition,[],[f1061,f888]) ).
thf(f1124,plain,
( ( $true
= ( q @ sK29 ) )
| ~ spl36_57
| ~ spl36_79 ),
inference(trivial_inequality_removal,[],[f1117]) ).
thf(f1129,plain,
( ( $true = $false )
| ~ spl36_57
| ~ spl36_58
| ~ spl36_79 ),
inference(forward_demodulation,[],[f1124,f893]) ).
thf(f1130,plain,
( $false
| ~ spl36_57
| ~ spl36_58
| ~ spl36_79 ),
inference(trivial_inequality_removal,[],[f1129]) ).
thf(f1131,plain,
( ~ spl36_57
| ~ spl36_58
| ~ spl36_79 ),
inference(avatar_contradiction_clause,[],[f1130]) ).
thf(f1132,plain,
( ( $true = $false )
| ( $true
= ( p @ sK22 ) )
| ~ spl36_43
| ~ spl36_80 ),
inference(constrained_superposition,[],[f1064,f798]) ).
thf(f1141,plain,
( ( $true
= ( p @ sK22 ) )
| ~ spl36_43
| ~ spl36_80 ),
inference(trivial_inequality_removal,[],[f1132]) ).
thf(f1145,plain,
( ( $true = $false )
| ~ spl36_43
| ~ spl36_44
| ~ spl36_80 ),
inference(forward_demodulation,[],[f1141,f803]) ).
thf(f1146,plain,
( $false
| ~ spl36_43
| ~ spl36_44
| ~ spl36_80 ),
inference(trivial_inequality_removal,[],[f1145]) ).
thf(f1147,plain,
( ~ spl36_43
| ~ spl36_44
| ~ spl36_80 ),
inference(avatar_contradiction_clause,[],[f1146]) ).
thf(f1314,definition,
( spl36_84
<=> ! [X1: $i] :
( ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( r @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_84])],[avatar_definition]) ).
thf(f1315,plain,
( ! [X1: $i] :
( ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( r @ X1 ) ) )
| ~ spl36_84 ),
inference(avatar_component_clause,[],[f1314]) ).
thf(f1340,plain,
( ( $true = $false )
| ( $true
= ( r @ sK29 ) )
| ~ spl36_57
| ~ spl36_84 ),
inference(constrained_superposition,[],[f1315,f888]) ).
thf(f1349,plain,
( ( $true
= ( r @ sK29 ) )
| ~ spl36_57
| ~ spl36_84 ),
inference(trivial_inequality_removal,[],[f1340]) ).
thf(f1355,plain,
( ( $true = $false )
| ~ spl36_57
| ~ spl36_59
| ~ spl36_84 ),
inference(forward_demodulation,[],[f1349,f897]) ).
thf(f1356,plain,
( $false
| ~ spl36_57
| ~ spl36_59
| ~ spl36_84 ),
inference(trivial_inequality_removal,[],[f1355]) ).
thf(f1357,plain,
( ~ spl36_57
| ~ spl36_59
| ~ spl36_84 ),
inference(avatar_contradiction_clause,[],[f1356]) ).
thf(f1413,plain,
( ! [X0: $i,X1: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK15 @ X0 ) )
| ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( r @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_30 ),
inference(constrained_superposition,[],[f729,f570]) ).
thf(f1417,plain,
( ! [X0: $i,X1: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK15 @ X0 ) )
| ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( q @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_1
| ~ spl36_30 ),
inference(constrained_superposition,[],[f729,f566]) ).
thf(f1452,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( irel @ sK15 @ X0 ) )
| ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( q @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_1
| ~ spl36_30 ),
inference(trivial_inequality_removal,[],[f1417]) ).
thf(f1456,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( irel @ sK15 @ X0 ) )
| ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( r @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_30 ),
inference(trivial_inequality_removal,[],[f1413]) ).
thf(f1462,definition,
( spl36_87
<=> ! [X1: $i] :
( ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( q @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_87])],[avatar_definition]) ).
thf(f1463,plain,
( ! [X1: $i] :
( ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( q @ X1 ) ) )
| ~ spl36_87 ),
inference(avatar_component_clause,[],[f1462]) ).
thf(f1465,definition,
( spl36_88
<=> ! [X0: $i] :
( ( $false
= ( irel @ sK15 @ X0 ) )
| ( $true
= ( p @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_88])],[avatar_definition]) ).
thf(f1466,plain,
( ! [X0: $i] :
( ( $false
= ( irel @ sK15 @ X0 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_88 ),
inference(avatar_component_clause,[],[f1465]) ).
thf(f1469,definition,
( spl36_89
<=> ! [X1: $i] :
( ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( r @ X1 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl36_89])],[avatar_definition]) ).
thf(f1470,plain,
( ! [X1: $i] :
( ( $false
= ( irel @ sK15 @ X1 ) )
| ( $true
= ( r @ X1 ) ) )
| ~ spl36_89 ),
inference(avatar_component_clause,[],[f1469]) ).
thf(f1476,plain,
( spl36_87
| spl36_88
| ~ spl36_1
| ~ spl36_30 ),
inference(avatar_split_clause,[],[f1452,f727,f565,f1465,f1462]) ).
thf(f1477,plain,
( spl36_89
| spl36_88
| ~ spl36_2
| ~ spl36_30 ),
inference(avatar_split_clause,[],[f1456,f727,f569,f1465,f1469]) ).
thf(f1626,plain,
( ( $true = $false )
| ( $true
= ( p @ sK30 ) )
| ~ spl36_61
| ~ spl36_88 ),
inference(constrained_superposition,[],[f1466,f906]) ).
thf(f1639,plain,
( ( $true
= ( p @ sK30 ) )
| ~ spl36_61
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f1626]) ).
thf(f1644,plain,
( ( $true = $false )
| ~ spl36_61
| ~ spl36_63
| ~ spl36_88 ),
inference(forward_demodulation,[],[f1639,f916]) ).
thf(f1645,plain,
( $false
| ~ spl36_61
| ~ spl36_63
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f1644]) ).
thf(f1646,plain,
( ~ spl36_61
| ~ spl36_63
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f1645]) ).
thf(f1802,plain,
( ( $true = $false )
| ( $true
= ( r @ sK33 ) )
| ~ spl36_67
| ~ spl36_89 ),
inference(constrained_superposition,[],[f1470,f946]) ).
thf(f1815,plain,
( ( $true
= ( r @ sK33 ) )
| ~ spl36_67
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f1802]) ).
thf(f1822,plain,
( ( $true = $false )
| ~ spl36_67
| ~ spl36_69
| ~ spl36_89 ),
inference(forward_demodulation,[],[f1815,f956]) ).
thf(f1823,plain,
( $false
| ~ spl36_67
| ~ spl36_69
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f1822]) ).
thf(f1824,plain,
( ~ spl36_67
| ~ spl36_69
| ~ spl36_89 ),
inference(avatar_contradiction_clause,[],[f1823]) ).
thf(f1906,plain,
( ( $true = $false )
| ( $true
= ( q @ sK35 ) )
| ~ spl36_70
| ~ spl36_87 ),
inference(constrained_superposition,[],[f966,f1463]) ).
thf(f1943,plain,
( ( $true
= ( q @ sK35 ) )
| ~ spl36_70
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f1906]) ).
thf(f1960,plain,
( ( $true = $false )
| ~ spl36_70
| ~ spl36_71
| ~ spl36_87 ),
inference(forward_demodulation,[],[f1943,f971]) ).
thf(f1961,plain,
( $false
| ~ spl36_70
| ~ spl36_71
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f1960]) ).
thf(f1962,plain,
( ~ spl36_70
| ~ spl36_71
| ~ spl36_87 ),
inference(avatar_contradiction_clause,[],[f1961]) ).
thf(f2323,plain,
( ( $true = $false )
| ( $true
= ( r @ sK19 ) )
| ~ spl36_38
| ~ spl36_89 ),
inference(constrained_superposition,[],[f770,f1470]) ).
thf(f2370,plain,
( ( $true
= ( r @ sK19 ) )
| ~ spl36_38
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f2323]) ).
thf(f2390,plain,
( ( $true = $false )
| ~ spl36_38
| ~ spl36_40
| ~ spl36_89 ),
inference(forward_demodulation,[],[f2370,f780]) ).
thf(f2391,plain,
( $false
| ~ spl36_38
| ~ spl36_40
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f2390]) ).
thf(f2392,plain,
( ~ spl36_38
| ~ spl36_40
| ~ spl36_89 ),
inference(avatar_contradiction_clause,[],[f2391]) ).
thf(f2820,plain,
( ( $true = $false )
| ( $true
= ( p @ sK16 ) )
| ~ spl36_32
| ~ spl36_88 ),
inference(constrained_superposition,[],[f1466,f738]) ).
thf(f2822,plain,
( ( $true = $false )
| ( $true
= ( p @ sK23 ) )
| ~ spl36_46
| ~ spl36_88 ),
inference(constrained_superposition,[],[f1466,f812]) ).
thf(f2825,plain,
( ( $true = $false )
| ( $true
= ( p @ sK31 ) )
| ~ spl36_60
| ~ spl36_88 ),
inference(constrained_superposition,[],[f1466,f902]) ).
thf(f2864,plain,
( ( $true
= ( p @ sK31 ) )
| ~ spl36_60
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2825]) ).
thf(f2867,plain,
( ( $true
= ( p @ sK23 ) )
| ~ spl36_46
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2822]) ).
thf(f2869,plain,
( ( $true
= ( p @ sK16 ) )
| ~ spl36_32
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2820]) ).
thf(f2888,plain,
( ( $true = $false )
| ~ spl36_60
| ~ spl36_62
| ~ spl36_88 ),
inference(forward_demodulation,[],[f2864,f911]) ).
thf(f2889,plain,
( $false
| ~ spl36_60
| ~ spl36_62
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2888]) ).
thf(f2890,plain,
( ~ spl36_60
| ~ spl36_62
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f2889]) ).
thf(f2891,plain,
( ( $true = $false )
| ~ spl36_46
| ~ spl36_48
| ~ spl36_88 ),
inference(forward_demodulation,[],[f2867,f822]) ).
thf(f2892,plain,
( $false
| ~ spl36_46
| ~ spl36_48
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2891]) ).
thf(f2893,plain,
( ~ spl36_46
| ~ spl36_48
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f2892]) ).
thf(f2894,plain,
( ( $true = $false )
| ~ spl36_32
| ~ spl36_34
| ~ spl36_88 ),
inference(forward_demodulation,[],[f2869,f748]) ).
thf(f2895,plain,
( $false
| ~ spl36_32
| ~ spl36_34
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f2894]) ).
thf(f2896,plain,
( ~ spl36_32
| ~ spl36_34
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f2895]) ).
thf(f2908,definition,
( spl36_115
<=> ( $false
= ( irel @ sK0 @ sK12 ) ) ),
introduced(definition,[new_symbols(definition,[spl36_115])],[avatar_definition]) ).
thf(f2910,plain,
( ( $false
= ( irel @ sK0 @ sK12 ) )
| ~ spl36_115 ),
inference(avatar_component_clause,[],[f2908]) ).
thf(f3091,plain,
( ! [X0: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( r @ sK29 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_57 ),
inference(constrained_superposition,[],[f888,f570]) ).
thf(f3132,plain,
( ! [X0: $i] :
( ( $false
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( r @ sK29 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_57 ),
inference(trivial_inequality_removal,[],[f3091]) ).
thf(f3135,plain,
( ( $true = $false )
| ( $true
= ( p @ sK17 ) )
| ~ spl36_31
| ~ spl36_88 ),
inference(constrained_superposition,[],[f734,f1466]) ).
thf(f3184,plain,
( ( $true
= ( p @ sK17 ) )
| ~ spl36_31
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f3135]) ).
thf(f3200,plain,
( ( $true = $false )
| ~ spl36_31
| ~ spl36_33
| ~ spl36_88 ),
inference(forward_demodulation,[],[f3184,f743]) ).
thf(f3201,plain,
( $false
| ~ spl36_31
| ~ spl36_33
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f3200]) ).
thf(f3202,plain,
( ~ spl36_31
| ~ spl36_33
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f3201]) ).
thf(f3307,plain,
( ! [X0: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_57
| ~ spl36_59 ),
inference(forward_demodulation,[],[f3132,f897]) ).
thf(f3308,plain,
( ! [X0: $i] :
( ( $false
= ( irel @ sK0 @ sK12 ) )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_57
| ~ spl36_59 ),
inference(trivial_inequality_removal,[],[f3307]) ).
thf(f3320,plain,
( spl36_80
| spl36_115
| ~ spl36_2
| ~ spl36_57
| ~ spl36_59 ),
inference(avatar_split_clause,[],[f3308,f895,f886,f569,f2908,f1063]) ).
thf(f3323,plain,
( ! [X0: $i,X1: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( r @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_24 ),
inference(constrained_superposition,[],[f695,f570]) ).
thf(f3327,plain,
( ! [X0: $i,X1: $i] :
( ( $true = $false )
| ( $false
= ( irel @ sK12 @ X0 ) )
| ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( q @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_1
| ~ spl36_24 ),
inference(constrained_superposition,[],[f695,f566]) ).
thf(f3384,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( irel @ sK12 @ X0 ) )
| ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( q @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_1
| ~ spl36_24 ),
inference(trivial_inequality_removal,[],[f3327]) ).
thf(f3388,plain,
( ! [X0: $i,X1: $i] :
( ( $false
= ( irel @ sK12 @ X0 ) )
| ( $false
= ( irel @ sK12 @ X1 ) )
| ( $true
= ( r @ X1 ) )
| ( $true
= ( p @ X0 ) ) )
| ~ spl36_2
| ~ spl36_24 ),
inference(trivial_inequality_removal,[],[f3323]) ).
thf(f3391,plain,
( spl36_79
| spl36_80
| ~ spl36_1
| ~ spl36_24 ),
inference(avatar_split_clause,[],[f3384,f693,f565,f1063,f1060]) ).
thf(f3392,plain,
( spl36_84
| spl36_80
| ~ spl36_2
| ~ spl36_24 ),
inference(avatar_split_clause,[],[f3388,f693,f569,f1063,f1314]) ).
thf(f3411,plain,
( ( $true = $false )
| ~ spl36_24
| ~ spl36_115 ),
inference(constrained_superposition,[],[f2910,f695]) ).
thf(f3424,plain,
( $false
| ~ spl36_24
| ~ spl36_115 ),
inference(trivial_inequality_removal,[],[f3411]) ).
thf(f3425,plain,
( ~ spl36_24
| ~ spl36_115 ),
inference(avatar_contradiction_clause,[],[f3424]) ).
thf(f4155,plain,
( ( $true = $false )
| ( $true
= ( p @ sK24 ) )
| ~ spl36_45
| ~ spl36_88 ),
inference(constrained_superposition,[],[f808,f1466]) ).
thf(f4220,plain,
( ( $true
= ( p @ sK24 ) )
| ~ spl36_45
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f4155]) ).
thf(f4236,plain,
( ( $true = $false )
| ~ spl36_45
| ~ spl36_47
| ~ spl36_88 ),
inference(forward_demodulation,[],[f4220,f817]) ).
thf(f4237,plain,
( $false
| ~ spl36_45
| ~ spl36_47
| ~ spl36_88 ),
inference(trivial_inequality_removal,[],[f4236]) ).
thf(f4238,plain,
( ~ spl36_45
| ~ spl36_47
| ~ spl36_88 ),
inference(avatar_contradiction_clause,[],[f4237]) ).
thf(f4496,plain,
( ( $true = $false )
| ( $true
= ( q @ sK21 ) )
| ~ spl36_41
| ~ spl36_87 ),
inference(constrained_superposition,[],[f1463,f786]) ).
thf(f4562,plain,
( ( $true
= ( q @ sK21 ) )
| ~ spl36_41
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f4496]) ).
thf(f4590,plain,
( ( $true = $false )
| ~ spl36_41
| ~ spl36_42
| ~ spl36_87 ),
inference(forward_demodulation,[],[f4562,f791]) ).
thf(f4591,plain,
( $false
| ~ spl36_41
| ~ spl36_42
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f4590]) ).
thf(f4592,plain,
( ~ spl36_41
| ~ spl36_42
| ~ spl36_87 ),
inference(avatar_contradiction_clause,[],[f4591]) ).
thf(f4658,plain,
( ( $true = $false )
| ( $true
= ( r @ sK26 ) )
| ~ spl36_52
| ~ spl36_89 ),
inference(constrained_superposition,[],[f1470,f852]) ).
thf(f4716,plain,
( ( $true
= ( r @ sK26 ) )
| ~ spl36_52
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f4658]) ).
thf(f4733,plain,
( ( $true = $false )
| ~ spl36_52
| ~ spl36_54
| ~ spl36_89 ),
inference(forward_demodulation,[],[f4716,f862]) ).
thf(f4734,plain,
( $false
| ~ spl36_52
| ~ spl36_54
| ~ spl36_89 ),
inference(trivial_inequality_removal,[],[f4733]) ).
thf(f4735,plain,
( ~ spl36_52
| ~ spl36_54
| ~ spl36_89 ),
inference(avatar_contradiction_clause,[],[f4734]) ).
thf(f4847,plain,
( ( $true = $false )
| ( $true
= ( q @ sK28 ) )
| ~ spl36_55
| ~ spl36_87 ),
inference(constrained_superposition,[],[f872,f1463]) ).
thf(f4914,plain,
( ( $true
= ( q @ sK28 ) )
| ~ spl36_55
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f4847]) ).
thf(f4931,plain,
( ( $true = $false )
| ~ spl36_55
| ~ spl36_56
| ~ spl36_87 ),
inference(forward_demodulation,[],[f4914,f877]) ).
thf(f4932,plain,
( $false
| ~ spl36_55
| ~ spl36_56
| ~ spl36_87 ),
inference(trivial_inequality_removal,[],[f4931]) ).
thf(f4933,plain,
( ~ spl36_55
| ~ spl36_56
| ~ spl36_87 ),
inference(avatar_contradiction_clause,[],[f4932]) ).
cnf(s1,plain,
( spl36_1
| spl36_1 ),
inference(sat_conversion,[],[f567]) ).
cnf(s2,plain,
spl36_1,
inference(rat,[],[s1]) ).
cnf(s5,plain,
( spl36_2
| spl36_2 ),
inference(sat_conversion,[],[f573]) ).
cnf(s6,plain,
spl36_2,
inference(rat,[],[s5]) ).
cnf(s51,plain,
( spl36_24
| spl36_30 ),
inference(sat_conversion,[],[f730]) ).
cnf(s52,plain,
( spl36_24
| spl36_31
| spl36_32 ),
inference(sat_conversion,[],[f739]) ).
cnf(s53,plain,
( spl36_24
| spl36_32
| spl36_33 ),
inference(sat_conversion,[],[f744]) ).
cnf(s54,plain,
( spl36_24
| spl36_31
| spl36_34 ),
inference(sat_conversion,[],[f749]) ).
cnf(s55,plain,
( spl36_24
| spl36_33
| spl36_34 ),
inference(sat_conversion,[],[f750]) ).
cnf(s64,plain,
( spl36_24
| spl36_38
| spl36_41 ),
inference(sat_conversion,[],[f787]) ).
cnf(s65,plain,
( spl36_24
| spl36_38
| spl36_42 ),
inference(sat_conversion,[],[f792]) ).
cnf(s66,plain,
( spl36_24
| spl36_40
| spl36_41 ),
inference(sat_conversion,[],[f793]) ).
cnf(s67,plain,
( spl36_24
| spl36_40
| spl36_42 ),
inference(sat_conversion,[],[f794]) ).
cnf(s68,plain,
( spl36_30
| spl36_43 ),
inference(sat_conversion,[],[f799]) ).
cnf(s69,plain,
( spl36_30
| spl36_44 ),
inference(sat_conversion,[],[f804]) ).
cnf(s70,plain,
( spl36_43
| spl36_45
| spl36_46 ),
inference(sat_conversion,[],[f813]) ).
cnf(s71,plain,
( spl36_43
| spl36_46
| spl36_47 ),
inference(sat_conversion,[],[f818]) ).
cnf(s72,plain,
( spl36_43
| spl36_45
| spl36_48 ),
inference(sat_conversion,[],[f823]) ).
cnf(s73,plain,
( spl36_43
| spl36_47
| spl36_48 ),
inference(sat_conversion,[],[f824]) ).
cnf(s74,plain,
( spl36_44
| spl36_45
| spl36_46 ),
inference(sat_conversion,[],[f825]) ).
cnf(s75,plain,
( spl36_44
| spl36_46
| spl36_47 ),
inference(sat_conversion,[],[f826]) ).
cnf(s76,plain,
( spl36_44
| spl36_45
| spl36_48 ),
inference(sat_conversion,[],[f827]) ).
cnf(s77,plain,
( spl36_44
| spl36_47
| spl36_48 ),
inference(sat_conversion,[],[f828]) ).
cnf(s94,plain,
( spl36_43
| spl36_52
| spl36_55 ),
inference(sat_conversion,[],[f873]) ).
cnf(s95,plain,
( spl36_43
| spl36_52
| spl36_56 ),
inference(sat_conversion,[],[f878]) ).
cnf(s96,plain,
( spl36_43
| spl36_54
| spl36_55 ),
inference(sat_conversion,[],[f879]) ).
cnf(s97,plain,
( spl36_43
| spl36_54
| spl36_56 ),
inference(sat_conversion,[],[f880]) ).
cnf(s98,plain,
( spl36_44
| spl36_52
| spl36_55 ),
inference(sat_conversion,[],[f881]) ).
cnf(s99,plain,
( spl36_44
| spl36_52
| spl36_56 ),
inference(sat_conversion,[],[f882]) ).
cnf(s100,plain,
( spl36_44
| spl36_54
| spl36_55 ),
inference(sat_conversion,[],[f883]) ).
cnf(s101,plain,
( spl36_44
| spl36_54
| spl36_56 ),
inference(sat_conversion,[],[f884]) ).
cnf(s102,plain,
( spl36_30
| spl36_57 ),
inference(sat_conversion,[],[f889]) ).
cnf(s103,plain,
( spl36_30
| spl36_58
| spl36_59 ),
inference(sat_conversion,[],[f898]) ).
cnf(s104,plain,
( spl36_57
| spl36_60
| spl36_61 ),
inference(sat_conversion,[],[f907]) ).
cnf(s105,plain,
( spl36_57
| spl36_61
| spl36_62 ),
inference(sat_conversion,[],[f912]) ).
cnf(s106,plain,
( spl36_57
| spl36_60
| spl36_63 ),
inference(sat_conversion,[],[f917]) ).
cnf(s107,plain,
( spl36_57
| spl36_62
| spl36_63 ),
inference(sat_conversion,[],[f918]) ).
cnf(s108,plain,
( spl36_58
| spl36_59
| spl36_60
| spl36_61 ),
inference(sat_conversion,[],[f919]) ).
cnf(s109,plain,
( spl36_58
| spl36_59
| spl36_61
| spl36_62 ),
inference(sat_conversion,[],[f920]) ).
cnf(s110,plain,
( spl36_58
| spl36_59
| spl36_60
| spl36_63 ),
inference(sat_conversion,[],[f921]) ).
cnf(s111,plain,
( spl36_58
| spl36_59
| spl36_62
| spl36_63 ),
inference(sat_conversion,[],[f922]) ).
cnf(s128,plain,
( spl36_57
| spl36_67
| spl36_70 ),
inference(sat_conversion,[],[f967]) ).
cnf(s129,plain,
( spl36_57
| spl36_67
| spl36_71 ),
inference(sat_conversion,[],[f972]) ).
cnf(s130,plain,
( spl36_57
| spl36_69
| spl36_70 ),
inference(sat_conversion,[],[f973]) ).
cnf(s131,plain,
( spl36_57
| spl36_69
| spl36_71 ),
inference(sat_conversion,[],[f974]) ).
cnf(s132,plain,
( spl36_58
| spl36_59
| spl36_67
| spl36_70 ),
inference(sat_conversion,[],[f975]) ).
cnf(s133,plain,
( spl36_58
| spl36_59
| spl36_67
| spl36_71 ),
inference(sat_conversion,[],[f976]) ).
cnf(s134,plain,
( spl36_58
| spl36_59
| spl36_69
| spl36_70 ),
inference(sat_conversion,[],[f977]) ).
cnf(s135,plain,
( spl36_58
| spl36_59
| spl36_69
| spl36_71 ),
inference(sat_conversion,[],[f978]) ).
cnf(s151,plain,
( ~ spl36_57
| ~ spl36_58
| ~ spl36_79 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s153,plain,
( ~ spl36_43
| ~ spl36_44
| ~ spl36_80 ),
inference(sat_conversion,[],[f1147]) ).
cnf(s165,plain,
( ~ spl36_57
| ~ spl36_59
| ~ spl36_84 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s170,plain,
( ~ spl36_1
| ~ spl36_30
| spl36_87
| spl36_88 ),
inference(sat_conversion,[],[f1476]) ).
cnf(s171,plain,
( ~ spl36_2
| ~ spl36_30
| spl36_88
| spl36_89 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s189,plain,
( ~ spl36_61
| ~ spl36_63
| ~ spl36_88 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s191,plain,
( ~ spl36_67
| ~ spl36_69
| ~ spl36_89 ),
inference(sat_conversion,[],[f1824]) ).
cnf(s199,plain,
( ~ spl36_70
| ~ spl36_71
| ~ spl36_87 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s213,plain,
( ~ spl36_38
| ~ spl36_40
| ~ spl36_89 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s249,plain,
( ~ spl36_60
| ~ spl36_62
| ~ spl36_88 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s250,plain,
( ~ spl36_46
| ~ spl36_48
| ~ spl36_88 ),
inference(sat_conversion,[],[f2893]) ).
cnf(s251,plain,
( ~ spl36_32
| ~ spl36_34
| ~ spl36_88 ),
inference(sat_conversion,[],[f2896]) ).
cnf(s295,plain,
( ~ spl36_31
| ~ spl36_33
| ~ spl36_88 ),
inference(sat_conversion,[],[f3202]) ).
cnf(s335,plain,
( ~ spl36_2
| ~ spl36_57
| ~ spl36_59
| spl36_80
| spl36_115 ),
inference(sat_conversion,[],[f3320]) ).
cnf(s338,plain,
( ~ spl36_1
| ~ spl36_24
| spl36_79
| spl36_80 ),
inference(sat_conversion,[],[f3391]) ).
cnf(s339,plain,
( ~ spl36_2
| ~ spl36_24
| spl36_80
| spl36_84 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s341,plain,
( ~ spl36_24
| ~ spl36_115 ),
inference(sat_conversion,[],[f3425]) ).
cnf(s359,plain,
( ~ spl36_45
| ~ spl36_47
| ~ spl36_88 ),
inference(sat_conversion,[],[f4238]) ).
cnf(s390,plain,
( ~ spl36_41
| ~ spl36_42
| ~ spl36_87 ),
inference(sat_conversion,[],[f4592]) ).
cnf(s405,plain,
( ~ spl36_52
| ~ spl36_54
| ~ spl36_89 ),
inference(sat_conversion,[],[f4735]) ).
cnf(s413,plain,
( ~ spl36_55
| ~ spl36_56
| ~ spl36_87 ),
inference(sat_conversion,[],[f4933]) ).
cnf(s425,plain,
( spl36_40
| ~ spl36_87
| spl36_24 ),
inference(rat,[],[s390,s66,s67]) ).
cnf(s426,plain,
( spl36_88
| spl36_24 ),
inference(rat,[],[s390,s64,s65,s213,s425,s170,s171,s51,s2,s6]) ).
cnf(s428,plain,
( spl36_34
| spl36_24 ),
inference(rat,[],[s295,s54,s55,s426]) ).
cnf(s429,plain,
spl36_24,
inference(rat,[],[s295,s52,s53,s251,s428,s426]) ).
cnf(s430,plain,
~ spl36_115,
inference(rat,[],[s341,s429]) ).
cnf(s432,plain,
( spl36_54
| spl36_44
| ~ spl36_87 ),
inference(rat,[],[s413,s100,s101]) ).
cnf(s434,plain,
( spl36_54
| spl36_43
| ~ spl36_87 ),
inference(rat,[],[s413,s96,s97]) ).
cnf(s435,plain,
( spl36_43
| ~ spl36_87
| ~ spl36_89 ),
inference(rat,[],[s413,s95,s94,s405,s434]) ).
cnf(s437,plain,
( spl36_69
| spl36_57
| ~ spl36_87 ),
inference(rat,[],[s199,s130,s131]) ).
cnf(s438,plain,
( spl36_57
| ~ spl36_87
| ~ spl36_89 ),
inference(rat,[],[s199,s128,s129,s191,s437]) ).
cnf(s439,plain,
( spl36_69
| spl36_58
| spl36_59
| ~ spl36_87 ),
inference(rat,[],[s199,s134,s135]) ).
cnf(s440,plain,
( spl36_80
| ~ spl36_87
| ~ spl36_89 ),
inference(rat,[],[s199,s132,s133,s191,s439,s151,s165,s338,s339,s438,s2,s429,s6]) ).
cnf(s441,plain,
( ~ spl36_87
| ~ spl36_89 ),
inference(rat,[],[s413,s99,s98,s405,s432,s153,s440,s435]) ).
cnf(s442,plain,
( ~ spl36_30
| spl36_88 ),
inference(rat,[],[s441,s170,s171,s6,s2]) ).
cnf(s443,plain,
spl36_30,
inference(rat,[],[s103,s151,s335,s338,s153,s68,s69,s102,s6,s430,s2,s429]) ).
cnf(s444,plain,
spl36_88,
inference(rat,[],[s442,s443]) ).
cnf(s448,plain,
( spl36_45
| spl36_44 ),
inference(rat,[],[s250,s74,s76,s444]) ).
cnf(s449,plain,
( spl36_47
| spl36_44 ),
inference(rat,[],[s250,s75,s77,s444]) ).
cnf(s450,plain,
spl36_44,
inference(rat,[],[s449,s359,s448,s444]) ).
cnf(s451,plain,
( spl36_48
| spl36_43 ),
inference(rat,[],[s359,s72,s73,s444]) ).
cnf(s452,plain,
( spl36_46
| spl36_43 ),
inference(rat,[],[s359,s70,s71,s444]) ).
cnf(s453,plain,
spl36_43,
inference(rat,[],[s452,s250,s451,s444]) ).
cnf(s454,plain,
~ spl36_80,
inference(rat,[],[s153,s450,s453]) ).
cnf(s456,plain,
spl36_79,
inference(rat,[],[s338,s429,s2,s454]) ).
cnf(s463,plain,
( spl36_60
| spl36_57 ),
inference(rat,[],[s189,s104,s106,s444]) ).
cnf(s464,plain,
( spl36_62
| spl36_57 ),
inference(rat,[],[s189,s105,s107,s444]) ).
cnf(s465,plain,
spl36_57,
inference(rat,[],[s464,s249,s463,s444]) ).
cnf(s466,plain,
~ spl36_59,
inference(rat,[],[s335,s430,s454,s6,s465]) ).
cnf(s469,plain,
~ spl36_58,
inference(rat,[],[s151,s456,s465]) ).
cnf(s474,plain,
spl36_63,
inference(rat,[],[s249,s110,s111,s444,s466,s469]) ).
cnf(s475,plain,
~ spl36_61,
inference(rat,[],[s189,s444,s474]) ).
cnf(s478,plain,
spl36_62,
inference(rat,[],[s109,s469,s466,s475]) ).
cnf(s479,plain,
spl36_60,
inference(rat,[],[s108,s469,s466,s475]) ).
cnf(s481,plain,
$false,
inference(rat,[],[s249,s444,s478,s479]) ).
thf(f4948,plain,
$false,
inference(avatar_sat_refutation,[],[s481]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN045^4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n017.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 16:09:52 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.06/0.49 % (523520)Will run a generic schedule for satisfiability detection.
% 1.06/0.49 % (523527)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3599471661:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.06/0.49 % (523526)% WARNING: option uhcvi not known.
% 1.06/0.49 % (523526)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1898080657:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.06/0.49 % (523529)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2756755039:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.06/0.49 % (523528)dis+10_1_sil=32000:sp=arity:random_seed=2510289667:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.06/0.49 % (523525)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2735438765_2999 on theBenchmark for (2999ds/0Mi)
% 1.06/0.49 % (523530)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3700610856:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.06/0.49 % (523526)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.06/0.49 % (523529)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.06/0.49 % (523526)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.06/0.49 % Exception at run slice level
% 1.06/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.06/0.49 % (523531)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=87609486:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.06/0.49 % (523538)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3456926045:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.06/0.49 % Exception at run slice level
% 1.06/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.06/0.49 % (523541)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3089663316:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.06/0.49 % (523528)Instruction limit reached!
% 1.06/0.49 % (523528)------------------------------
% 1.06/0.49 % (523528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523528)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523528)Termination reason: Instruction limit
% 1.06/0.49 % (523528)Termination phase: Saturation
% 1.06/0.49 % (523528)Time elapsed: 0.047 s
% 1.06/0.49 % (523528)Peak memory usage: 12 MB
% 1.06/0.49 % (523528)Instructions burned: 104 (million)
% 1.06/0.49 % (523529)Instruction limit reached!
% 1.06/0.49 % (523529)------------------------------
% 1.06/0.49 % (523529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523529)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523529)Termination reason: Instruction limit
% 1.06/0.49 % (523529)Termination phase: Saturation
% 1.06/0.49 % (523529)Time elapsed: 0.053 s
% 1.06/0.49 % (523529)Peak memory usage: 12 MB
% 1.06/0.49 % (523529)Instructions burned: 116 (million)
% 1.06/0.49 % (523530)Instruction limit reached!
% 1.06/0.49 % (523530)------------------------------
% 1.06/0.49 % (523530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523530)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523530)Termination reason: Instruction limit
% 1.06/0.49 % (523530)Termination phase: Saturation
% 1.06/0.49 % (523530)Time elapsed: 0.059 s
% 1.06/0.49 % (523530)Peak memory usage: 12 MB
% 1.06/0.49 % (523530)Instructions burned: 131 (million)
% 1.06/0.49 % (523543)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2392264979:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.06/0.49 % (523543)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.06/0.49 % (523543)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.06/0.49 % (523544)ott-21_1_sil=16000:fs=off:random_seed=1490185706:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.06/0.49 % (523545)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=85521489:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.06/0.49 % (523531)Instruction limit reached!
% 1.06/0.49 % (523531)------------------------------
% 1.06/0.49 % (523531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523531)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523531)Termination reason: Instruction limit
% 1.06/0.49 % (523531)Termination phase: Saturation
% 1.06/0.49 % (523531)Time elapsed: 0.080 s
% 1.06/0.49 % (523531)Peak memory usage: 13 MB
% 1.06/0.49 % (523531)Instructions burned: 160 (million)
% 1.06/0.49 % (523541)Instruction limit reached!
% 1.06/0.49 % (523541)------------------------------
% 1.06/0.49 % (523541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523541)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523541)Termination reason: Instruction limit
% 1.06/0.49 % (523541)Termination phase: Saturation
% 1.06/0.49 % (523541)Time elapsed: 0.061 s
% 1.06/0.49 % (523541)Peak memory usage: 12 MB
% 1.06/0.49 % (523541)Instructions burned: 132 (million)
% 1.06/0.49 % (523550)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2622950012:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.06/0.49 % (523549)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3758010002:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.06/0.49 % Exception at run slice level
% 1.06/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.06/0.49 % (523553)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1925137165:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.06/0.49 % Exception at run slice level
% 1.06/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.06/0.49 % (523544)Instruction limit reached!
% 1.06/0.49 % (523544)------------------------------
% 1.06/0.49 % (523544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523544)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523544)Termination reason: Instruction limit
% 1.06/0.49 % (523544)Termination phase: Saturation
% 1.06/0.49 % (523544)Time elapsed: 0.090 s
% 1.06/0.49 % (523544)Peak memory usage: 13 MB
% 1.06/0.49 % (523544)Instructions burned: 180 (million)
% 1.06/0.49 % (523555)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1730271692:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.06/0.49 % (523555)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.06/0.49 % (523556)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=366028766:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 1.06/0.49 % (523556)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.06/0.49 % (523543) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-523520-523543"...
% 1.06/0.49 % (523543)...printing done.
% 1.06/0.49 % (523543)Refutation found. Thanks to Tanya!
% 1.06/0.49 % SZS status Theorem for theBenchmark
% 1.06/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 1.06/0.49 % (523543)------------------------------
% 1.06/0.49 % (523543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.06/0.49 % (523543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.06/0.49 % (523543)CaDiCaL version: 2.1.3
% 1.06/0.49 % (523543)Termination reason: Refutation
% 1.06/0.49 % (523543)Time elapsed: 0.152 s
% 1.06/0.49 % (523543)Peak memory usage: 14 MB
% 1.06/0.49 % (523543)Instructions burned: 329 (million)
% 1.06/0.49 % (523520)Success in time 0.253 s
% 1.06/0.49 % Vampire exiting
%------------------------------------------------------------------------------