%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:40 PM UTC 2026
% Result : Unsatisfiable 5.81s 1.36s
% Output : Proof 5.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 99
% Number of leaves : 45
% Syntax : Number of formulae : 497 ( 497 unt; 0 def)
% Number of atoms : 497 ( 496 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 54 ( 54 usr; 52 con; 0-3 aty)
% Number of variables : 56 ( 8 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f2,axiom,
store(A,I,select(A,I)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
fof(f2_nnf,plain,
! [A,I] : store(A,I,select(A,I)) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,I] : store(A,I,select(A,I)) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t49,plain,
store(X1,X2,select(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t54,plain,
store(X1,X2,select(X1,X2)) = X1,
inference(orient,[status(thm)],[t49]) ).
cnf(f25,hypothesis,
e_40 = select(a2,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f25_nnf,plain,
e_40 = select(a2,i1),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
e_40 = select(a2,i1),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(t8,plain,
select(a2,i1) = e_40,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t160,plain,
select(a2,i1) = e_40,
inference(orient,[status(thm)],[t8]) ).
cnf(t161,plain,
a2 = store(a2,i1,e_40),
inference(cp,[status(thm)],[t54,t160]) ).
cnf(t387,plain,
store(a2,i1,e_40) = a2,
inference(orient,[status(thm)],[t161]) ).
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/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(t48,plain,
select(store(X1,X2,X3),X2) = X3,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t55,plain,
select(store(X1,X2,X3),X2) = X3,
inference(orient,[status(thm)],[t48]) ).
cnf(f5,hypothesis,
a_41 = store(a1,i1,e_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f5_nnf,plain,
a_41 = store(a1,i1,e_40),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
a_41 = store(a1,i1,e_40),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t27,plain,
store(a1,i1,e_40) = a_41,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t116,plain,
store(a1,i1,e_40) = a_41,
inference(orient,[status(thm)],[t27]) ).
cnf(t118,plain,
e_40 = select(a_41,i1),
inference(cp,[status(thm)],[t55,t116]) ).
cnf(t319,plain,
select(a_41,i1) = e_40,
inference(orient,[status(thm)],[t118]) ).
cnf(f7,hypothesis,
a_45 = store(a_41,i2,e_44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f7_nnf,plain,
a_45 = store(a_41,i2,e_44),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
a_45 = store(a_41,i2,e_44),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t29,plain,
store(a_41,i2,e_44) = a_45,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t110,plain,
store(a_41,i2,e_44) = a_45,
inference(orient,[status(thm)],[t29]) ).
cnf(f9,hypothesis,
a_49 = store(a_45,i3,e_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f9_nnf,plain,
a_49 = store(a_45,i3,e_48),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
a_49 = store(a_45,i3,e_48),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t31,plain,
store(a_45,i3,e_48) = a_49,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t68,plain,
store(a_45,i3,e_48) = a_49,
inference(orient,[status(thm)],[t31]) ).
cnf(f3,axiom,
store(store(A,I,E),I,F) = store(A,I,F),
file('/export/starexec/sandbox2/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(t51,plain,
store(store(X1,X2,X3),X2,X4) = store(X1,X2,X4),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t61,plain,
store(store(X1,X2,X3),X2,X4) = store(X1,X2,X4),
inference(orient,[status(thm)],[t51]) ).
cnf(t69,plain,
store(a_45,i3,X1) = store(a_49,i3,X1),
inference(cp,[status(thm)],[t61,t68]) ).
cnf(t420,plain,
store(a_45,i3,X1) = store(a_49,i3,X1),
inference(orient,[status(thm)],[t69]) ).
cnf(t624,plain,
store(a_49,i3,e_48) = a_49,
inference(step,[status(thm)],[t68,t420]) ).
cnf(t426,plain,
store(a_49,i3,e_48) = a_49,
inference(rw,[status(thm)],[t624]) ).
cnf(f11,hypothesis,
a_53 = store(a_49,i4,e_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f11_nnf,plain,
a_53 = store(a_49,i4,e_52),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
a_53 = store(a_49,i4,e_52),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t33,plain,
store(a_49,i4,e_52) = a_53,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t74,plain,
store(a_49,i4,e_52) = a_53,
inference(orient,[status(thm)],[t33]) ).
cnf(f13,hypothesis,
a_57 = store(a_53,i5,e_56),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f13_nnf,plain,
a_57 = store(a_53,i5,e_56),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
a_57 = store(a_53,i5,e_56),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t35,plain,
store(a_53,i5,e_56) = a_57,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t80,plain,
store(a_53,i5,e_56) = a_57,
inference(orient,[status(thm)],[t35]) ).
cnf(f15,hypothesis,
a_61 = store(a_57,i6,e_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f15_nnf,plain,
a_61 = store(a_57,i6,e_60),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
a_61 = store(a_57,i6,e_60),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t37,plain,
store(a_57,i6,e_60) = a_61,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t86,plain,
store(a_57,i6,e_60) = a_61,
inference(orient,[status(thm)],[t37]) ).
cnf(f17,hypothesis,
a_65 = store(a_61,i7,e_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f17_nnf,plain,
a_65 = store(a_61,i7,e_64),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
a_65 = store(a_61,i7,e_64),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(t39,plain,
store(a_61,i7,e_64) = a_65,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t92,plain,
store(a_61,i7,e_64) = a_65,
inference(orient,[status(thm)],[t39]) ).
cnf(f19,hypothesis,
a_69 = store(a_65,i8,e_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f19_nnf,plain,
a_69 = store(a_65,i8,e_68),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
a_69 = store(a_65,i8,e_68),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(t41,plain,
store(a_65,i8,e_68) = a_69,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t98,plain,
store(a_65,i8,e_68) = a_69,
inference(orient,[status(thm)],[t41]) ).
cnf(f21,hypothesis,
a_73 = store(a_69,i9,e_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f21_nnf,plain,
a_73 = store(a_69,i9,e_72),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
a_73 = store(a_69,i9,e_72),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t43,plain,
store(a_69,i9,e_72) = a_73,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t104,plain,
store(a_69,i9,e_72) = a_73,
inference(orient,[status(thm)],[t43]) ).
cnf(f23,hypothesis,
a_77 = store(a_73,i10,e_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f23_nnf,plain,
a_77 = store(a_73,i10,e_76),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
a_77 = store(a_73,i10,e_76),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(t45,plain,
store(a_73,i10,e_76) = a_77,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t62,plain,
store(a_73,i10,e_76) = a_77,
inference(orient,[status(thm)],[t45]) ).
cnf(f45,hypothesis,
a_77 = a_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f45_nnf,plain,
a_77 = a_79,
inference(nnf_transformation,[status(thm)],[f45]) ).
cnf(c45,plain,
a_77 = a_79,
inference(cnf_transformation,[status(esa)],[f45_nnf]) ).
cnf(t0,plain,
a_79 = a_77,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t259,plain,
a_77 = a_79,
inference(orient,[status(thm)],[t0]) ).
cnf(t580,plain,
store(a_73,i10,e_76) = a_79,
inference(step,[status(thm)],[t62,t259]) ).
cnf(t260,plain,
store(a_73,i10,e_76) = a_79,
inference(orient,[status(thm)],[t580]) ).
cnf(f24,hypothesis,
a_79 = store(a_75,i10,e_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f24_nnf,plain,
a_79 = store(a_75,i10,e_78),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
a_79 = store(a_75,i10,e_78),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t46,plain,
store(a_75,i10,e_78) = a_79,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t65,plain,
store(a_75,i10,e_78) = a_79,
inference(orient,[status(thm)],[t46]) ).
cnf(t67,plain,
e_78 = select(a_79,i10),
inference(cp,[status(thm)],[t55,t65]) ).
cnf(t64,plain,
e_76 = select(a_77,i10),
inference(cp,[status(thm)],[t55,t62]) ).
cnf(t582,plain,
e_76 = select(a_79,i10),
inference(step,[status(thm)],[t64,t259]) ).
cnf(t262,plain,
select(a_79,i10) = e_76,
inference(orient,[status(thm)],[t582]) ).
cnf(t583,plain,
e_78 = e_76,
inference(step,[status(thm)],[t67,t262]) ).
cnf(t265,plain,
e_76 = e_78,
inference(orient,[status(thm)],[t583]) ).
cnf(t588,plain,
store(a_73,i10,e_78) = a_79,
inference(step,[status(thm)],[t260,t265]) ).
cnf(t270,plain,
store(a_73,i10,e_78) = a_79,
inference(rw,[status(thm)],[t588]) ).
cnf(f44,hypothesis,
e_78 = select(a_73,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f44_nnf,plain,
e_78 = select(a_73,i10),
inference(nnf_transformation,[status(thm)],[f44]) ).
cnf(c44,plain,
e_78 = select(a_73,i10),
inference(cnf_transformation,[status(esa)],[f44_nnf]) ).
cnf(t25,plain,
select(a_73,i10) = e_78,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(t122,plain,
select(a_73,i10) = e_78,
inference(orient,[status(thm)],[t25]) ).
cnf(t123,plain,
a_73 = store(a_73,i10,e_78),
inference(cp,[status(thm)],[t54,t122]) ).
cnf(t325,plain,
store(a_73,i10,e_78) = a_73,
inference(orient,[status(thm)],[t123]) ).
cnf(t596,plain,
a_73 = a_79,
inference(step,[status(thm)],[t270,t325]) ).
cnf(t393,plain,
a_73 = a_79,
inference(orient,[status(thm)],[t596]) ).
cnf(t597,plain,
store(a_69,i9,e_72) = a_79,
inference(step,[status(thm)],[t104,t393]) ).
cnf(t394,plain,
store(a_69,i9,e_72) = a_79,
inference(orient,[status(thm)],[t597]) ).
cnf(t106,plain,
e_72 = select(a_73,i9),
inference(cp,[status(thm)],[t55,t104]) ).
cnf(t307,plain,
select(a_73,i9) = e_72,
inference(orient,[status(thm)],[t106]) ).
cnf(t599,plain,
select(a_79,i9) = e_72,
inference(step,[status(thm)],[t307,t393]) ).
cnf(f22,hypothesis,
a_75 = store(a_71,i9,e_74),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f22_nnf,plain,
a_75 = store(a_71,i9,e_74),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
a_75 = store(a_71,i9,e_74),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(t44,plain,
store(a_71,i9,e_74) = a_75,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t107,plain,
store(a_71,i9,e_74) = a_75,
inference(orient,[status(thm)],[t44]) ).
cnf(t109,plain,
e_74 = select(a_75,i9),
inference(cp,[status(thm)],[t55,t107]) ).
cnf(t310,plain,
select(a_75,i9) = e_74,
inference(orient,[status(thm)],[t109]) ).
cnf(f43,hypothesis,
e_76 = select(a_75,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f43_nnf,plain,
e_76 = select(a_75,i10),
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c43,plain,
e_76 = select(a_75,i10),
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(t26,plain,
select(a_75,i10) = e_76,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t124,plain,
select(a_75,i10) = e_76,
inference(orient,[status(thm)],[t26]) ).
cnf(t125,plain,
a_75 = store(a_75,i10,e_76),
inference(cp,[status(thm)],[t54,t124]) ).
cnf(t589,plain,
a_75 = store(a_75,i10,e_78),
inference(step,[status(thm)],[t125,t265]) ).
cnf(t590,plain,
a_75 = a_79,
inference(step,[status(thm)],[t589,t65]) ).
cnf(t328,plain,
a_75 = a_79,
inference(orient,[status(thm)],[t590]) ).
cnf(t593,plain,
select(a_79,i9) = e_74,
inference(step,[status(thm)],[t310,t328]) ).
cnf(t331,plain,
select(a_79,i9) = e_74,
inference(rw,[status(thm)],[t593]) ).
cnf(t333,plain,
select(a_79,i9) = e_74,
inference(orient,[status(thm)],[t331]) ).
cnf(t600,plain,
e_74 = e_72,
inference(step,[status(thm)],[t599,t333]) ).
cnf(t396,plain,
e_74 = e_72,
inference(rw,[status(thm)],[t600]) ).
cnf(t397,plain,
e_72 = e_74,
inference(orient,[status(thm)],[t396]) ).
cnf(t605,plain,
store(a_69,i9,e_74) = a_79,
inference(step,[status(thm)],[t394,t397]) ).
cnf(f42,hypothesis,
e_74 = select(a_69,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f42_nnf,plain,
e_74 = select(a_69,i9),
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c42,plain,
e_74 = select(a_69,i9),
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(t23,plain,
select(a_69,i9) = e_74,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(t150,plain,
select(a_69,i9) = e_74,
inference(orient,[status(thm)],[t23]) ).
cnf(t151,plain,
a_69 = store(a_69,i9,e_74),
inference(cp,[status(thm)],[t54,t150]) ).
cnf(t372,plain,
store(a_69,i9,e_74) = a_69,
inference(orient,[status(thm)],[t151]) ).
cnf(t606,plain,
a_69 = a_79,
inference(step,[status(thm)],[t605,t372]) ).
cnf(t401,plain,
a_69 = a_79,
inference(rw,[status(thm)],[t606]) ).
cnf(t407,plain,
a_69 = a_79,
inference(orient,[status(thm)],[t401]) ).
cnf(t611,plain,
store(a_65,i8,e_68) = a_79,
inference(step,[status(thm)],[t98,t407]) ).
cnf(t408,plain,
store(a_65,i8,e_68) = a_79,
inference(orient,[status(thm)],[t611]) ).
cnf(t100,plain,
e_68 = select(a_69,i8),
inference(cp,[status(thm)],[t55,t98]) ).
cnf(t301,plain,
select(a_69,i8) = e_68,
inference(orient,[status(thm)],[t100]) ).
cnf(t615,plain,
select(a_79,i8) = e_68,
inference(step,[status(thm)],[t301,t407]) ).
cnf(t411,plain,
select(a_79,i8) = e_68,
inference(rw,[status(thm)],[t615]) ).
cnf(f20,hypothesis,
a_71 = store(a_67,i8,e_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f20_nnf,plain,
a_71 = store(a_67,i8,e_70),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
a_71 = store(a_67,i8,e_70),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(t42,plain,
store(a_67,i8,e_70) = a_71,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t101,plain,
store(a_67,i8,e_70) = a_71,
inference(orient,[status(thm)],[t42]) ).
cnf(t103,plain,
e_70 = select(a_71,i8),
inference(cp,[status(thm)],[t55,t101]) ).
cnf(t304,plain,
select(a_71,i8) = e_70,
inference(orient,[status(thm)],[t103]) ).
cnf(f41,hypothesis,
e_72 = select(a_71,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f41_nnf,plain,
e_72 = select(a_71,i9),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
e_72 = select(a_71,i9),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(t24,plain,
select(a_71,i9) = e_72,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t152,plain,
select(a_71,i9) = e_72,
inference(orient,[status(thm)],[t24]) ).
cnf(t153,plain,
a_71 = store(a_71,i9,e_72),
inference(cp,[status(thm)],[t54,t152]) ).
cnf(t375,plain,
store(a_71,i9,e_72) = a_71,
inference(orient,[status(thm)],[t153]) ).
cnf(t603,plain,
store(a_71,i9,e_74) = a_71,
inference(step,[status(thm)],[t375,t397]) ).
cnf(t591,plain,
store(a_71,i9,e_74) = a_79,
inference(step,[status(thm)],[t107,t328]) ).
cnf(t329,plain,
store(a_71,i9,e_74) = a_79,
inference(orient,[status(thm)],[t591]) ).
cnf(t604,plain,
a_79 = a_71,
inference(step,[status(thm)],[t603,t329]) ).
cnf(t400,plain,
a_79 = a_71,
inference(rw,[status(thm)],[t604]) ).
cnf(t402,plain,
a_71 = a_79,
inference(orient,[status(thm)],[t400]) ).
cnf(t609,plain,
select(a_79,i8) = e_70,
inference(step,[status(thm)],[t304,t402]) ).
cnf(t405,plain,
select(a_79,i8) = e_70,
inference(rw,[status(thm)],[t609]) ).
cnf(t412,plain,
select(a_79,i8) = e_70,
inference(orient,[status(thm)],[t405]) ).
cnf(t616,plain,
e_70 = e_68,
inference(step,[status(thm)],[t411,t412]) ).
cnf(t415,plain,
e_68 = e_70,
inference(orient,[status(thm)],[t616]) ).
cnf(t621,plain,
store(a_65,i8,e_70) = a_79,
inference(step,[status(thm)],[t408,t415]) ).
cnf(f40,hypothesis,
e_70 = select(a_65,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f40_nnf,plain,
e_70 = select(a_65,i8),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
e_70 = select(a_65,i8),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(t21,plain,
select(a_65,i8) = e_70,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t146,plain,
select(a_65,i8) = e_70,
inference(orient,[status(thm)],[t21]) ).
cnf(t147,plain,
a_65 = store(a_65,i8,e_70),
inference(cp,[status(thm)],[t54,t146]) ).
cnf(t366,plain,
store(a_65,i8,e_70) = a_65,
inference(orient,[status(thm)],[t147]) ).
cnf(t622,plain,
a_65 = a_79,
inference(step,[status(thm)],[t621,t366]) ).
cnf(t419,plain,
a_65 = a_79,
inference(rw,[status(thm)],[t622]) ).
cnf(t432,plain,
a_65 = a_79,
inference(orient,[status(thm)],[t419]) ).
cnf(t629,plain,
store(a_61,i7,e_64) = a_79,
inference(step,[status(thm)],[t92,t432]) ).
cnf(t433,plain,
store(a_61,i7,e_64) = a_79,
inference(orient,[status(thm)],[t629]) ).
cnf(t94,plain,
e_64 = select(a_65,i7),
inference(cp,[status(thm)],[t55,t92]) ).
cnf(t295,plain,
select(a_65,i7) = e_64,
inference(orient,[status(thm)],[t94]) ).
cnf(t633,plain,
select(a_79,i7) = e_64,
inference(step,[status(thm)],[t295,t432]) ).
cnf(t436,plain,
select(a_79,i7) = e_64,
inference(rw,[status(thm)],[t633]) ).
cnf(f18,hypothesis,
a_67 = store(a_63,i7,e_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f18_nnf,plain,
a_67 = store(a_63,i7,e_66),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
a_67 = store(a_63,i7,e_66),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(t40,plain,
store(a_63,i7,e_66) = a_67,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t95,plain,
store(a_63,i7,e_66) = a_67,
inference(orient,[status(thm)],[t40]) ).
cnf(t97,plain,
e_66 = select(a_67,i7),
inference(cp,[status(thm)],[t55,t95]) ).
cnf(t298,plain,
select(a_67,i7) = e_66,
inference(orient,[status(thm)],[t97]) ).
cnf(f39,hypothesis,
e_68 = select(a_67,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f39_nnf,plain,
e_68 = select(a_67,i8),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c39,plain,
e_68 = select(a_67,i8),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(t22,plain,
select(a_67,i8) = e_68,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t148,plain,
select(a_67,i8) = e_68,
inference(orient,[status(thm)],[t22]) ).
cnf(t149,plain,
a_67 = store(a_67,i8,e_68),
inference(cp,[status(thm)],[t54,t148]) ).
cnf(t369,plain,
store(a_67,i8,e_68) = a_67,
inference(orient,[status(thm)],[t149]) ).
cnf(t619,plain,
store(a_67,i8,e_70) = a_67,
inference(step,[status(thm)],[t369,t415]) ).
cnf(t607,plain,
store(a_67,i8,e_70) = a_79,
inference(step,[status(thm)],[t101,t402]) ).
cnf(t403,plain,
store(a_67,i8,e_70) = a_79,
inference(orient,[status(thm)],[t607]) ).
cnf(t620,plain,
a_79 = a_67,
inference(step,[status(thm)],[t619,t403]) ).
cnf(t418,plain,
a_79 = a_67,
inference(rw,[status(thm)],[t620]) ).
cnf(t427,plain,
a_67 = a_79,
inference(orient,[status(thm)],[t418]) ).
cnf(t627,plain,
select(a_79,i7) = e_66,
inference(step,[status(thm)],[t298,t427]) ).
cnf(t430,plain,
select(a_79,i7) = e_66,
inference(rw,[status(thm)],[t627]) ).
cnf(t437,plain,
select(a_79,i7) = e_66,
inference(orient,[status(thm)],[t430]) ).
cnf(t634,plain,
e_66 = e_64,
inference(step,[status(thm)],[t436,t437]) ).
cnf(t440,plain,
e_64 = e_66,
inference(orient,[status(thm)],[t634]) ).
cnf(t639,plain,
store(a_61,i7,e_66) = a_79,
inference(step,[status(thm)],[t433,t440]) ).
cnf(f38,hypothesis,
e_66 = select(a_61,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f38_nnf,plain,
e_66 = select(a_61,i7),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
e_66 = select(a_61,i7),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
cnf(t19,plain,
select(a_61,i7) = e_66,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t142,plain,
select(a_61,i7) = e_66,
inference(orient,[status(thm)],[t19]) ).
cnf(t143,plain,
a_61 = store(a_61,i7,e_66),
inference(cp,[status(thm)],[t54,t142]) ).
cnf(t360,plain,
store(a_61,i7,e_66) = a_61,
inference(orient,[status(thm)],[t143]) ).
cnf(t640,plain,
a_61 = a_79,
inference(step,[status(thm)],[t639,t360]) ).
cnf(t444,plain,
a_61 = a_79,
inference(rw,[status(thm)],[t640]) ).
cnf(t450,plain,
a_61 = a_79,
inference(orient,[status(thm)],[t444]) ).
cnf(t645,plain,
store(a_57,i6,e_60) = a_79,
inference(step,[status(thm)],[t86,t450]) ).
cnf(t451,plain,
store(a_57,i6,e_60) = a_79,
inference(orient,[status(thm)],[t645]) ).
cnf(t88,plain,
e_60 = select(a_61,i6),
inference(cp,[status(thm)],[t55,t86]) ).
cnf(t289,plain,
select(a_61,i6) = e_60,
inference(orient,[status(thm)],[t88]) ).
cnf(t649,plain,
select(a_79,i6) = e_60,
inference(step,[status(thm)],[t289,t450]) ).
cnf(t454,plain,
select(a_79,i6) = e_60,
inference(rw,[status(thm)],[t649]) ).
cnf(f16,hypothesis,
a_63 = store(a_59,i6,e_62),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f16_nnf,plain,
a_63 = store(a_59,i6,e_62),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
a_63 = store(a_59,i6,e_62),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t38,plain,
store(a_59,i6,e_62) = a_63,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t89,plain,
store(a_59,i6,e_62) = a_63,
inference(orient,[status(thm)],[t38]) ).
cnf(t91,plain,
e_62 = select(a_63,i6),
inference(cp,[status(thm)],[t55,t89]) ).
cnf(t292,plain,
select(a_63,i6) = e_62,
inference(orient,[status(thm)],[t91]) ).
cnf(f37,hypothesis,
e_64 = select(a_63,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f37_nnf,plain,
e_64 = select(a_63,i7),
inference(nnf_transformation,[status(thm)],[f37]) ).
cnf(c37,plain,
e_64 = select(a_63,i7),
inference(cnf_transformation,[status(esa)],[f37_nnf]) ).
cnf(t20,plain,
select(a_63,i7) = e_64,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t144,plain,
select(a_63,i7) = e_64,
inference(orient,[status(thm)],[t20]) ).
cnf(t145,plain,
a_63 = store(a_63,i7,e_64),
inference(cp,[status(thm)],[t54,t144]) ).
cnf(t363,plain,
store(a_63,i7,e_64) = a_63,
inference(orient,[status(thm)],[t145]) ).
cnf(t637,plain,
store(a_63,i7,e_66) = a_63,
inference(step,[status(thm)],[t363,t440]) ).
cnf(t625,plain,
store(a_63,i7,e_66) = a_79,
inference(step,[status(thm)],[t95,t427]) ).
cnf(t428,plain,
store(a_63,i7,e_66) = a_79,
inference(orient,[status(thm)],[t625]) ).
cnf(t638,plain,
a_79 = a_63,
inference(step,[status(thm)],[t637,t428]) ).
cnf(t443,plain,
a_79 = a_63,
inference(rw,[status(thm)],[t638]) ).
cnf(t445,plain,
a_63 = a_79,
inference(orient,[status(thm)],[t443]) ).
cnf(t643,plain,
select(a_79,i6) = e_62,
inference(step,[status(thm)],[t292,t445]) ).
cnf(t448,plain,
select(a_79,i6) = e_62,
inference(rw,[status(thm)],[t643]) ).
cnf(t455,plain,
select(a_79,i6) = e_62,
inference(orient,[status(thm)],[t448]) ).
cnf(t650,plain,
e_62 = e_60,
inference(step,[status(thm)],[t454,t455]) ).
cnf(t458,plain,
e_60 = e_62,
inference(orient,[status(thm)],[t650]) ).
cnf(t655,plain,
store(a_57,i6,e_62) = a_79,
inference(step,[status(thm)],[t451,t458]) ).
cnf(f36,hypothesis,
e_62 = select(a_57,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f36_nnf,plain,
e_62 = select(a_57,i6),
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c36,plain,
e_62 = select(a_57,i6),
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(t17,plain,
select(a_57,i6) = e_62,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t138,plain,
select(a_57,i6) = e_62,
inference(orient,[status(thm)],[t17]) ).
cnf(t139,plain,
a_57 = store(a_57,i6,e_62),
inference(cp,[status(thm)],[t54,t138]) ).
cnf(t354,plain,
store(a_57,i6,e_62) = a_57,
inference(orient,[status(thm)],[t139]) ).
cnf(t656,plain,
a_57 = a_79,
inference(step,[status(thm)],[t655,t354]) ).
cnf(t462,plain,
a_57 = a_79,
inference(rw,[status(thm)],[t656]) ).
cnf(t468,plain,
a_57 = a_79,
inference(orient,[status(thm)],[t462]) ).
cnf(t661,plain,
store(a_53,i5,e_56) = a_79,
inference(step,[status(thm)],[t80,t468]) ).
cnf(t469,plain,
store(a_53,i5,e_56) = a_79,
inference(orient,[status(thm)],[t661]) ).
cnf(t82,plain,
e_56 = select(a_57,i5),
inference(cp,[status(thm)],[t55,t80]) ).
cnf(t283,plain,
select(a_57,i5) = e_56,
inference(orient,[status(thm)],[t82]) ).
cnf(t665,plain,
select(a_79,i5) = e_56,
inference(step,[status(thm)],[t283,t468]) ).
cnf(t472,plain,
select(a_79,i5) = e_56,
inference(rw,[status(thm)],[t665]) ).
cnf(f14,hypothesis,
a_59 = store(a_55,i5,e_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f14_nnf,plain,
a_59 = store(a_55,i5,e_58),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
a_59 = store(a_55,i5,e_58),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t36,plain,
store(a_55,i5,e_58) = a_59,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t83,plain,
store(a_55,i5,e_58) = a_59,
inference(orient,[status(thm)],[t36]) ).
cnf(t85,plain,
e_58 = select(a_59,i5),
inference(cp,[status(thm)],[t55,t83]) ).
cnf(t286,plain,
select(a_59,i5) = e_58,
inference(orient,[status(thm)],[t85]) ).
cnf(f35,hypothesis,
e_60 = select(a_59,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f35_nnf,plain,
e_60 = select(a_59,i6),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
e_60 = select(a_59,i6),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(t18,plain,
select(a_59,i6) = e_60,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t140,plain,
select(a_59,i6) = e_60,
inference(orient,[status(thm)],[t18]) ).
cnf(t141,plain,
a_59 = store(a_59,i6,e_60),
inference(cp,[status(thm)],[t54,t140]) ).
cnf(t357,plain,
store(a_59,i6,e_60) = a_59,
inference(orient,[status(thm)],[t141]) ).
cnf(t653,plain,
store(a_59,i6,e_62) = a_59,
inference(step,[status(thm)],[t357,t458]) ).
cnf(t641,plain,
store(a_59,i6,e_62) = a_79,
inference(step,[status(thm)],[t89,t445]) ).
cnf(t446,plain,
store(a_59,i6,e_62) = a_79,
inference(orient,[status(thm)],[t641]) ).
cnf(t654,plain,
a_79 = a_59,
inference(step,[status(thm)],[t653,t446]) ).
cnf(t461,plain,
a_79 = a_59,
inference(rw,[status(thm)],[t654]) ).
cnf(t463,plain,
a_59 = a_79,
inference(orient,[status(thm)],[t461]) ).
cnf(t659,plain,
select(a_79,i5) = e_58,
inference(step,[status(thm)],[t286,t463]) ).
cnf(t466,plain,
select(a_79,i5) = e_58,
inference(rw,[status(thm)],[t659]) ).
cnf(t473,plain,
select(a_79,i5) = e_58,
inference(orient,[status(thm)],[t466]) ).
cnf(t666,plain,
e_58 = e_56,
inference(step,[status(thm)],[t472,t473]) ).
cnf(t476,plain,
e_56 = e_58,
inference(orient,[status(thm)],[t666]) ).
cnf(t671,plain,
store(a_53,i5,e_58) = a_79,
inference(step,[status(thm)],[t469,t476]) ).
cnf(f34,hypothesis,
e_58 = select(a_53,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f34_nnf,plain,
e_58 = select(a_53,i5),
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
e_58 = select(a_53,i5),
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(t15,plain,
select(a_53,i5) = e_58,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t134,plain,
select(a_53,i5) = e_58,
inference(orient,[status(thm)],[t15]) ).
cnf(t135,plain,
a_53 = store(a_53,i5,e_58),
inference(cp,[status(thm)],[t54,t134]) ).
cnf(t348,plain,
store(a_53,i5,e_58) = a_53,
inference(orient,[status(thm)],[t135]) ).
cnf(t672,plain,
a_53 = a_79,
inference(step,[status(thm)],[t671,t348]) ).
cnf(t480,plain,
a_53 = a_79,
inference(rw,[status(thm)],[t672]) ).
cnf(t486,plain,
a_53 = a_79,
inference(orient,[status(thm)],[t480]) ).
cnf(t677,plain,
store(a_49,i4,e_52) = a_79,
inference(step,[status(thm)],[t74,t486]) ).
cnf(t487,plain,
store(a_49,i4,e_52) = a_79,
inference(orient,[status(thm)],[t677]) ).
cnf(t76,plain,
e_52 = select(a_53,i4),
inference(cp,[status(thm)],[t55,t74]) ).
cnf(t277,plain,
select(a_53,i4) = e_52,
inference(orient,[status(thm)],[t76]) ).
cnf(t681,plain,
select(a_79,i4) = e_52,
inference(step,[status(thm)],[t277,t486]) ).
cnf(t490,plain,
select(a_79,i4) = e_52,
inference(rw,[status(thm)],[t681]) ).
cnf(f12,hypothesis,
a_55 = store(a_51,i4,e_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f12_nnf,plain,
a_55 = store(a_51,i4,e_54),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
a_55 = store(a_51,i4,e_54),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t34,plain,
store(a_51,i4,e_54) = a_55,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t77,plain,
store(a_51,i4,e_54) = a_55,
inference(orient,[status(thm)],[t34]) ).
cnf(t79,plain,
e_54 = select(a_55,i4),
inference(cp,[status(thm)],[t55,t77]) ).
cnf(t280,plain,
select(a_55,i4) = e_54,
inference(orient,[status(thm)],[t79]) ).
cnf(f33,hypothesis,
e_56 = select(a_55,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f33_nnf,plain,
e_56 = select(a_55,i5),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
e_56 = select(a_55,i5),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(t16,plain,
select(a_55,i5) = e_56,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t136,plain,
select(a_55,i5) = e_56,
inference(orient,[status(thm)],[t16]) ).
cnf(t137,plain,
a_55 = store(a_55,i5,e_56),
inference(cp,[status(thm)],[t54,t136]) ).
cnf(t351,plain,
store(a_55,i5,e_56) = a_55,
inference(orient,[status(thm)],[t137]) ).
cnf(t669,plain,
store(a_55,i5,e_58) = a_55,
inference(step,[status(thm)],[t351,t476]) ).
cnf(t657,plain,
store(a_55,i5,e_58) = a_79,
inference(step,[status(thm)],[t83,t463]) ).
cnf(t464,plain,
store(a_55,i5,e_58) = a_79,
inference(orient,[status(thm)],[t657]) ).
cnf(t670,plain,
a_79 = a_55,
inference(step,[status(thm)],[t669,t464]) ).
cnf(t479,plain,
a_79 = a_55,
inference(rw,[status(thm)],[t670]) ).
cnf(t481,plain,
a_55 = a_79,
inference(orient,[status(thm)],[t479]) ).
cnf(t675,plain,
select(a_79,i4) = e_54,
inference(step,[status(thm)],[t280,t481]) ).
cnf(t484,plain,
select(a_79,i4) = e_54,
inference(rw,[status(thm)],[t675]) ).
cnf(t491,plain,
select(a_79,i4) = e_54,
inference(orient,[status(thm)],[t484]) ).
cnf(t682,plain,
e_54 = e_52,
inference(step,[status(thm)],[t490,t491]) ).
cnf(t494,plain,
e_52 = e_54,
inference(orient,[status(thm)],[t682]) ).
cnf(t687,plain,
store(a_49,i4,e_54) = a_79,
inference(step,[status(thm)],[t487,t494]) ).
cnf(f32,hypothesis,
e_54 = select(a_49,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f32_nnf,plain,
e_54 = select(a_49,i4),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
e_54 = select(a_49,i4),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t13,plain,
select(a_49,i4) = e_54,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t130,plain,
select(a_49,i4) = e_54,
inference(orient,[status(thm)],[t13]) ).
cnf(t131,plain,
a_49 = store(a_49,i4,e_54),
inference(cp,[status(thm)],[t54,t130]) ).
cnf(t342,plain,
store(a_49,i4,e_54) = a_49,
inference(orient,[status(thm)],[t131]) ).
cnf(t688,plain,
a_49 = a_79,
inference(step,[status(thm)],[t687,t342]) ).
cnf(t498,plain,
a_49 = a_79,
inference(rw,[status(thm)],[t688]) ).
cnf(t504,plain,
a_49 = a_79,
inference(orient,[status(thm)],[t498]) ).
cnf(t709,plain,
store(a_79,i3,e_48) = a_49,
inference(step,[status(thm)],[t426,t504]) ).
cnf(t70,plain,
e_48 = select(a_49,i3),
inference(cp,[status(thm)],[t55,t68]) ).
cnf(t271,plain,
select(a_49,i3) = e_48,
inference(orient,[status(thm)],[t70]) ).
cnf(t697,plain,
select(a_79,i3) = e_48,
inference(step,[status(thm)],[t271,t504]) ).
cnf(t508,plain,
select(a_79,i3) = e_48,
inference(rw,[status(thm)],[t697]) ).
cnf(f10,hypothesis,
a_51 = store(a_47,i3,e_50),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f10_nnf,plain,
a_51 = store(a_47,i3,e_50),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
a_51 = store(a_47,i3,e_50),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t32,plain,
store(a_47,i3,e_50) = a_51,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t71,plain,
store(a_47,i3,e_50) = a_51,
inference(orient,[status(thm)],[t32]) ).
cnf(t73,plain,
e_50 = select(a_51,i3),
inference(cp,[status(thm)],[t55,t71]) ).
cnf(t274,plain,
select(a_51,i3) = e_50,
inference(orient,[status(thm)],[t73]) ).
cnf(f31,hypothesis,
e_52 = select(a_51,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f31_nnf,plain,
e_52 = select(a_51,i4),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
e_52 = select(a_51,i4),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t14,plain,
select(a_51,i4) = e_52,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t132,plain,
select(a_51,i4) = e_52,
inference(orient,[status(thm)],[t14]) ).
cnf(t133,plain,
a_51 = store(a_51,i4,e_52),
inference(cp,[status(thm)],[t54,t132]) ).
cnf(t345,plain,
store(a_51,i4,e_52) = a_51,
inference(orient,[status(thm)],[t133]) ).
cnf(t685,plain,
store(a_51,i4,e_54) = a_51,
inference(step,[status(thm)],[t345,t494]) ).
cnf(t673,plain,
store(a_51,i4,e_54) = a_79,
inference(step,[status(thm)],[t77,t481]) ).
cnf(t482,plain,
store(a_51,i4,e_54) = a_79,
inference(orient,[status(thm)],[t673]) ).
cnf(t686,plain,
a_79 = a_51,
inference(step,[status(thm)],[t685,t482]) ).
cnf(t497,plain,
a_79 = a_51,
inference(rw,[status(thm)],[t686]) ).
cnf(t499,plain,
a_51 = a_79,
inference(orient,[status(thm)],[t497]) ).
cnf(t691,plain,
select(a_79,i3) = e_50,
inference(step,[status(thm)],[t274,t499]) ).
cnf(t502,plain,
select(a_79,i3) = e_50,
inference(rw,[status(thm)],[t691]) ).
cnf(t509,plain,
select(a_79,i3) = e_50,
inference(orient,[status(thm)],[t502]) ).
cnf(t698,plain,
e_50 = e_48,
inference(step,[status(thm)],[t508,t509]) ).
cnf(t512,plain,
e_48 = e_50,
inference(orient,[status(thm)],[t698]) ).
cnf(t710,plain,
store(a_79,i3,e_50) = a_49,
inference(step,[status(thm)],[t709,t512]) ).
cnf(t421,plain,
store(a_49,i3,select(a_45,i3)) = a_45,
inference(cp,[status(thm)],[t420,t54]) ).
cnf(t707,plain,
store(a_79,i3,select(a_45,i3)) = a_45,
inference(step,[status(thm)],[t421,t504]) ).
cnf(f30,hypothesis,
e_50 = select(a_45,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f30_nnf,plain,
e_50 = select(a_45,i3),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
e_50 = select(a_45,i3),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(t11,plain,
select(a_45,i3) = e_50,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t126,plain,
select(a_45,i3) = e_50,
inference(orient,[status(thm)],[t11]) ).
cnf(t708,plain,
store(a_79,i3,e_50) = a_45,
inference(step,[status(thm)],[t707,t126]) ).
cnf(t539,plain,
store(a_79,i3,e_50) = a_45,
inference(orient,[status(thm)],[t708]) ).
cnf(t711,plain,
a_45 = a_49,
inference(step,[status(thm)],[t710,t539]) ).
cnf(t712,plain,
a_45 = a_79,
inference(step,[status(thm)],[t711,t504]) ).
cnf(t543,plain,
a_45 = a_79,
inference(orient,[status(thm)],[t712]) ).
cnf(t713,plain,
store(a_41,i2,e_44) = a_79,
inference(step,[status(thm)],[t110,t543]) ).
cnf(t544,plain,
store(a_41,i2,e_44) = a_79,
inference(orient,[status(thm)],[t713]) ).
cnf(t112,plain,
e_44 = select(a_45,i2),
inference(cp,[status(thm)],[t55,t110]) ).
cnf(t313,plain,
select(a_45,i2) = e_44,
inference(orient,[status(thm)],[t112]) ).
cnf(t719,plain,
select(a_79,i2) = e_44,
inference(step,[status(thm)],[t313,t543]) ).
cnf(f8,hypothesis,
a_47 = store(a_43,i2,e_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f8_nnf,plain,
a_47 = store(a_43,i2,e_46),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
a_47 = store(a_43,i2,e_46),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t30,plain,
store(a_43,i2,e_46) = a_47,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t113,plain,
store(a_43,i2,e_46) = a_47,
inference(orient,[status(thm)],[t30]) ).
cnf(t115,plain,
e_46 = select(a_47,i2),
inference(cp,[status(thm)],[t55,t113]) ).
cnf(t316,plain,
select(a_47,i2) = e_46,
inference(orient,[status(thm)],[t115]) ).
cnf(f29,hypothesis,
e_48 = select(a_47,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f29_nnf,plain,
e_48 = select(a_47,i3),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
e_48 = select(a_47,i3),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(t12,plain,
select(a_47,i3) = e_48,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t128,plain,
select(a_47,i3) = e_48,
inference(orient,[status(thm)],[t12]) ).
cnf(t129,plain,
a_47 = store(a_47,i3,e_48),
inference(cp,[status(thm)],[t54,t128]) ).
cnf(t339,plain,
store(a_47,i3,e_48) = a_47,
inference(orient,[status(thm)],[t129]) ).
cnf(t701,plain,
store(a_47,i3,e_50) = a_47,
inference(step,[status(thm)],[t339,t512]) ).
cnf(t689,plain,
store(a_47,i3,e_50) = a_79,
inference(step,[status(thm)],[t71,t499]) ).
cnf(t500,plain,
store(a_47,i3,e_50) = a_79,
inference(orient,[status(thm)],[t689]) ).
cnf(t702,plain,
a_79 = a_47,
inference(step,[status(thm)],[t701,t500]) ).
cnf(t515,plain,
a_79 = a_47,
inference(rw,[status(thm)],[t702]) ).
cnf(t516,plain,
a_47 = a_79,
inference(orient,[status(thm)],[t515]) ).
cnf(t705,plain,
select(a_79,i2) = e_46,
inference(step,[status(thm)],[t316,t516]) ).
cnf(t519,plain,
select(a_79,i2) = e_46,
inference(rw,[status(thm)],[t705]) ).
cnf(t521,plain,
select(a_79,i2) = e_46,
inference(orient,[status(thm)],[t519]) ).
cnf(t720,plain,
e_46 = e_44,
inference(step,[status(thm)],[t719,t521]) ).
cnf(t549,plain,
e_46 = e_44,
inference(rw,[status(thm)],[t720]) ).
cnf(t550,plain,
e_44 = e_46,
inference(orient,[status(thm)],[t549]) ).
cnf(t725,plain,
store(a_41,i2,e_46) = a_79,
inference(step,[status(thm)],[t544,t550]) ).
cnf(f28,hypothesis,
e_46 = select(a_41,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f28_nnf,plain,
e_46 = select(a_41,i2),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
e_46 = select(a_41,i2),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(t9,plain,
select(a_41,i2) = e_46,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t154,plain,
select(a_41,i2) = e_46,
inference(orient,[status(thm)],[t9]) ).
cnf(t155,plain,
a_41 = store(a_41,i2,e_46),
inference(cp,[status(thm)],[t54,t154]) ).
cnf(t378,plain,
store(a_41,i2,e_46) = a_41,
inference(orient,[status(thm)],[t155]) ).
cnf(t726,plain,
a_41 = a_79,
inference(step,[status(thm)],[t725,t378]) ).
cnf(t554,plain,
a_41 = a_79,
inference(rw,[status(thm)],[t726]) ).
cnf(t561,plain,
a_41 = a_79,
inference(orient,[status(thm)],[t554]) ).
cnf(t739,plain,
select(a_79,i1) = e_40,
inference(step,[status(thm)],[t319,t561]) ).
cnf(t566,plain,
select(a_79,i1) = e_40,
inference(rw,[status(thm)],[t739]) ).
cnf(f6,hypothesis,
a_43 = store(a2,i1,e_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f6_nnf,plain,
a_43 = store(a2,i1,e_42),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
a_43 = store(a2,i1,e_42),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t28,plain,
store(a2,i1,e_42) = a_43,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t119,plain,
store(a2,i1,e_42) = a_43,
inference(orient,[status(thm)],[t28]) ).
cnf(t121,plain,
e_42 = select(a_43,i1),
inference(cp,[status(thm)],[t55,t119]) ).
cnf(t322,plain,
select(a_43,i1) = e_42,
inference(orient,[status(thm)],[t121]) ).
cnf(f27,hypothesis,
e_44 = select(a_43,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f27_nnf,plain,
e_44 = select(a_43,i2),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
e_44 = select(a_43,i2),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(t10,plain,
select(a_43,i2) = e_44,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t156,plain,
select(a_43,i2) = e_44,
inference(orient,[status(thm)],[t10]) ).
cnf(t157,plain,
a_43 = store(a_43,i2,e_44),
inference(cp,[status(thm)],[t54,t156]) ).
cnf(t381,plain,
store(a_43,i2,e_44) = a_43,
inference(orient,[status(thm)],[t157]) ).
cnf(t723,plain,
store(a_43,i2,e_46) = a_43,
inference(step,[status(thm)],[t381,t550]) ).
cnf(t703,plain,
store(a_43,i2,e_46) = a_79,
inference(step,[status(thm)],[t113,t516]) ).
cnf(t517,plain,
store(a_43,i2,e_46) = a_79,
inference(orient,[status(thm)],[t703]) ).
cnf(t724,plain,
a_79 = a_43,
inference(step,[status(thm)],[t723,t517]) ).
cnf(t553,plain,
a_79 = a_43,
inference(rw,[status(thm)],[t724]) ).
cnf(t555,plain,
a_43 = a_79,
inference(orient,[status(thm)],[t553]) ).
cnf(t731,plain,
select(a_79,i1) = e_42,
inference(step,[status(thm)],[t322,t555]) ).
cnf(t559,plain,
select(a_79,i1) = e_42,
inference(rw,[status(thm)],[t731]) ).
cnf(t567,plain,
select(a_79,i1) = e_42,
inference(orient,[status(thm)],[t559]) ).
cnf(t740,plain,
e_42 = e_40,
inference(step,[status(thm)],[t566,t567]) ).
cnf(t570,plain,
e_40 = e_42,
inference(orient,[status(thm)],[t740]) ).
cnf(t743,plain,
store(a2,i1,e_42) = a2,
inference(step,[status(thm)],[t387,t570]) ).
cnf(t727,plain,
store(a2,i1,e_42) = a_79,
inference(step,[status(thm)],[t119,t555]) ).
cnf(t556,plain,
store(a2,i1,e_42) = a_79,
inference(orient,[status(thm)],[t727]) ).
cnf(t744,plain,
a_79 = a2,
inference(step,[status(thm)],[t743,t556]) ).
cnf(t573,plain,
a_79 = a2,
inference(rw,[status(thm)],[t744]) ).
cnf(t575,plain,
a2 = a_79,
inference(orient,[status(thm)],[t573]) ).
cnf(t733,plain,
store(a1,i1,e_40) = a_79,
inference(step,[status(thm)],[t116,t561]) ).
cnf(t562,plain,
store(a1,i1,e_40) = a_79,
inference(orient,[status(thm)],[t733]) ).
cnf(t745,plain,
store(a1,i1,e_42) = a_79,
inference(step,[status(thm)],[t562,t570]) ).
cnf(f26,hypothesis,
e_42 = select(a1,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f26_nnf,plain,
e_42 = select(a1,i1),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
e_42 = select(a1,i1),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t7,plain,
select(a1,i1) = e_42,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t158,plain,
select(a1,i1) = e_42,
inference(orient,[status(thm)],[t7]) ).
cnf(t159,plain,
a1 = store(a1,i1,e_42),
inference(cp,[status(thm)],[t54,t158]) ).
cnf(t384,plain,
store(a1,i1,e_42) = a1,
inference(orient,[status(thm)],[t159]) ).
cnf(t746,plain,
a1 = a_79,
inference(step,[status(thm)],[t745,t384]) ).
cnf(t574,plain,
a1 = a_79,
inference(rw,[status(thm)],[t746]) ).
cnf(t578,plain,
a1 = a_79,
inference(orient,[status(thm)],[t574]) ).
cnf(f46,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f46_nnf,plain,
a1 != a2,
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
a1 != a2,
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
a1 != a2,
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(goal_0,negated_conjecture,
a2 != a1,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(g0_0,plain,
a_79 != a1,
inference(rw,[status(thm)],[goal_0,t575]) ).
cnf(g0_1,plain,
a_79 != a_79,
inference(rw,[status(thm)],[g0_0,t578]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV558-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n014.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 20:30:32 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.81/1.36 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.81/1.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------