%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV535-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:14 PM UTC 2026
% Result : Unsatisfiable 6.51s 3.07s
% Output : CNFRefutation 6.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 28
% Syntax : Number of formulae : 113 ( 43 unt; 25 def)
% Number of atoms : 596 ( 244 equ)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 136 ( 4 ~; 132 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 25 usr; 26 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 26 ( 0 sgn 26 !; 0 ?; 19 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,negated_conjecture,
select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))) != select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_54,negated_conjecture,
select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))) != select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i0)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3)),i2)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))),
inference(cnf_transformation,[],[f3]) ).
tcf(c_67,plain,
select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))) != select(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),sk(store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i2)),i2,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),store(store(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i2,select(store(store(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i2)),i2,select(store(store(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i0)),i0,select(store(store(a1,i1,select(a1,i1)),i1,select(a1,i1)),i3)),i3)),i0)))),
inference(demodulation,[status(thm)],[c_54,c_52]) ).
tcf(c_73,definition,
iPr_def_10 = select(a1,i1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_74,definition,
iPr_def_11 = store(a1,i1,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_75,definition,
iPr_def_12 = store(iPr_def_11,i1,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_76,definition,
iPr_def_13 = select(iPr_def_12,i0),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_77,definition,
iPr_def_14 = store(iPr_def_12,i3,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_78,definition,
iPr_def_15 = select(iPr_def_12,i3),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_79,definition,
iPr_def_16 = store(iPr_def_14,i0,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_80,definition,
iPr_def_17 = select(iPr_def_16,i2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_81,definition,
iPr_def_18 = store(iPr_def_16,i3,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_82,definition,
iPr_def_19 = select(iPr_def_16,i3),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_83,definition,
iPr_def_20 = store(iPr_def_18,i2,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_84,definition,
iPr_def_21 = store(iPr_def_20,i0,iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_85,definition,
iPr_def_22 = select(iPr_def_20,i0),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_86,definition,
iPr_def_23 = store(iPr_def_21,i2,iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_87,definition,
iPr_def_24 = store(iPr_def_12,i0,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_88,definition,
iPr_def_25 = store(iPr_def_24,i3,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_89,definition,
iPr_def_26 = select(iPr_def_25,i2),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_90,definition,
iPr_def_27 = store(iPr_def_25,i3,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_91,definition,
iPr_def_28 = store(iPr_def_27,i2,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_92,definition,
iPr_def_29 = select(iPr_def_28,i0),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_93,definition,
iPr_def_30 = store(iPr_def_28,i2,iPr_def_29),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_94,definition,
iPr_def_31 = store(iPr_def_30,i0,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_95,definition,
iPr_def_32 = sk(iPr_def_31,iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_96,definition,
iPr_def_33 = select(iPr_def_23,iPr_def_32),
introduced(definition,[new_symbols(definition,[iPr_def_33])],[]) ).
tcf(c_97,definition,
iPr_def_34 = select(iPr_def_31,iPr_def_32),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_98,plain,
iPr_def_33 != iPr_def_34,
inference(demodulation,[status(thm)],[c_67,c_97,c_92,c_89,c_87,c_88,c_90,c_91,c_93,c_94,c_95,c_85,c_82,c_80,c_78,c_76,c_73,c_74,c_75,c_77,c_79,c_81,c_83,c_84,c_86,c_96]) ).
tcf(c_196,plain,
select(iPr_def_14,i3) = iPr_def_13,
inference(superposition,[status(thm)],[c_77,c_52]) ).
tcf(c_197,plain,
select(iPr_def_16,i0) = iPr_def_15,
inference(superposition,[status(thm)],[c_79,c_52]) ).
tcf(c_198,plain,
select(iPr_def_18,i3) = iPr_def_17,
inference(superposition,[status(thm)],[c_81,c_52]) ).
tcf(c_199,plain,
select(iPr_def_20,i2) = iPr_def_19,
inference(superposition,[status(thm)],[c_83,c_52]) ).
tcf(c_200,plain,
select(iPr_def_21,i0) = iPr_def_19,
inference(superposition,[status(thm)],[c_84,c_52]) ).
tcf(c_201,plain,
select(iPr_def_23,i2) = iPr_def_22,
inference(superposition,[status(thm)],[c_86,c_52]) ).
tcf(c_202,plain,
select(iPr_def_24,i0) = iPr_def_15,
inference(superposition,[status(thm)],[c_87,c_52]) ).
tcf(c_204,plain,
select(iPr_def_27,i3) = iPr_def_26,
inference(superposition,[status(thm)],[c_90,c_52]) ).
tcf(c_205,plain,
select(iPr_def_28,i2) = iPr_def_13,
inference(superposition,[status(thm)],[c_91,c_52]) ).
tcf(c_206,plain,
select(iPr_def_30,i2) = iPr_def_29,
inference(superposition,[status(thm)],[c_93,c_52]) ).
tcf(c_207,plain,
select(iPr_def_31,i0) = iPr_def_13,
inference(superposition,[status(thm)],[c_94,c_52]) ).
tcf(c_213,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(iPr_def_12,X0) = select(iPr_def_14,X0) ) ),
inference(superposition,[status(thm)],[c_77,c_53]) ).
tcf(c_214,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(iPr_def_14,X0) = select(iPr_def_16,X0) ) ),
inference(superposition,[status(thm)],[c_79,c_53]) ).
tcf(c_215,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(iPr_def_16,X0) = select(iPr_def_18,X0) ) ),
inference(superposition,[status(thm)],[c_81,c_53]) ).
tcf(c_216,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(iPr_def_18,X0) = select(iPr_def_20,X0) ) ),
inference(superposition,[status(thm)],[c_83,c_53]) ).
tcf(c_217,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(iPr_def_20,X0) = select(iPr_def_21,X0) ) ),
inference(superposition,[status(thm)],[c_84,c_53]) ).
tcf(c_218,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(iPr_def_21,X0) = select(iPr_def_23,X0) ) ),
inference(superposition,[status(thm)],[c_86,c_53]) ).
tcf(c_219,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(iPr_def_12,X0) = select(iPr_def_24,X0) ) ),
inference(superposition,[status(thm)],[c_87,c_53]) ).
tcf(c_220,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(iPr_def_24,X0) = select(iPr_def_25,X0) ) ),
inference(superposition,[status(thm)],[c_88,c_53]) ).
tcf(c_221,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(iPr_def_25,X0) = select(iPr_def_27,X0) ) ),
inference(superposition,[status(thm)],[c_90,c_53]) ).
tcf(c_222,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(iPr_def_27,X0) = select(iPr_def_28,X0) ) ),
inference(superposition,[status(thm)],[c_91,c_53]) ).
tcf(c_223,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(iPr_def_28,X0) = select(iPr_def_30,X0) ) ),
inference(superposition,[status(thm)],[c_93,c_53]) ).
tcf(c_224,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(iPr_def_30,X0) = select(iPr_def_31,X0) ) ),
inference(superposition,[status(thm)],[c_94,c_53]) ).
tcf(c_272,plain,
( ( i0 = i2 )
| ( select(iPr_def_18,i0) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_216,c_85]) ).
tcf(c_325,plain,
( ( i0 = i2 )
| ( select(iPr_def_14,i2) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_214,c_80]) ).
tcf(c_326,plain,
( ( i0 = i3 )
| ( select(iPr_def_14,i3) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_214,c_82]) ).
tcf(c_328,plain,
( ( iPr_def_13 = iPr_def_19 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_326,c_196]) ).
tcf(c_348,plain,
( ( iPr_def_13 = iPr_def_19 )
| ( select(iPr_def_16,i3) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_328,c_197]) ).
tcf(c_355,plain,
( ( iPr_def_13 = iPr_def_19 )
| ( select(iPr_def_12,i3) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_328,c_76]) ).
tcf(c_356,plain,
( ( iPr_def_13 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_355,c_78]) ).
tcf(c_363,plain,
( ( iPr_def_15 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_348,c_82]) ).
tcf(c_405,plain,
( ( iPr_def_13 = iPr_def_15 )
| ( store(iPr_def_18,i2,iPr_def_13) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_356,c_83]) ).
tcf(c_435,plain,
( ( i3 = i2 )
| ( i0 = i2 )
| ( select(iPr_def_12,i2) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_213,c_325]) ).
tcf(c_480,plain,
( ( i2 = iPr_def_32 )
| ( select(iPr_def_21,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_218,c_96]) ).
tcf(c_553,plain,
( ( iPr_def_13 = iPr_def_15 )
| ( select(iPr_def_20,i2) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_405,c_52]) ).
tcf(c_591,plain,
( ( i0 = i2 )
| ( i0 = i3 )
| ( select(iPr_def_16,i0) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_215,c_272]) ).
tcf(c_592,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( i0 = i2 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_591,c_197]) ).
tcf(c_607,plain,
( ( i2 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_20,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_217,c_480]) ).
tcf(c_648,plain,
( ( i3 = i2 )
| ( select(iPr_def_24,i2) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_220,c_89]) ).
tcf(c_656,plain,
( ( i3 = i2 )
| ( i0 = i2 )
| ( select(iPr_def_12,i2) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_219,c_648]) ).
tcf(c_668,plain,
( ( i0 = i2 )
| ( select(iPr_def_27,i0) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_222,c_92]) ).
tcf(c_693,plain,
( ( i0 = i2 )
| ( i0 = i3 )
| ( select(iPr_def_25,i0) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_221,c_668]) ).
tcf(c_717,plain,
( ( i0 = iPr_def_32 )
| ( select(iPr_def_30,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_224,c_97]) ).
tcf(c_726,plain,
( ( i2 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_28,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_223,c_717]) ).
tcf(c_906,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( i0 = i3 )
| ( select(iPr_def_28,i0) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_592,c_205]) ).
tcf(c_908,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( i0 = i3 )
| ( select(iPr_def_20,i0) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_592,c_199]) ).
tcf(c_922,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_22 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_908,c_85]) ).
tcf(c_929,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_13 = iPr_def_29 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_906,c_92]) ).
tcf(c_1487,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_22 )
| ( i0 = i2 )
| ( select(iPr_def_27,i3) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_922,c_668]) ).
tcf(c_1491,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_22 )
| ( i0 = i2 )
| ( select(iPr_def_18,i3) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_922,c_272]) ).
tcf(c_1538,plain,
( ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_17 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_22 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1491,c_198]) ).
tcf(c_1547,plain,
( ( iPr_def_26 = iPr_def_29 )
| ( iPr_def_19 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_22 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1487,c_204]) ).
tcf(c_1589,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_13 = iPr_def_29 )
| ( select(iPr_def_16,i3) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_929,c_197]) ).
tcf(c_1607,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_15 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_1589,c_82]) ).
tcf(c_1826,plain,
( ( i2 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_18,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_216,c_607]) ).
tcf(c_1845,plain,
( ( iPr_def_17 = iPr_def_26 )
| ( i3 = i2 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_656,c_435]) ).
tcf(c_2012,plain,
( ( iPr_def_17 = iPr_def_26 )
| ( i3 = i2 )
| ( select(iPr_def_25,i0) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1845,c_89]) ).
tcf(c_2962,plain,
( ( i0 = i2 )
| ( i0 = i3 )
| ( select(iPr_def_24,i0) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_693,c_220]) ).
tcf(c_2966,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i0 = i2 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_2962,c_202]) ).
tcf(c_3174,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i0 = i3 )
| ( select(iPr_def_25,i0) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2966,c_89]) ).
tcf(c_4185,plain,
( ( i2 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_27,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_222,c_726]) ).
tcf(c_4781,plain,
( ( iPr_def_17 = iPr_def_26 )
| ( i3 = i2 )
| ( i0 = i3 )
| ( select(iPr_def_24,i0) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2012,c_220]) ).
tcf(c_5163,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_16,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_215,c_1826]) ).
tcf(c_5221,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i0 = i3 )
| ( select(iPr_def_24,i0) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_3174,c_220]) ).
tcf(c_7352,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_25,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_221,c_4185]) ).
tcf(c_29139,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_14,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_5163,c_214]) ).
tcf(c_29166,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_24,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_220,c_7352]) ).
tcf(c_31582,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_12,iPr_def_32) = iPr_def_33 ) ),
inference(superposition,[status(thm)],[c_213,c_29139]) ).
tcf(c_31599,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_12,iPr_def_32) = iPr_def_34 ) ),
inference(superposition,[status(thm)],[c_29166,c_219]) ).
tcf(c_31749,plain,
( ( iPr_def_33 = iPr_def_34 )
| ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 ) ),
inference(superposition,[status(thm)],[c_31599,c_31582]) ).
tcf(c_31750,plain,
( ( i2 = iPr_def_32 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31749,c_98]) ).
tcf(c_31860,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( i0 = i3 ) ),
inference(superposition,[status(thm)],[c_31750,c_2966]) ).
tcf(c_31885,plain,
( ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_25,iPr_def_32) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_31750,c_89]) ).
tcf(c_35293,plain,
( ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_24,iPr_def_32) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_220,c_31885]) ).
tcf(c_36969,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( i0 = i2 )
| ( select(iPr_def_27,i3) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_31860,c_668]) ).
tcf(c_36973,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( i0 = i2 )
| ( select(iPr_def_18,i3) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_31860,c_272]) ).
tcf(c_36977,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( select(iPr_def_16,i3) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_31860,c_197]) ).
tcf(c_36979,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 )
| ( store(iPr_def_12,i3,iPr_def_15) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_31860,c_87]) ).
tcf(c_37002,plain,
( ( iPr_def_15 = iPr_def_29 )
| ( iPr_def_15 = iPr_def_19 )
| ( i3 = iPr_def_32 )
| ( i0 = iPr_def_32 ) ),
inference(light_normalisation,[status(thm)],[c_36977,c_82]) ).
tcf(c_41744,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_37002,c_36979,c_36973,c_36969,c_35293,c_31750,c_5221,c_4781,c_4185,c_2966,c_1845,c_1826,c_1607,c_1547,c_1538,c_717,c_592,c_553,c_480,c_363,c_348,c_325,c_207,c_206,c_205,c_204,c_202,c_201,c_200,c_199,c_198,c_197,c_98,c_97,c_96,c_92,c_85,c_82,c_80,c_78,c_77]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV535-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.59 % Computer : n003.cluster.edu
% 0.13/0.59 % Model : x86_64 x86_64
% 0.13/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.59 % Memory : 8046.5625MB
% 0.13/0.59 % OS : Linux 6.8.0-71-generic
% 0.13/0.59 % CPULimit : 300
% 0.13/0.59 % WCLimit : 300
% 0.13/0.59 % DateTime : Thu Sep 24 20:22:36 UTC 2026
% 0.13/0.59 % CPUTime :
% 0.13/0.59 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/0.63 Running first-order theorem proving
% 0.16/0.63 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.64
% 0.16/0.64 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.64
% 0.16/0.64 % Detected problem language: tptp
% 0.16/0.66 % Proving...
% 6.51/3.07 % SZS status Started for theBenchmark.p
% 6.51/3.07 % SZS status Unsatisfiable for theBenchmark.p
% 6.51/3.07
% 6.51/3.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.51/3.07
% 6.51/3.07 % ------ iProver source info
% 6.51/3.07
% 6.51/3.07 % git: date: 2026-07-19 20:42:38 +0200
% 6.51/3.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.51/3.07 % git: non_committed_changes: false
% 6.51/3.07
% 6.51/3.07 % ------ Parsing...% successful
% 6.51/3.07
% 6.51/3.07
% 6.51/3.07 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.51/3.07
% 6.51/3.07 % ------ Preprocessing... sup_sim: 1 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.51/3.07
% 6.51/3.07 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.51/3.07
% 6.51/3.07 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.51/3.07 % ------ Proving...
% 6.51/3.07 % ------ Problem Properties
% 6.51/3.07
% 6.51/3.07 %
% 6.51/3.07 % clauses 28
% 6.51/3.07 % conjectures 0
% 6.51/3.07 % EPR 1
% 6.51/3.07 % Horn 27
% 6.51/3.07 % unary 27
% 6.51/3.07 % binary 1
% 6.51/3.07 % lits 29
% 6.51/3.07 % lits eq 29
% 6.51/3.07 % fd_pure 0
% 6.51/3.07 % fd_pseudo 0
% 6.51/3.07 % fd_cond 0
% 6.51/3.07 % fd_pseudo_cond 1
% 6.51/3.07 % AC symbols 0
% 6.51/3.07
% 6.51/3.07 % ------ Schedule dynamic 5 is on
% 6.51/3.07
% 6.51/3.07 % ------ no conjectures: strip conj schedule
% 6.51/3.07
% 6.51/3.07 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 6.51/3.07
% 6.51/3.07
% 6.51/3.07 % ------
% 6.51/3.07 % Current options:
% 6.51/3.07 % ------
% 6.51/3.07
% 6.51/3.07
% 6.51/3.07 %
% 6.51/3.07
% 6.51/3.07 % ------ Proving...
% 6.51/3.07 %
% 6.51/3.07
% 6.51/3.07 % SZS status Unsatisfiable for theBenchmark.p
% 6.51/3.07
% 6.51/3.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.51/3.07
% 6.51/3.07
%------------------------------------------------------------------------------