%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV539-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.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:13:34 PM UTC 2026
% Result : Unsatisfiable 49.37s 7.71s
% Output : Proof 49.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 87
% Number of leaves : 5
% Syntax : Number of formulae : 199 ( 20 unt; 0 def)
% Number of atoms : 768 ( 767 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 733 ( 164 ~; 569 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-3 aty)
% Number of variables : 64 ( 6 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f0_nnf,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f4,axiom,
( store(store(A,I,E),J,F) = store(store(A,J,F),I,E)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f4_nnf,plain,
! [I,J,A,E,F] :
( store(store(A,I,E),J,F) = store(store(A,J,F),I,E)
| I = J ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [I,J,A,E,F] :
( store(store(A,I,E),J,F) = store(store(A,J,F),I,E)
| I = J ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f1,axiom,
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f1_nnf,plain,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f5,negated_conjecture,
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/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f5_nnf,plain,
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(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
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(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
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,[status(esa)],[f5_sk]) ).
cnf(p14,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i2,select(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0))
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,c5]) ).
cnf(p25,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i2,select(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c1,p14]) ).
cnf(p27,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i0)),i2,select(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[c1,p25]) ).
cnf(p1488,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i2 = i0
| i3 = i0
| i3 = i2
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p27]) ).
cnf(p5344,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i2
| i2 = i0 ),
inference(factoring,[status(thm)],[p1488]) ).
cnf(p5386,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i0
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p5344]) ).
cnf(p5389,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5386]) ).
cnf(p5391,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p5389]) ).
cnf(p5409,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p5391]) ).
cnf(p5511,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c1,p5409]) ).
cnf(p5526,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5511]) ).
cnf(p5535,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p5526]) ).
cnf(p5538,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5535]) ).
cnf(p5644,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p5538]) ).
cnf(p5647,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p5644]) ).
cnf(p5653,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p5647]) ).
cnf(p5655,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5653]) ).
cnf(p5748,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p5655]) ).
cnf(p5762,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p5748]) ).
cnf(p5764,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p5762]) ).
cnf(p5799,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5764]) ).
cnf(p5805,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p5799]) ).
cnf(p6058,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p5805]) ).
cnf(p6060,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i3 = i2
| i2 = i0
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[c1,p6058]) ).
cnf(p6066,plain,
( store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6060]) ).
cnf(p6160,plain,
( i2 = i0
| i3 = i0
| i3 = i2 ),
inference(equality_resolution,[status(thm)],[p6066]) ).
cnf(p8,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(a1,i0)),i2,select(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0))
| i3 = i2 ),
inference(superposition,[status(thm)],[c1,c5]) ).
cnf(p6181,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i2
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[p6160,p8]) ).
cnf(p6353,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6181]) ).
cnf(p6413,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i2
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[p6160,p6353]) ).
cnf(p6418,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6413]) ).
cnf(p6420,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6418]) ).
cnf(p6423,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i0
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p6420]) ).
cnf(p6502,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p6423]) ).
cnf(p6510,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p6502]) ).
cnf(p6514,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p6510]) ).
cnf(p6522,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[p6160,p6514]) ).
cnf(p6599,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6522]) ).
cnf(p6601,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6599]) ).
cnf(p6609,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i3)),i2,select(a1,i0))
| i3 = i0
| i3 = i2
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[p6160,p6601]) ).
cnf(p6611,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i3)),i2,select(a1,i0))
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6609]) ).
cnf(p6691,plain,
( a1 != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i3)),i2,select(a1,i0))
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6611]) ).
cnf(p6696,plain,
( a1 != store(store(a1,i0,select(a1,i3)),i2,select(a1,i0))
| i3 = i0
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p6691]) ).
cnf(p6699,plain,
( a1 != store(store(a1,i0,select(a1,i3)),i2,select(a1,i0))
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p6696]) ).
cnf(p6702,plain,
( a1 != a1
| i3 = i2
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[p6160,p6699]) ).
cnf(p6769,plain,
( a1 != a1
| i3 = i0
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6702]) ).
cnf(p6771,plain,
( a1 != a1
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p6769]) ).
cnf(p6772,plain,
( i3 = i0
| i3 = i2 ),
inference(equality_resolution,[status(thm)],[p6771]) ).
cnf(p28,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p25]) ).
cnf(p6816,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[p6772,p28]) ).
cnf(p7162,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p6816]) ).
cnf(p7164,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7162]) ).
cnf(p7165,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c1,p7164]) ).
cnf(p7178,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7165]) ).
cnf(p7258,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[p6772,p7178]) ).
cnf(p7260,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7258]) ).
cnf(p7261,plain,
( a1 != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p7260]) ).
cnf(p7266,plain,
( a1 != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7261]) ).
cnf(p7294,plain,
( a1 != store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p7266]) ).
cnf(p7296,plain,
( a1 != store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7294]) ).
cnf(p7298,plain,
( a1 != store(store(a1,i3,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p7296]) ).
cnf(p7300,plain,
( a1 != store(store(a1,i3,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7298]) ).
cnf(p7327,plain,
( a1 != a1
| i2 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[p6772,p7300]) ).
cnf(p7328,plain,
( a1 != a1
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7327]) ).
cnf(p7329,plain,
( i2 = i0
| i3 = i0 ),
inference(equality_resolution,[status(thm)],[p7328]) ).
cnf(p7486,plain,
( i3 = i0
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[p7329,p6772]) ).
cnf(p7583,plain,
( i3 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p7486]) ).
cnf(p7584,plain,
i3 = i0,
inference(factoring,[status(thm)],[p7583]) ).
cnf(p1487,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i2 = i0
| i3 = i0
| i3 = i2
| i0 = i2 ),
inference(superposition,[status(thm)],[c4,p27]) ).
cnf(p2830,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i0
| i3 = i2
| i0 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p1487]) ).
cnf(p2835,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i2
| i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p2830]) ).
cnf(p2836,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i2
| i0 = i2
| i3 = i0
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p2835]) ).
cnf(p2926,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i2
| i3 = i0
| i0 = i2 ),
inference(factoring,[status(thm)],[p2836]) ).
cnf(p2927,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i2
| i3 = i0
| i0 = i2
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p2926]) ).
cnf(p2949,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2
| i2 = i0 ),
inference(factoring,[status(thm)],[p2927]) ).
cnf(p2950,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c1,p2949]) ).
cnf(p3023,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i0 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p2950]) ).
cnf(p3024,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i0 = i2
| i2 = i0
| i3 = i0
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p3023]) ).
cnf(p3038,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0
| i0 = i2 ),
inference(factoring,[status(thm)],[p3024]) ).
cnf(p3039,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i3 = i2
| i2 = i0
| i3 = i0
| i0 = i2
| i3 = i2 ),
inference(superposition,[status(thm)],[c1,p3038]) ).
cnf(p3084,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i0
| i0 = i2
| i3 = i2 ),
inference(factoring,[status(thm)],[p3039]) ).
cnf(p3094,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3084]) ).
cnf(p3096,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3094]) ).
cnf(p3102,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i0 = i2
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p3096]) ).
cnf(p3182,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p3102]) ).
cnf(p3188,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3182]) ).
cnf(p3189,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p3188]) ).
cnf(p3190,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p3189]) ).
cnf(p3273,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p3190]) ).
cnf(p3274,plain,
( store(store(a1,i3,select(a1,i2)),i2,select(a1,i3)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3273]) ).
cnf(p3278,plain,
( store(store(a1,i3,select(a1,i2)),i2,select(a1,i3)) != store(store(a1,i3,select(a1,i2)),i2,select(a1,i3))
| i0 = i2
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p3274]) ).
cnf(p3279,plain,
( i0 = i2
| i3 = i2
| i2 = i0
| i3 = i0 ),
inference(equality_resolution,[status(thm)],[p3278]) ).
cnf(p3351,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i3 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[p3279,p8]) ).
cnf(p3427,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3351]) ).
cnf(p3450,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[p3279,p3427]) ).
cnf(p3455,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3450]) ).
cnf(p3499,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3455]) ).
cnf(p3501,plain,
( store(store(store(a1,i0,select(a1,i3)),i3,select(store(a1,i0,select(a1,i3)),i2)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3499]) ).
cnf(p3505,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3501]) ).
cnf(p3518,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3505]) ).
cnf(p3611,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i0 = i2
| i3 = i2
| i3 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3518]) ).
cnf(p3617,plain,
( store(a1,i3,select(store(a1,i0,select(a1,i3)),i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3611]) ).
cnf(p3619,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i0 = i2
| i3 = i2
| i3 = i0
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p3617]) ).
cnf(p3631,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2 ),
inference(factoring,[status(thm)],[p3619]) ).
cnf(p3717,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p3631]) ).
cnf(p3727,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2 ),
inference(factoring,[status(thm)],[p3717]) ).
cnf(p3729,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i0))
| i3 = i2
| i3 = i0
| i0 = i2
| i3 = i2 ),
inference(superposition,[status(thm)],[c1,p3727]) ).
cnf(p3738,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i0))
| i3 = i0
| i0 = i2
| i3 = i2 ),
inference(factoring,[status(thm)],[p3729]) ).
cnf(p3817,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i0))
| i3 = i0
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p3738]) ).
cnf(p3903,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i2)),i2,select(a1,i0))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3817]) ).
cnf(p3905,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(a1,i0,select(a1,i3)),i2,select(a1,i0)),i3,select(a1,i2))
| i0 = i2
| i3 = i2
| i3 = i0
| i3 = i2 ),
inference(superposition,[status(thm)],[c4,p3903]) ).
cnf(p3979,plain,
( store(a1,i3,select(a1,i2)) != store(store(store(a1,i0,select(a1,i3)),i2,select(a1,i0)),i3,select(a1,i2))
| i0 = i2
| i3 = i0
| i3 = i2 ),
inference(factoring,[status(thm)],[p3905]) ).
cnf(p3983,plain,
( store(a1,i3,select(a1,i2)) != store(a1,i3,select(a1,i2))
| i0 = i2
| i3 = i0
| i3 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[p3279,p3979]) ).
cnf(p4025,plain,
( store(a1,i3,select(a1,i2)) != store(a1,i3,select(a1,i2))
| i0 = i2
| i3 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p3983]) ).
cnf(p4028,plain,
( store(a1,i3,select(a1,i2)) != store(a1,i3,select(a1,i2))
| i0 = i2
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4025]) ).
cnf(p4030,plain,
( store(a1,i3,select(a1,i2)) != store(a1,i3,select(a1,i2))
| i0 = i2
| i3 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4028]) ).
cnf(p4113,plain,
( i0 = i2
| i3 = i2
| i3 = i0 ),
inference(equality_resolution,[status(thm)],[p4030]) ).
cnf(f3,axiom,
store(store(A,I,E),I,F) = store(A,I,F),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f3_nnf,plain,
! [A,I,E,F] : store(store(A,I,E),I,F) = store(A,I,F),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,I,E,F] : store(store(A,I,E),I,F) = store(A,I,F),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p31,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i2,select(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3 ),
inference(superposition,[status(thm)],[c1,p25]) ).
cnf(p43,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3 ),
inference(superposition,[status(thm)],[c3,p31]) ).
cnf(p48,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3
| i0 = i3 ),
inference(superposition,[status(thm)],[c1,p43]) ).
cnf(p49,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3 ),
inference(factoring,[status(thm)],[p48]) ).
cnf(p51,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p49]) ).
cnf(p1153,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i3 = i0
| i0 = i3
| i2 = i0 ),
inference(factoring,[status(thm)],[p51]) ).
cnf(p1154,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i3 = i0
| i0 = i3
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c1,p1153]) ).
cnf(p1214,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i0 = i3
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p1154]) ).
cnf(p1215,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0,select(a1,i0)),i2,select(a1,i3))
| i0 = i3
| i2 = i0
| i3 = i0
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p1214]) ).
cnf(p1243,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i0 = i3
| i2 = i0
| i3 = i0
| i0 = i2
| i0 = i2 ),
inference(superposition,[status(thm)],[c4,p1215]) ).
cnf(p1252,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0))
| i0 = i3
| i2 = i0
| i3 = i0
| i0 = i2 ),
inference(factoring,[status(thm)],[p1243]) ).
cnf(p1299,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i0 = i3
| i2 = i0
| i3 = i0
| i0 = i2
| i0 = i3 ),
inference(superposition,[status(thm)],[c4,p1252]) ).
cnf(p1303,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i0,select(a1,i3)),i2,select(a1,i3)),i0,select(a1,i0))
| i2 = i0
| i3 = i0
| i0 = i2
| i0 = i3 ),
inference(factoring,[status(thm)],[p1299]) ).
cnf(p1313,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i2
| i0 = i3
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p1303]) ).
cnf(p1317,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i0,select(a1,i0)),i2,select(a1,i3))
| i3 = i0
| i0 = i2
| i0 = i3
| i2 = i0 ),
inference(factoring,[status(thm)],[p1313]) ).
cnf(p1357,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i3 = i0
| i0 = i2
| i0 = i3
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p1317]) ).
cnf(p1359,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)),i0,select(a1,i0)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p1357]) ).
cnf(p1362,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i2 = i0
| i3 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p1359]) ).
cnf(p1416,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0,select(a1,i0)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i3 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p1362]) ).
cnf(p1419,plain,
( store(store(a1,i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i3 = i0
| i2 = i0
| i3 = i0 ),
inference(superposition,[status(thm)],[c4,p1416]) ).
cnf(p1426,plain,
( store(store(a1,i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i2 = i0
| i3 = i0 ),
inference(factoring,[status(thm)],[p1419]) ).
cnf(p1461,plain,
( store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i0 = i3
| i2 = i0
| i3 = i0
| i0 = i3 ),
inference(superposition,[status(thm)],[c4,p1426]) ).
cnf(p1498,plain,
( store(store(a1,i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i2 = i0
| i3 = i0
| i0 = i3 ),
inference(factoring,[status(thm)],[p1461]) ).
cnf(p1501,plain,
( store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i0 = i2
| i2 = i0
| i3 = i0
| i0 = i3
| i0 = i2 ),
inference(superposition,[status(thm)],[c1,p1498]) ).
cnf(p1504,plain,
( store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3)) != store(store(a1,i3,select(store(a1,i3,select(a1,i0)),i2)),i2,select(a1,i3))
| i2 = i0
| i3 = i0
| i0 = i3
| i0 = i2 ),
inference(factoring,[status(thm)],[p1501]) ).
cnf(p1505,plain,
( i2 = i0
| i3 = i0
| i0 = i3
| i0 = i2 ),
inference(equality_resolution,[status(thm)],[p1504]) ).
cnf(p1537,plain,
( i2 != i3
| i2 = i0
| i3 = i0
| i0 = i2 ),
inference(equality_factoring,[status(thm)],[p1505]) ).
cnf(p4187,plain,
( i3 != i3
| i2 = i0
| i3 = i0
| i0 = i2
| i0 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[p4113,p1537]) ).
cnf(p4300,plain,
( i3 != i3
| i2 = i0
| i0 = i2
| i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4187]) ).
cnf(p4387,plain,
( i3 != i3
| i2 = i0
| i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4300]) ).
cnf(p4388,plain,
( i2 = i0
| i0 = i2
| i3 = i0 ),
inference(equality_resolution,[status(thm)],[p4387]) ).
cnf(p4500,plain,
( i0 = i2
| i3 = i0
| i3 = i0
| i0 = i2
| i3 = i0 ),
inference(superposition,[status(thm)],[p4388,p4113]) ).
cnf(p4507,plain,
( i0 = i2
| i3 = i0
| i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4500]) ).
cnf(p4562,plain,
( i0 = i2
| i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4507]) ).
cnf(p4564,plain,
( i0 = i2
| i3 = i0 ),
inference(factoring,[status(thm)],[p4562]) ).
cnf(p89,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0))
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,c5]) ).
cnf(p6679,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(a1,i3,select(a1,i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0))
| i2 = i0
| i0 = i2 ),
inference(superposition,[status(thm)],[p4564,p89]) ).
cnf(p8678,plain,
( store(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i2,select(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0))
| i2 = i0
| i0 = i2 ),
inference(demodulation,[status(thm)],[p7584,p6679]) ).
cnf(p8767,plain,
( store(store(store(a1,i0,select(a1,i2)),i2,select(store(store(a1,i0,select(a1,i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != a1
| i2 = i0
| i0 = i2
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p8678]) ).
cnf(p8781,plain,
( store(store(store(a1,i0,select(a1,i2)),i2,select(store(store(a1,i0,select(a1,i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != a1
| i0 = i2
| i2 = i0 ),
inference(factoring,[status(thm)],[p8767]) ).
cnf(p8782,plain,
( store(store(store(a1,i0,select(a1,i2)),i2,select(a1,i2)),i0,select(a1,i0)) != a1
| i0 = i2
| i2 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p8781]) ).
cnf(p8789,plain,
( store(store(store(a1,i0,select(a1,i2)),i2,select(a1,i2)),i0,select(a1,i0)) != a1
| i0 = i2
| i2 = i0 ),
inference(factoring,[status(thm)],[p8782]) ).
cnf(p8808,plain,
( a1 != a1
| i0 = i2
| i2 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p8789]) ).
cnf(p8810,plain,
( a1 != a1
| i0 = i2
| i2 = i0 ),
inference(factoring,[status(thm)],[p8808]) ).
cnf(p8811,plain,
( i0 = i2
| i2 = i0 ),
inference(equality_resolution,[status(thm)],[p8810]) ).
cnf(p6773,plain,
( i2 != i0
| i3 = i2 ),
inference(equality_factoring,[status(thm)],[p6772]) ).
cnf(p8703,plain,
( i2 != i0
| i0 = i2 ),
inference(demodulation,[status(thm)],[p7584,p6773]) ).
cnf(p8812,plain,
( i0 = i2
| i0 = i2 ),
inference(resolution,[status(thm)],[p8811,p8703]) ).
cnf(p8835,plain,
i0 = i2,
inference(factoring,[status(thm)],[p8812]) ).
cnf(p20,plain,
( store(store(store(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0))
| i2 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c1,p14]) ).
cnf(p1062,plain,
( store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i0)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3))
| i2 = i0
| i2 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[c4,p20]) ).
cnf(p7767,plain,
( store(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i0)),i0,select(a1,i0)) != store(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0))
| i2 = i0
| i2 = i0
| i2 = i0 ),
inference(demodulation,[status(thm)],[p7584,p1062]) ).
cnf(p8839,plain,
( a1 != store(store(store(a1,i0,select(a1,i2)),i2,select(a1,i2)),i0,select(a1,i0))
| i2 = i0
| i2 = i0
| i2 = i0 ),
inference(superposition,[status(thm)],[p8835,p7767]) ).
cnf(p8843,plain,
( a1 != store(store(store(a1,i0,select(a1,i2)),i2,select(a1,i2)),i0,select(a1,i0))
| i2 = i0
| i2 = i0 ),
inference(factoring,[status(thm)],[p8839]) ).
cnf(p8867,plain,
( a1 != store(store(store(a1,i0,select(a1,i2)),i2,select(a1,i2)),i0,select(a1,i0))
| i2 = i0 ),
inference(factoring,[status(thm)],[p8843]) ).
cnf(p8869,plain,
( a1 != a1
| i2 = i0 ),
inference(superposition,[status(thm)],[p8835,p8867]) ).
cnf(p8871,plain,
i2 = i0,
inference(equality_resolution,[status(thm)],[p8869]) ).
cnf(p39,plain,
store(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i3)),i3,select(store(store(a1,i0,select(a1,i3)),i3,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i2,select(store(store(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i2)),i2,select(store(store(a1,i3,select(a1,i0)),i0,select(a1,i3)),i3)),i0)),
inference(superposition,[status(thm)],[c3,c5]) ).
cnf(p7599,plain,
store(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i2,select(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i2)),i2,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0)),
inference(demodulation,[status(thm)],[p7584,p39]) ).
cnf(p8875,plain,
store(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(store(a1,i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(a1,i0)),i0)),i0,select(a1,i0)) != store(store(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0,select(store(store(a1,i0,select(a1,i0)),i0,select(a1,i0)),i0)),i0)),
inference(demodulation,[status(thm)],[p8871,p7599]) ).
cnf(p8955,plain,
a1 != a1,
inference(superposition,[status(thm)],[c0,p8875]) ).
cnf(p8956,plain,
$false,
inference(equality_resolution,[status(thm)],[p8955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV539-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Thu Sep 24 20:20:39 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 49.37/7.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.37/7.71 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------