%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP378_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 11:33:44 AM UTC 2026
% Result : Theorem 24.95s 4.89s
% Output : Refutation 27.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 7
% Syntax : Number of formulae : 99 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 641 ( 92 equ)
% Maximal formula atoms : 24 ( 6 avg)
% Number of connectives : 874 ( 332 ~; 305 |; 177 &)
% ( 7 <=>; 53 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 8 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of FOOLs : 2 ( 2 fml; 0 var)
% Number arithmetic : 677 ( 192 atm; 97 fun; 388 num; 0 var)
% Number of types : 24 ( 22 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 167 ( 159 usr; 24 con; 0-4 aty)
% Number of variables : 197 ( 171 !; 26 ?; 197 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Int_bool_fun$': $tType ).
tff(type_def_6,type,
'Pratt_list_list$': $tType ).
tff(type_def_7,type,
'Pratt_list_bool_fun$': $tType ).
tff(type_def_8,type,
'Pratt_list$': $tType ).
tff(type_def_9,type,
'Nat_list$': $tType ).
tff(type_def_10,type,
'Int_set$': $tType ).
tff(type_def_11,type,
'Int_int_fun$': $tType ).
tff(type_def_12,type,
'Nat_nat_fun$': $tType ).
tff(type_def_13,type,
'Nat$': $tType ).
tff(type_def_14,type,
'Pratt$': $tType ).
tff(type_def_15,type,
'Pratt_bool_fun$': $tType ).
tff(type_def_16,type,
'Nat_multiset_nat_multiset_fun$': $tType ).
tff(type_def_17,type,
'Nat_multiset$': $tType ).
tff(type_def_18,type,
'Int_multiset$': $tType ).
tff(type_def_19,type,
'Pratt_list_pratt_list_list_fun$': $tType ).
tff(type_def_20,type,
tlbool: $tType ).
tff(type_def_21,type,
'Pratt_list_pratt_list_bool_fun_fun$': $tType ).
tff(type_def_22,type,
'Int_multiset_int_multiset_fun$': $tType ).
tff(type_def_23,type,
'Nat_bool_fun$': $tType ).
tff(type_def_24,type,
'Pratt_set$': $tType ).
tff(type_def_25,type,
'Nat_set$': $tType ).
tff(type_def_26,type,
'Nat_int_fun$': $tType ).
tff(func_def_0,type,
'collect$b': 'Pratt_bool_fun$' > 'Pratt_set$' ).
tff(func_def_1,type,
'nil$': 'Pratt_list$' ).
tff(func_def_2,type,
'prime$b': 'Int_bool_fun$' ).
tff(func_def_3,type,
'uub$': 'Pratt_set$' > 'Pratt_bool_fun$' ).
tff(func_def_4,type,
'fun_app$h': ( 'Int_multiset_int_multiset_fun$' * 'Int_multiset$' ) > 'Int_multiset$' ).
tff(func_def_5,type,
'collect$a': 'Nat_bool_fun$' > 'Nat_set$' ).
tff(func_def_6,type,
'pa$': 'Nat$' ).
tff(func_def_7,type,
'zero$': 'Nat$' ).
tff(func_def_8,type,
'minus$b': 'Int_multiset$' > 'Int_multiset_int_multiset_fun$' ).
tff(func_def_9,type,
'ta$': 'Pratt$' ).
tff(func_def_10,type,
'cong$': ( 'Nat$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_11,type,
'valid_cert_rel$': 'Pratt_list_pratt_list_bool_fun_fun$' ).
tff(func_def_12,type,
'pratt_triple$': ( 'Nat$' * 'Nat$' ) > 'Nat_bool_fun$' ).
tff(func_def_13,type,
'times$a': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_14,type,
'prime_factorization$': 'Nat$' > 'Nat_multiset$' ).
tff(func_def_15,type,
'of_nat$': 'Nat$' > $int ).
tff(func_def_16,type,
'fun_app$j': ( 'Pratt_list_pratt_list_list_fun$' * 'Pratt_list$' ) > 'Pratt_list_list$' ).
tff(func_def_17,type,
'zero$a': 'Int_multiset$' ).
tff(func_def_18,type,
'nil$a': 'Pratt_list_list$' ).
tff(func_def_19,type,
'fun_app$g': ( 'Nat_multiset_nat_multiset_fun$' * 'Nat_multiset$' ) > 'Nat_multiset$' ).
tff(func_def_20,type,
'c$': 'Pratt_list$' ).
tff(func_def_21,type,
tltrue: tlbool ).
tff(func_def_22,type,
'times$': ( $int * $int ) > $int ).
tff(func_def_23,type,
'minus$a': 'Nat_multiset$' > 'Nat_multiset_nat_multiset_fun$' ).
tff(func_def_24,type,
'one$': 'Nat$' ).
tff(func_def_25,type,
'fun_app$f': ( 'Nat_int_fun$' * 'Nat$' ) > $int ).
tff(func_def_26,type,
'triple$': ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Pratt$' ).
tff(func_def_27,type,
'set_mset$a': 'Int_multiset$' > 'Int_set$' ).
tff(func_def_28,type,
'fun_app$i': ( 'Pratt_list_pratt_list_bool_fun_fun$' * 'Pratt_list$' ) > 'Pratt_list_bool_fun$' ).
tff(func_def_29,type,
'cons$a': ( 'Pratt_list$' * 'Pratt_list_list$' ) > 'Pratt_list_list$' ).
tff(func_def_30,type,
'power$a': $int > 'Nat_int_fun$' ).
tff(func_def_31,type,
'fun_app$d': ( 'Nat_nat_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_32,type,
'divide$': $int > 'Int_int_fun$' ).
tff(func_def_33,type,
'fun_app$': ( 'Int_int_fun$' * $int ) > $int ).
tff(func_def_34,type,
'dvd$': $int > 'Int_bool_fun$' ).
tff(func_def_35,type,
'less$': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_36,type,
'ys$': 'Pratt_list$' ).
tff(func_def_37,type,
'n_lists$': 'Nat$' > 'Pratt_list_pratt_list_list_fun$' ).
tff(func_def_38,type,
'xa$': 'Nat$' ).
tff(func_def_39,type,
't$': 'Pratt$' ).
tff(func_def_40,type,
'size_pratt$': 'Pratt$' > 'Nat$' ).
tff(func_def_41,type,
'totient$': 'Nat$' > 'Nat$' ).
tff(func_def_42,type,
'dvd$a': 'Nat$' > 'Nat_bool_fun$' ).
tff(func_def_43,type,
'set$': 'Pratt_list$' > 'Pratt_set$' ).
tff(func_def_44,type,
'uu$': 'Int_set$' > 'Int_bool_fun$' ).
tff(func_def_45,type,
'cons$b': ( 'Nat$' * 'Nat_list$' ) > 'Nat_list$' ).
tff(func_def_46,type,
'prime$a': 'Nat_bool_fun$' ).
tff(func_def_47,type,
'minus$': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_48,type,
'prime_factorization$a': $int > 'Int_multiset$' ).
tff(func_def_49,type,
tlfalse: tlbool ).
tff(func_def_50,type,
'nat$': $int > 'Nat$' ).
tff(func_def_51,type,
'valid_cert$': 'Pratt_list_bool_fun$' ).
tff(func_def_52,type,
'accp$': 'Pratt_list_pratt_list_bool_fun_fun$' > 'Pratt_list_bool_fun$' ).
tff(func_def_53,type,
'set_mset$': 'Nat_multiset$' > 'Nat_set$' ).
tff(func_def_54,type,
'divide$a': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_55,type,
'aa$': 'Nat$' ).
tff(func_def_56,type,
'uuc$': $int > 'Int_int_fun$' ).
tff(func_def_57,type,
'zero$b': 'Nat_multiset$' ).
tff(func_def_58,type,
'set$a': 'Nat_list$' > 'Nat_set$' ).
tff(func_def_59,type,
'cons$': ( 'Pratt$' * 'Pratt_list$' ) > 'Pratt_list$' ).
tff(func_def_60,type,
'uua$': 'Nat_set$' > 'Nat_bool_fun$' ).
tff(func_def_61,type,
'cong$a': ( $int * $int ) > 'Int_bool_fun$' ).
tff(func_def_62,type,
'prime$': 'Nat$' > 'Pratt$' ).
tff(func_def_63,type,
'collect$': 'Int_bool_fun$' > 'Int_set$' ).
tff(func_def_64,type,
'power$': 'Nat$' > 'Nat_nat_fun$' ).
tff(func_def_65,type,
'y$': 'Pratt$' ).
tff(func_def_72,type,
sK0: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_73,type,
sK1: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_74,type,
sK2: ( 'Nat_bool_fun$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_75,type,
sK3: 'Pratt$' > 'Nat$' ).
tff(func_def_76,type,
sK4: 'Pratt$' > 'Nat$' ).
tff(func_def_77,type,
sK5: 'Pratt$' > 'Nat$' ).
tff(func_def_78,type,
sK6: 'Pratt$' > 'Nat$' ).
tff(func_def_79,type,
sK7: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_80,type,
sK8: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_81,type,
sK9: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_82,type,
sK10: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_83,type,
sK11: ( $int * $int ) > $int ).
tff(func_def_84,type,
sK12: ( $int * $int * $int ) > $int ).
tff(func_def_85,type,
sK13: ( $int * $int * $int ) > $int ).
tff(func_def_86,type,
sK14: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_87,type,
sK15: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_88,type,
sK16: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_89,type,
sK17: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_90,type,
sK18: 'Nat$' > 'Nat$' ).
tff(func_def_91,type,
sK19: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_92,type,
sK20: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_93,type,
sK21: 'Nat$' > 'Nat$' ).
tff(func_def_94,type,
sK22: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_95,type,
sK23: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_96,type,
sK24: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_97,type,
sK25: 'Nat$' > 'Nat$' ).
tff(func_def_98,type,
sK26: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_99,type,
sK27: 'Nat$' ).
tff(func_def_100,type,
sK28: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_101,type,
sK29: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_102,type,
sK30: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_103,type,
sK31: 'Pratt_list$' > 'Pratt$' ).
tff(func_def_104,type,
sK32: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_105,type,
sK33: 'Nat$' > 'Nat$' ).
tff(func_def_106,type,
sK34: 'Nat$' > 'Nat$' ).
tff(func_def_107,type,
sK35: 'Nat$' > 'Nat$' ).
tff(func_def_108,type,
sK36: ( $int * $int ) > $int ).
tff(func_def_109,type,
sK37: ( $int * $int * $int ) > $int ).
tff(func_def_110,type,
sK38: ( $int * $int * $int ) > $int ).
tff(func_def_111,type,
sK39: 'Nat$' > 'Nat$' ).
tff(func_def_112,type,
sK40: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_113,type,
sK41: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_114,type,
sK42: 'Nat_bool_fun$' > 'Nat$' ).
tff(func_def_115,type,
sK43: 'Nat$' > 'Nat$' ).
tff(func_def_116,type,
sK44: ( 'Pratt_list$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_117,type,
sK45: 'Nat$' > 'Nat$' ).
tff(func_def_118,type,
sK46: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_119,type,
sK47: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_120,type,
sK48: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_121,type,
sK49: ( $int * $int ) > $int ).
tff(func_def_122,type,
sK50: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_123,type,
sK51: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_124,type,
sK52: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_125,type,
sK53: 'Nat$' > 'Nat$' ).
tff(func_def_126,type,
sK54: 'Nat$' > 'Nat$' ).
tff(func_def_127,type,
sK55: 'Nat$' > 'Nat$' ).
tff(func_def_128,type,
sK56: 'Pratt_list$' > 'Nat$' ).
tff(func_def_129,type,
sK57: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_130,type,
sK58: 'Pratt_list$' > 'Nat$' ).
tff(func_def_131,type,
sK59: 'Pratt_list$' > 'Nat$' ).
tff(func_def_132,type,
sK60: 'Pratt_list$' > 'Nat$' ).
tff(func_def_133,type,
sK61: 'Pratt_list$' > 'Nat$' ).
tff(func_def_134,type,
sK62: 'Pratt_list$' > 'Nat$' ).
tff(func_def_135,type,
sK63: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_136,type,
sK64: 'Pratt_list$' > 'Nat$' ).
tff(func_def_137,type,
sK65: 'Pratt_list_bool_fun$' > 'Pratt$' ).
tff(func_def_138,type,
sK66: 'Pratt_list_bool_fun$' > 'Pratt_list$' ).
tff(func_def_139,type,
sK67: 'Pratt_list_bool_fun$' > 'Pratt$' ).
tff(func_def_140,type,
sK68: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_141,type,
sK69: 'Pratt_list$' > 'Nat$' ).
tff(func_def_142,type,
sK70: 'Pratt_list$' > 'Nat$' ).
tff(func_def_143,type,
sK71: 'Pratt_list$' > 'Nat$' ).
tff(func_def_144,type,
sK72: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_145,type,
sK73: 'Pratt_list$' > 'Nat$' ).
tff(func_def_146,type,
sK74: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_147,type,
sK75: ( 'Nat$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_148,type,
sK76: ( 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_149,type,
sK77: ( 'Pratt_list$' * 'Pratt$' ) > 'Pratt_list$' ).
tff(func_def_150,type,
sK78: ( 'Pratt_list$' * 'Pratt$' ) > 'Pratt_list$' ).
tff(func_def_151,type,
sK79: ( 'Pratt_list$' * 'Pratt$' ) > 'Pratt$' ).
tff(func_def_152,type,
sK80: ( $int * $int ) > $int ).
tff(func_def_153,type,
sK81: 'Pratt_list$' > 'Nat$' ).
tff(func_def_154,type,
sK82: 'Pratt_list$' > 'Nat$' ).
tff(func_def_155,type,
sK83: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_156,type,
sK84: 'Pratt_list$' > 'Nat$' ).
tff(func_def_157,type,
sK85: 'Pratt_list$' > 'Nat$' ).
tff(func_def_158,type,
sK86: 'Pratt_list$' > 'Pratt_list$' ).
tff(func_def_159,type,
sK87: 'Pratt$' > 'Nat$' ).
tff(func_def_160,type,
sK88: 'Pratt$' > 'Nat$' ).
tff(func_def_161,type,
sK89: 'Pratt$' > 'Nat$' ).
tff(func_def_162,type,
sK90: 'Pratt$' > 'Nat$' ).
tff(func_def_163,type,
sK91: ( 'Nat$' * 'Pratt_list$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_164,type,
sK92: ( 'Nat$' * 'Pratt_list$' * 'Nat$' * 'Nat$' ) > 'Nat$' ).
tff(func_def_168,type,
-1: $int > $int ).
tff(func_def_169,type,
2: $int > $int ).
tff(pred_def_1,type,
'member$': ( 'Pratt$' * 'Pratt_set$' ) > $o ).
tff(pred_def_2,type,
'member$a': ( 'Nat$' * 'Nat_set$' ) > $o ).
tff(pred_def_3,type,
'fun_app$e': ( 'Pratt_list_bool_fun$' * 'Pratt_list$' ) > $o ).
tff(pred_def_4,type,
'fun_app$b': ( 'Nat_bool_fun$' * 'Nat$' ) > $o ).
tff(pred_def_5,type,
'fun_app$a': ( 'Pratt_bool_fun$' * 'Pratt$' ) > $o ).
tff(pred_def_6,type,
'member$b': ( $int * 'Int_set$' ) > $o ).
tff(pred_def_7,type,
'fun_app$c': ( 'Int_bool_fun$' * $int ) > $o ).
tff(f5,conjecture,
( ( ( 'ta$' = 'triple$'('pa$','aa$','xa$') )
=> ( $less(0,'of_nat$'('xa$'))
& ! [X0: 'Nat$'] :
( 'member$a'(X0,'set_mset$'('prime_factorization$'('xa$')))
=> ~ ( ( $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X0)))),'nat$'(1)),'pa$') )
& ( ~ $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($difference('of_nat$'('pa$'),1)),'of_nat$'(X0)))),'nat$'(1)),'pa$') ) ) ) ) )
& ( ( 'ta$' = 'prime$'('pa$') )
=> 'fun_app$b'('prime$a','pa$') ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture4) ).
tff(f6,negated_conjecture,
~ ( ( ( 'ta$' = 'triple$'('pa$','aa$','xa$') )
=> ( $less(0,'of_nat$'('xa$'))
& ! [X0: 'Nat$'] :
( 'member$a'(X0,'set_mset$'('prime_factorization$'('xa$')))
=> ~ ( ( $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X0)))),'nat$'(1)),'pa$') )
& ( ~ $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($difference('of_nat$'('pa$'),1)),'of_nat$'(X0)))),'nat$'(1)),'pa$') ) ) ) ) )
& ( ( 'ta$' = 'prime$'('pa$') )
=> 'fun_app$b'('prime$a','pa$') ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
tff(f11,axiom,
! [X0: 'Pratt$'] :
( ( ! [X1: 'Nat$',X2: 'Nat$',X3: 'Nat$'] :
( ( X0 = 'triple$'(X1,X2,X3) )
=> $false )
& ! [X1: 'Nat$'] :
( ( X0 = 'prime$'(X1) )
=> $false ) )
=> $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom9) ).
tff(f101,axiom,
'member$'('ta$','set$'('ys$')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom99) ).
tff(f193,axiom,
! [X3: 'Nat$',X2: 'Nat$',X1: 'Nat$',X0: 'Pratt$'] :
( ( 'member$'(X0,'set$'('ys$'))
& 'fun_app$e'('valid_cert$','ys$') )
=> ( ( ( X0 = 'prime$'(X1) )
=> 'fun_app$b'('prime$a',X1) )
& ( ( X0 = 'triple$'(X1,X2,X3) )
=> ( ! [X4: 'Nat$'] :
( 'member$a'(X4,'set_mset$'('prime_factorization$'(X3)))
=> ~ ( ( ~ $less('of_nat$'(X1),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'('fun_app$'('divide$'($difference('of_nat$'(X1),1)),'of_nat$'(X4)))),'nat$'(1)),X1) )
& ( $less('of_nat$'(X1),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X1) ) ) )
& $less(0,'of_nat$'(X3)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom191) ).
tff(f201,axiom,
'fun_app$e'('valid_cert$','cons$'('y$','ys$')),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom199) ).
tff(f203,axiom,
! [X0: 'Nat$',X1: 'Pratt_list$'] :
( ( ? [X2: 'Nat$'] :
( ( $less('of_nat$'(X0),1)
=> 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
& ( ~ $less('of_nat$'(X0),1)
=> 'member$'('triple$'(X0,X2,'nat$'($difference('of_nat$'(X0),1))),'set$'(X1)) )
& ( $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($difference('of_nat$'(X0),1))),'nat$'(1)),X0) ) )
& $less(1,'of_nat$'(X0))
& 'fun_app$e'('valid_cert$',X1) )
<=> 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom201) ).
tff(f205,axiom,
! [X0: 'Nat$',X3: 'Pratt_list$',X2: 'Nat$',X1: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$',X3)
& ( ? [X4: 'Nat$',X5: 'Nat$'] :
( 'member$'('triple$'(X0,X1,X5),'set$'(X3))
& 'member$'('prime$'(X4),'set$'(X3))
& ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& ~ ( ( ~ $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($difference('of_nat$'(X0),1)),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& $less(1,'of_nat$'(X0))
& $less(0,'of_nat$'(X2)) )
<=> 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X1,X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom203) ).
tff(f655,plain,
! [X3: 'Nat$',X2: 'Nat$',X1: 'Nat$',X0: 'Pratt$'] :
( ( 'member$'(X0,'set$'('ys$'))
& 'fun_app$e'('valid_cert$','ys$') )
=> ( ( ( X0 = 'prime$'(X1) )
=> 'fun_app$b'('prime$a',X1) )
& ( ( X0 = 'triple$'(X1,X2,X3) )
=> ( ! [X4: 'Nat$'] :
( 'member$a'(X4,'set_mset$'('prime_factorization$'(X3)))
=> ~ ( ( ~ $less('of_nat$'(X1),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X1),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X1) )
& ( $less('of_nat$'(X1),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X1) ) ) )
& $less(0,'of_nat$'(X3)) ) ) ) ),
inference(theory_normalization,[],[f193]) ).
tff(f673,plain,
! [X0: 'Nat$',X1: 'Pratt_list$'] :
( 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1))
<=> ( 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0))
& ? [X2: 'Nat$'] :
( ( $less('of_nat$'(X0),1)
=> 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
& ( ~ $less('of_nat$'(X0),1)
=> 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
& ( $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) ) ) ),
inference(theory_normalization,[],[f203]) ).
tff(f694,plain,
~ ( ( ( 'ta$' = 'triple$'('pa$','aa$','xa$') )
=> ( $less(0,'of_nat$'('xa$'))
& ! [X0: 'Nat$'] :
( 'member$a'(X0,'set_mset$'('prime_factorization$'('xa$')))
=> ~ ( ( $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X0)))),'nat$'(1)),'pa$') )
& ( ~ $less('of_nat$'('pa$'),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(X0)))),'nat$'(1)),'pa$') ) ) ) ) )
& ( ( 'ta$' = 'prime$'('pa$') )
=> 'fun_app$b'('prime$a','pa$') ) ),
inference(theory_normalization,[],[f6]) ).
tff(f698,plain,
! [X0: 'Nat$',X3: 'Pratt_list$',X2: 'Nat$',X1: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$',X3)
& ( ? [X4: 'Nat$',X5: 'Nat$'] :
( 'member$'('triple$'(X0,X1,X5),'set$'(X3))
& 'member$'('prime$'(X4),'set$'(X3))
& ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& ~ ( ( ~ $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& $less(1,'of_nat$'(X0))
& $less(0,'of_nat$'(X2)) )
<=> 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X1,X2),X3)) ),
inference(theory_normalization,[],[f205]) ).
tff(f842,plain,
! [X0: 'Pratt$'] :
( ( ! [X1: 'Nat$',X2: 'Nat$',X3: 'Nat$'] :
( ( X0 = 'triple$'(X1,X2,X3) )
=> $false )
& ! [X4: 'Nat$'] :
( ( 'prime$'(X4) = X0 )
=> $false ) )
=> $false ),
inference(rectify,[],[f11]) ).
tff(f843,plain,
! [X0: 'Pratt$'] :
~ ( ! [X1: 'Nat$',X2: 'Nat$',X3: 'Nat$'] :
( ( ~ X0 ) = 'triple$'(X1,X2,X3) )
& ! [X4: 'Nat$'] :
( ( ~ 'prime$'(X4) ) = X0 ) ),
inference(true_and_false_elimination,[],[f842]) ).
tff(f844,plain,
! [X0: 'Pratt$'] :
~ ( ! [X4: 'Nat$'] : ( 'prime$'(X4) != X0 )
& ! [X1: 'Nat$',X3: 'Nat$',X2: 'Nat$'] : ( 'triple$'(X1,X2,X3) != X0 ) ),
inference(flattening,[],[f843]) ).
tff(f883,plain,
! [X2: 'Nat$',X1: 'Nat$',X3: 'Pratt$',X0: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$','ys$')
& 'member$'(X3,'set$'('ys$')) )
=> ( ( ( 'triple$'(X2,X1,X0) = X3 )
=> ( $less(0,'of_nat$'(X0))
& ! [X4: 'Nat$'] :
( 'member$a'(X4,'set_mset$'('prime_factorization$'(X0)))
=> ~ ( ( ~ $less('of_nat$'(X2),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X2),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X2) )
& ( $less('of_nat$'(X2),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X2) ) ) ) ) )
& ( ( 'prime$'(X2) = X3 )
=> 'fun_app$b'('prime$a',X2) ) ) ),
inference(rectify,[],[f655]) ).
tff(f999,plain,
! [X1: 'Pratt_list$',X3: 'Nat$',X0: 'Nat$',X2: 'Nat$'] :
( ( ( ? [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& 'member$'('triple$'(X0,X3,X5),'set$'(X1))
& 'member$'('prime$'(X4),'set$'(X1))
& ~ ( ( ~ $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( $less('of_nat$'(X0),1)
=> 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& $less(1,'of_nat$'(X0))
& 'fun_app$e'('valid_cert$',X1)
& $less(0,'of_nat$'(X2)) )
<=> 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1)) ),
inference(rectify,[],[f698]) ).
tff(f1014,plain,
! [X0: 'Nat$',X1: 'Pratt_list$',X2: 'Nat$',X3: 'Nat$'] :
( 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
<=> ( $less(0,'of_nat$'(X2))
& ( ? [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& 'member$'('prime$'(X4),'set$'(X1))
& 'member$'('triple$'(X0,X3,X5),'set$'(X1))
& ( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) ) ),
inference(ennf_transformation,[],[f999]) ).
tff(f1032,plain,
! [X1: 'Pratt_list$',X0: 'Nat$'] :
( ( ? [X2: 'Nat$'] :
( ( ~ $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
& ( $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0)
| ~ $less('of_nat$'(X0),1) )
& ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
<=> 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1)) ),
inference(ennf_transformation,[],[f673]) ).
tff(f1048,plain,
( ( ( ~ $less(0,'of_nat$'('xa$'))
| ? [X0: 'Nat$'] :
( ( ~ $less('of_nat$'('pa$'),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X0)))),'nat$'(1)),'pa$') )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(X0)))),'nat$'(1)),'pa$')
| $less('of_nat$'('pa$'),1) )
& 'member$a'(X0,'set_mset$'('prime_factorization$'('xa$'))) ) )
& ( 'ta$' = 'triple$'('pa$','aa$','xa$') ) )
| ( ~ 'fun_app$b'('prime$a','pa$')
& ( 'ta$' = 'prime$'('pa$') ) ) ),
inference(ennf_transformation,[],[f694]) ).
tff(f1049,plain,
( ( ~ 'fun_app$b'('prime$a','pa$')
& ( 'ta$' = 'prime$'('pa$') ) )
| ( ( ? [X0: 'Nat$'] :
( 'member$a'(X0,'set_mset$'('prime_factorization$'('xa$')))
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(X0)))),'nat$'(1)),'pa$')
| $less('of_nat$'('pa$'),1) )
& ( ~ $less('of_nat$'('pa$'),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X0)))),'nat$'(1)),'pa$') ) )
| ~ $less(0,'of_nat$'('xa$')) )
& ( 'ta$' = 'triple$'('pa$','aa$','xa$') ) ) ),
inference(flattening,[],[f1048]) ).
tff(f1234,plain,
! [X2: 'Nat$',X1: 'Nat$',X3: 'Pratt$',X0: 'Nat$'] :
( ( ( ( $less(0,'of_nat$'(X0))
& ! [X4: 'Nat$'] :
( ( ~ $less('of_nat$'(X2),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X2),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X2) )
| ( $less('of_nat$'(X2),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X2) )
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X0))) ) )
| ( 'triple$'(X2,X1,X0) != X3 ) )
& ( 'fun_app$b'('prime$a',X2)
| ( 'prime$'(X2) != X3 ) ) )
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(ennf_transformation,[],[f883]) ).
tff(f1235,plain,
! [X2: 'Nat$',X1: 'Nat$',X0: 'Nat$',X3: 'Pratt$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ( ( 'fun_app$b'('prime$a',X2)
| ( 'prime$'(X2) != X3 ) )
& ( ( 'triple$'(X2,X1,X0) != X3 )
| ( ! [X4: 'Nat$'] :
( ( ~ $less('of_nat$'(X2),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X2),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X2) )
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X0)))
| ( $less('of_nat$'(X2),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X2) ) )
& $less(0,'of_nat$'(X0)) ) ) )
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(flattening,[],[f1234]) ).
tff(f1325,plain,
! [X0: 'Pratt$'] :
( ? [X1: 'Nat$',X2: 'Nat$',X3: 'Nat$'] : ( 'triple$'(X1,X2,X3) = X0 )
| ? [X4: 'Nat$'] : ( 'prime$'(X4) = X0 ) ),
inference(ennf_transformation,[],[f844]) ).
tff(f1373,plain,
! [X0: 'Pratt$'] :
( ( 'triple$'(sK3(X0),sK4(X0),sK5(X0)) = X0 )
| ( 'prime$'(sK6(X0)) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X1,sK3(X0)),skolemize(X2,sK4(X0)),skolemize(X3,sK5(X0)),skolemize(X4,sK6(X0))],[f1325]) ).
tff(f1489,plain,
( ( ~ 'fun_app$b'('prime$a','pa$')
& ( 'ta$' = 'prime$'('pa$') ) )
| ( ( ( 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| $less('of_nat$'('pa$'),1) )
& ( ~ $less('of_nat$'('pa$'),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(sK27)))),'nat$'(1)),'pa$') ) )
| ~ $less(0,'of_nat$'('xa$')) )
& ( 'ta$' = 'triple$'('pa$','aa$','xa$') ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X0,sK27)],[f1049]) ).
tff(f1613,plain,
! [X0: 'Nat$',X1: 'Nat$',X2: 'Nat$',X3: 'Pratt$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ( ( 'fun_app$b'('prime$a',X0)
| ( 'prime$'(X0) != X3 ) )
& ( ( 'triple$'(X0,X1,X2) != X3 )
| ( ! [X4: 'Nat$'] :
( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2)))
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) )
& $less(0,'of_nat$'(X2)) ) ) )
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(rectify,[],[f1235]) ).
tff(f1618,plain,
! [X1: 'Pratt_list$',X0: 'Nat$'] :
( ( ( ? [X2: 'Nat$'] :
( ( ~ $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
& ( $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0)
| ~ $less('of_nat$'(X0),1) )
& ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1)) )
& ( 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1))
| ! [X2: 'Nat$'] :
( ( $less('of_nat$'(X0),1)
& ~ 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
| ( ~ $less('of_nat$'(X0),1)
& ~ 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
| ( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0)
& $less('of_nat$'(X0),1) )
| ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) ) ),
inference(nnf_transformation,[],[f1032]) ).
tff(f1619,plain,
! [X1: 'Pratt_list$',X0: 'Nat$'] :
( ( ( ? [X2: 'Nat$'] :
( ( ~ $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
& ( $less('of_nat$'(X0),1)
| 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0)
| ~ $less('of_nat$'(X0),1) )
& ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1)) )
& ( 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),X1))
| ! [X2: 'Nat$'] :
( ( $less('of_nat$'(X0),1)
& ~ 'member$'('triple$'(X0,X2,'nat$'(0)),'set$'(X1)) )
| ( ~ $less('of_nat$'(X0),1)
& ~ 'member$'('triple$'(X0,X2,'nat$'($sum('of_nat$'(X0),$uminus(1)))),'set$'(X1)) )
| ( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X0)
& $less('of_nat$'(X0),1) )
| ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X0),$uminus(1)))),'nat$'(1)),X0) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) ) ),
inference(flattening,[],[f1618]) ).
tff(f1620,plain,
! [X0: 'Pratt_list$',X1: 'Nat$'] :
( ( ( ? [X2: 'Nat$'] :
( ( ~ $less('of_nat$'(X1),1)
| 'member$'('triple$'(X1,X2,'nat$'(0)),'set$'(X0)) )
& ( $less('of_nat$'(X1),1)
| 'member$'('triple$'(X1,X2,'nat$'($sum('of_nat$'(X1),$uminus(1)))),'set$'(X0)) )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'(0)),'nat$'(1)),X1)
| ~ $less('of_nat$'(X1),1) )
& ( $less('of_nat$'(X1),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X2),'nat$'($sum('of_nat$'(X1),$uminus(1)))),'nat$'(1)),X1) ) )
& 'fun_app$e'('valid_cert$',X0)
& $less(1,'of_nat$'(X1)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X1),X0)) )
& ( 'fun_app$e'('valid_cert$','cons$'('prime$'(X1),X0))
| ! [X3: 'Nat$'] :
( ( $less('of_nat$'(X1),1)
& ~ 'member$'('triple$'(X1,X3,'nat$'(0)),'set$'(X0)) )
| ( ~ $less('of_nat$'(X1),1)
& ~ 'member$'('triple$'(X1,X3,'nat$'($sum('of_nat$'(X1),$uminus(1)))),'set$'(X0)) )
| ( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'(0)),'nat$'(1)),X1)
& $less('of_nat$'(X1),1) )
| ( ~ $less('of_nat$'(X1),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'($sum('of_nat$'(X1),$uminus(1)))),'nat$'(1)),X1) ) )
| ~ 'fun_app$e'('valid_cert$',X0)
| ~ $less(1,'of_nat$'(X1)) ) ),
inference(rectify,[],[f1619]) ).
tff(f1621,plain,
! [X0: 'Pratt_list$',X1: 'Nat$'] :
( ( ( ( ~ $less('of_nat$'(X1),1)
| 'member$'('triple$'(X1,sK44(X0,X1),'nat$'(0)),'set$'(X0)) )
& ( $less('of_nat$'(X1),1)
| 'member$'('triple$'(X1,sK44(X0,X1),'nat$'($sum('of_nat$'(X1),$uminus(1)))),'set$'(X0)) )
& ( 'fun_app$b'('cong$'('fun_app$d'('power$'(sK44(X0,X1)),'nat$'(0)),'nat$'(1)),X1)
| ~ $less('of_nat$'(X1),1) )
& ( $less('of_nat$'(X1),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(sK44(X0,X1)),'nat$'($sum('of_nat$'(X1),$uminus(1)))),'nat$'(1)),X1) )
& 'fun_app$e'('valid_cert$',X0)
& $less(1,'of_nat$'(X1)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X1),X0)) )
& ( 'fun_app$e'('valid_cert$','cons$'('prime$'(X1),X0))
| ! [X3: 'Nat$'] :
( ( $less('of_nat$'(X1),1)
& ~ 'member$'('triple$'(X1,X3,'nat$'(0)),'set$'(X0)) )
| ( ~ $less('of_nat$'(X1),1)
& ~ 'member$'('triple$'(X1,X3,'nat$'($sum('of_nat$'(X1),$uminus(1)))),'set$'(X0)) )
| ( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'(0)),'nat$'(1)),X1)
& $less('of_nat$'(X1),1) )
| ( ~ $less('of_nat$'(X1),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'($sum('of_nat$'(X1),$uminus(1)))),'nat$'(1)),X1) ) )
| ~ 'fun_app$e'('valid_cert$',X0)
| ~ $less(1,'of_nat$'(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X2,sK44(X0,X1))],[f1620]) ).
tff(f1794,plain,
! [X0: 'Nat$',X1: 'Pratt_list$',X2: 'Nat$',X3: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
| ~ $less(0,'of_nat$'(X2))
| ( ! [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) != 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
| ~ 'member$'('prime$'(X4),'set$'(X1))
| ~ 'member$'('triple$'(X0,X3,X5),'set$'(X1))
| ( ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
& ( 1 != 'of_nat$'(X2) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) )
& ( ( $less(0,'of_nat$'(X2))
& ( ? [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& 'member$'('prime$'(X4),'set$'(X1))
& 'member$'('triple$'(X0,X3,X5),'set$'(X1))
& ( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1)) ) ),
inference(nnf_transformation,[],[f1014]) ).
tff(f1795,plain,
! [X0: 'Nat$',X1: 'Pratt_list$',X2: 'Nat$',X3: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
| ~ $less(0,'of_nat$'(X2))
| ( ! [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) != 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
| ~ 'member$'('prime$'(X4),'set$'(X1))
| ~ 'member$'('triple$'(X0,X3,X5),'set$'(X1))
| ( ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
& ( 1 != 'of_nat$'(X2) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) )
& ( ( $less(0,'of_nat$'(X2))
& ( ? [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) = 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
& 'member$'('prime$'(X4),'set$'(X1))
& 'member$'('triple$'(X0,X3,X5),'set$'(X1))
& ( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1)) ) ),
inference(flattening,[],[f1794]) ).
tff(f1796,plain,
! [X0: 'Nat$',X1: 'Pratt_list$',X2: 'Nat$',X3: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
| ~ $less(0,'of_nat$'(X2))
| ( ! [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) != 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
| ~ 'member$'('prime$'(X4),'set$'(X1))
| ~ 'member$'('triple$'(X0,X3,X5),'set$'(X1))
| ( ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
& ( 1 != 'of_nat$'(X2) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) )
& ( ( $less(0,'of_nat$'(X2))
& ( ? [X6: 'Nat$',X7: 'Nat$'] :
( ( 'of_nat$'(X2) = 'times$'('of_nat$'(X6),'of_nat$'(X7)) )
& 'member$'('prime$'(X6),'set$'(X1))
& 'member$'('triple$'(X0,X3,X7),'set$'(X1))
& ( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X6)))),'nat$'(1)),X0) )
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X6)))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1)) ) ),
inference(rectify,[],[f1795]) ).
tff(f1797,plain,
! [X0: 'Nat$',X1: 'Pratt_list$',X2: 'Nat$',X3: 'Nat$'] :
( ( 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
| ~ $less(0,'of_nat$'(X2))
| ( ! [X4: 'Nat$',X5: 'Nat$'] :
( ( 'of_nat$'(X2) != 'times$'('of_nat$'(X4),'of_nat$'(X5)) )
| ~ 'member$'('prime$'(X4),'set$'(X1))
| ~ 'member$'('triple$'(X0,X3,X5),'set$'(X1))
| ( ( $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0) )
& ( ~ $less('of_nat$'(X0),1)
| 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0) ) ) )
& ( 1 != 'of_nat$'(X2) ) )
| ~ 'fun_app$e'('valid_cert$',X1)
| ~ $less(1,'of_nat$'(X0)) )
& ( ( $less(0,'of_nat$'(X2))
& ( ( ( 'of_nat$'(X2) = 'times$'('of_nat$'(sK91(X0,X1,X2,X3)),'of_nat$'(sK92(X0,X1,X2,X3))) )
& 'member$'('prime$'(sK91(X0,X1,X2,X3)),'set$'(X1))
& 'member$'('triple$'(X0,X3,sK92(X0,X1,X2,X3)),'set$'(X1))
& ( ( ~ $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(sK91(X0,X1,X2,X3))))),'nat$'(1)),X0) )
| ( $less('of_nat$'(X0),1)
& ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X3),'nat$'('fun_app$'('divide$'(0),'of_nat$'(sK91(X0,X1,X2,X3))))),'nat$'(1)),X0) ) ) )
| ( 'of_nat$'(X2) = 1 ) )
& 'fun_app$e'('valid_cert$',X1)
& $less(1,'of_nat$'(X0)) )
| ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91,sK92]),skolemize(X6,sK91(X0,X1,X2,X3)),skolemize(X7,sK92(X0,X1,X2,X3))],[f1796]) ).
tff(f1822,plain,
! [X0: 'Pratt$'] :
( ( 'triple$'(sK3(X0),sK4(X0),sK5(X0)) = X0 )
| ( 'prime$'(sK6(X0)) = X0 ) ),
inference(cnf_transformation,[],[f1373]) ).
tff(f2037,plain,
( ( 'ta$' = 'triple$'('pa$','aa$','xa$') )
| ( 'ta$' = 'prime$'('pa$') ) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2038,plain,
( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ $less('of_nat$'('pa$'),1)
| ( 'ta$' = 'prime$'('pa$') )
| ~ $less(0,'of_nat$'('xa$')) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2039,plain,
( ( 'ta$' = 'prime$'('pa$') )
| 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ $less(0,'of_nat$'('xa$'))
| $less('of_nat$'('pa$'),1) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2040,plain,
( 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') ) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2041,plain,
( ( 'ta$' = 'triple$'('pa$','aa$','xa$') )
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2042,plain,
( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'(0),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ 'fun_app$b'('prime$a','pa$')
| ~ $less(0,'of_nat$'('xa$'))
| ~ $less('of_nat$'('pa$'),1) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2043,plain,
( $less('of_nat$'('pa$'),1)
| ~ $less(0,'of_nat$'('xa$'))
| 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),$uminus(1))),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2044,plain,
( 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ $less(0,'of_nat$'('xa$')) ),
inference(cnf_transformation,[],[f1489]) ).
tff(f2156,plain,
'fun_app$e'('valid_cert$','cons$'('y$','ys$')),
inference(cnf_transformation,[],[f201]) ).
tff(f2260,plain,
! [X2: 'Nat$',X3: 'Pratt$',X0: 'Nat$',X1: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'triple$'(X0,X1,X2) != X3 )
| $less(0,'of_nat$'(X2))
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(cnf_transformation,[],[f1613]) ).
tff(f2262,plain,
! [X2: 'Nat$',X3: 'Pratt$',X0: 'Nat$',X1: 'Nat$',X4: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'triple$'(X0,X1,X2) != X3 )
| ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0)
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2)))
| $less('of_nat$'(X0),1)
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(cnf_transformation,[],[f1613]) ).
tff(f2263,plain,
! [X2: 'Nat$',X3: 'Pratt$',X0: 'Nat$',X1: 'Nat$',X4: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'triple$'(X0,X1,X2) != X3 )
| ~ $less('of_nat$'(X0),1)
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2)))
| ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0)
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(cnf_transformation,[],[f1613]) ).
tff(f2265,plain,
! [X3: 'Pratt$',X0: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| 'fun_app$b'('prime$a',X0)
| ( 'prime$'(X0) != X3 )
| ~ 'member$'(X3,'set$'('ys$')) ),
inference(cnf_transformation,[],[f1613]) ).
tff(f2290,plain,
! [X0: 'Pratt_list$',X1: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X1),X0))
| 'fun_app$e'('valid_cert$',X0) ),
inference(cnf_transformation,[],[f1621]) ).
tff(f2350,plain,
'member$'('ta$','set$'('ys$')),
inference(cnf_transformation,[],[f101]) ).
tff(f2757,plain,
! [X2: 'Nat$',X3: 'Nat$',X0: 'Nat$',X1: 'Pratt_list$'] :
( ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X3,X2),X1))
| 'fun_app$e'('valid_cert$',X1) ),
inference(cnf_transformation,[],[f1797]) ).
tff(f2822,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('prime$'(X0),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| 'fun_app$b'('prime$a',X0) ),
inference(equality_resolution,[],[f2265]) ).
tff(f2824,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$',X4: 'Nat$'] :
( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'(0),'of_nat$'(X4)))),'nat$'(1)),X0)
| ~ 'member$'('triple$'(X0,X1,X2),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less('of_nat$'(X0),1)
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2))) ),
inference(equality_resolution,[],[f2263]) ).
tff(f2825,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$',X4: 'Nat$'] :
( $less('of_nat$'(X0),1)
| ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),$uminus(1))),'of_nat$'(X4)))),'nat$'(1)),X0)
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'('triple$'(X0,X1,X2),'set$'('ys$'))
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2))) ),
inference(equality_resolution,[],[f2262]) ).
tff(f2827,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$'] :
( ~ 'member$'('triple$'(X0,X1,X2),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| $less(0,'of_nat$'(X2)) ),
inference(equality_resolution,[],[f2260]) ).
tff(f2947,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$',X4: 'Nat$'] :
( ~ 'fun_app$b'('cong$'('fun_app$d'('power$'(X1),'nat$'('fun_app$'('divide$'($sum('of_nat$'(X0),-1)),'of_nat$'(X4)))),'nat$'(1)),X0)
| $less('of_nat$'(X0),1)
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'('triple$'(X0,X1,X2),'set$'('ys$'))
| ~ 'member$a'(X4,'set_mset$'('prime_factorization$'(X2))) ),
inference(evaluation,[],[f2825]) ).
tff(f3050,plain,
( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),-1)),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ 'fun_app$b'('prime$a','pa$')
| ~ $less(0,'of_nat$'('xa$'))
| $less('of_nat$'('pa$'),1) ),
inference(evaluation,[],[f2043]) ).
tff(f3051,plain,
( 'fun_app$b'('cong$'('fun_app$d'('power$'('aa$'),'nat$'('fun_app$'('divide$'($sum('of_nat$'('pa$'),-1)),'of_nat$'(sK27)))),'nat$'(1)),'pa$')
| ~ $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') )
| $less('of_nat$'('pa$'),1) ),
inference(evaluation,[],[f2039]) ).
tff(f3074,plain,
( ~ 'member$'('ta$','set$'('ys$'))
| $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(constrained_superposition,[],[f2827,f2041]) ).
tff(f3075,plain,
( $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(forward_subsumption_resolution,[],[f3074,f2350]) ).
tff(f3099,plain,
( ~ 'fun_app$e'('valid_cert$','ys$')
| $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$'('ta$','set$'('ys$')) ),
inference(constrained_superposition,[],[f2827,f2037]) ).
tff(f3102,plain,
( $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f3099,f2350]) ).
tff(f3119,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ $less(0,'of_nat$'('xa$'))
| ~ $less('of_nat$'('pa$'),1)
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less('of_nat$'('pa$'),1)
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(resolution,[],[f2042,f2824]) ).
tff(f3137,plain,
! [X0: 'Nat$'] :
( ~ $less(0,'of_nat$'('xa$'))
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less('of_nat$'('pa$'),1)
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0))) ),
inference(duplicate_literal_removal,[],[f3119]) ).
tff(f3140,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less('of_nat$'('pa$'),1) ),
inference(forward_subsumption_resolution,[],[f3137,f3075]) ).
tff(f3148,plain,
! [X0: 'Nat$'] :
( ~ $less('of_nat$'('pa$'),1)
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ $less('of_nat$'('pa$'),1)
| ( 'ta$' = 'prime$'('pa$') ) ),
inference(resolution,[],[f2038,f2824]) ).
tff(f3166,plain,
! [X0: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ $less('of_nat$'('pa$'),1) ),
inference(duplicate_literal_removal,[],[f3148]) ).
tff(f3168,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ $less('of_nat$'('pa$'),1)
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f3166,f3102]) ).
tff(f3186,plain,
! [X0: 'Nat$'] :
( ~ $less(0,'of_nat$'('xa$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| $less('of_nat$'('pa$'),1)
| $less('of_nat$'('pa$'),1) ),
inference(resolution,[],[f3050,f2947]) ).
tff(f3209,plain,
! [X0: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| $less('of_nat$'('pa$'),1)
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(duplicate_literal_removal,[],[f3186]) ).
tff(f3212,plain,
! [X0: 'Nat$'] :
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(forward_subsumption_resolution,[],[f3209,f3140]) ).
tff(f3219,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0))) ),
inference(forward_subsumption_resolution,[],[f3212,f3075]) ).
tff(f3229,plain,
! [X0: 'Nat$'] :
( ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| $less('of_nat$'('pa$'),1)
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ $less(0,'of_nat$'('xa$'))
| $less('of_nat$'('pa$'),1) ),
inference(resolution,[],[f3051,f2947]) ).
tff(f3252,plain,
! [X0: 'Nat$'] :
( ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| $less('of_nat$'('pa$'),1)
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$')) ),
inference(duplicate_literal_removal,[],[f3229]) ).
tff(f3259,plain,
! [X0: 'Nat$'] :
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ $less(0,'of_nat$'('xa$'))
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$')) ),
inference(forward_subsumption_resolution,[],[f3252,f3168]) ).
tff(f3265,plain,
! [X0: 'Nat$'] :
( ~ 'member$'('triple$'('pa$','aa$',X0),'set$'('ys$'))
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'(X0)))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'ta$' = 'prime$'('pa$') ) ),
inference(forward_subsumption_resolution,[],[f3259,f3102]) ).
tff(f4939,plain,
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ 'member$'('ta$','set$'('ys$'))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(constrained_superposition,[],[f3219,f2041]) ).
tff(f4940,plain,
( ~ 'member$'('ta$','set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$'))) ),
inference(duplicate_literal_removal,[],[f4939]) ).
tff(f4943,plain,
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$b'('prime$a','pa$') ),
inference(forward_subsumption_resolution,[],[f4940,f2350]) ).
tff(f4975,plain,
( ( 'ta$' = 'prime$'('pa$') )
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ 'member$'('ta$','set$'('ys$')) ),
inference(constrained_superposition,[],[f3265,f2037]) ).
tff(f4977,plain,
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'member$'('ta$','set$'('ys$')) ),
inference(duplicate_literal_removal,[],[f4975]) ).
tff(f4979,plain,
( ~ 'member$a'(sK27,'set_mset$'('prime_factorization$'('xa$')))
| ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f4977,f2350]) ).
tff(f5013,plain,
( ~ 'fun_app$b'('prime$a','pa$')
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(resolution,[],[f4943,f2044]) ).
tff(f5016,plain,
( ~ 'fun_app$b'('prime$a','pa$')
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(duplicate_literal_removal,[],[f5013]) ).
tff(f5020,plain,
( ~ 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f5016,f3075]) ).
tff(f5294,plain,
( ( 'ta$' = 'prime$'('pa$') )
| ~ $less(0,'of_nat$'('xa$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ( 'ta$' = 'prime$'('pa$') ) ),
inference(resolution,[],[f4979,f2040]) ).
tff(f5298,plain,
( ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ $less(0,'of_nat$'('xa$')) ),
inference(duplicate_literal_removal,[],[f5294]) ).
tff(f5300,plain,
( ( 'ta$' = 'prime$'('pa$') )
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f5298,f3102]) ).
tff(f5326,plain,
( 'fun_app$b'('prime$a','pa$')
| ~ 'member$'('ta$','set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$')
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(constrained_superposition,[],[f2822,f5300]) ).
tff(f5328,plain,
( ~ 'member$'('ta$','set$'('ys$'))
| 'fun_app$b'('prime$a','pa$')
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(duplicate_literal_removal,[],[f5326]) ).
tff(f5331,plain,
( ~ 'member$'('ta$','set$'('ys$'))
| ~ 'fun_app$e'('valid_cert$','ys$') ),
inference(forward_subsumption_resolution,[],[f5328,f5020]) ).
tff(f5332,plain,
~ 'fun_app$e'('valid_cert$','ys$'),
inference(forward_subsumption_resolution,[],[f5331,f2350]) ).
tff(f5367,plain,
! [X0: 'Nat$'] : ~ 'fun_app$e'('valid_cert$','cons$'('prime$'(X0),'ys$')),
inference(unit_resulting_resolution,[],[f2290,f5332]) ).
tff(f5368,plain,
! [X2: 'Nat$',X0: 'Nat$',X1: 'Nat$'] : ~ 'fun_app$e'('valid_cert$','cons$'('triple$'(X0,X1,X2),'ys$')),
inference(unit_resulting_resolution,[],[f2757,f5332]) ).
tff(f5426,plain,
! [X0: 'Pratt$'] :
( ~ 'fun_app$e'('valid_cert$','cons$'(X0,'ys$'))
| ( 'prime$'(sK6(X0)) = X0 ) ),
inference(constrained_superposition,[],[f5368,f1822]) ).
tff(f5591,plain,
'y$' = 'prime$'(sK6('y$')),
inference(resolution,[],[f5426,f2156]) ).
tff(f6562,plain,
~ 'fun_app$e'('valid_cert$','cons$'('y$','ys$')),
inference(constrained_superposition,[],[f5367,f5591]) ).
tff(f6565,plain,
$false,
inference(forward_subsumption_resolution,[],[f6562,f2156]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP378_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.45 % Computer : n011.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 27 12:56:15 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.51 Running first-order theorem proving
% 0.22/0.51 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
% 5.41/1.94 % (2377129)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.41/1.94 % (2377135)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=245024642:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.41/1.94 % (2377138)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3528928404:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.41/1.94 % (2377134)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1595821261:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.41/1.94 % (2377136)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1165935775:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.41/1.94 % (2377138)Instruction limit reached!
% 5.41/1.94 % (2377138)------------------------------
% 5.41/1.94 % (2377138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.94 % (2377138)CaDiCaL version: 2.1.3
% 5.41/1.94 % (2377138)Termination reason: Instruction limit
% 5.41/1.94 % (2377138)Termination phase: Property scanning
% 5.41/1.94 % (2377138)Time elapsed: 0.005 s
% 5.41/1.94 % (2377138)Peak memory usage: 86 MB
% 5.41/1.94 % (2377138)Instructions burned: 4 (million)
% 5.41/1.94 % (2377134)Instruction limit reached!
% 5.41/1.94 % (2377134)------------------------------
% 5.41/1.94 % (2377134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.94 % (2377134)CaDiCaL version: 2.1.3
% 5.41/1.94 % (2377134)Termination reason: Instruction limit
% 5.41/1.94 % (2377134)Termination phase: shuffling
% 5.41/1.94 % (2377134)Time elapsed: 0.013 s
% 5.41/1.94 % (2377134)Peak memory usage: 86 MB
% 5.41/1.94 % (2377134)Instructions burned: 13 (million)
% 5.41/1.94 % (2377139)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1602528141:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.41/1.94 % (2377137)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2288902885:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.41/1.94 % (2377137)Instruction limit reached!
% 5.41/1.94 % (2377137)------------------------------
% 5.41/1.94 % (2377137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.94 % (2377137)CaDiCaL version: 2.1.3
% 5.41/1.94 % (2377137)Termination reason: Instruction limit
% 5.41/1.94 % (2377137)Termination phase: Property scanning
% 5.41/1.94 % (2377137)Time elapsed: 0.008 s
% 5.41/1.94 % (2377137)Peak memory usage: 86 MB
% 5.41/1.94 % (2377137)Instructions burned: 7 (million)
% 5.41/1.94 % (2377140)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3978360652:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.41/1.94 % (2377139)Instruction limit reached!
% 5.41/1.94 % (2377139)------------------------------
% 5.41/1.94 % (2377139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.94 % (2377139)CaDiCaL version: 2.1.3
% 5.41/1.94 % (2377139)Termination reason: Instruction limit
% 5.41/1.94 % (2377139)Termination phase: Property scanning
% 5.41/1.94 % (2377139)Time elapsed: 0.043 s
% 5.41/1.94 % (2377139)Peak memory usage: 88 MB
% 5.41/1.94 % (2377139)Instructions burned: 47 (million)
% 5.41/1.94 % (2377140)Instruction limit reached!
% 5.41/1.94 % (2377140)------------------------------
% 5.41/1.94 % (2377140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.94 % (2377140)CaDiCaL version: 2.1.3
% 5.41/1.94 % (2377140)Termination reason: Instruction limit
% 5.41/1.94 % (2377140)Termination phase: Preprocessing 3
% 5.41/1.94 % (2377140)Time elapsed: 0.033 s
% 5.41/1.94 % (2377140)Peak memory usage: 88 MB
% 5.41/1.94 % (2377140)Instructions burned: 34 (million)
% 5.41/1.94 % (2377135)Instruction limit reached!
% 5.41/1.94 % (2377135)------------------------------
% 5.41/1.94 % (2377135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.94 % (2377135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377135)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377135)Termination reason: Instruction limit
% 8.06/2.21 % (2377135)Termination phase: Property scanning
% 8.06/2.21 % (2377135)Time elapsed: 0.128 s
% 8.06/2.21 % (2377135)Peak memory usage: 88 MB
% 8.06/2.21 % (2377135)Instructions burned: 310 (million)
% 8.06/2.21 % (2377136)Instruction limit reached!
% 8.06/2.21 % (2377136)------------------------------
% 8.06/2.21 % (2377136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.21 % (2377136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377136)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377136)Termination reason: Instruction limit
% 8.06/2.21 % (2377136)Termination phase: Saturation
% 8.06/2.21 % (2377136)Time elapsed: 0.229 s
% 8.06/2.21 % (2377136)Peak memory usage: 118 MB
% 8.06/2.21 % (2377136)Instructions burned: 201 (million)
% 8.06/2.21 % (2377153)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=493879157:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 8.06/2.21 % (2377145)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2884531921:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2996 on theBenchmark for (2996ds/14Mi)
% 8.06/2.21 % (2377150)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3399196488:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 8.06/2.21 % (2377148)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=351459675:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2996 on theBenchmark for (2996ds/29Mi)
% 8.06/2.21 % (2377145)Instruction limit reached!
% 8.06/2.21 % (2377145)------------------------------
% 8.06/2.21 % (2377145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.21 % (2377145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377145)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377145)Termination reason: Instruction limit
% 8.06/2.21 % (2377145)Termination phase: SInE selection
% 8.06/2.21 % (2377145)Time elapsed: 0.014 s
% 8.06/2.21 % (2377145)Peak memory usage: 86 MB
% 8.06/2.21 % (2377145)Instructions burned: 14 (million)
% 8.06/2.21 % (2377150)Instruction limit reached!
% 8.06/2.21 % (2377150)------------------------------
% 8.06/2.21 % (2377150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.21 % (2377150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377150)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377150)Termination reason: Instruction limit
% 8.06/2.21 % (2377150)Termination phase: Preprocessing 1
% 8.06/2.21 % (2377150)Time elapsed: 0.016 s
% 8.06/2.21 % (2377150)Peak memory usage: 86 MB
% 8.06/2.21 % (2377150)Instructions burned: 16 (million)
% 8.06/2.21 % (2377153)Instruction limit reached!
% 8.06/2.21 % (2377153)------------------------------
% 8.06/2.21 % (2377153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.21 % (2377153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377153)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377153)Termination reason: Instruction limit
% 8.06/2.21 % (2377153)Termination phase: Equality resolution with deletion
% 8.06/2.21 % (2377153)Time elapsed: 0.051 s
% 8.06/2.21 % (2377153)Peak memory usage: 88 MB
% 8.06/2.21 % (2377153)Instructions burned: 86 (million)
% 8.06/2.21 % (2377148)Instruction limit reached!
% 8.06/2.21 % (2377148)------------------------------
% 8.06/2.21 % (2377148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.06/2.21 % (2377148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.06/2.21 % (2377148)CaDiCaL version: 2.1.3
% 8.06/2.21 % (2377148)Termination reason: Instruction limit
% 8.06/2.21 % (2377148)Termination phase: Preprocessing 2
% 8.06/2.21 % (2377148)Time elapsed: 0.028 s
% 8.06/2.21 % (2377148)Peak memory usage: 86 MB
% 8.06/2.21 % (2377148)Instructions burned: 29 (million)
% 8.06/2.21 % (2377151)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=211320895:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 8.06/2.21 % (2377152)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=1051519188:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 8.06/2.21 % (2377151)Instruction limit reached!
% 8.76/2.49 % (2377151)------------------------------
% 8.76/2.49 % (2377151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377151)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377151)Termination reason: Instruction limit
% 8.76/2.49 % (2377151)Termination phase: Preprocessing 1
% 8.76/2.49 % (2377151)Time elapsed: 0.021 s
% 8.76/2.49 % (2377151)Peak memory usage: 86 MB
% 8.76/2.49 % (2377151)Instructions burned: 24 (million)
% 8.76/2.49 % (2377152)Instruction limit reached!
% 8.76/2.49 % (2377152)------------------------------
% 8.76/2.49 % (2377152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377152)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377152)Termination reason: Instruction limit
% 8.76/2.49 % (2377152)Termination phase: Preprocessing 1
% 8.76/2.49 % (2377152)Time elapsed: 0.025 s
% 8.76/2.49 % (2377152)Peak memory usage: 86 MB
% 8.76/2.49 % (2377152)Instructions burned: 27 (million)
% 8.76/2.49 % (2377155)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2927577852:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2994 on theBenchmark for (2994ds/2Mi)
% 8.76/2.49 % (2377155)Instruction limit reached!
% 8.76/2.49 % (2377155)------------------------------
% 8.76/2.49 % (2377155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377155)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377155)Termination reason: Instruction limit
% 8.76/2.49 % (2377155)Termination phase: shuffling
% 8.76/2.49 % (2377155)Time elapsed: 0.003 s
% 8.76/2.49 % (2377155)Peak memory usage: 85 MB
% 8.76/2.49 % (2377155)Instructions burned: 2 (million)
% 8.76/2.49 % (2377162)lrs+10_1_thi=all:si=on:fd=off:random_seed=3679193789:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 8.76/2.49 % (2377159)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3476571209:i=181:rtra=on:ss=axioms:ev=cautious_2993 on theBenchmark for (2993ds/181Mi)
% 8.76/2.49 % (2377162)Instruction limit reached!
% 8.76/2.49 % (2377162)------------------------------
% 8.76/2.49 % (2377162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377162)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377162)Termination reason: Instruction limit
% 8.76/2.49 % (2377162)Termination phase: Naming
% 8.76/2.49 % (2377162)Time elapsed: 0.026 s
% 8.76/2.49 % (2377162)Peak memory usage: 87 MB
% 8.76/2.49 % (2377162)Instructions burned: 55 (million)
% 8.76/2.49 % (2377160)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1511625800:i=4:ep=RST:ins=2:rtra=on_2993 on theBenchmark for (2993ds/4Mi)
% 8.76/2.49 % (2377161)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3425725408:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi)
% 8.76/2.49 % (2377160)Instruction limit reached!
% 8.76/2.49 % (2377160)------------------------------
% 8.76/2.49 % (2377160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377160)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377160)Termination reason: Instruction limit
% 8.76/2.49 % (2377160)Termination phase: Property scanning
% 8.76/2.49 % (2377160)Time elapsed: 0.005 s
% 8.76/2.49 % (2377160)Peak memory usage: 85 MB
% 8.76/2.49 % (2377160)Instructions burned: 4 (million)
% 8.76/2.49 % (2377165)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=1330085789:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 8.76/2.49 % (2377165)Instruction limit reached!
% 8.76/2.49 % (2377165)------------------------------
% 8.76/2.49 % (2377165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.49 % (2377165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.49 % (2377165)CaDiCaL version: 2.1.3
% 8.76/2.49 % (2377165)Termination reason: Instruction limit
% 8.76/2.49 % (2377165)Termination phase: Property scanning
% 8.76/2.49 % (2377165)Time elapsed: 0.008 s
% 8.76/2.49 % (2377165)Peak memory usage: 85 MB
% 10.49/2.78 % (2377165)Instructions burned: 8 (million)
% 10.49/2.78 % (2377161)Instruction limit reached!
% 10.49/2.78 % (2377161)------------------------------
% 10.49/2.78 % (2377161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377161)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377161)Termination reason: Instruction limit
% 10.49/2.78 % (2377161)Termination phase: shuffling
% 10.49/2.78 % (2377161)Time elapsed: 0.060 s
% 10.49/2.78 % (2377161)Peak memory usage: 88 MB
% 10.49/2.78 % (2377161)Instructions burned: 66 (million)
% 10.49/2.78 % (2377166)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2318836363:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 10.49/2.78 % (2377166)Instruction limit reached!
% 10.49/2.78 % (2377166)------------------------------
% 10.49/2.78 % (2377166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377166)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377166)Termination reason: Instruction limit
% 10.49/2.78 % (2377166)Termination phase: shuffling
% 10.49/2.78 % (2377166)Time elapsed: 0.004 s
% 10.49/2.78 % (2377166)Peak memory usage: 85 MB
% 10.49/2.78 % (2377166)Instructions burned: 2 (million)
% 10.49/2.78 % (2377168)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=1488753217:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.49/2.78 % (2377168)Instruction limit reached!
% 10.49/2.78 % (2377168)------------------------------
% 10.49/2.78 % (2377168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377168)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377168)Termination reason: Instruction limit
% 10.49/2.78 % (2377168)Termination phase: Property scanning
% 10.49/2.78 % (2377168)Time elapsed: 0.005 s
% 10.49/2.78 % (2377168)Peak memory usage: 86 MB
% 10.49/2.78 % (2377168)Instructions burned: 4 (million)
% 10.49/2.78 % (2377159)Instruction limit reached!
% 10.49/2.78 % (2377159)------------------------------
% 10.49/2.78 % (2377159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377159)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377159)Termination reason: Instruction limit
% 10.49/2.78 % (2377159)Termination phase: Saturation
% 10.49/2.78 % (2377159)Time elapsed: 0.197 s
% 10.49/2.78 % (2377159)Peak memory usage: 92 MB
% 10.49/2.78 % (2377159)Instructions burned: 181 (million)
% 10.49/2.78 % (2377174)dis+10_1_si=on:random_seed=915325655:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.49/2.78 % (2377171)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3792846097:i=127:doe=on:rtra=on_2991 on theBenchmark for (2991ds/127Mi)
% 10.49/2.78 % (2377174)Instruction limit reached!
% 10.49/2.78 % (2377174)------------------------------
% 10.49/2.78 % (2377174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377174)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377174)Termination reason: Instruction limit
% 10.49/2.78 % (2377174)Termination phase: Property scanning
% 10.49/2.78 % (2377174)Time elapsed: 0.006 s
% 10.49/2.78 % (2377174)Peak memory usage: 86 MB
% 10.49/2.78 % (2377174)Instructions burned: 13 (million)
% 10.49/2.78 % (2377176)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2510780473:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 10.49/2.78 % (2377176)Instruction limit reached!
% 10.49/2.78 % (2377176)------------------------------
% 10.49/2.78 % (2377176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.49/2.78 % (2377176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.49/2.78 % (2377176)CaDiCaL version: 2.1.3
% 10.49/2.78 % (2377176)Termination reason: Instruction limit
% 10.49/2.78 % (2377176)Termination phase: Preprocessing 1
% 10.49/2.78 % (2377176)Time elapsed: 0.025 s
% 10.49/2.78 % (2377176)Peak memory usage: 86 MB
% 10.49/2.78 % (2377176)Instructions burned: 26 (million)
% 10.49/2.78 % (2377177)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=804247011:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi)
% 15.29/3.21 % (2377179)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=284371961:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 15.29/3.21 % (2377179)Instruction limit reached!
% 15.29/3.21 % (2377179)------------------------------
% 15.29/3.21 % (2377179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377179)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377179)Termination reason: Instruction limit
% 15.29/3.21 % (2377179)Termination phase: shuffling
% 15.29/3.21 % (2377179)Time elapsed: 0.004 s
% 15.29/3.21 % (2377179)Peak memory usage: 85 MB
% 15.29/3.21 % (2377179)Instructions burned: 2 (million)
% 15.29/3.21 % (2377182)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2570304813:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 15.29/3.21 % (2377177)Instruction limit reached!
% 15.29/3.21 % (2377177)------------------------------
% 15.29/3.21 % (2377177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377177)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377177)Termination reason: Instruction limit
% 15.29/3.21 % (2377177)Termination phase: Preprocessing 3
% 15.29/3.21 % (2377177)Time elapsed: 0.036 s
% 15.29/3.21 % (2377177)Peak memory usage: 88 MB
% 15.29/3.21 % (2377177)Instructions burned: 36 (million)
% 15.29/3.21 % (2377171)Instruction limit reached!
% 15.29/3.21 % (2377171)------------------------------
% 15.29/3.21 % (2377171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377171)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377171)Termination reason: Instruction limit
% 15.29/3.21 % (2377171)Termination phase: Saturation
% 15.29/3.21 % (2377171)Time elapsed: 0.152 s
% 15.29/3.21 % (2377171)Peak memory usage: 115 MB
% 15.29/3.21 % (2377171)Instructions burned: 128 (million)
% 15.29/3.21 % (2377181)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3294668674:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 15.29/3.21 % (2377181)Instruction limit reached!
% 15.29/3.21 % (2377181)------------------------------
% 15.29/3.21 % (2377181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377181)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377181)Termination reason: Instruction limit
% 15.29/3.21 % (2377181)Termination phase: Property scanning
% 15.29/3.21 % (2377181)Time elapsed: 0.009 s
% 15.29/3.21 % (2377181)Peak memory usage: 86 MB
% 15.29/3.21 % (2377181)Instructions burned: 9 (million)
% 15.29/3.21 % (2377185)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2959481153:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 15.29/3.21 % (2377185)Instruction limit reached!
% 15.29/3.21 % (2377185)------------------------------
% 15.29/3.21 % (2377185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377185)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377185)Termination reason: Instruction limit
% 15.29/3.21 % (2377185)Termination phase: Property scanning
% 15.29/3.21 % (2377185)Time elapsed: 0.012 s
% 15.29/3.21 % (2377185)Peak memory usage: 85 MB
% 15.29/3.21 % (2377185)Instructions burned: 13 (million)
% 15.29/3.21 % (2377187)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4101255267:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 15.29/3.21 % (2377182)Instruction limit reached!
% 15.29/3.21 % (2377182)------------------------------
% 15.29/3.21 % (2377182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.29/3.21 % (2377182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.29/3.21 % (2377182)CaDiCaL version: 2.1.3
% 15.29/3.21 % (2377182)Termination reason: Instruction limit
% 15.29/3.21 % (2377182)Termination phase: Saturation
% 15.29/3.21 % (2377182)Time elapsed: 0.253 s
% 15.29/3.21 % (2377182)Peak memory usage: 94 MB
% 15.29/3.21 % (2377182)Instructions burned: 370 (million)
% 16.06/3.50 % (2377193)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=4087057394:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 16.06/3.50 % (2377191)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=926988734:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 16.06/3.50 % (2377192)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3242175954:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 16.06/3.50 % (2377191)Instruction limit reached!
% 16.06/3.50 % (2377191)------------------------------
% 16.06/3.50 % (2377191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.06/3.50 % (2377191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/3.50 % (2377191)CaDiCaL version: 2.1.3
% 16.06/3.50 % (2377191)Termination reason: Instruction limit
% 16.06/3.50 % (2377191)Termination phase: Property scanning
% 16.06/3.50 % (2377191)Time elapsed: 0.010 s
% 16.06/3.50 % (2377191)Peak memory usage: 86 MB
% 16.06/3.50 % (2377191)Instructions burned: 10 (million)
% 16.06/3.50 % (2377195)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=4151188908:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 16.06/3.50 % (2377187)Instruction limit reached!
% 16.06/3.50 % (2377187)------------------------------
% 16.06/3.50 % (2377187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.06/3.50 % (2377187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/3.50 % (2377187)CaDiCaL version: 2.1.3
% 16.06/3.50 % (2377187)Termination reason: Instruction limit
% 16.06/3.50 % (2377187)Termination phase: Saturation
% 16.06/3.50 % (2377187)Time elapsed: 0.144 s
% 16.06/3.50 % (2377187)Peak memory usage: 119 MB
% 16.06/3.50 % (2377187)Instructions burned: 226 (million)
% 16.06/3.50 % (2377192)Instruction limit reached!
% 16.06/3.50 % (2377192)------------------------------
% 16.06/3.50 % (2377192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.06/3.50 % (2377192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/3.50 % (2377192)CaDiCaL version: 2.1.3
% 16.06/3.50 % (2377192)Termination reason: Instruction limit
% 16.06/3.50 % (2377192)Termination phase: Property scanning
% 16.06/3.50 % (2377192)Time elapsed: 0.066 s
% 16.06/3.50 % (2377192)Peak memory usage: 88 MB
% 16.06/3.50 % (2377192)Instructions burned: 71 (million)
% 16.06/3.50 % (2377193)Instruction limit reached!
% 16.06/3.50 % (2377193)------------------------------
% 16.06/3.50 % (2377193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.06/3.50 % (2377193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/3.50 % (2377193)CaDiCaL version: 2.1.3
% 16.06/3.50 % (2377193)Termination reason: Instruction limit
% 16.06/3.50 % (2377193)Termination phase: Property scanning
% 16.06/3.50 % (2377193)Time elapsed: 0.067 s
% 16.06/3.50 % (2377193)Peak memory usage: 88 MB
% 16.06/3.50 % (2377193)Instructions burned: 76 (million)
% 16.06/3.50 % (2377197)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=212882193:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/130Mi)
% 16.06/3.50 % (2377203)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2679792108:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 16.06/3.50 % (2377199)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3685133585:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 16.06/3.50 % (2377197)Instruction limit reached!
% 16.06/3.50 % (2377197)------------------------------
% 16.06/3.50 % (2377197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.06/3.50 % (2377197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.06/3.50 % (2377197)CaDiCaL version: 2.1.3
% 16.06/3.50 % (2377197)Termination reason: Instruction limit
% 16.06/3.50 % (2377197)Termination phase: Property scanning
% 16.06/3.50 % (2377197)Time elapsed: 0.108 s
% 16.06/3.50 % (2377197)Peak memory usage: 89 MB
% 16.06/3.50 % (2377197)Instructions burned: 130 (million)
% 16.06/3.50 % (2377205)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1972176321:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 16.06/3.50 % (2377203)Instruction limit reached!
% 21.45/4.07 % (2377203)------------------------------
% 21.45/4.07 % (2377203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.45/4.07 % (2377203)CaDiCaL version: 2.1.3
% 21.45/4.07 % (2377203)Termination reason: Instruction limit
% 21.45/4.07 % (2377203)Termination phase: Property scanning
% 21.45/4.07 % (2377203)Time elapsed: 0.035 s
% 21.45/4.07 % (2377203)Peak memory usage: 86 MB
% 21.45/4.07 % (2377203)Instructions burned: 41 (million)
% 21.45/4.07 % (2377195)Instruction limit reached!
% 21.45/4.07 % (2377195)------------------------------
% 21.45/4.07 % (2377195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.45/4.07 % (2377195)CaDiCaL version: 2.1.3
% 21.45/4.07 % (2377195)Termination reason: Instruction limit
% 21.45/4.07 % (2377195)Termination phase: Property scanning
% 21.45/4.07 % (2377195)Time elapsed: 0.232 s
% 21.45/4.07 % (2377195)Peak memory usage: 89 MB
% 21.45/4.07 % (2377195)Instructions burned: 295 (million)
% 21.45/4.07 % (2377206)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=172546040:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 21.45/4.07 % (2377207)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3426564680:i=131:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/131Mi)
% 21.45/4.07 % (2377199)Instruction limit reached!
% 21.45/4.07 % (2377199)------------------------------
% 21.45/4.07 % (2377199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.45/4.07 % (2377199)CaDiCaL version: 2.1.3
% 21.45/4.07 % (2377199)Termination reason: Instruction limit
% 21.45/4.07 % (2377199)Termination phase: Saturation
% 21.45/4.07 % (2377199)Time elapsed: 0.181 s
% 21.45/4.07 % (2377199)Peak memory usage: 132 MB
% 21.45/4.07 % (2377199)Instructions burned: 131 (million)
% 21.45/4.07 % (2377205)Instruction limit reached!
% 21.45/4.07 % (2377205)------------------------------
% 21.45/4.07 % (2377205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.45/4.07 % (2377205)CaDiCaL version: 2.1.3
% 21.45/4.07 % (2377205)Termination reason: Instruction limit
% 21.45/4.07 % (2377205)Termination phase: Saturation
% 21.45/4.07 % (2377205)Time elapsed: 0.168 s
% 21.45/4.07 % (2377205)Peak memory usage: 93 MB
% 21.45/4.07 % (2377205)Instructions burned: 308 (million)
% 21.45/4.07 % (2377211)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=715589601:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2982 on theBenchmark for (2982ds/259Mi)
% 21.45/4.07 % (2377207)Instruction limit reached!
% 21.45/4.07 % (2377207)------------------------------
% 21.45/4.07 % (2377207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.45/4.07 % (2377207)CaDiCaL version: 2.1.3
% 21.45/4.07 % (2377207)Termination reason: Instruction limit
% 21.45/4.07 % (2377207)Termination phase: Saturation
% 21.45/4.07 % (2377207)Time elapsed: 0.157 s
% 21.45/4.07 % (2377207)Peak memory usage: 115 MB
% 21.45/4.07 % (2377207)Instructions burned: 134 (million)
% 21.45/4.07 % (2377213)dis+10_1_si=on:random_seed=222186091:s2a=on:i=1000:rtra=on:gtg=exists_all_2982 on theBenchmark for (2982ds/1000Mi)
% 21.45/4.07 % (2377214)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=150607636:i=383:fsr=off:rtra=on:ev=force_2982 on theBenchmark for (2982ds/383Mi)
% 21.45/4.07 % (2377217)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4169117615:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 21.45/4.07 % (2377218)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=249219143:i=65:nm=16:rtra=on_2980 on theBenchmark for (2980ds/65Mi)
% 21.45/4.07 % (2377218)Instruction limit reached!
% 21.45/4.07 % (2377218)------------------------------
% 21.45/4.07 % (2377218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.45/4.07 % (2377218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.53 % (2377218)CaDiCaL version: 2.1.3
% 22.58/4.53 % (2377218)Termination reason: Instruction limit
% 22.58/4.53 % (2377218)Termination phase: Property scanning
% 22.58/4.53 % (2377218)Time elapsed: 0.060 s
% 22.58/4.53 % (2377218)Peak memory usage: 89 MB
% 22.58/4.53 % (2377218)Instructions burned: 67 (million)
% 22.58/4.53 % (2377217)Instruction limit reached!
% 22.58/4.53 % (2377217)------------------------------
% 22.58/4.53 % (2377217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.53 % (2377217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.53 % (2377217)CaDiCaL version: 2.1.3
% 22.58/4.53 % (2377217)Termination reason: Instruction limit
% 22.58/4.53 % (2377217)Termination phase: Saturation
% 22.58/4.53 % (2377217)Time elapsed: 0.073 s
% 22.58/4.53 % (2377217)Peak memory usage: 91 MB
% 22.58/4.53 % (2377217)Instructions burned: 142 (million)
% 22.58/4.53 % (2377211)Instruction limit reached!
% 22.58/4.53 % (2377211)------------------------------
% 22.58/4.53 % (2377211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.53 % (2377211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.53 % (2377211)CaDiCaL version: 2.1.3
% 22.58/4.53 % (2377211)Termination reason: Instruction limit
% 22.58/4.53 % (2377211)Termination phase: Saturation
% 22.58/4.53 % (2377211)Time elapsed: 0.293 s
% 22.58/4.53 % (2377211)Peak memory usage: 118 MB
% 22.58/4.53 % (2377211)Instructions burned: 260 (million)
% 22.58/4.53 % (2377220)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1140647269:i=121:nm=16:rtra=on_2980 on theBenchmark for (2980ds/121Mi)
% 22.58/4.53 % (2377226)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=1311560826:i=39:ins=3:rtra=on_2978 on theBenchmark for (2978ds/39Mi)
% 22.58/4.53 % (2377225)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=828810336:s2a=on:i=128:s2at=5:ins=3:rtra=on_2978 on theBenchmark for (2978ds/128Mi)
% 22.58/4.53 % (2377226)Instruction limit reached!
% 22.58/4.53 % (2377226)------------------------------
% 22.58/4.53 % (2377226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.53 % (2377226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.54 % (2377226)CaDiCaL version: 2.1.3
% 22.58/4.54 % (2377226)Termination reason: Instruction limit
% 22.58/4.54 % (2377226)Termination phase: Preprocessing 3
% 22.58/4.54 % (2377226)Time elapsed: 0.022 s
% 22.58/4.54 % (2377226)Peak memory usage: 87 MB
% 22.58/4.54 % (2377226)Instructions burned: 40 (million)
% 22.58/4.54 % (2377220)Instruction limit reached!
% 22.58/4.54 % (2377220)------------------------------
% 22.58/4.54 % (2377220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.54 % (2377220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.54 % (2377220)CaDiCaL version: 2.1.3
% 22.58/4.54 % (2377220)Termination reason: Instruction limit
% 22.58/4.54 % (2377220)Termination phase: Saturation
% 22.58/4.54 % (2377220)Time elapsed: 0.113 s
% 22.58/4.54 % (2377220)Peak memory usage: 91 MB
% 22.58/4.54 % (2377220)Instructions burned: 122 (million)
% 22.58/4.54 % (2377214)Instruction limit reached!
% 22.58/4.54 % (2377214)------------------------------
% 22.58/4.54 % (2377214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.54 % (2377214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.54 % (2377214)CaDiCaL version: 2.1.3
% 22.58/4.54 % (2377214)Termination reason: Instruction limit
% 22.58/4.54 % (2377214)Termination phase: Saturation
% 22.58/4.54 % (2377214)Time elapsed: 0.396 s
% 22.58/4.54 % (2377214)Peak memory usage: 96 MB
% 22.58/4.54 % (2377214)Instructions burned: 383 (million)
% 22.58/4.54 % (2377225)Instruction limit reached!
% 22.58/4.54 % (2377225)------------------------------
% 22.58/4.54 % (2377225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.58/4.54 % (2377225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.58/4.54 % (2377225)CaDiCaL version: 2.1.3
% 22.58/4.54 % (2377225)Termination reason: Instruction limit
% 22.58/4.54 % (2377225)Termination phase: Saturation
% 22.58/4.54 % (2377225)Time elapsed: 0.085 s
% 22.58/4.54 % (2377225)Peak memory usage: 91 MB
% 22.58/4.54 % (2377225)Instructions burned: 128 (million)
% 22.58/4.54 % (2377206)Instruction limit reached!
% 22.58/4.54 % (2377206)------------------------------
% 22.58/4.54 % (2377206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377206)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377206)Termination reason: Instruction limit
% 24.95/4.89 % (2377206)Termination phase: Saturation
% 24.95/4.89 % (2377206)Time elapsed: 0.672 s
% 24.95/4.89 % (2377206)Peak memory usage: 138 MB
% 24.95/4.89 % (2377206)Instructions burned: 599 (million)
% 24.95/4.89 % (2377227)dis+1010_1_to=kbo:si=on:random_seed=1190913399:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2977 on theBenchmark for (2977ds/175Mi)
% 24.95/4.89 % (2377231)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1262021401:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2976 on theBenchmark for (2976ds/329Mi)
% 24.95/4.89 % (2377232)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=835076721:s2a=on:i=483:doe=on:nm=32:rtra=on_2975 on theBenchmark for (2975ds/483Mi)
% 24.95/4.89 % (2377233)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4217819:thitd=on:i=215:nm=0:rtra=on:ev=force_2975 on theBenchmark for (2975ds/215Mi)
% 24.95/4.89 % (2377227)Instruction limit reached!
% 24.95/4.89 % (2377227)------------------------------
% 24.95/4.89 % (2377227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377227)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377227)Termination reason: Instruction limit
% 24.95/4.89 % (2377227)Termination phase: Saturation
% 24.95/4.89 % (2377227)Time elapsed: 0.174 s
% 24.95/4.89 % (2377227)Peak memory usage: 92 MB
% 24.95/4.89 % (2377227)Instructions burned: 175 (million)
% 24.95/4.89 % (2377234)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3053342602:i=349:rtra=on_2975 on theBenchmark for (2975ds/349Mi)
% 24.95/4.89 % (2377231)Instruction limit reached!
% 24.95/4.89 % (2377231)------------------------------
% 24.95/4.89 % (2377231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377231)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377231)Termination reason: Instruction limit
% 24.95/4.89 % (2377231)Termination phase: Saturation
% 24.95/4.89 % (2377231)Time elapsed: 0.191 s
% 24.95/4.89 % (2377231)Peak memory usage: 120 MB
% 24.95/4.89 % (2377231)Instructions burned: 330 (million)
% 24.95/4.89 % (2377235)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=3036296516:st=2:i=295:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/295Mi)
% 24.95/4.89 % (2377233)Instruction limit reached!
% 24.95/4.89 % (2377233)------------------------------
% 24.95/4.89 % (2377233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377233)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377233)Termination reason: Instruction limit
% 24.95/4.89 % (2377233)Termination phase: Property scanning
% 24.95/4.89 % (2377233)Time elapsed: 0.169 s
% 24.95/4.89 % (2377233)Peak memory usage: 89 MB
% 24.95/4.89 % (2377233)Instructions burned: 215 (million)
% 24.95/4.89 % (2377246)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=878384192:i=281:gtgl=2:rtra=on:gtg=all_2972 on theBenchmark for (2972ds/281Mi)
% 24.95/4.89 % (2377242)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1008917281:i=328:kws=inv_frequency:nm=20:rtra=on_2972 on theBenchmark for (2972ds/328Mi)
% 24.95/4.89 % (2377213)Instruction limit reached!
% 24.95/4.89 % (2377213)------------------------------
% 24.95/4.89 % (2377213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377213)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377213)Termination reason: Instruction limit
% 24.95/4.89 % (2377213)Termination phase: Saturation
% 24.95/4.89 % (2377213)Time elapsed: 0.974 s
% 24.95/4.89 % (2377213)Peak memory usage: 98 MB
% 24.95/4.89 % (2377213)Instructions burned: 1000 (million)
% 24.95/4.89 % (2377246)Instruction limit reached!
% 24.95/4.89 % (2377246)------------------------------
% 24.95/4.89 % (2377246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377246)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377246)Termination reason: Instruction limit
% 24.95/4.89 % (2377246)Termination phase: Saturation
% 24.95/4.89 % (2377246)Time elapsed: 0.148 s
% 24.95/4.89 % (2377246)Peak memory usage: 118 MB
% 24.95/4.89 % (2377246)Instructions burned: 282 (million)
% 24.95/4.89 % (2377235)Instruction limit reached!
% 24.95/4.89 % (2377235)------------------------------
% 24.95/4.89 % (2377235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377235)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377235)Termination reason: Instruction limit
% 24.95/4.89 % (2377235)Termination phase: Saturation
% 24.95/4.89 % (2377235)Time elapsed: 0.289 s
% 24.95/4.89 % (2377235)Peak memory usage: 92 MB
% 24.95/4.89 % (2377235)Instructions burned: 295 (million)
% 24.95/4.89 % (2377234)Instruction limit reached!
% 24.95/4.89 % (2377234)------------------------------
% 24.95/4.89 % (2377234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377234)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377234)Termination reason: Instruction limit
% 24.95/4.89 % (2377234)Termination phase: Saturation
% 24.95/4.89 % (2377234)Time elapsed: 0.403 s
% 24.95/4.89 % (2377234)Peak memory usage: 120 MB
% 24.95/4.89 % (2377234)Instructions burned: 349 (million)
% 24.95/4.89 % (2377248)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2406703439:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2971 on theBenchmark for (2971ds/484Mi)
% 24.95/4.89 % (2377251)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1240778144:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2969 on theBenchmark for (2969ds/321Mi)
% 24.95/4.89 % (2377232)Instruction limit reached!
% 24.95/4.89 % (2377232)------------------------------
% 24.95/4.89 % (2377232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377232)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377232)Termination reason: Instruction limit
% 24.95/4.89 % (2377232)Termination phase: Saturation
% 24.95/4.89 % (2377232)Time elapsed: 0.543 s
% 24.95/4.89 % (2377232)Peak memory usage: 137 MB
% 24.95/4.89 % (2377232)Instructions burned: 484 (million)
% 24.95/4.89 % (2377252)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1935703024:i=416:rtra=on:gtg=position:ss=axioms_2969 on theBenchmark for (2969ds/416Mi)
% 24.95/4.89 % (2377242)Instruction limit reached!
% 24.95/4.89 % (2377242)------------------------------
% 24.95/4.89 % (2377242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377242)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377242)Termination reason: Instruction limit
% 24.95/4.89 % (2377242)Termination phase: Saturation
% 24.95/4.89 % (2377242)Time elapsed: 0.355 s
% 24.95/4.89 % (2377242)Peak memory usage: 119 MB
% 24.95/4.89 % (2377242)Instructions burned: 328 (million)
% 24.95/4.89 % (2377253)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=2949087199:i=471:thf=on:kws=precedence:rtra=on_2969 on theBenchmark for (2969ds/471Mi)
% 24.95/4.89 % (2377255)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1780921950:avsq=on:i=276:avsqr=1,2:rtra=on_2968 on theBenchmark for (2968ds/276Mi)
% 24.95/4.89 % (2377259)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=977912283:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/387Mi)
% 24.95/4.89 % (2377257)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=2674564398:i=375:kws=inv_arity_squared:rtra=on_2967 on theBenchmark for (2967ds/375Mi)
% 24.95/4.89 % (2377252)Instruction limit reached!
% 24.95/4.89 % (2377252)------------------------------
% 24.95/4.89 % (2377252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377252)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377252)Termination reason: Instruction limit
% 24.95/4.89 % (2377252)Termination phase: Saturation
% 24.95/4.89 % (2377252)Time elapsed: 0.254 s
% 24.95/4.89 % (2377252)Peak memory usage: 121 MB
% 24.95/4.89 % (2377252)Instructions burned: 417 (million)
% 24.95/4.89 % (2377251)Instruction limit reached!
% 24.95/4.89 % (2377251)------------------------------
% 24.95/4.89 % (2377251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377251)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377251)Termination reason: Instruction limit
% 24.95/4.89 % (2377251)Termination phase: Saturation
% 24.95/4.89 % (2377251)Time elapsed: 0.314 s
% 24.95/4.89 % (2377251)Peak memory usage: 120 MB
% 24.95/4.89 % (2377251)Instructions burned: 321 (million)
% 24.95/4.89 % (2377248)First to succeed.
% 24.95/4.89 % (2377248)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2377129"
% 24.95/4.89 % (2377259)Instruction limit reached!
% 24.95/4.89 % (2377259)------------------------------
% 24.95/4.89 % (2377259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377259)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377259)Termination reason: Instruction limit
% 24.95/4.89 % (2377259)Termination phase: Saturation
% 24.95/4.89 % (2377259)Time elapsed: 0.256 s
% 24.95/4.89 % (2377259)Peak memory usage: 120 MB
% 24.95/4.89 % (2377259)Instructions burned: 388 (million)
% 24.95/4.89 % (2377255)Instruction limit reached!
% 24.95/4.89 % (2377255)------------------------------
% 24.95/4.89 % (2377255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377255)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377255)Termination reason: Instruction limit
% 24.95/4.89 % (2377255)Termination phase: Saturation
% 24.95/4.89 % (2377255)Time elapsed: 0.333 s
% 24.95/4.89 % (2377255)Peak memory usage: 136 MB
% 24.95/4.89 % (2377255)Instructions burned: 276 (million)
% 24.95/4.89 % (2377265)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3199488835:i=334:rtra=on_2964 on theBenchmark for (2964ds/334Mi)
% 24.95/4.89 % (2377253)Instruction limit reached!
% 24.95/4.89 % (2377253)------------------------------
% 24.95/4.89 % (2377253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.95/4.89 % (2377253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.95/4.89 % (2377253)CaDiCaL version: 2.1.3
% 24.95/4.89 % (2377253)Termination reason: Instruction limit
% 24.95/4.89 % (2377253)Termination phase: Saturation
% 24.95/4.89 % (2377253)Time elapsed: 0.490 s
% 24.95/4.89 % (2377253)Peak memory usage: 121 MB
% 24.95/4.89 % (2377253)Instructions burned: 471 (million)
% 24.95/4.89 % (2377264)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=3360375725:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2964 on theBenchmark for (2964ds/513Mi)
% 24.95/4.89 % (2377248)Refutation found. Thanks to Tanya!
% 24.95/4.89 % SZS status Theorem for theBenchmark
% 24.95/4.89 % SZS output start Proof for theBenchmark
% See solution above
% 27.51/5.06 % (2377248)------------------------------
% 27.51/5.06 % (2377248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.51/5.06 % (2377248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.51/5.06 % (2377248)CaDiCaL version: 2.1.3
% 27.51/5.06 % (2377248)Termination reason: Refutation
% 27.51/5.06 % (2377248)Time elapsed: 0.405 s
% 27.51/5.06 % (2377248)Peak memory usage: 93 MB
% 27.51/5.06 % (2377248)Instructions burned: 433 (million)
% 27.51/5.06 % (2377248)------------------------------
% 27.51/5.06 % (2377248)------------------------------
% 27.51/5.06 % (2377129)Success in time 3.867 s
% 27.51/5.06 % Vampire exiting
%------------------------------------------------------------------------------