%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWV095+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 04:46:05 PM UTC 2025
% Result : Theorem 27.44s 3.83s
% Output : CNFRefutation 27.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 331 ( 311 unt; 0 def)
% Number of atoms : 929 ( 772 equ)
% Maximal formula atoms : 74 ( 2 avg)
% Number of connectives : 1053 ( 455 ~; 452 |; 140 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 20 con; 0-3 aty)
% Number of variables : 12 ( 0 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(quaternion_ds1_inuse_0007,plain,
( ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [A,B] :
( ( leq(n0,A)
& leq(n0,B)
& leq(A,n2)
& leq(B,minus(pv5,n1)) )
=> ( a_select3(u_defuse,A,B) = use
& a_select3(z_defuse,A,B) = use ) ) )
=> ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [C,D] :
( ( leq(n0,C)
& leq(n0,D)
& leq(C,n2)
& leq(D,minus(pv5,n1)) )
=> ( a_select3(u_defuse,C,D) = use
& a_select3(z_defuse,C,D) = use ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_inuse_0007) ).
fof(quaternion_ds1_inuse_0007_negated,plain,
~ ( ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [A,B] :
( ( leq(n0,A)
& leq(n0,B)
& leq(A,n2)
& leq(B,minus(pv5,n1)) )
=> ( a_select3(u_defuse,A,B) = use
& a_select3(z_defuse,A,B) = use ) ) )
=> ( a_select2(rho_defuse,n0) = use
& a_select2(rho_defuse,n1) = use
& a_select2(rho_defuse,n2) = use
& a_select2(sigma_defuse,n0) = use
& a_select2(sigma_defuse,n1) = use
& a_select2(sigma_defuse,n2) = use
& a_select2(sigma_defuse,n3) = use
& a_select2(sigma_defuse,n4) = use
& a_select2(sigma_defuse,n5) = use
& a_select3(u_defuse,n0,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n2,n0) = use
& a_select2(xinit_defuse,n3) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_mean_defuse,n0) = use
& a_select2(xinit_mean_defuse,n1) = use
& a_select2(xinit_mean_defuse,n2) = use
& a_select2(xinit_mean_defuse,n3) = use
& a_select2(xinit_mean_defuse,n4) = use
& a_select2(xinit_mean_defuse,n5) = use
& a_select2(xinit_noise_defuse,n0) = use
& a_select2(xinit_noise_defuse,n1) = use
& a_select2(xinit_noise_defuse,n2) = use
& a_select2(xinit_noise_defuse,n3) = use
& a_select2(xinit_noise_defuse,n4) = use
& a_select2(xinit_noise_defuse,n5) = use
& leq(n0,pv5)
& leq(n0,pv51)
& leq(pv5,minus(n999,n1))
& leq(pv51,minus(n6,n1))
& ! [C,D] :
( ( leq(n0,C)
& leq(n0,D)
& leq(C,n2)
& leq(D,minus(pv5,n1)) )
=> ( a_select3(u_defuse,C,D) = use
& a_select3(z_defuse,C,D) = use ) ) ) ),
inference(negate_conjecture,[status(cth)],[quaternion_ds1_inuse_0007]) ).
cnf(152,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,sK28,sK29) != use
| a_select3(z_defuse,sK28,sK29) != use ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l0,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,sK28,sK29) != use
| a_select3(z_defuse,sK28,sK29) != use ),
inference(instantiation,[status(thm)],[152]) ).
cnf(117,plain,
a_select2(rho_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l869,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(147,plain,
( ~ leq(X0,n2)
| ~ leq(X1,minus(pv5,n1))
| ~ leq(n0,X0)
| ~ leq(n0,X1)
| a_select3(z_defuse,X0,X1) = use ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1177,plain,
( ~ leq(sK28,n2)
| ~ leq(sK29,minus(pv5,n1))
| ~ leq(n0,sK28)
| ~ leq(n0,sK29)
| a_select3(z_defuse,sK28,sK29) = use ),
inference(instantiation,[status(thm)],[147]) ).
cnf(123,plain,
a_select2(sigma_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l856,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(125,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l861,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(130,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l906,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(131,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l925,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(132,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l904,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(136,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l890,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(144,plain,
leq(pv5,minus(n999,n1)),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l213,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(120,plain,
a_select2(sigma_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l899,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(133,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l865,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(128,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l860,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(119,plain,
a_select2(sigma_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l880,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(134,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l858,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(122,plain,
a_select2(sigma_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l852,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(116,plain,
a_select2(rho_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l886,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(146,plain,
( ~ leq(X0,n2)
| ~ leq(X1,minus(pv5,n1))
| ~ leq(n0,X0)
| ~ leq(n0,X1)
| a_select3(u_defuse,X0,X1) = use ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l891,plain,
( ~ leq(sK28,n2)
| ~ leq(sK29,minus(pv5,n1))
| ~ leq(n0,sK28)
| ~ leq(n0,sK29)
| a_select3(u_defuse,sK28,sK29) = use ),
inference(instantiation,[status(thm)],[146]) ).
cnf(137,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l853,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(149,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK29) ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l970,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK29) ),
inference(instantiation,[status(thm)],[149]) ).
cnf(143,plain,
leq(n0,pv51),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1071,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(138,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l875,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1110,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(150,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK28,n2) ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l957,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK28,n2) ),
inference(instantiation,[status(thm)],[150]) ).
cnf(145,plain,
leq(pv51,minus(n6,n1)),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l195,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1011,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1020,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(135,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1061,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1103,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(127,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1057,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(151,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK29,minus(pv5,n1)) ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l916,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK29,minus(pv5,n1)) ),
inference(instantiation,[status(thm)],[151]) ).
cnf(l1107,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l859,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1016,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1114,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(139,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1021,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(124,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l862,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1012,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(129,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1010,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1005,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1113,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1000,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(121,plain,
a_select2(sigma_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1111,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(142,plain,
leq(n0,pv5),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1063,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(126,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l855,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1073,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1047,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1031,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(141,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1066,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1007,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1104,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(140,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1059,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1065,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1048,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1072,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1033,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1058,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1013,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1026,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1044,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1050,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1067,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1008,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1025,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1036,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1002,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1018,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1060,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1029,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1112,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1096,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1015,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l892,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(118,plain,
a_select2(sigma_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l1116,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1097,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1051,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l879,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1038,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l999,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1069,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1102,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1041,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1040,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1099,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1009,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1034,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1106,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1045,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1052,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l998,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1024,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l866,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1027,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l191,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1030,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1178,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK29) ),
inference(instantiation,[status(thm)],[149]) ).
cnf(115,plain,
a_select2(rho_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l179,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1046,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1105,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1003,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1189,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1043,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1204,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1004,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l871,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1179,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK28,n2) ),
inference(instantiation,[status(thm)],[150]) ).
cnf(l1062,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(148,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK28) ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0007_negated]) ).
cnf(l959,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK28) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l1244,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l960,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1001,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1227,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1019,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1017,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1079,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1092,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1090,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1074,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1233,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1100,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1076,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l965,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1209,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1006,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1190,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1262,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1023,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1037,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1084,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1194,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1028,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1081,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1195,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1070,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1214,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1039,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1088,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1232,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1087,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1055,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1276,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1054,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1235,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1035,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l966,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1205,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1246,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1056,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1086,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1223,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1221,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1191,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1091,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1064,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1239,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1089,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1265,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l900,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1042,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1206,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1241,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l964,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l881,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1202,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1077,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1228,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1022,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1231,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1224,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1098,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1192,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1240,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1226,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l961,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1094,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1186,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1238,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1242,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1247,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1219,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1075,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l968,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1211,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1083,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1181,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(n0,sK28) ),
inference(instantiation,[status(thm)],[148]) ).
cnf(l1197,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1207,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1287,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1185,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1203,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1180,plain,
( ~ leq(n0,pv5)
| ~ leq(n0,pv51)
| ~ leq(pv5,minus(n999,n1))
| ~ leq(pv51,minus(n6,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_defuse,n1) != use
| a_select2(sigma_defuse,n0) != use
| a_select2(sigma_defuse,n5) != use
| a_select2(sigma_defuse,n2) != use
| a_select2(sigma_defuse,n4) != use
| a_select2(sigma_defuse,n3) != use
| a_select2(sigma_defuse,n1) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select2(xinit_noise_defuse,n0) != use
| a_select2(xinit_noise_defuse,n5) != use
| a_select2(xinit_noise_defuse,n2) != use
| a_select2(xinit_noise_defuse,n4) != use
| a_select2(xinit_noise_defuse,n3) != use
| a_select2(xinit_noise_defuse,n1) != use
| a_select2(xinit_mean_defuse,n0) != use
| a_select2(xinit_mean_defuse,n5) != use
| a_select2(xinit_mean_defuse,n2) != use
| a_select2(xinit_mean_defuse,n4) != use
| a_select2(xinit_mean_defuse,n3) != use
| a_select2(xinit_mean_defuse,n1) != use
| a_select3(u_defuse,n0,n0) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| leq(sK29,minus(pv5,n1)) ),
inference(instantiation,[status(thm)],[151]) ).
cnf(l1108,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1225,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1243,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l864,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1085,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1293,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1068,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1236,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1032,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1268,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1280,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1291,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1212,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1248,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1277,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1093,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1253,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1229,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1082,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1252,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1263,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1183,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1282,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1284,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1270,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1259,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1237,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1078,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1222,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1300,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1213,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1193,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1182,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1297,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1258,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1261,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1289,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1196,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1049,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1220,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1275,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1260,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1266,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1080,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1218,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1095,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1249,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l1251,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1257,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1296,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1299,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1267,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1201,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1230,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1210,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1255,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l963,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1256,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1272,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1290,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1271,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1199,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1234,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1188,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1217,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1298,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(l969,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1303,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1250,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1292,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1304,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1216,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1295,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1294,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1279,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1264,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1245,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1302,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1286,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1273,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1274,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1014,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1200,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1288,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1184,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1301,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1215,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1109,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1198,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1278,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1283,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1187,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1254,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1269,plain,
leq(pv51,minus(n6,n1)),
inference(instantiation,[status(thm)],[145]) ).
cnf(l1208,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1285,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1305,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1281,plain,
leq(n0,pv51),
inference(instantiation,[status(thm)],[143]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l869,l1177,l856,l861,l906,l925,l904,l890,l213,l899,l865,l860,l880,l858,l852,l886,l891,l853,l970,l1071,l875,l1110,l957,l195,l1011,l1020,l1061,l1103,l1057,l916,l1107,l859,l1016,l1114,l1021,l862,l1012,l1010,l1005,l1113,l1000,l1111,l1063,l855,l1073,l1047,l1031,l1066,l1007,l1104,l1059,l1065,l1048,l1072,l1033,l1058,l1013,l1026,l1044,l1050,l1067,l1008,l1025,l1036,l1002,l1018,l1060,l1029,l1112,l1096,l1015,l892,l1116,l1097,l1051,l879,l1038,l999,l1069,l1102,l1041,l1040,l1099,l1009,l1034,l1106,l1045,l1052,l998,l1,l1024,l866,l1027,l191,l1030,l1178,l179,l1046,l1105,l1003,l1189,l1043,l1204,l1004,l871,l1179,l1062,l959,l1244,l960,l1001,l1227,l1019,l1017,l1079,l1092,l1090,l1074,l1233,l1100,l1076,l965,l1209,l1006,l1190,l1262,l1023,l1037,l1084,l1194,l1028,l1081,l1195,l1070,l1214,l1039,l1088,l1232,l1087,l1055,l1276,l1054,l1235,l1035,l966,l1205,l1246,l1056,l1086,l1223,l1221,l1191,l1091,l1064,l1239,l1089,l1265,l900,l1042,l1206,l1241,l964,l881,l1202,l1077,l1228,l1022,l1231,l1224,l1098,l1192,l1240,l1226,l961,l1094,l1186,l1238,l1242,l1247,l1219,l1075,l968,l1211,l1083,l1181,l1197,l1207,l1287,l1185,l1203,l1180,l1108,l1225,l1243,l864,l1085,l1293,l1068,l1236,l1032,l1268,l1280,l1291,l1212,l1248,l1277,l1093,l1253,l1229,l1082,l1252,l1263,l1183,l1282,l1284,l1270,l1259,l1237,l1078,l1222,l1300,l1213,l1193,l1182,l1297,l1258,l1261,l1289,l1196,l1049,l1220,l1275,l1260,l1266,l1080,l1218,l1095,l1249,l1251,l1257,l1296,l1299,l1267,l1201,l1230,l1210,l1255,l963,l1256,l1272,l1290,l1271,l1199,l1234,l1188,l1217,l1298,l969,l1303,l1250,l1292,l1304,l1216,l1295,l1294,l1279,l1264,l1245,l1302,l1286,l1273,l1274,l1014,l1200,l1288,l1184,l1301,l1215,l1109,l1198,l1278,l1283,l1187,l1254,l1269,l1208,l1285,l1305,l1281]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWV095+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.35 % Computer : n027.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Tue Jul 22 08:12:19 EDT 2025
% 0.12/0.35 % CPUTime :
% 0.12/0.36 % launching worker at depth: 2
% 0.12/0.36 % launching worker at depth: 4
% 0.12/0.36 % launching worker at depth: 6
% 0.12/0.36 % launching worker at depth: 8
% 0.12/0.36 % launching worker at depth: 5
% 0.12/0.36 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 7
% 0.12/0.36 % launching worker at depth: 1
% 3.45/0.79 % launching worker at depth: 9
% 27.44/3.83 % SZS status Theorem for theBenchmark
% 27.44/3.83 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------