%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV553-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 : n012.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:32 PM UTC 2026
% Result : Unsatisfiable 6.91s 2.58s
% Output : CNFRefutation 6.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 7
% Syntax : Number of formulae : 167 ( 21 unt; 3 def)
% Number of atoms : 1213 ( 512 equ)
% Maximal formula atoms : 7 ( 7 avg)
% Number of connectives : 349 ( 3 ~; 346 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-3 aty)
% Number of variables : 37 ( 0 sgn 37 !; 0 ?; 30 :)
% 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,axiom,
store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f4,negated_conjecture,
select(a1,sk(a1,a2)) != select(a2,sk(a1,a2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_54,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_55,plain,
store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_56,negated_conjecture,
select(a1,sk(a1,a2)) != select(a2,sk(a1,a2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_76,definition,
iPr_def_10 = sk(a1,a2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_77,definition,
iPr_def_11 = select(a1,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_78,definition,
iPr_def_12 = select(a2,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_79,negated_conjecture,
iPr_def_11 != iPr_def_12,
inference(demodulation,[status(thm)],[c_56,c_78,c_76,c_77]) ).
tcf(c_142,plain,
( ( i2 = i3 )
| ( store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)) = store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) ) ),
inference(superposition,[status(thm)],[c_54,c_55]) ).
tcf(c_144,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),X0) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_55,c_54]) ).
tcf(c_145,plain,
select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i4) = select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4),
inference(superposition,[status(thm)],[c_55,c_53]) ).
tcf(c_159,plain,
select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4),
inference(demodulation,[status(thm)],[c_145,c_53]) ).
tcf(c_162,plain,
( ( i1 = i2 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_159]) ).
tcf(c_163,plain,
( ( i2 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_159]) ).
tcf(c_165,plain,
( ( i3 = i4 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4) ) ),
inference(superposition,[status(thm)],[c_159,c_54]) ).
tcf(c_224,plain,
( ( i3 = i4 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4) ) ),
inference(superposition,[status(thm)],[c_165,c_54]) ).
tcf(c_242,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4) = select(store(a2,i1,select(a1,i1)),i4) ) ),
inference(superposition,[status(thm)],[c_224,c_54]) ).
tcf(c_261,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(store(a1,i1,select(a2,i1)),i4) = select(store(a2,i1,select(a1,i1)),i4) ) ),
inference(superposition,[status(thm)],[c_242,c_54]) ).
tcf(c_300,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(store(a1,i1,select(a2,i1)),i4) = select(a2,i4) ) ),
inference(superposition,[status(thm)],[c_54,c_261]) ).
tcf(c_314,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(a1,i4) = select(a2,i4) ) ),
inference(superposition,[status(thm)],[c_54,c_300]) ).
tcf(c_916,plain,
( ( i1 = i2 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_162]) ).
tcf(c_917,plain,
( ( i2 = i3 )
| ( i1 = i2 )
| ( select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4) = select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_162]) ).
tcf(c_1047,plain,
( ( i2 = i3 )
| ( store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)) = store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)) ) ),
inference(light_normalisation,[status(thm)],[c_142,c_159]) ).
tcf(c_1405,plain,
( ( i2 = i3 )
| ( i1 = i2 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_917]) ).
tcf(c_1451,plain,
( ( i2 = i3 )
| ( i1 = i2 )
| ( store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)) ) ),
inference(superposition,[status(thm)],[c_1405,c_1047]) ).
tcf(c_1611,plain,
( ( i2 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_163]) ).
tcf(c_1692,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),X0) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0) ) ),
inference(light_normalisation,[status(thm)],[c_144,c_159]) ).
tcf(c_1706,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)),X0) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_163,c_1692]) ).
tcf(c_1707,plain,
! [X0: $i] :
( ( i3 = i4 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4)),X0) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_165,c_1692]) ).
tcf(c_1712,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_1692,c_54]) ).
tcf(c_1771,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_1611]) ).
tcf(c_1803,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4) ) ),
inference(superposition,[status(thm)],[c_54,c_1771]) ).
tcf(c_2528,plain,
( ( i3 = i4 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i3) = select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) ) ),
inference(superposition,[status(thm)],[c_1712,c_53]) ).
tcf(c_2529,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),X0) ) ),
inference(superposition,[status(thm)],[c_1712,c_54]) ).
tcf(c_2680,plain,
( ( i3 = i4 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3) ) ),
inference(demodulation,[status(thm)],[c_2528,c_53]) ).
tcf(c_2688,plain,
( ( i3 = i4 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3) ) ),
inference(superposition,[status(thm)],[c_54,c_2680]) ).
tcf(c_2689,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3) = select(store(a2,i1,select(a1,i1)),i3) ) ),
inference(superposition,[status(thm)],[c_2680,c_54]) ).
tcf(c_2744,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( select(store(a1,i1,select(a2,i1)),i3) = select(store(a2,i1,select(a1,i1)),i3) ) ),
inference(superposition,[status(thm)],[c_2689,c_54]) ).
tcf(c_2842,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( select(store(a1,i1,select(a2,i1)),i3) = select(a2,i3) ) ),
inference(superposition,[status(thm)],[c_54,c_2744]) ).
tcf(c_2994,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( select(a1,i3) = select(a2,i3) ) ),
inference(superposition,[status(thm)],[c_54,c_2842]) ).
tcf(c_3405,plain,
( ( i3 = i4 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3) ) ),
inference(superposition,[status(thm)],[c_54,c_2688]) ).
tcf(c_3815,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),X0) ) ),
inference(superposition,[status(thm)],[c_2529,c_54]) ).
tcf(c_3910,plain,
! [X0: $i] :
( ( i1 = i2 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0) = select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),X0) ) ),
inference(superposition,[status(thm)],[c_54,c_3815]) ).
tcf(c_3911,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2) = select(store(a1,i1,select(a2,i1)),i2) ) ),
inference(superposition,[status(thm)],[c_3815,c_53]) ).
tcf(c_3912,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0) = select(store(a2,i1,select(a1,i1)),X0) ) ),
inference(superposition,[status(thm)],[c_3815,c_54]) ).
tcf(c_3939,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( select(store(a1,i1,select(a2,i1)),i2) = select(store(a2,i1,select(a1,i1)),i2) ) ),
inference(demodulation,[status(thm)],[c_3911,c_53]) ).
tcf(c_5379,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(store(a1,i1,select(a2,i1)),X0) = select(store(a2,i1,select(a1,i1)),X0) ) ),
inference(superposition,[status(thm)],[c_3912,c_54]) ).
tcf(c_5475,plain,
( ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(store(a1,i1,select(a2,i1)),i1) = select(a1,i1) ) ),
inference(superposition,[status(thm)],[c_5379,c_53]) ).
tcf(c_5476,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(store(a1,i1,select(a2,i1)),X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_5379,c_54]) ).
tcf(c_5537,plain,
( ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = select(a2,i1) ) ),
inference(demodulation,[status(thm)],[c_5475,c_53]) ).
tcf(c_6660,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(a1,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_5476,c_54]) ).
tcf(c_6851,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( select(a1,iPr_def_10) = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_6660,c_78]) ).
tcf(c_6887,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_6851,c_77]) ).
tcf(c_6888,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6887,c_79]) ).
tcf(c_6979,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i4 )
| ( select(a1,iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_6888,c_314]) ).
tcf(c_6987,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i4 ) ),
inference(light_normalisation,[status(thm)],[c_6979,c_77,c_78]) ).
tcf(c_6988,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i4 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6987,c_79]) ).
tcf(c_8015,plain,
( ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i4 ) ),
inference(superposition,[status(thm)],[c_6888,c_6988]) ).
tcf(c_8377,plain,
! [X0: $i] :
( ( i1 = i2 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),X0) = select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),X0) ) ),
inference(superposition,[status(thm)],[c_54,c_3910]) ).
tcf(c_8807,plain,
( ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i4 ) ),
inference(superposition,[status(thm)],[c_8015,c_6888]) ).
tcf(c_8912,plain,
( ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_8807,c_6888]) ).
tcf(c_9023,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 )
| ( select(a1,iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_8912,c_2994]) ).
tcf(c_9097,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_9023,c_77,c_78]) ).
tcf(c_9098,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9097,c_79]) ).
tcf(c_9843,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i3) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i3) ) ),
inference(superposition,[status(thm)],[c_9098,c_1803]) ).
tcf(c_16973,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 )
| ( select(a1,i3) = select(a2,i3) ) ),
inference(demodulation,[status(thm)],[c_9843,c_53]) ).
tcf(c_16989,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 )
| ( select(a1,iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_8912,c_16973]) ).
tcf(c_17005,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_16989,c_77,c_78]) ).
tcf(c_17006,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_17005,c_79]) ).
tcf(c_17072,plain,
( ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i3 ) ),
inference(superposition,[status(thm)],[c_17006,c_8912]) ).
tcf(c_17195,plain,
( ( i2 = iPr_def_10 )
| ( i1 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_17072,c_8912]) ).
tcf(c_17911,plain,
! [X0: $i] :
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,select(a2,iPr_def_10)),X0) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,select(a1,iPr_def_10)),X0) ) ),
inference(superposition,[status(thm)],[c_17195,c_8377]) ).
tcf(c_17923,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = select(store(a2,i1,select(a1,i1)),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_17195,c_3939]) ).
tcf(c_17931,plain,
( ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,select(a2,iPr_def_10)),i3) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,select(a1,iPr_def_10)),i3) ) ),
inference(superposition,[status(thm)],[c_17195,c_3405]) ).
tcf(c_18070,plain,
( ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),i3) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),i3) ) ),
inference(light_normalisation,[status(thm)],[c_17931,c_77,c_78]) ).
tcf(c_18108,plain,
! [X0: $i] :
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),X0) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),X0) ) ),
inference(light_normalisation,[status(thm)],[c_17911,c_77,c_78]) ).
tcf(c_20726,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_54,c_17923]) ).
tcf(c_20728,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = iPr_def_12 ) ),
inference(light_normalisation,[status(thm)],[c_20726,c_78]) ).
tcf(c_20745,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(a1,iPr_def_10) = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_20728,c_54]) ).
tcf(c_20747,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_20745,c_77]) ).
tcf(c_20748,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_20747,c_79]) ).
tcf(c_20852,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2) = select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i2) ) ),
inference(superposition,[status(thm)],[c_20748,c_224]) ).
tcf(c_22455,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),i2) = select(store(a2,i1,select(a1,i1)),i2) ) ),
inference(demodulation,[status(thm)],[c_20852,c_53]) ).
tcf(c_22470,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = select(store(a2,i1,select(a1,i1)),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_17195,c_22455]) ).
tcf(c_23091,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_54,c_22470]) ).
tcf(c_23093,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(store(a1,i1,select(a2,i1)),iPr_def_10) = iPr_def_12 ) ),
inference(light_normalisation,[status(thm)],[c_23091,c_78]) ).
tcf(c_23110,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 )
| ( select(a1,iPr_def_10) = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_23093,c_54]) ).
tcf(c_23112,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_23110,c_77]) ).
tcf(c_23113,plain,
( ( i3 = i4 )
| ( i2 = i3 )
| ( i1 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23112,c_79]) ).
tcf(c_23134,plain,
( ( i2 = i3 )
| ( i1 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_23113,c_20748]) ).
tcf(c_23964,plain,
( ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),i2) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),i2) ) ),
inference(superposition,[status(thm)],[c_23134,c_18070]) ).
tcf(c_26316,plain,
( ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),iPr_def_10) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_17195,c_23964]) ).
tcf(c_26322,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(demodulation,[status(thm)],[c_26316,c_53]) ).
tcf(c_26323,plain,
( ( i3 = i4 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_26322,c_79]) ).
tcf(c_26396,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i3) = select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i3) ) ),
inference(superposition,[status(thm)],[c_26323,c_916]) ).
tcf(c_28970,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),iPr_def_10) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_18108,c_53]) ).
tcf(c_28983,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(demodulation,[status(thm)],[c_28970,c_53]) ).
tcf(c_28984,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_28983,c_79]) ).
tcf(c_29004,plain,
( ( i3 = iPr_def_10 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_28984,c_26323]) ).
tcf(c_30281,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3) = select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3) ) ),
inference(demodulation,[status(thm)],[c_26396,c_53]) ).
tcf(c_30295,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,select(a2,iPr_def_10)),i3) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,select(a1,iPr_def_10)),i3) ) ),
inference(superposition,[status(thm)],[c_17195,c_30281]) ).
tcf(c_30323,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),i3) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),i3) ) ),
inference(light_normalisation,[status(thm)],[c_30295,c_77,c_78]) ).
tcf(c_31076,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 )
| ( select(store(store(a1,i1,select(a2,i1)),iPr_def_10,iPr_def_12),iPr_def_10) = select(store(store(a2,i1,select(a1,i1)),iPr_def_10,iPr_def_11),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_29004,c_30323]) ).
tcf(c_31085,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(demodulation,[status(thm)],[c_31076,c_53]) ).
tcf(c_31086,plain,
( ( i1 = iPr_def_10 )
| ( i1 = i2 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31085,c_79]) ).
tcf(c_31126,plain,
i1 = iPr_def_10,
inference(superposition,[status(thm)],[c_31086,c_17195]) ).
tcf(c_31338,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( select(a1,iPr_def_10) = select(a2,iPr_def_10) ) ),
inference(demodulation,[status(thm)],[c_5537,c_31126]) ).
tcf(c_31353,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2,select(a2,i2)),i3) = select(store(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2,select(a1,i2)),i3) ) ),
inference(demodulation,[status(thm)],[c_3405,c_31126]) ).
tcf(c_31437,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(store(a1,iPr_def_10,select(a2,iPr_def_10)),i4) = select(store(a2,iPr_def_10,select(a1,iPr_def_10)),i4) ) ),
inference(demodulation,[status(thm)],[c_261,c_31126]) ).
tcf(c_31439,plain,
( ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2,select(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2)),i4) = select(store(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2,select(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2)),i4) ) ),
inference(demodulation,[status(thm)],[c_224,c_31126]) ).
tcf(c_31442,plain,
select(store(store(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2,select(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2)),i3,select(store(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2,select(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2)),i3)),i4) = select(store(store(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2,select(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2)),i3,select(store(store(a1,iPr_def_10,select(a2,iPr_def_10)),i2,select(store(a2,iPr_def_10,select(a1,iPr_def_10)),i2)),i3)),i4),
inference(demodulation,[status(thm)],[c_159,c_31126]) ).
tcf(c_31443,plain,
select(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3)),i4) = select(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3)),i4),
inference(light_normalisation,[status(thm)],[c_31442,c_77,c_78]) ).
tcf(c_31450,plain,
( ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i4) = select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i4) ) ),
inference(light_normalisation,[status(thm)],[c_31439,c_77,c_78]) ).
tcf(c_31457,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(store(a1,iPr_def_10,iPr_def_12),i4) = select(store(a2,iPr_def_10,iPr_def_11),i4) ) ),
inference(light_normalisation,[status(thm)],[c_31437,c_77,c_78]) ).
tcf(c_31827,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(a2,i2)),i3) = select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(a1,i2)),i3) ) ),
inference(light_normalisation,[status(thm)],[c_31353,c_77,c_78]) ).
tcf(c_31899,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 ) ),
inference(light_normalisation,[status(thm)],[c_31338,c_77,c_78]) ).
tcf(c_31900,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31899,c_79]) ).
tcf(c_33090,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 )
| ( select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10) = select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_31900,c_31457]) ).
tcf(c_33144,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 ) ),
inference(demodulation,[status(thm)],[c_33090,c_53]) ).
tcf(c_33145,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33144,c_79]) ).
tcf(c_33164,plain,
( ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 )
| ( i2 = i4 ) ),
inference(superposition,[status(thm)],[c_33145,c_31900]) ).
tcf(c_33183,plain,
( ( i3 = iPr_def_10 )
| ( i2 = iPr_def_10 ) ),
inference(superposition,[status(thm)],[c_33164,c_31900]) ).
tcf(c_36061,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(a2,i2)),iPr_def_10) = select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(a1,i2)),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_33183,c_31827]) ).
tcf(c_36138,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(a2,i2)),iPr_def_10) = select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_54,c_36061]) ).
tcf(c_36143,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(a2,i2)),iPr_def_10) = iPr_def_11 ) ),
inference(demodulation,[status(thm)],[c_36138,c_53]) ).
tcf(c_36156,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 )
| ( select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10) = iPr_def_11 ) ),
inference(superposition,[status(thm)],[c_36143,c_54]) ).
tcf(c_36386,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = i4 )
| ( i2 = iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_36156,c_53]) ).
tcf(c_36387,plain,
( ( i3 = i4 )
| ( i2 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_36386,c_79]) ).
tcf(c_37678,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( store(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(a2,iPr_def_10,iPr_def_11),i3)),i4,select(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3)),i4)) = store(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3)),i4,select(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(a1,i2)),i3,select(store(a1,iPr_def_10,iPr_def_12),i3)),i4)) ) ),
inference(light_normalisation,[status(thm)],[c_1451,c_77,c_78,c_31126]) ).
tcf(c_37717,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( store(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(a2,iPr_def_10,iPr_def_11),i3)),i3,select(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3)),i3)) = store(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3)),i3,select(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(a1,i2)),i3,select(store(a1,iPr_def_10,iPr_def_12),i3)),i3)) ) ),
inference(superposition,[status(thm)],[c_36387,c_37678]) ).
tcf(c_39580,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( store(store(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3)),i3,select(store(a1,iPr_def_10,iPr_def_12),i3)) = store(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(a2,iPr_def_10,iPr_def_11),i3)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3)) ) ),
inference(demodulation,[status(thm)],[c_37717,c_53]) ).
tcf(c_39611,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( select(store(store(store(store(a1,iPr_def_10,iPr_def_12),i2,select(store(a2,iPr_def_10,iPr_def_11),i2)),i3,select(store(a2,iPr_def_10,iPr_def_11),i3)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3)),i3) = select(store(a1,iPr_def_10,iPr_def_12),i3) ) ),
inference(superposition,[status(thm)],[c_39580,c_53]) ).
tcf(c_39813,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( select(store(store(a2,iPr_def_10,iPr_def_11),i2,select(store(a1,iPr_def_10,iPr_def_12),i2)),i3) = select(store(a1,iPr_def_10,iPr_def_12),i3) ) ),
inference(demodulation,[status(thm)],[c_39611,c_53]) ).
tcf(c_39830,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( select(store(a1,iPr_def_10,iPr_def_12),i3) = select(store(a2,iPr_def_10,iPr_def_11),i3) ) ),
inference(superposition,[status(thm)],[c_39813,c_54]) ).
tcf(c_39893,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 )
| ( select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10) = select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_33183,c_39830]) ).
tcf(c_40101,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i2 = iPr_def_10 )
| ( i2 = i3 ) ),
inference(demodulation,[status(thm)],[c_39893,c_53]) ).
tcf(c_40102,plain,
( ( i2 = iPr_def_10 )
| ( i2 = i3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40101,c_79]) ).
tcf(c_40155,plain,
i2 = iPr_def_10,
inference(superposition,[status(thm)],[c_40102,c_33183]) ).
tcf(c_40183,plain,
( ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),i4) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i4) ) ),
inference(demodulation,[status(thm)],[c_31450,c_40155]) ).
tcf(c_40477,plain,
! [X0: $i] :
( ( i3 = iPr_def_10 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i3)),i4,select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i3,select(store(a1,iPr_def_10,iPr_def_12),i3)),i4)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),i3)),X0) ) ),
inference(light_normalisation,[status(thm)],[c_1706,c_77,c_78,c_31126,c_40155]) ).
tcf(c_40478,plain,
! [X0: $i] :
( ( i3 = iPr_def_10 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),i4,select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3,select(store(a1,iPr_def_10,iPr_def_12),i3)),i4)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3)),X0) ) ),
inference(demodulation,[status(thm)],[c_40477,c_53]) ).
tcf(c_40494,plain,
! [X0: $i] :
( ( i3 = iPr_def_10 )
| ( X0 = i4 )
| ( select(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_40478,c_54]) ).
tcf(c_40522,plain,
! [X0: $i] :
( ( i3 = iPr_def_10 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),X0) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),X0) ) ),
inference(superposition,[status(thm)],[c_40494,c_54]) ).
tcf(c_40581,plain,
! [X0: $i] :
( ( i3 = iPr_def_10 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),X0) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),X0) ) ),
inference(superposition,[status(thm)],[c_40522,c_54]) ).
tcf(c_40657,plain,
! [X0: $i] :
( ( i3 = i4 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i3)),i4,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i4)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),i3)),X0) ) ),
inference(light_normalisation,[status(thm)],[c_1707,c_77,c_78,c_31126,c_40155]) ).
tcf(c_40658,plain,
! [X0: $i] :
( ( i3 = i4 )
| ( X0 = i4 )
| ( select(store(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),i4,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i4)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3)),X0) ) ),
inference(demodulation,[status(thm)],[c_40657,c_53]) ).
tcf(c_40674,plain,
! [X0: $i] :
( ( i3 = i4 )
| ( X0 = i4 )
| ( select(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),X0) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3)),X0) ) ),
inference(superposition,[status(thm)],[c_40658,c_54]) ).
tcf(c_40704,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),iPr_def_10) = iPr_def_12 ) ),
inference(superposition,[status(thm)],[c_40581,c_53]) ).
tcf(c_40718,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_40704,c_53]) ).
tcf(c_40719,plain,
( ( i4 = iPr_def_10 )
| ( i3 = iPr_def_10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40718,c_79]) ).
tcf(c_42266,plain,
( ( i3 = i4 )
| ( select(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3)),i3) = select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3) ) ),
inference(superposition,[status(thm)],[c_40674,c_53]) ).
tcf(c_42287,plain,
( ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i3) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i3) ) ),
inference(demodulation,[status(thm)],[c_42266,c_53]) ).
tcf(c_42896,plain,
( ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),i4) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),i4) ) ),
inference(demodulation,[status(thm)],[c_40183,c_53]) ).
tcf(c_42904,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),iPr_def_10) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),iPr_def_10) ) ),
inference(superposition,[status(thm)],[c_40719,c_42896]) ).
tcf(c_42914,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i3 = iPr_def_10 )
| ( i3 = i4 ) ),
inference(demodulation,[status(thm)],[c_42904,c_53]) ).
tcf(c_42915,plain,
( ( i3 = iPr_def_10 )
| ( i3 = i4 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_42914,c_79]) ).
tcf(c_42929,plain,
i3 = iPr_def_10,
inference(superposition,[status(thm)],[c_42915,c_40719]) ).
tcf(c_42938,plain,
( ( i4 = iPr_def_10 )
| ( select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,iPr_def_11),iPr_def_10) = select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,iPr_def_12),iPr_def_10) ) ),
inference(demodulation,[status(thm)],[c_42287,c_42929]) ).
tcf(c_43092,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( i4 = iPr_def_10 ) ),
inference(demodulation,[status(thm)],[c_42938,c_53]) ).
tcf(c_43093,plain,
i4 = iPr_def_10,
inference(forward_subsumption_resolution,[status(thm)],[c_43092,c_79]) ).
tcf(c_44442,plain,
select(store(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),iPr_def_10,select(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),iPr_def_10)),iPr_def_10) = select(store(store(store(a2,iPr_def_10,iPr_def_11),iPr_def_10,select(store(a1,iPr_def_10,iPr_def_12),iPr_def_10)),iPr_def_10,select(store(store(a1,iPr_def_10,iPr_def_12),iPr_def_10,select(store(a2,iPr_def_10,iPr_def_11),iPr_def_10)),iPr_def_10)),iPr_def_10),
inference(light_normalisation,[status(thm)],[c_31443,c_40155,c_42929,c_43093]) ).
tcf(c_44443,plain,
iPr_def_11 = iPr_def_12,
inference(demodulation,[status(thm)],[c_44442,c_53]) ).
tcf(c_44444,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_44443,c_79]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV553-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Thu Sep 24 20:28:36 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.33 Running first-order theorem proving
% 0.03/0.33 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.06/0.33
% 0.06/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.33
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.34 % Proving...
% 6.91/2.58 % SZS status Started for theBenchmark.p
% 6.91/2.58 % SZS status Unsatisfiable for theBenchmark.p
% 6.91/2.58
% 6.91/2.58 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.91/2.58
% 6.91/2.58 % ------ iProver source info
% 6.91/2.58
% 6.91/2.58 % git: date: 2026-07-19 20:42:38 +0200
% 6.91/2.58 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.91/2.58 % git: non_committed_changes: false
% 6.91/2.58
% 6.91/2.58 % ------ Parsing...% successful
% 6.91/2.58
% 6.91/2.58
% 6.91/2.58 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.91/2.58
% 6.91/2.58 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.91/2.58
% 6.91/2.58 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.91/2.58
% 6.91/2.58 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 6.91/2.58 % ------ Proving...
% 6.91/2.58 % ------ Problem Properties
% 6.91/2.58
% 6.91/2.58 %
% 6.91/2.58 % clauses 7
% 6.91/2.58 % conjectures 1
% 6.91/2.58 % EPR 1
% 6.91/2.58 % Horn 6
% 6.91/2.58 % unary 6
% 6.91/2.58 % binary 1
% 6.91/2.58 % lits 8
% 6.91/2.58 % lits eq 8
% 6.91/2.58 % fd_pure 0
% 6.91/2.58 % fd_pseudo 0
% 6.91/2.58 % fd_cond 0
% 6.91/2.58 % fd_pseudo_cond 1
% 6.91/2.58 % AC symbols 0
% 6.91/2.58
% 6.91/2.58 % ------ Schedule dynamic 5 is on
% 6.91/2.58
% 6.91/2.58 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.91/2.58
% 6.91/2.58
% 6.91/2.58 % ------
% 6.91/2.58 % Current options:
% 6.91/2.58 % ------
% 6.91/2.58
% 6.91/2.58
% 6.91/2.58 %
% 6.91/2.58
% 6.91/2.58 % ------ Proving...
% 6.91/2.58 %
% 6.91/2.58
% 6.91/2.58 % SZS status Unsatisfiable for theBenchmark.p
% 6.91/2.58
% 6.91/2.58 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.91/2.58
% 6.91/2.58
%------------------------------------------------------------------------------