%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV829-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:26:30 PM UTC 2026
% Result : Unsatisfiable 10.96s 4.16s
% Output : Refutation 10.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 38
% Syntax : Number of formulae : 103 ( 88 unt; 20 def)
% Number of atoms : 118 ( 74 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 32 ( 17 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 30 con; 0-5 aty)
% Number of variables : 99 ( 99 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f51,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f300,axiom,
! [X2,X3,X0,X1] : c_Fun_Ofun__upd(X0,X1,hAPP(X0,X1),X2,X3) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_fun__upd__idem__iff_1) ).
fof(f523,axiom,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),X1,tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__is__Un_0) ).
fof(f620,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_fun(X2,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__absorb1_0) ).
fof(f629,axiom,
! [X2,X0,X1] : c_lessequals(X0,c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__upper1_0) ).
fof(f654,axiom,
! [X0,X1] : c_Collect(c_fequal(X0,X1),X1) = c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
fof(f655,plain,
! [X0,X1] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1) = c_Collect(c_fequal(X0,X1),X1),
inference(reorient_equations,[],[f654]) ).
fof(f725,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(c_in(X1,X5,X3))
| c_Set_Oimage(c_Fun_Ofun__upd(X0,X1,X2,X3,X4),X5,X3,X4) = c_Set_Oinsert(X2,c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X3,tc_bool)),X5),c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3)),X3,X4),X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_fun__upd__image_0) ).
fof(f777,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_Set_Oinsert(X0,X1,X2),c_Set_Oinsert(X0,X3,X2),tc_fun(X2,tc_bool))
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__mono_0) ).
fof(f802,axiom,
! [X2,X0,X1] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f832,axiom,
! [X0,X1] :
( c_lessequals(c_Orderings_Obot__class_Obot(X0),X1,X0)
| ~ class_Orderings_Obot(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot__least_0) ).
fof(f844,axiom,
! [X2,X0,X1] :
( hBOOL(c_in(X0,X1,X2))
| ~ hBOOL(hAPP(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f864,axiom,
! [X2,X0,X1] :
( ~ hBOOL(c_in(X0,X1,X2))
| c_Set_Oinsert(X0,X1,X2) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f871,negated_conjecture,
hBOOL(c_in(v_pn,v_Procs,tc_Com_Opname)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f872,negated_conjecture,
~ c_lessequals(c_Set_Oinsert(hAPP(hAPP(hAPP(c_Hoare__Mirabelle_Otriple_Otriple(t_a),hAPP(v_P,v_pn)),hAPP(c_Com_Ocom_OBODY,v_pn)),hAPP(v_Q,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),c_Set_Oimage(c_COMBS(c_COMBS(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_a),v_P,tc_fun(t_a,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_a,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a))),tc_Com_Opname),c_Com_Ocom_OBODY,tc_Com_Opname,tc_Com_Ocom,tc_fun(tc_fun(t_a,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a))),v_Q,tc_Com_Opname,tc_fun(t_a,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),v_Procs,tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(t_a)),tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f884,axiom,
! [X0,X1] :
( class_Orderings_Obot(tc_fun(X0,X1))
| ~ class_Orderings_Obot(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_fun__Orderings_Obot) ).
fof(f921,axiom,
class_Orderings_Obot(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_bool__Orderings_Obot) ).
fof(f926,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBS(X0,X1,X2,X3,X4),X5) = hAPP(hAPP(X0,X5),hAPP(X1,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBS__def_0) ).
fof(f928,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBB(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBB__def_0) ).
fof(f931,definition,
sF0 = c_in(v_pn,v_Procs,tc_Com_Opname),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f932,plain,
c_in(v_pn,v_Procs,tc_Com_Opname) = sF0,
inference(reorient_equations,[],[f931]) ).
fof(f933,plain,
hBOOL(sF0),
inference(definition_folding,[],[f871,f932]) ).
fof(f934,definition,
sF1 = c_Hoare__Mirabelle_Otriple_Otriple(t_a),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f935,plain,
c_Hoare__Mirabelle_Otriple_Otriple(t_a) = sF1,
inference(reorient_equations,[],[f934]) ).
fof(f936,definition,
sF2 = hAPP(v_P,v_pn),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f937,plain,
hAPP(v_P,v_pn) = sF2,
inference(reorient_equations,[],[f936]) ).
fof(f938,definition,
sF3 = hAPP(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f939,plain,
hAPP(sF1,sF2) = sF3,
inference(reorient_equations,[],[f938]) ).
fof(f940,definition,
sF4 = hAPP(c_Com_Ocom_OBODY,v_pn),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f941,plain,
hAPP(c_Com_Ocom_OBODY,v_pn) = sF4,
inference(reorient_equations,[],[f940]) ).
fof(f942,definition,
sF5 = hAPP(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f943,plain,
hAPP(sF3,sF4) = sF5,
inference(reorient_equations,[],[f942]) ).
fof(f944,definition,
sF6 = hAPP(v_Q,v_pn),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f945,plain,
hAPP(v_Q,v_pn) = sF6,
inference(reorient_equations,[],[f944]) ).
fof(f946,definition,
sF7 = hAPP(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f947,plain,
hAPP(sF5,sF6) = sF7,
inference(reorient_equations,[],[f946]) ).
fof(f948,definition,
sF8 = tc_Hoare__Mirabelle_Otriple(t_a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f949,plain,
tc_Hoare__Mirabelle_Otriple(t_a) = sF8,
inference(reorient_equations,[],[f948]) ).
fof(f950,definition,
sF9 = tc_fun(sF8,tc_bool),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f951,plain,
tc_fun(sF8,tc_bool) = sF9,
inference(reorient_equations,[],[f950]) ).
fof(f952,definition,
sF10 = c_Orderings_Obot__class_Obot(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f953,plain,
c_Orderings_Obot__class_Obot(sF9) = sF10,
inference(reorient_equations,[],[f952]) ).
fof(f954,definition,
sF11 = c_Set_Oinsert(sF7,sF10,sF8),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f955,plain,
c_Set_Oinsert(sF7,sF10,sF8) = sF11,
inference(reorient_equations,[],[f954]) ).
fof(f956,definition,
sF12 = tc_fun(tc_Com_Ostate,tc_bool),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f957,plain,
tc_fun(tc_Com_Ostate,tc_bool) = sF12,
inference(reorient_equations,[],[f956]) ).
fof(f958,definition,
sF13 = tc_fun(t_a,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f959,plain,
tc_fun(t_a,sF12) = sF13,
inference(reorient_equations,[],[f958]) ).
fof(f960,definition,
sF14 = tc_fun(sF13,sF8),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f961,plain,
tc_fun(sF13,sF8) = sF14,
inference(reorient_equations,[],[f960]) ).
fof(f962,definition,
sF15 = tc_fun(tc_Com_Ocom,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f963,plain,
tc_fun(tc_Com_Ocom,sF14) = sF15,
inference(reorient_equations,[],[f962]) ).
fof(f964,definition,
sF16 = c_COMBB(sF1,v_P,sF13,sF15,tc_Com_Opname),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f965,plain,
c_COMBB(sF1,v_P,sF13,sF15,tc_Com_Opname) = sF16,
inference(reorient_equations,[],[f964]) ).
fof(f966,definition,
sF17 = c_COMBS(sF16,c_Com_Ocom_OBODY,tc_Com_Opname,tc_Com_Ocom,sF14),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f967,plain,
c_COMBS(sF16,c_Com_Ocom_OBODY,tc_Com_Opname,tc_Com_Ocom,sF14) = sF17,
inference(reorient_equations,[],[f966]) ).
fof(f968,definition,
sF18 = c_COMBS(sF17,v_Q,tc_Com_Opname,sF13,sF8),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f969,plain,
c_COMBS(sF17,v_Q,tc_Com_Opname,sF13,sF8) = sF18,
inference(reorient_equations,[],[f968]) ).
fof(f970,definition,
sF19 = c_Set_Oimage(sF18,v_Procs,tc_Com_Opname,sF8),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f971,plain,
c_Set_Oimage(sF18,v_Procs,tc_Com_Opname,sF8) = sF19,
inference(reorient_equations,[],[f970]) ).
fof(f972,plain,
~ c_lessequals(sF11,sF19,sF9),
inference(definition_folding,[],[f872,f951,f949,f971,f949,f969,f949,f959,f957,f967,f961,f949,f959,f957,f965,f963,f961,f949,f959,f957,f959,f957,f935,f955,f949,f953,f951,f949,f947,f945,f943,f941,f939,f937,f935]) ).
fof(f985,plain,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Lattices_Oupper__semilattice__class_Osup(c_Collect(c_fequal(X0,X2),X2),X1,tc_fun(X2,tc_bool)),
inference(forward_demodulation,[],[f523,f655]) ).
fof(f1007,plain,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Lattices_Oupper__semilattice__class_Osup(c_fequal(X0,X2),X1,tc_fun(X2,tc_bool)),
inference(forward_demodulation,[],[f985,f51]) ).
fof(f1095,plain,
( class_Orderings_Obot(sF9)
| ~ class_Orderings_Obot(tc_bool) ),
inference(superposition,[],[f884,f951]) ).
fof(f1101,plain,
class_Orderings_Obot(sF9),
inference(forward_subsumption_resolution,[],[f1095,f921]) ).
fof(f1129,plain,
! [X0] :
( c_lessequals(sF10,X0,sF9)
| ~ class_Orderings_Obot(sF9) ),
inference(superposition,[],[f832,f953]) ).
fof(f1130,plain,
! [X0] : c_lessequals(sF10,X0,sF9),
inference(forward_subsumption_resolution,[],[f1129,f1101]) ).
fof(f1577,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X1,X0))
| c_Set_Oinsert(X0,X1,X2) = X1 ),
inference(resolution,[],[f864,f844]) ).
fof(f3079,plain,
! [X0,X1] : c_Set_Oinsert(X0,X1,tc_Com_Ostate) = c_Lattices_Oupper__semilattice__class_Osup(c_fequal(X0,tc_Com_Ostate),X1,sF12),
inference(superposition,[],[f1007,f957]) ).
fof(f3092,plain,
! [X2,X0,X1] : c_lessequals(c_fequal(X0,X2),c_Set_Oinsert(X0,X1,X2),tc_fun(X2,tc_bool)),
inference(superposition,[],[f629,f1007]) ).
fof(f4045,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,sF12)
| c_Lattices_Oupper__semilattice__class_Osup(X0,X1,sF12) = X1 ),
inference(superposition,[],[f620,f957]) ).
fof(f4494,plain,
! [X0] : hAPP(sF1,hAPP(v_P,X0)) = hAPP(sF16,X0),
inference(superposition,[],[f928,f965]) ).
fof(f6111,plain,
! [X0] : hAPP(hAPP(sF16,X0),hAPP(c_Com_Ocom_OBODY,X0)) = hAPP(sF17,X0),
inference(superposition,[],[f926,f967]) ).
fof(f6112,plain,
! [X0] : hAPP(sF18,X0) = hAPP(hAPP(sF17,X0),hAPP(v_Q,X0)),
inference(superposition,[],[f926,f969]) ).
fof(f8451,plain,
! [X0] :
( c_lessequals(sF11,c_Set_Oinsert(sF7,X0,sF8),tc_fun(sF8,tc_bool))
| ~ c_lessequals(sF10,X0,tc_fun(sF8,tc_bool)) ),
inference(superposition,[],[f777,f955]) ).
fof(f8476,plain,
! [X0] :
( c_lessequals(sF11,c_Set_Oinsert(sF7,X0,sF8),sF9)
| ~ c_lessequals(sF10,X0,tc_fun(sF8,tc_bool)) ),
inference(forward_demodulation,[],[f8451,f951]) ).
fof(f8486,plain,
! [X0] :
( ~ c_lessequals(sF10,X0,sF9)
| c_lessequals(sF11,c_Set_Oinsert(sF7,X0,sF8),sF9) ),
inference(forward_demodulation,[],[f8476,f951]) ).
fof(f8487,plain,
! [X0] : c_lessequals(sF11,c_Set_Oinsert(sF7,X0,sF8),sF9),
inference(forward_subsumption_resolution,[],[f8486,f1130]) ).
fof(f26986,plain,
! [X2,X0,X1] :
( ~ hBOOL(sF0)
| c_Set_Oimage(c_Fun_Ofun__upd(X0,v_pn,X1,tc_Com_Opname,X2),v_Procs,tc_Com_Opname,X2) = c_Set_Oinsert(X1,c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_bool)),v_Procs),c_Set_Oinsert(v_pn,c_Orderings_Obot__class_Obot(tc_fun(tc_Com_Opname,tc_bool)),tc_Com_Opname)),tc_Com_Opname,X2),X2) ),
inference(superposition,[],[f725,f932]) ).
fof(f26988,plain,
! [X2,X0,X1] : c_Set_Oimage(c_Fun_Ofun__upd(X0,v_pn,X1,tc_Com_Opname,X2),v_Procs,tc_Com_Opname,X2) = c_Set_Oinsert(X1,c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_bool)),v_Procs),c_Set_Oinsert(v_pn,c_Orderings_Obot__class_Obot(tc_fun(tc_Com_Opname,tc_bool)),tc_Com_Opname)),tc_Com_Opname,X2),X2),
inference(forward_subsumption_resolution,[],[f26986,f933]) ).
fof(f27038,plain,
! [X2,X0,X1] : c_Set_Oimage(c_Fun_Ofun__upd(X0,v_pn,X1,tc_Com_Opname,X2),v_Procs,tc_Com_Opname,X2) = c_Set_Oinsert(X1,c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_bool)),v_Procs),c_Collect(c_fequal(v_pn,tc_Com_Opname),tc_Com_Opname)),tc_Com_Opname,X2),X2),
inference(forward_demodulation,[],[f26988,f655]) ).
fof(f27087,plain,
! [X2,X0,X1] : c_Set_Oimage(c_Fun_Ofun__upd(X0,v_pn,X1,tc_Com_Opname,X2),v_Procs,tc_Com_Opname,X2) = c_Set_Oinsert(X1,c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(tc_Com_Opname,tc_bool)),v_Procs),c_fequal(v_pn,tc_Com_Opname)),tc_Com_Opname,X2),X2),
inference(forward_demodulation,[],[f27038,f51]) ).
fof(f29981,plain,
! [X2,X0,X1] : hBOOL(hAPP(c_Set_Oimage(c_Fun_Ofun__upd(X0,v_pn,X1,tc_Com_Opname,X2),v_Procs,tc_Com_Opname,X2),X1)),
inference(superposition,[],[f802,f27087]) ).
fof(f30040,plain,
! [X0,X1] : hBOOL(hAPP(c_Set_Oimage(X0,v_Procs,tc_Com_Opname,X1),hAPP(X0,v_pn))),
inference(superposition,[],[f29981,f300]) ).
fof(f30119,plain,
hBOOL(hAPP(sF19,hAPP(sF18,v_pn))),
inference(superposition,[],[f30040,f971]) ).
fof(f33027,plain,
hAPP(sF1,sF2) = hAPP(sF16,v_pn),
inference(superposition,[],[f4494,f937]) ).
fof(f33056,plain,
sF3 = hAPP(sF16,v_pn),
inference(forward_demodulation,[],[f33027,f939]) ).
fof(f33597,plain,
! [X0] : sF19 = c_Set_Oinsert(hAPP(sF18,v_pn),sF19,X0),
inference(resolution,[],[f1577,f30119]) ).
fof(f38696,plain,
! [X0] : c_lessequals(c_fequal(hAPP(sF18,v_pn),X0),sF19,tc_fun(X0,tc_bool)),
inference(superposition,[],[f3092,f33597]) ).
fof(f40560,plain,
hAPP(sF17,v_pn) = hAPP(hAPP(sF16,v_pn),sF4),
inference(superposition,[],[f6111,f941]) ).
fof(f40597,plain,
hAPP(sF3,sF4) = hAPP(sF17,v_pn),
inference(forward_demodulation,[],[f40560,f33056]) ).
fof(f40601,plain,
sF5 = hAPP(sF17,v_pn),
inference(forward_demodulation,[],[f40597,f943]) ).
fof(f40608,plain,
hAPP(sF18,v_pn) = hAPP(hAPP(sF17,v_pn),sF6),
inference(superposition,[],[f6112,f945]) ).
fof(f40645,plain,
hAPP(sF5,sF6) = hAPP(sF18,v_pn),
inference(forward_demodulation,[],[f40608,f40601]) ).
fof(f40649,plain,
sF7 = hAPP(sF18,v_pn),
inference(forward_demodulation,[],[f40645,f947]) ).
fof(f42103,plain,
c_lessequals(c_fequal(hAPP(sF18,v_pn),tc_Com_Ostate),sF19,sF12),
inference(superposition,[],[f38696,f957]) ).
fof(f42104,plain,
c_lessequals(c_fequal(sF7,tc_Com_Ostate),sF19,sF12),
inference(forward_demodulation,[],[f42103,f40649]) ).
fof(f42179,plain,
sF19 = c_Lattices_Oupper__semilattice__class_Osup(c_fequal(sF7,tc_Com_Ostate),sF19,sF12),
inference(resolution,[],[f42104,f4045]) ).
fof(f42220,plain,
sF19 = c_Set_Oinsert(sF7,sF19,tc_Com_Ostate),
inference(forward_demodulation,[],[f42179,f3079]) ).
fof(f42255,plain,
hBOOL(hAPP(sF19,sF7)),
inference(superposition,[],[f802,f42220]) ).
fof(f42549,plain,
! [X0] : sF19 = c_Set_Oinsert(sF7,sF19,X0),
inference(resolution,[],[f42255,f1577]) ).
fof(f43183,plain,
c_lessequals(sF11,sF19,sF9),
inference(superposition,[],[f8487,f42549]) ).
fof(f43243,plain,
$false,
inference(forward_subsumption_resolution,[],[f43183,f972]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV829-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 12:40:25 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.04/1.55 % (2226910)Will run a generic schedule for satisfiability detection.
% 8.04/1.55 % (2226920)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4150082898:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.04/1.55 % (2226916)% WARNING: option uhcvi not known.
% 8.04/1.55 % (2226915)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2090537639_2999 on theBenchmark for (2999ds/0Mi)
% 8.04/1.55 % (2226916)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1802706668:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.04/1.55 % (2226917)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=977875047:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.04/1.55 % (2226918)dis+10_1_sil=32000:sp=arity:random_seed=1751736201:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.04/1.55 % (2226919)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4056368093:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.04/1.55 % (2226921)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3412837331:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.04/1.55 % (2226920)Instruction limit reached!
% 8.04/1.55 % (2226920)------------------------------
% 8.04/1.55 % (2226920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.04/1.55 % (2226920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.04/1.55 % (2226920)CaDiCaL version: 2.1.3
% 8.04/1.55 % (2226920)Termination reason: Instruction limit
% 8.04/1.55 % (2226920)Termination phase: Saturation
% 8.04/1.55 % (2226920)Time elapsed: 0.050 s
% 8.04/1.55 % (2226920)Peak memory usage: 14 MB
% 8.04/1.55 % (2226920)Instructions burned: 136 (million)
% 8.04/1.55 % (2226929)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2466679834:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.04/1.55 % (2226918)Instruction limit reached!
% 8.04/1.55 % (2226918)------------------------------
% 8.04/1.55 % (2226918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.04/1.55 % (2226918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.04/1.55 % (2226918)CaDiCaL version: 2.1.3
% 8.04/1.55 % (2226918)Termination reason: Instruction limit
% 8.04/1.55 % (2226918)Termination phase: Saturation
% 8.04/1.55 % (2226918)Time elapsed: 0.069 s
% 8.04/1.55 % (2226918)Peak memory usage: 13 MB
% 8.04/1.55 % (2226918)Instructions burned: 104 (million)
% 8.04/1.55 % (2226919)Instruction limit reached!
% 8.04/1.55 % (2226919)------------------------------
% 8.04/1.55 % (2226919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.04/1.55 % (2226919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.04/1.55 % (2226919)CaDiCaL version: 2.1.3
% 8.04/1.55 % (2226919)Termination reason: Instruction limit
% 8.04/1.55 % (2226919)Termination phase: Saturation
% 8.04/1.55 % (2226919)Time elapsed: 0.075 s
% 8.04/1.55 % (2226919)Peak memory usage: 14 MB
% 8.04/1.55 % (2226919)Instructions burned: 116 (million)
% 8.04/1.55 % (2226931)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2193758178:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.04/1.55 % (2226932)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2395737048:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.04/1.55 % (2226921)Instruction limit reached!
% 8.04/1.55 % (2226921)------------------------------
% 8.04/1.55 % (2226921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.04/1.55 % (2226921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.04/1.55 % (2226921)CaDiCaL version: 2.1.3
% 8.04/1.55 % (2226921)Termination reason: Instruction limit
% 8.04/1.55 % (2226921)Termination phase: Saturation
% 8.04/1.55 % (2226921)Time elapsed: 0.104 s
% 8.04/1.55 % (2226921)Peak memory usage: 14 MB
% 8.04/1.55 % (2226921)Instructions burned: 159 (million)
% 8.04/1.55 % (2226935)ott-21_1_sil=16000:fs=off:random_seed=2570122308:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.04/1.55 % TRYING [1]
% 8.04/1.55 % TRYING [2]
% 8.04/1.55 % TRYING [1]
% 8.04/1.55 % (2226931)Instruction limit reached!
% 8.04/1.55 % (2226931)------------------------------
% 8.04/1.55 % (2226931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.04/1.55 % (2226931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226931)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226931)Termination reason: Instruction limit
% 25.84/4.03 % (2226931)Termination phase: Saturation
% 25.84/4.03 % (2226931)Time elapsed: 0.078 s
% 25.84/4.03 % (2226931)Peak memory usage: 13 MB
% 25.84/4.03 % (2226931)Instructions burned: 132 (million)
% 25.84/4.03 % TRYING [2]
% 25.84/4.03 % (2226937)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2738083495:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 25.84/4.03 % TRYING [3]
% 25.84/4.03 % (2226935)Instruction limit reached!
% 25.84/4.03 % (2226935)------------------------------
% 25.84/4.03 % (2226935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226935)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226935)Termination reason: Instruction limit
% 25.84/4.03 % (2226935)Termination phase: Saturation
% 25.84/4.03 % (2226935)Time elapsed: 0.102 s
% 25.84/4.03 % (2226935)Peak memory usage: 13 MB
% 25.84/4.03 % (2226935)Instructions burned: 181 (million)
% 25.84/4.03 % (2226929)Instruction limit reached!
% 25.84/4.03 % (2226929)------------------------------
% 25.84/4.03 % (2226929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226929)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226929)Termination reason: Instruction limit
% 25.84/4.03 % (2226929)Termination phase: Finite model building constraint generation
% 25.84/4.03 % (2226929)Time elapsed: 0.175 s
% 25.84/4.03 % (2226929)Peak memory usage: 39 MB
% 25.84/4.03 % (2226929)Instructions burned: 715 (million)
% 25.84/4.03 % (2226940)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2156760605:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 25.84/4.03 % (2226939)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1219185173:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 25.84/4.03 % TRYING [3]
% 25.84/4.03 % TRYING [1]
% 25.84/4.03 % (2226937)Instruction limit reached!
% 25.84/4.03 % (2226937)------------------------------
% 25.84/4.03 % (2226937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226937)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226937)Termination reason: Instruction limit
% 25.84/4.03 % (2226937)Termination phase: Saturation
% 25.84/4.03 % (2226937)Time elapsed: 0.300 s
% 25.84/4.03 % (2226937)Peak memory usage: 15 MB
% 25.84/4.03 % (2226937)Instructions burned: 478 (million)
% 25.84/4.03 % TRYING [2]
% 25.84/4.03 % (2226943)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=330972125:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 25.84/4.03 % (2226932)Instruction limit reached!
% 25.84/4.03 % (2226932)------------------------------
% 25.84/4.03 % (2226932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226932)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226932)Termination reason: Instruction limit
% 25.84/4.03 % (2226932)Termination phase: Saturation
% 25.84/4.03 % (2226932)Time elapsed: 0.442 s
% 25.84/4.03 % (2226932)Peak memory usage: 17 MB
% 25.84/4.03 % (2226932)Instructions burned: 684 (million)
% 25.84/4.03 % (2226945)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2900602656:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 25.84/4.03 % (2226940)Instruction limit reached!
% 25.84/4.03 % (2226940)------------------------------
% 25.84/4.03 % (2226940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226940)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226940)Termination reason: Instruction limit
% 25.84/4.03 % (2226940)Termination phase: Saturation
% 25.84/4.03 % (2226940)Time elapsed: 0.390 s
% 25.84/4.03 % (2226940)Peak memory usage: 23 MB
% 25.84/4.03 % (2226940)Instructions burned: 1182 (million)
% 25.84/4.03 % (2226939)Instruction limit reached!
% 25.84/4.03 % (2226939)------------------------------
% 25.84/4.03 % (2226939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.84/4.03 % (2226939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.84/4.03 % (2226939)CaDiCaL version: 2.1.3
% 25.84/4.03 % (2226939)Termination reason: Instruction limit
% 10.96/4.16 % (2226939)Termination phase: Finite model building SAT solving
% 10.96/4.16 % (2226939)Time elapsed: 0.398 s
% 10.96/4.16 % (2226939)Peak memory usage: 38 MB
% 10.96/4.16 % (2226939)Instructions burned: 866 (million)
% 10.96/4.16 % (2226947)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2283149754:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 10.96/4.16 % (2226943)Cannot represent all propositional literals internally
% 10.96/4.16 % (2226943)Refutation not found, incomplete strategy
% 10.96/4.16 % (2226943)------------------------------
% 10.96/4.16 % (2226943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226943)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226943)Termination reason: Refutation not found, incomplete strategy
% 10.96/4.16 % (2226943)Time elapsed: 0.159 s
% 10.96/4.16 % (2226943)Peak memory usage: 17 MB
% 10.96/4.16 % (2226943)Instructions burned: 316 (million)
% 10.96/4.16 % (2226949)fmb+10_1_sil=64000:random_seed=1356231782:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 10.96/4.16 % (2226943)------------------------------
% 10.96/4.16 % (2226943)------------------------------
% 10.96/4.16 % (2226951)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1402975735:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 10.96/4.16 % TRYING [1]
% 10.96/4.16 % (2226951)Cannot represent all propositional literals internally
% 10.96/4.16 % (2226951)Refutation not found, incomplete strategy
% 10.96/4.16 % (2226951)------------------------------
% 10.96/4.16 % (2226951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226951)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226951)Termination reason: Refutation not found, incomplete strategy
% 10.96/4.16 % (2226951)Time elapsed: 0.158 s
% 10.96/4.16 % (2226951)Peak memory usage: 17 MB
% 10.96/4.16 % (2226951)Instructions burned: 316 (million)
% 10.96/4.16 % (2226951)------------------------------
% 10.96/4.16 % (2226951)------------------------------
% 10.96/4.16 % TRYING [2]
% 10.96/4.16 % (2226953)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4185743168:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 10.96/4.16 % (2226947)Instruction limit reached!
% 10.96/4.16 % (2226947)------------------------------
% 10.96/4.16 % (2226947)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226947)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226947)Termination reason: Instruction limit
% 10.96/4.16 % (2226947)Termination phase: Saturation
% 10.96/4.16 % (2226947)Time elapsed: 0.272 s
% 10.96/4.16 % (2226947)Peak memory usage: 20 MB
% 10.96/4.16 % (2226947)Instructions burned: 882 (million)
% 10.96/4.16 % (2226955)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1253717288:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 10.96/4.16 % (2226945)Instruction limit reached!
% 10.96/4.16 % (2226945)------------------------------
% 10.96/4.16 % (2226945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226945)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226945)Termination reason: Instruction limit
% 10.96/4.16 % (2226945)Termination phase: Saturation
% 10.96/4.16 % (2226945)Time elapsed: 0.468 s
% 10.96/4.16 % (2226945)Peak memory usage: 20 MB
% 10.96/4.16 % (2226945)Instructions burned: 692 (million)
% 10.96/4.16 % TRYING [8]
% 10.96/4.16 % (2226957)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2880237814:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 10.96/4.16 % (2226953)Instruction limit reached!
% 10.96/4.16 % (2226953)------------------------------
% 10.96/4.16 % (2226953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226953)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226953)Termination reason: Instruction limit
% 10.96/4.16 % (2226953)Termination phase: Finite model building constraint generation
% 10.96/4.16 % (2226953)Time elapsed: 0.363 s
% 10.96/4.16 % (2226953)Peak memory usage: 55 MB
% 10.96/4.16 % (2226953)Instructions burned: 922 (million)
% 10.96/4.16 % (2226959)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=714221909:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 10.96/4.16 % (2226959)Cannot represent all propositional literals internally
% 10.96/4.16 % (2226959)Refutation not found, incomplete strategy
% 10.96/4.16 % (2226959)------------------------------
% 10.96/4.16 % (2226959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226959)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226959)Termination reason: Refutation not found, incomplete strategy
% 10.96/4.16 % (2226959)Time elapsed: 0.167 s
% 10.96/4.16 % (2226959)Peak memory usage: 17 MB
% 10.96/4.16 % (2226959)Instructions burned: 332 (million)
% 10.96/4.16 % (2226959)------------------------------
% 10.96/4.16 % (2226959)------------------------------
% 10.96/4.16 % TRYING [4]
% 10.96/4.16 % (2226962)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3815017843:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi)
% 10.96/4.16 % TRYING [3]
% 10.96/4.16 % (2226957)Instruction limit reached!
% 10.96/4.16 % (2226957)------------------------------
% 10.96/4.16 % (2226957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226957)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226957)Termination reason: Instruction limit
% 10.96/4.16 % (2226957)Termination phase: Saturation
% 10.96/4.16 % (2226957)Time elapsed: 0.782 s
% 10.96/4.16 % (2226957)Peak memory usage: 32 MB
% 10.96/4.16 % (2226957)Instructions burned: 1472 (million)
% 10.96/4.16 % (2226964)ott-2_1_sil=16000:newcnf=on:random_seed=456316619:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2981 on theBenchmark for (2981ds/869Mi)
% 10.96/4.16 % (2226962)Cannot represent all propositional literals internally
% 10.96/4.16 % (2226962)Refutation not found, incomplete strategy
% 10.96/4.16 % (2226962)------------------------------
% 10.96/4.16 % (2226962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226962)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226962)Termination reason: Refutation not found, incomplete strategy
% 10.96/4.16 % (2226962)Time elapsed: 0.742 s
% 10.96/4.16 % (2226962)Peak memory usage: 29 MB
% 10.96/4.16 % (2226962)Instructions burned: 1521 (million)
% 10.96/4.16 % (2226962)------------------------------
% 10.96/4.16 % (2226962)------------------------------
% 10.96/4.16 % (2226966)ott+10_1_sil=32000:tgt=ground:random_seed=4215940472:i=5114:av=off_2977 on theBenchmark for (2977ds/5114Mi)
% 10.96/4.16 % (2226964)Instruction limit reached!
% 10.96/4.16 % (2226964)------------------------------
% 10.96/4.16 % (2226964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226964)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226964)Termination reason: Instruction limit
% 10.96/4.16 % (2226964)Termination phase: Saturation
% 10.96/4.16 % (2226964)Time elapsed: 0.470 s
% 10.96/4.16 % (2226964)Peak memory usage: 17 MB
% 10.96/4.16 % (2226964)Instructions burned: 869 (million)
% 10.96/4.16 % (2226968)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3882459986:i=54282_2976 on theBenchmark for (2976ds/54282Mi)
% 10.96/4.16 % TRYING [1]
% 10.96/4.16 % TRYING [2]
% 10.96/4.16 % (2226955)Instruction limit reached!
% 10.96/4.16 % (2226955)------------------------------
% 10.96/4.16 % (2226955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226955)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226955)Termination reason: Instruction limit
% 10.96/4.16 % (2226955)Termination phase: Saturation
% 10.96/4.16 % (2226955)Time elapsed: 1.634 s
% 10.96/4.16 % (2226955)Peak memory usage: 45 MB
% 10.96/4.16 % (2226955)Instructions burned: 5133 (million)
% 10.96/4.16 % (2226970)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1058398281:i=3512:aac=none_2973 on theBenchmark for (2973ds/3512Mi)
% 10.96/4.16 % TRYING [3]
% 10.96/4.16 % (2226970)Instruction limit reached!
% 10.96/4.16 % (2226970)------------------------------
% 10.96/4.16 % (2226970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226970)CaDiCaL version: 2.1.3
% 10.96/4.16 % (2226970)Termination reason: Instruction limit
% 10.96/4.16 % (2226970)Termination phase: Saturation
% 10.96/4.16 % (2226970)Time elapsed: 1.150 s
% 10.96/4.16 % (2226970)Peak memory usage: 36 MB
% 10.96/4.16 % (2226970)Instructions burned: 3512 (million)
% 10.96/4.16 % (2226972)dis+21_1_sil=32000:sas=cadical:random_seed=2596911583:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 10.96/4.16 % (2226966) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2226910-2226966"...
% 10.96/4.16 % TRYING [4]
% 10.96/4.16 % (2226966)...printing done.
% 10.96/4.16 % (2226966)Refutation found. Thanks to Tanya!
% 10.96/4.16 % SZS status Unsatisfiable for theBenchmark
% 10.96/4.16 % SZS output start Proof for theBenchmark
% See solution above
% 10.96/4.16 % (2226966)------------------------------
% 10.96/4.16 % (2226966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.96/4.16 % (2226966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.96/4.16 % (2226966)CaDiCaL version: 2.1.3
% 10.96/4.17 % (2226966)Termination reason: Refutation
% 10.96/4.17 % (2226966)Time elapsed: 1.564 s
% 10.96/4.17 % (2226966)Peak memory usage: 35 MB
% 10.96/4.17 % (2226966)Instructions burned: 2389 (million)
% 10.96/4.17 % (2226910)Success in time 3.925 s
% 10.96/4.17 % Vampire exiting
%------------------------------------------------------------------------------