%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV742-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 : Tue Sep 29 01:19:23 PM UTC 2026
% Result : Unsatisfiable 7.89s 1.98s
% Output : Refutation 9.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 24
% Syntax : Number of formulae : 152 ( 16 unt; 18 def)
% Number of atoms : 400 ( 105 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 411 ( 163 ~; 230 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 19 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 195 ( 0 sgn 195 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f43,axiom,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(X0,X1))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_keymode_Oinduct_0) ).
fof(f53,axiom,
c_Public_Okeymode_OEncryption != c_Public_Okeymode_OSignature,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_keymode_Osimps_I2_J_0) ).
fof(f54,plain,
c_Public_Okeymode_OSignature != c_Public_Okeymode_OEncryption,
inference(reorient_equations,[],[f53]) ).
fof(f59,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f487,axiom,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X3))
| ~ hBOOL(hAPP(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__code_2) ).
fof(f512,axiom,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(X0,X1))
| X2 = X1
| ~ hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__code_0) ).
fof(f513,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1))
| X1 = X2
| hBOOL(hAPP(X0,X1)) ),
inference(reorient_equations,[],[f512]) ).
fof(f534,axiom,
! [X2,X0,X1] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f815,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(X1,X0,X2),c_Public_Okeymode_OSignature))
| hBOOL(hAPP(c_Set_Oinsert(X1,X0,X2),X3))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption)) ),
inference(resolution,[],[f487,f43]) ).
fof(f817,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption)) ),
inference(resolution,[],[f534,f815]) ).
fof(f818,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),c_Public_Okeymode_OSignature))
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2)) ),
inference(resolution,[],[f534,f43]) ).
fof(f819,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) ),
inference(resolution,[],[f818,f487]) ).
fof(f829,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X1,c_Public_Okeymode_OSignature))
| hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OEncryption = X0 ),
inference(resolution,[],[f513,f819]) ).
fof(f830,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X1,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[],[f513,f817]) ).
fof(f832,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2))
| c_Public_Okeymode_OSignature = X2 ),
inference(resolution,[],[f830,f534]) ).
fof(f837,plain,
! [X0,X1] :
( hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[],[f832,f513]) ).
fof(f840,plain,
! [X0] :
( c_Public_Okeymode_OSignature = X0
| c_Public_Okeymode_OEncryption = X0 ),
inference(resolution,[],[f837,f59]) ).
fof(f846,plain,
! [X0,X1] :
( X0 = X1
| c_Public_Okeymode_OEncryption = X1
| c_Public_Okeymode_OEncryption = X0 ),
inference(superposition,[],[f840,f840]) ).
fof(f869,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption ),
inference(superposition,[],[f59,f840]) ).
fof(f1067,definition,
( spl25_37
<=> ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl25_37])],[avatar_definition]) ).
fof(f1068,plain,
( ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1)
| ~ spl25_37 ),
inference(avatar_component_clause,[],[f1067]) ).
fof(f1087,definition,
( spl25_42
<=> ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption ),
introduced(definition,[new_symbols(definition,[spl25_42])],[avatar_definition]) ).
fof(f1088,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption
| ~ spl25_42 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1090,definition,
( spl25_43
<=> ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1)) ),
introduced(definition,[new_symbols(definition,[spl25_43])],[avatar_definition]) ).
fof(f1091,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1))
| ~ spl25_43 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1092,plain,
( spl25_42
| spl25_43 ),
inference(avatar_split_clause,[],[f869,f1090,f1087]) ).
fof(f1165,definition,
( spl25_60
<=> ! [X0] : ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) ),
introduced(definition,[new_symbols(definition,[spl25_60])],[avatar_definition]) ).
fof(f1166,plain,
( ! [X0] : ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| ~ spl25_60 ),
inference(avatar_component_clause,[],[f1165]) ).
fof(f1249,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Public_Okeymode_OEncryption
| c_Public_Okeymode_OEncryption = X0 ),
inference(superposition,[],[f59,f846]) ).
fof(f1309,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = X2
| c_Public_Okeymode_OEncryption = X2 ),
inference(superposition,[],[f59,f846]) ).
fof(f1315,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ),
inference(superposition,[],[f819,f846]) ).
fof(f1448,definition,
( spl25_63
<=> ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2)) ),
introduced(definition,[new_symbols(definition,[spl25_63])],[avatar_definition]) ).
fof(f1449,plain,
( ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| ~ spl25_63 ),
inference(avatar_component_clause,[],[f1448]) ).
fof(f1460,definition,
( spl25_66
<=> ! [X0,X1,X3] :
( ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X3
| c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_66])],[avatar_definition]) ).
fof(f1461,plain,
( ! [X3,X0,X1] :
( ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X3
| c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3 )
| ~ spl25_66 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1480,definition,
( spl25_70
<=> hBOOL(c_Public_Okeymode_OEncryption) ),
introduced(definition,[new_symbols(definition,[spl25_70])],[avatar_definition]) ).
fof(f1481,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| spl25_70 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1482,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_70 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1551,plain,
( spl25_66
| spl25_63 ),
inference(avatar_split_clause,[],[f1315,f1448,f1460]) ).
fof(f1554,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_42 ),
inference(forward_demodulation,[],[f1309,f1088]) ).
fof(f1555,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) )
| ~ spl25_42 ),
inference(duplicate_literal_removal,[],[f1554]) ).
fof(f1650,definition,
( spl25_84
<=> ! [X1] : c_Public_Okeymode_OEncryption = X1 ),
introduced(definition,[new_symbols(definition,[spl25_84])],[avatar_definition]) ).
fof(f1651,plain,
( ! [X1] : c_Public_Okeymode_OEncryption = X1
| ~ spl25_84 ),
inference(avatar_component_clause,[],[f1650]) ).
fof(f1661,definition,
( spl25_85
<=> ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) ),
introduced(definition,[new_symbols(definition,[spl25_85])],[avatar_definition]) ).
fof(f1662,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| ~ spl25_85 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1699,plain,
( spl25_85
| spl25_84
| ~ spl25_42 ),
inference(avatar_split_clause,[],[f1555,f1087,f1650,f1661]) ).
fof(f1878,definition,
( spl25_102
<=> ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 ) ),
introduced(definition,[new_symbols(definition,[spl25_102])],[avatar_definition]) ).
fof(f1879,plain,
( ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_102 ),
inference(avatar_component_clause,[],[f1878]) ).
fof(f1880,plain,
( spl25_42
| spl25_102 ),
inference(avatar_split_clause,[],[f1249,f1878,f1087]) ).
fof(f2119,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_84 ),
inference(superposition,[],[f59,f1651]) ).
fof(f2123,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_84 ),
inference(superposition,[],[f534,f1651]) ).
fof(f2131,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| ~ spl25_84 ),
inference(superposition,[],[f59,f1651]) ).
fof(f2185,plain,
( $false
| ~ spl25_63
| ~ spl25_84 ),
inference(forward_subsumption_resolution,[],[f2131,f1449]) ).
fof(f2186,plain,
( ~ spl25_63
| ~ spl25_84 ),
inference(avatar_contradiction_clause,[],[f2185]) ).
fof(f2191,plain,
( $false
| spl25_70
| ~ spl25_84 ),
inference(forward_subsumption_resolution,[],[f2123,f1481]) ).
fof(f2192,plain,
( spl25_70
| ~ spl25_84 ),
inference(avatar_contradiction_clause,[],[f2191]) ).
fof(f2197,plain,
( $false
| ~ spl25_63
| ~ spl25_85 ),
inference(forward_subsumption_resolution,[],[f1662,f1449]) ).
fof(f2198,plain,
( ~ spl25_63
| ~ spl25_85 ),
inference(avatar_contradiction_clause,[],[f2197]) ).
fof(f2473,plain,
( $false
| ~ spl25_70
| ~ spl25_84 ),
inference(forward_subsumption_resolution,[],[f2119,f1482]) ).
fof(f2474,plain,
( ~ spl25_70
| ~ spl25_84 ),
inference(avatar_contradiction_clause,[],[f2473]) ).
fof(f2489,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2))
| c_Public_Okeymode_OEncryption = X2 ),
inference(resolution,[],[f829,f534]) ).
fof(f2519,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2
| c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ),
inference(superposition,[],[f2489,f846]) ).
fof(f2523,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Public_Okeymode_OSignature,X2))
| c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) ),
inference(superposition,[],[f2489,f840]) ).
fof(f2532,plain,
( ! [X2,X0,X1] :
( c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) )
| ~ spl25_43 ),
inference(forward_subsumption_resolution,[],[f2523,f1091]) ).
fof(f2534,definition,
( spl25_150
<=> ! [X2,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X1,X2) ),
introduced(definition,[new_symbols(definition,[spl25_150])],[avatar_definition]) ).
fof(f2535,plain,
( ! [X2,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X1,X2)
| ~ spl25_150 ),
inference(avatar_component_clause,[],[f2534]) ).
fof(f2542,plain,
( ! [X2,X3,X0,X1] :
( c_Public_Okeymode_OEncryption = X2
| c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_85 ),
inference(forward_subsumption_resolution,[],[f2519,f1662]) ).
fof(f2545,plain,
( spl25_150
| spl25_84
| ~ spl25_43 ),
inference(avatar_split_clause,[],[f2532,f1090,f1650,f2534]) ).
fof(f2547,definition,
( spl25_152
<=> ! [X0,X1,X3] :
( c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_152])],[avatar_definition]) ).
fof(f2548,plain,
( ! [X3,X0,X1] :
( c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_152 ),
inference(avatar_component_clause,[],[f2547]) ).
fof(f2550,plain,
( spl25_152
| spl25_84
| ~ spl25_85 ),
inference(avatar_split_clause,[],[f2542,f1661,f1650,f2547]) ).
fof(f2559,plain,
( ! [X2,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_150 ),
inference(forward_demodulation,[],[f2519,f2535]) ).
fof(f2560,plain,
( ! [X2,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_150 ),
inference(duplicate_literal_removal,[],[f2559]) ).
fof(f2566,definition,
( spl25_154
<=> ! [X2] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 ) ),
introduced(definition,[new_symbols(definition,[spl25_154])],[avatar_definition]) ).
fof(f2567,plain,
( ! [X2] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_154 ),
inference(avatar_component_clause,[],[f2566]) ).
fof(f2569,plain,
( spl25_154
| spl25_84
| ~ spl25_150 ),
inference(avatar_split_clause,[],[f2560,f2534,f1650,f2566]) ).
fof(f2582,plain,
( ! [X2] : c_Public_Okeymode_OEncryption = X2
| ~ spl25_85
| ~ spl25_154 ),
inference(forward_subsumption_resolution,[],[f2567,f1662]) ).
fof(f2583,plain,
( spl25_84
| ~ spl25_85
| ~ spl25_154 ),
inference(avatar_split_clause,[],[f2582,f2566,f1661,f1650]) ).
fof(f2635,plain,
( ! [X0] :
( hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_152 ),
inference(superposition,[],[f534,f2548]) ).
fof(f2699,plain,
( ! [X0] : c_Public_Okeymode_OEncryption = X0
| ~ spl25_60
| ~ spl25_152 ),
inference(forward_subsumption_resolution,[],[f2635,f1166]) ).
fof(f2709,plain,
( spl25_84
| ~ spl25_60
| ~ spl25_152 ),
inference(avatar_split_clause,[],[f2699,f2547,f1165,f1650]) ).
fof(f2725,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(X0,X1))
| X0 = X1
| X0 = X2
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_154 ),
inference(superposition,[],[f2567,f846]) ).
fof(f2736,plain,
( ! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Public_Okeymode_OEncryption
| ~ spl25_102 ),
inference(resolution,[],[f1879,f534]) ).
fof(f2757,plain,
( ! [X2,X3,X0,X1,X4] :
( c_Set_Oinsert(X0,X1,X2) = X3
| c_Set_Oinsert(X0,X1,X2) = X4
| c_Public_Okeymode_OEncryption = X4
| X0 = X3
| hBOOL(hAPP(X1,X3)) )
| ~ spl25_154 ),
inference(resolution,[],[f2725,f513]) ).
fof(f2766,plain,
( ! [X2,X3,X0,X1,X4] :
( c_Public_Okeymode_OEncryption = X3
| c_Set_Oinsert(X0,X1,X2) = X4
| c_Public_Okeymode_OEncryption = X4
| X0 = X3
| hBOOL(hAPP(X1,X3)) )
| ~ spl25_102
| ~ spl25_154 ),
inference(forward_demodulation,[],[f2757,f2736]) ).
fof(f2769,plain,
( ! [X3,X0,X1,X4] :
( c_Public_Okeymode_OEncryption = X4
| c_Public_Okeymode_OEncryption = X3
| c_Public_Okeymode_OEncryption = X4
| X0 = X3
| hBOOL(hAPP(X1,X3)) )
| ~ spl25_102
| ~ spl25_154 ),
inference(forward_demodulation,[],[f2766,f2736]) ).
fof(f2770,plain,
( ! [X3,X0,X1,X4] :
( c_Public_Okeymode_OEncryption = X4
| c_Public_Okeymode_OEncryption = X3
| X0 = X3
| hBOOL(hAPP(X1,X3)) )
| ~ spl25_102
| ~ spl25_154 ),
inference(duplicate_literal_removal,[],[f2769]) ).
fof(f2774,definition,
( spl25_163
<=> ! [X0,X1,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(X1,X3))
| X0 = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_163])],[avatar_definition]) ).
fof(f2775,plain,
( ! [X3,X0,X1] :
( hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OEncryption = X3
| X0 = X3 )
| ~ spl25_163 ),
inference(avatar_component_clause,[],[f2774]) ).
fof(f2776,plain,
( spl25_163
| spl25_84
| ~ spl25_102
| ~ spl25_154 ),
inference(avatar_split_clause,[],[f2770,f2566,f1878,f1650,f2774]) ).
fof(f2789,plain,
( ! [X3,X0] :
( c_Public_Okeymode_OEncryption = X3
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_37
| ~ spl25_66 ),
inference(forward_demodulation,[],[f1461,f1068]) ).
fof(f2790,plain,
( ! [X3,X0] :
( c_Public_Okeymode_OEncryption = X3
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) )
| ~ spl25_37
| ~ spl25_66 ),
inference(duplicate_literal_removal,[],[f2789]) ).
fof(f2796,plain,
( spl25_60
| spl25_84
| ~ spl25_37
| ~ spl25_66 ),
inference(avatar_split_clause,[],[f2790,f1460,f1067,f1650,f1165]) ).
fof(f2936,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),c_Public_Okeymode_OSignature))
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X4))
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X2,X3) )
| ~ spl25_152 ),
inference(superposition,[],[f818,f2548]) ).
fof(f2945,plain,
( ! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X4))
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X2,X3) )
| ~ spl25_152 ),
inference(forward_subsumption_resolution,[],[f2936,f534]) ).
fof(f2959,definition,
( spl25_166
<=> ! [X4,X0,X1] : hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X4)) ),
introduced(definition,[new_symbols(definition,[spl25_166])],[avatar_definition]) ).
fof(f2960,plain,
( ! [X0,X1,X4] : hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X4))
| ~ spl25_166 ),
inference(avatar_component_clause,[],[f2959]) ).
fof(f2961,plain,
( spl25_37
| spl25_166
| ~ spl25_152 ),
inference(avatar_split_clause,[],[f2945,f2547,f2959,f1067]) ).
fof(f2964,definition,
( spl25_167
<=> ! [X1,X3] :
( c_Public_Okeymode_OSignature = X3
| hBOOL(hAPP(X1,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl25_167])],[avatar_definition]) ).
fof(f2965,plain,
( ! [X3,X1] :
( hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OSignature = X3 )
| ~ spl25_167 ),
inference(avatar_component_clause,[],[f2964]) ).
fof(f2968,plain,
( ! [X0] : c_Public_Okeymode_OSignature = X0
| ~ spl25_167 ),
inference(resolution,[],[f2965,f59]) ).
fof(f3029,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1))
| ~ spl25_167 ),
inference(superposition,[],[f59,f2968]) ).
fof(f3067,plain,
( spl25_43
| ~ spl25_167 ),
inference(avatar_split_clause,[],[f3029,f2964,f1090]) ).
fof(f3087,definition,
( spl25_168
<=> ! [X1] : c_Public_Okeymode_OSignature = X1 ),
introduced(definition,[new_symbols(definition,[spl25_168])],[avatar_definition]) ).
fof(f3088,plain,
( ! [X1] : c_Public_Okeymode_OSignature = X1
| ~ spl25_168 ),
inference(avatar_component_clause,[],[f3087]) ).
fof(f3095,plain,
( ! [X2,X0,X1] :
( c_Public_Okeymode_OSignature = c_Public_Okeymode_OEncryption
| c_Public_Okeymode_OSignature = X0
| hBOOL(hAPP(X1,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_163 ),
inference(resolution,[],[f2775,f829]) ).
fof(f3144,plain,
( ! [X0] : hBOOL(hAPP(c_Public_Okeymode_OSignature,X0))
| ~ spl25_168 ),
inference(superposition,[],[f534,f3088]) ).
fof(f3180,plain,
( $false
| ~ spl25_43
| ~ spl25_168 ),
inference(forward_subsumption_resolution,[],[f3144,f1091]) ).
fof(f3181,plain,
( ~ spl25_43
| ~ spl25_168 ),
inference(avatar_contradiction_clause,[],[f3180]) ).
fof(f3193,plain,
( ! [X0,X1] :
( c_Public_Okeymode_OSignature = X0
| hBOOL(hAPP(X1,X0)) )
| ~ spl25_166 ),
inference(resolution,[],[f2960,f513]) ).
fof(f3220,plain,
( spl25_167
| ~ spl25_166 ),
inference(avatar_split_clause,[],[f3193,f2959,f2964]) ).
fof(f3600,plain,
( ! [X2,X0,X1] :
( c_Public_Okeymode_OSignature = X0
| hBOOL(hAPP(X1,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_163 ),
inference(forward_subsumption_resolution,[],[f3095,f54]) ).
fof(f3603,definition,
( spl25_184
<=> ! [X2,X1] :
( hBOOL(hAPP(X1,X2))
| c_Public_Okeymode_OEncryption = X2 ) ),
introduced(definition,[new_symbols(definition,[spl25_184])],[avatar_definition]) ).
fof(f3604,plain,
( ! [X2,X1] :
( hBOOL(hAPP(X1,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_184 ),
inference(avatar_component_clause,[],[f3603]) ).
fof(f3605,plain,
( spl25_184
| spl25_168
| ~ spl25_163 ),
inference(avatar_split_clause,[],[f3600,f2774,f3087,f3603]) ).
fof(f3606,plain,
( ! [X0] : c_Public_Okeymode_OEncryption = X0
| ~ spl25_184 ),
inference(resolution,[],[f3604,f59]) ).
fof(f3624,plain,
( spl25_84
| ~ spl25_184 ),
inference(avatar_split_clause,[],[f3606,f3603,f1650]) ).
cnf(s25,plain,
( spl25_42
| spl25_43 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s56,plain,
( spl25_63
| spl25_66 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s92,plain,
( ~ spl25_42
| spl25_84
| spl25_85 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s149,plain,
( spl25_42
| spl25_102 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s198,plain,
( ~ spl25_63
| ~ spl25_84 ),
inference(sat_conversion,[],[f2186]) ).
cnf(s200,plain,
( spl25_70
| ~ spl25_84 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s201,plain,
( ~ spl25_63
| ~ spl25_85 ),
inference(sat_conversion,[],[f2198]) ).
cnf(s272,plain,
( ~ spl25_70
| ~ spl25_84 ),
inference(sat_conversion,[],[f2474]) ).
cnf(s276,plain,
( ~ spl25_43
| spl25_84
| spl25_150 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s278,plain,
( spl25_84
| ~ spl25_85
| spl25_152 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s281,plain,
( spl25_84
| ~ spl25_150
| spl25_154 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s287,plain,
( spl25_84
| ~ spl25_85
| ~ spl25_154 ),
inference(sat_conversion,[],[f2583]) ).
cnf(s295,plain,
( ~ spl25_60
| spl25_84
| ~ spl25_152 ),
inference(sat_conversion,[],[f2709]) ).
cnf(s303,plain,
( spl25_84
| ~ spl25_102
| ~ spl25_154
| spl25_163 ),
inference(sat_conversion,[],[f2776]) ).
cnf(s309,plain,
( ~ spl25_37
| spl25_60
| ~ spl25_66
| spl25_84 ),
inference(sat_conversion,[],[f2796]) ).
cnf(s315,plain,
( spl25_37
| ~ spl25_152
| spl25_166 ),
inference(sat_conversion,[],[f2961]) ).
cnf(s319,plain,
( spl25_43
| ~ spl25_167 ),
inference(sat_conversion,[],[f3067]) ).
cnf(s324,plain,
( ~ spl25_43
| ~ spl25_168 ),
inference(sat_conversion,[],[f3181]) ).
cnf(s329,plain,
( ~ spl25_166
| spl25_167 ),
inference(sat_conversion,[],[f3220]) ).
cnf(s349,plain,
( ~ spl25_163
| spl25_168
| spl25_184 ),
inference(sat_conversion,[],[f3605]) ).
cnf(s352,plain,
( spl25_84
| ~ spl25_184 ),
inference(sat_conversion,[],[f3624]) ).
cnf(s356,plain,
( ~ spl25_63
| ~ spl25_42 ),
inference(rat,[],[s92,s198,s201]) ).
cnf(s357,plain,
( spl25_84
| spl25_152
| ~ spl25_42 ),
inference(rat,[],[s92,s278]) ).
cnf(s358,plain,
~ spl25_84,
inference(rat,[],[s200,s272]) ).
cnf(s359,plain,
~ spl25_184,
inference(rat,[],[s352,s358]) ).
cnf(s361,plain,
spl25_43,
inference(rat,[],[s309,s295,s315,s56,s357,s356,s329,s25,s319,s358]) ).
cnf(s362,plain,
~ spl25_168,
inference(rat,[],[s324,s361]) ).
cnf(s363,plain,
spl25_150,
inference(rat,[],[s276,s358,s361]) ).
cnf(s365,plain,
~ spl25_163,
inference(rat,[],[s349,s359,s362]) ).
cnf(s366,plain,
spl25_154,
inference(rat,[],[s281,s358,s363]) ).
cnf(s369,plain,
~ spl25_85,
inference(rat,[],[s287,s358,s366]) ).
cnf(s370,plain,
~ spl25_102,
inference(rat,[],[s303,s365,s358,s366]) ).
cnf(s373,plain,
~ spl25_42,
inference(rat,[],[s92,s358,s369]) ).
cnf(s374,plain,
$false,
inference(rat,[],[s149,s370,s373]) ).
fof(f3632,plain,
$false,
inference(avatar_sat_refutation,[],[s374]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV742-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 12:25:32 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.89/1.98 % (1892131)Input is clausal, will run a generic CNF schedule.
% 7.89/1.98 % (1892137)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1123015824:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.89/1.98 % (1892140)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=347004869:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.89/1.98 % (1892136)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3978047322:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.89/1.98 % (1892139)lrs+10_1_sil=8000:sp=occurrence:random_seed=2164551114:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.89/1.98 % (1892138)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1933368221:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.89/1.98 % (1892142)dis-21_1_sil=8000:lcm=predicate:random_seed=398306499:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.89/1.98 % (1892141)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4029166254:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.89/1.98 % (1892142)Instruction limit reached!
% 7.89/1.98 % (1892142)------------------------------
% 7.89/1.98 % (1892142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892142)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892142)Termination reason: Instruction limit
% 7.89/1.98 % (1892142)Termination phase: Saturation
% 7.89/1.98 % (1892142)Time elapsed: 0.070 s
% 7.89/1.98 % (1892142)Peak memory usage: 89 MB
% 7.89/1.98 % (1892142)Instructions burned: 117 (million)
% 7.89/1.98 % (1892139)Instruction limit reached!
% 7.89/1.98 % (1892139)------------------------------
% 7.89/1.98 % (1892139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892139)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892139)Termination reason: Instruction limit
% 7.89/1.98 % (1892139)Termination phase: Saturation
% 7.89/1.98 % (1892139)Time elapsed: 0.073 s
% 7.89/1.98 % (1892139)Peak memory usage: 89 MB
% 7.89/1.98 % (1892139)Instructions burned: 108 (million)
% 7.89/1.98 % (1892140)Instruction limit reached!
% 7.89/1.98 % (1892140)------------------------------
% 7.89/1.98 % (1892140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892140)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892140)Termination reason: Instruction limit
% 7.89/1.98 % (1892140)Termination phase: Saturation
% 7.89/1.98 % (1892140)Time elapsed: 0.076 s
% 7.89/1.98 % (1892140)Peak memory usage: 88 MB
% 7.89/1.98 % (1892140)Instructions burned: 115 (million)
% 7.89/1.98 % (1892141)Instruction limit reached!
% 7.89/1.98 % (1892141)------------------------------
% 7.89/1.98 % (1892141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892141)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892141)Termination reason: Instruction limit
% 7.89/1.98 % (1892141)Termination phase: Saturation
% 7.89/1.98 % (1892141)Time elapsed: 0.117 s
% 7.89/1.98 % (1892141)Peak memory usage: 90 MB
% 7.89/1.98 % (1892141)Instructions burned: 180 (million)
% 7.89/1.98 % (1892150)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1946134779:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.89/1.98 % (1892151)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2817884113:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.89/1.98 % (1892152)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1403814188:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.89/1.98 % (1892150)Refutation not found, incomplete strategy
% 7.89/1.98 % (1892150)------------------------------
% 7.89/1.98 % (1892150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892150)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892150)Termination reason: Refutation not found, incomplete strategy
% 7.89/1.98 % (1892150)Time elapsed: 0.032 s
% 7.89/1.98 % (1892150)Peak memory usage: 89 MB
% 7.89/1.98 % (1892150)Instructions burned: 51 (million)
% 7.89/1.98 % (1892152)Refutation not found, incomplete strategy
% 7.89/1.98 % (1892152)------------------------------
% 7.89/1.98 % (1892152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892152)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892152)Termination reason: Refutation not found, incomplete strategy
% 7.89/1.98 % (1892152)Time elapsed: 0.036 s
% 7.89/1.98 % (1892152)Peak memory usage: 89 MB
% 7.89/1.98 % (1892152)Instructions burned: 60 (million)
% 7.89/1.98 % (1892153)lrs+10_64_to=lpo:sil=8000:random_seed=2545298886:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 7.89/1.98 % (1892151)Instruction limit reached!
% 7.89/1.98 % (1892151)------------------------------
% 7.89/1.98 % (1892151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892151)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892151)Termination reason: Instruction limit
% 7.89/1.98 % (1892151)Termination phase: Saturation
% 7.89/1.98 % (1892151)Time elapsed: 0.106 s
% 7.89/1.98 % (1892151)Peak memory usage: 90 MB
% 7.89/1.98 % (1892151)Instructions burned: 189 (million)
% 7.89/1.98 % (1892153)Instruction limit reached!
% 7.89/1.98 % (1892153)------------------------------
% 7.89/1.98 % (1892153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892153)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892153)Termination reason: Instruction limit
% 7.89/1.98 % (1892153)Termination phase: Saturation
% 7.89/1.98 % (1892153)Time elapsed: 0.077 s
% 7.89/1.98 % (1892153)Peak memory usage: 90 MB
% 7.89/1.98 % (1892153)Instructions burned: 126 (million)
% 7.89/1.98 % (1892150)------------------------------
% 7.89/1.98 % (1892150)------------------------------
% 7.89/1.98 % (1892152)------------------------------
% 7.89/1.98 % (1892152)------------------------------
% 7.89/1.98 % (1892158)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3402825486:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 7.89/1.98 % (1892159)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3122028747:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 7.89/1.98 % (1892158)Instruction limit reached!
% 7.89/1.98 % (1892158)------------------------------
% 7.89/1.98 % (1892158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892158)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892158)Termination reason: Instruction limit
% 7.89/1.98 % (1892158)Termination phase: Saturation
% 7.89/1.98 % (1892158)Time elapsed: 0.118 s
% 7.89/1.98 % (1892158)Peak memory usage: 90 MB
% 7.89/1.98 % (1892158)Instructions burned: 194 (million)
% 7.89/1.98 % (1892160)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3918316755:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 7.89/1.98 % (1892159)Instruction limit reached!
% 7.89/1.98 % (1892159)------------------------------
% 7.89/1.98 % (1892159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892159)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892159)Termination reason: Instruction limit
% 7.89/1.98 % (1892159)Termination phase: Saturation
% 7.89/1.98 % (1892159)Time elapsed: 0.104 s
% 7.89/1.98 % (1892159)Peak memory usage: 91 MB
% 7.89/1.98 % (1892159)Instructions burned: 158 (million)
% 7.89/1.98 % (1892162)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=4232751011:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 7.89/1.98 % (1892162)Instruction limit reached!
% 7.89/1.98 % (1892162)------------------------------
% 7.89/1.98 % (1892162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892162)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892162)Termination reason: Instruction limit
% 7.89/1.98 % (1892162)Termination phase: Saturation
% 7.89/1.98 % (1892162)Time elapsed: 0.060 s
% 7.89/1.98 % (1892162)Peak memory usage: 90 MB
% 7.89/1.98 % (1892162)Instructions burned: 107 (million)
% 7.89/1.98 % (1892164)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=138542217:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 7.89/1.98 % (1892166)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=445946521:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 7.89/1.98 % (1892164)Instruction limit reached!
% 7.89/1.98 % (1892164)------------------------------
% 7.89/1.98 % (1892164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892164)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892164)Termination reason: Instruction limit
% 7.89/1.98 % (1892164)Termination phase: Saturation
% 7.89/1.98 % (1892164)Time elapsed: 0.068 s
% 7.89/1.98 % (1892164)Peak memory usage: 90 MB
% 7.89/1.98 % (1892164)Instructions burned: 107 (million)
% 7.89/1.98 % (1892136)First to succeed.
% 7.89/1.98 % (1892136)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1892131"
% 7.89/1.98 % (1892168)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2282494999:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 7.89/1.98 % (1892166)Instruction limit reached!
% 7.89/1.98 % (1892166)------------------------------
% 7.89/1.98 % (1892166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892166)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892166)Termination reason: Instruction limit
% 7.89/1.98 % (1892166)Termination phase: Saturation
% 7.89/1.98 % (1892166)Time elapsed: 0.150 s
% 7.89/1.98 % (1892166)Peak memory usage: 90 MB
% 7.89/1.98 % (1892166)Instructions burned: 242 (million)
% 7.89/1.98 % (1892171)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1533238482:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 7.89/1.98 % (1892171)Instruction limit reached!
% 7.89/1.98 % (1892171)------------------------------
% 7.89/1.98 % (1892171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.89/1.98 % (1892171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.89/1.98 % (1892171)CaDiCaL version: 2.1.3
% 7.89/1.98 % (1892171)Termination reason: Instruction limit
% 7.89/1.98 % (1892171)Termination phase: Saturation
% 7.89/1.98 % (1892171)Time elapsed: 0.091 s
% 7.89/1.98 % (1892171)Peak memory usage: 90 MB
% 7.89/1.98 % (1892171)Instructions burned: 134 (million)
% 7.89/1.98 % (1892136)Refutation found. Thanks to Tanya!
% 7.89/1.98 % SZS status Unsatisfiable for theBenchmark
% 7.89/1.98 % SZS output start Proof for theBenchmark
% See solution above
% 9.56/2.12 % (1892136)------------------------------
% 9.56/2.12 % (1892136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.56/2.12 % (1892136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.56/2.12 % (1892136)CaDiCaL version: 2.1.3
% 9.56/2.12 % (1892136)Termination reason: Refutation
% 9.56/2.12 % (1892136)Time elapsed: 0.845 s
% 9.56/2.12 % (1892136)Peak memory usage: 134 MB
% 9.56/2.12 % (1892136)Instructions burned: 1350 (million)
% 9.56/2.12 % (1892136)------------------------------
% 9.56/2.12 % (1892136)------------------------------
% 9.56/2.12 % (1892131)Success in time 1.301 s
% 9.56/2.12 % Vampire exiting
%------------------------------------------------------------------------------