%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV743-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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.29s 1.79s
% Output : Refutation 9.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 21
% Syntax : Number of formulae : 138 ( 12 unt; 16 def)
% Number of atoms : 378 ( 106 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 389 ( 149 ~; 224 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 17 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 181 ( 0 sgn 181 !; 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/sandbox/benchmark/theBenchmark.p',cls_keymode_Oinduct_0) ).
fof(f59,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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(f870,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(f1074,definition,
( spl25_38
<=> ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl25_38])],[avatar_definition]) ).
fof(f1075,plain,
( ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1)
| ~ spl25_38 ),
inference(avatar_component_clause,[],[f1074]) ).
fof(f1094,definition,
( spl25_43
<=> ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption ),
introduced(definition,[new_symbols(definition,[spl25_43])],[avatar_definition]) ).
fof(f1095,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption
| ~ spl25_43 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1097,definition,
( spl25_44
<=> ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1)) ),
introduced(definition,[new_symbols(definition,[spl25_44])],[avatar_definition]) ).
fof(f1098,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1))
| ~ spl25_44 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1099,plain,
( spl25_43
| spl25_44 ),
inference(avatar_split_clause,[],[f870,f1097,f1094]) ).
fof(f1173,definition,
( spl25_61
<=> ! [X0] : ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) ),
introduced(definition,[new_symbols(definition,[spl25_61])],[avatar_definition]) ).
fof(f1174,plain,
( ! [X0] : ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| ~ spl25_61 ),
inference(avatar_component_clause,[],[f1173]) ).
fof(f1208,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OSignature = X3
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X1,X2) ),
inference(superposition,[],[f832,f846]) ).
fof(f1260,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(f1322,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(f1328,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(f1465,definition,
( spl25_64
<=> ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2)) ),
introduced(definition,[new_symbols(definition,[spl25_64])],[avatar_definition]) ).
fof(f1466,plain,
( ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| ~ spl25_64 ),
inference(avatar_component_clause,[],[f1465]) ).
fof(f1477,definition,
( spl25_67
<=> ! [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_67])],[avatar_definition]) ).
fof(f1478,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_67 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1497,definition,
( spl25_71
<=> hBOOL(c_Public_Okeymode_OEncryption) ),
introduced(definition,[new_symbols(definition,[spl25_71])],[avatar_definition]) ).
fof(f1498,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| spl25_71 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1499,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_71 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1569,plain,
( spl25_67
| spl25_64 ),
inference(avatar_split_clause,[],[f1328,f1465,f1477]) ).
fof(f1572,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_43 ),
inference(forward_demodulation,[],[f1322,f1095]) ).
fof(f1573,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) )
| ~ spl25_43 ),
inference(duplicate_literal_removal,[],[f1572]) ).
fof(f1609,definition,
( spl25_82
<=> ! [X0,X3] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OSignature = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_82])],[avatar_definition]) ).
fof(f1610,plain,
( ! [X3,X0] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OSignature = X3 )
| ~ spl25_82 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1637,plain,
( spl25_38
| spl25_82 ),
inference(avatar_split_clause,[],[f1208,f1609,f1074]) ).
fof(f1670,definition,
( spl25_85
<=> ! [X1] : c_Public_Okeymode_OEncryption = X1 ),
introduced(definition,[new_symbols(definition,[spl25_85])],[avatar_definition]) ).
fof(f1671,plain,
( ! [X1] : c_Public_Okeymode_OEncryption = X1
| ~ spl25_85 ),
inference(avatar_component_clause,[],[f1670]) ).
fof(f1685,definition,
( spl25_86
<=> ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) ),
introduced(definition,[new_symbols(definition,[spl25_86])],[avatar_definition]) ).
fof(f1686,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| ~ spl25_86 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1725,plain,
( spl25_86
| spl25_85
| ~ spl25_43 ),
inference(avatar_split_clause,[],[f1573,f1094,f1670,f1685]) ).
fof(f1912,definition,
( spl25_104
<=> ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 ) ),
introduced(definition,[new_symbols(definition,[spl25_104])],[avatar_definition]) ).
fof(f1913,plain,
( ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_104 ),
inference(avatar_component_clause,[],[f1912]) ).
fof(f1914,plain,
( spl25_43
| spl25_104 ),
inference(avatar_split_clause,[],[f1260,f1912,f1094]) ).
fof(f2175,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_85 ),
inference(superposition,[],[f59,f1671]) ).
fof(f2179,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl25_85 ),
inference(superposition,[],[f534,f1671]) ).
fof(f2187,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| ~ spl25_85 ),
inference(superposition,[],[f59,f1671]) ).
fof(f2244,plain,
( $false
| ~ spl25_64
| ~ spl25_85 ),
inference(forward_subsumption_resolution,[],[f2187,f1466]) ).
fof(f2245,plain,
( ~ spl25_64
| ~ spl25_85 ),
inference(avatar_contradiction_clause,[],[f2244]) ).
fof(f2250,plain,
( $false
| spl25_71
| ~ spl25_85 ),
inference(forward_subsumption_resolution,[],[f2179,f1498]) ).
fof(f2251,plain,
( spl25_71
| ~ spl25_85 ),
inference(avatar_contradiction_clause,[],[f2250]) ).
fof(f2256,plain,
( $false
| ~ spl25_64
| ~ spl25_86 ),
inference(forward_subsumption_resolution,[],[f1686,f1466]) ).
fof(f2257,plain,
( ~ spl25_64
| ~ spl25_86 ),
inference(avatar_contradiction_clause,[],[f2256]) ).
fof(f2582,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(f2612,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,[],[f2582,f846]) ).
fof(f2616,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,[],[f2582,f840]) ).
fof(f2625,plain,
( ! [X2,X0,X1] :
( c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) )
| ~ spl25_44 ),
inference(forward_subsumption_resolution,[],[f2616,f1098]) ).
fof(f2627,definition,
( spl25_153
<=> ! [X2,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X1,X2) ),
introduced(definition,[new_symbols(definition,[spl25_153])],[avatar_definition]) ).
fof(f2628,plain,
( ! [X2,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X1,X2)
| ~ spl25_153 ),
inference(avatar_component_clause,[],[f2627]) ).
fof(f2635,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_86 ),
inference(forward_subsumption_resolution,[],[f2612,f1686]) ).
fof(f2638,plain,
( spl25_153
| spl25_85
| ~ spl25_44 ),
inference(avatar_split_clause,[],[f2625,f1097,f1670,f2627]) ).
fof(f2640,definition,
( spl25_155
<=> ! [X0,X1,X3] :
( c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_155])],[avatar_definition]) ).
fof(f2641,plain,
( ! [X3,X0,X1] :
( c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_155 ),
inference(avatar_component_clause,[],[f2640]) ).
fof(f2643,plain,
( spl25_155
| spl25_85
| ~ spl25_86 ),
inference(avatar_split_clause,[],[f2635,f1685,f1670,f2640]) ).
fof(f2652,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_153 ),
inference(forward_demodulation,[],[f2612,f2628]) ).
fof(f2653,plain,
( ! [X2,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_153 ),
inference(duplicate_literal_removal,[],[f2652]) ).
fof(f2659,definition,
( spl25_157
<=> ! [X2] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 ) ),
introduced(definition,[new_symbols(definition,[spl25_157])],[avatar_definition]) ).
fof(f2660,plain,
( ! [X2] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_157 ),
inference(avatar_component_clause,[],[f2659]) ).
fof(f2662,plain,
( spl25_157
| spl25_85
| ~ spl25_153 ),
inference(avatar_split_clause,[],[f2653,f2627,f1670,f2659]) ).
fof(f2669,plain,
( $false
| ~ spl25_71
| ~ spl25_85 ),
inference(forward_subsumption_resolution,[],[f2175,f1499]) ).
fof(f2670,plain,
( ~ spl25_71
| ~ spl25_85 ),
inference(avatar_contradiction_clause,[],[f2669]) ).
fof(f2691,plain,
( ! [X2] : c_Public_Okeymode_OEncryption = X2
| ~ spl25_86
| ~ spl25_157 ),
inference(forward_subsumption_resolution,[],[f2660,f1686]) ).
fof(f2694,plain,
( spl25_85
| ~ spl25_86
| ~ spl25_157 ),
inference(avatar_split_clause,[],[f2691,f2659,f1685,f1670]) ).
fof(f2746,plain,
( ! [X0] :
( hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_155 ),
inference(superposition,[],[f534,f2641]) ).
fof(f2810,plain,
( ! [X0] : c_Public_Okeymode_OEncryption = X0
| ~ spl25_61
| ~ spl25_155 ),
inference(forward_subsumption_resolution,[],[f2746,f1174]) ).
fof(f2820,plain,
( spl25_85
| ~ spl25_61
| ~ spl25_155 ),
inference(avatar_split_clause,[],[f2810,f2640,f1173,f1670]) ).
fof(f2836,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(X0,X1))
| X0 = X1
| X0 = X2
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl25_157 ),
inference(superposition,[],[f2660,f846]) ).
fof(f2847,plain,
( ! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Public_Okeymode_OEncryption
| ~ spl25_104 ),
inference(resolution,[],[f1913,f534]) ).
fof(f2868,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_157 ),
inference(resolution,[],[f2836,f513]) ).
fof(f2877,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_104
| ~ spl25_157 ),
inference(forward_demodulation,[],[f2868,f2847]) ).
fof(f2880,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_104
| ~ spl25_157 ),
inference(forward_demodulation,[],[f2877,f2847]) ).
fof(f2881,plain,
( ! [X3,X0,X1,X4] :
( c_Public_Okeymode_OEncryption = X4
| c_Public_Okeymode_OEncryption = X3
| X0 = X3
| hBOOL(hAPP(X1,X3)) )
| ~ spl25_104
| ~ spl25_157 ),
inference(duplicate_literal_removal,[],[f2880]) ).
fof(f2885,definition,
( spl25_167
<=> ! [X0,X1,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(X1,X3))
| X0 = X3 ) ),
introduced(definition,[new_symbols(definition,[spl25_167])],[avatar_definition]) ).
fof(f2886,plain,
( ! [X3,X0,X1] :
( hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OEncryption = X3
| X0 = X3 )
| ~ spl25_167 ),
inference(avatar_component_clause,[],[f2885]) ).
fof(f2887,plain,
( spl25_167
| spl25_85
| ~ spl25_104
| ~ spl25_157 ),
inference(avatar_split_clause,[],[f2881,f2659,f1912,f1670,f2885]) ).
fof(f2900,plain,
( ! [X3,X0] :
( c_Public_Okeymode_OEncryption = X3
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl25_38
| ~ spl25_67 ),
inference(forward_demodulation,[],[f1478,f1075]) ).
fof(f2901,plain,
( ! [X3,X0] :
( c_Public_Okeymode_OEncryption = X3
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature)) )
| ~ spl25_38
| ~ spl25_67 ),
inference(duplicate_literal_removal,[],[f2900]) ).
fof(f2907,plain,
( spl25_61
| spl25_85
| ~ spl25_38
| ~ spl25_67 ),
inference(avatar_split_clause,[],[f2901,f1477,f1074,f1670,f1173]) ).
fof(f2979,plain,
( ! [X3,X0,X1] :
( ~ hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OSignature = X3
| hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_155 ),
inference(superposition,[],[f513,f2641]) ).
fof(f3042,definition,
( spl25_171
<=> ! [X1,X3] :
( c_Public_Okeymode_OSignature = X3
| hBOOL(hAPP(X1,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl25_171])],[avatar_definition]) ).
fof(f3043,plain,
( ! [X3,X1] :
( hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OSignature = X3 )
| ~ spl25_171 ),
inference(avatar_component_clause,[],[f3042]) ).
fof(f3046,plain,
( ! [X0] : c_Public_Okeymode_OSignature = X0
| ~ spl25_171 ),
inference(resolution,[],[f3043,f59]) ).
fof(f3106,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OSignature,X1))
| ~ spl25_171 ),
inference(superposition,[],[f59,f3046]) ).
fof(f3147,plain,
( spl25_44
| ~ spl25_171 ),
inference(avatar_split_clause,[],[f3106,f3042,f1097]) ).
fof(f3163,plain,
( ! [X3,X0,X1] :
( c_Public_Okeymode_OSignature = X3
| hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_82
| ~ spl25_155 ),
inference(forward_subsumption_resolution,[],[f2979,f1610]) ).
fof(f3166,plain,
( spl25_85
| spl25_171
| ~ spl25_82
| ~ spl25_155 ),
inference(avatar_split_clause,[],[f3163,f2640,f1609,f3042,f1670]) ).
fof(f3169,plain,
( ! [X0,X1] :
( c_Public_Okeymode_OEncryption = X0
| X0 = X1 )
| ~ spl25_167 ),
inference(resolution,[],[f2886,f59]) ).
fof(f3431,plain,
( ! [X0] :
( X0 != X0
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl25_167 ),
inference(equality_factoring,[],[f3169]) ).
fof(f3432,plain,
( ! [X0] : c_Public_Okeymode_OEncryption = X0
| ~ spl25_167 ),
inference(trivial_inequality_removal,[],[f3431]) ).
fof(f3435,plain,
( spl25_85
| ~ spl25_167 ),
inference(avatar_split_clause,[],[f3432,f2885,f1670]) ).
cnf(s26,plain,
( spl25_43
| spl25_44 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s57,plain,
( spl25_64
| spl25_67 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s81,plain,
( spl25_38
| spl25_82 ),
inference(sat_conversion,[],[f1637]) ).
cnf(s93,plain,
( ~ spl25_43
| spl25_85
| spl25_86 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s152,plain,
( spl25_43
| spl25_104 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s206,plain,
( ~ spl25_64
| ~ spl25_85 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s208,plain,
( spl25_71
| ~ spl25_85 ),
inference(sat_conversion,[],[f2251]) ).
cnf(s209,plain,
( ~ spl25_64
| ~ spl25_86 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s287,plain,
( ~ spl25_44
| spl25_85
| spl25_153 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s289,plain,
( spl25_85
| ~ spl25_86
| spl25_155 ),
inference(sat_conversion,[],[f2643]) ).
cnf(s292,plain,
( spl25_85
| ~ spl25_153
| spl25_157 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s296,plain,
( ~ spl25_71
| ~ spl25_85 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s304,plain,
( spl25_85
| ~ spl25_86
| ~ spl25_157 ),
inference(sat_conversion,[],[f2694]) ).
cnf(s312,plain,
( ~ spl25_61
| spl25_85
| ~ spl25_155 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s320,plain,
( spl25_85
| ~ spl25_104
| ~ spl25_157
| spl25_167 ),
inference(sat_conversion,[],[f2887]) ).
cnf(s326,plain,
( ~ spl25_38
| spl25_61
| ~ spl25_67
| spl25_85 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s337,plain,
( spl25_44
| ~ spl25_171 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s343,plain,
( ~ spl25_82
| spl25_85
| ~ spl25_155
| spl25_171 ),
inference(sat_conversion,[],[f3166]) ).
cnf(s350,plain,
( spl25_85
| ~ spl25_167 ),
inference(sat_conversion,[],[f3435]) ).
cnf(s367,plain,
( ~ spl25_64
| ~ spl25_43 ),
inference(rat,[],[s93,s206,s209]) ).
cnf(s368,plain,
( spl25_85
| ~ spl25_82
| spl25_44 ),
inference(rat,[],[s93,s289,s343,s337,s26]) ).
cnf(s369,plain,
~ spl25_85,
inference(rat,[],[s208,s296]) ).
cnf(s370,plain,
~ spl25_167,
inference(rat,[],[s350,s369]) ).
cnf(s373,plain,
spl25_44,
inference(rat,[],[s312,s326,s289,s57,s81,s93,s367,s368,s26,s369]) ).
cnf(s374,plain,
spl25_153,
inference(rat,[],[s287,s369,s373]) ).
cnf(s376,plain,
spl25_157,
inference(rat,[],[s292,s369,s374]) ).
cnf(s379,plain,
~ spl25_86,
inference(rat,[],[s304,s369,s376]) ).
cnf(s380,plain,
~ spl25_104,
inference(rat,[],[s320,s370,s369,s376]) ).
cnf(s382,plain,
~ spl25_43,
inference(rat,[],[s93,s369,s379]) ).
cnf(s383,plain,
$false,
inference(rat,[],[s152,s380,s382]) ).
fof(f3561,plain,
$false,
inference(avatar_sat_refutation,[],[s383]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV743-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n007.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 12:23:10 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running first-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.29/1.79 % (2358069)Input is clausal, will run a generic CNF schedule.
% 7.29/1.79 % (2358080)dis-21_1_sil=8000:lcm=predicate:random_seed=3408739070: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.29/1.79 % (2358075)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1859216735:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.29/1.79 % (2358077)lrs+10_1_sil=8000:sp=occurrence:random_seed=4221210101:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.29/1.79 % (2358078)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1462566032:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.29/1.79 % (2358074)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=1515163171:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.29/1.79 % (2358079)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4163576821:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.29/1.79 % (2358076)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3725852937:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.29/1.79 % (2358080)Instruction limit reached!
% 7.29/1.79 % (2358080)------------------------------
% 7.29/1.79 % (2358080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358080)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358080)Termination reason: Instruction limit
% 7.29/1.79 % (2358080)Termination phase: Saturation
% 7.29/1.79 % (2358080)Time elapsed: 0.038 s
% 7.29/1.79 % (2358080)Peak memory usage: 89 MB
% 7.29/1.79 % (2358080)Instructions burned: 117 (million)
% 7.29/1.79 % (2358077)Instruction limit reached!
% 7.29/1.79 % (2358077)------------------------------
% 7.29/1.79 % (2358077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358077)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358077)Termination reason: Instruction limit
% 7.29/1.79 % (2358077)Termination phase: Saturation
% 7.29/1.79 % (2358077)Time elapsed: 0.073 s
% 7.29/1.79 % (2358077)Peak memory usage: 89 MB
% 7.29/1.79 % (2358077)Instructions burned: 107 (million)
% 7.29/1.79 % (2358078)Instruction limit reached!
% 7.29/1.79 % (2358078)------------------------------
% 7.29/1.79 % (2358078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358078)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358078)Termination reason: Instruction limit
% 7.29/1.79 % (2358078)Termination phase: Saturation
% 7.29/1.79 % (2358078)Time elapsed: 0.076 s
% 7.29/1.79 % (2358078)Peak memory usage: 89 MB
% 7.29/1.79 % (2358078)Instructions burned: 115 (million)
% 7.29/1.79 % (2358079)Instruction limit reached!
% 7.29/1.79 % (2358079)------------------------------
% 7.29/1.79 % (2358079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358079)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358079)Termination reason: Instruction limit
% 7.29/1.79 % (2358079)Termination phase: Saturation
% 7.29/1.79 % (2358079)Time elapsed: 0.114 s
% 7.29/1.79 % (2358079)Peak memory usage: 90 MB
% 7.29/1.79 % (2358079)Instructions burned: 180 (million)
% 7.29/1.79 % (2358088)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=3602514341:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.29/1.79 % (2358088)Refutation not found, incomplete strategy
% 7.29/1.79 % (2358088)------------------------------
% 7.29/1.79 % (2358088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358088)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358088)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.79 % (2358088)Time elapsed: 0.018 s
% 7.29/1.79 % (2358088)Peak memory usage: 89 MB
% 7.29/1.79 % (2358088)Instructions burned: 51 (million)
% 7.29/1.79 % (2358090)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1795683743:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.29/1.79 % (2358089)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3136468581: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.29/1.79 % (2358090)Refutation not found, incomplete strategy
% 7.29/1.79 % (2358090)------------------------------
% 7.29/1.79 % (2358090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358090)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358090)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.79 % (2358090)Time elapsed: 0.036 s
% 7.29/1.79 % (2358090)Peak memory usage: 89 MB
% 7.29/1.79 % (2358090)Instructions burned: 59 (million)
% 7.29/1.79 % (2358091)lrs+10_64_to=lpo:sil=8000:random_seed=2270083786:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.29/1.79 % (2358088)------------------------------
% 7.29/1.79 % (2358088)------------------------------
% 7.29/1.79 % (2358089)Instruction limit reached!
% 7.29/1.79 % (2358089)------------------------------
% 7.29/1.79 % (2358089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358089)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358089)Termination reason: Instruction limit
% 7.29/1.79 % (2358089)Termination phase: Saturation
% 7.29/1.79 % (2358089)Time elapsed: 0.106 s
% 7.29/1.79 % (2358089)Peak memory usage: 90 MB
% 7.29/1.79 % (2358089)Instructions burned: 189 (million)
% 7.29/1.79 % (2358091)Instruction limit reached!
% 7.29/1.79 % (2358091)------------------------------
% 7.29/1.79 % (2358091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358091)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358091)Termination reason: Instruction limit
% 7.29/1.79 % (2358091)Termination phase: Saturation
% 7.29/1.79 % (2358091)Time elapsed: 0.077 s
% 7.29/1.79 % (2358091)Peak memory usage: 90 MB
% 7.29/1.79 % (2358091)Instructions burned: 127 (million)
% 7.29/1.79 % (2358096)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1906759185:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 7.29/1.79 % (2358097)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2469974497:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 7.29/1.79 % (2358096)Instruction limit reached!
% 7.29/1.79 % (2358096)------------------------------
% 7.29/1.79 % (2358096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358096)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358096)Termination reason: Instruction limit
% 7.29/1.79 % (2358096)Termination phase: Saturation
% 7.29/1.79 % (2358096)Time elapsed: 0.065 s
% 7.29/1.79 % (2358096)Peak memory usage: 90 MB
% 7.29/1.79 % (2358096)Instructions burned: 197 (million)
% 7.29/1.79 % (2358090)------------------------------
% 7.29/1.79 % (2358090)------------------------------
% 7.29/1.79 % (2358098)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2779737928:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 7.29/1.79 % (2358097)Instruction limit reached!
% 7.29/1.79 % (2358097)------------------------------
% 7.29/1.79 % (2358097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358097)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358097)Termination reason: Instruction limit
% 7.29/1.79 % (2358097)Termination phase: Saturation
% 7.29/1.79 % (2358097)Time elapsed: 0.106 s
% 7.29/1.79 % (2358097)Peak memory usage: 91 MB
% 7.29/1.79 % (2358097)Instructions burned: 157 (million)
% 7.29/1.79 % (2358101)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=2761271987:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 7.29/1.79 % (2358101)Instruction limit reached!
% 7.29/1.79 % (2358101)------------------------------
% 7.29/1.79 % (2358101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358101)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358101)Termination reason: Instruction limit
% 7.29/1.79 % (2358101)Termination phase: Saturation
% 7.29/1.79 % (2358101)Time elapsed: 0.032 s
% 7.29/1.79 % (2358101)Peak memory usage: 89 MB
% 7.29/1.79 % (2358101)Instructions burned: 106 (million)
% 7.29/1.79 % (2358102)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=536316385:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 7.29/1.79 % (2358102)Instruction limit reached!
% 7.29/1.79 % (2358102)------------------------------
% 7.29/1.79 % (2358102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358102)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358102)Termination reason: Instruction limit
% 7.29/1.79 % (2358102)Termination phase: Saturation
% 7.29/1.79 % (2358102)Time elapsed: 0.069 s
% 7.29/1.79 % (2358102)Peak memory usage: 90 MB
% 7.29/1.79 % (2358102)Instructions burned: 107 (million)
% 7.29/1.79 % (2358104)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2913458438:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 7.29/1.79 % (2358106)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2620081433:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 7.29/1.79 % (2358074)First to succeed.
% 7.29/1.79 % (2358074)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2358069"
% 7.29/1.79 % (2358104)Instruction limit reached!
% 7.29/1.79 % (2358104)------------------------------
% 7.29/1.79 % (2358104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358104)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358104)Termination reason: Instruction limit
% 7.29/1.79 % (2358104)Termination phase: Saturation
% 7.29/1.79 % (2358104)Time elapsed: 0.152 s
% 7.29/1.79 % (2358104)Peak memory usage: 90 MB
% 7.29/1.79 % (2358104)Instructions burned: 242 (million)
% 7.29/1.79 % (2358108)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1019945319:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 7.29/1.79 % (2358108)Instruction limit reached!
% 7.29/1.79 % (2358108)------------------------------
% 7.29/1.79 % (2358108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.79 % (2358108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.79 % (2358108)CaDiCaL version: 2.1.3
% 7.29/1.79 % (2358108)Termination reason: Instruction limit
% 7.29/1.79 % (2358108)Termination phase: Saturation
% 7.29/1.79 % (2358108)Time elapsed: 0.092 s
% 7.29/1.79 % (2358108)Peak memory usage: 90 MB
% 7.29/1.79 % (2358108)Instructions burned: 134 (million)
% 7.29/1.79 % (2358111)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1731529150:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 7.29/1.79 % (2358074)Refutation found. Thanks to Tanya!
% 7.29/1.79 % SZS status Unsatisfiable for theBenchmark
% 7.29/1.79 % SZS output start Proof for theBenchmark
% See solution above
% 9.41/1.98 % (2358074)------------------------------
% 9.41/1.98 % (2358074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.41/1.98 % (2358074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.41/1.98 % (2358074)CaDiCaL version: 2.1.3
% 9.41/1.98 % (2358074)Termination reason: Refutation
% 9.41/1.98 % (2358074)Time elapsed: 0.846 s
% 9.41/1.98 % (2358074)Peak memory usage: 133 MB
% 9.41/1.98 % (2358074)Instructions burned: 1352 (million)
% 9.41/1.98 % (2358074)------------------------------
% 9.41/1.98 % (2358074)------------------------------
% 9.41/1.98 % (2358069)Success in time 1.274 s
% 9.41/1.98 % Vampire exiting
%------------------------------------------------------------------------------