%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG216+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 09:29:48 AM UTC 2026
% Result : Theorem 78.94s 11.79s
% Output : Refutation 78.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 13
% Syntax : Number of formulae : 147 ( 38 unt; 5 def)
% Number of atoms : 905 ( 61 equ)
% Maximal formula atoms : 23 ( 6 avg)
% Number of connectives : 1209 ( 451 ~; 641 |; 92 &)
% ( 5 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 6 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 74 ( 0 sgn 68 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2183,axiom,
! [X0] :
( l2_struct_0(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+200.ax',dt_l2_struct_0) ).
fof(f2315,axiom,
! [X0] :
( l1_rlvect_1(X0)
=> l2_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+210.ax',dt_l1_rlvect_1) ).
fof(f2321,axiom,
! [X0] :
( l2_struct_0(X0)
=> m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+210.ax',dt_k1_rlvect_1) ).
fof(f2743,axiom,
! [X0] :
( l2_vectsp_1(X0)
=> ( l1_vectsp_1(X0)
& l2_struct_0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+213.ax',dt_l2_vectsp_1) ).
fof(f2745,axiom,
! [X0] :
( l3_vectsp_1(X0)
=> ( l1_rlvect_1(X0)
& l2_vectsp_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+213.ax',dt_l3_vectsp_1) ).
fof(f3075,axiom,
! [X0] :
( l1_struct_0(X0)
=> ! [X1] :
( l1_vectsp_2(X1,X0)
=> l1_rlvect_1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+241.ax',dt_l1_vectsp_2) ).
fof(f3448,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( v1_rmod_5(k8_rlvect_2(X1,X2,X3),X0,X1)
=> ( k1_rlvect_1(X0) = k2_group_1(X0)
| ( X2 != k1_rlvect_1(X1)
& X3 != k1_rlvect_1(X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_rmod_5) ).
fof(f3449,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( k1_rlvect_1(X0) != k2_group_1(X0)
=> ( ~ v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
& ~ v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X2),X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_rmod_5) ).
fof(f3450,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( k1_rlvect_1(X0) != k2_group_1(X0)
=> ( ~ v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
& ~ v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X2),X0,X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3449]) ).
fof(f5602,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_struct_0(X0) ),
inference(ennf_transformation,[],[f2183]) ).
fof(f5805,plain,
! [X0] :
( l2_struct_0(X0)
| ~ l1_rlvect_1(X0) ),
inference(ennf_transformation,[],[f2315]) ).
fof(f5811,plain,
! [X0] :
( m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0))
| ~ l2_struct_0(X0) ),
inference(ennf_transformation,[],[f2321]) ).
fof(f6351,plain,
! [X0] :
( ( l1_vectsp_1(X0)
& l2_struct_0(X0) )
| ~ l2_vectsp_1(X0) ),
inference(ennf_transformation,[],[f2743]) ).
fof(f6352,plain,
! [X0] :
( ( l1_rlvect_1(X0)
& l2_vectsp_1(X0) )
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f2745]) ).
fof(f6773,plain,
! [X0] :
( ! [X1] :
( l1_rlvect_1(X1)
| ~ l1_vectsp_2(X1,X0) )
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f3075]) ).
fof(f7337,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| ( X2 != k1_rlvect_1(X1)
& X3 != k1_rlvect_1(X1) )
| ~ v1_rmod_5(k8_rlvect_2(X1,X2,X3),X0,X1)
| ~ m1_subset_1(X3,u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f3448]) ).
fof(f7338,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( k1_rlvect_1(X0) = k2_group_1(X0)
| ( X2 != k1_rlvect_1(X1)
& X3 != k1_rlvect_1(X1) )
| ~ v1_rmod_5(k8_rlvect_2(X1,X2,X3),X0,X1)
| ~ m1_subset_1(X3,u1_struct_0(X1)) )
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_vectsp_2(X1,X0)
| ~ l1_vectsp_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v4_group_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(flattening,[],[f7337]) ).
fof(f7339,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
| v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X2),X0,X1) )
& k1_rlvect_1(X0) != k2_group_1(X0)
& m1_subset_1(X2,u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) ),
inference(ennf_transformation,[],[f3450]) ).
fof(f7340,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
| v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X2),X0,X1) )
& k1_rlvect_1(X0) != k2_group_1(X0)
& m1_subset_1(X2,u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v3_rlvect_1(X1)
& v4_rlvect_1(X1)
& v5_rlvect_1(X1)
& v6_rlvect_1(X1)
& v5_vectsp_2(X1,X0)
& l1_vectsp_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_rlvect_1(X0)
& v4_rlvect_1(X0)
& v5_rlvect_1(X0)
& v6_rlvect_1(X0)
& v4_group_1(X0)
& v6_vectsp_1(X0)
& v7_vectsp_1(X0)
& v8_vectsp_1(X0)
& l3_vectsp_1(X0) ),
inference(flattening,[],[f7339]) ).
fof(f11630,plain,
! [X0] :
( ~ l2_struct_0(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f5602]) ).
fof(f11878,plain,
! [X0] :
( ~ l1_rlvect_1(X0)
| l2_struct_0(X0) ),
inference(cnf_transformation,[],[f5805]) ).
fof(f11884,plain,
! [X0] :
( ~ l2_struct_0(X0)
| m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f5811]) ).
fof(f12625,plain,
! [X0] :
( ~ l2_vectsp_1(X0)
| l2_struct_0(X0) ),
inference(cnf_transformation,[],[f6351]) ).
fof(f12628,plain,
! [X0] :
( ~ l3_vectsp_1(X0)
| l2_vectsp_1(X0) ),
inference(cnf_transformation,[],[f6352]) ).
fof(f13238,plain,
! [X0,X1] :
( ~ l1_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| l1_rlvect_1(X1) ),
inference(cnf_transformation,[],[f6773]) ).
fof(f13794,plain,
! [X2,X3,X0,X1] :
( ~ l3_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_rmod_5(k8_rlvect_2(X1,X2,X3),X0,X1)
| k1_rlvect_1(X1) != X3
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(cnf_transformation,[],[f7338]) ).
fof(f13795,plain,
! [X2,X3,X0,X1] :
( ~ l3_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_rmod_5(k8_rlvect_2(X1,X2,X3),X0,X1)
| k1_rlvect_1(X1) != X2
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(cnf_transformation,[],[f7338]) ).
fof(f13796,plain,
( v1_rmod_5(k8_rlvect_2(sK962,k1_rlvect_1(sK962),sK963),sK961,sK962)
| v1_rmod_5(k8_rlvect_2(sK962,sK963,k1_rlvect_1(sK962)),sK961,sK962) ),
inference(cnf_transformation,[],[f7340]) ).
fof(f13797,plain,
m1_subset_1(sK963,u1_struct_0(sK962)),
inference(cnf_transformation,[],[f7340]) ).
fof(f13798,plain,
k1_rlvect_1(sK961) != k2_group_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13799,plain,
l1_vectsp_2(sK962,sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13800,plain,
v5_vectsp_2(sK962,sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13801,plain,
v6_rlvect_1(sK962),
inference(cnf_transformation,[],[f7340]) ).
fof(f13802,plain,
v5_rlvect_1(sK962),
inference(cnf_transformation,[],[f7340]) ).
fof(f13803,plain,
v4_rlvect_1(sK962),
inference(cnf_transformation,[],[f7340]) ).
fof(f13804,plain,
v3_rlvect_1(sK962),
inference(cnf_transformation,[],[f7340]) ).
fof(f13805,plain,
~ v3_struct_0(sK962),
inference(cnf_transformation,[],[f7340]) ).
fof(f13806,plain,
l3_vectsp_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13807,plain,
v8_vectsp_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13808,plain,
v7_vectsp_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13809,plain,
v6_vectsp_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13810,plain,
v4_group_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13811,plain,
v6_rlvect_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13812,plain,
v5_rlvect_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13813,plain,
v4_rlvect_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13814,plain,
v3_rlvect_1(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f13815,plain,
~ v3_struct_0(sK961),
inference(cnf_transformation,[],[f7340]) ).
fof(f16494,plain,
! [X3,X0,X1] :
( ~ l3_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(k1_rlvect_1(X1),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X3),X0,X1)
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(equality_resolution,[],[f13795]) ).
fof(f16495,plain,
! [X2,X0,X1] :
( ~ l3_vectsp_1(X0)
| ~ v8_vectsp_1(X0)
| ~ v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| ~ v6_rlvect_1(X0)
| ~ v5_rlvect_1(X0)
| ~ v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(k1_rlvect_1(X1),u1_struct_0(X1))
| ~ v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(equality_resolution,[],[f13794]) ).
fof(f20348,plain,
! [X0] :
( l2_struct_0(X0)
| l1_rlvect_1(X0) ),
inference(consistent_polarity_flipping,[],[f11878]) ).
fof(f20352,plain,
! [X0] :
( ~ m1_subset_1(k1_rlvect_1(X0),u1_struct_0(X0))
| ~ l2_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f11884]) ).
fof(f21030,plain,
! [X0] :
( l2_vectsp_1(X0)
| l2_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f12625]) ).
fof(f21033,plain,
! [X0] :
( ~ l2_vectsp_1(X0)
| ~ l3_vectsp_1(X0) ),
inference(consistent_polarity_flipping,[],[f12628]) ).
fof(f21582,plain,
! [X0,X1] :
( ~ l1_rlvect_1(X1)
| ~ l1_vectsp_2(X1,X0)
| ~ l1_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f13238]) ).
fof(f22132,plain,
! [X3,X0,X1] :
( ~ v1_rmod_5(k8_rlvect_2(X1,k1_rlvect_1(X1),X3),X0,X1)
| v8_vectsp_1(X0)
| v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| v6_rlvect_1(X0)
| v5_rlvect_1(X0)
| v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| v6_rlvect_1(X1)
| v5_rlvect_1(X1)
| v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ v3_struct_0(X1)
| m1_subset_1(k1_rlvect_1(X1),u1_struct_0(X1))
| m1_subset_1(X3,u1_struct_0(X1))
| ~ l3_vectsp_1(X0)
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f16494]) ).
fof(f22133,plain,
! [X2,X0,X1] :
( ~ v1_rmod_5(k8_rlvect_2(X1,X2,k1_rlvect_1(X1)),X0,X1)
| v8_vectsp_1(X0)
| v7_vectsp_1(X0)
| ~ v6_vectsp_1(X0)
| ~ v4_group_1(X0)
| v6_rlvect_1(X0)
| v5_rlvect_1(X0)
| v4_rlvect_1(X0)
| ~ v3_rlvect_1(X0)
| ~ v3_struct_0(X0)
| ~ l1_vectsp_2(X1,X0)
| ~ v5_vectsp_2(X1,X0)
| v6_rlvect_1(X1)
| v5_rlvect_1(X1)
| v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ v3_struct_0(X1)
| m1_subset_1(X2,u1_struct_0(X1))
| m1_subset_1(k1_rlvect_1(X1),u1_struct_0(X1))
| ~ l3_vectsp_1(X0)
| k1_rlvect_1(X0) = k2_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f16495]) ).
fof(f22134,plain,
v3_struct_0(sK961),
inference(consistent_polarity_flipping,[],[f13815]) ).
fof(f22135,plain,
~ v4_rlvect_1(sK961),
inference(consistent_polarity_flipping,[],[f13813]) ).
fof(f22136,plain,
~ v5_rlvect_1(sK961),
inference(consistent_polarity_flipping,[],[f13812]) ).
fof(f22137,plain,
~ v6_rlvect_1(sK961),
inference(consistent_polarity_flipping,[],[f13811]) ).
fof(f22138,plain,
~ v7_vectsp_1(sK961),
inference(consistent_polarity_flipping,[],[f13808]) ).
fof(f22139,plain,
~ v8_vectsp_1(sK961),
inference(consistent_polarity_flipping,[],[f13807]) ).
fof(f22140,plain,
v3_struct_0(sK962),
inference(consistent_polarity_flipping,[],[f13805]) ).
fof(f22141,plain,
~ v4_rlvect_1(sK962),
inference(consistent_polarity_flipping,[],[f13803]) ).
fof(f22142,plain,
~ v5_rlvect_1(sK962),
inference(consistent_polarity_flipping,[],[f13802]) ).
fof(f22143,plain,
~ v6_rlvect_1(sK962),
inference(consistent_polarity_flipping,[],[f13801]) ).
fof(f22144,plain,
~ m1_subset_1(sK963,u1_struct_0(sK962)),
inference(consistent_polarity_flipping,[],[f13797]) ).
fof(f22158,definition,
( spl964_1
<=> v1_rmod_5(k8_rlvect_2(sK962,sK963,k1_rlvect_1(sK962)),sK961,sK962) ),
introduced(definition,[new_symbols(definition,[spl964_1])],[avatar_definition]) ).
fof(f22160,plain,
( v1_rmod_5(k8_rlvect_2(sK962,sK963,k1_rlvect_1(sK962)),sK961,sK962)
| ~ spl964_1 ),
inference(avatar_component_clause,[],[f22158]) ).
fof(f22162,definition,
( spl964_2
<=> v1_rmod_5(k8_rlvect_2(sK962,k1_rlvect_1(sK962),sK963),sK961,sK962) ),
introduced(definition,[new_symbols(definition,[spl964_2])],[avatar_definition]) ).
fof(f22164,plain,
( v1_rmod_5(k8_rlvect_2(sK962,k1_rlvect_1(sK962),sK963),sK961,sK962)
| ~ spl964_2 ),
inference(avatar_component_clause,[],[f22162]) ).
fof(f22165,plain,
( spl964_1
| spl964_2 ),
inference(avatar_split_clause,[],[f13796,f22162,f22158]) ).
fof(f25216,plain,
! [X0] :
( l2_struct_0(X0)
| ~ l3_vectsp_1(X0) ),
inference(resolution,[],[f21033,f21030]) ).
fof(f25250,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l3_vectsp_1(X0) ),
inference(resolution,[],[f25216,f11630]) ).
fof(f86583,definition,
( spl964_4330
<=> l1_struct_0(sK961) ),
introduced(definition,[new_symbols(definition,[spl964_4330])],[avatar_definition]) ).
fof(f86585,plain,
( ~ l1_struct_0(sK961)
| spl964_4330 ),
inference(avatar_component_clause,[],[f86583]) ).
fof(f93727,definition,
( spl964_4716
<=> l1_rlvect_1(sK962) ),
introduced(definition,[new_symbols(definition,[spl964_4716])],[avatar_definition]) ).
fof(f93728,plain,
( ~ l1_rlvect_1(sK962)
| spl964_4716 ),
inference(avatar_component_clause,[],[f93727]) ).
fof(f93729,plain,
( l1_rlvect_1(sK962)
| ~ spl964_4716 ),
inference(avatar_component_clause,[],[f93727]) ).
fof(f128920,plain,
( ! [X0] :
( ~ l1_vectsp_2(sK962,X0)
| ~ l1_struct_0(X0) )
| ~ spl964_4716 ),
inference(resolution,[],[f93729,f21582]) ).
fof(f129541,plain,
( ~ l1_struct_0(sK961)
| ~ spl964_4716 ),
inference(resolution,[],[f128920,f13799]) ).
fof(f129542,plain,
( ~ spl964_4330
| ~ spl964_4716 ),
inference(avatar_split_clause,[],[f129541,f93727,f86583]) ).
fof(f129638,plain,
( ~ l3_vectsp_1(sK961)
| spl964_4330 ),
inference(resolution,[],[f86585,f25250]) ).
fof(f129645,plain,
( $false
| spl964_4330 ),
inference(forward_subsumption_resolution,[],[f129638,f13806]) ).
fof(f129646,plain,
spl964_4330,
inference(avatar_contradiction_clause,[],[f129645]) ).
fof(f129935,definition,
( spl964_7125
<=> m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962)) ),
introduced(definition,[new_symbols(definition,[spl964_7125])],[avatar_definition]) ).
fof(f129936,plain,
( ~ m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| spl964_7125 ),
inference(avatar_component_clause,[],[f129935]) ).
fof(f129937,plain,
( m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ spl964_7125 ),
inference(avatar_component_clause,[],[f129935]) ).
fof(f263334,plain,
( v8_vectsp_1(sK961)
| v7_vectsp_1(sK961)
| ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(resolution,[],[f22133,f22160]) ).
fof(f263335,plain,
( v7_vectsp_1(sK961)
| ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263334,f22139]) ).
fof(f263336,plain,
( ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263335,f22138]) ).
fof(f263337,plain,
( ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263336,f13809]) ).
fof(f263338,plain,
( v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263337,f13810]) ).
fof(f263339,plain,
( v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263338,f22137]) ).
fof(f263340,plain,
( v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263339,f22136]) ).
fof(f263341,plain,
( ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263340,f22135]) ).
fof(f263342,plain,
( ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263341,f13814]) ).
fof(f263343,plain,
( ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263342,f22134]) ).
fof(f263344,plain,
( ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263343,f13799]) ).
fof(f263345,plain,
( v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263344,f13800]) ).
fof(f263346,plain,
( v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263345,f22143]) ).
fof(f263347,plain,
( v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263346,f22142]) ).
fof(f263348,plain,
( ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263347,f22141]) ).
fof(f263349,plain,
( ~ v3_struct_0(sK962)
| m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263348,f13804]) ).
fof(f263350,plain,
( m1_subset_1(sK963,u1_struct_0(sK962))
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263349,f22140]) ).
fof(f263351,plain,
( m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263350,f22144]) ).
fof(f263352,plain,
( m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263351,f13806]) ).
fof(f263353,plain,
( m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| ~ spl964_1 ),
inference(forward_subsumption_resolution,[],[f263352,f13798]) ).
fof(f263354,plain,
( spl964_7125
| ~ spl964_1 ),
inference(avatar_split_clause,[],[f263353,f22158,f129935]) ).
fof(f263707,plain,
( ~ l2_struct_0(sK962)
| ~ spl964_7125 ),
inference(resolution,[],[f129937,f20352]) ).
fof(f263724,plain,
( l1_rlvect_1(sK962)
| ~ spl964_7125 ),
inference(resolution,[],[f263707,f20348]) ).
fof(f263725,plain,
( $false
| spl964_4716
| ~ spl964_7125 ),
inference(forward_subsumption_resolution,[],[f263724,f93728]) ).
fof(f263726,plain,
( spl964_4716
| ~ spl964_7125 ),
inference(avatar_contradiction_clause,[],[f263725]) ).
fof(f263734,plain,
( v8_vectsp_1(sK961)
| v7_vectsp_1(sK961)
| ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(resolution,[],[f22164,f22132]) ).
fof(f263739,plain,
( v7_vectsp_1(sK961)
| ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263734,f22139]) ).
fof(f263742,plain,
( ~ v6_vectsp_1(sK961)
| ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263739,f22138]) ).
fof(f263745,plain,
( ~ v4_group_1(sK961)
| v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263742,f13809]) ).
fof(f263748,plain,
( v6_rlvect_1(sK961)
| v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263745,f13810]) ).
fof(f263751,plain,
( v5_rlvect_1(sK961)
| v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263748,f22137]) ).
fof(f263754,plain,
( v4_rlvect_1(sK961)
| ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263751,f22136]) ).
fof(f263757,plain,
( ~ v3_rlvect_1(sK961)
| ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263754,f22135]) ).
fof(f263760,plain,
( ~ v3_struct_0(sK961)
| ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263757,f13814]) ).
fof(f263763,plain,
( ~ l1_vectsp_2(sK962,sK961)
| ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263760,f22134]) ).
fof(f263766,plain,
( ~ v5_vectsp_2(sK962,sK961)
| v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263763,f13799]) ).
fof(f263769,plain,
( v6_rlvect_1(sK962)
| v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263766,f13800]) ).
fof(f263772,plain,
( v5_rlvect_1(sK962)
| v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263769,f22143]) ).
fof(f263775,plain,
( v4_rlvect_1(sK962)
| ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263772,f22142]) ).
fof(f263778,plain,
( ~ v3_rlvect_1(sK962)
| ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263775,f22141]) ).
fof(f263781,plain,
( ~ v3_struct_0(sK962)
| m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263778,f13804]) ).
fof(f263784,plain,
( m1_subset_1(k1_rlvect_1(sK962),u1_struct_0(sK962))
| m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2 ),
inference(forward_subsumption_resolution,[],[f263781,f22140]) ).
fof(f263787,plain,
( m1_subset_1(sK963,u1_struct_0(sK962))
| ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2
| spl964_7125 ),
inference(forward_subsumption_resolution,[],[f263784,f129936]) ).
fof(f263793,plain,
( ~ l3_vectsp_1(sK961)
| k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2
| spl964_7125 ),
inference(forward_subsumption_resolution,[],[f263787,f22144]) ).
fof(f263795,plain,
( k1_rlvect_1(sK961) = k2_group_1(sK961)
| ~ spl964_2
| spl964_7125 ),
inference(forward_subsumption_resolution,[],[f263793,f13806]) ).
fof(f263796,plain,
( $false
| ~ spl964_2
| spl964_7125 ),
inference(forward_subsumption_resolution,[],[f263795,f13798]) ).
fof(f263797,plain,
( ~ spl964_2
| spl964_7125 ),
inference(avatar_contradiction_clause,[],[f263796]) ).
cnf(s1,plain,
( spl964_1
| spl964_2 ),
inference(sat_conversion,[],[f22165]) ).
cnf(s5806,plain,
( ~ spl964_4330
| ~ spl964_4716 ),
inference(sat_conversion,[],[f129542]) ).
cnf(s5821,plain,
spl964_4330,
inference(sat_conversion,[],[f129646]) ).
cnf(s12897,plain,
( ~ spl964_1
| spl964_7125 ),
inference(sat_conversion,[],[f263354]) ).
cnf(s12898,plain,
( spl964_4716
| ~ spl964_7125 ),
inference(sat_conversion,[],[f263726]) ).
cnf(s12902,plain,
( ~ spl964_2
| spl964_7125 ),
inference(sat_conversion,[],[f263797]) ).
cnf(s13246,plain,
~ spl964_4716,
inference(rat,[],[s5806,s5821]) ).
cnf(s13247,plain,
~ spl964_7125,
inference(rat,[],[s12898,s13246]) ).
cnf(s13252,plain,
~ spl964_2,
inference(rat,[],[s12902,s13247]) ).
cnf(s13253,plain,
~ spl964_1,
inference(rat,[],[s12897,s13247]) ).
cnf(s13349,plain,
$false,
inference(rat,[],[s1,s13252,s13253]) ).
fof(f263798,plain,
$false,
inference(avatar_sat_refutation,[],[s13349]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG216+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.30 % Computer : n005.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8046.5625MB
% 0.12/0.30 % OS : Linux 6.8.0-71-generic
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 300
% 0.12/0.30 % DateTime : Mon Sep 28 19:44:47 UTC 2026
% 0.12/0.30 % CPUTime :
% 0.12/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.30/0.36 Running first-order model finding
% 0.30/0.36 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
% 29.32/4.77 % (1084820)Will run a generic schedule for satisfiability detection.
% 29.32/4.77 % (1084830)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2571751860:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 29.32/4.77 % (1084826)% WARNING: option uhcvi not known.
% 29.32/4.77 % (1084826)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3138300202:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 29.32/4.77 % (1084825)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3898211168_2997 on theBenchmark for (2997ds/0Mi)
% 29.32/4.77 % (1084827)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2555718059:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 29.32/4.77 % (1084828)dis+10_1_sil=32000:sp=arity:random_seed=747088706:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 29.32/4.77 % (1084829)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2458222313:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 29.32/4.77 % (1084831)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=465614405:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 29.32/4.77 % (1084830)Instruction limit reached!
% 29.32/4.77 % (1084830)------------------------------
% 29.32/4.77 % (1084830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.32/4.77 % (1084830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.32/4.77 % (1084830)CaDiCaL version: 2.1.3
% 29.32/4.77 % (1084830)Termination reason: Instruction limit
% 29.32/4.77 % (1084830)Termination phase: Clausification
% 29.32/4.77 % (1084830)Time elapsed: 0.078 s
% 29.32/4.77 % (1084830)Peak memory usage: 22 MB
% 29.32/4.77 % (1084830)Instructions burned: 132 (million)
% 29.32/4.77 % (1084828)Instruction limit reached!
% 29.32/4.77 % (1084828)------------------------------
% 29.32/4.77 % (1084828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.32/4.77 % (1084828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.32/4.77 % (1084828)CaDiCaL version: 2.1.3
% 29.32/4.77 % (1084828)Termination reason: Instruction limit
% 29.32/4.77 % (1084828)Termination phase: Preprocessing 3
% 29.32/4.77 % (1084828)Time elapsed: 0.109 s
% 29.32/4.77 % (1084828)Peak memory usage: 20 MB
% 29.32/4.77 % (1084828)Instructions burned: 103 (million)
% 29.32/4.77 % (1084829)Instruction limit reached!
% 29.32/4.77 % (1084829)------------------------------
% 29.32/4.77 % (1084829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.32/4.77 % (1084829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.32/4.77 % (1084829)CaDiCaL version: 2.1.3
% 29.32/4.77 % (1084829)Termination reason: Instruction limit
% 29.32/4.77 % (1084829)Termination phase: NewCNF
% 29.32/4.77 % (1084829)Time elapsed: 0.120 s
% 29.32/4.77 % (1084829)Peak memory usage: 22 MB
% 29.32/4.77 % (1084829)Instructions burned: 116 (million)
% 29.32/4.77 % (1084839)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=537538426:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 29.32/4.77 % (1084840)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1209210142:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 29.32/4.77 % (1084842)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=3337043835:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 29.32/4.77 % (1084831)Instruction limit reached!
% 29.32/4.77 % (1084831)------------------------------
% 29.32/4.77 % (1084831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.32/4.77 % (1084831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.32/4.77 % (1084831)CaDiCaL version: 2.1.3
% 29.32/4.77 % (1084831)Termination reason: Instruction limit
% 29.32/4.77 % (1084831)Termination phase: Property scanning
% 29.32/4.77 % (1084831)Time elapsed: 0.168 s
% 29.32/4.77 % (1084831)Peak memory usage: 22 MB
% 29.32/4.77 % (1084831)Instructions burned: 160 (million)
% 29.32/4.77 % (1084845)ott-21_1_sil=16000:fs=off:random_seed=3709666860:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 29.32/4.77 % (1084840)Instruction limit reached!
% 29.32/4.77 % (1084840)------------------------------
% 29.32/4.77 % (1084840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.32/4.77 % (1084840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084840)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084840)Termination reason: Instruction limit
% 52.98/8.07 % (1084840)Termination phase: Clausification
% 52.98/8.07 % (1084840)Time elapsed: 0.134 s
% 52.98/8.07 % (1084840)Peak memory usage: 22 MB
% 52.98/8.07 % (1084840)Instructions burned: 131 (million)
% 52.98/8.07 % (1084847)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3531322003:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 52.98/8.07 % (1084845)Instruction limit reached!
% 52.98/8.07 % (1084845)------------------------------
% 52.98/8.07 % (1084845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084845)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084845)Termination reason: Instruction limit
% 52.98/8.07 % (1084845)Termination phase: Property scanning
% 52.98/8.07 % (1084845)Time elapsed: 0.178 s
% 52.98/8.07 % (1084845)Peak memory usage: 22 MB
% 52.98/8.07 % (1084845)Instructions burned: 180 (million)
% 52.98/8.07 % (1084849)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2384947499:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 52.98/8.07 % (1084847)Instruction limit reached!
% 52.98/8.07 % (1084847)------------------------------
% 52.98/8.07 % (1084847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084847)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084847)Termination reason: Instruction limit
% 52.98/8.07 % (1084847)Termination phase: Saturation
% 52.98/8.07 % (1084847)Time elapsed: 0.248 s
% 52.98/8.07 % (1084847)Peak memory usage: 26 MB
% 52.98/8.07 % (1084847)Instructions burned: 477 (million)
% 52.98/8.07 % (1084851)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2582290374:i=1179_2991 on theBenchmark for (2991ds/1179Mi)
% 52.98/8.07 % (1084839)Instruction limit reached!
% 52.98/8.07 % (1084839)------------------------------
% 52.98/8.07 % (1084839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084839)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084839)Termination reason: Instruction limit
% 52.98/8.07 % (1084839)Termination phase: Finite model building preprocessing
% 52.98/8.07 % (1084839)Time elapsed: 0.526 s
% 52.98/8.07 % (1084839)Peak memory usage: 32 MB
% 52.98/8.07 % (1084839)Instructions burned: 715 (million)
% 52.98/8.07 % (1084853)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3300949885:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 52.98/8.07 % (1084842)Instruction limit reached!
% 52.98/8.07 % (1084842)------------------------------
% 52.98/8.07 % (1084842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084842)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084842)Termination reason: Instruction limit
% 52.98/8.07 % (1084842)Termination phase: Saturation
% 52.98/8.07 % (1084842)Time elapsed: 0.589 s
% 52.98/8.07 % (1084842)Peak memory usage: 28 MB
% 52.98/8.07 % (1084842)Instructions burned: 685 (million)
% 52.98/8.07 % (1084855)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=4084096858: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)
% 52.98/8.07 % (1084851)Instruction limit reached!
% 52.98/8.07 % (1084851)------------------------------
% 52.98/8.07 % (1084851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084851)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084851)Termination reason: Instruction limit
% 52.98/8.07 % (1084851)Termination phase: Saturation
% 52.98/8.07 % (1084851)Time elapsed: 0.467 s
% 52.98/8.07 % (1084851)Peak memory usage: 40 MB
% 52.98/8.07 % (1084851)Instructions burned: 1180 (million)
% 52.98/8.07 % (1084849)Instruction limit reached!
% 52.98/8.07 % (1084849)------------------------------
% 52.98/8.07 % (1084849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.98/8.07 % (1084849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.07 % (1084849)CaDiCaL version: 2.1.3
% 52.98/8.07 % (1084849)Termination reason: Instruction limit
% 52.98/8.07 % (1084849)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084849)Time elapsed: 0.645 s
% 78.94/11.79 % (1084849)Peak memory usage: 31 MB
% 78.94/11.79 % (1084849)Instructions burned: 865 (million)
% 78.94/11.79 % (1084857)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1720319175:i=879:kws=inv_precedence:fsr=off_2986 on theBenchmark for (2986ds/879Mi)
% 78.94/11.79 % (1084858)fmb+10_1_sil=64000:random_seed=2188895832:i=22061:nm=2:gsp=on_2986 on theBenchmark for (2986ds/22061Mi)
% 78.94/11.79 % (1084857)Instruction limit reached!
% 78.94/11.79 % (1084857)------------------------------
% 78.94/11.79 % (1084857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084857)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084857)Termination reason: Instruction limit
% 78.94/11.79 % (1084857)Termination phase: Saturation
% 78.94/11.79 % (1084857)Time elapsed: 0.229 s
% 78.94/11.79 % (1084857)Peak memory usage: 34 MB
% 78.94/11.79 % (1084857)Instructions burned: 883 (million)
% 78.94/11.79 % (1084861)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2253170452:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 78.94/11.79 % (1084855)Instruction limit reached!
% 78.94/11.79 % (1084855)------------------------------
% 78.94/11.79 % (1084855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084855)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084855)Termination reason: Instruction limit
% 78.94/11.79 % (1084855)Termination phase: Saturation
% 78.94/11.79 % (1084855)Time elapsed: 0.530 s
% 78.94/11.79 % (1084855)Peak memory usage: 32 MB
% 78.94/11.79 % (1084855)Instructions burned: 693 (million)
% 78.94/11.79 % (1084863)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3939622652:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 78.94/11.79 % (1084853)Instruction limit reached!
% 78.94/11.79 % (1084853)------------------------------
% 78.94/11.79 % (1084853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084853)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084853)Termination reason: Instruction limit
% 78.94/11.79 % (1084853)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084853)Time elapsed: 0.686 s
% 78.94/11.79 % (1084853)Peak memory usage: 32 MB
% 78.94/11.79 % (1084853)Instructions burned: 891 (million)
% 78.94/11.79 % (1084865)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2526184809:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 78.94/11.79 % (1084863)Instruction limit reached!
% 78.94/11.79 % (1084863)------------------------------
% 78.94/11.79 % (1084863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084863)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084863)Termination reason: Instruction limit
% 78.94/11.79 % (1084863)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084863)Time elapsed: 0.436 s
% 78.94/11.79 % (1084863)Peak memory usage: 33 MB
% 78.94/11.79 % (1084863)Instructions burned: 921 (million)
% 78.94/11.79 % (1084867)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=58100462:i=1472:ins=7:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/1472Mi)
% 78.94/11.79 % (1084867)Instruction limit reached!
% 78.94/11.79 % (1084867)------------------------------
% 78.94/11.79 % (1084867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084867)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084867)Termination reason: Instruction limit
% 78.94/11.79 % (1084867)Termination phase: Saturation
% 78.94/11.79 % (1084867)Time elapsed: 0.670 s
% 78.94/11.79 % (1084867)Peak memory usage: 33 MB
% 78.94/11.79 % (1084867)Instructions burned: 1474 (million)
% 78.94/11.79 % (1084869)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1897600485:i=6324_2972 on theBenchmark for (2972ds/6324Mi)
% 78.94/11.79 % (1084861)Instruction limit reached!
% 78.94/11.79 % (1084861)------------------------------
% 78.94/11.79 % (1084861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084861)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084861)Termination reason: Instruction limit
% 78.94/11.79 % (1084861)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084861)Time elapsed: 2.787 s
% 78.94/11.79 % (1084861)Peak memory usage: 57 MB
% 78.94/11.79 % (1084861)Instructions burned: 9518 (million)
% 78.94/11.79 % (1084871)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2381039444:fmbsr=2.30978:i=2174_2955 on theBenchmark for (2955ds/2174Mi)
% 78.94/11.79 % (1084865)Instruction limit reached!
% 78.94/11.79 % (1084865)------------------------------
% 78.94/11.79 % (1084865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084865)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084865)Termination reason: Instruction limit
% 78.94/11.79 % (1084865)Termination phase: Saturation
% 78.94/11.79 % (1084865)Time elapsed: 2.904 s
% 78.94/11.79 % (1084865)Peak memory usage: 65 MB
% 78.94/11.79 % (1084865)Instructions burned: 5131 (million)
% 78.94/11.79 % (1084873)ott-2_1_sil=16000:newcnf=on:random_seed=1128291753:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 78.94/11.79 % (1084871)Instruction limit reached!
% 78.94/11.79 % (1084871)------------------------------
% 78.94/11.79 % (1084871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084871)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084871)Termination reason: Instruction limit
% 78.94/11.79 % (1084871)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084871)Time elapsed: 0.499 s
% 78.94/11.79 % (1084871)Peak memory usage: 47 MB
% 78.94/11.79 % (1084871)Instructions burned: 2176 (million)
% 78.94/11.79 % (1084875)ott+10_1_sil=32000:tgt=ground:random_seed=3644549616:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 78.94/11.79 % (1084873)Instruction limit reached!
% 78.94/11.79 % (1084873)------------------------------
% 78.94/11.79 % (1084873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084873)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084873)Termination reason: Instruction limit
% 78.94/11.79 % (1084873)Termination phase: Saturation
% 78.94/11.79 % (1084873)Time elapsed: 0.419 s
% 78.94/11.79 % (1084873)Peak memory usage: 33 MB
% 78.94/11.79 % (1084873)Instructions burned: 870 (million)
% 78.94/11.79 % (1084877)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4171645259:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 78.94/11.79 % (1084869)Instruction limit reached!
% 78.94/11.79 % (1084869)------------------------------
% 78.94/11.79 % (1084869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084869)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084869)Termination reason: Instruction limit
% 78.94/11.79 % (1084869)Termination phase: Finite model building preprocessing
% 78.94/11.79 % (1084869)Time elapsed: 3.371 s
% 78.94/11.79 % (1084869)Peak memory usage: 52 MB
% 78.94/11.79 % (1084869)Instructions burned: 6326 (million)
% 78.94/11.79 % (1084879)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3531169718:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi)
% 78.94/11.79 % (1084875)Instruction limit reached!
% 78.94/11.79 % (1084875)------------------------------
% 78.94/11.79 % (1084875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084875)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084875)Termination reason: Instruction limit
% 78.94/11.79 % (1084875)Termination phase: Saturation
% 78.94/11.79 % (1084875)Time elapsed: 1.656 s
% 78.94/11.79 % (1084875)Peak memory usage: 86 MB
% 78.94/11.79 % (1084875)Instructions burned: 5115 (million)
% 78.94/11.79 % (1084881)dis+21_1_sil=32000:sas=cadical:random_seed=1672096058:i=3773:amm=off_2934 on theBenchmark for (2934ds/3773Mi)
% 78.94/11.79 % (1084881)Instruction limit reached!
% 78.94/11.79 % (1084881)------------------------------
% 78.94/11.79 % (1084881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084881)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084881)Termination reason: Instruction limit
% 78.94/11.79 % (1084881)Termination phase: Saturation
% 78.94/11.79 % (1084881)Time elapsed: 1.095 s
% 78.94/11.79 % (1084881)Peak memory usage: 61 MB
% 78.94/11.79 % (1084881)Instructions burned: 3777 (million)
% 78.94/11.79 % (1084883)ott+11_1_sil=16000:gs=on:random_seed=1485508821:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2922 on theBenchmark for (2922ds/2251Mi)
% 78.94/11.79 % (1084879)Instruction limit reached!
% 78.94/11.79 % (1084879)------------------------------
% 78.94/11.79 % (1084879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084879)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084879)Termination reason: Instruction limit
% 78.94/11.79 % (1084879)Termination phase: Saturation
% 78.94/11.79 % (1084879)Time elapsed: 1.867 s
% 78.94/11.79 % (1084879)Peak memory usage: 52 MB
% 78.94/11.79 % (1084879)Instructions burned: 3514 (million)
% 78.94/11.79 % (1084885)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2201768266:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 78.94/11.79 % (1084883)Instruction limit reached!
% 78.94/11.79 % (1084883)------------------------------
% 78.94/11.79 % (1084883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084883)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084883)Termination reason: Instruction limit
% 78.94/11.79 % (1084883)Termination phase: Saturation
% 78.94/11.79 % (1084883)Time elapsed: 0.705 s
% 78.94/11.79 % (1084883)Peak memory usage: 58 MB
% 78.94/11.79 % (1084883)Instructions burned: 2254 (million)
% 78.94/11.79 % (1084887)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2025361213:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2915 on theBenchmark for (2915ds/4591Mi)
% 78.94/11.79 % (1084887)Instruction limit reached!
% 78.94/11.79 % (1084887)------------------------------
% 78.94/11.79 % (1084887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.79 % (1084887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.79 % (1084887)CaDiCaL version: 2.1.3
% 78.94/11.79 % (1084887)Termination reason: Instruction limit
% 78.94/11.79 % (1084887)Termination phase: Saturation
% 78.94/11.79 % (1084887)Time elapsed: 0.971 s
% 78.94/11.79 % (1084887)Peak memory usage: 38 MB
% 78.94/11.79 % (1084887)Instructions burned: 4596 (million)
% 78.94/11.79 % (1084889)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=698746377:i=29340_2905 on theBenchmark for (2905ds/29340Mi)
% 78.94/11.79 % (1084826) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1084820-1084826"...
% 78.94/11.79 % (1084826)...printing done.
% 78.94/11.79 % (1084826)Refutation found. Thanks to Tanya!
% 78.94/11.79 % SZS status Theorem for theBenchmark
% 78.94/11.79 % SZS output start Proof for theBenchmark
% See solution above
% 78.94/11.80 % (1084826)------------------------------
% 78.94/11.80 % (1084826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.94/11.80 % (1084826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.94/11.80 % (1084826)CaDiCaL version: 2.1.3
% 78.94/11.80 % (1084826)Termination reason: Refutation
% 78.94/11.80 % (1084826)Time elapsed: 11.074 s
% 78.94/11.80 % (1084826)Peak memory usage: 144 MB
% 78.94/11.80 % (1084826)Instructions burned: 19895 (million)
% 78.94/11.80 % (1084820)Success in time 11.417 s
% 78.94/11.80 % Vampire exiting
%------------------------------------------------------------------------------