%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWV096+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 : n017.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 25.13s 3.51s
% Output : CNFRefutation 25.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 311 ( 291 unt; 0 def)
% Number of atoms : 877 ( 772 equ)
% Maximal formula atoms : 72 ( 2 avg)
% Number of connectives : 993 ( 427 ~; 424 |; 136 &)
% ( 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_0008,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(pv5,minus(n999,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_0008) ).
fof(quaternion_ds1_inuse_0008_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(pv5,minus(n999,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_0008]) ).
cnf(152,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_select3(z_defuse,sK28,sK29) != 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 ),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l0,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_select3(z_defuse,sK28,sK29) != 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 ),
inference(instantiation,[status(thm)],[152]) ).
cnf(131,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l763,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(144,plain,
leq(pv5,minus(n999,n1)),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l134,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(139,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l795,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(118,plain,
a_select2(sigma_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l753,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(137,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l762,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(141,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l766,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(127,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l781,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(119,plain,
a_select2(sigma_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l751,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(136,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l757,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(120,plain,
a_select2(sigma_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l749,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(134,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l758,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(138,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l774,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(117,plain,
a_select2(rho_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l138,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(129,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l791,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(116,plain,
a_select2(rho_defuse,n1) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l130,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(130,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l788,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(115,plain,
a_select2(rho_defuse,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l132,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(132,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l775,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
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_0008_negated]) ).
cnf(l754,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(128,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l779,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(150,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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_0008_negated]) ).
cnf(l773,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(122,plain,
a_select2(sigma_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l760,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1141,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(123,plain,
a_select2(sigma_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l786,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1107,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1098,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(149,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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_0008_negated]) ).
cnf(l854,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1109,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(142,plain,
leq(n0,pv5),
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1106,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(124,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l771,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1138,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1093,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1096,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1076,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1159,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(133,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1124,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1117,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1201,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1226,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(126,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1113,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1151,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(140,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l805,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1147,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(151,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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_0008_negated]) ).
cnf(l848,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1146,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1050,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(135,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1110,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1077,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(125,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1043,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1062,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1058,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1154,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1111,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1149,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1094,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1150,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1112,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1153,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1189,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1052,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1086,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1099,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1101,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1089,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1105,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1045,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1081,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1046,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1082,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1087,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(121,plain,
a_select2(sigma_defuse,n3) = use,
inference(cnf,[status(esa)],[quaternion_ds1_inuse_0008_negated]) ).
cnf(l1064,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1063,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1044,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1085,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1103,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1139,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1152,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1084,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1095,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1091,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1066,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1116,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1104,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1232,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1083,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1235,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1115,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1092,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1108,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1200,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l752,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1097,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1079,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1078,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1119,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1155,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1148,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1080,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1135,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1102,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1074,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1057,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1053,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1071,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
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_0008_negated]) ).
cnf(l1026,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(l1047,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1070,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l778,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1140,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1126,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l750,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1048,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l777,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1075,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1042,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1049,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1100,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1205,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1227,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1206,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1054,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1059,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1230,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1223,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(148,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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_0008_negated]) ).
cnf(l792,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1145,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1177,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1051,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1241,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1183,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1167,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1242,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1246,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1191,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1202,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1208,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1088,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1192,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1220,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1214,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1197,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1225,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1186,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1211,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1172,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1221,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1090,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1185,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1142,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1222,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1179,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1196,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1243,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1174,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1199,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1168,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1212,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1162,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1203,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1180,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1068,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1182,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1144,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1160,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1181,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1239,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1204,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1173,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1219,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1061,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1175,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1037,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1122,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1184,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1207,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1170,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1056,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1169,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1161,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1228,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1065,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1178,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1143,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1127,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1249,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1251,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1072,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1210,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1120,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1157,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1262,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1237,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1250,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1136,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1067,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1247,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1130,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1229,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1125,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1121,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(l1158,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1188,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1231,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1164,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1209,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1198,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1118,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1128,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1171,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1166,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1213,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1236,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1165,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1240,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1245,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1176,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1055,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1134,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1233,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1244,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1238,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1218,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1248,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1123,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1187,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1261,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1027,plain,
( ~ leq(n0,pv5)
| ~ leq(pv5,minus(n999,n1))
| a_select2(rho_defuse,n0) != use
| a_select2(rho_defuse,n2) != use
| a_select2(rho_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_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != 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_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_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(l1224,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1029,plain,
a_select2(xinit_noise_defuse,n1) = use,
inference(instantiation,[status(thm)],[137]) ).
cnf(l1038,plain,
a_select2(xinit_mean_defuse,n4) = use,
inference(instantiation,[status(thm)],[134]) ).
cnf(l1032,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l782,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1259,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1253,plain,
a_select2(sigma_defuse,n2) = use,
inference(instantiation,[status(thm)],[120]) ).
cnf(l1258,plain,
a_select3(u_defuse,n1,n0) = use,
inference(instantiation,[status(thm)],[125]) ).
cnf(l1260,plain,
a_select2(xinit_noise_defuse,n5) = use,
inference(instantiation,[status(thm)],[141]) ).
cnf(l1257,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1190,plain,
a_select2(sigma_defuse,n3) = use,
inference(instantiation,[status(thm)],[121]) ).
cnf(l1028,plain,
a_select2(sigma_defuse,n1) = use,
inference(instantiation,[status(thm)],[119]) ).
cnf(l1039,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1060,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1256,plain,
a_select2(xinit_defuse,n3) = use,
inference(instantiation,[status(thm)],[127]) ).
cnf(l1156,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1073,plain,
a_select2(sigma_defuse,n0) = use,
inference(instantiation,[status(thm)],[118]) ).
cnf(l1255,plain,
a_select2(sigma_defuse,n4) = use,
inference(instantiation,[status(thm)],[122]) ).
cnf(l1234,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1030,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1131,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1114,plain,
a_select2(xinit_mean_defuse,n3) = use,
inference(instantiation,[status(thm)],[133]) ).
cnf(l1035,plain,
a_select2(sigma_defuse,n5) = use,
inference(instantiation,[status(thm)],[123]) ).
cnf(l1254,plain,
leq(n0,pv5),
inference(instantiation,[status(thm)],[142]) ).
cnf(l1216,plain,
a_select2(rho_defuse,n2) = use,
inference(instantiation,[status(thm)],[117]) ).
cnf(l1137,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1041,plain,
a_select2(rho_defuse,n1) = use,
inference(instantiation,[status(thm)],[116]) ).
cnf(l1163,plain,
a_select2(xinit_mean_defuse,n2) = use,
inference(instantiation,[status(thm)],[132]) ).
cnf(l1031,plain,
a_select2(xinit_noise_defuse,n2) = use,
inference(instantiation,[status(thm)],[138]) ).
cnf(l1195,plain,
a_select2(xinit_mean_defuse,n0) = use,
inference(instantiation,[status(thm)],[130]) ).
cnf(l1193,plain,
a_select2(xinit_noise_defuse,n4) = use,
inference(instantiation,[status(thm)],[140]) ).
cnf(l1194,plain,
a_select2(xinit_mean_defuse,n1) = use,
inference(instantiation,[status(thm)],[131]) ).
cnf(l1040,plain,
a_select2(xinit_defuse,n4) = use,
inference(instantiation,[status(thm)],[128]) ).
cnf(l1133,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1036,plain,
leq(pv5,minus(n999,n1)),
inference(instantiation,[status(thm)],[144]) ).
cnf(l1034,plain,
a_select3(u_defuse,n2,n0) = use,
inference(instantiation,[status(thm)],[126]) ).
cnf(l1252,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1069,plain,
a_select2(xinit_mean_defuse,n5) = use,
inference(instantiation,[status(thm)],[135]) ).
cnf(l1132,plain,
a_select2(xinit_noise_defuse,n0) = use,
inference(instantiation,[status(thm)],[136]) ).
cnf(l1129,plain,
a_select2(rho_defuse,n0) = use,
inference(instantiation,[status(thm)],[115]) ).
cnf(l1217,plain,
a_select3(u_defuse,n0,n0) = use,
inference(instantiation,[status(thm)],[124]) ).
cnf(l1033,plain,
a_select2(xinit_noise_defuse,n3) = use,
inference(instantiation,[status(thm)],[139]) ).
cnf(l1215,plain,
a_select2(xinit_defuse,n5) = use,
inference(instantiation,[status(thm)],[129]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l763,l134,l795,l753,l762,l766,l781,l751,l757,l749,l758,l774,l138,l791,l130,l788,l132,l775,l754,l779,l773,l760,l1141,l786,l1107,l1098,l854,l1109,l1106,l771,l1138,l1093,l1096,l1076,l1159,l1124,l1117,l1201,l1226,l1113,l1151,l805,l1147,l848,l1146,l1050,l1110,l1077,l1043,l1062,l1058,l1154,l1111,l1149,l1094,l1150,l1112,l1153,l1189,l1052,l1086,l1099,l1101,l1089,l1105,l1,l1045,l1081,l1046,l1082,l1087,l1064,l1063,l1044,l1085,l1103,l1139,l1152,l1084,l1095,l1091,l1066,l1116,l1104,l1232,l1083,l1235,l1115,l1092,l1108,l1200,l752,l1097,l1079,l1078,l1119,l1155,l1148,l1080,l1135,l1102,l1074,l1057,l1053,l1071,l1026,l1047,l1070,l778,l1140,l1126,l750,l1048,l777,l1075,l1042,l1049,l1100,l1205,l1227,l1206,l1054,l1059,l1230,l1223,l792,l1145,l1177,l1051,l1241,l1183,l1167,l1242,l1246,l1191,l1202,l1208,l1088,l1192,l1220,l1214,l1197,l1225,l1186,l1211,l1172,l1221,l1090,l1185,l1142,l1222,l1179,l1196,l1243,l1174,l1199,l1168,l1212,l1162,l1203,l1180,l1068,l1182,l1144,l1160,l1181,l1239,l1204,l1173,l1219,l1061,l1175,l1037,l1122,l1184,l1207,l1170,l1056,l1169,l1161,l1228,l1065,l1178,l1143,l1127,l1249,l1251,l1072,l1210,l1120,l1157,l1262,l1237,l1250,l1136,l1067,l1247,l1130,l1229,l1125,l1121,l1158,l1188,l1231,l1164,l1209,l1198,l1118,l1128,l1171,l1166,l1213,l1236,l1165,l1240,l1245,l1176,l1055,l1134,l1233,l1244,l1238,l1218,l1248,l1123,l1187,l1261,l1027,l1224,l1029,l1038,l1032,l782,l1259,l1253,l1258,l1260,l1257,l1190,l1028,l1039,l1060,l1256,l1156,l1073,l1255,l1234,l1030,l1131,l1114,l1035,l1254,l1216,l1137,l1041,l1163,l1031,l1195,l1193,l1194,l1040,l1133,l1036,l1034,l1252,l1069,l1132,l1129,l1217,l1033,l1215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV096+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jul 22 08:12:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.19/0.34 % launching worker at depth: 3
% 0.19/0.34 % launching worker at depth: 4
% 0.19/0.34 % launching worker at depth: 2
% 0.19/0.34 % launching worker at depth: 1
% 0.19/0.34 % launching worker at depth: 6
% 0.19/0.34 % launching worker at depth: 5
% 0.19/0.34 % launching worker at depth: 7
% 0.19/0.34 % launching worker at depth: 8
% 2.55/0.71 % launching worker at depth: 9
% 25.13/3.51 % SZS status Theorem for theBenchmark
% 25.13/3.51 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------