%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GEG014^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 07:49:29 AM UTC 2026
% Result : Theorem 265.96s 37.76s
% Output : Refutation 265.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 15
% Syntax : Number of formulae : 150 ( 72 unt; 0 typ; 3 def)
% Number of atoms : 1452 ( 240 equ; 0 cnn)
% Maximal formula atoms : 6 ( 9 avg)
% Number of connectives : 2900 ( 120 ~; 145 |; 180 &;1986 @)
% ( 3 <=>; 193 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 4 ( 2 usr)
% Number of type conns : 24 ( 24 >; 0 *; 0 +; 0 <<)
% Number of symbols : 89 ( 84 usr; 16 con; 0-4 aty)
% ( 192 !!; 81 ??; 0 @@+; 0 @@-)
% Number of variables : 673 ( 12 sgn 193 !; 10 ?; 673 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
mu: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_7,type,
reg: $tType ).
thf(func_def_0,type,
meq_ind: mu > mu > $i > $o ).
thf(func_def_1,type,
meq_prop: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_3,type,
mnot: ( $i > $o ) > $i > $o ).
thf(func_def_4,type,
mor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_5,type,
mand: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_6,type,
mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_7,type,
mimplied: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_8,type,
mequiv: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_9,type,
mxor: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_10,type,
mforall_ind: ( mu > $i > $o ) > $i > $o ).
thf(func_def_11,type,
mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_12,type,
mexists_ind: ( mu > $i > $o ) > $i > $o ).
thf(func_def_13,type,
mexists_prop: ( ( $i > $o ) > $i > $o ) > $i > $o ).
thf(func_def_14,type,
mtrue: $i > $o ).
thf(func_def_15,type,
mfalse: $i > $o ).
thf(func_def_16,type,
mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_17,type,
mdia: ( $i > $i > $o ) > ( $i > $o ) > $i > $o ).
thf(func_def_18,type,
mreflexive: ( $i > $i > $o ) > $o ).
thf(func_def_19,type,
msymmetric: ( $i > $i > $o ) > $o ).
thf(func_def_20,type,
mserial: ( $i > $i > $o ) > $o ).
thf(func_def_21,type,
mtransitive: ( $i > $i > $o ) > $o ).
thf(func_def_22,type,
meuclidean: ( $i > $i > $o ) > $o ).
thf(func_def_23,type,
mpartially_functional: ( $i > $i > $o ) > $o ).
thf(func_def_24,type,
mfunctional: ( $i > $i > $o ) > $o ).
thf(func_def_25,type,
mweakly_dense: ( $i > $i > $o ) > $o ).
thf(func_def_26,type,
mweakly_connected: ( $i > $i > $o ) > $o ).
thf(func_def_27,type,
mweakly_directed: ( $i > $i > $o ) > $o ).
thf(func_def_28,type,
mvalid: ( $i > $o ) > $o ).
thf(func_def_29,type,
minvalid: ( $i > $o ) > $o ).
thf(func_def_30,type,
msatisfiable: ( $i > $o ) > $o ).
thf(func_def_31,type,
mcountersatisfiable: ( $i > $o ) > $o ).
thf(func_def_32,type,
c: reg > reg > $o ).
thf(func_def_33,type,
dc: reg > reg > $o ).
thf(func_def_34,type,
p: reg > reg > $o ).
thf(func_def_35,type,
eq: reg > reg > $o ).
thf(func_def_36,type,
o: reg > reg > $o ).
thf(func_def_37,type,
po: reg > reg > $o ).
thf(func_def_38,type,
ec: reg > reg > $o ).
thf(func_def_39,type,
pp: reg > reg > $o ).
thf(func_def_40,type,
tpp: reg > reg > $o ).
thf(func_def_41,type,
ntpp: reg > reg > $o ).
thf(func_def_42,type,
catalunya: reg ).
thf(func_def_43,type,
france: reg ).
thf(func_def_44,type,
spain: reg ).
thf(func_def_45,type,
paris: reg ).
thf(func_def_46,type,
a: $i > $i > $o ).
thf(func_def_47,type,
fool: $i > $i > $o ).
thf(func_def_48,type,
vOR: $o > $o > $o ).
thf(func_def_49,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_50,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_51,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_52,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_53,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_56,type,
vIMP: $o > $o > $o ).
thf(func_def_57,type,
vAND: $o > $o > $o ).
thf(func_def_58,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_59,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_60,type,
vNOT: $o > $o ).
thf(func_def_61,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_62,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_63,type,
sK0: $i > ( $i > $o ) > $i ).
thf(func_def_66,type,
sK3: reg > reg > reg ).
thf(func_def_67,type,
sK4: reg > reg ).
thf(func_def_68,type,
sK5: reg > reg > reg ).
thf(func_def_69,type,
sK6: reg > reg ).
thf(func_def_70,type,
sK7: reg > reg ).
thf(func_def_71,type,
sK8: reg > reg ).
thf(func_def_72,type,
sK9: reg ).
thf(func_def_73,type,
sK10: $i > ( $i > $o ) > $i ).
thf(func_def_74,type,
sK11: reg > reg ).
thf(func_def_75,type,
sK12: reg > reg ).
thf(func_def_76,type,
sK13: $i > ( $i > $o ) > $i ).
thf(func_def_77,type,
sK14: reg ).
thf(func_def_78,type,
sK15: reg > reg ).
thf(func_def_79,type,
sK16: reg > reg ).
thf(func_def_80,type,
sK17: reg > reg ).
thf(func_def_81,type,
sK18: reg > reg ).
thf(func_def_82,type,
sK19: reg ).
thf(f16,axiom,
( ( ^ [X0: $i > $i > $o,X1: $i > $o,X2: $i] :
! [X3: $i] :
( ~ ( X0 @ X2 @ X3 )
| ( X1 @ X3 ) ) )
= mbox ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mbox) ).
thf(f28,axiom,
( mvalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL013^0.ax',mvalid) ).
thf(f32,axiom,
! [X0: reg] : ( c @ X0 @ X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',c_reflexive) ).
thf(f33,axiom,
! [X0: reg,X1: reg] :
( ( c @ X0 @ X1 )
=> ( c @ X1 @ X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',c_symmetric) ).
thf(f35,axiom,
( ( ^ [X0: reg,X1: reg] :
! [X2: reg] :
( ( c @ X2 @ X0 )
=> ( c @ X2 @ X1 ) ) )
= p ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',p) ).
thf(f36,axiom,
( ( ^ [X0: reg,X1: reg] :
( ( p @ X1 @ X0 )
& ( p @ X0 @ X1 ) ) )
= eq ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',eq) ).
thf(f37,axiom,
( ( ^ [X0: reg,X1: reg] :
? [X2: reg] :
( ( p @ X2 @ X0 )
& ( p @ X2 @ X1 ) ) )
= o ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',o) ).
thf(f39,axiom,
( ( ^ [X0: reg,X1: reg] :
( ~ ( o @ X0 @ X1 )
& ( c @ X0 @ X1 ) ) )
= ec ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',ec) ).
thf(f40,axiom,
( pp
= ( ^ [X0: reg,X1: reg] :
( ~ ( p @ X1 @ X0 )
& ( p @ X0 @ X1 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',pp) ).
thf(f42,axiom,
( ntpp
= ( ^ [X0: reg,X1: reg] :
( ( pp @ X0 @ X1 )
& ~ ? [X2: reg] :
( ( ec @ X2 @ X1 )
& ( ec @ X2 @ X0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/LCL014^0.ax',ntpp) ).
thf(f48,axiom,
( mvalid
@ ( mbox @ a
@ ^ [X0: $i] : ( ntpp @ paris @ france ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
thf(f49,conjecture,
( mvalid
@ ( mbox @ a
@ ^ [X0: $i] :
? [X1: reg,X2: reg] :
( ~ ( eq @ X1 @ X2 )
& ( o @ X1 @ france )
& ( o @ X1 @ france ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con) ).
thf(f50,negated_conjecture,
~ ( mvalid
@ ( mbox @ a
@ ^ [X0: $i] :
? [X1: reg,X2: reg] :
( ~ ( eq @ X1 @ X2 )
& ( o @ X1 @ france )
& ( o @ X1 @ france ) ) ) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
thf(f55,plain,
! [X0: reg] : ( c @ X0 @ X0 ),
inference(rectify,[],[f32]) ).
thf(f56,plain,
! [X0: reg] :
( ( c @ X0 @ X0 )
= $true ),
inference(fool_elimination,[],[f55]) ).
thf(f59,plain,
( ( ^ [X0: reg,X1: reg] :
( ~ ( o @ X0 @ X1 )
& ( c @ X0 @ X1 ) ) )
= ec ),
inference(rectify,[],[f39]) ).
thf(f60,plain,
( ec
= ( ^ [Y0: reg,Y1: reg] :
( ( c @ Y0 @ Y1 )
& ~ ( o @ Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f59]) ).
thf(f65,plain,
( pp
= ( ^ [X0: reg,X1: reg] :
( ~ ( p @ X1 @ X0 )
& ( p @ X0 @ X1 ) ) ) ),
inference(rectify,[],[f40]) ).
thf(f66,plain,
( pp
= ( ^ [Y0: reg,Y1: reg] :
( ( p @ Y0 @ Y1 )
& ~ ( p @ Y1 @ Y0 ) ) ) ),
inference(fool_elimination,[],[f65]) ).
thf(f68,plain,
( ( ^ [X0: reg,X1: reg] :
! [X2: reg] :
( ( c @ X2 @ X0 )
=> ( c @ X2 @ X1 ) ) )
= p ),
inference(rectify,[],[f35]) ).
thf(f69,plain,
( p
= ( ^ [Y0: reg,Y1: reg] :
( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y0 )
=> ( c @ Y2 @ Y1 ) ) ) ) ),
inference(fool_elimination,[],[f68]) ).
thf(f75,plain,
~ ( mvalid
@ ( mbox @ a
@ ^ [X0: $i] :
? [X1: reg,X2: reg] :
( ~ ( eq @ X1 @ X2 )
& ( o @ X1 @ france )
& ( o @ X1 @ france ) ) ) ),
inference(rectify,[],[f50]) ).
thf(f76,plain,
( ( mvalid
@ ( mbox @ a
@ ^ [Y0: $i] :
( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( o @ Y2 @ france )
& ( o @ Y2 @ france )
& ~ ( eq @ Y2 @ Y1 ) ) ) ) ) )
!= $true ),
inference(fool_elimination,[],[f75]) ).
thf(f99,plain,
( ntpp
= ( ^ [X0: reg,X1: reg] :
( ( pp @ X0 @ X1 )
& ~ ? [X2: reg] :
( ( ec @ X2 @ X1 )
& ( ec @ X2 @ X0 ) ) ) ) ),
inference(rectify,[],[f42]) ).
thf(f100,plain,
( ntpp
= ( ^ [Y0: reg,Y1: reg] :
( ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( ec @ Y2 @ Y0 )
& ( ec @ Y2 @ Y1 ) ) )
& ( pp @ Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f99]) ).
thf(f109,plain,
( ( ^ [X0: $i > $i > $o,X1: $i > $o,X2: $i] :
! [X3: $i] :
( ~ ( X0 @ X2 @ X3 )
| ( X1 @ X3 ) ) )
= mbox ),
inference(rectify,[],[f16]) ).
thf(f110,plain,
( mbox
= ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( Y0 @ Y2 @ Y3 ) ) ) ) ),
inference(fool_elimination,[],[f109]) ).
thf(f114,plain,
( mvalid
= ( ^ [X0: $i > $o] :
! [X1: $i] : ( X0 @ X1 ) ) ),
inference(rectify,[],[f28]) ).
thf(f115,plain,
( mvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(fool_elimination,[],[f114]) ).
thf(f119,plain,
( ( ^ [X0: reg,X1: reg] :
? [X2: reg] :
( ( p @ X2 @ X0 )
& ( p @ X2 @ X1 ) ) )
= o ),
inference(rectify,[],[f37]) ).
thf(f120,plain,
( o
= ( ^ [Y0: reg,Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( p @ Y2 @ Y1 )
& ( p @ Y2 @ Y0 ) ) ) ) ),
inference(fool_elimination,[],[f119]) ).
thf(f121,plain,
( mvalid
@ ( mbox @ a
@ ^ [X0: $i] : ( ntpp @ paris @ france ) ) ),
inference(rectify,[],[f48]) ).
thf(f122,plain,
( $true
= ( mvalid
@ ( mbox @ a
@ ^ [Y0: $i] : ( ntpp @ paris @ france ) ) ) ),
inference(fool_elimination,[],[f121]) ).
thf(f127,plain,
! [X0: reg,X1: reg] :
( ( c @ X0 @ X1 )
=> ( c @ X1 @ X0 ) ),
inference(rectify,[],[f33]) ).
thf(f128,plain,
! [X1: reg,X0: reg] :
( ( ( c @ X0 @ X1 )
= $true )
=> ( ( c @ X1 @ X0 )
= $true ) ),
inference(fool_elimination,[],[f127]) ).
thf(f130,plain,
( ( ^ [X0: reg,X1: reg] :
( ( p @ X1 @ X0 )
& ( p @ X0 @ X1 ) ) )
= eq ),
inference(rectify,[],[f36]) ).
thf(f131,plain,
( eq
= ( ^ [Y0: reg,Y1: reg] :
( ( p @ Y0 @ Y1 )
& ( p @ Y1 @ Y0 ) ) ) ),
inference(fool_elimination,[],[f130]) ).
thf(f138,plain,
( ( mvalid
@ ( mbox @ a
@ ^ [Y0: $i] :
( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( o @ Y2 @ france )
& ( o @ Y2 @ france )
& ~ ( eq @ Y2 @ Y1 ) ) ) ) ) )
!= $true ),
inference(flattening,[],[f76]) ).
thf(f139,plain,
! [X1: reg,X0: reg] :
( ( ( c @ X1 @ X0 )
= $true )
| ( ( c @ X0 @ X1 )
!= $true ) ),
inference(ennf_transformation,[],[f128]) ).
thf(f140,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( ( c @ X1 @ X0 )
!= $true ) ),
inference(rectify,[],[f139]) ).
thf(f148,plain,
( ntpp
= ( ^ [Y0: reg,Y1: reg] :
( ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( ec @ Y2 @ Y0 )
& ( ec @ Y2 @ Y1 ) ) )
& ( pp @ Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f100]) ).
thf(f150,plain,
( p
= ( ^ [Y0: reg,Y1: reg] :
( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y0 )
=> ( c @ Y2 @ Y1 ) ) ) ) ),
inference(cnf_transformation,[],[f69]) ).
thf(f155,plain,
( $true
= ( mvalid
@ ( mbox @ a
@ ^ [Y0: $i] : ( ntpp @ paris @ france ) ) ) ),
inference(cnf_transformation,[],[f122]) ).
thf(f158,plain,
( mvalid
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f115]) ).
thf(f164,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X1 @ X0 )
!= $true )
| ( ( c @ X0 @ X1 )
= $true ) ),
inference(cnf_transformation,[],[f140]) ).
thf(f166,plain,
( pp
= ( ^ [Y0: reg,Y1: reg] :
( ( p @ Y0 @ Y1 )
& ~ ( p @ Y1 @ Y0 ) ) ) ),
inference(cnf_transformation,[],[f66]) ).
thf(f167,plain,
( ec
= ( ^ [Y0: reg,Y1: reg] :
( ( c @ Y0 @ Y1 )
& ~ ( o @ Y0 @ Y1 ) ) ) ),
inference(cnf_transformation,[],[f60]) ).
thf(f170,plain,
( o
= ( ^ [Y0: reg,Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( p @ Y2 @ Y1 )
& ( p @ Y2 @ Y0 ) ) ) ) ),
inference(cnf_transformation,[],[f120]) ).
thf(f175,plain,
! [X0: reg] :
( ( c @ X0 @ X0 )
= $true ),
inference(cnf_transformation,[],[f56]) ).
thf(f177,plain,
( eq
= ( ^ [Y0: reg,Y1: reg] :
( ( p @ Y0 @ Y1 )
& ( p @ Y1 @ Y0 ) ) ) ),
inference(cnf_transformation,[],[f131]) ).
thf(f181,plain,
( mbox
= ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( Y0 @ Y2 @ Y3 ) ) ) ) ),
inference(cnf_transformation,[],[f110]) ).
thf(f184,plain,
( ( mvalid
@ ( mbox @ a
@ ^ [Y0: $i] :
( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( o @ Y2 @ france )
& ( o @ Y2 @ france )
& ~ ( eq @ Y2 @ Y1 ) ) ) ) ) )
!= $true ),
inference(cnf_transformation,[],[f138]) ).
thf(f201,plain,
( eq
= ( ^ [Y0: reg,Y1: reg] :
( ( ^ [Y2: reg,Y3: reg] :
( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) )
@ Y0
@ Y1 )
& ( ^ [Y2: reg,Y3: reg] :
( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) )
@ Y1
@ Y0 ) ) ) ),
inference(definition_unfolding,[],[f177,f150,f150]) ).
thf(f202,plain,
( o
= ( ^ [Y0: reg,Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( ^ [Y3: reg,Y4: reg] :
( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y3 )
=> ( c @ Y5 @ Y4 ) ) )
@ Y2
@ Y1 )
& ( ^ [Y3: reg,Y4: reg] :
( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y3 )
=> ( c @ Y5 @ Y4 ) ) )
@ Y2
@ Y0 ) ) ) ) ),
inference(definition_unfolding,[],[f170,f150,f150]) ).
thf(f204,plain,
( ec
= ( ^ [Y0: reg,Y1: reg] :
( ( c @ Y0 @ Y1 )
& ~ ( ^ [Y2: reg,Y3: reg] :
( ?? @ reg
@ ^ [Y4: reg] :
( ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y4
@ Y3 )
& ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y4
@ Y2 ) ) )
@ Y0
@ Y1 ) ) ) ),
inference(definition_unfolding,[],[f167,f202]) ).
thf(f205,plain,
( pp
= ( ^ [Y0: reg,Y1: reg] :
( ( ^ [Y2: reg,Y3: reg] :
( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) )
@ Y0
@ Y1 )
& ~ ( ^ [Y2: reg,Y3: reg] :
( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) )
@ Y1
@ Y0 ) ) ) ),
inference(definition_unfolding,[],[f166,f150,f150]) ).
thf(f207,plain,
( ntpp
= ( ^ [Y0: reg,Y1: reg] :
( ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( ^ [Y3: reg,Y4: reg] :
( ( c @ Y3 @ Y4 )
& ~ ( ^ [Y5: reg,Y6: reg] :
( ?? @ reg
@ ^ [Y7: reg] :
( ( ^ [Y8: reg,Y9: reg] :
( !! @ reg
@ ^ [Y10: reg] :
( ( c @ Y10 @ Y8 )
=> ( c @ Y10 @ Y9 ) ) )
@ Y7
@ Y6 )
& ( ^ [Y8: reg,Y9: reg] :
( !! @ reg
@ ^ [Y10: reg] :
( ( c @ Y10 @ Y8 )
=> ( c @ Y10 @ Y9 ) ) )
@ Y7
@ Y5 ) ) )
@ Y3
@ Y4 ) )
@ Y2
@ Y0 )
& ( ^ [Y3: reg,Y4: reg] :
( ( c @ Y3 @ Y4 )
& ~ ( ^ [Y5: reg,Y6: reg] :
( ?? @ reg
@ ^ [Y7: reg] :
( ( ^ [Y8: reg,Y9: reg] :
( !! @ reg
@ ^ [Y10: reg] :
( ( c @ Y10 @ Y8 )
=> ( c @ Y10 @ Y9 ) ) )
@ Y7
@ Y6 )
& ( ^ [Y8: reg,Y9: reg] :
( !! @ reg
@ ^ [Y10: reg] :
( ( c @ Y10 @ Y8 )
=> ( c @ Y10 @ Y9 ) ) )
@ Y7
@ Y5 ) ) )
@ Y3
@ Y4 ) )
@ Y2
@ Y1 ) ) )
& ( ^ [Y2: reg,Y3: reg] :
( ( ^ [Y4: reg,Y5: reg] :
( !! @ reg
@ ^ [Y6: reg] :
( ( c @ Y6 @ Y4 )
=> ( c @ Y6 @ Y5 ) ) )
@ Y2
@ Y3 )
& ~ ( ^ [Y4: reg,Y5: reg] :
( !! @ reg
@ ^ [Y6: reg] :
( ( c @ Y6 @ Y4 )
=> ( c @ Y6 @ Y5 ) ) )
@ Y3
@ Y2 ) )
@ Y0
@ Y1 ) ) ) ),
inference(definition_unfolding,[],[f148,f204,f204,f205]) ).
thf(f209,plain,
( $true
= ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( Y0 @ Y2 @ Y3 ) ) )
@ a
@ ^ [Y0: $i] :
( ^ [Y1: reg,Y2: reg] :
( ~ ( ?? @ reg
@ ^ [Y3: reg] :
( ( ^ [Y4: reg,Y5: reg] :
( ( c @ Y4 @ Y5 )
& ~ ( ^ [Y6: reg,Y7: reg] :
( ?? @ reg
@ ^ [Y8: reg] :
( ( ^ [Y9: reg,Y10: reg] :
( !! @ reg
@ ^ [Y11: reg] :
( ( c @ Y11 @ Y9 )
=> ( c @ Y11 @ Y10 ) ) )
@ Y8
@ Y7 )
& ( ^ [Y9: reg,Y10: reg] :
( !! @ reg
@ ^ [Y11: reg] :
( ( c @ Y11 @ Y9 )
=> ( c @ Y11 @ Y10 ) ) )
@ Y8
@ Y6 ) ) )
@ Y4
@ Y5 ) )
@ Y3
@ Y1 )
& ( ^ [Y4: reg,Y5: reg] :
( ( c @ Y4 @ Y5 )
& ~ ( ^ [Y6: reg,Y7: reg] :
( ?? @ reg
@ ^ [Y8: reg] :
( ( ^ [Y9: reg,Y10: reg] :
( !! @ reg
@ ^ [Y11: reg] :
( ( c @ Y11 @ Y9 )
=> ( c @ Y11 @ Y10 ) ) )
@ Y8
@ Y7 )
& ( ^ [Y9: reg,Y10: reg] :
( !! @ reg
@ ^ [Y11: reg] :
( ( c @ Y11 @ Y9 )
=> ( c @ Y11 @ Y10 ) ) )
@ Y8
@ Y6 ) ) )
@ Y4
@ Y5 ) )
@ Y3
@ Y2 ) ) )
& ( ^ [Y3: reg,Y4: reg] :
( ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y3
@ Y4 )
& ~ ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y4
@ Y3 ) )
@ Y1
@ Y2 ) )
@ paris
@ france ) ) ) ),
inference(definition_unfolding,[],[f155,f158,f181,f207]) ).
thf(f214,plain,
( ( ^ [Y0: $i > $o] :
( !! @ $i
@ ^ [Y1: $i] : ( Y0 @ Y1 ) )
@ ( ^ [Y0: $i > $i > $o,Y1: $i > $o,Y2: $i] :
( !! @ $i
@ ^ [Y3: $i] :
( ( Y1 @ Y3 )
| ~ ( Y0 @ Y2 @ Y3 ) ) )
@ a
@ ^ [Y0: $i] :
( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( ^ [Y3: reg,Y4: reg] :
( ?? @ reg
@ ^ [Y5: reg] :
( ( ^ [Y6: reg,Y7: reg] :
( !! @ reg
@ ^ [Y8: reg] :
( ( c @ Y8 @ Y6 )
=> ( c @ Y8 @ Y7 ) ) )
@ Y5
@ Y4 )
& ( ^ [Y6: reg,Y7: reg] :
( !! @ reg
@ ^ [Y8: reg] :
( ( c @ Y8 @ Y6 )
=> ( c @ Y8 @ Y7 ) ) )
@ Y5
@ Y3 ) ) )
@ Y2
@ france )
& ( ^ [Y3: reg,Y4: reg] :
( ?? @ reg
@ ^ [Y5: reg] :
( ( ^ [Y6: reg,Y7: reg] :
( !! @ reg
@ ^ [Y8: reg] :
( ( c @ Y8 @ Y6 )
=> ( c @ Y8 @ Y7 ) ) )
@ Y5
@ Y4 )
& ( ^ [Y6: reg,Y7: reg] :
( !! @ reg
@ ^ [Y8: reg] :
( ( c @ Y8 @ Y6 )
=> ( c @ Y8 @ Y7 ) ) )
@ Y5
@ Y3 ) ) )
@ Y2
@ france )
& ~ ( ^ [Y3: reg,Y4: reg] :
( ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y3
@ Y4 )
& ( ^ [Y5: reg,Y6: reg] :
( !! @ reg
@ ^ [Y7: reg] :
( ( c @ Y7 @ Y5 )
=> ( c @ Y7 @ Y6 ) ) )
@ Y4
@ Y3 ) )
@ Y2
@ Y1 ) ) ) ) ) )
!= $true ),
inference(definition_unfolding,[],[f184,f158,f181,f202,f202,f201]) ).
thf(f227,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ?? @ reg
@ ^ [Y2: reg] :
( ?? @ reg
@ ^ [Y3: reg] :
( ( ?? @ reg
@ ^ [Y4: reg] :
( ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ france ) ) )
& ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ Y3 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y4: reg] :
( ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ france ) ) )
& ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ Y3 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) ) ) ) ) )
| ~ ( a @ Y0 @ Y1 ) ) ) )
!= $true ),
inference(beta-eta_normalization,[],[f214]) ).
thf(f228,plain,
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ?? @ reg
@ ^ [Y2: reg] :
( ?? @ reg
@ ^ [Y3: reg] :
( ( ?? @ reg
@ ^ [Y4: reg] :
( ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ france ) ) )
& ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ Y3 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y4: reg] :
( ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ france ) ) )
& ( !! @ reg
@ ^ [Y5: reg] :
( ( c @ Y5 @ Y4 )
=> ( c @ Y5 @ Y3 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y2 )
=> ( c @ Y4 @ Y3 ) ) ) ) ) ) )
| ~ ( a @ Y0 @ Y1 ) ) )
@ sK1 )
= $false ),
inference(sigma_proxy_clausification,[],[f227]) ).
thf(f229,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( ( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y1 )
=> ( c @ Y3 @ Y2 ) ) ) ) ) ) )
| ~ ( a @ sK1 @ Y0 ) ) )
= $false ),
inference(beta-eta_normalization,[],[f228]) ).
thf(f230,plain,
( ( ^ [Y0: $i] :
( ( ?? @ reg
@ ^ [Y1: reg] :
( ?? @ reg
@ ^ [Y2: reg] :
( ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y1 )
=> ( c @ Y3 @ Y2 ) ) ) ) ) ) )
| ~ ( a @ sK1 @ Y0 ) )
@ sK2 )
= $false ),
inference(sigma_proxy_clausification,[],[f229]) ).
thf(f231,plain,
( ( ( ?? @ reg
@ ^ [Y0: reg] :
( ?? @ reg
@ ^ [Y1: reg] :
( ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y0 )
=> ( c @ Y2 @ Y1 ) ) ) ) ) ) )
| ~ ( a @ sK1 @ sK2 ) )
= $false ),
inference(beta-eta_normalization,[],[f230]) ).
thf(f232,plain,
( $false
= ( ~ ( a @ sK1 @ sK2 ) ) ),
inference(or_proxy_clausification,[],[f231]) ).
thf(f233,plain,
( ( ?? @ reg
@ ^ [Y0: reg] :
( ?? @ reg
@ ^ [Y1: reg] :
( ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y0 )
=> ( c @ Y2 @ Y1 ) ) ) ) ) ) )
= $false ),
inference(or_proxy_clausification,[],[f231]) ).
thf(f234,plain,
! [X1: reg] :
( ( ^ [Y0: reg] :
( ?? @ reg
@ ^ [Y1: reg] :
( ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y0 )
=> ( c @ Y2 @ Y1 ) ) ) ) ) )
@ X1 )
= $false ),
inference(pi_proxy_clausification,[],[f233]) ).
thf(f235,plain,
! [X1: reg] :
( ( ?? @ reg
@ ^ [Y0: reg] :
( ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ X1 )
=> ( c @ Y1 @ Y0 ) ) ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f234]) ).
thf(f236,plain,
! [X2: reg,X1: reg] :
( ( ^ [Y0: reg] :
( ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ X1 )
=> ( c @ Y1 @ Y0 ) ) ) ) )
@ X2 )
= $false ),
inference(pi_proxy_clausification,[],[f235]) ).
thf(f237,plain,
! [X2: reg,X1: reg] :
( ( ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) )
& ~ ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X1 )
=> ( c @ Y0 @ X2 ) ) ) ) )
= $false ),
inference(beta-eta_normalization,[],[f236]) ).
thf(f238,plain,
! [X2: reg,X1: reg] :
( ( ( ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) )
& ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) ) )
= $false )
| ( ( ~ ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X1 )
=> ( c @ Y0 @ X2 ) ) ) ) )
= $false ) ),
inference(and_proxy_clausification,[],[f237]) ).
thf(f239,plain,
! [X2: reg,X1: reg] :
( ( ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) )
= $false )
| ( ( ?? @ reg
@ ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) ) )
= $false )
| ( ( ~ ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X1 )
=> ( c @ Y0 @ X2 ) ) ) ) )
= $false ) ),
inference(and_proxy_clausification,[],[f238]) ).
thf(f240,plain,
! [X2: reg,X3: reg,X1: reg] :
( ( ( ~ ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X1 )
=> ( c @ Y0 @ X2 ) ) ) ) )
= $false )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false ) ),
inference(pi_proxy_clausification,[],[f239]) ).
thf(f241,plain,
! [X2: reg,X3: reg,X1: reg] :
( ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false )
| ( ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X1 )
=> ( c @ Y0 @ X2 ) ) ) )
= $true )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false ) ),
inference(not_proxy_clausification,[],[f240]) ).
thf(f243,plain,
! [X2: reg,X3: reg,X1: reg] :
( ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) ) )
= $true )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false ) ),
inference(and_proxy_clausification,[],[f241]) ).
thf(f244,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( $true
= ( ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) )
@ X4 ) )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false ) ),
inference(pi_proxy_clausification,[],[f243]) ).
thf(f245,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( $true
= ( ^ [Y0: reg] :
( ( c @ Y0 @ X2 )
=> ( c @ Y0 @ X1 ) )
@ X4 ) )
| ( ( ^ [Y0: reg] :
( ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ france ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ Y0 )
=> ( c @ Y1 @ X2 ) ) ) )
@ X3 )
= $false ) ),
inference(duplicate_literal_removal,[],[f244]) ).
thf(f246,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( ( c @ X4 @ X2 )
=> ( c @ X4 @ X1 ) )
= $true )
| ( ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ france ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ X2 ) ) ) )
= $false ) ),
inference(beta-eta_normalization,[],[f245]) ).
thf(f247,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ france ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ X2 ) ) ) )
= $false )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f246]) ).
thf(f248,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( $false
= ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ X2 ) ) ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ france ) ) )
= $false )
| ( $true
= ( c @ X4 @ X1 ) ) ),
inference(and_proxy_clausification,[],[f247]) ).
thf(f249,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ X4 @ X2 )
= $false )
| ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ france ) ) )
= $false )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ X2 ) )
@ ( sK3 @ X3 @ X2 ) )
= $false ) ),
inference(sigma_proxy_clausification,[],[f248]) ).
thf(f250,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ X4 @ X2 )
= $false )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ X2 ) )
@ ( sK3 @ X3 @ X2 ) )
= $false )
| ( ( ^ [Y0: reg] :
( ( c @ Y0 @ X3 )
=> ( c @ Y0 @ france ) )
@ ( sK4 @ X3 ) )
= $false ) ),
inference(sigma_proxy_clausification,[],[f249]) ).
thf(f251,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( ( c @ ( sK4 @ X3 ) @ X3 )
=> ( c @ ( sK4 @ X3 ) @ france ) )
= $false )
| ( ( ( c @ ( sK3 @ X3 @ X2 ) @ X3 )
=> ( c @ ( sK3 @ X3 @ X2 ) @ X2 ) )
= $false )
| ( ( c @ X4 @ X2 )
= $false )
| ( $true
= ( c @ X4 @ X1 ) ) ),
inference(beta-eta_normalization,[],[f250]) ).
thf(f252,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ ( sK4 @ X3 ) @ france )
= $false )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( ( c @ ( sK3 @ X3 @ X2 ) @ X3 )
=> ( c @ ( sK3 @ X3 @ X2 ) @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f251]) ).
thf(f253,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ X4 @ X2 )
= $false )
| ( ( ( c @ ( sK3 @ X3 @ X2 ) @ X3 )
=> ( c @ ( sK3 @ X3 @ X2 ) @ X2 ) )
= $false )
| ( ( c @ ( sK4 @ X3 ) @ X3 )
= $true )
| ( $true
= ( c @ X4 @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f251]) ).
thf(f254,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ ( sK4 @ X3 ) @ X3 )
= $true )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( c @ ( sK3 @ X3 @ X2 ) @ X2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f253]) ).
thf(f255,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ ( sK3 @ X3 @ X2 ) @ X3 )
= $true )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( c @ ( sK4 @ X3 ) @ X3 )
= $true ) ),
inference(imp_proxy_clausification,[],[f253]) ).
thf(f256,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ ( sK3 @ X3 @ X2 ) @ X2 )
= $false )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( c @ ( sK4 @ X3 ) @ france )
= $false ) ),
inference(imp_proxy_clausification,[],[f252]) ).
thf(f257,plain,
! [X2: reg,X3: reg,X1: reg,X4: reg] :
( ( ( c @ ( sK3 @ X3 @ X2 ) @ X3 )
= $true )
| ( $true
= ( c @ X4 @ X1 ) )
| ( ( c @ X4 @ X2 )
= $false )
| ( ( c @ ( sK4 @ X3 ) @ france )
= $false ) ),
inference(imp_proxy_clausification,[],[f252]) ).
thf(f272,plain,
( ( a @ sK1 @ sK2 )
= $true ),
inference(not_proxy_clausification,[],[f232]) ).
thf(f273,plain,
( ( !! @ $i
@ ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ paris )
& ~ ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ paris ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ( c @ Y2 @ france )
& ~ ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ paris )
=> ( c @ Y2 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ france )
=> ( c @ Y2 @ paris ) ) ) )
| ~ ( a @ Y0 @ Y1 ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f209]) ).
thf(f274,plain,
! [X1: $i] :
( ( ^ [Y0: $i] :
( !! @ $i
@ ^ [Y1: $i] :
( ( ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ paris )
& ~ ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ paris ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) )
& ( c @ Y2 @ france )
& ~ ( ?? @ reg
@ ^ [Y3: reg] :
( ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ france ) ) )
& ( !! @ reg
@ ^ [Y4: reg] :
( ( c @ Y4 @ Y3 )
=> ( c @ Y4 @ Y2 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ paris )
=> ( c @ Y2 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ france )
=> ( c @ Y2 @ paris ) ) ) )
| ~ ( a @ Y0 @ Y1 ) ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f273]) ).
thf(f275,plain,
! [X1: $i] :
( $true
= ( !! @ $i
@ ^ [Y0: $i] :
( ( ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ paris )
& ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ paris ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ( c @ Y1 @ france )
& ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ paris )
=> ( c @ Y1 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ france )
=> ( c @ Y1 @ paris ) ) ) )
| ~ ( a @ X1 @ Y0 ) ) ) ),
inference(beta-eta_normalization,[],[f274]) ).
thf(f276,plain,
! [X2: $i,X1: $i] :
( $true
= ( ^ [Y0: $i] :
( ( ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ paris )
& ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ paris ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) )
& ( c @ Y1 @ france )
& ~ ( ?? @ reg
@ ^ [Y2: reg] :
( ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ france ) ) )
& ( !! @ reg
@ ^ [Y3: reg] :
( ( c @ Y3 @ Y2 )
=> ( c @ Y3 @ Y1 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ paris )
=> ( c @ Y1 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y1: reg] :
( ( c @ Y1 @ france )
=> ( c @ Y1 @ paris ) ) ) )
| ~ ( a @ X1 @ Y0 ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f275]) ).
thf(f277,plain,
! [X2: $i,X1: $i] :
( ( ( ~ ( ?? @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ paris ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ( c @ Y0 @ france )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
=> ( c @ Y0 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) ) )
| ~ ( a @ X1 @ X2 ) )
= $true ),
inference(beta-eta_normalization,[],[f276]) ).
thf(f278,plain,
! [X2: $i,X1: $i] :
( ( $true
= ( ~ ( a @ X1 @ X2 ) ) )
| ( ( ~ ( ?? @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ paris ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ( c @ Y0 @ france )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
=> ( c @ Y0 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) ) )
= $true ) ),
inference(or_proxy_clausification,[],[f277]) ).
thf(f279,plain,
! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( ( ~ ( ?? @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ paris ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) )
& ( c @ Y0 @ france )
& ~ ( ?? @ reg
@ ^ [Y1: reg] :
( ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ france ) ) )
& ( !! @ reg
@ ^ [Y2: reg] :
( ( c @ Y2 @ Y1 )
=> ( c @ Y2 @ Y0 ) ) ) ) ) ) )
& ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
=> ( c @ Y0 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) ) )
= $true ) ),
inference(not_proxy_clausification,[],[f278]) ).
thf(f280,plain,
! [X2: $i,X1: $i] :
( ( ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ paris )
=> ( c @ Y0 @ france ) ) )
& ~ ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) ) )
= $true )
| ( ( a @ X1 @ X2 )
= $false ) ),
inference(and_proxy_clausification,[],[f279]) ).
thf(f319,plain,
! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( ( ~ ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) ) )
= $true ) ),
inference(and_proxy_clausification,[],[f280]) ).
thf(f324,plain,
! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( ( !! @ reg
@ ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) ) )
= $false ) ),
inference(not_proxy_clausification,[],[f319]) ).
thf(f325,plain,
! [X2: $i,X1: $i] :
( ( ( ^ [Y0: reg] :
( ( c @ Y0 @ france )
=> ( c @ Y0 @ paris ) )
@ sK9 )
= $false )
| ( ( a @ X1 @ X2 )
= $false ) ),
inference(sigma_proxy_clausification,[],[f324]) ).
thf(f326,plain,
! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( ( ( c @ sK9 @ france )
=> ( c @ sK9 @ paris ) )
= $false ) ),
inference(beta-eta_normalization,[],[f325]) ).
thf(f327,plain,
! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( ( c @ sK9 @ paris )
= $false ) ),
inference(imp_proxy_clausification,[],[f326]) ).
thf(f488,definition,
( spl20_4
<=> ! [X4: reg,X1: reg] :
( $true
= ( c @ X4 @ X1 ) ) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
thf(f489,plain,
( ! [X1: reg,X4: reg] :
( $true
= ( c @ X4 @ X1 ) )
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f488]) ).
thf(f543,plain,
( ! [X2: $i,X1: $i] :
( ( ( a @ X1 @ X2 )
= $false )
| ( $true = $false ) )
| ~ spl20_4 ),
inference(forward_demodulation,[],[f327,f489]) ).
thf(f544,plain,
( ! [X2: $i,X1: $i] :
( ( a @ X1 @ X2 )
= $false )
| ~ spl20_4 ),
inference(trivial_inequality_removal,[],[f543]) ).
thf(f547,plain,
( ( $true = $false )
| ~ spl20_4 ),
inference(constrained_superposition,[],[f272,f544]) ).
thf(f551,plain,
( $false
| ~ spl20_4 ),
inference(trivial_inequality_removal,[],[f547]) ).
thf(f552,plain,
~ spl20_4,
inference(avatar_contradiction_clause,[],[f551]) ).
thf(f1147,plain,
! [X2: reg,X0: reg,X1: reg] :
( ( ( c @ ( sK3 @ X1 @ X0 ) @ X1 )
= $true )
| ( ( c @ ( sK4 @ X1 ) @ X1 )
= $true )
| ( $true
= ( c @ X0 @ X2 ) )
| ( $true = $false ) ),
inference(constrained_superposition,[],[f255,f175]) ).
thf(f1150,plain,
! [X2: reg,X0: reg,X1: reg] :
( ( ( c @ ( sK3 @ X1 @ X0 ) @ X1 )
= $true )
| ( $true
= ( c @ X0 @ X2 ) )
| ( ( c @ ( sK4 @ X1 ) @ X1 )
= $true ) ),
inference(trivial_inequality_removal,[],[f1147]) ).
thf(f1189,plain,
! [X2: reg,X0: reg,X1: reg] :
( ( $true
= ( c @ X0 @ X2 ) )
| ( $true = $false )
| ( ( c @ ( sK4 @ X1 ) @ france )
= $false )
| ( ( c @ ( sK3 @ X1 @ X0 ) @ X1 )
= $true ) ),
inference(constrained_superposition,[],[f257,f175]) ).
thf(f1252,plain,
! [X2: reg,X0: reg,X1: reg] :
( ( ( c @ ( sK3 @ X1 @ X0 ) @ X1 )
= $true )
| ( $true
= ( c @ X0 @ X2 ) )
| ( ( c @ ( sK4 @ X1 ) @ france )
= $false ) ),
inference(trivial_inequality_removal,[],[f1189]) ).
thf(f1873,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( ( c @ X1 @ X0 )
= $false )
| ( $true = $false )
| ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( ( c @ X1 @ X2 )
= $true )
| ( ( c @ X0 @ X3 )
= $true ) ),
inference(constrained_superposition,[],[f254,f1150]) ).
thf(f1889,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( ( c @ X1 @ X0 )
= $false )
| ( ( c @ X0 @ X3 )
= $true )
| ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( $true = $false )
| ( ( c @ X1 @ X2 )
= $true ) ),
inference(duplicate_literal_removal,[],[f1873]) ).
thf(f1890,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( ( c @ X1 @ X2 )
= $true )
| ( ( c @ X1 @ X0 )
= $false )
| ( ( c @ X0 @ X3 )
= $true ) ),
inference(trivial_inequality_removal,[],[f1889]) ).
thf(f1959,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( $true != $true )
| ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( ( c @ X0 @ X0 )
= $false ) ),
inference(equality_factoring,[],[f1890]) ).
thf(f2003,plain,
! [X0: reg,X1: reg] :
( ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true )
| ( ( c @ X0 @ X0 )
= $false )
| ( ( c @ X0 @ X1 )
= $true ) ),
inference(trivial_inequality_removal,[],[f1959]) ).
thf(f2018,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( $true = $false )
| ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true ) ),
inference(forward_demodulation,[],[f2003,f175]) ).
thf(f2019,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( ( c @ ( sK4 @ X0 ) @ X0 )
= $true ) ),
inference(trivial_inequality_removal,[],[f2018]) ).
thf(f2598,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( ( c @ X1 @ X0 )
= $false )
| ( ( c @ X1 @ X2 )
= $true )
| ( $true = $false )
| ( ( c @ X0 @ X3 )
= $true )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) ) ),
inference(constrained_superposition,[],[f256,f1252]) ).
thf(f2616,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( ( c @ X1 @ X0 )
= $false )
| ( ( c @ X1 @ X2 )
= $true )
| ( $true = $false )
| ( ( c @ X0 @ X3 )
= $true )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) ) ),
inference(duplicate_literal_removal,[],[f2598]) ).
thf(f2617,plain,
! [X2: reg,X3: reg,X0: reg,X1: reg] :
( ( $false
= ( c @ ( sK4 @ X0 ) @ france ) )
| ( ( c @ X1 @ X2 )
= $true )
| ( ( c @ X1 @ X0 )
= $false )
| ( ( c @ X0 @ X3 )
= $true ) ),
inference(trivial_inequality_removal,[],[f2616]) ).
thf(f2741,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X0 )
= $false )
| ( $true != $true )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) )
| ( ( c @ X0 @ X1 )
= $true ) ),
inference(equality_factoring,[],[f2617]) ).
thf(f2772,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X0 )
= $false )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) )
| ( ( c @ X0 @ X1 )
= $true ) ),
inference(trivial_inequality_removal,[],[f2741]) ).
thf(f2847,plain,
! [X0: reg,X1: reg] :
( ( $true = $false )
| ( ( c @ X0 @ X1 )
= $true )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) ) ),
inference(forward_demodulation,[],[f2772,f175]) ).
thf(f2848,plain,
! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( $false
= ( c @ ( sK4 @ X0 ) @ france ) ) ),
inference(trivial_inequality_removal,[],[f2847]) ).
thf(f2856,definition,
( spl20_13
<=> ! [X1: reg] :
( ( c @ france @ X1 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
thf(f2857,plain,
( ! [X1: reg] :
( ( c @ france @ X1 )
= $true )
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f2856]) ).
thf(f2911,plain,
! [X0: reg,X1: reg] :
( ( $true = $false )
| ( ( c @ france @ X0 )
= $true )
| ( ( c @ france @ X1 )
= $true ) ),
inference(constrained_superposition,[],[f2848,f2019]) ).
thf(f2944,plain,
! [X0: reg,X1: reg] :
( ( ( c @ france @ X1 )
= $true )
| ( ( c @ france @ X0 )
= $true ) ),
inference(trivial_inequality_removal,[],[f2911]) ).
thf(f15633,definition,
( spl20_43
<=> ! [X0: reg] :
( ( c @ X0 @ france )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl20_43])],[avatar_definition]) ).
thf(f15634,plain,
( ! [X0: reg] :
( ( c @ X0 @ france )
= $true )
| ~ spl20_43 ),
inference(avatar_component_clause,[],[f15633]) ).
thf(f17448,plain,
( ! [X0: reg] :
( ( ( c @ X0 @ france )
= $true )
| ( $true != $true ) )
| ~ spl20_13 ),
inference(constrained_superposition,[],[f164,f2857]) ).
thf(f17474,plain,
( ! [X0: reg] :
( ( c @ X0 @ france )
= $true )
| ~ spl20_13 ),
inference(trivial_inequality_removal,[],[f17448]) ).
thf(f17663,plain,
( spl20_43
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f17474,f2856,f15633]) ).
thf(f17683,plain,
( ! [X0: reg,X1: reg] :
( ( ( c @ X0 @ X1 )
= $true )
| ( $true = $false ) )
| ~ spl20_43 ),
inference(constrained_superposition,[],[f15634,f2848]) ).
thf(f17724,plain,
( ! [X0: reg,X1: reg] :
( ( c @ X0 @ X1 )
= $true )
| ~ spl20_43 ),
inference(trivial_inequality_removal,[],[f17683]) ).
thf(f17787,plain,
( spl20_4
| ~ spl20_43 ),
inference(avatar_split_clause,[],[f17724,f15633,f488]) ).
thf(f17933,plain,
( spl20_13
| spl20_13 ),
inference(avatar_split_clause,[],[f2944,f2856,f2856]) ).
cnf(s76,plain,
~ spl20_4,
inference(sat_conversion,[],[f552]) ).
cnf(s2724,plain,
( ~ spl20_13
| spl20_43 ),
inference(sat_conversion,[],[f17663]) ).
cnf(s2773,plain,
( spl20_4
| ~ spl20_43 ),
inference(sat_conversion,[],[f17787]) ).
cnf(s2887,plain,
( spl20_13
| spl20_13 ),
inference(sat_conversion,[],[f17933]) ).
cnf(s2888,plain,
spl20_13,
inference(rat,[],[s2887]) ).
cnf(s2889,plain,
spl20_43,
inference(rat,[],[s2724,s2888]) ).
cnf(s2890,plain,
spl20_4,
inference(rat,[],[s2773,s2889]) ).
cnf(s2901,plain,
$false,
inference(rat,[],[s76,s2890]) ).
thf(f17934,plain,
$false,
inference(avatar_sat_refutation,[],[s2901]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEG014^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n016.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 18:39:20 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.18/0.97 % (741824)Will run a generic schedule for satisfiability detection.
% 4.18/0.97 % (741830)% WARNING: option uhcvi not known.
% 4.18/0.97 % (741830)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1934747415:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.18/0.97 % (741830)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.18/0.97 % (741830)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.18/0.97 % (741829)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1897976888_2999 on theBenchmark for (2999ds/0Mi)
% 4.18/0.97 % (741831)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4259520574:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.18/0.97 % (741832)dis+10_1_sil=32000:sp=arity:random_seed=2547312589:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.18/0.97 % (741834)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=911726297:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.18/0.97 % (741833)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=225039279:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.18/0.97 % (741835)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3165130268:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.18/0.97 % (741833)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.18/0.97 % Exception at run slice level
% 4.18/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.18/0.97 % (741843)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3143305374:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.18/0.97 % Exception at run slice level
% 4.18/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.18/0.97 % (741832)Instruction limit reached!
% 4.18/0.97 % (741832)------------------------------
% 4.18/0.97 % (741832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.97 % (741832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.97 % (741832)CaDiCaL version: 2.1.3
% 4.18/0.97 % (741832)Termination reason: Instruction limit
% 4.18/0.97 % (741832)Termination phase: Saturation
% 4.18/0.97 % (741832)Time elapsed: 0.049 s
% 4.18/0.97 % (741832)Peak memory usage: 12 MB
% 4.18/0.97 % (741832)Instructions burned: 103 (million)
% 4.18/0.97 % (741833)Instruction limit reached!
% 4.18/0.97 % (741833)------------------------------
% 4.18/0.97 % (741833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.97 % (741833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.97 % (741833)CaDiCaL version: 2.1.3
% 4.18/0.97 % (741833)Termination reason: Instruction limit
% 4.18/0.97 % (741833)Termination phase: Saturation
% 4.18/0.97 % (741833)Time elapsed: 0.056 s
% 4.18/0.97 % (741833)Peak memory usage: 13 MB
% 4.18/0.97 % (741833)Instructions burned: 118 (million)
% 4.18/0.97 % (741845)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1181606494:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.18/0.97 % (741834)Instruction limit reached!
% 4.18/0.97 % (741834)------------------------------
% 4.18/0.97 % (741834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.18/0.97 % (741834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/0.97 % (741834)CaDiCaL version: 2.1.3
% 4.18/0.97 % (741834)Termination reason: Instruction limit
% 4.18/0.97 % (741834)Termination phase: Saturation
% 4.18/0.97 % (741834)Time elapsed: 0.062 s
% 4.18/0.97 % (741834)Peak memory usage: 13 MB
% 4.18/0.97 % (741834)Instructions burned: 132 (million)
% 4.18/0.97 % (741846)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=1134229624:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.18/0.97 % (741846)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.18/0.97 % (741846)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.18/0.97 % (741848)ott-21_1_sil=16000:fs=off:random_seed=1778322090:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.18/0.97 % (741835)Instruction limit reached!
% 4.18/0.97 % (741835)------------------------------
% 17.67/2.86 % (741835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.67/2.86 % (741835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/2.86 % (741835)CaDiCaL version: 2.1.3
% 17.67/2.86 % (741835)Termination reason: Instruction limit
% 17.67/2.86 % (741835)Termination phase: Saturation
% 17.67/2.86 % (741835)Time elapsed: 0.079 s
% 17.67/2.86 % (741835)Peak memory usage: 12 MB
% 17.67/2.86 % (741835)Instructions burned: 159 (million)
% 17.67/2.86 % (741849)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2789654352:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 17.67/2.86 % (741852)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2927993643:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.67/2.86 % Exception at run slice level
% 17.67/2.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.67/2.86 % (741845)Instruction limit reached!
% 17.67/2.86 % (741845)------------------------------
% 17.67/2.86 % (741845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.67/2.86 % (741845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/2.86 % (741845)CaDiCaL version: 2.1.3
% 17.67/2.86 % (741845)Termination reason: Instruction limit
% 17.67/2.86 % (741845)Termination phase: Saturation
% 17.67/2.86 % (741845)Time elapsed: 0.060 s
% 17.67/2.86 % (741845)Peak memory usage: 12 MB
% 17.67/2.86 % (741845)Instructions burned: 131 (million)
% 17.67/2.86 % (741864)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3098505742:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 17.67/2.86 % (741871)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3993429011:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 17.67/2.86 % Exception at run slice level
% 17.67/2.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.67/2.86 % (741883)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=2848118298: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)
% 17.67/2.86 % (741848)Instruction limit reached!
% 17.67/2.86 % (741848)------------------------------
% 17.67/2.86 % (741848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.67/2.86 % (741848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/2.86 % (741848)CaDiCaL version: 2.1.3
% 17.67/2.86 % (741848)Termination reason: Instruction limit
% 17.67/2.86 % (741848)Termination phase: Saturation
% 17.67/2.86 % (741848)Time elapsed: 0.085 s
% 17.67/2.86 % (741848)Peak memory usage: 12 MB
% 17.67/2.86 % (741848)Instructions burned: 181 (million)
% 17.67/2.86 % (741883)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.67/2.86 % (741896)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3409056103:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 17.67/2.86 % (741896)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.67/2.86 % (741849)Instruction limit reached!
% 17.67/2.86 % (741849)------------------------------
% 17.67/2.86 % (741849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.67/2.86 % (741849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.67/2.86 % (741849)CaDiCaL version: 2.1.3
% 17.67/2.86 % (741849)Termination reason: Instruction limit
% 17.67/2.86 % (741849)Termination phase: Saturation
% 17.67/2.86 % (741849)Time elapsed: 0.233 s
% 17.67/2.86 % (741849)Peak memory usage: 14 MB
% 17.67/2.86 % (741849)Instructions burned: 478 (million)
% 17.67/2.86 % (741954)fmb+10_1_sil=64000:random_seed=1430968944:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 17.67/2.86 % (741954)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.67/2.86 % Exception at run slice level
% 17.67/2.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.67/2.86 % (741961)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3790594893:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 17.67/2.86 % Exception at run slice level
% 17.67/2.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.67/2.86 % (741846)Instruction limit reached!
% 17.67/2.86 % (741846)------------------------------
% 46.63/6.88 % (741846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.63/6.88 % (741846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.63/6.88 % (741846)CaDiCaL version: 2.1.3
% 46.63/6.88 % (741846)Termination reason: Instruction limit
% 46.63/6.88 % (741846)Termination phase: Saturation
% 46.63/6.88 % (741846)Time elapsed: 0.312 s
% 46.63/6.88 % (741846)Peak memory usage: 14 MB
% 46.63/6.88 % (741846)Instructions burned: 686 (million)
% 46.63/6.88 % (741972)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=671395323:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 46.63/6.88 % Exception at run slice level
% 46.63/6.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.63/6.88 % (741978)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1462473043:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 46.63/6.88 % (741978)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.63/6.88 % (741982)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=477542213:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 46.63/6.88 % (741982)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.63/6.88 % (741982)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 46.63/6.88 % (741883)Instruction limit reached!
% 46.63/6.88 % (741883)------------------------------
% 46.63/6.88 % (741883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.63/6.88 % (741883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.63/6.88 % (741883)CaDiCaL version: 2.1.3
% 46.63/6.88 % (741883)Termination reason: Instruction limit
% 46.63/6.88 % (741883)Termination phase: Saturation
% 46.63/6.88 % (741883)Time elapsed: 0.354 s
% 46.63/6.88 % (741883)Peak memory usage: 18 MB
% 46.63/6.88 % (741883)Instructions burned: 693 (million)
% 46.63/6.88 % (742025)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3557695451:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 46.63/6.88 % Exception at run slice level
% 46.63/6.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.63/6.88 % (742027)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=103405735:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 46.63/6.88 % Exception at run slice level
% 46.63/6.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.63/6.88 % (742029)ott-2_1_sil=16000:newcnf=on:random_seed=222093962:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 46.63/6.88 % (742029)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.63/6.88 % (741896)Instruction limit reached!
% 46.63/6.88 % (741896)------------------------------
% 46.63/6.88 % (741896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.63/6.88 % (741896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.63/6.88 % (741896)CaDiCaL version: 2.1.3
% 46.63/6.88 % (741896)Termination reason: Instruction limit
% 46.63/6.88 % (741896)Termination phase: Saturation
% 46.63/6.88 % (741896)Time elapsed: 0.427 s
% 46.63/6.89 % (741896)Peak memory usage: 16 MB
% 46.63/6.89 % (741896)Instructions burned: 880 (million)
% 46.63/6.89 % (742031)ott+10_1_sil=32000:tgt=ground:random_seed=2074924112:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 46.63/6.89 % (741864)Instruction limit reached!
% 46.63/6.89 % (741864)------------------------------
% 46.63/6.89 % (741864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.63/6.89 % (741864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.63/6.89 % (741864)CaDiCaL version: 2.1.3
% 46.63/6.89 % (741864)Termination reason: Instruction limit
% 46.63/6.89 % (741864)Termination phase: Saturation
% 46.63/6.89 % (741864)Time elapsed: 0.551 s
% 46.63/6.89 % (741864)Peak memory usage: 16 MB
% 46.63/6.89 % (741864)Instructions burned: 1179 (million)
% 46.63/6.89 % (742033)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=193420388:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 46.63/6.89 % Exception at run slice level
% 46.63/6.89 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.63/6.89 % (742035)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=723883615:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 102.20/14.75 % (742035)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 102.20/14.75 % (742029)Instruction limit reached!
% 102.20/14.75 % (742029)------------------------------
% 102.20/14.75 % (742029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (742029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (742029)CaDiCaL version: 2.1.3
% 102.20/14.75 % (742029)Termination reason: Instruction limit
% 102.20/14.75 % (742029)Termination phase: Saturation
% 102.20/14.75 % (742029)Time elapsed: 0.356 s
% 102.20/14.75 % (742029)Peak memory usage: 14 MB
% 102.20/14.75 % (742029)Instructions burned: 871 (million)
% 102.20/14.75 % (742037)dis+21_1_sil=32000:sas=cadical:random_seed=1228302227:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 102.20/14.75 % (741982)Instruction limit reached!
% 102.20/14.75 % (741982)------------------------------
% 102.20/14.75 % (741982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (741982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (741982)CaDiCaL version: 2.1.3
% 102.20/14.75 % (741982)Termination reason: Instruction limit
% 102.20/14.75 % (741982)Termination phase: Saturation
% 102.20/14.75 % (741982)Time elapsed: 0.746 s
% 102.20/14.75 % (741982)Peak memory usage: 20 MB
% 102.20/14.75 % (741982)Instructions burned: 1474 (million)
% 102.20/14.75 % (742039)ott+11_1_sil=16000:gs=on:random_seed=1081507397:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 102.20/14.75 % (742039)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 102.20/14.75 % (742039)Instruction limit reached!
% 102.20/14.75 % (742039)------------------------------
% 102.20/14.75 % (742039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (742039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (742039)CaDiCaL version: 2.1.3
% 102.20/14.75 % (742039)Termination reason: Instruction limit
% 102.20/14.75 % (742039)Termination phase: Saturation
% 102.20/14.75 % (742039)Time elapsed: 1.024 s
% 102.20/14.75 % (742039)Peak memory usage: 19 MB
% 102.20/14.75 % (742039)Instructions burned: 2253 (million)
% 102.20/14.75 % (742041)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3502985143:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi)
% 102.20/14.75 % Exception at run slice level
% 102.20/14.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 102.20/14.75 % (742043)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3423047110:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi)
% 102.20/14.75 % (742035)Instruction limit reached!
% 102.20/14.75 % (742035)------------------------------
% 102.20/14.75 % (742035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (742035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (742035)CaDiCaL version: 2.1.3
% 102.20/14.75 % (742035)Termination reason: Instruction limit
% 102.20/14.75 % (742035)Termination phase: Saturation
% 102.20/14.75 % (742035)Time elapsed: 1.532 s
% 102.20/14.75 % (742035)Peak memory usage: 19 MB
% 102.20/14.75 % (742035)Instructions burned: 3513 (million)
% 102.20/14.75 % (742045)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1191583936:i=29340_2977 on theBenchmark for (2977ds/29340Mi)
% 102.20/14.75 % (742037)Instruction limit reached!
% 102.20/14.75 % (742037)------------------------------
% 102.20/14.75 % (742037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (742037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (742037)CaDiCaL version: 2.1.3
% 102.20/14.75 % (742037)Termination reason: Instruction limit
% 102.20/14.75 % (742037)Termination phase: Saturation
% 102.20/14.75 % (742037)Time elapsed: 1.635 s
% 102.20/14.75 % (742037)Peak memory usage: 20 MB
% 102.20/14.75 % (742037)Instructions burned: 3774 (million)
% 102.20/14.75 % (741978)Instruction limit reached!
% 102.20/14.75 % (741978)------------------------------
% 102.20/14.75 % (741978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.20/14.75 % (741978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.20/14.75 % (741978)CaDiCaL version: 2.1.3
% 153.79/21.97 % (741978)Termination reason: Instruction limit
% 153.79/21.97 % (741978)Termination phase: Saturation
% 153.79/21.97 % (741978)Time elapsed: 2.208 s
% 153.79/21.97 % (741978)Peak memory usage: 21 MB
% 153.79/21.97 % (741978)Instructions burned: 5132 (million)
% 153.79/21.97 % (742047)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2559350064:i=5211_2973 on theBenchmark for (2973ds/5211Mi)
% 153.79/21.97 % (742048)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2498785295:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi)
% 153.79/21.97 % Exception at run slice level
% 153.79/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 153.79/21.97 % (742051)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1641382353:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 153.79/21.97 % Exception at run slice level
% 153.79/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 153.79/21.97 % (742053)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=929481164:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 153.79/21.97 % Exception at run slice level
% 153.79/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 153.79/21.97 % (742055)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3542826820:i=22565:add=on:rawr=on_2972 on theBenchmark for (2972ds/22565Mi)
% 153.79/21.97 % (742031)Instruction limit reached!
% 153.79/21.97 % (742031)------------------------------
% 153.79/21.97 % (742031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 153.79/21.97 % (742031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.79/21.97 % (742031)CaDiCaL version: 2.1.3
% 153.79/21.97 % (742031)Termination reason: Instruction limit
% 153.79/21.97 % (742031)Termination phase: Saturation
% 153.79/21.97 % (742031)Time elapsed: 2.275 s
% 153.79/21.97 % (742031)Peak memory usage: 22 MB
% 153.79/21.97 % (742031)Instructions burned: 5115 (million)
% 153.79/21.97 % (742057)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3623770646:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi)
% 153.79/21.97 % (742043)Instruction limit reached!
% 153.79/21.97 % (742043)------------------------------
% 153.79/21.97 % (742043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 153.79/21.97 % (742043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.79/21.97 % (742043)CaDiCaL version: 2.1.3
% 153.79/21.97 % (742043)Termination reason: Instruction limit
% 153.79/21.97 % (742043)Termination phase: Saturation
% 153.79/21.97 % (742043)Time elapsed: 1.954 s
% 153.79/21.97 % (742043)Peak memory usage: 20 MB
% 153.79/21.97 % (742043)Instructions burned: 4592 (million)
% 153.79/21.97 % (742059)dis+10_16:1_sil=16000:random_seed=4102912860:i=9155:fsr=off_2957 on theBenchmark for (2957ds/9155Mi)
% 153.79/21.97 % (742047)Instruction limit reached!
% 153.79/21.97 % (742047)------------------------------
% 153.79/21.97 % (742047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 153.79/21.97 % (742047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.79/21.97 % (742047)CaDiCaL version: 2.1.3
% 153.79/21.97 % (742047)Termination reason: Instruction limit
% 153.79/21.97 % (742047)Termination phase: Saturation
% 153.79/21.97 % (742047)Time elapsed: 2.330 s
% 153.79/21.97 % (742047)Peak memory usage: 26 MB
% 153.79/21.97 % (742047)Instructions burned: 5213 (million)
% 153.79/21.97 % (742061)ott-3_8_sil=64000:random_seed=3903913044:i=20139:bs=on_2950 on theBenchmark for (2950ds/20139Mi)
% 153.79/21.97 % (742057)Instruction limit reached!
% 153.79/21.97 % (742057)------------------------------
% 153.79/21.97 % (742057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 153.79/21.97 % (742057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.79/21.97 % (742057)CaDiCaL version: 2.1.3
% 153.79/21.97 % (742057)Termination reason: Instruction limit
% 153.79/21.97 % (742057)Termination phase: Saturation
% 153.79/21.97 % (742057)Time elapsed: 3.659 s
% 153.79/21.97 % (742057)Peak memory usage: 34 MB
% 153.79/21.97 % (742057)Instructions burned: 8174 (million)
% 153.79/21.97 % (742063)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1143025286:fmbsr=2:i=32576_2933 on theBenchmark for (2933ds/32576Mi)
% 153.79/21.97 % Exception at run slice level
% 153.79/21.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 153.79/21.97 % (742065)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4055582317:i=11404_2933 on theBenchmark for (2933ds/11404Mi)
% 163.06/23.27 % (742059)Instruction limit reached!
% 163.06/23.27 % (742059)------------------------------
% 163.06/23.27 % (742059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742059)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742059)Termination reason: Instruction limit
% 163.06/23.27 % (742059)Termination phase: Saturation
% 163.06/23.27 % (742059)Time elapsed: 3.880 s
% 163.06/23.27 % (742059)Peak memory usage: 25 MB
% 163.06/23.27 % (742059)Instructions burned: 9157 (million)
% 163.06/23.27 % (742067)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=970104545:i=14134_2918 on theBenchmark for (2918ds/14134Mi)
% 163.06/23.27 % (742067)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 163.06/23.27 % (742065)Instruction limit reached!
% 163.06/23.27 % (742065)------------------------------
% 163.06/23.27 % (742065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742065)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742065)Termination reason: Instruction limit
% 163.06/23.27 % (742065)Termination phase: Saturation
% 163.06/23.27 % (742065)Time elapsed: 5.200 s
% 163.06/23.27 % (742065)Peak memory usage: 40 MB
% 163.06/23.27 % (742065)Instructions burned: 11406 (million)
% 163.06/23.27 % (742069)dis+33_16_sil=32000:sac=on:random_seed=2039799103:i=15851:nm=0_2881 on theBenchmark for (2881ds/15851Mi)
% 163.06/23.27 % (742055)Instruction limit reached!
% 163.06/23.27 % (742055)------------------------------
% 163.06/23.27 % (742055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742055)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742055)Termination reason: Instruction limit
% 163.06/23.27 % (742055)Termination phase: Saturation
% 163.06/23.27 % (742055)Time elapsed: 10.929 s
% 163.06/23.27 % (742055)Peak memory usage: 48 MB
% 163.06/23.27 % (742055)Instructions burned: 22566 (million)
% 163.06/23.27 % (742061)Instruction limit reached!
% 163.06/23.27 % (742061)------------------------------
% 163.06/23.27 % (742061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742061)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742061)Termination reason: Instruction limit
% 163.06/23.27 % (742061)Termination phase: Saturation
% 163.06/23.27 % (742061)Time elapsed: 8.688 s
% 163.06/23.27 % (742061)Peak memory usage: 39 MB
% 163.06/23.27 % (742061)Instructions burned: 20141 (million)
% 163.06/23.27 % (742071)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1893623542:avsq=on:i=17627:add=on:amm=off_2863 on theBenchmark for (2863ds/17627Mi)
% 163.06/23.27 % (742073)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=856568253:s2a=on:i=53295_2863 on theBenchmark for (2863ds/53295Mi)
% 163.06/23.27 % (742045)Instruction limit reached!
% 163.06/23.27 % (742045)------------------------------
% 163.06/23.27 % (742045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742045)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742045)Termination reason: Instruction limit
% 163.06/23.27 % (742045)Termination phase: Saturation
% 163.06/23.27 % (742045)Time elapsed: 11.631 s
% 163.06/23.27 % (742045)Peak memory usage: 29 MB
% 163.06/23.27 % (742045)Instructions burned: 29342 (million)
% 163.06/23.27 % (742119)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=877419157:i=26857:ins=20_2860 on theBenchmark for (2860ds/26857Mi)
% 163.06/23.27 % Exception at run slice level
% 163.06/23.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 163.06/23.27 % (742126)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=368161979:i=28120:bs=on:fsr=off_2860 on theBenchmark for (2860ds/28120Mi)
% 163.06/23.27 % (742067)Instruction limit reached!
% 163.06/23.27 % (742067)------------------------------
% 163.06/23.27 % (742067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 163.06/23.27 % (742067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.06/23.27 % (742067)CaDiCaL version: 2.1.3
% 163.06/23.27 % (742067)Termination reason: Instruction limit
% 163.06/23.27 % (742067)Termination phase: Saturation
% 163.06/23.27 % (742067)Time elapsed: 6.368 s
% 185.03/26.32 % (742067)Peak memory usage: 45 MB
% 185.03/26.32 % (742067)Instructions burned: 14136 (million)
% 185.03/26.32 % (742311)fmb+10_1_sil=256000:fmbss=7:random_seed=1364919822:fmbsr=1.6:i=182295_2854 on theBenchmark for (2854ds/182295Mi)
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742325)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2560625058:i=44625:gsp=on_2854 on theBenchmark for (2854ds/44625Mi)
% 185.03/26.32 % (742325)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 185.03/26.32 % (742325)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742337)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2488341998:i=160505_2854 on theBenchmark for (2854ds/160505Mi)
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742350)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=3747936564:fmbsr=1.3:i=225729_2853 on theBenchmark for (2853ds/225729Mi)
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742363)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1535392480:fmbsr=2:i=185024:ins=7_2853 on theBenchmark for (2853ds/185024Mi)
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742378)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2565992842:rtra=on_2853 on theBenchmark for (2853ds/0Mi)
% 185.03/26.32 % Exception at run slice level
% 185.03/26.32 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 185.03/26.32 % (742389)% WARNING: option uhcvi not known.
% 185.03/26.32 % (742389)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2207848674:i=271062:add=off:rtra=on:rawr=on_2853 on theBenchmark for (2853ds/271062Mi)
% 185.03/26.32 % (742389)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 185.03/26.32 % (742389)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 185.03/26.32 % (742069)Instruction limit reached!
% 185.03/26.32 % (742069)------------------------------
% 185.03/26.32 % (742069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 185.03/26.32 % (742069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 185.03/26.32 % (742069)CaDiCaL version: 2.1.3
% 185.03/26.32 % (742069)Termination reason: Instruction limit
% 185.03/26.32 % (742069)Termination phase: Saturation
% 185.03/26.32 % (742069)Time elapsed: 6.564 s
% 185.03/26.32 % (742069)Peak memory usage: 32 MB
% 185.03/26.32 % (742069)Instructions burned: 15852 (million)
% 185.03/26.32 % (742471)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2154153563:i=176048:add=on:rtra=on:rawr=on_2815 on theBenchmark for (2815ds/176048Mi)
% 185.03/26.32 % (742071)Instruction limit reached!
% 185.03/26.32 % (742071)------------------------------
% 185.03/26.32 % (742071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 185.03/26.32 % (742071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 185.03/26.32 % (742071)CaDiCaL version: 2.1.3
% 185.03/26.32 % (742071)Termination reason: Instruction limit
% 185.03/26.32 % (742071)Termination phase: Saturation
% 185.03/26.32 % (742071)Time elapsed: 7.928 s
% 185.03/26.32 % (742071)Peak memory usage: 69 MB
% 185.03/26.32 % (742071)Instructions burned: 17630 (million)
% 185.03/26.32 % (742473)dis+10_1_sil=32000:si=on:sp=arity:random_seed=915128483:i=206:fgj=on:rtra=on_2783 on theBenchmark for (2783ds/206Mi)
% 185.03/26.32 % (742473)Instruction limit reached!
% 185.03/26.32 % (742473)------------------------------
% 185.03/26.32 % (742473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 185.03/26.32 % (742473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 185.03/26.32 % (742473)CaDiCaL version: 2.1.3
% 185.03/26.32 % (742473)Termination reason: Instruction limit
% 185.03/26.32 % (742473)Termination phase: Saturation
% 185.03/26.32 % (742473)Time elapsed: 0.099 s
% 204.41/29.08 % (742473)Peak memory usage: 13 MB
% 204.41/29.08 % (742473)Instructions burned: 208 (million)
% 204.41/29.08 % (742475)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3240867601:i=232:rtra=on_2782 on theBenchmark for (2782ds/232Mi)
% 204.41/29.08 % (742475)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 204.41/29.08 % (742475)Instruction limit reached!
% 204.41/29.08 % (742475)------------------------------
% 204.41/29.08 % (742475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.41/29.08 % (742475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.41/29.08 % (742475)CaDiCaL version: 2.1.3
% 204.41/29.08 % (742475)Termination reason: Instruction limit
% 204.41/29.08 % (742475)Termination phase: Saturation
% 204.41/29.08 % (742475)Time elapsed: 0.114 s
% 204.41/29.08 % (742475)Peak memory usage: 13 MB
% 204.41/29.08 % (742475)Instructions burned: 232 (million)
% 204.41/29.08 % (742477)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2735586838:i=262:rtra=on_2781 on theBenchmark for (2781ds/262Mi)
% 204.41/29.08 % (742477)Instruction limit reached!
% 204.41/29.08 % (742477)------------------------------
% 204.41/29.08 % (742477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.41/29.08 % (742477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.41/29.08 % (742477)CaDiCaL version: 2.1.3
% 204.41/29.08 % (742477)Termination reason: Instruction limit
% 204.41/29.08 % (742477)Termination phase: Saturation
% 204.41/29.08 % (742477)Time elapsed: 0.129 s
% 204.41/29.08 % (742477)Peak memory usage: 13 MB
% 204.41/29.08 % (742477)Instructions burned: 264 (million)
% 204.41/29.08 % (742479)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2694795364:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2779 on theBenchmark for (2779ds/318Mi)
% 204.41/29.08 % (742479)Instruction limit reached!
% 204.41/29.08 % (742479)------------------------------
% 204.41/29.08 % (742479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.41/29.08 % (742479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.41/29.08 % (742479)CaDiCaL version: 2.1.3
% 204.41/29.08 % (742479)Termination reason: Instruction limit
% 204.41/29.08 % (742479)Termination phase: Saturation
% 204.41/29.08 % (742479)Time elapsed: 0.150 s
% 204.41/29.08 % (742479)Peak memory usage: 13 MB
% 204.41/29.08 % (742479)Instructions burned: 319 (million)
% 204.41/29.08 % (742481)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2460133084:i=1428:nm=2:rtra=on_2778 on theBenchmark for (2778ds/1428Mi)
% 204.41/29.08 % Exception at run slice level
% 204.41/29.08 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 204.41/29.08 % (742483)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2268905635:i=262:bd=preordered:rtra=on:fsd=on_2777 on theBenchmark for (2777ds/262Mi)
% 204.41/29.08 % (742483)Instruction limit reached!
% 204.41/29.08 % (742483)------------------------------
% 204.41/29.08 % (742483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.41/29.08 % (742483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.41/29.08 % (742483)CaDiCaL version: 2.1.3
% 204.41/29.08 % (742483)Termination reason: Instruction limit
% 204.41/29.08 % (742483)Termination phase: Saturation
% 204.41/29.08 % (742483)Time elapsed: 0.135 s
% 204.41/29.08 % (742483)Peak memory usage: 13 MB
% 204.41/29.08 % (742483)Instructions burned: 263 (million)
% 204.41/29.08 % (742485)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1604007889:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2776 on theBenchmark for (2776ds/1368Mi)
% 204.41/29.08 % (742485)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 204.41/29.08 % (742485)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 204.41/29.08 % (742485)Instruction limit reached!
% 204.41/29.08 % (742485)------------------------------
% 204.41/29.08 % (742485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.41/29.08 % (742485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.41/29.08 % (742485)CaDiCaL version: 2.1.3
% 204.41/29.08 % (742485)Termination reason: Instruction limit
% 204.41/29.08 % (742485)Termination phase: Saturation
% 204.41/29.08 % (742485)Time elapsed: 0.624 s
% 204.41/29.08 % (742485)Peak memory usage: 15 MB
% 204.41/29.08 % (742485)Instructions burned: 1369 (million)
% 204.41/29.08 % (742487)ott-21_1_sil=16000:si=on:fs=off:random_seed=2417643275:i=360:av=off:fsr=off:rtra=on_2769 on theBenchmark for (2769ds/360Mi)
% 241.83/34.38 % (742487)Instruction limit reached!
% 241.83/34.38 % (742487)------------------------------
% 241.83/34.38 % (742487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.83/34.38 % (742487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.83/34.38 % (742487)CaDiCaL version: 2.1.3
% 241.83/34.38 % (742487)Termination reason: Instruction limit
% 241.83/34.38 % (742487)Termination phase: Saturation
% 241.83/34.38 % (742487)Time elapsed: 0.170 s
% 241.83/34.38 % (742487)Peak memory usage: 13 MB
% 241.83/34.38 % (742487)Instructions burned: 362 (million)
% 241.83/34.38 % (742489)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1655104739:i=954:bd=all:rtra=on_2767 on theBenchmark for (2767ds/954Mi)
% 241.83/34.38 % (742489)Instruction limit reached!
% 241.83/34.38 % (742489)------------------------------
% 241.83/34.38 % (742489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.83/34.38 % (742489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.83/34.38 % (742489)CaDiCaL version: 2.1.3
% 241.83/34.38 % (742489)Termination reason: Instruction limit
% 241.83/34.38 % (742489)Termination phase: Saturation
% 241.83/34.38 % (742489)Time elapsed: 0.465 s
% 241.83/34.38 % (742489)Peak memory usage: 15 MB
% 241.83/34.38 % (742489)Instructions burned: 956 (million)
% 241.83/34.38 % (742491)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=418390084:fmbsr=1.3:i=1730:ins=25:rtra=on_2762 on theBenchmark for (2762ds/1730Mi)
% 241.83/34.38 % Exception at run slice level
% 241.83/34.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 241.83/34.38 % (742493)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4075125030:i=2358:rtra=on_2762 on theBenchmark for (2762ds/2358Mi)
% 241.83/34.38 % (742493)Instruction limit reached!
% 241.83/34.38 % (742493)------------------------------
% 241.83/34.38 % (742493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.83/34.38 % (742493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.83/34.38 % (742493)CaDiCaL version: 2.1.3
% 241.83/34.38 % (742493)Termination reason: Instruction limit
% 241.83/34.38 % (742493)Termination phase: Saturation
% 241.83/34.38 % (742493)Time elapsed: 1.134 s
% 241.83/34.38 % (742493)Peak memory usage: 19 MB
% 241.83/34.38 % (742493)Instructions burned: 2360 (million)
% 241.83/34.38 % (742495)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=1001732561:i=1778:ins=1:rtra=on_2751 on theBenchmark for (2751ds/1778Mi)
% 241.83/34.38 % Exception at run slice level
% 241.83/34.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 241.83/34.38 % (742497)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2023410894:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2750 on theBenchmark for (2750ds/1384Mi)
% 241.83/34.38 % (742497)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 241.83/34.38 % (742497)Instruction limit reached!
% 241.83/34.38 % (742497)------------------------------
% 241.83/34.38 % (742497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.83/34.38 % (742497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.83/34.38 % (742497)CaDiCaL version: 2.1.3
% 241.83/34.38 % (742497)Termination reason: Instruction limit
% 241.83/34.38 % (742497)Termination phase: Saturation
% 241.83/34.38 % (742497)Time elapsed: 0.696 s
% 241.83/34.38 % (742497)Peak memory usage: 20 MB
% 241.83/34.38 % (742497)Instructions burned: 1385 (million)
% 241.83/34.38 % (742499)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=3230801388:i=1758:kws=inv_precedence:fsr=off:rtra=on_2743 on theBenchmark for (2743ds/1758Mi)
% 241.83/34.38 % (742499)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 241.83/34.38 % (742126)Instruction limit reached!
% 241.83/34.38 % (742126)------------------------------
% 241.83/34.38 % (742126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 241.83/34.38 % (742126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.83/34.38 % (742126)CaDiCaL version: 2.1.3
% 241.83/34.38 % (742126)Termination reason: Instruction limit
% 241.83/34.38 % (742126)Termination phase: Saturation
% 241.83/34.38 % (742126)Time elapsed: 12.118 s
% 265.96/37.76 % (742126)Peak memory usage: 56 MB
% 265.96/37.76 % (742126)Instructions burned: 28123 (million)
% 265.96/37.76 % (742501)fmb+10_1_sil=64000:si=on:random_seed=2672113868:i=44122:nm=2:rtra=on:gsp=on_2738 on theBenchmark for (2738ds/44122Mi)
% 265.96/37.76 % (742501)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742503)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2381274574:i=19030:nm=5:rtra=on_2738 on theBenchmark for (2738ds/19030Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742505)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=18463166:fmbsr=1.7:i=1840:rtra=on_2738 on theBenchmark for (2738ds/1840Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742507)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3889357967:i=10262:rtra=on_2738 on theBenchmark for (2738ds/10262Mi)
% 265.96/37.76 % (742507)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 265.96/37.76 % (742499)Instruction limit reached!
% 265.96/37.76 % (742499)------------------------------
% 265.96/37.76 % (742499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742499)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742499)Termination reason: Instruction limit
% 265.96/37.76 % (742499)Termination phase: Saturation
% 265.96/37.76 % (742499)Time elapsed: 0.859 s
% 265.96/37.76 % (742499)Peak memory usage: 19 MB
% 265.96/37.76 % (742499)Instructions burned: 1760 (million)
% 265.96/37.76 % (742509)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3697386188:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2734 on theBenchmark for (2734ds/2944Mi)
% 265.96/37.76 % (742509)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 265.96/37.76 % (742509)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 265.96/37.76 % (742509)Instruction limit reached!
% 265.96/37.76 % (742509)------------------------------
% 265.96/37.76 % (742509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742509)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742509)Termination reason: Instruction limit
% 265.96/37.76 % (742509)Termination phase: Saturation
% 265.96/37.76 % (742509)Time elapsed: 1.490 s
% 265.96/37.76 % (742509)Peak memory usage: 21 MB
% 265.96/37.76 % (742509)Instructions burned: 2946 (million)
% 265.96/37.76 % (742511)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4159561351:i=12648:rtra=on_2719 on theBenchmark for (2719ds/12648Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742513)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=266043877:fmbsr=2.30978:i=4348:rtra=on_2719 on theBenchmark for (2719ds/4348Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742515)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=3680164522:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2719 on theBenchmark for (2719ds/1738Mi)
% 265.96/37.76 % (742515)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 265.96/37.76 % (742515)Instruction limit reached!
% 265.96/37.76 % (742515)------------------------------
% 265.96/37.76 % (742515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742515)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742515)Termination reason: Instruction limit
% 265.96/37.76 % (742515)Termination phase: Saturation
% 265.96/37.76 % (742515)Time elapsed: 0.744 s
% 265.96/37.76 % (742515)Peak memory usage: 15 MB
% 265.96/37.76 % (742515)Instructions burned: 1739 (million)
% 265.96/37.76 % (742539)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=3228086411:i=10228:av=off:rtra=on_2711 on theBenchmark for (2711ds/10228Mi)
% 265.96/37.76 % (742507)Instruction limit reached!
% 265.96/37.76 % (742507)------------------------------
% 265.96/37.76 % (742507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742507)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742507)Termination reason: Instruction limit
% 265.96/37.76 % (742507)Termination phase: Saturation
% 265.96/37.76 % (742507)Time elapsed: 4.700 s
% 265.96/37.76 % (742507)Peak memory usage: 27 MB
% 265.96/37.76 % (742507)Instructions burned: 10263 (million)
% 265.96/37.76 % (742889)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1431901877:i=108564:rtra=on_2690 on theBenchmark for (2690ds/108564Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742891)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1347773623:i=7024:aac=none:rtra=on_2690 on theBenchmark for (2690ds/7024Mi)
% 265.96/37.76 % (742891)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 265.96/37.76 % (741830)Instruction limit reached!
% 265.96/37.76 % (741830)------------------------------
% 265.96/37.76 % (741830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (741830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (741830)CaDiCaL version: 2.1.3
% 265.96/37.76 % (741830)Termination reason: Instruction limit
% 265.96/37.76 % (741830)Termination phase: Saturation
% 265.96/37.76 % (741830)Time elapsed: 31.188 s
% 265.96/37.76 % (741830)Peak memory usage: 168 MB
% 265.96/37.76 % (741830)Instructions burned: 135535 (million)
% 265.96/37.76 % (742893)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=86846783:i=7546:rtra=on:amm=off_2687 on theBenchmark for (2687ds/7546Mi)
% 265.96/37.76 % (742893)Instruction limit reached!
% 265.96/37.76 % (742893)------------------------------
% 265.96/37.76 % (742893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742893)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742893)Termination reason: Instruction limit
% 265.96/37.76 % (742893)Termination phase: Saturation
% 265.96/37.76 % (742893)Time elapsed: 1.822 s
% 265.96/37.76 % (742893)Peak memory usage: 24 MB
% 265.96/37.76 % (742893)Instructions burned: 7550 (million)
% 265.96/37.76 % (742895)ott+11_1_sil=16000:si=on:gs=on:random_seed=685839999:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2669 on theBenchmark for (2669ds/4502Mi)
% 265.96/37.76 % (742895)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 265.96/37.76 % (742539)Instruction limit reached!
% 265.96/37.76 % (742539)------------------------------
% 265.96/37.76 % (742539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742539)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742539)Termination reason: Instruction limit
% 265.96/37.76 % (742539)Termination phase: Saturation
% 265.96/37.76 % (742539)Time elapsed: 4.859 s
% 265.96/37.76 % (742539)Peak memory usage: 31 MB
% 265.96/37.76 % (742539)Instructions burned: 10229 (million)
% 265.96/37.76 % (742897)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2502052548:fmbsr=1.6:i=135068:rtra=on_2662 on theBenchmark for (2662ds/135068Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742899)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=997802115:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2662 on theBenchmark for (2662ds/9182Mi)
% 265.96/37.76 % (742895)Instruction limit reached!
% 265.96/37.76 % (742895)------------------------------
% 265.96/37.76 % (742895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742895)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742895)Termination reason: Instruction limit
% 265.96/37.76 % (742895)Termination phase: Saturation
% 265.96/37.76 % (742895)Time elapsed: 1.086 s
% 265.96/37.76 % (742895)Peak memory usage: 21 MB
% 265.96/37.76 % (742895)Instructions burned: 4504 (million)
% 265.96/37.76 % (742891)Instruction limit reached!
% 265.96/37.76 % (742891)------------------------------
% 265.96/37.76 % (742891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742891)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742891)Termination reason: Instruction limit
% 265.96/37.76 % (742891)Termination phase: Saturation
% 265.96/37.76 % (742891)Time elapsed: 3.210 s
% 265.96/37.76 % (742891)Peak memory usage: 23 MB
% 265.96/37.76 % (742891)Instructions burned: 7025 (million)
% 265.96/37.76 % (742901)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=1103720454:i=58680:rtra=on_2658 on theBenchmark for (2658ds/58680Mi)
% 265.96/37.76 % (742902)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=562037240:i=10422:rtra=on_2658 on theBenchmark for (2658ds/10422Mi)
% 265.96/37.76 % (742073)Instruction limit reached!
% 265.96/37.76 % (742073)------------------------------
% 265.96/37.76 % (742073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742073)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742073)Termination reason: Instruction limit
% 265.96/37.76 % (742073)Termination phase: Saturation
% 265.96/37.76 % (742073)Time elapsed: 22.874 s
% 265.96/37.76 % (742073)Peak memory usage: 163 MB
% 265.96/37.76 % (742073)Instructions burned: 53297 (million)
% 265.96/37.76 % (742905)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=144082817:i=10994:nm=2:rtra=on_2633 on theBenchmark for (2633ds/10994Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742907)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=1735766733:fmbsr=2:i=92664:rtra=on_2633 on theBenchmark for (2633ds/92664Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742909)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=2132926180:i=28142:rtra=on_2633 on theBenchmark for (2633ds/28142Mi)
% 265.96/37.76 % Exception at run slice level
% 265.96/37.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 265.96/37.76 % (742911)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2198937698:i=45130:add=on:rtra=on:rawr=on_2633 on theBenchmark for (2633ds/45130Mi)
% 265.96/37.76 % (742911) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-741824-742911"...
% 265.96/37.76 % (742911)...printing done.
% 265.96/37.76 % (742911)Refutation found. Thanks to Tanya!
% 265.96/37.76 % SZS status Theorem for theBenchmark
% 265.96/37.76 % SZS output start Proof for theBenchmark
% See solution above
% 265.96/37.76 % (742911)------------------------------
% 265.96/37.76 % (742911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 265.96/37.76 % (742911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 265.96/37.76 % (742911)CaDiCaL version: 2.1.3
% 265.96/37.76 % (742911)Termination reason: Refutation
% 265.96/37.76 % (742911)Time elapsed: 0.807 s
% 265.96/37.76 % (742911)Peak memory usage: 17 MB
% 265.96/37.76 % (742911)Instructions burned: 1666 (million)
% 265.96/37.76 % (741824)Success in time 37.538 s
% 265.96/37.76 % Vampire exiting
%------------------------------------------------------------------------------