%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV759-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 : n006.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:26 PM UTC 2026
% Result : Unsatisfiable 10.75s 2.19s
% Output : Refutation 11.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 22
% Syntax : Number of formulae : 159 ( 20 unt; 16 def)
% Number of atoms : 455 ( 147 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 471 ( 175 ~; 280 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 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 : 233 ( 0 sgn 233 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f54,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(f87,axiom,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_keymode_Oinduct_0) ).
fof(f88,axiom,
c_Public_Okeymode_OSignature != c_Public_Okeymode_OEncryption,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_keymode_Osimps_I1_J_0) ).
fof(f89,plain,
c_Public_Okeymode_OEncryption != c_Public_Okeymode_OSignature,
inference(reorient_equations,[],[f88]) ).
fof(f454,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(f457,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(f458,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(X2,X0,X3),X1))
| X1 = X2
| hBOOL(hAPP(X0,X1)) ),
inference(reorient_equations,[],[f457]) ).
fof(f462,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(f853,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(X1,X0,X2),c_Public_Okeymode_OEncryption))
| ~ hBOOL(hAPP(X0,c_Public_Okeymode_OSignature))
| hBOOL(hAPP(c_Set_Oinsert(X1,X0,X2),X3)) ),
inference(resolution,[],[f462,f87]) ).
fof(f859,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,[],[f454,f853]) ).
fof(f860,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2)) ),
inference(resolution,[],[f454,f87]) ).
fof(f862,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,[],[f860,f462]) ).
fof(f873,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X1,c_Public_Okeymode_OEncryption))
| hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[],[f458,f862]) ).
fof(f874,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X1,c_Public_Okeymode_OSignature))
| hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OEncryption = X0 ),
inference(resolution,[],[f458,f859]) ).
fof(f877,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X2))
| c_Public_Okeymode_OEncryption = X2 ),
inference(resolution,[],[f874,f454]) ).
fof(f882,plain,
! [X0,X1] :
( hBOOL(hAPP(X1,X0))
| c_Public_Okeymode_OSignature = X0
| c_Public_Okeymode_OEncryption = X0 ),
inference(resolution,[],[f877,f458]) ).
fof(f885,plain,
! [X0] :
( c_Public_Okeymode_OSignature = X0
| c_Public_Okeymode_OEncryption = X0 ),
inference(resolution,[],[f882,f54]) ).
fof(f891,plain,
! [X0,X1] :
( X0 = X1
| c_Public_Okeymode_OEncryption = X1
| c_Public_Okeymode_OEncryption = X0 ),
inference(superposition,[],[f885,f885]) ).
fof(f918,plain,
! [X0,X1] :
( ~ hBOOL(c_Public_Okeymode_OSignature)
| hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Public_Okeymode_OEncryption ),
inference(superposition,[],[f54,f885]) ).
fof(f1140,definition,
( spl21_40
<=> hBOOL(c_Public_Okeymode_OSignature) ),
introduced(definition,[new_symbols(definition,[spl21_40])],[avatar_definition]) ).
fof(f1141,plain,
( ~ hBOOL(c_Public_Okeymode_OSignature)
| spl21_40 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1142,plain,
( hBOOL(c_Public_Okeymode_OSignature)
| ~ spl21_40 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1185,definition,
( spl21_51
<=> ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Public_Okeymode_OEncryption ),
introduced(definition,[new_symbols(definition,[spl21_51])],[avatar_definition]) ).
fof(f1186,plain,
( ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Public_Okeymode_OEncryption
| ~ spl21_51 ),
inference(avatar_component_clause,[],[f1185]) ).
fof(f1187,plain,
( spl21_51
| ~ spl21_40 ),
inference(avatar_split_clause,[],[f918,f1140,f1185]) ).
fof(f1219,definition,
( spl21_58
<=> ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) ),
introduced(definition,[new_symbols(definition,[spl21_58])],[avatar_definition]) ).
fof(f1220,plain,
( ! [X0,X1] : c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1)
| ~ spl21_58 ),
inference(avatar_component_clause,[],[f1219]) ).
fof(f1243,definition,
( spl21_64
<=> ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption ),
introduced(definition,[new_symbols(definition,[spl21_64])],[avatar_definition]) ).
fof(f1244,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Public_Okeymode_OEncryption
| ~ spl21_64 ),
inference(avatar_component_clause,[],[f1243]) ).
fof(f1277,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Public_Okeymode_OEncryption ),
inference(superposition,[],[f54,f891]) ).
fof(f1283,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OEncryption = X3
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X1,X2) ),
inference(superposition,[],[f877,f891]) ).
fof(f1414,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,[],[f54,f891]) ).
fof(f1420,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,[],[f877,f891]) ).
fof(f1502,plain,
! [X2,X0,X1] :
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = X2
| c_Public_Okeymode_OEncryption = X2 ),
inference(superposition,[],[f54,f891]) ).
fof(f1590,definition,
( spl21_72
<=> hBOOL(c_Public_Okeymode_OEncryption) ),
introduced(definition,[new_symbols(definition,[spl21_72])],[avatar_definition]) ).
fof(f1591,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| spl21_72 ),
inference(avatar_component_clause,[],[f1590]) ).
fof(f1592,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl21_72 ),
inference(avatar_component_clause,[],[f1590]) ).
fof(f1636,definition,
( spl21_80
<=> ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2)) ),
introduced(definition,[new_symbols(definition,[spl21_80])],[avatar_definition]) ).
fof(f1637,plain,
( ! [X2] : hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| ~ spl21_80 ),
inference(avatar_component_clause,[],[f1636]) ).
fof(f1716,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl21_64 ),
inference(forward_demodulation,[],[f1414,f1244]) ).
fof(f1717,plain,
( ! [X2,X1] :
( c_Public_Okeymode_OEncryption = X2
| ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) )
| ~ spl21_64 ),
inference(duplicate_literal_removal,[],[f1716]) ).
fof(f1824,definition,
( spl21_90
<=> ! [X3] : c_Public_Okeymode_OEncryption = X3 ),
introduced(definition,[new_symbols(definition,[spl21_90])],[avatar_definition]) ).
fof(f1825,plain,
( ! [X3] : c_Public_Okeymode_OEncryption = X3
| ~ spl21_90 ),
inference(avatar_component_clause,[],[f1824]) ).
fof(f1840,definition,
( spl21_92
<=> ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1)) ),
introduced(definition,[new_symbols(definition,[spl21_92])],[avatar_definition]) ).
fof(f1841,plain,
( ! [X1] : ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X1))
| ~ spl21_92 ),
inference(avatar_component_clause,[],[f1840]) ).
fof(f1889,plain,
( spl21_92
| spl21_90
| ~ spl21_64 ),
inference(avatar_split_clause,[],[f1717,f1243,f1824,f1840]) ).
fof(f2148,definition,
( spl21_114
<=> ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 ) ),
introduced(definition,[new_symbols(definition,[spl21_114])],[avatar_definition]) ).
fof(f2149,plain,
( ! [X2,X0] :
( ~ hBOOL(hAPP(X0,X2))
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl21_114 ),
inference(avatar_component_clause,[],[f2148]) ).
fof(f2151,plain,
( spl21_64
| spl21_114 ),
inference(avatar_split_clause,[],[f1277,f2148,f1243]) ).
fof(f2159,definition,
( spl21_115
<=> ! [X0,X3] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = X3 ) ),
introduced(definition,[new_symbols(definition,[spl21_115])],[avatar_definition]) ).
fof(f2160,plain,
( ! [X3,X0] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_115 ),
inference(avatar_component_clause,[],[f2159]) ).
fof(f2164,plain,
( spl21_58
| spl21_115 ),
inference(avatar_split_clause,[],[f1283,f2159,f1219]) ).
fof(f2476,plain,
( ~ hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl21_90 ),
inference(superposition,[],[f54,f1825]) ).
fof(f2484,plain,
( hBOOL(c_Public_Okeymode_OEncryption)
| ~ spl21_90 ),
inference(superposition,[],[f454,f1825]) ).
fof(f2543,plain,
( $false
| ~ spl21_72
| ~ spl21_90 ),
inference(forward_subsumption_resolution,[],[f2476,f1592]) ).
fof(f2544,plain,
( ~ spl21_72
| ~ spl21_90 ),
inference(avatar_contradiction_clause,[],[f2543]) ).
fof(f2564,plain,
( ! [X2,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = X2
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl21_72 ),
inference(forward_subsumption_resolution,[],[f1502,f1592]) ).
fof(f2681,plain,
( ! [X2] :
( c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl21_51
| ~ spl21_72 ),
inference(forward_demodulation,[],[f2564,f1186]) ).
fof(f2682,plain,
( ! [X2] : c_Public_Okeymode_OEncryption = X2
| ~ spl21_51
| ~ spl21_72 ),
inference(duplicate_literal_removal,[],[f2681]) ).
fof(f2772,plain,
( spl21_90
| ~ spl21_51
| ~ spl21_72 ),
inference(avatar_split_clause,[],[f2682,f1590,f1185,f1824]) ).
fof(f2807,plain,
( $false
| spl21_72
| ~ spl21_90 ),
inference(forward_subsumption_resolution,[],[f2484,f1591]) ).
fof(f2808,plain,
( spl21_72
| ~ spl21_90 ),
inference(avatar_contradiction_clause,[],[f2807]) ).
fof(f2814,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 )
| ~ spl21_92 ),
inference(forward_subsumption_resolution,[],[f1420,f1841]) ).
fof(f2902,plain,
( ! [X2,X3] :
( c_Public_Okeymode_OEncryption = X3
| c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_58
| ~ spl21_92 ),
inference(forward_demodulation,[],[f2814,f1220]) ).
fof(f2903,plain,
( ! [X2,X3] :
( c_Public_Okeymode_OEncryption = X3
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl21_58
| ~ spl21_92 ),
inference(duplicate_literal_removal,[],[f2902]) ).
fof(f2947,plain,
( spl21_90
| spl21_90
| ~ spl21_58
| ~ spl21_92 ),
inference(avatar_split_clause,[],[f2903,f1840,f1219,f1824,f1824]) ).
fof(f3034,plain,
( ! [X3,X0] :
( c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_114
| ~ spl21_115 ),
inference(forward_subsumption_resolution,[],[f2160,f2149]) ).
fof(f3037,plain,
( spl21_90
| spl21_90
| ~ spl21_114
| ~ spl21_115 ),
inference(avatar_split_clause,[],[f3034,f2159,f2148,f1824,f1824]) ).
fof(f3256,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X2))
| c_Public_Okeymode_OSignature = X2 ),
inference(resolution,[],[f873,f454]) ).
fof(f3279,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X3))
| c_Public_Okeymode_OSignature = X3
| X0 = X4
| c_Public_Okeymode_OEncryption = X4 ),
inference(superposition,[],[f3256,f891]) ).
fof(f3280,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X2))
| c_Public_Okeymode_OSignature = X2
| c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ),
inference(superposition,[],[f3256,f891]) ).
fof(f3305,plain,
( ! [X2,X3,X0,X1] :
( c_Public_Okeymode_OSignature = X2
| c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_92 ),
inference(forward_subsumption_resolution,[],[f3280,f1841]) ).
fof(f3307,definition,
( spl21_185
<=> ! [X0,X1,X3] :
( c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 ) ),
introduced(definition,[new_symbols(definition,[spl21_185])],[avatar_definition]) ).
fof(f3308,plain,
( ! [X3,X0,X1] :
( c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1) = X3
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_185 ),
inference(avatar_component_clause,[],[f3307]) ).
fof(f3310,definition,
( spl21_186
<=> ! [X2] : c_Public_Okeymode_OSignature = X2 ),
introduced(definition,[new_symbols(definition,[spl21_186])],[avatar_definition]) ).
fof(f3311,plain,
( ! [X2] : c_Public_Okeymode_OSignature = X2
| ~ spl21_186 ),
inference(avatar_component_clause,[],[f3310]) ).
fof(f3313,plain,
( spl21_185
| spl21_186
| ~ spl21_92 ),
inference(avatar_split_clause,[],[f3305,f1840,f3310,f3307]) ).
fof(f3442,plain,
( ! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X4))
| c_Public_Okeymode_OEncryption = X4
| c_Public_Okeymode_OEncryption = c_Set_Oinsert(c_Public_Okeymode_OSignature,X2,X3) )
| ~ spl21_185 ),
inference(superposition,[],[f877,f3308]) ).
fof(f3515,definition,
( spl21_196
<=> ! [X4,X0,X1] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X4))
| c_Public_Okeymode_OEncryption = X4 ) ),
introduced(definition,[new_symbols(definition,[spl21_196])],[avatar_definition]) ).
fof(f3516,plain,
( ! [X0,X1,X4] :
( hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OEncryption,X0,X1),X4))
| c_Public_Okeymode_OEncryption = X4 )
| ~ spl21_196 ),
inference(avatar_component_clause,[],[f3515]) ).
fof(f3517,plain,
( spl21_58
| spl21_196
| ~ spl21_185 ),
inference(avatar_split_clause,[],[f3442,f3307,f3515,f1219]) ).
fof(f3527,definition,
( spl21_198
<=> ! [X1,X3] :
( c_Public_Okeymode_OEncryption = X3
| hBOOL(hAPP(X1,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl21_198])],[avatar_definition]) ).
fof(f3528,plain,
( ! [X3,X1] :
( hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OEncryption = X3 )
| ~ spl21_198 ),
inference(avatar_component_clause,[],[f3527]) ).
fof(f3573,plain,
( ~ hBOOL(c_Public_Okeymode_OSignature)
| ~ spl21_186 ),
inference(superposition,[],[f54,f3311]) ).
fof(f3578,plain,
( hBOOL(c_Public_Okeymode_OSignature)
| ~ spl21_186 ),
inference(superposition,[],[f454,f3311]) ).
fof(f3617,plain,
( $false
| ~ spl21_40
| ~ spl21_186 ),
inference(forward_subsumption_resolution,[],[f3573,f1142]) ).
fof(f3618,plain,
( ~ spl21_40
| ~ spl21_186 ),
inference(avatar_contradiction_clause,[],[f3617]) ).
fof(f3632,plain,
( $false
| spl21_40
| ~ spl21_186 ),
inference(forward_subsumption_resolution,[],[f3578,f1141]) ).
fof(f3633,plain,
( spl21_40
| ~ spl21_186 ),
inference(avatar_contradiction_clause,[],[f3632]) ).
fof(f3699,plain,
( ! [X0] : c_Public_Okeymode_OEncryption = X0
| ~ spl21_198 ),
inference(resolution,[],[f3528,f54]) ).
fof(f3713,plain,
( spl21_90
| ~ spl21_198 ),
inference(avatar_split_clause,[],[f3699,f3527,f1824]) ).
fof(f3864,plain,
( ! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Public_Okeymode_OEncryption
| ~ spl21_114 ),
inference(resolution,[],[f2149,f454]) ).
fof(f4035,plain,
( ! [X0,X1] :
( c_Public_Okeymode_OEncryption = X0
| c_Public_Okeymode_OEncryption = X0
| hBOOL(hAPP(X1,X0)) )
| ~ spl21_196 ),
inference(resolution,[],[f3516,f458]) ).
fof(f4052,plain,
( ! [X0,X1] :
( c_Public_Okeymode_OEncryption = X0
| hBOOL(hAPP(X1,X0)) )
| ~ spl21_196 ),
inference(duplicate_literal_removal,[],[f4035]) ).
fof(f4056,plain,
( spl21_198
| ~ spl21_196 ),
inference(avatar_split_clause,[],[f4052,f3515,f3527]) ).
fof(f4180,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(X3,X0))
| X1 = X2
| c_Public_Okeymode_OEncryption = X2
| X0 = X1
| c_Public_Okeymode_OSignature = X0 ),
inference(resolution,[],[f3279,f458]) ).
fof(f4213,plain,
! [X2,X0,X1] :
( X0 = X1
| c_Public_Okeymode_OEncryption = X1
| X0 = X2
| c_Public_Okeymode_OSignature = X2 ),
inference(resolution,[],[f4180,f54]) ).
fof(f4672,definition,
( spl21_231
<=> ! [X2,X0,X1] :
( X0 = X1
| c_Public_Okeymode_OSignature = X2
| X0 = X2
| c_Public_Okeymode_OEncryption = X1 ) ),
introduced(definition,[new_symbols(definition,[spl21_231])],[avatar_definition]) ).
fof(f4673,plain,
( ! [X2,X0,X1] :
( X0 = X1
| c_Public_Okeymode_OSignature = X2
| X0 = X2
| c_Public_Okeymode_OEncryption = X1 )
| ~ spl21_231 ),
inference(avatar_component_clause,[],[f4672]) ).
fof(f4682,plain,
spl21_231,
inference(avatar_split_clause,[],[f4213,f4672]) ).
fof(f5019,plain,
( ! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OSignature = X3
| X0 = X4
| c_Public_Okeymode_OSignature = c_Set_Oinsert(c_Public_Okeymode_OEncryption,X1,X2)
| c_Public_Okeymode_OEncryption = X4 )
| ~ spl21_231 ),
inference(superposition,[],[f3256,f4673]) ).
fof(f5096,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(c_Public_Okeymode_OEncryption,X3))
| X0 = X3
| hBOOL(hAPP(X1,X3))
| c_Set_Oinsert(X0,X1,X2) = X4
| c_Public_Okeymode_OSignature = X5
| X4 = X5 )
| ~ spl21_231 ),
inference(superposition,[],[f458,f4673]) ).
fof(f5169,plain,
( ! [X0,X1] :
( X0 != X1
| c_Public_Okeymode_OSignature = X1
| c_Public_Okeymode_OSignature = X1
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl21_231 ),
inference(equality_factoring,[],[f4673]) ).
fof(f5206,plain,
( ! [X0,X1] :
( X0 != X1
| c_Public_Okeymode_OSignature = X1
| c_Public_Okeymode_OEncryption = X0 )
| ~ spl21_231 ),
inference(duplicate_literal_removal,[],[f5169]) ).
fof(f5317,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( X0 = X3
| hBOOL(hAPP(X1,X3))
| c_Set_Oinsert(X0,X1,X2) = X4
| c_Public_Okeymode_OSignature = X5
| X4 = X5 )
| ~ spl21_80
| ~ spl21_231 ),
inference(forward_subsumption_resolution,[],[f5096,f1637]) ).
fof(f5514,plain,
( ! [X3,X0,X4] :
( c_Public_Okeymode_OEncryption = c_Public_Okeymode_OSignature
| hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OSignature = X3
| X0 = X4
| c_Public_Okeymode_OEncryption = X4 )
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_demodulation,[],[f5019,f3864]) ).
fof(f5710,plain,
( ! [X3,X0,X1,X4,X5] :
( c_Public_Okeymode_OEncryption = X4
| X0 = X3
| hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OSignature = X5
| X4 = X5 )
| ~ spl21_80
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_demodulation,[],[f5317,f3864]) ).
fof(f5765,plain,
( ! [X3,X0,X4] :
( hBOOL(hAPP(X0,X3))
| c_Public_Okeymode_OSignature = X3
| X0 = X4
| c_Public_Okeymode_OEncryption = X4 )
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_subsumption_resolution,[],[f5514,f89]) ).
fof(f5902,plain,
( ! [X3,X0,X1,X4,X5] :
( c_Public_Okeymode_OEncryption = X4
| X0 = X3
| hBOOL(hAPP(X1,X3))
| c_Public_Okeymode_OSignature = X5 )
| ~ spl21_80
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_subsumption_resolution,[],[f5710,f5206]) ).
fof(f5925,definition,
( spl21_335
<=> ! [X0,X1,X3] :
( X0 = X3
| hBOOL(hAPP(X1,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl21_335])],[avatar_definition]) ).
fof(f5926,plain,
( ! [X3,X0,X1] :
( hBOOL(hAPP(X1,X3))
| X0 = X3 )
| ~ spl21_335 ),
inference(avatar_component_clause,[],[f5925]) ).
fof(f5927,plain,
( spl21_186
| spl21_335
| spl21_90
| ~ spl21_80
| ~ spl21_114
| ~ spl21_231 ),
inference(avatar_split_clause,[],[f5902,f4672,f2148,f1636,f1824,f5925,f3310]) ).
fof(f6381,plain,
( ! [X0,X1] : X0 = X1
| ~ spl21_335 ),
inference(resolution,[],[f5926,f54]) ).
fof(f6767,plain,
( ! [X2,X3,X0,X1] :
( c_Public_Okeymode_OEncryption = c_Public_Okeymode_OSignature
| c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X2
| c_Public_Okeymode_OEncryption = X2
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X3)) )
| ~ spl21_114
| ~ spl21_231 ),
inference(resolution,[],[f5765,f860]) ).
fof(f6810,plain,
( ! [X2,X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,X0)),X2))
| ~ spl21_335 ),
inference(superposition,[],[f54,f6381]) ).
fof(f6942,plain,
( ! [X0] : hBOOL(X0)
| ~ spl21_335 ),
inference(superposition,[],[f454,f6381]) ).
fof(f7012,plain,
( $false
| ~ spl21_335 ),
inference(forward_subsumption_resolution,[],[f6810,f6942]) ).
fof(f7013,plain,
~ spl21_335,
inference(avatar_contradiction_clause,[],[f7012]) ).
fof(f7214,plain,
( ! [X2,X3,X0,X1] :
( c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1) = X2
| c_Public_Okeymode_OEncryption = X2
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X3)) )
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_subsumption_resolution,[],[f6767,f89]) ).
fof(f7404,plain,
( ! [X2,X3,X0,X1] :
( c_Public_Okeymode_OEncryption = X2
| c_Public_Okeymode_OEncryption = X2
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X3)) )
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_demodulation,[],[f7214,f3864]) ).
fof(f7405,plain,
( ! [X2,X3,X0,X1] :
( c_Public_Okeymode_OEncryption = X2
| hBOOL(hAPP(c_Set_Oinsert(c_Public_Okeymode_OSignature,X0,X1),X3)) )
| ~ spl21_114
| ~ spl21_231 ),
inference(duplicate_literal_removal,[],[f7404]) ).
fof(f7921,plain,
( ! [X2,X3] :
( hBOOL(hAPP(c_Public_Okeymode_OEncryption,X3))
| c_Public_Okeymode_OEncryption = X2 )
| ~ spl21_114
| ~ spl21_231 ),
inference(forward_demodulation,[],[f7405,f3864]) ).
fof(f7968,plain,
( spl21_90
| spl21_80
| ~ spl21_114
| ~ spl21_231 ),
inference(avatar_split_clause,[],[f7921,f4672,f2148,f1636,f1824]) ).
cnf(s32,plain,
( ~ spl21_40
| spl21_51 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s94,plain,
( ~ spl21_64
| spl21_90
| spl21_92 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s168,plain,
( spl21_64
| spl21_114 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s174,plain,
( spl21_58
| spl21_115 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s238,plain,
( ~ spl21_72
| ~ spl21_90 ),
inference(sat_conversion,[],[f2544]) ).
cnf(s280,plain,
( ~ spl21_51
| ~ spl21_72
| spl21_90 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s294,plain,
( spl21_72
| ~ spl21_90 ),
inference(sat_conversion,[],[f2808]) ).
cnf(s319,plain,
( spl21_90
| ~ spl21_58
| spl21_90
| ~ spl21_92 ),
inference(sat_conversion,[],[f2947]) ).
cnf(s320,plain,
( ~ spl21_58
| spl21_90
| ~ spl21_92 ),
inference(rat,[],[s319]) ).
cnf(s342,plain,
( spl21_90
| spl21_90
| ~ spl21_114
| ~ spl21_115 ),
inference(sat_conversion,[],[f3037]) ).
cnf(s343,plain,
( spl21_90
| ~ spl21_114
| ~ spl21_115 ),
inference(rat,[],[s342]) ).
cnf(s364,plain,
( ~ spl21_92
| spl21_185
| spl21_186 ),
inference(sat_conversion,[],[f3313]) ).
cnf(s382,plain,
( spl21_58
| ~ spl21_185
| spl21_196 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s386,plain,
( ~ spl21_40
| ~ spl21_186 ),
inference(sat_conversion,[],[f3618]) ).
cnf(s393,plain,
( spl21_40
| ~ spl21_186 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s417,plain,
( spl21_90
| ~ spl21_198 ),
inference(sat_conversion,[],[f3713]) ).
cnf(s441,plain,
( ~ spl21_196
| spl21_198 ),
inference(sat_conversion,[],[f4056]) ).
cnf(s472,plain,
spl21_231,
inference(sat_conversion,[],[f4682]) ).
cnf(s578,plain,
( ~ spl21_80
| spl21_90
| ~ spl21_114
| spl21_186
| ~ spl21_231
| spl21_335 ),
inference(sat_conversion,[],[f5927]) ).
cnf(s605,plain,
~ spl21_335,
inference(sat_conversion,[],[f7013]) ).
cnf(s650,plain,
( spl21_80
| spl21_90
| ~ spl21_114
| ~ spl21_231 ),
inference(sat_conversion,[],[f7968]) ).
cnf(s653,plain,
( ~ spl21_80
| spl21_90
| ~ spl21_114
| spl21_186
| ~ spl21_231 ),
inference(rat,[],[s578,s605]) ).
cnf(s657,plain,
( ~ spl21_72
| ~ spl21_51 ),
inference(rat,[],[s238,s280]) ).
cnf(s658,plain,
( ~ spl21_92
| ~ spl21_40 ),
inference(rat,[],[s382,s320,s364,s386,s441,s417,s294,s657,s32]) ).
cnf(s659,plain,
~ spl21_40,
inference(rat,[],[s653,s650,s168,s94,s658,s294,s657,s32,s386,s472]) ).
cnf(s662,plain,
~ spl21_186,
inference(rat,[],[s393,s659]) ).
cnf(s670,plain,
~ spl21_90,
inference(rat,[],[s238,s294]) ).
cnf(s673,plain,
~ spl21_198,
inference(rat,[],[s417,s670]) ).
cnf(s676,plain,
~ spl21_196,
inference(rat,[],[s441,s673]) ).
cnf(s686,plain,
spl21_58,
inference(rat,[],[s94,s168,s364,s343,s382,s174,s670,s662,s676]) ).
cnf(s688,plain,
~ spl21_92,
inference(rat,[],[s320,s670,s686]) ).
cnf(s691,plain,
~ spl21_64,
inference(rat,[],[s94,s670,s688]) ).
cnf(s692,plain,
spl21_114,
inference(rat,[],[s168,s691]) ).
cnf(s706,plain,
spl21_80,
inference(rat,[],[s650,s472,s670,s692]) ).
cnf(s707,plain,
$false,
inference(rat,[],[s653,s472,s662,s670,s692,s706]) ).
fof(f7995,plain,
$false,
inference(avatar_sat_refutation,[],[s707]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV759-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.09/0.18 % Computer : n006.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 12:27:18 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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.47/2.03 % (3929385)Input is clausal, will run a generic CNF schedule.
% 7.47/2.03 % (3929393)lrs+10_1_sil=8000:sp=occurrence:random_seed=3086178160:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.47/2.03 % (3929395)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4179362868:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.47/2.03 % (3929391)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=851900043:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.47/2.03 % (3929394)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4177614473:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.47/2.03 % (3929392)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3196295306:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.47/2.03 % (3929396)dis-21_1_sil=8000:lcm=predicate:random_seed=2504921427: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.47/2.03 % (3929390)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=3070585354:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.47/2.03 % (3929393)Instruction limit reached!
% 7.47/2.03 % (3929393)------------------------------
% 7.47/2.03 % (3929393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.03 % (3929393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.03 % (3929393)CaDiCaL version: 2.1.3
% 7.47/2.03 % (3929393)Termination reason: Instruction limit
% 7.47/2.03 % (3929393)Termination phase: Saturation
% 7.47/2.03 % (3929393)Time elapsed: 0.041 s
% 7.47/2.03 % (3929393)Peak memory usage: 90 MB
% 7.47/2.03 % (3929393)Instructions burned: 109 (million)
% 7.47/2.03 % (3929396)Instruction limit reached!
% 7.47/2.03 % (3929396)------------------------------
% 7.47/2.03 % (3929396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.03 % (3929396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.03 % (3929396)CaDiCaL version: 2.1.3
% 7.47/2.03 % (3929396)Termination reason: Instruction limit
% 7.47/2.03 % (3929396)Termination phase: Saturation
% 7.47/2.03 % (3929396)Time elapsed: 0.069 s
% 7.47/2.03 % (3929396)Peak memory usage: 89 MB
% 7.47/2.03 % (3929396)Instructions burned: 118 (million)
% 7.47/2.03 % (3929394)Instruction limit reached!
% 7.47/2.03 % (3929394)------------------------------
% 7.47/2.03 % (3929394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.03 % (3929394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.03 % (3929394)CaDiCaL version: 2.1.3
% 7.47/2.03 % (3929394)Termination reason: Instruction limit
% 7.47/2.03 % (3929394)Termination phase: Saturation
% 7.47/2.03 % (3929394)Time elapsed: 0.079 s
% 7.47/2.03 % (3929394)Peak memory usage: 88 MB
% 7.47/2.03 % (3929394)Instructions burned: 115 (million)
% 7.47/2.03 % (3929395)Instruction limit reached!
% 7.47/2.03 % (3929395)------------------------------
% 7.47/2.03 % (3929395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.03 % (3929395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.03 % (3929395)CaDiCaL version: 2.1.3
% 7.47/2.03 % (3929395)Termination reason: Instruction limit
% 7.47/2.03 % (3929395)Termination phase: Saturation
% 7.47/2.03 % (3929395)Time elapsed: 0.113 s
% 7.47/2.03 % (3929395)Peak memory usage: 90 MB
% 7.47/2.03 % (3929395)Instructions burned: 180 (million)
% 7.47/2.03 % (3929404)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=2653697994:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.47/2.03 % (3929404)Instruction limit reached!
% 7.47/2.03 % (3929404)------------------------------
% 7.47/2.03 % (3929404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.47/2.03 % (3929404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.47/2.03 % (3929404)CaDiCaL version: 2.1.3
% 7.47/2.03 % (3929404)Termination reason: Instruction limit
% 7.47/2.03 % (3929404)Termination phase: Saturation
% 7.47/2.03 % (3929404)Time elapsed: 0.049 s
% 7.47/2.03 % (3929404)Peak memory usage: 90 MB
% 7.47/2.03 % (3929404)Instructions burned: 145 (million)
% 7.47/2.03 % (3929405)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1235361668: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)
% 10.75/2.19 % (3929406)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=481579619:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.75/2.19 % (3929407)lrs+10_64_to=lpo:sil=8000:random_seed=4000190833:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.75/2.19 % (3929406)Refutation not found, incomplete strategy
% 10.75/2.19 % (3929406)------------------------------
% 10.75/2.19 % (3929406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929406)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929406)Termination reason: Refutation not found, incomplete strategy
% 10.75/2.19 % (3929406)Time elapsed: 0.044 s
% 10.75/2.19 % (3929406)Peak memory usage: 89 MB
% 10.75/2.19 % (3929406)Instructions burned: 71 (million)
% 10.75/2.19 % (3929409)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3817098703:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 10.75/2.19 % (3929405)Instruction limit reached!
% 10.75/2.19 % (3929405)------------------------------
% 10.75/2.19 % (3929405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929405)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929405)Termination reason: Instruction limit
% 10.75/2.19 % (3929405)Termination phase: Saturation
% 10.75/2.19 % (3929405)Time elapsed: 0.108 s
% 10.75/2.19 % (3929405)Peak memory usage: 90 MB
% 10.75/2.19 % (3929405)Instructions burned: 189 (million)
% 10.75/2.19 % (3929407)Instruction limit reached!
% 10.75/2.19 % (3929407)------------------------------
% 10.75/2.19 % (3929407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929407)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929407)Termination reason: Instruction limit
% 10.75/2.19 % (3929407)Termination phase: Saturation
% 10.75/2.19 % (3929407)Time elapsed: 0.079 s
% 10.75/2.19 % (3929407)Peak memory usage: 90 MB
% 10.75/2.19 % (3929407)Instructions burned: 127 (million)
% 10.75/2.19 % (3929409)Instruction limit reached!
% 10.75/2.19 % (3929409)------------------------------
% 10.75/2.19 % (3929409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929409)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929409)Termination reason: Instruction limit
% 10.75/2.19 % (3929409)Termination phase: Saturation
% 10.75/2.19 % (3929409)Time elapsed: 0.060 s
% 10.75/2.19 % (3929409)Peak memory usage: 90 MB
% 10.75/2.19 % (3929409)Instructions burned: 195 (million)
% 10.75/2.19 % (3929416)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=3274863742:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 10.75/2.19 % (3929414)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2955695165:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.75/2.19 % (3929416)Instruction limit reached!
% 10.75/2.19 % (3929416)------------------------------
% 10.75/2.19 % (3929416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929416)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929416)Termination reason: Instruction limit
% 10.75/2.19 % (3929416)Termination phase: Saturation
% 10.75/2.19 % (3929416)Time elapsed: 0.032 s
% 10.75/2.19 % (3929416)Peak memory usage: 89 MB
% 10.75/2.19 % (3929416)Instructions burned: 107 (million)
% 10.75/2.19 % (3929415)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=724153330:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 10.75/2.19 % (3929406)------------------------------
% 10.75/2.19 % (3929406)------------------------------
% 10.75/2.19 % (3929414)Instruction limit reached!
% 10.75/2.19 % (3929414)------------------------------
% 10.75/2.19 % (3929414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929414)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929414)Termination reason: Instruction limit
% 10.75/2.19 % (3929414)Termination phase: Saturation
% 10.75/2.19 % (3929414)Time elapsed: 0.105 s
% 10.75/2.19 % (3929414)Peak memory usage: 91 MB
% 10.75/2.19 % (3929414)Instructions burned: 158 (million)
% 10.75/2.19 % (3929419)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2389191894:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 10.75/2.19 % (3929419)Instruction limit reached!
% 10.75/2.19 % (3929419)------------------------------
% 10.75/2.19 % (3929419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929419)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929419)Termination reason: Instruction limit
% 10.75/2.19 % (3929419)Termination phase: Saturation
% 10.75/2.19 % (3929419)Time elapsed: 0.037 s
% 10.75/2.19 % (3929419)Peak memory usage: 90 MB
% 10.75/2.19 % (3929419)Instructions burned: 107 (million)
% 10.75/2.19 % (3929421)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1433143170:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.75/2.19 % (3929422)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=580717943:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 10.75/2.19 % (3929424)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3322593341:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 10.75/2.19 % (3929424)Instruction limit reached!
% 10.75/2.19 % (3929424)------------------------------
% 10.75/2.19 % (3929424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929424)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929424)Termination reason: Instruction limit
% 10.75/2.19 % (3929424)Termination phase: Saturation
% 10.75/2.19 % (3929424)Time elapsed: 0.036 s
% 10.75/2.19 % (3929424)Peak memory usage: 89 MB
% 10.75/2.19 % (3929424)Instructions burned: 135 (million)
% 10.75/2.19 % (3929421)Instruction limit reached!
% 10.75/2.19 % (3929421)------------------------------
% 10.75/2.19 % (3929421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929421)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929421)Termination reason: Instruction limit
% 10.75/2.19 % (3929421)Termination phase: Saturation
% 10.75/2.19 % (3929421)Time elapsed: 0.142 s
% 10.75/2.19 % (3929421)Peak memory usage: 90 MB
% 10.75/2.19 % (3929421)Instructions burned: 242 (million)
% 10.75/2.19 % (3929428)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2019568540:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 10.75/2.19 % (3929429)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2610460026:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 10.75/2.19 % (3929390)First to succeed.
% 10.75/2.19 % (3929390)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3929385"
% 10.75/2.19 % (3929428)Instruction limit reached!
% 10.75/2.19 % (3929428)------------------------------
% 10.75/2.19 % (3929428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929428)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929428)Termination reason: Instruction limit
% 10.75/2.19 % (3929428)Termination phase: Saturation
% 10.75/2.19 % (3929428)Time elapsed: 0.173 s
% 10.75/2.19 % (3929428)Peak memory usage: 96 MB
% 10.75/2.19 % (3929428)Instructions burned: 499 (million)
% 10.75/2.19 % (3929429)Instruction limit reached!
% 10.75/2.19 % (3929429)------------------------------
% 10.75/2.19 % (3929429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929429)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929429)Termination reason: Instruction limit
% 10.75/2.19 % (3929429)Termination phase: Saturation
% 10.75/2.19 % (3929429)Time elapsed: 0.122 s
% 10.75/2.19 % (3929429)Peak memory usage: 91 MB
% 10.75/2.19 % (3929429)Instructions burned: 191 (million)
% 10.75/2.19 % (3929392)Also succeeded, but the first one will report.
% 10.75/2.19 % (3929432)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3383455373:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 10.75/2.19 % (3929433)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=878716429:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 10.75/2.19 % (3929432)Instruction limit reached!
% 10.75/2.19 % (3929432)------------------------------
% 10.75/2.19 % (3929432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.75/2.19 % (3929432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.75/2.19 % (3929432)CaDiCaL version: 2.1.3
% 10.75/2.19 % (3929432)Termination reason: Instruction limit
% 10.75/2.19 % (3929432)Termination phase: Saturation
% 10.75/2.19 % (3929432)Time elapsed: 0.084 s
% 10.75/2.19 % (3929432)Peak memory usage: 91 MB
% 10.75/2.19 % (3929432)Instructions burned: 267 (million)
% 10.75/2.19 % (3929390)Refutation found. Thanks to Tanya!
% 10.75/2.19 % SZS status Unsatisfiable for theBenchmark
% 10.75/2.19 % SZS output start Proof for theBenchmark
% See solution above
% 11.18/2.38 % (3929390)------------------------------
% 11.18/2.38 % (3929390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.38 % (3929390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.38 % (3929390)CaDiCaL version: 2.1.3
% 11.18/2.38 % (3929390)Termination reason: Refutation
% 11.18/2.38 % (3929390)Time elapsed: 1.041 s
% 11.18/2.38 % (3929390)Peak memory usage: 135 MB
% 11.18/2.38 % (3929390)Instructions burned: 1738 (million)
% 11.18/2.38 % (3929390)------------------------------
% 11.18/2.38 % (3929390)------------------------------
% 11.18/2.38 % (3929385)Success in time 1.534 s
% 11.18/2.38 % Vampire exiting
%------------------------------------------------------------------------------