%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : TOP025+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 02:34:22 PM UTC 2026
% Result : Theorem 28.06s 7.64s
% Output : Refutation 28.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 22
% Syntax : Number of formulae : 141 ( 41 unt; 7 def)
% Number of atoms : 409 ( 73 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 441 ( 173 ~; 200 |; 33 &)
% ( 14 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 8 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-2 aty)
% Number of variables : 101 ( 0 sgn 97 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f344,axiom,
! [X0] : k1_subset_1(X0) = k1_xboole_0,
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+7.ax',d3_subset_1) ).
fof(f345,axiom,
! [X0] : k2_subset_1(X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+7.ax',d4_subset_1) ).
fof(f368,axiom,
! [X0] : k2_subset_1(X0) = k3_subset_1(X0,k1_subset_1(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+7.ax',t22_subset_1) ).
fof(f427,axiom,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+7.ax',dt_k2_subset_1) ).
fof(f2183,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+206.ax',d3_pre_topc) ).
fof(f2240,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( ( v4_pre_topc(X1,X0)
=> k6_pre_topc(X0,X1) = X1 )
& ( ( v2_pre_topc(X0)
& k6_pre_topc(X0,X1) = X1 )
=> v4_pre_topc(X1,X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+206.ax',t52_pre_topc) ).
fof(f2245,axiom,
! [X0] :
( l1_pre_topc(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+206.ax',dt_l1_pre_topc) ).
fof(f2362,axiom,
! [X0] :
( l1_pre_topc(X0)
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tops_1(X1,X0)
<=> k6_pre_topc(X0,X1) = k2_pre_topc(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+207.ax',d3_tops_1) ).
fof(f2611,axiom,
! [X0] : u1_pre_topc(k2_pcomps_1(X0)) = k1_pcomps_1(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+301.ax',t7_pcomps_1) ).
fof(f2652,axiom,
! [X0] : k1_pcomps_1(X0) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+301.ax',redefinition_k1_pcomps_1) ).
fof(f3108,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
=> ( v1_tex_2(X1,k1_zfmisc_1(X0))
<=> X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+387.ax',t5_tex_2) ).
fof(f3435,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v3_pre_topc(X1,X0)
=> k3_tex_4(X0,X1) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET007/SET007+405.ax',t58_tex_4) ).
fof(f3582,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tsp_2) ).
fof(f3583,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ( v1_tsp_2(X1,X0)
=> v1_tops_1(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tsp_2) ).
fof(f3584,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( ( v3_pre_topc(X1,X0)
| v4_pre_topc(X1,X0) )
& v1_tsp_2(X1,X0)
& v1_tex_2(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_tsp_2) ).
fof(f3585,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> ~ ( ( v3_pre_topc(X1,X0)
| v4_pre_topc(X1,X0) )
& v1_tsp_2(X1,X0)
& v1_tex_2(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
inference(negated_conjecture,[status(cth)],[f3584]) ).
fof(f6100,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f2183]) ).
fof(f6146,plain,
! [X0] :
( ! [X1] :
( ( ( k6_pre_topc(X0,X1) = X1
| ~ v4_pre_topc(X1,X0) )
& ( v4_pre_topc(X1,X0)
| ~ v2_pre_topc(X0)
| k6_pre_topc(X0,X1) != X1 ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2240]) ).
fof(f6147,plain,
! [X0] :
( ! [X1] :
( ( ( k6_pre_topc(X0,X1) = X1
| ~ v4_pre_topc(X1,X0) )
& ( v4_pre_topc(X1,X0)
| ~ v2_pre_topc(X0)
| k6_pre_topc(X0,X1) != X1 ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f6146]) ).
fof(f6154,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2245]) ).
fof(f6306,plain,
! [X0] :
( ! [X1] :
( ( v1_tops_1(X1,X0)
<=> k6_pre_topc(X0,X1) = k2_pre_topc(X0) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f2362]) ).
fof(f7529,plain,
! [X0,X1] :
( ( v1_tex_2(X1,k1_zfmisc_1(X0))
<=> X1 != X0 )
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f3108]) ).
fof(f8156,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3435]) ).
fof(f8157,plain,
! [X0] :
( ! [X1] :
( k3_tex_4(X0,X1) = X1
| ~ v3_pre_topc(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8156]) ).
fof(f8415,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3582]) ).
fof(f8416,plain,
! [X0] :
( ! [X1] :
( ( v1_tsp_2(X1,X0)
<=> ( v1_tsp_1(X1,X0)
& k3_tex_4(X0,X1) = u1_struct_0(X0) ) )
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8415]) ).
fof(f8417,plain,
! [X0] :
( ! [X1] :
( v1_tops_1(X1,X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3583]) ).
fof(f8418,plain,
! [X0] :
( ! [X1] :
( v1_tops_1(X1,X0)
| ~ v1_tsp_2(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f8417]) ).
fof(f8419,plain,
? [X0] :
( ? [X1] :
( ( v3_pre_topc(X1,X0)
| v4_pre_topc(X1,X0) )
& v1_tsp_2(X1,X0)
& v1_tex_2(X1,k1_zfmisc_1(u1_struct_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f3585]) ).
fof(f8420,plain,
? [X0] :
( ? [X1] :
( ( v3_pre_topc(X1,X0)
| v4_pre_topc(X1,X0) )
& v1_tsp_2(X1,X0)
& v1_tex_2(X1,k1_zfmisc_1(u1_struct_0(X0)))
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f8419]) ).
fof(f8916,plain,
! [X0] : k1_xboole_0 = k1_subset_1(X0),
inference(cnf_transformation,[],[f344]) ).
fof(f8917,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[],[f345]) ).
fof(f8946,plain,
! [X0] : k2_subset_1(X0) = k3_subset_1(X0,k1_subset_1(X0)),
inference(cnf_transformation,[],[f368]) ).
fof(f9036,plain,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f427]) ).
fof(f12645,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f6100]) ).
fof(f12718,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v4_pre_topc(X1,X0)
| k6_pre_topc(X0,X1) = X1 ),
inference(cnf_transformation,[],[f6147]) ).
fof(f12730,plain,
! [X0] :
( ~ l1_pre_topc(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6154]) ).
fof(f12913,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k2_pre_topc(X0) = k6_pre_topc(X0,X1)
| ~ v1_tops_1(X1,X0) ),
inference(cnf_transformation,[],[f6306]) ).
fof(f13460,plain,
! [X0] : k1_pcomps_1(X0) = u1_pre_topc(k2_pcomps_1(X0)),
inference(cnf_transformation,[],[f2611]) ).
fof(f13583,plain,
! [X0] : k1_zfmisc_1(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f2652]) ).
fof(f14829,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| X0 != X1
| ~ v1_tex_2(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f7529]) ).
fof(f15905,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v3_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1 ),
inference(cnf_transformation,[],[f8157]) ).
fof(f16374,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| u1_struct_0(X0) = k3_tex_4(X0,X1)
| ~ v1_tsp_2(X1,X0) ),
inference(cnf_transformation,[],[f8416]) ).
fof(f16377,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_tsp_2(X1,X0)
| v1_tops_1(X1,X0) ),
inference(cnf_transformation,[],[f8418]) ).
fof(f16378,plain,
( v4_pre_topc(sK1158,sK1157)
| v3_pre_topc(sK1158,sK1157) ),
inference(cnf_transformation,[],[f8420]) ).
fof(f16379,plain,
m1_subset_1(sK1158,k1_zfmisc_1(u1_struct_0(sK1157))),
inference(cnf_transformation,[],[f8420]) ).
fof(f16380,plain,
v1_tex_2(sK1158,k1_zfmisc_1(u1_struct_0(sK1157))),
inference(cnf_transformation,[],[f8420]) ).
fof(f16381,plain,
v1_tsp_2(sK1158,sK1157),
inference(cnf_transformation,[],[f8420]) ).
fof(f16382,plain,
l1_pre_topc(sK1157),
inference(cnf_transformation,[],[f8420]) ).
fof(f16383,plain,
v2_pre_topc(sK1157),
inference(cnf_transformation,[],[f8420]) ).
fof(f16384,plain,
~ v3_struct_0(sK1157),
inference(cnf_transformation,[],[f8420]) ).
fof(f16386,plain,
! [X0] : k1_zfmisc_1(X0) = u1_pre_topc(k2_pcomps_1(X0)),
inference(definition_unfolding,[],[f13583,f13460]) ).
fof(f16388,plain,
! [X0] : k2_subset_1(X0) = k3_subset_1(X0,k1_xboole_0),
inference(definition_unfolding,[],[f8946,f8916]) ).
fof(f16616,plain,
! [X0] : k3_subset_1(X0,k1_xboole_0) = X0,
inference(definition_unfolding,[],[f8917,f16388]) ).
fof(f16711,plain,
! [X0] : m1_subset_1(k3_subset_1(X0,k1_xboole_0),u1_pre_topc(k2_pcomps_1(X0))),
inference(definition_unfolding,[],[f9036,f16388,f16386]) ).
fof(f17758,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ v4_pre_topc(X1,X0)
| k6_pre_topc(X0,X1) = X1 ),
inference(definition_unfolding,[],[f12718,f16386]) ).
fof(f17890,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| k2_pre_topc(X0) = k6_pre_topc(X0,X1)
| ~ v1_tops_1(X1,X0) ),
inference(definition_unfolding,[],[f12913,f16386]) ).
fof(f18876,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(X0)))
| X0 != X1
| ~ v1_tex_2(X1,u1_pre_topc(k2_pcomps_1(X0))) ),
inference(definition_unfolding,[],[f14829,f16386,f16386]) ).
fof(f19303,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ v3_pre_topc(X1,X0)
| k3_tex_4(X0,X1) = X1 ),
inference(definition_unfolding,[],[f15905,f16386]) ).
fof(f19566,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| u1_struct_0(X0) = k3_tex_4(X0,X1)
| ~ v1_tsp_2(X1,X0) ),
inference(definition_unfolding,[],[f16374,f16386]) ).
fof(f19567,plain,
! [X0,X1] :
( ~ l1_pre_topc(X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| ~ v1_tsp_2(X1,X0)
| v1_tops_1(X1,X0) ),
inference(definition_unfolding,[],[f16377,f16386]) ).
fof(f19568,plain,
v1_tex_2(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157)))),
inference(definition_unfolding,[],[f16380,f16386]) ).
fof(f19569,plain,
m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157)))),
inference(definition_unfolding,[],[f16379,f16386]) ).
fof(f20264,plain,
! [X1] :
( ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(X1)))
| ~ v1_tex_2(X1,u1_pre_topc(k2_pcomps_1(X1))) ),
inference(equality_resolution,[],[f18876]) ).
fof(f23054,plain,
! [X0] :
( l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f12645]) ).
fof(f23128,plain,
! [X0,X1] :
( ~ v4_pre_topc(X1,X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| l1_pre_topc(X0)
| k6_pre_topc(X0,X1) = X1 ),
inference(consistent_polarity_flipping,[],[f17758]) ).
fof(f23139,plain,
! [X0] :
( ~ l1_struct_0(X0)
| l1_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f12730]) ).
fof(f23319,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| l1_pre_topc(X0)
| k2_pre_topc(X0) = k6_pre_topc(X0,X1)
| v1_tops_1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f17890]) ).
fof(f26213,plain,
! [X0,X1] :
( ~ v3_pre_topc(X1,X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| l1_pre_topc(X0)
| k3_tex_4(X0,X1) = X1 ),
inference(consistent_polarity_flipping,[],[f19303]) ).
fof(f26670,plain,
! [X0,X1] :
( ~ v1_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| u1_struct_0(X0) = k3_tex_4(X0,X1)
| l1_pre_topc(X0) ),
inference(consistent_polarity_flipping,[],[f19566]) ).
fof(f26671,plain,
! [X0,X1] :
( ~ v1_tsp_2(X1,X0)
| ~ v2_pre_topc(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_pre_topc(k2_pcomps_1(u1_struct_0(X0))))
| l1_pre_topc(X0)
| ~ v1_tops_1(X1,X0) ),
inference(consistent_polarity_flipping,[],[f19567]) ).
fof(f26672,plain,
~ l1_pre_topc(sK1157),
inference(consistent_polarity_flipping,[],[f16382]) ).
fof(f26694,definition,
( spl1159_1
<=> v3_pre_topc(sK1158,sK1157) ),
introduced(definition,[new_symbols(definition,[spl1159_1])],[avatar_definition]) ).
fof(f26696,plain,
( v3_pre_topc(sK1158,sK1157)
| ~ spl1159_1 ),
inference(avatar_component_clause,[],[f26694]) ).
fof(f26698,definition,
( spl1159_2
<=> v4_pre_topc(sK1158,sK1157) ),
introduced(definition,[new_symbols(definition,[spl1159_2])],[avatar_definition]) ).
fof(f26700,plain,
( v4_pre_topc(sK1158,sK1157)
| ~ spl1159_2 ),
inference(avatar_component_clause,[],[f26698]) ).
fof(f26701,plain,
( spl1159_1
| spl1159_2 ),
inference(avatar_split_clause,[],[f16378,f26698,f26694]) ).
fof(f32198,plain,
! [X0] : m1_subset_1(X0,u1_pre_topc(k2_pcomps_1(X0))),
inference(forward_demodulation,[],[f16711,f16616]) ).
fof(f38590,definition,
( spl1159_1062
<=> sK1158 = u1_struct_0(sK1157) ),
introduced(definition,[new_symbols(definition,[spl1159_1062])],[avatar_definition]) ).
fof(f38591,plain,
( sK1158 != u1_struct_0(sK1157)
| spl1159_1062 ),
inference(avatar_component_clause,[],[f38590]) ).
fof(f38592,plain,
( sK1158 = u1_struct_0(sK1157)
| ~ spl1159_1062 ),
inference(avatar_component_clause,[],[f38590]) ).
fof(f42876,plain,
! [X1] : ~ v1_tex_2(X1,u1_pre_topc(k2_pcomps_1(X1))),
inference(forward_subsumption_resolution,[],[f20264,f32198]) ).
fof(f74643,definition,
( spl1159_2494
<=> l1_struct_0(sK1157) ),
introduced(definition,[new_symbols(definition,[spl1159_2494])],[avatar_definition]) ).
fof(f74644,plain,
( ~ l1_struct_0(sK1157)
| spl1159_2494 ),
inference(avatar_component_clause,[],[f74643]) ).
fof(f74645,plain,
( l1_struct_0(sK1157)
| ~ spl1159_2494 ),
inference(avatar_component_clause,[],[f74643]) ).
fof(f75217,definition,
( spl1159_2510
<=> sK1158 = k6_pre_topc(sK1157,sK1158) ),
introduced(definition,[new_symbols(definition,[spl1159_2510])],[avatar_definition]) ).
fof(f75219,plain,
( sK1158 = k6_pre_topc(sK1157,sK1158)
| ~ spl1159_2510 ),
inference(avatar_component_clause,[],[f75217]) ).
fof(f88324,definition,
( spl1159_3026
<=> sK1158 = k3_tex_4(sK1157,sK1158) ),
introduced(definition,[new_symbols(definition,[spl1159_3026])],[avatar_definition]) ).
fof(f88326,plain,
( sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_3026 ),
inference(avatar_component_clause,[],[f88324]) ).
fof(f95532,plain,
( ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| sK1158 = k6_pre_topc(sK1157,sK1158)
| ~ spl1159_2 ),
inference(resolution,[],[f23128,f26700]) ).
fof(f95558,plain,
( l1_pre_topc(sK1157)
| sK1158 = k6_pre_topc(sK1157,sK1158)
| ~ spl1159_2 ),
inference(forward_subsumption_resolution,[],[f95532,f19569]) ).
fof(f95569,plain,
( sK1158 = k6_pre_topc(sK1157,sK1158)
| ~ spl1159_2 ),
inference(forward_subsumption_resolution,[],[f95558,f26672]) ).
fof(f95570,plain,
( spl1159_2510
| ~ spl1159_2 ),
inference(avatar_split_clause,[],[f95569,f26698,f75217]) ).
fof(f96806,plain,
( l1_pre_topc(sK1157)
| ~ spl1159_2494 ),
inference(resolution,[],[f74645,f23139]) ).
fof(f96808,plain,
( $false
| ~ spl1159_2494 ),
inference(forward_subsumption_resolution,[],[f96806,f26672]) ).
fof(f96809,plain,
~ spl1159_2494,
inference(avatar_contradiction_clause,[],[f96808]) ).
fof(f96847,plain,
( u1_struct_0(sK1157) = k2_pre_topc(sK1157)
| spl1159_2494 ),
inference(resolution,[],[f74644,f23054]) ).
fof(f107567,plain,
( l1_pre_topc(sK1157)
| k2_pre_topc(sK1157) = k6_pre_topc(sK1157,sK1158)
| v1_tops_1(sK1158,sK1157) ),
inference(resolution,[],[f23319,f19569]) ).
fof(f107582,plain,
( k2_pre_topc(sK1157) = k6_pre_topc(sK1157,sK1158)
| v1_tops_1(sK1158,sK1157) ),
inference(forward_subsumption_resolution,[],[f107567,f26672]) ).
fof(f107608,plain,
( sK1158 = k2_pre_topc(sK1157)
| v1_tops_1(sK1158,sK1157)
| ~ spl1159_2510 ),
inference(forward_demodulation,[],[f107582,f75219]) ).
fof(f107609,plain,
( sK1158 = u1_struct_0(sK1157)
| v1_tops_1(sK1158,sK1157)
| spl1159_2494
| ~ spl1159_2510 ),
inference(forward_demodulation,[],[f107608,f96847]) ).
fof(f107611,definition,
( spl1159_3847
<=> v1_tops_1(sK1158,sK1157) ),
introduced(definition,[new_symbols(definition,[spl1159_3847])],[avatar_definition]) ).
fof(f107614,plain,
( spl1159_3847
| spl1159_1062
| spl1159_2494
| ~ spl1159_2510 ),
inference(avatar_split_clause,[],[f107609,f75217,f74643,f38590,f107611]) ).
fof(f107626,plain,
( v1_tex_2(sK1158,u1_pre_topc(k2_pcomps_1(sK1158)))
| ~ spl1159_1062 ),
inference(superposition,[],[f19568,f38592]) ).
fof(f108080,plain,
( $false
| ~ spl1159_1062 ),
inference(forward_subsumption_resolution,[],[f107626,f42876]) ).
fof(f108081,plain,
~ spl1159_1062,
inference(avatar_contradiction_clause,[],[f108080]) ).
fof(f122181,plain,
( ~ v2_pre_topc(sK1157)
| v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| ~ v1_tops_1(sK1158,sK1157) ),
inference(resolution,[],[f26671,f16381]) ).
fof(f122182,plain,
( v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| ~ v1_tops_1(sK1158,sK1157) ),
inference(forward_subsumption_resolution,[],[f122181,f16383]) ).
fof(f122183,plain,
( ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| ~ v1_tops_1(sK1158,sK1157) ),
inference(forward_subsumption_resolution,[],[f122182,f16384]) ).
fof(f122184,plain,
( l1_pre_topc(sK1157)
| ~ v1_tops_1(sK1158,sK1157) ),
inference(forward_subsumption_resolution,[],[f122183,f19569]) ).
fof(f122185,plain,
~ v1_tops_1(sK1158,sK1157),
inference(forward_subsumption_resolution,[],[f122184,f26672]) ).
fof(f122186,plain,
~ spl1159_3847,
inference(avatar_split_clause,[],[f122185,f107611]) ).
fof(f149062,plain,
( ~ v2_pre_topc(sK1157)
| v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_1 ),
inference(resolution,[],[f26213,f26696]) ).
fof(f149074,plain,
( v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_1 ),
inference(forward_subsumption_resolution,[],[f149062,f16383]) ).
fof(f149089,plain,
( ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| l1_pre_topc(sK1157)
| sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_1 ),
inference(forward_subsumption_resolution,[],[f149074,f16384]) ).
fof(f149098,plain,
( l1_pre_topc(sK1157)
| sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_1 ),
inference(forward_subsumption_resolution,[],[f149089,f19569]) ).
fof(f149107,plain,
( sK1158 = k3_tex_4(sK1157,sK1158)
| ~ spl1159_1 ),
inference(forward_subsumption_resolution,[],[f149098,f26672]) ).
fof(f149128,plain,
( spl1159_3026
| ~ spl1159_1 ),
inference(avatar_split_clause,[],[f149107,f26694,f88324]) ).
fof(f165519,plain,
( ~ v2_pre_topc(sK1157)
| v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| u1_struct_0(sK1157) = k3_tex_4(sK1157,sK1158)
| l1_pre_topc(sK1157) ),
inference(resolution,[],[f26670,f16381]) ).
fof(f165520,plain,
( v3_struct_0(sK1157)
| ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| u1_struct_0(sK1157) = k3_tex_4(sK1157,sK1158)
| l1_pre_topc(sK1157) ),
inference(forward_subsumption_resolution,[],[f165519,f16383]) ).
fof(f165521,plain,
( ~ m1_subset_1(sK1158,u1_pre_topc(k2_pcomps_1(u1_struct_0(sK1157))))
| u1_struct_0(sK1157) = k3_tex_4(sK1157,sK1158)
| l1_pre_topc(sK1157) ),
inference(forward_subsumption_resolution,[],[f165520,f16384]) ).
fof(f165522,plain,
( u1_struct_0(sK1157) = k3_tex_4(sK1157,sK1158)
| l1_pre_topc(sK1157) ),
inference(forward_subsumption_resolution,[],[f165521,f19569]) ).
fof(f165523,plain,
u1_struct_0(sK1157) = k3_tex_4(sK1157,sK1158),
inference(forward_subsumption_resolution,[],[f165522,f26672]) ).
fof(f165524,plain,
( sK1158 = u1_struct_0(sK1157)
| ~ spl1159_3026 ),
inference(forward_demodulation,[],[f165523,f88326]) ).
fof(f165525,plain,
( $false
| spl1159_1062
| ~ spl1159_3026 ),
inference(forward_subsumption_resolution,[],[f165524,f38591]) ).
fof(f165526,plain,
( spl1159_1062
| ~ spl1159_3026 ),
inference(avatar_contradiction_clause,[],[f165525]) ).
cnf(s1,plain,
( spl1159_1
| spl1159_2 ),
inference(sat_conversion,[],[f26701]) ).
cnf(s3439,plain,
( ~ spl1159_2
| spl1159_2510 ),
inference(sat_conversion,[],[f95570]) ).
cnf(s3500,plain,
~ spl1159_2494,
inference(sat_conversion,[],[f96809]) ).
cnf(s4011,plain,
( spl1159_1062
| spl1159_2494
| ~ spl1159_2510
| spl1159_3847 ),
inference(sat_conversion,[],[f107614]) ).
cnf(s4049,plain,
~ spl1159_1062,
inference(sat_conversion,[],[f108081]) ).
cnf(s4602,plain,
~ spl1159_3847,
inference(sat_conversion,[],[f122186]) ).
cnf(s6315,plain,
( ~ spl1159_1
| spl1159_3026 ),
inference(sat_conversion,[],[f149128]) ).
cnf(s6904,plain,
( spl1159_1062
| ~ spl1159_3026 ),
inference(sat_conversion,[],[f165526]) ).
cnf(s6924,plain,
~ spl1159_3026,
inference(rat,[],[s6904,s4049]) ).
cnf(s6926,plain,
~ spl1159_1,
inference(rat,[],[s6315,s6924]) ).
cnf(s6928,plain,
( spl1159_2494
| ~ spl1159_2510 ),
inference(rat,[],[s4011,s4602,s4049]) ).
cnf(s6930,plain,
~ spl1159_2510,
inference(rat,[],[s6928,s3500]) ).
cnf(s6949,plain,
~ spl1159_2,
inference(rat,[],[s3439,s6930]) ).
cnf(s7081,plain,
$false,
inference(rat,[],[s1,s6949,s6926]) ).
fof(f165527,plain,
$false,
inference(avatar_sat_refutation,[],[s7081]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : TOP025+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.25 % Computer : n014.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 18:50:31 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.26/0.31 Running first-order model finding
% 0.26/0.31 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
% 26.99/4.39 % (2054864)Will run a generic schedule for satisfiability detection.
% 26.99/4.39 % (2054869)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3055026934_2997 on theBenchmark for (2997ds/0Mi)
% 26.99/4.39 % (2054870)% WARNING: option uhcvi not known.
% 26.99/4.39 % (2054872)dis+10_1_sil=32000:sp=arity:random_seed=2950100098:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 26.99/4.39 % (2054870)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1785371389:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 26.99/4.39 % (2054873)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1400906605:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 26.99/4.39 % (2054871)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4115188088:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 26.99/4.39 % (2054874)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1292853565:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 26.99/4.39 % (2054875)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=731153044:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 26.99/4.39 % (2054872)Instruction limit reached!
% 26.99/4.39 % (2054872)------------------------------
% 26.99/4.39 % (2054872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2054872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2054872)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2054872)Termination reason: Instruction limit
% 26.99/4.39 % (2054872)Termination phase: Preprocessing 3
% 26.99/4.39 % (2054872)Time elapsed: 0.104 s
% 26.99/4.39 % (2054872)Peak memory usage: 21 MB
% 26.99/4.39 % (2054872)Instructions burned: 103 (million)
% 26.99/4.39 % (2054873)Instruction limit reached!
% 26.99/4.39 % (2054873)------------------------------
% 26.99/4.39 % (2054873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2054873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2054873)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2054873)Termination reason: Instruction limit
% 26.99/4.39 % (2054873)Termination phase: NewCNF
% 26.99/4.39 % (2054873)Time elapsed: 0.120 s
% 26.99/4.39 % (2054873)Peak memory usage: 22 MB
% 26.99/4.39 % (2054873)Instructions burned: 116 (million)
% 26.99/4.39 % (2054883)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2593945925:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 26.99/4.39 % (2054874)Instruction limit reached!
% 26.99/4.39 % (2054874)------------------------------
% 26.99/4.39 % (2054874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2054874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2054874)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2054874)Termination reason: Instruction limit
% 26.99/4.39 % (2054874)Termination phase: Preprocessing 3
% 26.99/4.39 % (2054874)Time elapsed: 0.137 s
% 26.99/4.39 % (2054874)Peak memory usage: 21 MB
% 26.99/4.39 % (2054874)Instructions burned: 131 (million)
% 26.99/4.39 % (2054884)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2199121952:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 26.99/4.39 % (2054886)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=4207357505:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 26.99/4.39 % (2054875)Instruction limit reached!
% 26.99/4.39 % (2054875)------------------------------
% 26.99/4.39 % (2054875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2054875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.99/4.39 % (2054875)CaDiCaL version: 2.1.3
% 26.99/4.39 % (2054875)Termination reason: Instruction limit
% 26.99/4.39 % (2054875)Termination phase: Property scanning
% 26.99/4.39 % (2054875)Time elapsed: 0.173 s
% 26.99/4.39 % (2054875)Peak memory usage: 24 MB
% 26.99/4.39 % (2054875)Instructions burned: 160 (million)
% 26.99/4.39 % (2054889)ott-21_1_sil=16000:fs=off:random_seed=64640833:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 26.99/4.39 % (2054884)Instruction limit reached!
% 26.99/4.39 % (2054884)------------------------------
% 26.99/4.39 % (2054884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.99/4.39 % (2054884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054884)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054884)Termination reason: Instruction limit
% 28.06/7.64 % (2054884)Termination phase: Preprocessing 3
% 28.06/7.64 % (2054884)Time elapsed: 0.135 s
% 28.06/7.64 % (2054884)Peak memory usage: 21 MB
% 28.06/7.64 % (2054884)Instructions burned: 131 (million)
% 28.06/7.64 % (2054891)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3451915018:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 28.06/7.64 % (2054889)Instruction limit reached!
% 28.06/7.64 % (2054889)------------------------------
% 28.06/7.64 % (2054889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054889)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054889)Termination reason: Instruction limit
% 28.06/7.64 % (2054889)Termination phase: Property scanning
% 28.06/7.64 % (2054889)Time elapsed: 0.196 s
% 28.06/7.64 % (2054889)Peak memory usage: 24 MB
% 28.06/7.64 % (2054889)Instructions burned: 180 (million)
% 28.06/7.64 % (2054893)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1121579047:fmbsr=1.3:i=865:ins=25_2992 on theBenchmark for (2992ds/865Mi)
% 28.06/7.64 % (2054886)Instruction limit reached!
% 28.06/7.64 % (2054886)------------------------------
% 28.06/7.64 % (2054886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054886)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054886)Termination reason: Instruction limit
% 28.06/7.64 % (2054886)Termination phase: Saturation
% 28.06/7.64 % (2054886)Time elapsed: 0.505 s
% 28.06/7.64 % (2054886)Peak memory usage: 30 MB
% 28.06/7.64 % (2054886)Instructions burned: 684 (million)
% 28.06/7.64 % (2054895)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2679236390:i=1179_2990 on theBenchmark for (2990ds/1179Mi)
% 28.06/7.64 % (2054883)Instruction limit reached!
% 28.06/7.64 % (2054883)------------------------------
% 28.06/7.64 % (2054883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054883)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054883)Termination reason: Instruction limit
% 28.06/7.64 % (2054883)Termination phase: Finite model building preprocessing
% 28.06/7.64 % (2054883)Time elapsed: 0.593 s
% 28.06/7.64 % (2054883)Peak memory usage: 34 MB
% 28.06/7.64 % (2054883)Instructions burned: 715 (million)
% 28.06/7.64 % (2054897)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1204821950:i=889:ins=1_2989 on theBenchmark for (2989ds/889Mi)
% 28.06/7.64 % (2054891)Instruction limit reached!
% 28.06/7.64 % (2054891)------------------------------
% 28.06/7.64 % (2054891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054891)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054891)Termination reason: Instruction limit
% 28.06/7.64 % (2054891)Termination phase: Saturation
% 28.06/7.64 % (2054891)Time elapsed: 0.445 s
% 28.06/7.64 % (2054891)Peak memory usage: 27 MB
% 28.06/7.64 % (2054891)Instructions burned: 477 (million)
% 28.06/7.64 % (2054899)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=2073489433:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi)
% 28.06/7.64 % (2054893)Instruction limit reached!
% 28.06/7.64 % (2054893)------------------------------
% 28.06/7.64 % (2054893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054893)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054893)Termination reason: Instruction limit
% 28.06/7.64 % (2054893)Termination phase: Finite model building preprocessing
% 28.06/7.64 % (2054893)Time elapsed: 0.735 s
% 28.06/7.64 % (2054893)Peak memory usage: 33 MB
% 28.06/7.64 % (2054893)Instructions burned: 865 (million)
% 28.06/7.64 % (2054901)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1891827585:i=879:kws=inv_precedence:fsr=off_2985 on theBenchmark for (2985ds/879Mi)
% 28.06/7.64 % Detected minimum model sizes of [5]
% 28.06/7.64 % Detected maximum model sizes of [max]
% 28.06/7.64 % TRYING [5]
% 28.06/7.64 % (2054899)Instruction limit reached!
% 28.06/7.64 % (2054899)------------------------------
% 28.06/7.64 % (2054899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054899)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054899)Termination reason: Instruction limit
% 28.06/7.64 % (2054899)Termination phase: Saturation
% 28.06/7.64 % (2054899)Time elapsed: 0.604 s
% 28.06/7.64 % (2054899)Peak memory usage: 31 MB
% 28.06/7.64 % (2054899)Instructions burned: 692 (million)
% 28.06/7.64 % (2054903)fmb+10_1_sil=64000:random_seed=3498503583:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 28.06/7.64 % (2054897)Instruction limit reached!
% 28.06/7.64 % (2054897)------------------------------
% 28.06/7.64 % (2054897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054897)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054897)Termination reason: Instruction limit
% 28.06/7.64 % (2054897)Termination phase: Finite model building preprocessing
% 28.06/7.64 % (2054897)Time elapsed: 0.809 s
% 28.06/7.64 % (2054897)Peak memory usage: 34 MB
% 28.06/7.64 % (2054897)Instructions burned: 889 (million)
% 28.06/7.64 % (2054905)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1388083240:i=9515:nm=5_2981 on theBenchmark for (2981ds/9515Mi)
% 28.06/7.64 % (2054895)Instruction limit reached!
% 28.06/7.64 % (2054895)------------------------------
% 28.06/7.64 % (2054895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054895)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054895)Termination reason: Instruction limit
% 28.06/7.64 % (2054895)Termination phase: Saturation
% 28.06/7.64 % (2054895)Time elapsed: 1.027 s
% 28.06/7.64 % (2054895)Peak memory usage: 40 MB
% 28.06/7.64 % (2054895)Instructions burned: 1180 (million)
% 28.06/7.64 % (2054907)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1812372032:fmbsr=1.7:i=920_2979 on theBenchmark for (2979ds/920Mi)
% 28.06/7.64 % (2054901)Instruction limit reached!
% 28.06/7.64 % (2054901)------------------------------
% 28.06/7.64 % (2054901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054901)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054901)Termination reason: Instruction limit
% 28.06/7.64 % (2054901)Termination phase: Saturation
% 28.06/7.64 % (2054901)Time elapsed: 0.764 s
% 28.06/7.64 % (2054901)Peak memory usage: 36 MB
% 28.06/7.64 % (2054901)Instructions burned: 880 (million)
% 28.06/7.64 % (2054909)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1128750752:i=5131_2977 on theBenchmark for (2977ds/5131Mi)
% 28.06/7.64 % (2054907)Instruction limit reached!
% 28.06/7.64 % (2054907)------------------------------
% 28.06/7.64 % (2054907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054907)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054907)Termination reason: Instruction limit
% 28.06/7.64 % (2054907)Termination phase: Finite model building preprocessing
% 28.06/7.64 % (2054907)Time elapsed: 0.751 s
% 28.06/7.64 % (2054907)Peak memory usage: 34 MB
% 28.06/7.64 % (2054907)Instructions burned: 921 (million)
% 28.06/7.64 % (2054911)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=685474797:i=1472:ins=7:fdi=8:gsp=on_2971 on theBenchmark for (2971ds/1472Mi)
% 28.06/7.64 % Detected minimum model sizes of [5]
% 28.06/7.64 % Detected maximum model sizes of [max]
% 28.06/7.64 % Detected minimum model sizes of [5]
% 28.06/7.64 % Detected maximum model sizes of [max]
% 28.06/7.64 % (2054905)Cannot represent all propositional literals internally
% 28.06/7.64 % (2054905)Refutation not found, incomplete strategy
% 28.06/7.64 % (2054905)------------------------------
% 28.06/7.64 % (2054905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054905)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054905)Termination reason: Refutation not found, incomplete strategy
% 28.06/7.64 % (2054905)Time elapsed: 2.135 s
% 28.06/7.64 % (2054905)Peak memory usage: 59 MB
% 28.06/7.64 % (2054905)Instructions burned: 2470 (million)
% 28.06/7.64 % (2054905)------------------------------
% 28.06/7.64 % (2054905)------------------------------
% 28.06/7.64 % (2054911)Instruction limit reached!
% 28.06/7.64 % (2054911)------------------------------
% 28.06/7.64 % (2054911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054911)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054911)Termination reason: Instruction limit
% 28.06/7.64 % (2054911)Termination phase: Saturation
% 28.06/7.64 % (2054911)Time elapsed: 1.215 s
% 28.06/7.64 % (2054911)Peak memory usage: 35 MB
% 28.06/7.64 % (2054911)Instructions burned: 1473 (million)
% 28.06/7.64 % (2054915)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=278454834:i=6324_2959 on theBenchmark for (2959ds/6324Mi)
% 28.06/7.64 % (2054916)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3477764578:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 28.06/7.64 % (2054916)Instruction limit reached!
% 28.06/7.64 % (2054916)------------------------------
% 28.06/7.64 % (2054916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054916)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054916)Termination reason: Instruction limit
% 28.06/7.64 % (2054916)Termination phase: Finite model building preprocessing
% 28.06/7.64 % (2054916)Time elapsed: 1.676 s
% 28.06/7.64 % (2054916)Peak memory usage: 49 MB
% 28.06/7.64 % (2054916)Instructions burned: 2174 (million)
% 28.06/7.64 % (2054921)ott-2_1_sil=16000:newcnf=on:random_seed=2259870364:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2941 on theBenchmark for (2941ds/869Mi)
% 28.06/7.64 % Detected minimum model sizes of [5]
% 28.06/7.64 % Detected maximum model sizes of [max]
% 28.06/7.64 % (2054915)Cannot represent all propositional literals internally
% 28.06/7.64 % (2054915)Refutation not found, incomplete strategy
% 28.06/7.64 % (2054915)------------------------------
% 28.06/7.64 % (2054915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054915)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054915)Termination reason: Refutation not found, incomplete strategy
% 28.06/7.64 % (2054915)Time elapsed: 2.162 s
% 28.06/7.64 % (2054915)Peak memory usage: 63 MB
% 28.06/7.64 % (2054915)Instructions burned: 2917 (million)
% 28.06/7.64 % (2054921)Instruction limit reached!
% 28.06/7.64 % (2054921)------------------------------
% 28.06/7.64 % (2054921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054921)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054921)Termination reason: Instruction limit
% 28.06/7.64 % (2054921)Termination phase: Saturation
% 28.06/7.64 % (2054921)Time elapsed: 0.436 s
% 28.06/7.64 % (2054921)Peak memory usage: 33 MB
% 28.06/7.64 % (2054921)Instructions burned: 870 (million)
% 28.06/7.64 % (2054915)------------------------------
% 28.06/7.64 % (2054915)------------------------------
% 28.06/7.64 % (2054923)ott+10_1_sil=32000:tgt=ground:random_seed=3243464416:i=5114:av=off_2937 on theBenchmark for (2937ds/5114Mi)
% 28.06/7.64 % (2054924)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1047216480:i=54282_2937 on theBenchmark for (2937ds/54282Mi)
% 28.06/7.64 % (2054909)Instruction limit reached!
% 28.06/7.64 % (2054909)------------------------------
% 28.06/7.64 % (2054909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.64 % (2054909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.64 % (2054909)CaDiCaL version: 2.1.3
% 28.06/7.64 % (2054909)Termination reason: Instruction limit
% 28.06/7.64 % (2054909)Termination phase: Saturation
% 28.06/7.64 % (2054909)Time elapsed: 4.588 s
% 28.06/7.64 % (2054909)Peak memory usage: 67 MB
% 28.06/7.64 % (2054909)Instructions burned: 5131 (million)
% 28.06/7.64 % (2055037)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2809677914:i=3512:aac=none_2930 on theBenchmark for (2930ds/3512Mi)
% 28.06/7.64 % (2054870) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2054864-2054870"...
% 28.06/7.64 % (2054870)...printing done.
% 28.06/7.64 % (2054870)Refutation found. Thanks to Tanya!
% 28.06/7.64 % SZS status Theorem for theBenchmark
% 28.06/7.64 % SZS output start Proof for theBenchmark
% See solution above
% 28.06/7.65 % (2054870)------------------------------
% 28.06/7.65 % (2054870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.06/7.65 % (2054870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.06/7.65 % (2054870)CaDiCaL version: 2.1.3
% 28.06/7.65 % (2054870)Termination reason: Refutation
% 28.06/7.65 % (2054870)Time elapsed: 6.928 s
% 28.06/7.65 % (2054870)Peak memory usage: 86 MB
% 28.06/7.65 % (2054870)Instructions burned: 8178 (million)
% 28.06/7.65 % (2054864)Success in time 7.326 s
% 28.06/7.65 % Vampire exiting
%------------------------------------------------------------------------------