%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV540-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 : Tue Sep 29 01:25:09 PM UTC 2026
% Result : Unsatisfiable 15.48s 2.70s
% Output : Refutation 15.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 58
% Syntax : Number of formulae : 380 ( 123 unt; 8 def)
% Number of atoms : 803 ( 391 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 752 ( 329 ~; 415 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 9 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-3 aty)
% Number of variables : 79 ( 0 sgn 79 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] :
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f8,axiom,
a_787 = store(a_785,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_789 = store(a_787,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_791 = store(a_789,i0,e_790),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_793 = store(a_791,i5,e_792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_795 = store(a_793,i2,e_794),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_797 = store(a_795,i5,e_796),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
a_799 = store(a_797,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
a_800 = store(a_799,i1,e_798),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
a_802 = store(a_800,i5,e_801),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
a_804 = store(a_802,i2,e_803),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
a_806 = store(a_804,i5,e_805),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
a_808 = store(a_806,i2,e_807),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f20,axiom,
a_809 = store(a_785,i1,e_788),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f21,axiom,
a_810 = store(a_809,i2,e_786),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
a_812 = store(a_810,i5,e_811),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f23,axiom,
a_814 = store(a_812,i0,e_813),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f24,axiom,
a_816 = store(a_814,i5,e_815),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f25,axiom,
a_818 = store(a_816,i2,e_817),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f26,axiom,
a_820 = store(a_818,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f27,axiom,
a_821 = store(a_820,i1,e_819),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f28,axiom,
a_823 = store(a_821,i5,e_822),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f29,axiom,
a_825 = store(a_823,i2,e_824),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f30,axiom,
a_827 = store(a_825,i5,e_826),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f31,axiom,
a_829 = store(a_827,i2,e_828),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f34,axiom,
e_786 = select(a_785,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f35,axiom,
e_788 = select(a_785,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f36,axiom,
e_790 = select(a_789,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f37,axiom,
e_792 = select(a_789,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f38,axiom,
e_794 = select(a_793,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f39,axiom,
e_796 = select(a_793,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f40,axiom,
e_798 = select(a_797,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f41,axiom,
e_801 = select(a_800,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f42,axiom,
e_803 = select(a_800,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f43,axiom,
e_805 = select(a_804,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f44,axiom,
e_807 = select(a_804,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f45,axiom,
e_811 = select(a_810,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f46,axiom,
e_813 = select(a_810,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f47,axiom,
e_815 = select(a_814,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f48,axiom,
e_817 = select(a_814,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp42) ).
fof(f49,axiom,
e_819 = select(a_818,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f50,axiom,
e_822 = select(a_821,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp44) ).
fof(f51,axiom,
e_824 = select(a_821,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp45) ).
fof(f52,axiom,
e_826 = select(a_825,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp46) ).
fof(f53,axiom,
e_828 = select(a_825,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp47) ).
fof(f54,negated_conjecture,
a_808 != a_829,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f58,plain,
e_788 = select(a_809,i1),
inference(superposition,[],[f1,f20]) ).
fof(f61,plain,
e_792 = select(a_793,i5),
inference(superposition,[],[f1,f11]) ).
fof(f62,plain,
e_794 = select(a_795,i2),
inference(superposition,[],[f1,f12]) ).
fof(f63,plain,
e_796 = select(a_797,i5),
inference(superposition,[],[f1,f13]) ).
fof(f64,plain,
e_798 = select(a_799,i1),
inference(superposition,[],[f1,f14]) ).
fof(f66,plain,
e_801 = select(a_802,i5),
inference(superposition,[],[f1,f16]) ).
fof(f67,plain,
e_803 = select(a_804,i2),
inference(superposition,[],[f1,f17]) ).
fof(f68,plain,
e_805 = select(a_806,i5),
inference(superposition,[],[f1,f18]) ).
fof(f72,plain,
e_813 = select(a_814,i0),
inference(superposition,[],[f1,f23]) ).
fof(f73,plain,
e_815 = select(a_816,i5),
inference(superposition,[],[f1,f24]) ).
fof(f74,plain,
e_817 = select(a_818,i2),
inference(superposition,[],[f1,f25]) ).
fof(f75,plain,
e_819 = select(a_820,i1),
inference(superposition,[],[f1,f26]) ).
fof(f77,plain,
e_822 = select(a_823,i5),
inference(superposition,[],[f1,f28]) ).
fof(f78,plain,
e_824 = select(a_825,i2),
inference(superposition,[],[f1,f29]) ).
fof(f79,plain,
e_826 = select(a_827,i5),
inference(superposition,[],[f1,f30]) ).
fof(f84,plain,
a_785 = store(a_785,i1,e_786),
inference(superposition,[],[f3,f34]) ).
fof(f85,plain,
a_785 = store(a_785,i2,e_788),
inference(superposition,[],[f3,f35]) ).
fof(f87,plain,
a_789 = store(a_789,i5,e_790),
inference(superposition,[],[f3,f36]) ).
fof(f89,plain,
a_793 = store(a_793,i5,e_794),
inference(superposition,[],[f3,f38]) ).
fof(f90,plain,
a_793 = store(a_793,i2,e_796),
inference(superposition,[],[f3,f39]) ).
fof(f91,plain,
a_797 = store(a_797,i1,e_798),
inference(superposition,[],[f3,f40]) ).
fof(f92,plain,
a_800 = store(a_800,i2,e_801),
inference(superposition,[],[f3,f41]) ).
fof(f98,plain,
a_814 = store(a_814,i2,e_815),
inference(superposition,[],[f3,f47]) ).
fof(f100,plain,
a_818 = store(a_818,i1,e_819),
inference(superposition,[],[f3,f49]) ).
fof(f102,plain,
a_821 = store(a_821,i5,e_824),
inference(superposition,[],[f3,f51]) ).
fof(f104,plain,
a_825 = store(a_825,i5,e_828),
inference(superposition,[],[f3,f53]) ).
fof(f114,plain,
! [X0] : store(a_793,i2,X0) = store(a_795,i2,X0),
inference(superposition,[],[f4,f12]) ).
fof(f115,plain,
! [X0] : store(a_795,i5,X0) = store(a_797,i5,X0),
inference(superposition,[],[f4,f13]) ).
fof(f118,plain,
! [X0] : store(a_800,i5,X0) = store(a_802,i5,X0),
inference(superposition,[],[f4,f16]) ).
fof(f120,plain,
! [X0] : store(a_804,i5,X0) = store(a_806,i5,X0),
inference(superposition,[],[f4,f18]) ).
fof(f124,plain,
! [X0] : store(a_812,i0,X0) = store(a_814,i0,X0),
inference(superposition,[],[f4,f23]) ).
fof(f126,plain,
! [X0] : store(a_816,i2,X0) = store(a_818,i2,X0),
inference(superposition,[],[f4,f25]) ).
fof(f129,plain,
! [X0] : store(a_821,i5,X0) = store(a_823,i5,X0),
inference(superposition,[],[f4,f28]) ).
fof(f130,plain,
! [X0] : store(a_823,i2,X0) = store(a_825,i2,X0),
inference(superposition,[],[f4,f29]) ).
fof(f131,plain,
! [X0] : store(a_825,i5,X0) = store(a_827,i5,X0),
inference(superposition,[],[f4,f30]) ).
fof(f151,plain,
! [X0] :
( select(a_802,X0) = select(a_804,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f17]) ).
fof(f158,plain,
! [X0] :
( select(a_816,X0) = select(a_818,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f25]) ).
fof(f166,plain,
a_809 = store(a_809,i1,e_788),
inference(superposition,[],[f3,f58]) ).
fof(f173,plain,
! [X0,X1] :
( store(store(a_785,X0,X1),i2,e_786) = store(a_787,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f8]) ).
fof(f179,plain,
! [X0,X1] :
( store(store(a_795,X0,X1),i5,e_796) = store(a_797,X0,X1)
| i5 = X0 ),
inference(superposition,[],[f5,f13]) ).
fof(f183,plain,
! [X0,X1] :
( store(store(a_802,X0,X1),i2,e_803) = store(a_804,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f17]) ).
fof(f187,plain,
! [X0,X1] :
( store(store(a_810,X0,X1),i5,e_811) = store(a_812,X0,X1)
| i5 = X0 ),
inference(superposition,[],[f5,f22]) ).
fof(f189,plain,
! [X0,X1] :
( store(store(a_814,X0,X1),i5,e_815) = store(a_816,X0,X1)
| i5 = X0 ),
inference(superposition,[],[f5,f24]) ).
fof(f194,plain,
! [X0,X1] :
( store(store(a_823,X0,X1),i2,e_824) = store(a_825,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f29]) ).
fof(f196,plain,
! [X0,X1] :
( store(store(a_827,X0,X1),i2,e_828) = store(a_829,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f31]) ).
fof(f229,plain,
! [X2,X3,X0,X1,X4] :
( select(store(store(X0,X1,X2),X3,X4),X1) = X2
| X1 = X3 ),
inference(superposition,[],[f1,f5]) ).
fof(f235,plain,
e_792 = e_794,
inference(superposition,[],[f61,f38]) ).
fof(f239,plain,
a_795 = store(a_793,i2,e_792),
inference(superposition,[],[f12,f235]) ).
fof(f240,plain,
a_797 = store(a_797,i5,e_796),
inference(superposition,[],[f3,f63]) ).
fof(f241,plain,
a_799 = store(a_799,i1,e_798),
inference(superposition,[],[f3,f64]) ).
fof(f242,plain,
a_799 = a_800,
inference(forward_demodulation,[],[f241,f15]) ).
fof(f247,plain,
e_803 = e_805,
inference(superposition,[],[f67,f43]) ).
fof(f251,plain,
e_803 = select(a_806,i5),
inference(forward_demodulation,[],[f68,f247]) ).
fof(f255,plain,
a_814 = store(a_814,i0,e_813),
inference(superposition,[],[f3,f72]) ).
fof(f258,plain,
a_820 = store(a_820,i1,e_819),
inference(superposition,[],[f3,f75]) ).
fof(f259,plain,
a_820 = a_821,
inference(forward_demodulation,[],[f258,f27]) ).
fof(f263,plain,
a_823 = store(a_823,i5,e_822),
inference(superposition,[],[f3,f77]) ).
fof(f264,plain,
e_824 = e_826,
inference(superposition,[],[f78,f52]) ).
fof(f268,plain,
e_824 = select(a_827,i5),
inference(forward_demodulation,[],[f79,f264]) ).
fof(f271,plain,
a_827 = store(a_827,i5,e_824),
inference(superposition,[],[f3,f268]) ).
fof(f290,plain,
a_793 = store(a_793,i5,e_792),
inference(forward_demodulation,[],[f89,f235]) ).
fof(f295,plain,
a_797 = a_799,
inference(superposition,[],[f14,f91]) ).
fof(f299,plain,
a_797 = a_800,
inference(forward_demodulation,[],[f295,f242]) ).
fof(f305,plain,
e_796 = select(a_800,i5),
inference(superposition,[],[f63,f299]) ).
fof(f313,plain,
e_796 = e_803,
inference(superposition,[],[f305,f42]) ).
fof(f334,plain,
a_818 = a_820,
inference(superposition,[],[f26,f100]) ).
fof(f338,plain,
a_818 = a_821,
inference(forward_demodulation,[],[f334,f259]) ).
fof(f344,plain,
e_817 = select(a_821,i2),
inference(superposition,[],[f74,f338]) ).
fof(f352,plain,
e_817 = e_822,
inference(superposition,[],[f344,f50]) ).
fof(f484,plain,
! [X0] : store(a_795,i5,X0) = store(a_800,i5,X0),
inference(forward_demodulation,[],[f115,f299]) ).
fof(f487,plain,
a_800 = store(a_800,i5,e_796),
inference(forward_demodulation,[],[f240,f299]) ).
fof(f524,plain,
a_806 = store(a_804,i5,select(a_806,i5)),
inference(superposition,[],[f3,f120]) ).
fof(f525,plain,
a_806 = store(a_804,i5,e_803),
inference(forward_demodulation,[],[f524,f251]) ).
fof(f528,plain,
a_806 = store(a_804,i5,e_796),
inference(forward_demodulation,[],[f525,f313]) ).
fof(f602,plain,
! [X0] : store(a_816,i2,X0) = store(a_821,i2,X0),
inference(forward_demodulation,[],[f126,f338]) ).
fof(f608,plain,
a_823 = store(a_823,i5,e_817),
inference(forward_demodulation,[],[f263,f352]) ).
fof(f624,plain,
! [X0,X1] :
( select(a_823,X1) = select(store(a_825,i2,X0),X1)
| i2 = X1 ),
inference(superposition,[],[f2,f130]) ).
fof(f638,plain,
a_827 = store(a_825,i5,select(a_827,i5)),
inference(superposition,[],[f3,f131]) ).
fof(f639,plain,
a_827 = store(a_825,i5,e_824),
inference(forward_demodulation,[],[f638,f268]) ).
fof(f665,plain,
! [X0,X1] :
( select(a_795,X1) = select(store(a_800,i5,X0),X1)
| i5 = X1 ),
inference(superposition,[],[f2,f484]) ).
fof(f673,plain,
a_816 = store(a_821,i2,select(a_816,i2)),
inference(superposition,[],[f602,f3]) ).
fof(f726,plain,
( e_801 = select(a_804,i5)
| i2 = i5 ),
inference(superposition,[],[f151,f66]) ).
fof(f735,plain,
a_823 = store(a_821,i5,e_817),
inference(superposition,[],[f608,f129]) ).
fof(f766,plain,
! [X0] :
( select(a_816,X0) = select(a_821,X0)
| i2 = X0 ),
inference(forward_demodulation,[],[f158,f338]) ).
fof(f795,plain,
( e_815 = select(a_821,i5)
| i2 = i5 ),
inference(superposition,[],[f766,f73]) ).
fof(f842,plain,
! [X0,X1] :
( e_801 = select(store(a_800,X0,X1),i2)
| i2 = X0 ),
inference(superposition,[],[f229,f92]) ).
fof(f890,plain,
! [X0,X1] :
( e_828 = select(store(a_825,X0,X1),i5)
| i5 = X0 ),
inference(superposition,[],[f229,f104]) ).
fof(f964,plain,
( store(a_787,i1,e_788) = store(a_809,i2,e_786)
| i2 = i1 ),
inference(superposition,[],[f173,f20]) ).
fof(f987,plain,
( store(a_787,i1,e_788) = a_810
| i2 = i1 ),
inference(forward_demodulation,[],[f964,f21]) ).
fof(f988,plain,
( a_789 = a_810
| i2 = i1 ),
inference(forward_demodulation,[],[f987,f9]) ).
fof(f990,definition,
( spl0_1
<=> i2 = i1 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f992,plain,
( i2 = i1
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f994,definition,
( spl0_2
<=> a_789 = a_810 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f995,plain,
( a_789 != a_810
| spl0_2 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f996,plain,
( a_789 = a_810
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f997,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f988,f994,f990]) ).
fof(f1024,plain,
( e_811 = select(a_789,i0)
| ~ spl0_2 ),
inference(superposition,[],[f45,f996]) ).
fof(f1025,plain,
( e_813 = select(a_789,i5)
| ~ spl0_2 ),
inference(superposition,[],[f46,f996]) ).
fof(f1030,plain,
( e_790 = e_813
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1025,f36]) ).
fof(f1031,plain,
( e_792 = e_811
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1024,f37]) ).
fof(f1053,plain,
( a_814 = store(a_814,i0,e_790)
| ~ spl0_2 ),
inference(superposition,[],[f255,f1030]) ).
fof(f1107,plain,
! [X0,X1] :
( store(store(a_795,X0,X1),i5,e_796) = store(a_800,X0,X1)
| i5 = X0 ),
inference(forward_demodulation,[],[f179,f299]) ).
fof(f1139,plain,
! [X0,X1] :
( store(a_804,X0,X1) = store(store(a_802,X0,X1),i2,e_796)
| i2 = X0 ),
inference(forward_demodulation,[],[f183,f313]) ).
fof(f1173,plain,
( ! [X0,X1] :
( store(a_812,X0,X1) = store(store(a_810,X0,X1),i5,e_792)
| i5 = X0 )
| ~ spl0_2 ),
inference(forward_demodulation,[],[f187,f1031]) ).
fof(f1174,plain,
( ! [X0,X1] :
( store(a_812,X0,X1) = store(store(a_789,X0,X1),i5,e_792)
| i5 = X0 )
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1173,f996]) ).
fof(f1190,plain,
( store(a_814,i5,e_815) = store(a_816,i2,e_815)
| i2 = i5 ),
inference(superposition,[],[f189,f98]) ).
fof(f1211,plain,
( a_816 = store(a_816,i2,e_815)
| i2 = i5 ),
inference(forward_demodulation,[],[f1190,f24]) ).
fof(f1224,plain,
! [X0] :
( store(a_825,i5,X0) = store(store(a_821,i5,X0),i2,e_824)
| i2 = i5 ),
inference(superposition,[],[f194,f129]) ).
fof(f1257,plain,
! [X0] :
( store(a_829,i5,X0) = store(store(a_825,i5,X0),i2,e_828)
| i2 = i5 ),
inference(superposition,[],[f196,f131]) ).
fof(f1418,plain,
! [X0] :
( store(a_800,i2,X0) = store(store(a_793,i2,X0),i5,e_796)
| i2 = i5 ),
inference(superposition,[],[f1107,f114]) ).
fof(f1476,plain,
! [X0] :
( store(a_804,i5,X0) = store(store(a_800,i5,X0),i2,e_796)
| i2 = i5 ),
inference(superposition,[],[f1139,f118]) ).
fof(f1557,plain,
( store(a_791,i5,e_792) = store(a_812,i0,e_790)
| i0 = i5
| ~ spl0_2 ),
inference(superposition,[],[f1174,f10]) ).
fof(f1578,plain,
( store(a_791,i5,e_792) = store(a_814,i0,e_790)
| i0 = i5
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1557,f124]) ).
fof(f1581,plain,
( store(a_791,i5,e_792) = a_814
| i0 = i5
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1578,f1053]) ).
fof(f1582,plain,
( a_793 = a_814
| i0 = i5
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1581,f11]) ).
fof(f1584,definition,
( spl0_5
<=> i0 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f1586,plain,
( i0 = i5
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1588,definition,
( spl0_6
<=> a_793 = a_814 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f1589,plain,
( a_793 != a_814
| spl0_6 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1590,plain,
( a_793 = a_814
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1591,plain,
( spl0_5
| spl0_6
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1582,f994,f1588,f1584]) ).
fof(f1617,plain,
( a_809 = store(a_785,i2,e_788)
| ~ spl0_1 ),
inference(superposition,[],[f20,f992]) ).
fof(f1629,plain,
( a_785 = store(a_785,i2,e_786)
| ~ spl0_1 ),
inference(superposition,[],[f84,f992]) ).
fof(f1652,plain,
( a_785 = a_809
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1617,f85]) ).
fof(f1701,plain,
( e_788 = select(a_785,i1)
| ~ spl0_1 ),
inference(superposition,[],[f58,f1652]) ).
fof(f1707,plain,
( e_786 = e_788
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1701,f34]) ).
fof(f1711,plain,
( a_809 = store(a_809,i1,e_786)
| ~ spl0_1 ),
inference(superposition,[],[f166,f1707]) ).
fof(f1718,plain,
( a_809 = store(a_809,i2,e_786)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1711,f992]) ).
fof(f1723,plain,
( a_809 = a_810
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1718,f21]) ).
fof(f1725,plain,
( a_785 = a_810
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1723,f1652]) ).
fof(f1734,plain,
( a_785 != a_789
| ~ spl0_1
| spl0_2 ),
inference(superposition,[],[f995,f1725]) ).
fof(f3503,plain,
( a_785 = a_787
| ~ spl0_1 ),
inference(superposition,[],[f1629,f8]) ).
fof(f3514,plain,
( a_789 = store(a_785,i1,e_788)
| ~ spl0_1 ),
inference(superposition,[],[f9,f3503]) ).
fof(f3525,plain,
( a_789 = store(a_785,i1,e_786)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f3514,f1707]) ).
fof(f3528,plain,
( a_785 = a_789
| ~ spl0_1 ),
inference(forward_demodulation,[],[f3525,f84]) ).
fof(f3530,plain,
( $false
| ~ spl0_1
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f3528,f1734]) ).
fof(f3531,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_contradiction_clause,[],[f3530]) ).
fof(f4312,plain,
( e_815 = select(a_793,i2)
| ~ spl0_6 ),
inference(superposition,[],[f47,f1590]) ).
fof(f4313,plain,
( e_817 = select(a_793,i5)
| ~ spl0_6 ),
inference(superposition,[],[f48,f1590]) ).
fof(f4321,plain,
( e_794 = e_817
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4313,f38]) ).
fof(f4322,plain,
( e_796 = e_815
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4312,f39]) ).
fof(f4447,definition,
( spl0_8
<=> i2 = i5 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f4448,plain,
( i2 != i5
| spl0_8 ),
inference(avatar_component_clause,[],[f4447]) ).
fof(f4449,plain,
( i2 = i5
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f4447]) ).
fof(f4480,plain,
( e_796 = select(a_821,i5)
| i2 = i5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f795,f4322]) ).
fof(f4499,definition,
( spl0_11
<=> e_796 = select(a_821,i5) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f4500,plain,
( e_796 != select(a_821,i5)
| spl0_11 ),
inference(avatar_component_clause,[],[f4499]) ).
fof(f4501,plain,
( e_796 = select(a_821,i5)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f4499]) ).
fof(f4502,plain,
( spl0_8
| spl0_11
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f4480,f1588,f4499,f4447]) ).
fof(f4503,plain,
( e_796 = e_824
| ~ spl0_11 ),
inference(superposition,[],[f4501,f51]) ).
fof(f4506,plain,
( a_821 = store(a_821,i5,e_796)
| ~ spl0_11 ),
inference(superposition,[],[f3,f4501]) ).
fof(f4550,plain,
( a_816 = store(a_816,i2,e_796)
| i2 = i5
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1211,f4322]) ).
fof(f4631,definition,
( spl0_16
<=> a_816 = store(a_816,i2,e_796) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f4633,plain,
( a_816 = store(a_816,i2,e_796)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f4631]) ).
fof(f4634,plain,
( spl0_8
| spl0_16
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f4550,f1588,f4631,f4447]) ).
fof(f4640,plain,
( a_816 = store(a_821,i2,e_796)
| ~ spl0_16 ),
inference(superposition,[],[f4633,f602]) ).
fof(f4686,plain,
( a_791 = store(a_789,i5,e_790)
| ~ spl0_5 ),
inference(superposition,[],[f10,f1586]) ).
fof(f4688,plain,
( e_792 = select(a_789,i5)
| ~ spl0_5 ),
inference(superposition,[],[f37,f1586]) ).
fof(f4716,plain,
( e_790 = e_792
| ~ spl0_5 ),
inference(forward_demodulation,[],[f4688,f36]) ).
fof(f4718,plain,
( a_789 = a_791
| ~ spl0_5 ),
inference(forward_demodulation,[],[f4686,f87]) ).
fof(f7351,plain,
( e_796 = e_815
| i2 = i5
| ~ spl0_11 ),
inference(forward_demodulation,[],[f795,f4501]) ).
fof(f7465,definition,
( spl0_22
<=> e_796 = e_815 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f7466,plain,
( e_796 != e_815
| spl0_22 ),
inference(avatar_component_clause,[],[f7465]) ).
fof(f7467,plain,
( e_796 = e_815
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f7465]) ).
fof(f7468,plain,
( spl0_8
| spl0_22
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f7351,f4499,f7465,f4447]) ).
fof(f7941,plain,
( a_795 = store(a_793,i5,e_794)
| ~ spl0_8 ),
inference(superposition,[],[f12,f4449]) ).
fof(f7949,plain,
( e_796 = select(a_793,i5)
| ~ spl0_8 ),
inference(superposition,[],[f39,f4449]) ).
fof(f7950,plain,
( e_801 = select(a_800,i5)
| ~ spl0_8 ),
inference(superposition,[],[f41,f4449]) ).
fof(f7952,plain,
( e_815 = select(a_814,i5)
| ~ spl0_8 ),
inference(superposition,[],[f47,f4449]) ).
fof(f7998,plain,
( a_816 = store(a_821,i5,select(a_816,i5))
| ~ spl0_8 ),
inference(superposition,[],[f673,f4449]) ).
fof(f8049,plain,
( a_816 = store(a_821,i5,e_815)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f7998,f73]) ).
fof(f8094,plain,
( e_796 = e_801
| ~ spl0_8 ),
inference(forward_demodulation,[],[f7950,f305]) ).
fof(f8095,plain,
( e_794 = e_796
| ~ spl0_8 ),
inference(forward_demodulation,[],[f7949,f38]) ).
fof(f8103,plain,
( a_795 = store(a_793,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f7941,f235]) ).
fof(f8107,plain,
( a_816 = store(a_821,i5,e_796)
| ~ spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f8049,f7467]) ).
fof(f8118,plain,
( e_792 = e_796
| ~ spl0_8 ),
inference(forward_demodulation,[],[f8095,f235]) ).
fof(f8122,plain,
( a_793 = a_795
| ~ spl0_8 ),
inference(forward_demodulation,[],[f8103,f290]) ).
fof(f8123,plain,
( a_816 = a_821
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f8107,f4506]) ).
fof(f10254,plain,
( e_828 = select(a_823,i5)
| i2 = i5
| i2 = i5 ),
inference(superposition,[],[f624,f890]) ).
fof(f10263,plain,
( e_828 = select(a_823,i5)
| i2 = i5 ),
inference(duplicate_literal_removal,[],[f10254]) ).
fof(f13987,plain,
( a_816 = store(a_814,i5,e_796)
| ~ spl0_22 ),
inference(superposition,[],[f24,f7467]) ).
fof(f13993,plain,
( a_816 = store(a_793,i5,e_796)
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_demodulation,[],[f13987,f1590]) ).
fof(f14840,plain,
( e_815 = select(a_793,i5)
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f7952,f1590]) ).
fof(f14841,plain,
( e_794 = e_815
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f14840,f38]) ).
fof(f14842,plain,
( e_792 = e_815
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f14841,f235]) ).
fof(f20402,plain,
( e_822 = e_828
| i2 = i5 ),
inference(forward_demodulation,[],[f10263,f77]) ).
fof(f20449,plain,
( e_817 = e_828
| i2 = i5 ),
inference(forward_demodulation,[],[f20402,f352]) ).
fof(f20476,plain,
( a_827 = store(a_827,i5,e_796)
| ~ spl0_11 ),
inference(superposition,[],[f271,f4503]) ).
fof(f21428,plain,
( ! [X0] : store(a_825,i5,X0) = store(store(a_821,i5,X0),i2,e_824)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1224,f4448]) ).
fof(f21429,plain,
( ! [X0] : store(a_825,i5,X0) = store(store(a_821,i5,X0),i2,e_796)
| spl0_8
| ~ spl0_11 ),
inference(forward_demodulation,[],[f21428,f4503]) ).
fof(f21447,plain,
( store(a_825,i5,e_824) = store(a_821,i2,e_796)
| spl0_8
| ~ spl0_11 ),
inference(superposition,[],[f21429,f102]) ).
fof(f21482,plain,
( a_816 = store(a_825,i5,e_824)
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f21447,f4640]) ).
fof(f21496,plain,
( a_816 = store(a_825,i5,e_796)
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f21482,f4503]) ).
fof(f21610,plain,
( ! [X0] : store(a_800,i2,X0) = store(store(a_793,i2,X0),i5,e_796)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1418,f4448]) ).
fof(f21621,plain,
( store(a_793,i5,e_796) = store(a_800,i2,e_796)
| spl0_8 ),
inference(superposition,[],[f21610,f90]) ).
fof(f21662,plain,
( a_816 = store(a_800,i2,e_796)
| ~ spl0_6
| spl0_8
| ~ spl0_22 ),
inference(forward_demodulation,[],[f21621,f13993]) ).
fof(f21680,plain,
( ! [X0] : store(a_804,i5,X0) = store(store(a_800,i5,X0),i2,e_796)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1476,f4448]) ).
fof(f21682,plain,
( store(a_804,i5,e_796) = store(a_800,i2,e_796)
| spl0_8 ),
inference(superposition,[],[f21680,f487]) ).
fof(f21723,plain,
( a_806 = store(a_800,i2,e_796)
| spl0_8 ),
inference(forward_demodulation,[],[f21682,f528]) ).
fof(f22091,plain,
( a_806 = a_816
| ~ spl0_6
| spl0_8
| ~ spl0_22 ),
inference(superposition,[],[f21723,f21662]) ).
fof(f22501,plain,
( a_827 = store(a_825,i5,e_796)
| ~ spl0_11 ),
inference(superposition,[],[f131,f20476]) ).
fof(f22514,plain,
( a_816 = a_827
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f22501,f21496]) ).
fof(f22635,plain,
( a_804 = store(a_802,i5,e_803)
| ~ spl0_8 ),
inference(superposition,[],[f17,f4449]) ).
fof(f22654,plain,
( e_824 = select(a_825,i5)
| ~ spl0_8 ),
inference(superposition,[],[f78,f4449]) ).
fof(f22796,plain,
( a_804 = store(a_802,i5,e_796)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22635,f313]) ).
fof(f23457,plain,
( e_811 = select(a_810,i5)
| ~ spl0_5 ),
inference(superposition,[],[f45,f1586]) ).
fof(f23480,plain,
( e_811 = select(a_789,i5)
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f23457,f996]) ).
fof(f23487,plain,
( e_790 = e_811
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f23480,f36]) ).
fof(f24585,plain,
( e_824 = e_828
| ~ spl0_8 ),
inference(superposition,[],[f22654,f53]) ).
fof(f24594,plain,
( a_829 = store(a_827,i2,e_824)
| ~ spl0_8 ),
inference(superposition,[],[f31,f24585]) ).
fof(f24602,plain,
( a_829 = store(a_827,i5,e_824)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f24594,f4449]) ).
fof(f24604,plain,
( a_827 = a_829
| ~ spl0_8 ),
inference(forward_demodulation,[],[f24602,f271]) ).
fof(f24608,plain,
( a_808 != a_827
| ~ spl0_8 ),
inference(superposition,[],[f54,f24604]) ).
fof(f24940,plain,
( a_802 = store(a_800,i5,e_796)
| ~ spl0_8 ),
inference(superposition,[],[f16,f8094]) ).
fof(f24941,plain,
( a_800 = a_802
| ~ spl0_8 ),
inference(forward_demodulation,[],[f24940,f487]) ).
fof(f30285,plain,
( e_792 = e_817
| ~ spl0_6 ),
inference(forward_demodulation,[],[f4321,f235]) ).
fof(f30490,plain,
( a_804 = store(a_800,i5,e_796)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f22796,f24941]) ).
fof(f30747,plain,
( a_800 = a_804
| ~ spl0_8 ),
inference(forward_demodulation,[],[f30490,f487]) ).
fof(f46004,plain,
( e_807 = select(a_800,i5)
| ~ spl0_8 ),
inference(superposition,[],[f44,f30747]) ).
fof(f46030,plain,
( e_803 = e_807
| ~ spl0_8 ),
inference(forward_demodulation,[],[f46004,f42]) ).
fof(f46038,plain,
( e_796 = e_807
| ~ spl0_8 ),
inference(forward_demodulation,[],[f46030,f313]) ).
fof(f46429,plain,
( e_801 = select(a_804,i5)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f726,f4448]) ).
fof(f46431,plain,
( e_801 = e_807
| spl0_8 ),
inference(superposition,[],[f46429,f44]) ).
fof(f46441,plain,
( a_808 = store(a_806,i2,e_801)
| spl0_8 ),
inference(superposition,[],[f19,f46431]) ).
fof(f46559,plain,
( e_817 = e_828
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f20449,f4448]) ).
fof(f48660,plain,
( a_793 = store(a_791,i5,e_790)
| ~ spl0_5 ),
inference(superposition,[],[f11,f4716]) ).
fof(f48670,plain,
( a_793 = store(a_789,i5,e_790)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f48660,f4718]) ).
fof(f48671,plain,
( a_789 = a_793
| ~ spl0_5 ),
inference(forward_demodulation,[],[f48670,f87]) ).
fof(f48675,plain,
( a_812 = store(a_810,i5,e_790)
| ~ spl0_2
| ~ spl0_5 ),
inference(superposition,[],[f22,f23487]) ).
fof(f48682,plain,
( a_812 = store(a_789,i5,e_790)
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f48675,f996]) ).
fof(f48684,plain,
( a_789 = a_812
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f48682,f87]) ).
fof(f48836,plain,
( e_801 = select(a_795,i2)
| i2 = i5
| i2 = i5 ),
inference(superposition,[],[f665,f842]) ).
fof(f48849,plain,
( e_801 = select(a_795,i2)
| i2 = i5 ),
inference(duplicate_literal_removal,[],[f48836]) ).
fof(f48856,plain,
( e_801 = select(a_795,i2)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f48849,f4448]) ).
fof(f48862,plain,
( e_794 = e_801
| spl0_8 ),
inference(forward_demodulation,[],[f48856,f62]) ).
fof(f48868,plain,
( e_792 = e_801
| spl0_8 ),
inference(forward_demodulation,[],[f48862,f235]) ).
fof(f48986,plain,
( a_814 = store(a_789,i0,e_813)
| ~ spl0_2
| ~ spl0_5 ),
inference(superposition,[],[f23,f48684]) ).
fof(f49007,plain,
( store(a_789,i0,e_790) = a_814
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f48986,f1030]) ).
fof(f49011,plain,
( a_814 = store(a_789,i5,e_790)
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f49007,f1586]) ).
fof(f49014,plain,
( a_789 = a_814
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f49011,f87]) ).
fof(f49063,plain,
( a_789 != a_793
| ~ spl0_2
| ~ spl0_5
| spl0_6 ),
inference(superposition,[],[f1589,f49014]) ).
fof(f49073,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f49063,f48671]) ).
fof(f49074,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_6 ),
inference(avatar_contradiction_clause,[],[f49073]) ).
fof(f49121,plain,
( a_829 = store(a_827,i2,e_817)
| spl0_8 ),
inference(superposition,[],[f31,f46559]) ).
fof(f49128,plain,
( store(a_816,i2,e_817) = a_829
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f49121,f22514]) ).
fof(f49129,plain,
( a_818 = a_829
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f49128,f25]) ).
fof(f49130,plain,
( a_821 = a_829
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f49129,f338]) ).
fof(f49223,plain,
( a_808 != a_821
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(superposition,[],[f54,f49130]) ).
fof(f49750,plain,
( ! [X0] : store(a_829,i5,X0) = store(store(a_825,i5,X0),i2,e_828)
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f1257,f4448]) ).
fof(f49751,plain,
( ! [X0] : store(a_829,i5,X0) = store(store(a_825,i5,X0),i2,e_817)
| spl0_8 ),
inference(forward_demodulation,[],[f49750,f46559]) ).
fof(f55631,plain,
( ! [X0] : store(a_821,i5,X0) = store(store(a_825,i5,X0),i2,e_817)
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f49751,f49130]) ).
fof(f56463,plain,
( ! [X0] : store(a_821,i5,X0) = store(store(a_825,i5,X0),i2,e_792)
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f55631,f30285]) ).
fof(f56609,plain,
( store(a_821,i5,e_824) = store(a_827,i2,e_792)
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(superposition,[],[f56463,f639]) ).
fof(f56661,plain,
( store(a_821,i5,e_824) = store(a_816,i2,e_792)
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_demodulation,[],[f56609,f22514]) ).
fof(f56668,plain,
( store(a_821,i5,e_824) = store(a_806,i2,e_792)
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_demodulation,[],[f56661,f22091]) ).
fof(f56672,plain,
( a_821 = store(a_806,i2,e_792)
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_demodulation,[],[f56668,f102]) ).
fof(f61426,plain,
( a_808 = store(a_806,i2,e_792)
| spl0_8 ),
inference(forward_demodulation,[],[f46441,f48868]) ).
fof(f61427,plain,
( a_808 = a_821
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_demodulation,[],[f61426,f56672]) ).
fof(f61428,plain,
( $false
| ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f61427,f49223]) ).
fof(f61429,plain,
( ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f61428]) ).
fof(f61624,plain,
( a_818 = store(a_816,i5,e_817)
| ~ spl0_8 ),
inference(superposition,[],[f25,f4449]) ).
fof(f61797,plain,
( a_818 = store(a_816,i5,e_792)
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f61624,f30285]) ).
fof(f61820,plain,
( a_821 = store(a_816,i5,e_792)
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f61797,f338]) ).
fof(f61922,plain,
( a_816 = store(a_814,i5,e_792)
| ~ spl0_6
| ~ spl0_8 ),
inference(superposition,[],[f24,f14842]) ).
fof(f61931,plain,
( a_816 = store(a_793,i5,e_792)
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f61922,f1590]) ).
fof(f61935,plain,
( a_793 = a_816
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f61931,f290]) ).
fof(f62307,plain,
( a_793 = a_821
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f61935,f8123]) ).
fof(f62611,plain,
( e_824 = select(a_793,i5)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f51,f62307]) ).
fof(f62622,plain,
( a_823 = store(a_793,i5,e_817)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f735,f62307]) ).
fof(f62656,plain,
( a_823 = store(a_793,i5,e_792)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62622,f30285]) ).
fof(f62665,plain,
( e_794 = e_824
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62611,f38]) ).
fof(f62676,plain,
( a_793 = a_823
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62656,f290]) ).
fof(f62683,plain,
( e_792 = e_824
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62665,f235]) ).
fof(f62804,plain,
( a_825 = store(a_793,i2,e_824)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f29,f62676]) ).
fof(f62851,plain,
( a_825 = store(a_793,i2,e_796)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62804,f4503]) ).
fof(f62859,plain,
( a_793 = a_825
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f62851,f90]) ).
fof(f69071,plain,
( a_797 = store(a_795,i5,e_792)
| ~ spl0_8 ),
inference(superposition,[],[f13,f8118]) ).
fof(f69111,plain,
( a_797 = store(a_793,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f69071,f8122]) ).
fof(f69123,plain,
( a_793 = a_797
| ~ spl0_8 ),
inference(forward_demodulation,[],[f69111,f290]) ).
fof(f69444,plain,
( e_792 = e_807
| ~ spl0_8 ),
inference(forward_demodulation,[],[f46038,f8118]) ).
fof(f70295,plain,
( a_793 = a_800
| ~ spl0_8 ),
inference(superposition,[],[f69123,f299]) ).
fof(f70349,plain,
( e_803 = select(a_793,i5)
| ~ spl0_8 ),
inference(superposition,[],[f42,f70295]) ).
fof(f70401,plain,
( e_794 = e_803
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70349,f38]) ).
fof(f70412,plain,
( e_792 = e_803
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70401,f235]) ).
fof(f70441,plain,
( a_827 = store(a_825,i5,e_792)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f639,f62683]) ).
fof(f70447,plain,
( a_827 = store(a_793,i5,e_792)
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f70441,f62859]) ).
fof(f70452,plain,
( a_793 = a_827
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_demodulation,[],[f70447,f290]) ).
fof(f70468,plain,
( a_804 = store(a_802,i2,e_792)
| ~ spl0_8 ),
inference(superposition,[],[f17,f70412]) ).
fof(f70469,plain,
( a_804 = store(a_802,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70468,f4449]) ).
fof(f70471,plain,
( a_804 = store(a_800,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70469,f24941]) ).
fof(f70472,plain,
( a_804 = store(a_793,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70471,f70295]) ).
fof(f70473,plain,
( a_793 = a_804
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70472,f290]) ).
fof(f70675,plain,
( a_793 != a_808
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(superposition,[],[f24608,f70452]) ).
fof(f70799,plain,
( a_806 = store(a_793,i5,e_796)
| ~ spl0_8 ),
inference(superposition,[],[f528,f70473]) ).
fof(f70822,plain,
( a_806 = store(a_793,i5,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70799,f8118]) ).
fof(f70840,plain,
( a_793 = a_806
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70822,f290]) ).
fof(f70974,plain,
( a_808 = store(a_793,i2,e_807)
| ~ spl0_8 ),
inference(superposition,[],[f19,f70840]) ).
fof(f71008,plain,
( a_808 = store(a_793,i2,e_792)
| ~ spl0_8 ),
inference(forward_demodulation,[],[f70974,f69444]) ).
fof(f71018,plain,
( a_795 = a_808
| ~ spl0_8 ),
inference(forward_demodulation,[],[f71008,f239]) ).
fof(f71020,plain,
( a_793 = a_808
| ~ spl0_8 ),
inference(forward_demodulation,[],[f71018,f8122]) ).
fof(f71021,plain,
( $false
| ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f71020,f70675]) ).
fof(f71022,plain,
( ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f71021]) ).
fof(f71023,plain,
( e_792 != e_796
| ~ spl0_6
| ~ spl0_8
| spl0_22 ),
inference(forward_demodulation,[],[f7466,f14842]) ).
fof(f71124,plain,
( a_821 = store(a_793,i5,e_792)
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f61820,f61935]) ).
fof(f71160,plain,
( $false
| ~ spl0_6
| ~ spl0_8
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f71023,f8118]) ).
fof(f71161,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f71160]) ).
fof(f71209,plain,
( a_793 = a_821
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_demodulation,[],[f71124,f290]) ).
fof(f71258,plain,
( e_792 != select(a_821,i5)
| ~ spl0_8
| spl0_11 ),
inference(forward_demodulation,[],[f4500,f8118]) ).
fof(f71380,plain,
( e_792 != select(a_793,i5)
| ~ spl0_6
| ~ spl0_8
| spl0_11 ),
inference(superposition,[],[f71258,f71209]) ).
fof(f71381,plain,
( $false
| ~ spl0_6
| ~ spl0_8
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f71380,f61]) ).
fof(f71382,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_11 ),
inference(avatar_contradiction_clause,[],[f71381]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f997]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s5,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f3531]) ).
cnf(s9,plain,
( ~ spl0_6
| spl0_8
| spl0_11 ),
inference(sat_conversion,[],[f4502]) ).
cnf(s14,plain,
( ~ spl0_6
| spl0_8
| spl0_16 ),
inference(sat_conversion,[],[f4634]) ).
cnf(s22,plain,
( spl0_8
| ~ spl0_11
| spl0_22 ),
inference(sat_conversion,[],[f7468]) ).
cnf(s138,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f49074]) ).
cnf(s148,plain,
( ~ spl0_6
| spl0_8
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(sat_conversion,[],[f61429]) ).
cnf(s150,plain,
( ~ spl0_6
| ~ spl0_8
| ~ spl0_11
| ~ spl0_22 ),
inference(sat_conversion,[],[f71022]) ).
cnf(s151,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_22 ),
inference(sat_conversion,[],[f71161]) ).
cnf(s152,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_11 ),
inference(sat_conversion,[],[f71382]) ).
cnf(s153,plain,
( spl0_8
| ~ spl0_6 ),
inference(rat,[],[s148,s22,s9,s14]) ).
cnf(s154,plain,
( ~ spl0_8
| ~ spl0_22
| ~ spl0_6 ),
inference(rat,[],[s152,s150]) ).
cnf(s155,plain,
( ~ spl0_8
| ~ spl0_6 ),
inference(rat,[],[s154,s151]) ).
cnf(s156,plain,
~ spl0_6,
inference(rat,[],[s155,s153]) ).
cnf(s157,plain,
~ spl0_2,
inference(rat,[],[s4,s138,s156]) ).
cnf(s158,plain,
~ spl0_1,
inference(rat,[],[s5,s157]) ).
cnf(s159,plain,
$false,
inference(rat,[],[s1,s157,s158]) ).
fof(f71419,plain,
$false,
inference(avatar_sat_refutation,[],[s159]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV540-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n005.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 11:38:31 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.23 Running first-order model finding
% 0.10/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.91/2.27 % (732013)Will run a generic schedule for satisfiability detection.
% 13.91/2.27 % (732021)dis+10_1_sil=32000:sp=arity:random_seed=2799239357:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.91/2.27 % (732019)% WARNING: option uhcvi not known.
% 13.91/2.27 % (732018)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2034933150_2999 on theBenchmark for (2999ds/0Mi)
% 13.91/2.27 % (732020)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3743627645:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.91/2.27 % (732019)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=996676206:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.91/2.27 % (732022)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=292538582:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.91/2.27 % (732023)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3551152470:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.91/2.27 % (732024)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3929975224:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.91/2.27 % TRYING [1]
% 13.91/2.27 % TRYING [2]
% 13.91/2.27 % TRYING [3]
% 13.91/2.27 % TRYING [4]
% 13.91/2.27 % (732021)Instruction limit reached!
% 13.91/2.27 % (732021)------------------------------
% 13.91/2.27 % (732021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.91/2.27 % (732021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.27 % (732021)CaDiCaL version: 2.1.3
% 13.91/2.27 % (732021)Termination reason: Instruction limit
% 13.91/2.27 % (732021)Termination phase: Saturation
% 13.91/2.27 % (732021)Time elapsed: 0.030 s
% 13.91/2.27 % (732021)Peak memory usage: 12 MB
% 13.91/2.27 % (732021)Instructions burned: 105 (million)
% 13.91/2.27 % (732032)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2009997065:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.91/2.27 % TRYING [1]
% 13.91/2.27 % TRYING [2]
% 13.91/2.27 % TRYING [3]
% 13.91/2.27 % TRYING [4]
% 13.91/2.27 % TRYING [5]
% 13.91/2.27 % (732022)Instruction limit reached!
% 13.91/2.27 % (732022)------------------------------
% 13.91/2.27 % (732022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.91/2.27 % (732022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.27 % (732022)CaDiCaL version: 2.1.3
% 13.91/2.27 % (732022)Termination reason: Instruction limit
% 13.91/2.27 % (732022)Termination phase: Saturation
% 13.91/2.27 % (732022)Time elapsed: 0.063 s
% 13.91/2.27 % (732022)Peak memory usage: 12 MB
% 13.91/2.27 % (732022)Instructions burned: 117 (million)
% 13.91/2.27 % (732023)Instruction limit reached!
% 13.91/2.27 % (732023)------------------------------
% 13.91/2.27 % (732023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.91/2.27 % (732023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.27 % (732023)CaDiCaL version: 2.1.3
% 13.91/2.27 % (732023)Termination reason: Instruction limit
% 13.91/2.27 % (732023)Termination phase: Saturation
% 13.91/2.27 % (732023)Time elapsed: 0.067 s
% 13.91/2.27 % (732023)Peak memory usage: 12 MB
% 13.91/2.27 % (732023)Instructions burned: 132 (million)
% 13.91/2.27 % TRYING [5]
% 13.91/2.27 % (732034)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3064158035:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.91/2.27 % (732024)Instruction limit reached!
% 13.91/2.27 % (732024)------------------------------
% 13.91/2.27 % (732024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.91/2.27 % (732024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/2.27 % (732024)CaDiCaL version: 2.1.3
% 13.91/2.27 % (732024)Termination reason: Instruction limit
% 13.91/2.27 % (732024)Termination phase: Saturation
% 13.91/2.27 % (732024)Time elapsed: 0.089 s
% 13.91/2.27 % (732024)Peak memory usage: 13 MB
% 13.91/2.27 % (732024)Instructions burned: 160 (million)
% 13.91/2.27 % (732035)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4167601060:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.91/2.27 % (732037)ott-21_1_sil=16000:fs=off:random_seed=2842391674:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.91/2.27 % TRYING [6]
% 13.91/2.27 % (732034)Instruction limit reached!
% 13.91/2.27 % (732034)------------------------------
% 13.91/2.27 % (732034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.91/2.27 % (732034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732034)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732034)Termination reason: Instruction limit
% 15.48/2.70 % (732034)Termination phase: Saturation
% 15.48/2.70 % (732034)Time elapsed: 0.069 s
% 15.48/2.70 % (732034)Peak memory usage: 12 MB
% 15.48/2.70 % (732034)Instructions burned: 133 (million)
% 15.48/2.70 % (732040)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3754622040:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 15.48/2.70 % TRYING [6]
% 15.48/2.70 % (732037)Instruction limit reached!
% 15.48/2.70 % (732037)------------------------------
% 15.48/2.70 % (732037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732037)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732037)Termination reason: Instruction limit
% 15.48/2.70 % (732037)Termination phase: Saturation
% 15.48/2.70 % (732037)Time elapsed: 0.089 s
% 15.48/2.70 % (732037)Peak memory usage: 12 MB
% 15.48/2.70 % (732037)Instructions burned: 180 (million)
% 15.48/2.70 % (732032)Instruction limit reached!
% 15.48/2.70 % (732032)------------------------------
% 15.48/2.70 % (732032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732032)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732032)Termination reason: Instruction limit
% 15.48/2.70 % (732032)Termination phase: Finite model building constraint generation
% 15.48/2.70 % (732032)Time elapsed: 0.175 s
% 15.48/2.70 % (732032)Peak memory usage: 27 MB
% 15.48/2.70 % (732032)Instructions burned: 720 (million)
% 15.48/2.70 % (732042)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3710313342:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 15.48/2.70 % (732043)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3095637744:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 15.48/2.70 % TRYING [1]
% 15.48/2.70 % TRYING [2]
% 15.48/2.70 % TRYING [3]
% 15.48/2.70 % TRYING [4]
% 15.48/2.70 % TRYING [5]
% 15.48/2.70 % TRYING [7]
% 15.48/2.70 % (732040)Instruction limit reached!
% 15.48/2.70 % (732040)------------------------------
% 15.48/2.70 % (732040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732040)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732040)Termination reason: Instruction limit
% 15.48/2.70 % (732040)Termination phase: Saturation
% 15.48/2.70 % (732040)Time elapsed: 0.260 s
% 15.48/2.70 % (732040)Peak memory usage: 13 MB
% 15.48/2.70 % (732040)Instructions burned: 478 (million)
% 15.48/2.70 % (732046)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=562781726:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 15.48/2.70 % (732035)Instruction limit reached!
% 15.48/2.70 % (732035)------------------------------
% 15.48/2.70 % (732035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732035)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732035)Termination reason: Instruction limit
% 15.48/2.70 % (732035)Termination phase: Saturation
% 15.48/2.70 % (732035)Time elapsed: 0.378 s
% 15.48/2.70 % (732035)Peak memory usage: 17 MB
% 15.48/2.70 % (732035)Instructions burned: 686 (million)
% 15.48/2.70 % (732048)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1901322886:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 15.48/2.70 % (732043)Instruction limit reached!
% 15.48/2.70 % (732043)------------------------------
% 15.48/2.70 % (732043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732043)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732043)Termination reason: Instruction limit
% 15.48/2.70 % (732043)Termination phase: Saturation
% 15.48/2.70 % (732043)Time elapsed: 0.306 s
% 15.48/2.70 % (732043)Peak memory usage: 21 MB
% 15.48/2.70 % (732043)Instructions burned: 1180 (million)
% 15.48/2.70 % (732042)Instruction limit reached!
% 15.48/2.70 % (732042)------------------------------
% 15.48/2.70 % (732042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732042)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732042)Termination reason: Instruction limit
% 15.48/2.70 % (732042)Termination phase: Finite model building SAT solving
% 15.48/2.70 % (732042)Time elapsed: 0.318 s
% 15.48/2.70 % (732042)Peak memory usage: 22 MB
% 15.48/2.70 % (732042)Instructions burned: 867 (million)
% 15.48/2.70 % (732050)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1758617966:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 15.48/2.70 % (732052)fmb+10_1_sil=64000:random_seed=3705059503:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 15.48/2.70 % TRYING [1]
% 15.48/2.70 % TRYING [2]
% 15.48/2.70 % TRYING [3]
% 15.48/2.70 % TRYING [4]
% 15.48/2.70 % TRYING [5]
% 15.48/2.70 % (732050)Instruction limit reached!
% 15.48/2.70 % (732050)------------------------------
% 15.48/2.70 % (732050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732050)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732050)Termination reason: Instruction limit
% 15.48/2.70 % (732050)Termination phase: Saturation
% 15.48/2.70 % (732050)Time elapsed: 0.228 s
% 15.48/2.70 % (732050)Peak memory usage: 20 MB
% 15.48/2.70 % (732050)Instructions burned: 881 (million)
% 15.48/2.70 % (732054)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2296610029:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 15.48/2.70 % TRYING [20]
% 15.48/2.70 % (732048)Instruction limit reached!
% 15.48/2.70 % (732048)------------------------------
% 15.48/2.70 % (732048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732048)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732048)Termination reason: Instruction limit
% 15.48/2.70 % (732048)Termination phase: Saturation
% 15.48/2.70 % (732048)Time elapsed: 0.332 s
% 15.48/2.70 % (732048)Peak memory usage: 18 MB
% 15.48/2.70 % (732048)Instructions burned: 693 (million)
% 15.48/2.70 % (732056)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1781470088:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 15.48/2.70 % TRYING [8]
% 15.48/2.70 % (732046)Instruction limit reached!
% 15.48/2.70 % (732046)------------------------------
% 15.48/2.70 % (732046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732046)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732046)Termination reason: Instruction limit
% 15.48/2.70 % (732046)Termination phase: Finite model building constraint generation
% 15.48/2.70 % (732046)Time elapsed: 0.420 s
% 15.48/2.70 % (732046)Peak memory usage: 110 MB
% 15.48/2.70 % (732046)Instructions burned: 891 (million)
% 15.48/2.70 % (732058)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=755779957:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 15.48/2.70 % TRYING [6]
% 15.48/2.70 % (732056)Instruction limit reached!
% 15.48/2.70 % (732056)------------------------------
% 15.48/2.70 % (732056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732056)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732056)Termination reason: Instruction limit
% 15.48/2.70 % (732056)Termination phase: Finite model building constraint generation
% 15.48/2.70 % (732056)Time elapsed: 0.344 s
% 15.48/2.70 % (732056)Peak memory usage: 79 MB
% 15.48/2.70 % (732056)Instructions burned: 920 (million)
% 15.48/2.70 % (732060)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=917949183:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 15.48/2.70 % TRYING [8]
% 15.48/2.70 % (732060)Instruction limit reached!
% 15.48/2.70 % (732060)------------------------------
% 15.48/2.70 % (732060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732060)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732060)Termination reason: Instruction limit
% 15.48/2.70 % (732060)Termination phase: Saturation
% 15.48/2.70 % (732060)Time elapsed: 0.748 s
% 15.48/2.70 % (732060)Peak memory usage: 28 MB
% 15.48/2.70 % (732060)Instructions burned: 1473 (million)
% 15.48/2.70 % (732062)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1061594526:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 15.48/2.70 % (732062)Cannot represent all propositional literals internally
% 15.48/2.70 % (732062)Refutation not found, incomplete strategy
% 15.48/2.70 % (732062)------------------------------
% 15.48/2.70 % (732062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.70 % (732062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.70 % (732062)CaDiCaL version: 2.1.3
% 15.48/2.70 % (732062)Termination reason: Refutation not found, incomplete strategy
% 15.48/2.70 % (732062)Time elapsed: 0.003 s
% 15.48/2.70 % (732062)Peak memory usage: 10 MB
% 15.48/2.70 % (732062)Instructions burned: 7 (million)
% 15.48/2.70 % (732062)------------------------------
% 15.48/2.70 % (732062)------------------------------
% 15.48/2.70 % (732064)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2571109655:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 15.48/2.70 % TRYING [16]
% 15.48/2.70 % TRYING [7]
% 15.48/2.70 % (732058) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-732013-732058"...
% 15.48/2.70 % (732058)...printing done.
% 15.48/2.70 % (732058)Refutation found. Thanks to Tanya!
% 15.48/2.70 % SZS status Unsatisfiable for theBenchmark
% 15.48/2.70 % SZS output start Proof for theBenchmark
% See solution above
% 15.48/2.71 % (732058)------------------------------
% 15.48/2.71 % (732058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.48/2.71 % (732058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.48/2.71 % (732058)CaDiCaL version: 2.1.3
% 15.48/2.71 % (732058)Termination reason: Refutation
% 15.48/2.71 % (732058)Time elapsed: 1.438 s
% 15.48/2.71 % (732058)Peak memory usage: 30 MB
% 15.48/2.71 % (732058)Instructions burned: 2768 (million)
% 15.48/2.71 % (732013)Success in time 2.466 s
% 15.48/2.71 % Vampire exiting
%------------------------------------------------------------------------------