%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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:21:08 PM UTC 2026
% Result : Theorem 5.98s 3.43s
% Output : Refutation 5.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 17
% Syntax : Number of formulae : 109 ( 15 unt; 8 def)
% Number of atoms : 270 ( 23 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 277 ( 116 ~; 128 |; 11 &)
% ( 11 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 9 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 173 ( 0 sgn 165 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
( less_than(X0,X1)
| less_than(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+0.ax',totality) ).
fof(f4,axiom,
! [X0,X1] :
( strictly_less_than(X0,X1)
<=> ( less_than(X0,X1)
& ~ less_than(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+0.ax',stricly_smaller_definition) ).
fof(f32,axiom,
! [X0,X1,X2,X3] :
( ( contains_slb(X1,X3)
& less_than(lookup_slb(X1,X3),X3) )
=> remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+3.ax',ax44) ).
fof(f33,axiom,
! [X0,X1,X2,X3] :
( ( contains_slb(X1,X3)
& strictly_less_than(X3,lookup_slb(X1,X3)) )
=> remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),bad) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+3.ax',ax45) ).
fof(f42,axiom,
! [X0,X1,X2] :
( check_cpq(triple(X0,X1,X2))
<=> ! [X3,X4] :
( pair_in_list(X1,X3,X4)
=> less_than(X4,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l27_li4142) ).
fof(f43,axiom,
! [X0,X1,X2] :
( pair_in_list(X0,X1,X2)
=> ! [X3] :
( contains_slb(X0,X3)
=> ( pair_in_list(remove_slb(X0,X3),X1,X2)
| X1 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l27_li2829) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( check_cpq(remove_cpq(triple(X0,X1,X2),X3))
& ok(remove_cpq(triple(X0,X1,X2),X3)) )
=> ! [X4] :
( pair_in_list(X1,X3,X4)
=> less_than(X4,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l27_l30) ).
fof(f45,axiom,
! [X0,X1,X2,X3] :
( ok(remove_cpq(triple(X0,X1,X2),X3))
=> contains_slb(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l27_l33) ).
fof(f46,conjecture,
! [X0,X1,X2,X3] :
( ( check_cpq(remove_cpq(triple(X0,X1,X2),X3))
& ok(remove_cpq(triple(X0,X1,X2),X3)) )
=> check_cpq(triple(X0,X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l27_co) ).
fof(f47,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( check_cpq(remove_cpq(triple(X0,X1,X2),X3))
& ok(remove_cpq(triple(X0,X1,X2),X3)) )
=> check_cpq(triple(X0,X1,X2)) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f52,plain,
! [X0,X1] :
( ( less_than(X0,X1)
& ~ less_than(X1,X0) )
=> strictly_less_than(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f4]) ).
fof(f55,plain,
! [X0,X1] :
( strictly_less_than(X0,X1)
| ~ less_than(X0,X1)
| less_than(X1,X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f56,plain,
! [X0,X1] :
( strictly_less_than(X0,X1)
| ~ less_than(X0,X1)
| less_than(X1,X0) ),
inference(flattening,[],[f55]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),X2)
| ~ contains_slb(X1,X3)
| ~ less_than(lookup_slb(X1,X3),X3) ),
inference(ennf_transformation,[],[f32]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),X2)
| ~ contains_slb(X1,X3)
| ~ less_than(lookup_slb(X1,X3),X3) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),bad)
| ~ contains_slb(X1,X3)
| ~ strictly_less_than(X3,lookup_slb(X1,X3)) ),
inference(ennf_transformation,[],[f33]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),bad)
| ~ contains_slb(X1,X3)
| ~ strictly_less_than(X3,lookup_slb(X1,X3)) ),
inference(flattening,[],[f73]) ).
fof(f82,plain,
! [X0,X1,X2] :
( check_cpq(triple(X0,X1,X2))
<=> ! [X3,X4] :
( less_than(X4,X3)
| ~ pair_in_list(X1,X3,X4) ) ),
inference(ennf_transformation,[],[f42]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ! [X3] :
( pair_in_list(remove_slb(X0,X3),X1,X2)
| X1 = X3
| ~ contains_slb(X0,X3) )
| ~ pair_in_list(X0,X1,X2) ),
inference(ennf_transformation,[],[f43]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ! [X3] :
( pair_in_list(remove_slb(X0,X3),X1,X2)
| X1 = X3
| ~ contains_slb(X0,X3) )
| ~ pair_in_list(X0,X1,X2) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( less_than(X4,X3)
| ~ pair_in_list(X1,X3,X4) )
| ~ check_cpq(remove_cpq(triple(X0,X1,X2),X3))
| ~ ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(ennf_transformation,[],[f44]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( less_than(X4,X3)
| ~ pair_in_list(X1,X3,X4) )
| ~ check_cpq(remove_cpq(triple(X0,X1,X2),X3))
| ~ ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( contains_slb(X1,X3)
| ~ ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(ennf_transformation,[],[f45]) ).
fof(f88,plain,
? [X0,X1,X2,X3] :
( ~ check_cpq(triple(X0,X1,X2))
& check_cpq(remove_cpq(triple(X0,X1,X2),X3))
& ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(ennf_transformation,[],[f47]) ).
fof(f89,plain,
? [X0,X1,X2,X3] :
( ~ check_cpq(triple(X0,X1,X2))
& check_cpq(remove_cpq(triple(X0,X1,X2),X3))
& ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(flattening,[],[f88]) ).
fof(f91,plain,
! [X0,X1] :
( less_than(X1,X0)
| less_than(X0,X1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
! [X0,X1] :
( strictly_less_than(X0,X1)
| ~ less_than(X0,X1)
| less_than(X1,X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f128,plain,
! [X2,X3,X0,X1] :
( ~ less_than(lookup_slb(X1,X3),X3)
| ~ contains_slb(X1,X3)
| remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),X2) ),
inference(cnf_transformation,[],[f72]) ).
fof(f129,plain,
! [X2,X3,X0,X1] :
( ~ strictly_less_than(X3,lookup_slb(X1,X3))
| ~ contains_slb(X1,X3)
| remove_cpq(triple(X0,X1,X2),X3) = triple(remove_pqp(X0,X3),remove_slb(X1,X3),bad) ),
inference(cnf_transformation,[],[f74]) ).
fof(f138,plain,
! [X2,X3,X0,X1,X4] :
( ~ check_cpq(triple(X0,X1,X2))
| ~ pair_in_list(X1,X3,X4)
| less_than(X4,X3) ),
inference(cnf_transformation,[],[f82]) ).
fof(f139,plain,
! [X2,X0,X1] :
( pair_in_list(X1,sK0(X1),sK1(X1))
| check_cpq(triple(X0,X1,X2)) ),
inference(cnf_transformation,[],[f82]) ).
fof(f140,plain,
! [X2,X0,X1] :
( check_cpq(triple(X0,X1,X2))
| ~ less_than(sK1(X1),sK0(X1)) ),
inference(cnf_transformation,[],[f82]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( pair_in_list(remove_slb(X0,X3),X1,X2)
| ~ contains_slb(X0,X3)
| X1 = X3
| ~ pair_in_list(X0,X1,X2) ),
inference(cnf_transformation,[],[f84]) ).
fof(f142,plain,
! [X2,X3,X0,X1,X4] :
( ~ ok(remove_cpq(triple(X0,X1,X2),X3))
| ~ pair_in_list(X1,X3,X4)
| ~ check_cpq(remove_cpq(triple(X0,X1,X2),X3))
| less_than(X4,X3) ),
inference(cnf_transformation,[],[f86]) ).
fof(f143,plain,
! [X2,X3,X0,X1] :
( ~ ok(remove_cpq(triple(X0,X1,X2),X3))
| contains_slb(X1,X3) ),
inference(cnf_transformation,[],[f87]) ).
fof(f144,plain,
ok(remove_cpq(triple(sK2,sK3,sK4),sK5)),
inference(cnf_transformation,[],[f89]) ).
fof(f145,plain,
check_cpq(remove_cpq(triple(sK2,sK3,sK4),sK5)),
inference(cnf_transformation,[],[f89]) ).
fof(f146,plain,
~ check_cpq(triple(sK2,sK3,sK4)),
inference(cnf_transformation,[],[f89]) ).
fof(f156,plain,
~ less_than(sK1(sK3),sK0(sK3)),
inference(resolution,[],[f140,f146]) ).
fof(f159,plain,
contains_slb(sK3,sK5),
inference(resolution,[],[f143,f144]) ).
fof(f473,plain,
! [X0] :
( ~ pair_in_list(sK3,sK5,X0)
| ~ check_cpq(remove_cpq(triple(sK2,sK3,sK4),sK5))
| less_than(X0,sK5) ),
inference(resolution,[],[f142,f144]) ).
fof(f480,plain,
! [X0] :
( ~ pair_in_list(sK3,sK5,X0)
| less_than(X0,sK5) ),
inference(forward_subsumption_resolution,[],[f473,f145]) ).
fof(f518,definition,
( spl6_4
<=> less_than(lookup_slb(sK3,sK5),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition]) ).
fof(f519,plain,
( less_than(lookup_slb(sK3,sK5),sK5)
| ~ spl6_4 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f520,plain,
( ~ less_than(lookup_slb(sK3,sK5),sK5)
| spl6_4 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f535,definition,
( spl6_6
<=> less_than(sK1(sK3),sK5) ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f536,plain,
( less_than(sK1(sK3),sK5)
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f537,plain,
( ~ less_than(sK1(sK3),sK5)
| spl6_6 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f884,definition,
( spl6_14
<=> strictly_less_than(sK5,lookup_slb(sK3,sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
fof(f885,plain,
( strictly_less_than(sK5,lookup_slb(sK3,sK5))
| ~ spl6_14 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f886,plain,
( ~ strictly_less_than(sK5,lookup_slb(sK3,sK5))
| spl6_14 ),
inference(avatar_component_clause,[],[f884]) ).
fof(f891,plain,
( ~ less_than(sK5,lookup_slb(sK3,sK5))
| less_than(lookup_slb(sK3,sK5),sK5)
| spl6_14 ),
inference(resolution,[],[f886,f93]) ).
fof(f892,plain,
( less_than(lookup_slb(sK3,sK5),sK5)
| spl6_14 ),
inference(forward_subsumption_resolution,[],[f891,f91]) ).
fof(f893,plain,
( $false
| spl6_4
| spl6_14 ),
inference(forward_subsumption_resolution,[],[f892,f520]) ).
fof(f894,plain,
( spl6_4
| spl6_14 ),
inference(avatar_contradiction_clause,[],[f893]) ).
fof(f895,plain,
( ! [X0,X1] :
( ~ contains_slb(sK3,sK5)
| remove_cpq(triple(X0,sK3,X1),sK5) = triple(remove_pqp(X0,sK5),remove_slb(sK3,sK5),X1) )
| ~ spl6_4 ),
inference(resolution,[],[f519,f128]) ).
fof(f899,plain,
( ! [X0,X1] : remove_cpq(triple(X0,sK3,X1),sK5) = triple(remove_pqp(X0,sK5),remove_slb(sK3,sK5),X1)
| ~ spl6_4 ),
inference(forward_subsumption_resolution,[],[f895,f159]) ).
fof(f924,plain,
( ! [X2,X3,X0,X1] :
( ~ check_cpq(remove_cpq(triple(X0,sK3,X1),sK5))
| ~ pair_in_list(remove_slb(sK3,sK5),X2,X3)
| less_than(X3,X2) )
| ~ spl6_4 ),
inference(superposition,[],[f138,f899]) ).
fof(f946,definition,
( spl6_19
<=> ! [X2,X3] :
( ~ pair_in_list(remove_slb(sK3,sK5),X2,X3)
| less_than(X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl6_19])],[avatar_definition]) ).
fof(f947,plain,
( ! [X2,X3] :
( ~ pair_in_list(remove_slb(sK3,sK5),X2,X3)
| less_than(X3,X2) )
| ~ spl6_19 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f949,definition,
( spl6_20
<=> ! [X0,X1] : ~ check_cpq(remove_cpq(triple(X0,sK3,X1),sK5)) ),
introduced(definition,[new_symbols(definition,[spl6_20])],[avatar_definition]) ).
fof(f950,plain,
( ! [X0,X1] : ~ check_cpq(remove_cpq(triple(X0,sK3,X1),sK5))
| ~ spl6_20 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f951,plain,
( spl6_19
| spl6_20
| ~ spl6_4 ),
inference(avatar_split_clause,[],[f924,f518,f949,f946]) ).
fof(f960,plain,
( ! [X0,X1] :
( ~ contains_slb(sK3,sK5)
| remove_cpq(triple(X0,sK3,X1),sK5) = triple(remove_pqp(X0,sK5),remove_slb(sK3,sK5),bad) )
| ~ spl6_14 ),
inference(resolution,[],[f885,f129]) ).
fof(f963,plain,
( ! [X0,X1] : remove_cpq(triple(X0,sK3,X1),sK5) = triple(remove_pqp(X0,sK5),remove_slb(sK3,sK5),bad)
| ~ spl6_14 ),
inference(forward_subsumption_resolution,[],[f960,f159]) ).
fof(f994,plain,
( ! [X2,X3,X0,X1] :
( ~ check_cpq(remove_cpq(triple(X0,sK3,X1),sK5))
| ~ pair_in_list(remove_slb(sK3,sK5),X2,X3)
| less_than(X3,X2) )
| ~ spl6_14 ),
inference(superposition,[],[f138,f963]) ).
fof(f1001,plain,
( spl6_19
| spl6_20
| ~ spl6_14 ),
inference(avatar_split_clause,[],[f994,f884,f949,f946]) ).
fof(f1211,definition,
( spl6_27
<=> ! [X0,X1] : check_cpq(triple(X0,sK3,X1)) ),
introduced(definition,[new_symbols(definition,[spl6_27])],[avatar_definition]) ).
fof(f1212,plain,
( ! [X0,X1] : check_cpq(triple(X0,sK3,X1))
| ~ spl6_27 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1214,definition,
( spl6_28
<=> sK5 = sK0(sK3) ),
introduced(definition,[new_symbols(definition,[spl6_28])],[avatar_definition]) ).
fof(f1215,plain,
( sK5 != sK0(sK3)
| spl6_28 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1216,plain,
( sK5 = sK0(sK3)
| ~ spl6_28 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1223,plain,
( $false
| ~ spl6_27 ),
inference(resolution,[],[f1212,f146]) ).
fof(f1225,plain,
~ spl6_27,
inference(avatar_contradiction_clause,[],[f1223]) ).
fof(f1240,plain,
( ~ less_than(sK1(sK3),sK5)
| ~ spl6_28 ),
inference(superposition,[],[f156,f1216]) ).
fof(f1255,plain,
( ! [X0,X1] :
( pair_in_list(sK3,sK5,sK1(sK3))
| check_cpq(triple(X0,sK3,X1)) )
| ~ spl6_28 ),
inference(superposition,[],[f139,f1216]) ).
fof(f1257,definition,
( spl6_29
<=> pair_in_list(sK3,sK5,sK1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl6_29])],[avatar_definition]) ).
fof(f1259,plain,
( pair_in_list(sK3,sK5,sK1(sK3))
| ~ spl6_29 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1260,plain,
( spl6_27
| spl6_29
| ~ spl6_28 ),
inference(avatar_split_clause,[],[f1255,f1214,f1257,f1211]) ).
fof(f1266,plain,
( $false
| ~ spl6_6
| ~ spl6_28 ),
inference(forward_subsumption_resolution,[],[f1240,f536]) ).
fof(f1267,plain,
( ~ spl6_6
| ~ spl6_28 ),
inference(avatar_contradiction_clause,[],[f1266]) ).
fof(f1321,plain,
( ! [X0,X1] :
( less_than(X0,X1)
| ~ contains_slb(sK3,sK5)
| sK5 = X1
| ~ pair_in_list(sK3,X1,X0) )
| ~ spl6_19 ),
inference(resolution,[],[f947,f141]) ).
fof(f1324,plain,
( ! [X0,X1] :
( ~ pair_in_list(sK3,X1,X0)
| sK5 = X1
| less_than(X0,X1) )
| ~ spl6_19 ),
inference(forward_subsumption_resolution,[],[f1321,f159]) ).
fof(f3009,plain,
( ! [X0,X1] :
( sK5 = sK0(sK3)
| less_than(sK1(sK3),sK0(sK3))
| check_cpq(triple(X0,sK3,X1)) )
| ~ spl6_19 ),
inference(resolution,[],[f1324,f139]) ).
fof(f3010,plain,
( ! [X0,X1] :
( sK5 = sK0(sK3)
| check_cpq(triple(X0,sK3,X1)) )
| ~ spl6_19 ),
inference(forward_subsumption_resolution,[],[f3009,f140]) ).
fof(f3011,plain,
( ! [X0,X1] : check_cpq(triple(X0,sK3,X1))
| ~ spl6_19
| spl6_28 ),
inference(forward_subsumption_resolution,[],[f3010,f1215]) ).
fof(f3012,plain,
( spl6_27
| ~ spl6_19
| spl6_28 ),
inference(avatar_split_clause,[],[f3011,f1214,f946,f1211]) ).
fof(f3261,plain,
( less_than(sK1(sK3),sK5)
| ~ spl6_29 ),
inference(resolution,[],[f1259,f480]) ).
fof(f3267,plain,
( $false
| spl6_6
| ~ spl6_29 ),
inference(forward_subsumption_resolution,[],[f3261,f537]) ).
fof(f3268,plain,
( spl6_6
| ~ spl6_29 ),
inference(avatar_contradiction_clause,[],[f3267]) ).
fof(f3274,plain,
( $false
| ~ spl6_20 ),
inference(resolution,[],[f950,f145]) ).
fof(f3275,plain,
~ spl6_20,
inference(avatar_contradiction_clause,[],[f3274]) ).
cnf(s14,plain,
( spl6_4
| spl6_14 ),
inference(sat_conversion,[],[f894]) ).
cnf(s17,plain,
( ~ spl6_4
| spl6_19
| spl6_20 ),
inference(sat_conversion,[],[f951]) ).
cnf(s20,plain,
( ~ spl6_14
| spl6_19
| spl6_20 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s31,plain,
~ spl6_27,
inference(sat_conversion,[],[f1225]) ).
cnf(s32,plain,
( spl6_27
| ~ spl6_28
| spl6_29 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s36,plain,
( ~ spl6_6
| ~ spl6_28 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s150,plain,
( ~ spl6_19
| spl6_27
| spl6_28 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s151,plain,
( spl6_6
| ~ spl6_29 ),
inference(sat_conversion,[],[f3268]) ).
cnf(s154,plain,
~ spl6_20,
inference(sat_conversion,[],[f3275]) ).
cnf(s161,plain,
( ~ spl6_14
| spl6_19 ),
inference(rat,[],[s20,s154]) ).
cnf(s162,plain,
( ~ spl6_4
| spl6_19 ),
inference(rat,[],[s17,s154]) ).
cnf(s164,plain,
~ spl6_28,
inference(rat,[],[s151,s32,s36,s31]) ).
cnf(s165,plain,
~ spl6_19,
inference(rat,[],[s150,s31,s164]) ).
cnf(s167,plain,
~ spl6_14,
inference(rat,[],[s161,s165]) ).
cnf(s168,plain,
~ spl6_4,
inference(rat,[],[s162,s165]) ).
cnf(s169,plain,
$false,
inference(rat,[],[s14,s167,s168]) ).
fof(f3276,plain,
$false,
inference(avatar_sat_refutation,[],[s169]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.17 % Computer : n026.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Mon Sep 28 10:50:57 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.20 Running first-order model finding
% 0.12/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.20/2.50 % (3777458)Will run a generic schedule for satisfiability detection.
% 16.20/2.50 % (3777469)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2415053271:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.20/2.50 % (3777464)% WARNING: option uhcvi not known.
% 16.20/2.50 % (3777465)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1591418389:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.20/2.50 % (3777463)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=433757474_2999 on theBenchmark for (2999ds/0Mi)
% 16.20/2.50 % (3777464)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2970621042:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.20/2.50 % (3777466)dis+10_1_sil=32000:sp=arity:random_seed=4178493381:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.20/2.50 % (3777467)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=434128811:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.20/2.50 % (3777468)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1762855246:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.20/2.50 % TRYING [1]
% 16.20/2.50 % TRYING [2]
% 16.20/2.50 % TRYING [3]
% 16.20/2.50 % TRYING [4]
% 16.20/2.50 % (3777469)Instruction limit reached!
% 16.20/2.50 % (3777469)------------------------------
% 16.20/2.50 % (3777469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.20/2.50 % (3777469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/2.50 % (3777469)CaDiCaL version: 2.1.3
% 16.20/2.50 % (3777469)Termination reason: Instruction limit
% 16.20/2.50 % (3777469)Termination phase: Saturation
% 16.20/2.50 % (3777469)Time elapsed: 0.049 s
% 16.20/2.50 % (3777469)Peak memory usage: 12 MB
% 16.20/2.50 % (3777469)Instructions burned: 159 (million)
% 16.20/2.50 % (3777477)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1757827212:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.20/2.50 % TRYING [1]
% 16.20/2.50 % TRYING [2]
% 16.20/2.50 % TRYING [3]
% 16.20/2.50 % (3777467)Instruction limit reached!
% 16.20/2.50 % (3777467)------------------------------
% 16.20/2.50 % (3777467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.20/2.50 % (3777467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/2.50 % (3777467)CaDiCaL version: 2.1.3
% 16.20/2.50 % (3777467)Termination reason: Instruction limit
% 16.20/2.50 % (3777467)Termination phase: Saturation
% 16.20/2.50 % (3777467)Time elapsed: 0.064 s
% 16.20/2.50 % (3777467)Peak memory usage: 12 MB
% 16.20/2.50 % (3777467)Instructions burned: 117 (million)
% 16.20/2.50 % (3777466)Instruction limit reached!
% 16.20/2.50 % (3777466)------------------------------
% 16.20/2.50 % (3777466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.20/2.50 % (3777466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/2.50 % (3777466)CaDiCaL version: 2.1.3
% 16.20/2.50 % (3777466)Termination reason: Instruction limit
% 16.20/2.50 % (3777466)Termination phase: Saturation
% 16.20/2.50 % (3777466)Time elapsed: 0.066 s
% 16.20/2.50 % (3777466)Peak memory usage: 12 MB
% 16.20/2.50 % (3777466)Instructions burned: 103 (million)
% 16.20/2.50 % TRYING [4]
% 16.20/2.50 % (3777468)Instruction limit reached!
% 16.20/2.50 % (3777468)------------------------------
% 16.20/2.50 % (3777468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.20/2.50 % (3777468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/2.50 % (3777468)CaDiCaL version: 2.1.3
% 16.20/2.50 % (3777468)Termination reason: Instruction limit
% 16.20/2.50 % (3777468)Termination phase: Saturation
% 16.20/2.50 % (3777468)Time elapsed: 0.081 s
% 16.20/2.50 % (3777468)Peak memory usage: 13 MB
% 16.20/2.50 % (3777468)Instructions burned: 131 (million)
% 16.20/2.50 % (3777479)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1947415091:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.20/2.50 % (3777480)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=3712828584:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.20/2.50 % (3777481)ott-21_1_sil=16000:fs=off:random_seed=2390557146:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.20/2.50 % TRYING [5]
% 16.20/2.50 % TRYING [5]
% 16.20/2.50 % (3777479)Instruction limit reached!
% 16.20/2.50 % (3777479)------------------------------
% 16.20/2.50 % (3777479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777479)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777479)Termination reason: Instruction limit
% 5.98/3.43 % (3777479)Termination phase: Saturation
% 5.98/3.43 % (3777479)Time elapsed: 0.088 s
% 5.98/3.43 % (3777479)Peak memory usage: 13 MB
% 5.98/3.43 % (3777479)Instructions burned: 132 (million)
% 5.98/3.43 % (3777481)Instruction limit reached!
% 5.98/3.43 % (3777481)------------------------------
% 5.98/3.43 % (3777481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777481)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777481)Termination reason: Instruction limit
% 5.98/3.43 % (3777481)Termination phase: Saturation
% 5.98/3.43 % (3777481)Time elapsed: 0.085 s
% 5.98/3.43 % (3777481)Peak memory usage: 12 MB
% 5.98/3.43 % (3777481)Instructions burned: 181 (million)
% 5.98/3.43 % (3777485)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4286294976:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.98/3.43 % (3777477)Instruction limit reached!
% 5.98/3.43 % (3777477)------------------------------
% 5.98/3.43 % (3777477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777477)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777477)Termination reason: Instruction limit
% 5.98/3.43 % (3777477)Termination phase: Finite model building constraint generation
% 5.98/3.43 % (3777477)Time elapsed: 0.146 s
% 5.98/3.43 % (3777477)Peak memory usage: 35 MB
% 5.98/3.43 % (3777477)Instructions burned: 715 (million)
% 5.98/3.43 % (3777486)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1187363245:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.98/3.43 % TRYING [1]
% 5.98/3.43 % TRYING [2]
% 5.98/3.43 % (3777488)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4066075048:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.98/3.43 % TRYING [3]
% 5.98/3.43 % TRYING [4]
% 5.98/3.43 % TRYING [6]
% 5.98/3.43 % (3777480)Instruction limit reached!
% 5.98/3.43 % (3777480)------------------------------
% 5.98/3.43 % (3777480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777480)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777480)Termination reason: Instruction limit
% 5.98/3.43 % (3777480)Termination phase: Saturation
% 5.98/3.43 % (3777480)Time elapsed: 0.307 s
% 5.98/3.43 % (3777480)Peak memory usage: 13 MB
% 5.98/3.43 % (3777480)Instructions burned: 685 (million)
% 5.98/3.43 % (3777492)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=768245137:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.98/3.43 % TRYING [5]
% 5.98/3.43 % (3777485)Instruction limit reached!
% 5.98/3.43 % (3777485)------------------------------
% 5.98/3.43 % (3777485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777485)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777485)Termination reason: Instruction limit
% 5.98/3.43 % (3777485)Termination phase: Saturation
% 5.98/3.43 % (3777485)Time elapsed: 0.299 s
% 5.98/3.43 % (3777485)Peak memory usage: 14 MB
% 5.98/3.43 % (3777485)Instructions burned: 478 (million)
% 5.98/3.43 % (3777494)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=3102806029: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)
% 5.98/3.43 % (3777486)Instruction limit reached!
% 5.98/3.43 % (3777486)------------------------------
% 5.98/3.43 % (3777486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777486)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777486)Termination reason: Instruction limit
% 5.98/3.43 % (3777486)Termination phase: Finite model building constraint generation
% 5.98/3.43 % (3777486)Time elapsed: 0.320 s
% 5.98/3.43 % (3777486)Peak memory usage: 27 MB
% 5.98/3.43 % (3777486)Instructions burned: 866 (million)
% 5.98/3.43 % (3777496)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=68904762:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.98/3.43 % (3777488)Instruction limit reached!
% 5.98/3.43 % (3777488)------------------------------
% 5.98/3.43 % (3777488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777488)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777488)Termination reason: Instruction limit
% 5.98/3.43 % (3777488)Termination phase: Saturation
% 5.98/3.43 % (3777488)Time elapsed: 0.375 s
% 5.98/3.43 % (3777488)Peak memory usage: 18 MB
% 5.98/3.43 % (3777488)Instructions burned: 1182 (million)
% 5.98/3.43 % (3777498)fmb+10_1_sil=64000:random_seed=3548240551:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.98/3.43 % TRYING [1]
% 5.98/3.43 % TRYING [2]
% 5.98/3.43 % TRYING [3]
% 5.98/3.43 % TRYING [4]
% 5.98/3.43 % TRYING [5]
% 5.98/3.43 % (3777492)Instruction limit reached!
% 5.98/3.43 % (3777492)------------------------------
% 5.98/3.43 % (3777492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777492)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777492)Termination reason: Instruction limit
% 5.98/3.43 % (3777492)Termination phase: Finite model building constraint generation
% 5.98/3.43 % (3777492)Time elapsed: 0.412 s
% 5.98/3.43 % (3777492)Peak memory usage: 105 MB
% 5.98/3.43 % (3777492)Instructions burned: 891 (million)
% 5.98/3.43 % (3777500)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2644901806:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 5.98/3.43 % TRYING [20]
% 5.98/3.43 % (3777494)Instruction limit reached!
% 5.98/3.43 % (3777494)------------------------------
% 5.98/3.43 % (3777494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777494)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777494)Termination reason: Instruction limit
% 5.98/3.43 % (3777494)Termination phase: Saturation
% 5.98/3.43 % (3777494)Time elapsed: 0.393 s
% 5.98/3.43 % (3777494)Peak memory usage: 18 MB
% 5.98/3.43 % (3777494)Instructions burned: 692 (million)
% 5.98/3.43 % (3777502)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3929182187:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 5.98/3.43 % TRYING [8]
% 5.98/3.43 % (3777496)Instruction limit reached!
% 5.98/3.43 % (3777496)------------------------------
% 5.98/3.43 % (3777496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777496)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777496)Termination reason: Instruction limit
% 5.98/3.43 % (3777496)Termination phase: Saturation
% 5.98/3.43 % (3777496)Time elapsed: 0.535 s
% 5.98/3.43 % (3777496)Peak memory usage: 19 MB
% 5.98/3.43 % (3777496)Instructions burned: 880 (million)
% 5.98/3.43 % (3777504)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=737210701:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 5.98/3.43 % TRYING [6]
% 5.98/3.43 % (3777502)Instruction limit reached!
% 5.98/3.43 % (3777502)------------------------------
% 5.98/3.43 % (3777502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777502)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777502)Termination reason: Instruction limit
% 5.98/3.43 % (3777502)Termination phase: Finite model building constraint generation
% 5.98/3.43 % (3777502)Time elapsed: 0.308 s
% 5.98/3.43 % (3777502)Peak memory usage: 65 MB
% 5.98/3.43 % (3777502)Instructions burned: 921 (million)
% 5.98/3.43 % (3777506)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2112979955:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 5.98/3.43 % TRYING [7]
% 5.98/3.43 % (3777506)Instruction limit reached!
% 5.98/3.43 % (3777506)------------------------------
% 5.98/3.43 % (3777506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777506)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777506)Termination reason: Instruction limit
% 5.98/3.43 % (3777506)Termination phase: Saturation
% 5.98/3.43 % (3777506)Time elapsed: 0.961 s
% 5.98/3.43 % (3777506)Peak memory usage: 27 MB
% 5.98/3.43 % (3777506)Instructions burned: 1472 (million)
% 5.98/3.43 % (3777508)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=321601846:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 5.98/3.43 % (3777508)Cannot represent all propositional literals internally
% 5.98/3.43 % (3777508)Refutation not found, incomplete strategy
% 5.98/3.43 % (3777508)------------------------------
% 5.98/3.43 % (3777508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777508)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777508)Termination reason: Refutation not found, incomplete strategy
% 5.98/3.43 % (3777508)Time elapsed: 0.007 s
% 5.98/3.43 % (3777508)Peak memory usage: 11 MB
% 5.98/3.43 % (3777508)Instructions burned: 13 (million)
% 5.98/3.43 % (3777508)------------------------------
% 5.98/3.43 % (3777508)------------------------------
% 5.98/3.43 % (3777510)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1254617064:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 5.98/3.43 % TRYING [16]
% 5.98/3.43 % TRYING [7]
% 5.98/3.43 % TRYING [8]
% 5.98/3.43 % (3777510)Instruction limit reached!
% 5.98/3.43 % (3777510)------------------------------
% 5.98/3.43 % (3777510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777510)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777510)Termination reason: Instruction limit
% 5.98/3.43 % (3777510)Termination phase: Finite model building constraint generation
% 5.98/3.43 % (3777510)Time elapsed: 0.745 s
% 5.98/3.43 % (3777510)Peak memory usage: 131 MB
% 5.98/3.43 % (3777510)Instructions burned: 2174 (million)
% 5.98/3.43 % (3777512)ott-2_1_sil=16000:newcnf=on:random_seed=3524164901:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 5.98/3.43 % (3777512) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3777458-3777512"...
% 5.98/3.43 % (3777512)...printing done.
% 5.98/3.43 % (3777512)Refutation found. Thanks to Tanya!
% 5.98/3.43 % SZS status Theorem for theBenchmark
% 5.98/3.43 % SZS output start Proof for theBenchmark
% See solution above
% 5.98/3.43 % (3777512)------------------------------
% 5.98/3.43 % (3777512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.98/3.43 % (3777512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/3.43 % (3777512)CaDiCaL version: 2.1.3
% 5.98/3.43 % (3777512)Termination reason: Refutation
% 5.98/3.43 % (3777512)Time elapsed: 0.067 s
% 5.98/3.43 % (3777512)Peak memory usage: 13 MB
% 5.98/3.43 % (3777512)Instructions burned: 104 (million)
% 5.98/3.43 % (3777458)Success in time 3.221 s
% 5.98/3.43 % Vampire exiting
%------------------------------------------------------------------------------