%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT319+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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:24 AM UTC 2026
% Result : Theorem 134.65s 24.55s
% Output : Refutation 134.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 31
% Syntax : Number of formulae : 298 ( 24 unt; 17 def)
% Number of atoms : 1377 ( 21 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1865 ( 786 ~; 869 |; 157 &)
% ( 31 <=>; 20 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 18 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-1 aty)
% Number of variables : 92 ( 0 sgn 90 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2324,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v13_lattices(X0)
& v14_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v15_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc3_lattices) ).
fof(f2328,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc5_lattices) ).
fof(f2329,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v17_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+205.ax',cc6_lattices) ).
fof(f2564,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',fc1_lattice2) ).
fof(f2569,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',fc6_lattice2) ).
fof(f2597,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t18_lattice2) ).
fof(f2615,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( r6_binop_1(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
=> v11_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t36_lattice2) ).
fof(f2616,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
=> r6_binop_1(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t37_lattice2) ).
fof(f2644,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t63_lattice2) ).
fof(f2645,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t64_lattice2) ).
fof(f2646,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',t65_lattice2) ).
fof(f2669,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET007/SET007+253.ax',dt_k1_lattice2) ).
fof(f2986,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t53_filter_2) ).
fof(f2987,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f2988,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f2987]) ).
fof(f5295,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2324]) ).
fof(f5296,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v15_lattices(X0) )
| v3_struct_0(X0)
| ~ v13_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5295]) ).
fof(f5299,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2328]) ).
fof(f5300,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5299]) ).
fof(f5301,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2329]) ).
fof(f5302,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ v16_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5301]) ).
fof(f5674,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f5675,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5674]) ).
fof(f5684,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2569]) ).
fof(f5685,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5684]) ).
fof(f5725,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2597]) ).
fof(f5726,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5725]) ).
fof(f5757,plain,
! [X0] :
( v11_lattices(X0)
| ~ r6_binop_1(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2615]) ).
fof(f5758,plain,
! [X0] :
( v11_lattices(X0)
| ~ r6_binop_1(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5757]) ).
fof(f5759,plain,
! [X0] :
( r6_binop_1(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2616]) ).
fof(f5760,plain,
! [X0] :
( r6_binop_1(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5759]) ).
fof(f5813,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2644]) ).
fof(f5814,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5813]) ).
fof(f5815,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2645]) ).
fof(f5816,plain,
! [X0] :
( ( v14_lattices(X0)
<=> v13_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5815]) ).
fof(f5817,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2646]) ).
fof(f5818,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v11_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5817]) ).
fof(f5861,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6295,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2986]) ).
fof(f6296,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6295]) ).
fof(f6297,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2988]) ).
fof(f6298,plain,
? [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<~> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6297]) ).
fof(f10649,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v13_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f5296]) ).
fof(f10679,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f5300]) ).
fof(f10680,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f5300]) ).
fof(f10681,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v14_lattices(X0) ),
inference(cnf_transformation,[],[f5300]) ).
fof(f10682,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(X0) ),
inference(cnf_transformation,[],[f5300]) ).
fof(f10683,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v11_lattices(X0) ),
inference(cnf_transformation,[],[f5300]) ).
fof(f10684,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| v17_lattices(X0) ),
inference(cnf_transformation,[],[f5302]) ).
fof(f11167,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5675]) ).
fof(f11188,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5685]) ).
fof(f11293,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5726]) ).
fof(f11294,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5726]) ).
fof(f11295,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5726]) ).
fof(f11315,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ r6_binop_1(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v11_lattices(X0) ),
inference(cnf_transformation,[],[f5758]) ).
fof(f11316,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| r6_binop_1(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f5760]) ).
fof(f11358,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ),
inference(cnf_transformation,[],[f5814]) ).
fof(f11360,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(k1_lattice2(X0))
| ~ v14_lattices(X0) ),
inference(cnf_transformation,[],[f5816]) ).
fof(f11361,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v11_lattices(X0) ),
inference(cnf_transformation,[],[f5818]) ).
fof(f11407,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5861]) ).
fof(f11928,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f6296]) ).
fof(f11929,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f6296]) ).
fof(f11931,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[],[f6296]) ).
fof(f11944,plain,
( v17_lattices(k1_lattice2(sK970))
| v17_lattices(sK970) ),
inference(cnf_transformation,[],[f6298]) ).
fof(f11951,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ v17_lattices(k1_lattice2(sK970))
| ~ v10_lattices(k1_lattice2(sK970))
| v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(sK970)
| ~ v17_lattices(sK970)
| ~ v10_lattices(sK970)
| v3_struct_0(sK970) ),
inference(cnf_transformation,[],[f6298]) ).
fof(f11952,plain,
l3_lattices(sK970),
inference(cnf_transformation,[],[f6298]) ).
fof(f11953,plain,
v10_lattices(sK970),
inference(cnf_transformation,[],[f6298]) ).
fof(f11954,plain,
~ v3_struct_0(sK970),
inference(cnf_transformation,[],[f6298]) ).
fof(f17254,plain,
! [X0] :
( v15_lattices(X0)
| v14_lattices(X0)
| ~ v13_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10649]) ).
fof(f17267,plain,
! [X0] :
( v11_lattices(X0)
| ~ v17_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10683]) ).
fof(f17268,plain,
! [X0] :
( v13_lattices(X0)
| ~ v17_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10682]) ).
fof(f17269,plain,
! [X0] :
( ~ v14_lattices(X0)
| ~ v17_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10681]) ).
fof(f17270,plain,
! [X0] :
( v15_lattices(X0)
| ~ v17_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10680]) ).
fof(f17271,plain,
! [X0] :
( v16_lattices(X0)
| ~ v17_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10679]) ).
fof(f17272,plain,
! [X0] :
( ~ v16_lattices(X0)
| ~ l3_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| ~ v3_struct_0(X0)
| v17_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f10684]) ).
fof(f17731,plain,
! [X0] :
( v3_struct_0(k1_lattice2(X0))
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11167]) ).
fof(f17761,plain,
! [X0] :
( ~ v10_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11188]) ).
fof(f17843,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f11295]) ).
fof(f17844,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| u2_lattices(X0) = u1_lattices(k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f11294]) ).
fof(f17845,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_struct_0(X0)
| u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f11293]) ).
fof(f17865,plain,
! [X0] :
( ~ r6_binop_1(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| v11_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11315]) ).
fof(f17866,plain,
! [X0] :
( ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| r6_binop_1(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(consistent_polarity_flipping,[],[f11316]) ).
fof(f17907,plain,
! [X0] :
( ~ v14_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v13_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11358]) ).
fof(f17909,plain,
! [X0] :
( v13_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| v14_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11360]) ).
fof(f17915,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| v10_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v11_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11361]) ).
fof(f18441,plain,
! [X0] :
( v16_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f11931]) ).
fof(f18443,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| v10_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v16_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11929]) ).
fof(f18444,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| v10_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v15_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f11928]) ).
fof(f18445,plain,
v3_struct_0(sK970),
inference(consistent_polarity_flipping,[],[f11954]) ).
fof(f18446,plain,
~ v10_lattices(sK970),
inference(consistent_polarity_flipping,[],[f11953]) ).
fof(f18447,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ v17_lattices(k1_lattice2(sK970))
| v10_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(sK970)
| ~ v17_lattices(sK970)
| v10_lattices(sK970)
| ~ v3_struct_0(sK970) ),
inference(consistent_polarity_flipping,[],[f11951]) ).
fof(f18469,definition,
( spl971_1
<=> v3_struct_0(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_1])],[avatar_definition]) ).
fof(f18471,plain,
( v3_struct_0(sK970)
| ~ spl971_1 ),
inference(avatar_component_clause,[],[f18469]) ).
fof(f18473,definition,
( spl971_2
<=> l3_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_2])],[avatar_definition]) ).
fof(f18474,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| spl971_2 ),
inference(avatar_component_clause,[],[f18473]) ).
fof(f18475,plain,
( l3_lattices(k1_lattice2(sK970))
| ~ spl971_2 ),
inference(avatar_component_clause,[],[f18473]) ).
fof(f18478,definition,
( spl971_3
<=> v17_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_3])],[avatar_definition]) ).
fof(f18480,plain,
( v17_lattices(k1_lattice2(sK970))
| ~ spl971_3 ),
inference(avatar_component_clause,[],[f18478]) ).
fof(f18483,definition,
( spl971_4
<=> v10_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_4])],[avatar_definition]) ).
fof(f18484,plain,
( v10_lattices(k1_lattice2(sK970))
| ~ spl971_4 ),
inference(avatar_component_clause,[],[f18483]) ).
fof(f18485,plain,
( ~ v10_lattices(k1_lattice2(sK970))
| spl971_4 ),
inference(avatar_component_clause,[],[f18483]) ).
fof(f18488,definition,
( spl971_5
<=> v3_struct_0(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_5])],[avatar_definition]) ).
fof(f18489,plain,
( ~ v3_struct_0(k1_lattice2(sK970))
| spl971_5 ),
inference(avatar_component_clause,[],[f18488]) ).
fof(f18490,plain,
( v3_struct_0(k1_lattice2(sK970))
| ~ spl971_5 ),
inference(avatar_component_clause,[],[f18488]) ).
fof(f18493,definition,
( spl971_6
<=> v10_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_6])],[avatar_definition]) ).
fof(f18495,plain,
( ~ v10_lattices(sK970)
| spl971_6 ),
inference(avatar_component_clause,[],[f18493]) ).
fof(f18501,definition,
( spl971_7
<=> v17_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_7])],[avatar_definition]) ).
fof(f18503,plain,
( v17_lattices(sK970)
| ~ spl971_7 ),
inference(avatar_component_clause,[],[f18501]) ).
fof(f18505,plain,
( spl971_7
| spl971_3 ),
inference(avatar_split_clause,[],[f11944,f18478,f18501]) ).
fof(f18509,definition,
( spl971_8
<=> l3_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_8])],[avatar_definition]) ).
fof(f18511,plain,
( l3_lattices(sK970)
| ~ spl971_8 ),
inference(avatar_component_clause,[],[f18509]) ).
fof(f18516,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_5
| spl971_4
| ~ spl971_3
| ~ spl971_2 ),
inference(avatar_split_clause,[],[f18447,f18473,f18478,f18483,f18488,f18509,f18501,f18493,f18469]) ).
fof(f18517,plain,
spl971_8,
inference(avatar_split_clause,[],[f11952,f18509]) ).
fof(f18518,plain,
~ spl971_6,
inference(avatar_split_clause,[],[f18446,f18493]) ).
fof(f18519,plain,
spl971_1,
inference(avatar_split_clause,[],[f18445,f18469]) ).
fof(f20840,plain,
( ~ l3_lattices(sK970)
| spl971_2 ),
inference(resolution,[],[f11407,f18474]) ).
fof(f20841,plain,
( $false
| spl971_2
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f20840,f18511]) ).
fof(f20842,plain,
( spl971_2
| ~ spl971_8 ),
inference(avatar_contradiction_clause,[],[f20841]) ).
fof(f33067,plain,
( ~ v3_struct_0(sK970)
| u1_struct_0(k1_lattice2(sK970)) = u1_struct_0(sK970)
| ~ spl971_8 ),
inference(resolution,[],[f17843,f18511]) ).
fof(f33068,plain,
( u1_struct_0(k1_lattice2(sK970)) = u1_struct_0(sK970)
| ~ spl971_1
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f33067,f18471]) ).
fof(f33103,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| spl971_5 ),
inference(resolution,[],[f18489,f17731]) ).
fof(f33104,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_5 ),
inference(forward_subsumption_resolution,[],[f33103,f18471]) ).
fof(f33105,plain,
( $false
| ~ spl971_1
| spl971_5
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f33104,f18511]) ).
fof(f33106,plain,
( ~ spl971_1
| spl971_5
| ~ spl971_8 ),
inference(avatar_contradiction_clause,[],[f33105]) ).
fof(f33122,plain,
( ~ v3_struct_0(sK970)
| u2_lattices(sK970) = u1_lattices(k1_lattice2(sK970))
| ~ spl971_8 ),
inference(resolution,[],[f17844,f18511]) ).
fof(f33123,plain,
( u2_lattices(sK970) = u1_lattices(k1_lattice2(sK970))
| ~ spl971_1
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f33122,f18471]) ).
fof(f33161,plain,
( ~ v3_struct_0(sK970)
| u2_lattices(k1_lattice2(sK970)) = u1_lattices(sK970)
| ~ spl971_8 ),
inference(resolution,[],[f17845,f18511]) ).
fof(f33162,plain,
( u2_lattices(k1_lattice2(sK970)) = u1_lattices(sK970)
| ~ spl971_1
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f33161,f18471]) ).
fof(f33256,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_4 ),
inference(resolution,[],[f18484,f17761]) ).
fof(f33257,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_4
| spl971_6 ),
inference(forward_subsumption_resolution,[],[f33256,f18495]) ).
fof(f33258,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| ~ spl971_4
| spl971_6 ),
inference(forward_subsumption_resolution,[],[f33257,f18471]) ).
fof(f33259,plain,
( $false
| ~ spl971_1
| ~ spl971_4
| spl971_6
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f33258,f18511]) ).
fof(f33260,plain,
( ~ spl971_1
| ~ spl971_4
| spl971_6
| ~ spl971_8 ),
inference(avatar_contradiction_clause,[],[f33259]) ).
fof(f39408,definition,
( spl971_1634
<=> v11_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_1634])],[avatar_definition]) ).
fof(f39409,plain,
( ~ v11_lattices(k1_lattice2(sK970))
| spl971_1634 ),
inference(avatar_component_clause,[],[f39408]) ).
fof(f39410,plain,
( v11_lattices(k1_lattice2(sK970))
| ~ spl971_1634 ),
inference(avatar_component_clause,[],[f39408]) ).
fof(f39504,definition,
( spl971_1643
<=> v13_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_1643])],[avatar_definition]) ).
fof(f39505,plain,
( v13_lattices(k1_lattice2(sK970))
| ~ spl971_1643 ),
inference(avatar_component_clause,[],[f39504]) ).
fof(f39506,plain,
( ~ v13_lattices(k1_lattice2(sK970))
| spl971_1643 ),
inference(avatar_component_clause,[],[f39504]) ).
fof(f39528,definition,
( spl971_1647
<=> v14_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_1647])],[avatar_definition]) ).
fof(f39529,plain,
( ~ v14_lattices(k1_lattice2(sK970))
| spl971_1647 ),
inference(avatar_component_clause,[],[f39528]) ).
fof(f39530,plain,
( v14_lattices(k1_lattice2(sK970))
| ~ spl971_1647 ),
inference(avatar_component_clause,[],[f39528]) ).
fof(f39552,definition,
( spl971_1651
<=> v16_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_1651])],[avatar_definition]) ).
fof(f39553,plain,
( ~ v16_lattices(k1_lattice2(sK970))
| spl971_1651 ),
inference(avatar_component_clause,[],[f39552]) ).
fof(f39554,plain,
( v16_lattices(k1_lattice2(sK970))
| ~ spl971_1651 ),
inference(avatar_component_clause,[],[f39552]) ).
fof(f49383,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| v14_lattices(sK970)
| spl971_1643 ),
inference(resolution,[],[f39506,f17909]) ).
fof(f49385,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| v14_lattices(sK970)
| spl971_6
| spl971_1643 ),
inference(forward_subsumption_resolution,[],[f49383,f18495]) ).
fof(f49386,plain,
( ~ l3_lattices(sK970)
| v14_lattices(sK970)
| ~ spl971_1
| spl971_6
| spl971_1643 ),
inference(forward_subsumption_resolution,[],[f49385,f18471]) ).
fof(f49387,plain,
( v14_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1643 ),
inference(forward_subsumption_resolution,[],[f49386,f18511]) ).
fof(f49437,plain,
( ~ v17_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1643 ),
inference(resolution,[],[f49387,f17269]) ).
fof(f49448,plain,
( ~ v17_lattices(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1643 ),
inference(forward_subsumption_resolution,[],[f49437,f18471]) ).
fof(f49451,plain,
( ~ v17_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1643 ),
inference(forward_subsumption_resolution,[],[f49448,f18511]) ).
fof(f49454,plain,
( ~ spl971_7
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1643 ),
inference(avatar_split_clause,[],[f49451,f39504,f18509,f18493,f18469,f18501]) ).
fof(f67281,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v13_lattices(sK970)
| ~ spl971_1647 ),
inference(resolution,[],[f39530,f17907]) ).
fof(f67289,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v13_lattices(sK970)
| spl971_6
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67281,f18495]) ).
fof(f67293,plain,
( ~ l3_lattices(sK970)
| ~ v13_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67289,f18471]) ).
fof(f67296,plain,
( ~ v13_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67293,f18511]) ).
fof(f67298,plain,
( ~ v17_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1647 ),
inference(resolution,[],[f67296,f17268]) ).
fof(f67299,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67298,f18503]) ).
fof(f67300,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67299,f18471]) ).
fof(f67301,plain,
( $false
| ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_1647 ),
inference(forward_subsumption_resolution,[],[f67300,f18511]) ).
fof(f67302,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_1647 ),
inference(avatar_contradiction_clause,[],[f67301]) ).
fof(f67420,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u2_lattices(k1_lattice2(sK970)),u1_lattices(k1_lattice2(sK970)))
| v10_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| ~ spl971_8 ),
inference(superposition,[],[f17865,f33068]) ).
fof(f67433,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u2_lattices(k1_lattice2(sK970)),u1_lattices(k1_lattice2(sK970)))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| spl971_4
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f67420,f18485]) ).
fof(f67440,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u2_lattices(k1_lattice2(sK970)),u1_lattices(k1_lattice2(sK970)))
| ~ l3_lattices(k1_lattice2(sK970))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| spl971_4
| ~ spl971_5
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f67433,f18490]) ).
fof(f67447,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u2_lattices(k1_lattice2(sK970)),u1_lattices(k1_lattice2(sK970)))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| ~ spl971_2
| spl971_4
| ~ spl971_5
| ~ spl971_8 ),
inference(forward_subsumption_resolution,[],[f67440,f18475]) ).
fof(f67458,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u2_lattices(k1_lattice2(sK970)),u2_lattices(sK970))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| ~ spl971_2
| spl971_4
| ~ spl971_5
| ~ spl971_8 ),
inference(forward_demodulation,[],[f67447,f33123]) ).
fof(f67464,plain,
( ~ r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970))
| v11_lattices(k1_lattice2(sK970))
| ~ spl971_1
| ~ spl971_2
| spl971_4
| ~ spl971_5
| ~ spl971_8 ),
inference(forward_demodulation,[],[f67458,f33162]) ).
fof(f67471,definition,
( spl971_2595
<=> r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_2595])],[avatar_definition]) ).
fof(f67478,plain,
( spl971_1634
| ~ spl971_2595
| ~ spl971_1
| ~ spl971_2
| spl971_4
| ~ spl971_5
| ~ spl971_8 ),
inference(avatar_split_clause,[],[f67464,f18509,f18488,f18483,f18473,f18469,f67471,f39408]) ).
fof(f123580,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v11_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f17915,f17761]) ).
fof(f123581,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v11_lattices(k1_lattice2(X0))
| v11_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f123580,f17731]) ).
fof(f123582,plain,
! [X0] :
( ~ v11_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| v11_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f123581,f11407]) ).
fof(f123879,definition,
( spl971_5529
<=> v11_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_5529])],[avatar_definition]) ).
fof(f123880,plain,
( v11_lattices(sK970)
| ~ spl971_5529 ),
inference(avatar_component_clause,[],[f123879]) ).
fof(f123881,plain,
( ~ v11_lattices(sK970)
| spl971_5529 ),
inference(avatar_component_clause,[],[f123879]) ).
fof(f123910,plain,
( ~ v17_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| spl971_5529 ),
inference(resolution,[],[f123881,f17267]) ).
fof(f123911,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_7
| spl971_5529 ),
inference(forward_subsumption_resolution,[],[f123910,f18503]) ).
fof(f123913,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| ~ spl971_7
| spl971_5529 ),
inference(forward_subsumption_resolution,[],[f123911,f18471]) ).
fof(f123915,plain,
( $false
| ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_5529 ),
inference(forward_subsumption_resolution,[],[f123913,f18511]) ).
fof(f123916,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_5529 ),
inference(avatar_contradiction_clause,[],[f123915]) ).
fof(f124376,plain,
( ~ l3_lattices(sK970)
| v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970))
| ~ spl971_5529 ),
inference(resolution,[],[f123880,f17866]) ).
fof(f124379,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970))
| ~ spl971_8
| ~ spl971_5529 ),
inference(forward_subsumption_resolution,[],[f124376,f18511]) ).
fof(f124382,plain,
( ~ v3_struct_0(sK970)
| r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970))
| spl971_6
| ~ spl971_8
| ~ spl971_5529 ),
inference(forward_subsumption_resolution,[],[f124379,f18495]) ).
fof(f124385,plain,
( r6_binop_1(u1_struct_0(sK970),u1_lattices(sK970),u2_lattices(sK970))
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_5529 ),
inference(forward_subsumption_resolution,[],[f124382,f18471]) ).
fof(f124388,plain,
( spl971_2595
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_5529 ),
inference(avatar_split_clause,[],[f124385,f123879,f18509,f18493,f18469,f67471]) ).
fof(f124607,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| v11_lattices(sK970)
| ~ spl971_1634 ),
inference(resolution,[],[f39410,f123582]) ).
fof(f161052,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v16_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f18443,f17761]) ).
fof(f161053,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| v16_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f161052,f17731]) ).
fof(f161054,plain,
! [X0] :
( ~ v16_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v15_lattices(k1_lattice2(X0))
| v16_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f161053,f11407]) ).
fof(f161072,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| ~ v3_struct_0(k1_lattice2(X0))
| v15_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f18444,f17761]) ).
fof(f161073,plain,
! [X0] :
( ~ l3_lattices(X0)
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(k1_lattice2(X0))
| ~ v16_lattices(k1_lattice2(X0))
| ~ v15_lattices(k1_lattice2(X0))
| v15_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f161072,f17731]) ).
fof(f161074,plain,
! [X0] :
( ~ v16_lattices(k1_lattice2(X0))
| v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v15_lattices(k1_lattice2(X0))
| v15_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f161073,f11407]) ).
fof(f356418,definition,
( spl971_18641
<=> v16_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_18641])],[avatar_definition]) ).
fof(f356419,plain,
( ~ v16_lattices(sK970)
| spl971_18641 ),
inference(avatar_component_clause,[],[f356418]) ).
fof(f356420,plain,
( v16_lattices(sK970)
| ~ spl971_18641 ),
inference(avatar_component_clause,[],[f356418]) ).
fof(f390127,definition,
( spl971_19071
<=> v15_lattices(sK970) ),
introduced(definition,[new_symbols(definition,[spl971_19071])],[avatar_definition]) ).
fof(f390129,plain,
( ~ v15_lattices(sK970)
| spl971_19071 ),
inference(avatar_component_clause,[],[f390127]) ).
fof(f391747,plain,
( ~ v17_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| spl971_18641 ),
inference(resolution,[],[f356419,f17271]) ).
fof(f391783,plain,
( ~ v17_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| spl971_1634 ),
inference(resolution,[],[f39409,f17267]) ).
fof(f391784,plain,
( ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_3
| spl971_1634 ),
inference(forward_subsumption_resolution,[],[f391783,f18480]) ).
fof(f391786,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_3
| ~ spl971_5
| spl971_1634 ),
inference(forward_subsumption_resolution,[],[f391784,f18490]) ).
fof(f391788,plain,
( $false
| ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_1634 ),
inference(forward_subsumption_resolution,[],[f391786,f18475]) ).
fof(f391789,plain,
( ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_1634 ),
inference(avatar_contradiction_clause,[],[f391788]) ).
fof(f391880,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| v11_lattices(sK970)
| spl971_6
| ~ spl971_1634 ),
inference(forward_subsumption_resolution,[],[f124607,f18495]) ).
fof(f392108,plain,
( ~ l3_lattices(sK970)
| v11_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_1634 ),
inference(forward_subsumption_resolution,[],[f391880,f18471]) ).
fof(f392301,plain,
( v11_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1634 ),
inference(forward_subsumption_resolution,[],[f392108,f18511]) ).
fof(f392852,plain,
( spl971_5529
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1634 ),
inference(avatar_split_clause,[],[f392301,f39408,f18509,f18493,f18469,f123879]) ).
fof(f450904,definition,
( spl971_21243
<=> v15_lattices(k1_lattice2(sK970)) ),
introduced(definition,[new_symbols(definition,[spl971_21243])],[avatar_definition]) ).
fof(f450906,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| spl971_21243 ),
inference(avatar_component_clause,[],[f450904]) ).
fof(f451052,plain,
( ~ l3_lattices(sK970)
| ~ v16_lattices(sK970)
| ~ v15_lattices(sK970)
| v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| spl971_1651 ),
inference(resolution,[],[f39553,f18441]) ).
fof(f451053,plain,
( ~ v17_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| spl971_1651 ),
inference(resolution,[],[f39553,f17271]) ).
fof(f451143,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v15_lattices(sK970)
| ~ spl971_1651 ),
inference(resolution,[],[f39554,f161074]) ).
fof(f451144,plain,
( v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v16_lattices(sK970)
| ~ spl971_1651 ),
inference(resolution,[],[f39554,f161054]) ).
fof(f451145,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ v15_lattices(k1_lattice2(sK970))
| ~ v11_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| v17_lattices(k1_lattice2(sK970))
| ~ spl971_1651 ),
inference(resolution,[],[f39554,f17272]) ).
fof(f451158,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v16_lattices(sK970)
| spl971_6
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451144,f18495]) ).
fof(f451159,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v15_lattices(sK970)
| spl971_6
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451143,f18495]) ).
fof(f451166,plain,
( ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v16_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451158,f18471]) ).
fof(f451167,plain,
( ~ l3_lattices(sK970)
| ~ v15_lattices(k1_lattice2(sK970))
| v15_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451159,f18471]) ).
fof(f451174,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| v16_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451166,f18511]) ).
fof(f451175,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| v15_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451167,f18511]) ).
fof(f451183,plain,
( spl971_19071
| ~ spl971_21243
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651 ),
inference(avatar_split_clause,[],[f451175,f39552,f18509,f18493,f18469,f450904,f390127]) ).
fof(f452654,plain,
( v14_lattices(k1_lattice2(sK970))
| ~ v13_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| spl971_21243 ),
inference(resolution,[],[f450906,f17254]) ).
fof(f452655,plain,
( ~ v17_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| spl971_21243 ),
inference(resolution,[],[f450906,f17270]) ).
fof(f452656,plain,
( ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_3
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452655,f18480]) ).
fof(f452657,plain,
( ~ v13_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| spl971_1647
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452654,f39529]) ).
fof(f452658,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_3
| ~ spl971_5
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452656,f18490]) ).
fof(f452659,plain,
( ~ v3_struct_0(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_1643
| spl971_1647
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452657,f39505]) ).
fof(f452660,plain,
( $false
| ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452658,f18475]) ).
fof(f452661,plain,
( ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_21243 ),
inference(avatar_contradiction_clause,[],[f452660]) ).
fof(f452662,plain,
( ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_5
| ~ spl971_1643
| spl971_1647
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452659,f18490]) ).
fof(f452663,plain,
( $false
| ~ spl971_2
| ~ spl971_5
| ~ spl971_1643
| spl971_1647
| spl971_21243 ),
inference(forward_subsumption_resolution,[],[f452662,f18475]) ).
fof(f452664,plain,
( ~ spl971_2
| ~ spl971_5
| ~ spl971_1643
| spl971_1647
| spl971_21243 ),
inference(avatar_contradiction_clause,[],[f452663]) ).
fof(f452731,plain,
( spl971_18641
| ~ spl971_21243
| ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651 ),
inference(avatar_split_clause,[],[f451174,f39552,f18509,f18493,f18469,f450904,f356418]) ).
fof(f452751,plain,
( ~ l3_lattices(sK970)
| ~ v15_lattices(sK970)
| ~ v11_lattices(sK970)
| ~ v3_struct_0(sK970)
| v17_lattices(sK970)
| ~ spl971_18641 ),
inference(resolution,[],[f356420,f17272]) ).
fof(f452764,plain,
( ~ v15_lattices(sK970)
| ~ v11_lattices(sK970)
| ~ v3_struct_0(sK970)
| v17_lattices(sK970)
| ~ spl971_8
| ~ spl971_18641 ),
inference(forward_subsumption_resolution,[],[f452751,f18511]) ).
fof(f452771,plain,
( ~ v15_lattices(sK970)
| ~ v3_struct_0(sK970)
| v17_lattices(sK970)
| ~ spl971_8
| ~ spl971_5529
| ~ spl971_18641 ),
inference(forward_subsumption_resolution,[],[f452764,f123880]) ).
fof(f452777,plain,
( ~ v15_lattices(sK970)
| v17_lattices(sK970)
| ~ spl971_1
| ~ spl971_8
| ~ spl971_5529
| ~ spl971_18641 ),
inference(forward_subsumption_resolution,[],[f452771,f18471]) ).
fof(f453401,plain,
( spl971_7
| ~ spl971_19071
| ~ spl971_1
| ~ spl971_8
| ~ spl971_5529
| ~ spl971_18641 ),
inference(avatar_split_clause,[],[f452777,f356418,f123879,f18509,f18469,f390127,f18501]) ).
fof(f453403,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| ~ v11_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| v17_lattices(k1_lattice2(sK970))
| ~ spl971_2
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451145,f18475]) ).
fof(f453798,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| ~ v3_struct_0(k1_lattice2(sK970))
| v17_lattices(k1_lattice2(sK970))
| ~ spl971_2
| ~ spl971_1634
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f453403,f39410]) ).
fof(f454000,plain,
( ~ v15_lattices(k1_lattice2(sK970))
| v17_lattices(k1_lattice2(sK970))
| ~ spl971_2
| ~ spl971_5
| ~ spl971_1634
| ~ spl971_1651 ),
inference(forward_subsumption_resolution,[],[f453798,f18490]) ).
fof(f454052,plain,
( spl971_3
| ~ spl971_21243
| ~ spl971_2
| ~ spl971_5
| ~ spl971_1634
| ~ spl971_1651 ),
inference(avatar_split_clause,[],[f454000,f39552,f39408,f18488,f18473,f450904,f18478]) ).
fof(f454078,plain,
( ~ v16_lattices(sK970)
| ~ v15_lattices(sK970)
| v10_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ spl971_8
| spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451052,f18511]) ).
fof(f454079,plain,
( ~ v17_lattices(k1_lattice2(sK970))
| ~ l3_lattices(k1_lattice2(sK970))
| ~ spl971_5
| spl971_1651 ),
inference(forward_subsumption_resolution,[],[f451053,f18490]) ).
fof(f454245,plain,
( ~ v17_lattices(k1_lattice2(sK970))
| ~ spl971_2
| ~ spl971_5
| spl971_1651 ),
inference(forward_subsumption_resolution,[],[f454079,f18475]) ).
fof(f454248,plain,
( ~ spl971_3
| ~ spl971_2
| ~ spl971_5
| spl971_1651 ),
inference(avatar_split_clause,[],[f454245,f39552,f18488,f18473,f18478]) ).
fof(f454631,plain,
( ~ v17_lattices(sK970)
| ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| spl971_19071 ),
inference(resolution,[],[f390129,f17270]) ).
fof(f454632,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_7
| spl971_19071 ),
inference(forward_subsumption_resolution,[],[f454631,f18503]) ).
fof(f454634,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| ~ spl971_7
| spl971_19071 ),
inference(forward_subsumption_resolution,[],[f454632,f18471]) ).
fof(f454636,plain,
( $false
| ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_19071 ),
inference(forward_subsumption_resolution,[],[f454634,f18511]) ).
fof(f454637,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_19071 ),
inference(avatar_contradiction_clause,[],[f454636]) ).
fof(f454641,plain,
( ~ v3_struct_0(sK970)
| ~ l3_lattices(sK970)
| ~ spl971_7
| spl971_18641 ),
inference(forward_subsumption_resolution,[],[f391747,f18503]) ).
fof(f454658,plain,
( ~ v16_lattices(sK970)
| ~ v15_lattices(sK970)
| ~ v3_struct_0(sK970)
| spl971_6
| ~ spl971_8
| spl971_1651 ),
inference(forward_subsumption_resolution,[],[f454078,f18495]) ).
fof(f454659,plain,
( ~ l3_lattices(sK970)
| ~ spl971_1
| ~ spl971_7
| spl971_18641 ),
inference(forward_subsumption_resolution,[],[f454641,f18471]) ).
fof(f454660,plain,
( ~ v16_lattices(sK970)
| ~ v15_lattices(sK970)
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1651 ),
inference(forward_subsumption_resolution,[],[f454658,f18471]) ).
fof(f454661,plain,
( $false
| ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_18641 ),
inference(forward_subsumption_resolution,[],[f454659,f18511]) ).
fof(f454662,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_18641 ),
inference(avatar_contradiction_clause,[],[f454661]) ).
fof(f454663,plain,
( ~ spl971_19071
| ~ spl971_18641
| ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1651 ),
inference(avatar_split_clause,[],[f454660,f39552,f18509,f18493,f18469,f356418,f390127]) ).
cnf(s10,plain,
( spl971_3
| spl971_7 ),
inference(sat_conversion,[],[f18505]) ).
cnf(s17,plain,
( ~ spl971_1
| ~ spl971_2
| ~ spl971_3
| spl971_4
| ~ spl971_5
| spl971_6
| ~ spl971_7
| ~ spl971_8 ),
inference(sat_conversion,[],[f18516]) ).
cnf(s18,plain,
spl971_8,
inference(sat_conversion,[],[f18517]) ).
cnf(s19,plain,
~ spl971_6,
inference(sat_conversion,[],[f18518]) ).
cnf(s20,plain,
spl971_1,
inference(sat_conversion,[],[f18519]) ).
cnf(s644,plain,
( spl971_2
| ~ spl971_8 ),
inference(sat_conversion,[],[f20842]) ).
cnf(s1318,plain,
( ~ spl971_1
| spl971_5
| ~ spl971_8 ),
inference(sat_conversion,[],[f33106]) ).
cnf(s1330,plain,
( ~ spl971_1
| ~ spl971_4
| spl971_6
| ~ spl971_8 ),
inference(sat_conversion,[],[f33260]) ).
cnf(s2068,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| spl971_1643 ),
inference(sat_conversion,[],[f49454]) ).
cnf(s2446,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_7
| ~ spl971_8
| ~ spl971_1647 ),
inference(sat_conversion,[],[f67302]) ).
cnf(s2453,plain,
( ~ spl971_1
| ~ spl971_2
| spl971_4
| ~ spl971_5
| ~ spl971_8
| spl971_1634
| ~ spl971_2595 ),
inference(sat_conversion,[],[f67478]) ).
cnf(s5425,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_5529 ),
inference(sat_conversion,[],[f123916]) ).
cnf(s5467,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_2595
| ~ spl971_5529 ),
inference(sat_conversion,[],[f124388]) ).
cnf(s20378,plain,
( ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_1634 ),
inference(sat_conversion,[],[f391789]) ).
cnf(s20535,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1634
| spl971_5529 ),
inference(sat_conversion,[],[f392852]) ).
cnf(s23059,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651
| spl971_19071
| ~ spl971_21243 ),
inference(sat_conversion,[],[f451183]) ).
cnf(s23083,plain,
( ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_21243 ),
inference(sat_conversion,[],[f452661]) ).
cnf(s23084,plain,
( ~ spl971_2
| ~ spl971_5
| ~ spl971_1643
| spl971_1647
| spl971_21243 ),
inference(sat_conversion,[],[f452664]) ).
cnf(s23098,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_8
| ~ spl971_1651
| spl971_18641
| ~ spl971_21243 ),
inference(sat_conversion,[],[f452731]) ).
cnf(s23137,plain,
( ~ spl971_1
| spl971_7
| ~ spl971_8
| ~ spl971_5529
| ~ spl971_18641
| ~ spl971_19071 ),
inference(sat_conversion,[],[f453401]) ).
cnf(s23318,plain,
( ~ spl971_2
| spl971_3
| ~ spl971_5
| ~ spl971_1634
| ~ spl971_1651
| ~ spl971_21243 ),
inference(sat_conversion,[],[f454052]) ).
cnf(s23364,plain,
( ~ spl971_2
| ~ spl971_3
| ~ spl971_5
| spl971_1651 ),
inference(sat_conversion,[],[f454248]) ).
cnf(s23368,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_19071 ),
inference(sat_conversion,[],[f454637]) ).
cnf(s23386,plain,
( ~ spl971_1
| ~ spl971_7
| ~ spl971_8
| spl971_18641 ),
inference(sat_conversion,[],[f454662]) ).
cnf(s23387,plain,
( ~ spl971_1
| spl971_6
| ~ spl971_8
| spl971_1651
| ~ spl971_18641
| ~ spl971_19071 ),
inference(sat_conversion,[],[f454663]) ).
cnf(s23971,plain,
spl971_2,
inference(rat,[],[s644,s18]) ).
cnf(s23993,plain,
spl971_5,
inference(rat,[],[s1318,s20,s18]) ).
cnf(s23994,plain,
~ spl971_4,
inference(rat,[],[s1330,s19,s20,s18]) ).
cnf(s24250,plain,
( ~ spl971_3
| ~ spl971_7 ),
inference(rat,[],[s17,s18,s19,s23993,s23994,s23971,s20]) ).
cnf(s24251,plain,
spl971_3,
inference(rat,[],[s2453,s23318,s23084,s5467,s23387,s2068,s2446,s5425,s23368,s23386,s10,s20,s23993,s18,s23971,s23994,s19]) ).
cnf(s24252,plain,
spl971_1651,
inference(rat,[],[s23364,s23971,s23993,s24251]) ).
cnf(s24253,plain,
spl971_21243,
inference(rat,[],[s23083,s23971,s23993,s24251]) ).
cnf(s24254,plain,
spl971_1634,
inference(rat,[],[s20378,s23971,s23993,s24251]) ).
cnf(s24263,plain,
~ spl971_7,
inference(rat,[],[s24250,s24251]) ).
cnf(s24266,plain,
spl971_18641,
inference(rat,[],[s23098,s24252,s18,s19,s20,s24253]) ).
cnf(s24267,plain,
spl971_19071,
inference(rat,[],[s23059,s24252,s18,s19,s20,s24253]) ).
cnf(s24270,plain,
spl971_5529,
inference(rat,[],[s20535,s18,s19,s20,s24254]) ).
cnf(s24342,plain,
$false,
inference(rat,[],[s23137,s24267,s24266,s18,s20,s24263,s24270]) ).
fof(f454664,plain,
$false,
inference(avatar_sat_refutation,[],[s24342]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT319+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:35:20 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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
% 27.59/4.43 % (3444335)Will run a generic schedule for satisfiability detection.
% 27.59/4.43 % (3444340)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2896216304_2998 on theBenchmark for (2998ds/0Mi)
% 27.59/4.43 % (3444341)% WARNING: option uhcvi not known.
% 27.59/4.43 % (3444341)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1430779677:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 27.59/4.43 % (3444342)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1007047929:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 27.59/4.43 % (3444343)dis+10_1_sil=32000:sp=arity:random_seed=1515599668:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 27.59/4.43 % (3444345)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3336880016:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 27.59/4.43 % (3444344)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2381634346:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 27.59/4.43 % (3444346)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2266218302:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 27.59/4.43 % (3444343)Instruction limit reached!
% 27.59/4.43 % (3444343)------------------------------
% 27.59/4.43 % (3444343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.59/4.43 % (3444343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.59/4.43 % (3444343)CaDiCaL version: 2.1.3
% 27.59/4.43 % (3444343)Termination reason: Instruction limit
% 27.59/4.43 % (3444343)Termination phase: Clausification
% 27.59/4.43 % (3444343)Time elapsed: 0.066 s
% 27.59/4.43 % (3444343)Peak memory usage: 19 MB
% 27.59/4.43 % (3444343)Instructions burned: 103 (million)
% 27.59/4.43 % (3444344)Instruction limit reached!
% 27.59/4.43 % (3444344)------------------------------
% 27.59/4.43 % (3444344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.59/4.43 % (3444344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.59/4.43 % (3444344)CaDiCaL version: 2.1.3
% 27.59/4.43 % (3444344)Termination reason: Instruction limit
% 27.59/4.43 % (3444344)Termination phase: NewCNF
% 27.59/4.43 % (3444344)Time elapsed: 0.072 s
% 27.59/4.43 % (3444344)Peak memory usage: 20 MB
% 27.59/4.43 % (3444344)Instructions burned: 117 (million)
% 27.59/4.43 % (3444345)Instruction limit reached!
% 27.59/4.43 % (3444345)------------------------------
% 27.59/4.43 % (3444345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.59/4.43 % (3444345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.59/4.43 % (3444345)CaDiCaL version: 2.1.3
% 27.59/4.43 % (3444345)Termination reason: Instruction limit
% 27.59/4.43 % (3444345)Termination phase: Property scanning
% 27.59/4.43 % (3444345)Time elapsed: 0.079 s
% 27.59/4.43 % (3444345)Peak memory usage: 20 MB
% 27.59/4.43 % (3444345)Instructions burned: 133 (million)
% 27.59/4.43 % (3444354)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1654926778:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.59/4.43 % (3444346)Instruction limit reached!
% 27.59/4.43 % (3444346)------------------------------
% 27.59/4.43 % (3444346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.59/4.43 % (3444346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.59/4.43 % (3444346)CaDiCaL version: 2.1.3
% 27.59/4.43 % (3444346)Termination reason: Instruction limit
% 27.59/4.43 % (3444346)Termination phase: Property scanning
% 27.59/4.43 % (3444346)Time elapsed: 0.091 s
% 27.59/4.43 % (3444346)Peak memory usage: 20 MB
% 27.59/4.43 % (3444346)Instructions burned: 161 (million)
% 27.59/4.43 % (3444355)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=956022413:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 27.59/4.43 % (3444356)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=3149633461:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 27.59/4.43 % (3444359)ott-21_1_sil=16000:fs=off:random_seed=1208808020:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 27.59/4.43 % (3444355)Instruction limit reached!
% 27.59/4.43 % (3444355)------------------------------
% 27.59/4.43 % (3444355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.59/4.43 % (3444355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444355)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444355)Termination reason: Instruction limit
% 57.24/8.63 % (3444355)Termination phase: Property scanning
% 57.24/8.63 % (3444355)Time elapsed: 0.078 s
% 57.24/8.63 % (3444355)Peak memory usage: 20 MB
% 57.24/8.63 % (3444355)Instructions burned: 132 (million)
% 57.24/8.63 % (3444362)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4263745308:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 57.24/8.63 % (3444359)Instruction limit reached!
% 57.24/8.63 % (3444359)------------------------------
% 57.24/8.63 % (3444359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444359)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444359)Termination reason: Instruction limit
% 57.24/8.63 % (3444359)Termination phase: Function definition elimination
% 57.24/8.63 % (3444359)Time elapsed: 0.097 s
% 57.24/8.63 % (3444359)Peak memory usage: 20 MB
% 57.24/8.63 % (3444359)Instructions burned: 181 (million)
% 57.24/8.63 % (3444364)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=341985581:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 57.24/8.63 % (3444354)Instruction limit reached!
% 57.24/8.63 % (3444354)------------------------------
% 57.24/8.63 % (3444354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444354)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444354)Termination reason: Instruction limit
% 57.24/8.63 % (3444354)Termination phase: Finite model building preprocessing
% 57.24/8.63 % (3444354)Time elapsed: 0.311 s
% 57.24/8.63 % (3444354)Peak memory usage: 28 MB
% 57.24/8.63 % (3444354)Instructions burned: 716 (million)
% 57.24/8.63 % (3444366)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2295067462:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 57.24/8.63 % (3444362)Instruction limit reached!
% 57.24/8.63 % (3444362)------------------------------
% 57.24/8.63 % (3444362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444362)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444362)Termination reason: Instruction limit
% 57.24/8.63 % (3444362)Termination phase: Saturation
% 57.24/8.63 % (3444362)Time elapsed: 0.238 s
% 57.24/8.63 % (3444362)Peak memory usage: 24 MB
% 57.24/8.63 % (3444362)Instructions burned: 477 (million)
% 57.24/8.63 % (3444356)Instruction limit reached!
% 57.24/8.63 % (3444356)------------------------------
% 57.24/8.63 % (3444356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444356)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444356)Termination reason: Instruction limit
% 57.24/8.63 % (3444356)Termination phase: Saturation
% 57.24/8.63 % (3444356)Time elapsed: 0.342 s
% 57.24/8.63 % (3444356)Peak memory usage: 28 MB
% 57.24/8.63 % (3444356)Instructions burned: 684 (million)
% 57.24/8.63 % (3444368)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=199112682:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 57.24/8.63 % (3444369)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=1438612482:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 57.24/8.63 % (3444364)Instruction limit reached!
% 57.24/8.63 % (3444364)------------------------------
% 57.24/8.63 % (3444364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.24/8.63 % (3444364)CaDiCaL version: 2.1.3
% 57.24/8.63 % (3444364)Termination reason: Instruction limit
% 57.24/8.63 % (3444364)Termination phase: Finite model building preprocessing
% 57.24/8.63 % (3444364)Time elapsed: 0.375 s
% 57.24/8.63 % (3444364)Peak memory usage: 30 MB
% 57.24/8.63 % (3444364)Instructions burned: 866 (million)
% 57.24/8.63 % (3444372)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2258733191:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 57.24/8.63 % (3444369)Instruction limit reached!
% 57.24/8.63 % (3444369)------------------------------
% 57.24/8.63 % (3444369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.24/8.63 % (3444369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444369)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444369)Termination reason: Instruction limit
% 126.21/18.31 % (3444369)Termination phase: Saturation
% 126.21/18.31 % (3444369)Time elapsed: 0.353 s
% 126.21/18.31 % (3444369)Peak memory usage: 30 MB
% 126.21/18.31 % (3444369)Instructions burned: 694 (million)
% 126.21/18.31 % (3444368)Instruction limit reached!
% 126.21/18.31 % (3444368)------------------------------
% 126.21/18.31 % (3444368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444368)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444368)Termination reason: Instruction limit
% 126.21/18.31 % (3444368)Termination phase: Finite model building preprocessing
% 126.21/18.31 % (3444368)Time elapsed: 0.382 s
% 126.21/18.31 % (3444368)Peak memory usage: 30 MB
% 126.21/18.31 % (3444368)Instructions burned: 890 (million)
% 126.21/18.31 % (3444374)fmb+10_1_sil=64000:random_seed=523664794:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 126.21/18.31 % (3444376)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3857137000:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 126.21/18.31 % (3444372)Instruction limit reached!
% 126.21/18.31 % (3444372)------------------------------
% 126.21/18.31 % (3444372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444372)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444372)Termination reason: Instruction limit
% 126.21/18.31 % (3444372)Termination phase: Saturation
% 126.21/18.31 % (3444372)Time elapsed: 0.382 s
% 126.21/18.31 % (3444372)Peak memory usage: 30 MB
% 126.21/18.31 % (3444372)Instructions burned: 882 (million)
% 126.21/18.31 % (3444366)Instruction limit reached!
% 126.21/18.31 % (3444366)------------------------------
% 126.21/18.31 % (3444366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444366)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444366)Termination reason: Instruction limit
% 126.21/18.31 % (3444366)Termination phase: Saturation
% 126.21/18.31 % (3444366)Time elapsed: 0.594 s
% 126.21/18.31 % (3444366)Peak memory usage: 33 MB
% 126.21/18.31 % (3444366)Instructions burned: 1181 (million)
% 126.21/18.31 % (3444378)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=621073099:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 126.21/18.31 % (3444379)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3409521928:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 126.21/18.31 % (3444378)Instruction limit reached!
% 126.21/18.31 % (3444378)------------------------------
% 126.21/18.31 % (3444378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444378)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444378)Termination reason: Instruction limit
% 126.21/18.31 % (3444378)Termination phase: Finite model building preprocessing
% 126.21/18.31 % (3444378)Time elapsed: 0.396 s
% 126.21/18.31 % (3444378)Peak memory usage: 30 MB
% 126.21/18.31 % (3444378)Instructions burned: 922 (million)
% 126.21/18.31 % (3444382)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1838961788:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 126.21/18.31 % (3444382)Instruction limit reached!
% 126.21/18.31 % (3444382)------------------------------
% 126.21/18.31 % (3444382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444382)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444382)Termination reason: Instruction limit
% 126.21/18.31 % (3444382)Termination phase: Saturation
% 126.21/18.31 % (3444382)Time elapsed: 0.615 s
% 126.21/18.31 % (3444382)Peak memory usage: 26 MB
% 126.21/18.31 % (3444382)Instructions burned: 1473 (million)
% 126.21/18.31 % (3444384)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1617964609:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 126.21/18.31 % (3444379)Instruction limit reached!
% 126.21/18.31 % (3444379)------------------------------
% 126.21/18.31 % (3444379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.21/18.31 % (3444379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.21/18.31 % (3444379)CaDiCaL version: 2.1.3
% 126.21/18.31 % (3444379)Termination reason: Instruction limit
% 134.65/24.55 % (3444379)Termination phase: Saturation
% 134.65/24.55 % (3444379)Time elapsed: 2.840 s
% 134.65/24.55 % (3444379)Peak memory usage: 61 MB
% 134.65/24.55 % (3444379)Instructions burned: 5133 (million)
% 134.65/24.55 % (3444386)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2631105912:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 134.65/24.55 % (3444386)Instruction limit reached!
% 134.65/24.55 % (3444386)------------------------------
% 134.65/24.55 % (3444386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444386)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444386)Termination reason: Instruction limit
% 134.65/24.55 % (3444386)Termination phase: Finite model building preprocessing
% 134.65/24.55 % (3444386)Time elapsed: 0.662 s
% 134.65/24.55 % (3444386)Peak memory usage: 37 MB
% 134.65/24.55 % (3444386)Instructions burned: 2179 (million)
% 134.65/24.55 % (3444388)ott-2_1_sil=16000:newcnf=on:random_seed=701387115:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 134.65/24.55 % (3444388)Instruction limit reached!
% 134.65/24.55 % (3444388)------------------------------
% 134.65/24.55 % (3444388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444388)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444388)Termination reason: Instruction limit
% 134.65/24.55 % (3444388)Termination phase: Saturation
% 134.65/24.55 % (3444388)Time elapsed: 0.421 s
% 134.65/24.55 % (3444388)Peak memory usage: 29 MB
% 134.65/24.55 % (3444388)Instructions burned: 871 (million)
% 134.65/24.55 % (3444390)ott+10_1_sil=32000:tgt=ground:random_seed=710580279:i=5114:av=off_2948 on theBenchmark for (2948ds/5114Mi)
% 134.65/24.55 % (3444384)Instruction limit reached!
% 134.65/24.55 % (3444384)------------------------------
% 134.65/24.55 % (3444384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444384)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444384)Termination reason: Instruction limit
% 134.65/24.55 % (3444384)Termination phase: Finite model building preprocessing
% 134.65/24.55 % (3444384)Time elapsed: 3.326 s
% 134.65/24.55 % (3444384)Peak memory usage: 46 MB
% 134.65/24.55 % (3444384)Instructions burned: 6326 (million)
% 134.65/24.55 % (3444392)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3216889808:i=54282_2944 on theBenchmark for (2944ds/54282Mi)
% 134.65/24.55 % (3444376)Instruction limit reached!
% 134.65/24.55 % (3444376)------------------------------
% 134.65/24.55 % (3444376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444376)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444376)Termination reason: Instruction limit
% 134.65/24.55 % (3444376)Termination phase: Finite model building preprocessing
% 134.65/24.55 % (3444376)Time elapsed: 5.074 s
% 134.65/24.55 % (3444376)Peak memory usage: 51 MB
% 134.65/24.55 % (3444376)Instructions burned: 9515 (million)
% 134.65/24.55 % (3444394)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=89224704:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi)
% 134.65/24.55 % (3444394)Instruction limit reached!
% 134.65/24.55 % (3444394)------------------------------
% 134.65/24.55 % (3444394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444394)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444394)Termination reason: Instruction limit
% 134.65/24.55 % (3444394)Termination phase: Saturation
% 134.65/24.55 % (3444394)Time elapsed: 1.920 s
% 134.65/24.55 % (3444394)Peak memory usage: 50 MB
% 134.65/24.55 % (3444394)Instructions burned: 3512 (million)
% 134.65/24.55 % (3444396)dis+21_1_sil=32000:sas=cadical:random_seed=1883237064:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi)
% 134.65/24.55 % (3444390)Instruction limit reached!
% 134.65/24.55 % (3444390)------------------------------
% 134.65/24.55 % (3444390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444390)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444390)Termination reason: Instruction limit
% 134.65/24.55 % (3444390)Termination phase: Saturation
% 134.65/24.55 % (3444390)Time elapsed: 3.043 s
% 134.65/24.55 % (3444390)Peak memory usage: 80 MB
% 134.65/24.55 % (3444390)Instructions burned: 5114 (million)
% 134.65/24.55 % (3444398)ott+11_1_sil=16000:gs=on:random_seed=2311429808:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2917 on theBenchmark for (2917ds/2251Mi)
% 134.65/24.55 % (3444398)Instruction limit reached!
% 134.65/24.55 % (3444398)------------------------------
% 134.65/24.55 % (3444398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444398)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444398)Termination reason: Instruction limit
% 134.65/24.55 % (3444398)Termination phase: Saturation
% 134.65/24.55 % (3444398)Time elapsed: 0.866 s
% 134.65/24.55 % (3444398)Peak memory usage: 28 MB
% 134.65/24.55 % (3444398)Instructions burned: 2252 (million)
% 134.65/24.55 % (3444400)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=924566635:fmbsr=1.6:i=67534_2908 on theBenchmark for (2908ds/67534Mi)
% 134.65/24.55 % (3444396)Instruction limit reached!
% 134.65/24.55 % (3444396)------------------------------
% 134.65/24.55 % (3444396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444396)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444396)Termination reason: Instruction limit
% 134.65/24.55 % (3444396)Termination phase: Saturation
% 134.65/24.55 % (3444396)Time elapsed: 2.017 s
% 134.65/24.55 % (3444396)Peak memory usage: 57 MB
% 134.65/24.55 % (3444396)Instructions burned: 3774 (million)
% 134.65/24.55 % (3444402)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2385649691:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2899 on theBenchmark for (2899ds/4591Mi)
% 134.65/24.55 % (3444374)Instruction limit reached!
% 134.65/24.55 % (3444374)------------------------------
% 134.65/24.55 % (3444374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444374)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444374)Termination reason: Instruction limit
% 134.65/24.55 % (3444374)Termination phase: Finite model building preprocessing
% 134.65/24.55 % (3444374)Time elapsed: 11.989 s
% 134.65/24.55 % (3444374)Peak memory usage: 67 MB
% 134.65/24.55 % (3444374)Instructions burned: 22062 (million)
% 134.65/24.55 % (3444402)Instruction limit reached!
% 134.65/24.55 % (3444402)------------------------------
% 134.65/24.55 % (3444402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444402)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444402)Termination reason: Instruction limit
% 134.65/24.55 % (3444402)Termination phase: Saturation
% 134.65/24.55 % (3444402)Time elapsed: 2.890 s
% 134.65/24.55 % (3444402)Peak memory usage: 120 MB
% 134.65/24.55 % (3444402)Instructions burned: 4592 (million)
% 134.65/24.55 % (3444404)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=187157432:i=29340_2870 on theBenchmark for (2870ds/29340Mi)
% 134.65/24.55 % (3444405)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2938048237:i=5211_2870 on theBenchmark for (2870ds/5211Mi)
% 134.65/24.55 % (3444405)Instruction limit reached!
% 134.65/24.55 % (3444405)------------------------------
% 134.65/24.55 % (3444405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444405)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444405)Termination reason: Instruction limit
% 134.65/24.55 % (3444405)Termination phase: Saturation
% 134.65/24.55 % (3444405)Time elapsed: 1.947 s
% 134.65/24.55 % (3444405)Peak memory usage: 50 MB
% 134.65/24.55 % (3444405)Instructions burned: 5211 (million)
% 134.65/24.55 % (3444408)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2516760801:i=5497:nm=2_2850 on theBenchmark for (2850ds/5497Mi)
% 134.65/24.55 % (3444408)Instruction limit reached!
% 134.65/24.55 % (3444408)------------------------------
% 134.65/24.55 % (3444408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.55 % (3444408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.55 % (3444408)CaDiCaL version: 2.1.3
% 134.65/24.55 % (3444408)Termination reason: Instruction limit
% 134.65/24.55 % (3444408)Termination phase: Finite model building preprocessing
% 134.65/24.55 % (3444408)Time elapsed: 2.912 s
% 134.65/24.55 % (3444408)Peak memory usage: 44 MB
% 134.65/24.55 % (3444408)Instructions burned: 5498 (million)
% 134.65/24.55 % (3444410)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3600523085:fmbsr=2:i=46332_2821 on theBenchmark for (2821ds/46332Mi)
% 134.65/24.55 % (3444341) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3444335-3444341"...
% 134.65/24.55 % (3444341)...printing done.
% 134.65/24.55 % (3444341)Refutation found. Thanks to Tanya!
% 134.65/24.55 % SZS status Theorem for theBenchmark
% 134.65/24.55 % SZS output start Proof for theBenchmark
% See solution above
% 134.65/24.56 % (3444341)------------------------------
% 134.65/24.56 % (3444341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.65/24.56 % (3444341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.65/24.56 % (3444341)CaDiCaL version: 2.1.3
% 134.65/24.56 % (3444341)Termination reason: Refutation
% 134.65/24.56 % (3444341)Time elapsed: 23.858 s
% 134.65/24.56 % (3444341)Peak memory usage: 260 MB
% 134.65/24.56 % (3444341)Instructions burned: 46168 (million)
% 134.65/24.56 % (3444335)Success in time 24.128 s
% 134.65/24.56 % Vampire exiting
%------------------------------------------------------------------------------