%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO076-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 09:36:01 AM UTC 2026
% Result : Unsatisfiable 100.90s 23.34s
% Output : Refutation 162.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 8
% Syntax : Number of formulae : 407 ( 407 unt; 6 def)
% Number of atoms : 407 ( 406 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 405 ( 405 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X2,X0,X1] : nand(nand(X0,nand(nand(X1,X0),X0)),nand(X1,nand(X2,X0))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sh_1) ).
fof(f2,negated_conjecture,
nand(a,nand(b,nand(a,c))) != nand(nand(nand(c,b),b),a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_meredith_2_basis_2) ).
fof(f3,definition,
sF0 = nand(a,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f4,plain,
nand(a,c) = sF0,
inference(reorient_equations,[],[f3]) ).
fof(f5,definition,
sF1 = nand(b,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f6,plain,
nand(b,sF0) = sF1,
inference(reorient_equations,[],[f5]) ).
fof(f7,definition,
sF2 = nand(a,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f8,plain,
nand(a,sF1) = sF2,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF3 = nand(c,b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f10,plain,
nand(c,b) = sF3,
inference(reorient_equations,[],[f9]) ).
fof(f11,definition,
sF4 = nand(sF3,b),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f12,plain,
nand(sF3,b) = sF4,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF5 = nand(sF4,a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f14,plain,
nand(sF4,a) = sF5,
inference(reorient_equations,[],[f13]) ).
fof(f15,plain,
sF2 != sF5,
inference(definition_folding,[],[f2,f14,f12,f10,f8,f6,f4]) ).
fof(f16,plain,
! [X2,X3,X0,X1] : nand(X2,nand(nand(X0,X2),X2)) = nand(nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,nand(X1,X2)))),nand(nand(X2,nand(nand(X0,X2),X2)),nand(X3,nand(X0,nand(X1,X2))))),
inference(superposition,[],[f1,f1]) ).
fof(f17,plain,
! [X2,X3,X0,X1] : nand(nand(nand(X0,nand(X1,X2)),nand(nand(X3,nand(X0,nand(X1,X2))),nand(X0,nand(X1,X2)))),nand(X3,X0)) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f18,plain,
! [X2,X0,X1] : nand(X2,nand(nand(X0,X2),X2)) = nand(nand(nand(X1,X2),nand(nand(nand(X2,nand(nand(X0,X2),X2)),nand(X1,X2)),nand(X1,X2))),X0),
inference(superposition,[],[f1,f1]) ).
fof(f19,plain,
! [X0] : nand(nand(c,nand(nand(X0,c),c)),nand(X0,sF0)) = X0,
inference(superposition,[],[f1,f4]) ).
fof(f20,plain,
! [X0] : a = nand(nand(c,nand(sF0,c)),nand(a,nand(X0,c))),
inference(superposition,[],[f1,f4]) ).
fof(f22,plain,
! [X0] : c = nand(nand(b,nand(sF3,b)),nand(c,nand(X0,b))),
inference(superposition,[],[f1,f10]) ).
fof(f23,plain,
! [X0] : c = nand(nand(b,sF4),nand(c,nand(X0,b))),
inference(forward_demodulation,[],[f22,f12]) ).
fof(f24,plain,
! [X0] : nand(nand(sF0,nand(nand(X0,sF0),sF0)),nand(X0,sF1)) = X0,
inference(superposition,[],[f1,f6]) ).
fof(f33,plain,
c = nand(nand(b,sF4),nand(c,sF4)),
inference(superposition,[],[f23,f12]) ).
fof(f49,plain,
! [X3,X0,X1] : nand(nand(X0,nand(nand(X3,X0),X0)),nand(X3,nand(X1,nand(nand(X0,X1),X1)))) = X3,
inference(superposition,[],[f17,f1]) ).
fof(f62,plain,
! [X2,X0,X1] : nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),nand(X2,X0)) = X2,
inference(superposition,[],[f1,f17]) ).
fof(f108,plain,
! [X0] : nand(sF1,nand(nand(X0,sF1),sF1)) = nand(nand(sF2,nand(nand(nand(sF1,nand(nand(X0,sF1),sF1)),sF2),sF2)),X0),
inference(superposition,[],[f18,f8]) ).
fof(f109,plain,
! [X0] : nand(sF0,nand(nand(X0,sF0),sF0)) = nand(nand(sF1,nand(nand(nand(sF0,nand(nand(X0,sF0),sF0)),sF1),sF1)),X0),
inference(superposition,[],[f18,f6]) ).
fof(f110,plain,
! [X0] : nand(b,nand(nand(X0,b),b)) = nand(nand(sF3,nand(nand(nand(b,nand(nand(X0,b),b)),sF3),sF3)),X0),
inference(superposition,[],[f18,f10]) ).
fof(f112,plain,
! [X0] : nand(a,nand(nand(X0,a),a)) = nand(nand(sF5,nand(nand(nand(a,nand(nand(X0,a),a)),sF5),sF5)),X0),
inference(superposition,[],[f18,f14]) ).
fof(f185,plain,
! [X0] : nand(nand(sF3,nand(nand(X0,sF3),sF3)),nand(X0,c)) = X0,
inference(superposition,[],[f62,f10]) ).
fof(f210,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))) = nand(nand(X0,nand(nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),X0),X0)),X2),
inference(superposition,[],[f18,f62]) ).
fof(f213,plain,
a = nand(nand(c,nand(sF0,c)),nand(a,sF0)),
inference(superposition,[],[f19,f4]) ).
fof(f215,plain,
b = nand(nand(c,nand(nand(b,c),c)),sF1),
inference(superposition,[],[f19,f6]) ).
fof(f244,plain,
a = nand(nand(sF0,nand(nand(a,sF0),sF0)),sF2),
inference(superposition,[],[f24,f8]) ).
fof(f380,plain,
! [X0,X1] : nand(X0,nand(nand(X0,X0),X0)) = nand(nand(X1,nand(nand(nand(X0,nand(nand(X0,X0),X0)),X1),X1)),X0),
inference(superposition,[],[f49,f1]) ).
fof(f381,plain,
! [X0,X1] : nand(nand(X0,nand(nand(X0,X0),X0)),nand(X0,nand(X0,nand(nand(X0,X0),X0)))) = nand(nand(X1,nand(nand(nand(nand(X0,nand(nand(X0,X0),X0)),nand(X0,nand(X0,nand(nand(X0,X0),X0)))),X1),X1)),nand(X0,nand(nand(X0,X0),X0))),
inference(superposition,[],[f49,f16]) ).
fof(f384,plain,
! [X0,X1] : nand(X0,nand(nand(X0,X0),X0)) = nand(X0,nand(nand(X0,nand(nand(X0,X0),X0)),nand(X1,nand(X0,nand(nand(X0,X0),X0))))),
inference(superposition,[],[f16,f49]) ).
fof(f385,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,X0),X0)),
inference(superposition,[],[f16,f49]) ).
fof(f398,plain,
! [X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,X0),nand(X1,nand(X0,X0)))),
inference(forward_demodulation,[],[f384,f385]) ).
fof(f399,plain,
! [X0,X1] : nand(nand(X0,X0),nand(X0,nand(X0,X0))) = nand(nand(X1,nand(nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),X1),X1)),nand(X0,X0)),
inference(forward_demodulation,[],[f381,f385]) ).
fof(f400,plain,
! [X0,X1] : nand(X0,X0) = nand(nand(X1,nand(nand(nand(X0,X0),X1),X1)),X0),
inference(forward_demodulation,[],[f380,f385]) ).
fof(f409,plain,
! [X0,X1] : nand(nand(X0,X0),nand(X0,nand(X1,X0))) = X0,
inference(superposition,[],[f1,f385]) ).
fof(f433,plain,
! [X0,X1] : nand(nand(X1,nand(nand(X0,X1),X1)),nand(X0,X0)) = X0,
inference(backward_demodulation,[],[f399,f409]) ).
fof(f534,plain,
! [X0,X1] : nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)) = nand(nand(nand(X0,X1),nand(nand(nand(X0,X1),nand(X0,X1)),nand(X0,X1))),nand(nand(X0,X1),nand(X0,X1))),
inference(superposition,[],[f18,f400]) ).
fof(f560,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1)),
inference(forward_demodulation,[],[f534,f433]) ).
fof(f586,plain,
nand(c,nand(sF0,c)) = nand(nand(nand(a,sF0),nand(a,nand(a,sF0))),nand(nand(c,nand(sF0,c)),nand(c,nand(sF0,c)))),
inference(superposition,[],[f433,f213]) ).
fof(f606,plain,
! [X0,X1] : nand(X1,nand(nand(X0,X1),X1)) = nand(nand(nand(X0,X0),nand(X0,nand(X0,X0))),nand(nand(X1,nand(nand(X0,X1),X1)),X0)),
inference(superposition,[],[f62,f433]) ).
fof(f608,plain,
! [X0,X1] : nand(X1,nand(nand(X0,X1),X1)) = nand(nand(X0,nand(nand(nand(X1,nand(nand(X0,X1),X1)),X0),X0)),X0),
inference(superposition,[],[f1,f433]) ).
fof(f626,plain,
! [X0,X1] : nand(X1,nand(nand(X0,X1),X1)) = nand(X0,nand(nand(X1,nand(nand(X0,X1),X1)),X0)),
inference(forward_demodulation,[],[f606,f409]) ).
fof(f726,plain,
! [X0,X1] : nand(nand(X0,X1),nand(nand(nand(X0,X0),nand(X0,X1)),nand(X0,X1))) = X0,
inference(superposition,[],[f560,f62]) ).
fof(f763,plain,
! [X0,X1] : nand(nand(X1,X1),nand(X0,X1)) = X1,
inference(superposition,[],[f409,f560]) ).
fof(f769,plain,
! [X0,X1] : nand(X1,X1) = nand(X1,nand(X0,nand(X1,X1))),
inference(superposition,[],[f398,f560]) ).
fof(f787,plain,
! [X0,X1] : nand(nand(nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1),nand(nand(X0,X1),nand(nand(nand(nand(X0,X1),nand(X0,X1)),X1),X1))),nand(X1,X1)) = X1,
inference(superposition,[],[f433,f560]) ).
fof(f1079,plain,
! [X0,X1] : nand(X1,X0) = nand(nand(nand(X1,X0),nand(X1,X0)),X0),
inference(superposition,[],[f763,f763]) ).
fof(f1125,plain,
! [X2,X0,X1] : nand(nand(X1,X0),nand(nand(X2,nand(X1,X0)),nand(X1,X0))) = nand(nand(X0,nand(nand(nand(nand(X1,X0),nand(nand(X2,nand(X1,X0)),nand(X1,X0))),X0),X0)),X2),
inference(superposition,[],[f18,f763]) ).
fof(f1147,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(nand(X0,X1),X1)),
inference(backward_demodulation,[],[f560,f1079]) ).
fof(f1160,plain,
! [X0,X1] : nand(nand(nand(nand(X0,X1),X1),nand(nand(X0,X1),nand(nand(X0,X1),X1))),nand(X1,X1)) = X1,
inference(backward_demodulation,[],[f787,f1079]) ).
fof(f1179,plain,
! [X2,X0,X1] : nand(nand(X1,X0),nand(X1,nand(X2,X0))) = X1,
inference(backward_demodulation,[],[f1,f1147]) ).
fof(f1181,plain,
! [X2,X0,X1] : nand(X0,X2) = nand(nand(nand(X1,X2),nand(nand(nand(X0,X2),nand(X1,X2)),nand(X1,X2))),X0),
inference(backward_demodulation,[],[f18,f1147]) ).
fof(f1183,plain,
! [X3,X0,X1] : nand(nand(X0,nand(nand(X3,X0),X0)),nand(X3,nand(X0,X1))) = X3,
inference(backward_demodulation,[],[f49,f1147]) ).
fof(f1207,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X0,X0)) = X0,
inference(backward_demodulation,[],[f433,f1147]) ).
fof(f1213,plain,
! [X0,X1] : nand(X0,X1) = nand(nand(X0,nand(nand(nand(X0,X1),X0),X0)),X0),
inference(backward_demodulation,[],[f608,f1147]) ).
fof(f1219,plain,
! [X0,X1] : nand(X0,X1) = nand(X0,nand(nand(X0,X1),X0)),
inference(backward_demodulation,[],[f626,f1147]) ).
fof(f1256,plain,
! [X2,X0,X1] : nand(nand(X1,X0),nand(nand(X2,nand(X1,X0)),nand(X1,X0))) = nand(nand(nand(nand(X1,X0),nand(nand(X2,nand(X1,X0)),nand(X1,X0))),X0),X2),
inference(backward_demodulation,[],[f1125,f1147]) ).
fof(f1258,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))) = nand(nand(nand(nand(X0,X1),nand(nand(X2,nand(X0,X1)),nand(X0,X1))),X0),X2),
inference(backward_demodulation,[],[f210,f1147]) ).
fof(f1316,plain,
! [X0,X1] : nand(nand(X0,X0),nand(X0,X1)) = X0,
inference(backward_demodulation,[],[f726,f1147]) ).
fof(f1383,plain,
! [X0] : nand(X0,a) = nand(nand(sF5,nand(nand(nand(X0,a),sF5),sF5)),X0),
inference(backward_demodulation,[],[f112,f1147]) ).
fof(f1396,plain,
! [X0] : nand(X0,b) = nand(nand(sF3,nand(nand(nand(X0,b),sF3),sF3)),X0),
inference(backward_demodulation,[],[f110,f1147]) ).
fof(f1420,plain,
b = nand(nand(b,c),sF1),
inference(backward_demodulation,[],[f215,f1147]) ).
fof(f1430,plain,
! [X0] : nand(X0,sF0) = nand(nand(sF1,nand(nand(nand(X0,sF0),sF1),sF1)),X0),
inference(backward_demodulation,[],[f109,f1147]) ).
fof(f1440,plain,
a = nand(nand(a,sF0),sF2),
inference(backward_demodulation,[],[f244,f1147]) ).
fof(f1443,plain,
! [X0] : nand(X0,sF1) = nand(nand(sF2,nand(nand(nand(X0,sF1),sF2),sF2)),X0),
inference(backward_demodulation,[],[f108,f1147]) ).
fof(f1454,plain,
! [X0] : nand(nand(X0,sF3),nand(X0,c)) = X0,
inference(backward_demodulation,[],[f185,f1147]) ).
fof(f1469,plain,
! [X0] : nand(X0,sF1) = nand(nand(nand(X0,sF1),sF2),X0),
inference(forward_demodulation,[],[f1443,f1147]) ).
fof(f1471,plain,
! [X0] : nand(X0,sF0) = nand(nand(nand(X0,sF0),sF1),X0),
inference(forward_demodulation,[],[f1430,f1147]) ).
fof(f1478,plain,
! [X0] : nand(X0,b) = nand(nand(nand(X0,b),sF3),X0),
inference(forward_demodulation,[],[f1396,f1147]) ).
fof(f1480,plain,
! [X0] : nand(X0,a) = nand(nand(nand(X0,a),sF5),X0),
inference(forward_demodulation,[],[f1383,f1147]) ).
fof(f1524,plain,
! [X2,X0,X1] : nand(X2,nand(X0,X1)) = nand(nand(nand(X2,nand(X0,X1)),X0),X2),
inference(forward_demodulation,[],[f1258,f1147]) ).
fof(f1526,plain,
! [X2,X0,X1] : nand(X2,nand(X1,X0)) = nand(nand(nand(X2,nand(X1,X0)),X0),X2),
inference(forward_demodulation,[],[f1256,f1147]) ).
fof(f1548,plain,
! [X0,X1] : nand(X0,X1) = nand(nand(nand(X0,X1),X0),X0),
inference(forward_demodulation,[],[f1213,f1147]) ).
fof(f1571,plain,
! [X3,X0,X1] : nand(nand(X3,X0),nand(X3,nand(X0,X1))) = X3,
inference(forward_demodulation,[],[f1183,f1147]) ).
fof(f1572,plain,
! [X2,X0,X1] : nand(X0,X2) = nand(nand(nand(X0,X2),nand(X1,X2)),X0),
inference(forward_demodulation,[],[f1181,f1147]) ).
fof(f1619,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X1,X1)) = X1,
inference(backward_demodulation,[],[f1160,f1179]) ).
fof(f1645,plain,
nand(c,nand(sF0,c)) = nand(a,nand(nand(c,nand(sF0,c)),nand(c,nand(sF0,c)))),
inference(backward_demodulation,[],[f586,f1179]) ).
fof(f1839,plain,
! [X0] : sF5 = nand(nand(sF5,nand(X0,a)),sF4),
inference(superposition,[],[f1572,f14]) ).
fof(f1860,plain,
nand(a,c) = nand(c,nand(sF0,c)),
inference(superposition,[],[f1572,f20]) ).
fof(f1862,plain,
nand(c,b) = nand(b,sF4),
inference(superposition,[],[f1572,f33]) ).
fof(f1872,plain,
sF3 = nand(b,sF4),
inference(forward_demodulation,[],[f1862,f10]) ).
fof(f1874,plain,
sF0 = nand(c,nand(sF0,c)),
inference(forward_demodulation,[],[f1860,f4]) ).
fof(f1936,plain,
a = nand(sF0,nand(a,sF0)),
inference(backward_demodulation,[],[f213,f1874]) ).
fof(f1949,plain,
sF0 = nand(a,nand(sF0,sF0)),
inference(backward_demodulation,[],[f1645,f1874]) ).
fof(f2164,plain,
! [X0,X1] : nand(X0,nand(X0,X1)) = nand(nand(X0,X1),X0),
inference(superposition,[],[f1147,f1548]) ).
fof(f2185,plain,
! [X0,X1] : nand(X0,X1) = nand(X0,nand(X0,nand(X0,X1))),
inference(backward_demodulation,[],[f1219,f2164]) ).
fof(f2207,plain,
b = nand(sF3,nand(b,b)),
inference(superposition,[],[f1207,f1872]) ).
fof(f2213,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(X1,nand(X0,X1))),
inference(superposition,[],[f2185,f1147]) ).
fof(f2257,plain,
nand(a,sF0) = nand(sF0,a),
inference(superposition,[],[f2164,f4]) ).
fof(f2260,plain,
nand(sF3,b) = nand(b,sF3),
inference(superposition,[],[f2164,f1872]) ).
fof(f2293,plain,
sF4 = nand(b,sF3),
inference(forward_demodulation,[],[f2260,f12]) ).
fof(f2303,plain,
a = nand(nand(sF0,a),sF2),
inference(backward_demodulation,[],[f1440,f2257]) ).
fof(f2304,plain,
a = nand(sF0,nand(sF0,a)),
inference(backward_demodulation,[],[f1936,f2257]) ).
fof(f2338,plain,
nand(b,sF4) = nand(sF4,b),
inference(superposition,[],[f2164,f2293]) ).
fof(f2341,plain,
sF3 = nand(sF4,b),
inference(forward_demodulation,[],[f2338,f1872]) ).
fof(f2492,plain,
! [X0,X1] : nand(X1,X0) = nand(X0,X1),
inference(superposition,[],[f1572,f1619]) ).
fof(f2524,plain,
! [X2,X0,X1] : nand(X2,nand(X0,X1)) = nand(X2,nand(nand(X2,nand(X0,X1)),X0)),
inference(backward_demodulation,[],[f1524,f2492]) ).
fof(f2526,plain,
! [X2,X0,X1] : nand(X2,nand(X1,X0)) = nand(X2,nand(nand(X2,nand(X1,X0)),X0)),
inference(backward_demodulation,[],[f1526,f2492]) ).
fof(f2546,plain,
! [X0] : nand(X0,sF0) = nand(X0,nand(nand(X0,sF0),sF1)),
inference(backward_demodulation,[],[f1471,f2492]) ).
fof(f2547,plain,
! [X0] : nand(X0,sF1) = nand(X0,nand(nand(X0,sF1),sF2)),
inference(backward_demodulation,[],[f1469,f2492]) ).
fof(f2548,plain,
! [X0] : nand(X0,b) = nand(X0,nand(nand(X0,b),sF3)),
inference(backward_demodulation,[],[f1478,f2492]) ).
fof(f2552,plain,
! [X0] : nand(X0,a) = nand(X0,nand(nand(X0,a),sF5)),
inference(backward_demodulation,[],[f1480,f2492]) ).
fof(f2634,plain,
sF3 = nand(b,c),
inference(backward_demodulation,[],[f10,f2492]) ).
fof(f2654,plain,
sF1 = nand(sF0,b),
inference(backward_demodulation,[],[f6,f2492]) ).
fof(f2661,plain,
b = nand(sF1,nand(b,c)),
inference(backward_demodulation,[],[f1420,f2492]) ).
fof(f2669,plain,
sF2 = nand(sF1,a),
inference(backward_demodulation,[],[f8,f2492]) ).
fof(f2673,plain,
a = nand(sF2,nand(sF0,a)),
inference(backward_demodulation,[],[f2303,f2492]) ).
fof(f2699,plain,
! [X0] : sF5 = nand(sF4,nand(sF5,nand(X0,a))),
inference(backward_demodulation,[],[f1839,f2492]) ).
fof(f2726,plain,
b = nand(sF1,sF3),
inference(backward_demodulation,[],[f2661,f2634]) ).
fof(f2756,plain,
! [X0] : nand(X0,a) = nand(X0,nand(sF5,nand(X0,a))),
inference(forward_demodulation,[],[f2552,f2492]) ).
fof(f2760,plain,
! [X0] : nand(X0,b) = nand(X0,nand(sF3,nand(X0,b))),
inference(forward_demodulation,[],[f2548,f2492]) ).
fof(f2761,plain,
! [X0] : nand(X0,sF1) = nand(X0,nand(sF2,nand(X0,sF1))),
inference(forward_demodulation,[],[f2547,f2492]) ).
fof(f2762,plain,
! [X0] : nand(X0,sF0) = nand(X0,nand(sF1,nand(X0,sF0))),
inference(forward_demodulation,[],[f2546,f2492]) ).
fof(f2767,plain,
! [X2,X0,X1] : nand(X2,nand(X1,X0)) = nand(X2,nand(X0,nand(X2,nand(X1,X0)))),
inference(forward_demodulation,[],[f2526,f2492]) ).
fof(f2769,plain,
! [X2,X0,X1] : nand(X2,nand(X0,X1)) = nand(X2,nand(X0,nand(X2,nand(X0,X1)))),
inference(forward_demodulation,[],[f2524,f2492]) ).
fof(f2800,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(X1,nand(X2,X0))) = X1,
inference(superposition,[],[f1179,f2492]) ).
fof(f2805,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(X1,nand(X0,X2))) = X1,
inference(superposition,[],[f1571,f2492]) ).
fof(f2810,plain,
! [X2,X0,X1] : nand(nand(X2,X1),nand(nand(X0,X1),X2)) = X2,
inference(superposition,[],[f1179,f2492]) ).
fof(f2902,plain,
! [X0] : nand(sF1,X0) = nand(X0,nand(sF2,nand(sF1,X0))),
inference(superposition,[],[f2761,f2492]) ).
fof(f2933,plain,
! [X0] : nand(sF0,X0) = nand(X0,nand(sF1,nand(sF0,X0))),
inference(superposition,[],[f2762,f2492]) ).
fof(f3056,plain,
! [X0] : nand(a,X0) = nand(X0,nand(sF5,nand(a,X0))),
inference(superposition,[],[f2756,f2492]) ).
fof(f3192,plain,
! [X2,X0,X1] : nand(nand(X0,X1),nand(nand(X2,X0),X1)) = X1,
inference(superposition,[],[f2810,f2492]) ).
fof(f3237,plain,
! [X0] : nand(nand(X0,sF3),nand(b,X0)) = X0,
inference(superposition,[],[f2810,f2726]) ).
fof(f3244,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(nand(nand(nand(X1,X2),X0),X2),X0),
inference(superposition,[],[f2810,f2810]) ).
fof(f3292,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(X0,nand(nand(nand(X1,X2),X0),X2)),
inference(forward_demodulation,[],[f3244,f2492]) ).
fof(f3352,plain,
! [X2,X0,X1] : nand(nand(X1,X2),X0) = nand(X0,nand(X2,nand(nand(X1,X2),X0))),
inference(forward_demodulation,[],[f3292,f2492]) ).
fof(f3622,plain,
! [X2,X0,X1] : nand(X1,X0) = nand(X1,nand(nand(X0,X2),nand(X1,X0))),
inference(superposition,[],[f2769,f1571]) ).
fof(f3625,plain,
! [X0] : nand(X0,sF0) = nand(X0,nand(a,nand(X0,sF0))),
inference(superposition,[],[f2769,f4]) ).
fof(f3682,plain,
! [X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,X1),X1)),
inference(superposition,[],[f2769,f1179]) ).
fof(f3713,plain,
! [X0,X1] : nand(X0,X0) = nand(X0,nand(X1,nand(X0,X1))),
inference(forward_demodulation,[],[f3682,f2492]) ).
fof(f3718,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X1,nand(X0,nand(X1,X2))),nand(X0,nand(X1,X2)))),
inference(superposition,[],[f3713,f2769]) ).
fof(f3724,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(sF3,nand(X0,b)),nand(X0,b))),
inference(superposition,[],[f3713,f2760]) ).
fof(f3728,plain,
! [X0,X1] : nand(X1,X1) = nand(X1,nand(X0,nand(X0,X1))),
inference(superposition,[],[f3713,f2492]) ).
fof(f3754,plain,
nand(sF2,sF2) = nand(sF2,nand(nand(sF0,a),a)),
inference(superposition,[],[f3713,f2673]) ).
fof(f3761,plain,
! [X0,X1] : nand(X1,nand(X0,X0)) = nand(X1,nand(X0,X1)),
inference(superposition,[],[f2769,f3713]) ).
fof(f3786,plain,
b = nand(sF3,nand(b,sF3)),
inference(backward_demodulation,[],[f2207,f3761]) ).
fof(f3809,plain,
nand(sF2,sF2) = nand(sF2,nand(a,nand(sF0,a))),
inference(forward_demodulation,[],[f3754,f2492]) ).
fof(f3836,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,b),nand(sF3,nand(X0,b)))),
inference(forward_demodulation,[],[f3724,f2492]) ).
fof(f3840,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X1,nand(X0,nand(X1,X2))))),
inference(forward_demodulation,[],[f3718,f2492]) ).
fof(f3851,plain,
b = nand(sF3,nand(sF3,b)),
inference(forward_demodulation,[],[f3786,f2492]) ).
fof(f3856,plain,
nand(sF2,sF2) = nand(sF2,nand(a,nand(sF0,sF0))),
inference(forward_demodulation,[],[f3809,f3761]) ).
fof(f3862,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,b),nand(sF3,sF3))),
inference(forward_demodulation,[],[f3836,f3761]) ).
fof(f3866,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X1,X1))),
inference(forward_demodulation,[],[f3840,f3761]) ).
fof(f3868,plain,
b = nand(sF3,sF4),
inference(forward_demodulation,[],[f3851,f12]) ).
fof(f3869,plain,
nand(sF2,sF2) = nand(sF2,sF0),
inference(forward_demodulation,[],[f3856,f1949]) ).
fof(f3876,plain,
nand(sF2,sF2) = nand(sF0,sF2),
inference(forward_demodulation,[],[f3869,f2492]) ).
fof(f3908,plain,
! [X0,X1] : nand(X0,nand(X0,X1)) = nand(X0,nand(X1,X1)),
inference(superposition,[],[f3761,f2492]) ).
fof(f3925,plain,
nand(sF3,b) = nand(sF3,nand(sF1,sF1)),
inference(superposition,[],[f3761,f2726]) ).
fof(f3956,plain,
! [X0,X1] : nand(nand(X1,X1),X0) = nand(X0,nand(X1,X0)),
inference(superposition,[],[f2492,f3761]) ).
fof(f3996,plain,
sF4 = nand(sF3,nand(sF1,sF1)),
inference(forward_demodulation,[],[f3925,f12]) ).
fof(f4070,plain,
! [X0,X1] : nand(X0,X1) = nand(X1,nand(nand(X0,X0),X1)),
inference(superposition,[],[f3956,f1619]) ).
fof(f4089,plain,
! [X0,X1] : nand(X0,nand(X0,X1)) = nand(nand(X1,X1),X0),
inference(superposition,[],[f3956,f2492]) ).
fof(f4262,plain,
! [X2,X0,X1] : nand(nand(X0,nand(X1,X2)),nand(X0,nand(X1,X2))) = nand(nand(X0,nand(X1,X2)),nand(nand(X0,X1),X0)),
inference(superposition,[],[f3728,f1571]) ).
fof(f4265,plain,
nand(c,c) = nand(c,nand(a,sF0)),
inference(superposition,[],[f3728,f4]) ).
fof(f4267,plain,
nand(c,c) = nand(c,nand(b,sF3)),
inference(superposition,[],[f3728,f2634]) ).
fof(f4307,plain,
nand(c,nand(sF3,b)) = nand(c,c),
inference(forward_demodulation,[],[f4267,f2492]) ).
fof(f4308,plain,
nand(c,c) = nand(c,nand(sF0,a)),
inference(forward_demodulation,[],[f4265,f2492]) ).
fof(f4311,plain,
! [X2,X0,X1] : nand(nand(X0,nand(X1,X2)),nand(X0,nand(X1,X2))) = nand(nand(X0,nand(X1,X2)),nand(X0,nand(X0,X1))),
inference(forward_demodulation,[],[f4262,f2492]) ).
fof(f4322,plain,
nand(c,sF4) = nand(c,c),
inference(forward_demodulation,[],[f4307,f12]) ).
fof(f4326,plain,
nand(c,c) = nand(sF4,c),
inference(forward_demodulation,[],[f4322,f2492]) ).
fof(f4333,plain,
nand(sF4,c) = nand(c,nand(sF0,a)),
inference(backward_demodulation,[],[f4308,f4326]) ).
fof(f4342,plain,
! [X0] : nand(X0,nand(sF4,c)) = nand(X0,nand(c,X0)),
inference(superposition,[],[f3761,f4326]) ).
fof(f4343,plain,
! [X0] : nand(nand(sF4,c),X0) = nand(X0,nand(c,X0)),
inference(superposition,[],[f3956,f4326]) ).
fof(f4514,plain,
! [X0,X1] : nand(X0,X1) = nand(X0,nand(X0,nand(X1,X1))),
inference(superposition,[],[f2185,f3908]) ).
fof(f4542,plain,
! [X0,X1] : nand(X0,nand(X0,X1)) = nand(X0,nand(X1,X0)),
inference(superposition,[],[f3761,f3908]) ).
fof(f4598,plain,
! [X0] : nand(sF0,sF2) = nand(sF2,nand(X0,nand(sF0,sF2))),
inference(superposition,[],[f769,f3876]) ).
fof(f4604,plain,
! [X0] : nand(X0,nand(X0,sF2)) = nand(X0,nand(sF0,sF2)),
inference(superposition,[],[f3908,f3876]) ).
fof(f4605,plain,
! [X0] : nand(nand(sF0,sF2),X0) = nand(X0,nand(sF2,X0)),
inference(superposition,[],[f3956,f3876]) ).
fof(f4732,plain,
! [X0,X1] : nand(X1,X0) = nand(X0,nand(X0,nand(X1,X1))),
inference(superposition,[],[f2213,f3761]) ).
fof(f5898,plain,
! [X0] : nand(sF2,X0) = nand(X0,nand(nand(sF0,sF2),X0)),
inference(superposition,[],[f4070,f3876]) ).
fof(f6237,plain,
a = nand(nand(a,sF3),sF0),
inference(superposition,[],[f1454,f4]) ).
fof(f6280,plain,
a = nand(sF0,nand(a,sF3)),
inference(forward_demodulation,[],[f6237,f2492]) ).
fof(f6292,plain,
a = nand(sF0,nand(sF3,a)),
inference(forward_demodulation,[],[f6280,f2492]) ).
fof(f7124,plain,
! [X2,X0,X1] : nand(X1,X0) = nand(nand(nand(X1,X0),nand(X2,X1)),X0),
inference(superposition,[],[f1179,f2800]) ).
fof(f7184,plain,
! [X2,X0,X1] : nand(X1,X0) = nand(X0,nand(nand(X1,X0),nand(X2,X1))),
inference(forward_demodulation,[],[f7124,f2492]) ).
fof(f7441,plain,
! [X0] : nand(c,X0) = nand(X0,nand(nand(c,X0),sF3)),
inference(superposition,[],[f7184,f2634]) ).
fof(f7452,plain,
! [X0] : nand(a,X0) = nand(X0,nand(nand(a,X0),sF2)),
inference(superposition,[],[f7184,f2669]) ).
fof(f7460,plain,
! [X0] : nand(sF4,X0) = nand(X0,nand(nand(sF4,X0),b)),
inference(superposition,[],[f7184,f3868]) ).
fof(f7555,plain,
! [X0] : nand(sF4,X0) = nand(X0,nand(b,nand(sF4,X0))),
inference(forward_demodulation,[],[f7460,f2492]) ).
fof(f7562,plain,
! [X0] : nand(a,X0) = nand(X0,nand(sF2,nand(a,X0))),
inference(forward_demodulation,[],[f7452,f2492]) ).
fof(f7572,plain,
! [X0] : nand(c,X0) = nand(X0,nand(sF3,nand(c,X0))),
inference(forward_demodulation,[],[f7441,f2492]) ).
fof(f8039,plain,
sF0 = nand(c,nand(sF2,sF0)),
inference(superposition,[],[f7562,f4]) ).
fof(f8110,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(sF2,nand(a,X0)),nand(a,X0))),
inference(superposition,[],[f3713,f7562]) ).
fof(f8128,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(a,X0),nand(sF2,nand(a,X0)))),
inference(forward_demodulation,[],[f8110,f2492]) ).
fof(f8167,plain,
sF0 = nand(c,nand(sF0,sF2)),
inference(forward_demodulation,[],[f8039,f2492]) ).
fof(f8174,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(sF0,sF2),nand(a,X0))),
inference(forward_demodulation,[],[f8128,f4605]) ).
fof(f8628,plain,
sF5 = nand(a,nand(b,sF5)),
inference(superposition,[],[f7555,f14]) ).
fof(f8843,plain,
a = nand(nand(a,b),sF5),
inference(superposition,[],[f1571,f8628]) ).
fof(f8885,plain,
a = nand(sF5,nand(a,b)),
inference(forward_demodulation,[],[f8843,f2492]) ).
fof(f8922,plain,
nand(nand(a,b),a) = nand(nand(a,b),nand(sF5,sF5)),
inference(superposition,[],[f3761,f8885]) ).
fof(f8928,plain,
nand(nand(a,b),nand(sF5,sF5)) = nand(a,nand(a,b)),
inference(forward_demodulation,[],[f8922,f2492]) ).
fof(f9090,plain,
! [X0] : nand(nand(c,X0),nand(sF0,X0)) = X0,
inference(superposition,[],[f3192,f4]) ).
fof(f9094,plain,
! [X0] : nand(nand(c,X0),nand(sF3,X0)) = X0,
inference(superposition,[],[f3192,f2634]) ).
fof(f9101,plain,
! [X0] : nand(nand(b,X0),nand(sF1,X0)) = X0,
inference(superposition,[],[f3192,f2654]) ).
fof(f9291,plain,
! [X0] : nand(nand(sF1,X0),nand(b,X0)) = X0,
inference(forward_demodulation,[],[f9101,f2492]) ).
fof(f9297,plain,
! [X0] : nand(nand(sF3,X0),nand(c,X0)) = X0,
inference(forward_demodulation,[],[f9094,f2492]) ).
fof(f9301,plain,
! [X0] : nand(nand(sF0,X0),nand(c,X0)) = X0,
inference(forward_demodulation,[],[f9090,f2492]) ).
fof(f9603,plain,
a = nand(sF2,nand(b,a)),
inference(superposition,[],[f9291,f2669]) ).
fof(f9775,plain,
a = nand(sF2,nand(a,b)),
inference(forward_demodulation,[],[f9603,f2492]) ).
fof(f9863,plain,
nand(nand(a,b),a) = nand(nand(a,b),nand(sF2,sF2)),
inference(superposition,[],[f3761,f9775]) ).
fof(f9869,plain,
nand(nand(a,b),a) = nand(nand(a,b),nand(sF0,sF2)),
inference(forward_demodulation,[],[f9863,f3876]) ).
fof(f9888,plain,
nand(nand(a,b),a) = nand(nand(sF0,sF2),nand(a,b)),
inference(forward_demodulation,[],[f9869,f2492]) ).
fof(f9896,plain,
nand(a,nand(a,b)) = nand(nand(sF0,sF2),nand(a,b)),
inference(forward_demodulation,[],[f9888,f2492]) ).
fof(f10315,plain,
! [X0] : nand(sF3,X0) = nand(nand(nand(sF3,X0),c),X0),
inference(superposition,[],[f1571,f9297]) ).
fof(f10367,plain,
! [X0] : nand(sF3,X0) = nand(X0,nand(nand(sF3,X0),c)),
inference(forward_demodulation,[],[f10315,f2492]) ).
fof(f10421,plain,
! [X0] : nand(sF3,X0) = nand(X0,nand(c,nand(sF3,X0))),
inference(forward_demodulation,[],[f10367,f2492]) ).
fof(f10504,plain,
nand(sF3,sF1) = nand(nand(sF2,nand(sF3,sF1)),nand(c,nand(sF3,sF1))),
inference(superposition,[],[f10421,f2761]) ).
fof(f10618,plain,
nand(sF3,sF1) = nand(nand(c,nand(sF3,sF1)),nand(sF2,nand(sF3,sF1))),
inference(forward_demodulation,[],[f10504,f2492]) ).
fof(f10662,plain,
nand(sF1,sF3) = nand(nand(c,nand(sF1,sF3)),nand(sF2,nand(sF1,sF3))),
inference(forward_demodulation,[],[f10618,f2492]) ).
fof(f10690,plain,
b = nand(nand(c,b),nand(sF2,b)),
inference(forward_demodulation,[],[f10662,f2726]) ).
fof(f10702,plain,
b = nand(nand(c,b),nand(b,sF2)),
inference(forward_demodulation,[],[f10690,f2492]) ).
fof(f10707,plain,
b = nand(nand(b,sF2),nand(c,b)),
inference(forward_demodulation,[],[f10702,f2492]) ).
fof(f10709,plain,
b = nand(nand(b,sF2),nand(b,c)),
inference(forward_demodulation,[],[f10707,f2492]) ).
fof(f10711,plain,
b = nand(nand(b,c),nand(b,sF2)),
inference(forward_demodulation,[],[f10709,f2492]) ).
fof(f10713,plain,
b = nand(sF3,nand(b,sF2)),
inference(forward_demodulation,[],[f10711,f2634]) ).
fof(f10745,plain,
nand(nand(b,sF2),b) = nand(nand(sF3,sF3),nand(b,sF2)),
inference(superposition,[],[f3956,f10713]) ).
fof(f10749,plain,
nand(nand(sF3,sF3),nand(b,sF2)) = nand(b,nand(b,sF2)),
inference(forward_demodulation,[],[f10745,f2492]) ).
fof(f10768,plain,
nand(b,nand(sF0,sF2)) = nand(nand(sF3,sF3),nand(b,sF2)),
inference(forward_demodulation,[],[f10749,f4604]) ).
fof(f12121,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X2,nand(X0,nand(X1,X2))),nand(X0,nand(X1,X2)))),
inference(superposition,[],[f3713,f2767]) ).
fof(f12142,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X2,nand(X0,nand(X1,X2))))),
inference(forward_demodulation,[],[f12121,f2492]) ).
fof(f12195,plain,
! [X2,X0,X1] : nand(X0,X0) = nand(X0,nand(nand(X0,nand(X1,X2)),nand(X2,X2))),
inference(forward_demodulation,[],[f12142,f3761]) ).
fof(f14258,plain,
nand(sF0,a) = nand(nand(sF0,nand(sF0,a)),nand(sF4,c)),
inference(superposition,[],[f9301,f4333]) ).
fof(f14298,plain,
nand(sF0,a) = nand(nand(sF4,c),nand(sF0,nand(sF0,a))),
inference(forward_demodulation,[],[f14258,f2492]) ).
fof(f14307,plain,
nand(sF0,a) = nand(nand(sF4,c),a),
inference(forward_demodulation,[],[f14298,f2304]) ).
fof(f14310,plain,
nand(sF0,a) = nand(a,nand(c,a)),
inference(forward_demodulation,[],[f14307,f4343]) ).
fof(f14311,plain,
nand(sF0,a) = nand(a,nand(sF4,c)),
inference(forward_demodulation,[],[f14310,f4342]) ).
fof(f14317,plain,
a = nand(nand(a,sF4),nand(sF0,a)),
inference(superposition,[],[f1571,f14311]) ).
fof(f14362,plain,
a = nand(nand(sF0,a),nand(a,sF4)),
inference(forward_demodulation,[],[f14317,f2492]) ).
fof(f14369,plain,
a = nand(nand(sF0,a),nand(sF4,a)),
inference(forward_demodulation,[],[f14362,f2492]) ).
fof(f14373,plain,
a = nand(nand(sF0,a),sF5),
inference(forward_demodulation,[],[f14369,f14]) ).
fof(f14375,plain,
a = nand(sF5,nand(sF0,a)),
inference(forward_demodulation,[],[f14373,f2492]) ).
fof(f14409,plain,
nand(sF5,sF5) = nand(sF5,nand(nand(sF0,a),a)),
inference(superposition,[],[f3713,f14375]) ).
fof(f14419,plain,
nand(sF5,sF5) = nand(sF5,nand(a,nand(sF0,a))),
inference(forward_demodulation,[],[f14409,f2492]) ).
fof(f14437,plain,
nand(sF5,sF5) = nand(sF5,nand(a,nand(sF0,sF0))),
inference(forward_demodulation,[],[f14419,f3761]) ).
fof(f14445,plain,
nand(sF5,sF5) = nand(sF5,sF0),
inference(forward_demodulation,[],[f14437,f1949]) ).
fof(f14447,plain,
nand(sF5,sF5) = nand(sF0,sF5),
inference(forward_demodulation,[],[f14445,f2492]) ).
fof(f14459,plain,
nand(a,nand(a,b)) = nand(nand(a,b),nand(sF0,sF5)),
inference(backward_demodulation,[],[f8928,f14447]) ).
fof(f14464,plain,
nand(a,nand(a,b)) = nand(nand(sF0,sF5),nand(a,b)),
inference(forward_demodulation,[],[f14459,f2492]) ).
fof(f14537,plain,
! [X0] : nand(sF0,sF5) = nand(sF5,nand(X0,nand(sF0,sF5))),
inference(superposition,[],[f769,f14447]) ).
fof(f14542,plain,
! [X0] : nand(X0,nand(sF0,sF5)) = nand(X0,nand(sF5,X0)),
inference(superposition,[],[f3761,f14447]) ).
fof(f14545,plain,
! [X0] : nand(nand(sF0,sF5),X0) = nand(X0,nand(sF5,X0)),
inference(superposition,[],[f3956,f14447]) ).
fof(f14546,plain,
! [X0] : nand(sF5,X0) = nand(X0,nand(nand(sF0,sF5),X0)),
inference(superposition,[],[f4070,f14447]) ).
fof(f14603,plain,
! [X0,X1] : nand(nand(X1,nand(sF5,nand(X0,X1))),nand(sF0,sF5)) = nand(nand(X1,nand(sF5,nand(X0,X1))),nand(sF5,nand(X0,X1))),
inference(superposition,[],[f14542,f2767]) ).
fof(f14787,plain,
! [X0,X1] : nand(nand(X1,nand(sF5,nand(X0,X1))),nand(sF0,sF5)) = nand(nand(sF5,nand(X0,X1)),nand(X1,nand(sF5,nand(X0,X1)))),
inference(forward_demodulation,[],[f14603,f2492]) ).
fof(f14831,plain,
! [X0,X1] : nand(nand(X1,nand(sF5,nand(X0,X1))),nand(sF0,sF5)) = nand(nand(sF5,nand(X0,X1)),nand(X1,X1)),
inference(forward_demodulation,[],[f14787,f3761]) ).
fof(f14863,plain,
! [X0,X1] : nand(nand(sF5,nand(X0,X1)),nand(X1,X1)) = nand(nand(sF0,sF5),nand(X1,nand(sF5,nand(X0,X1)))),
inference(forward_demodulation,[],[f14831,f2492]) ).
fof(f15342,plain,
nand(a,nand(b,sF0)) = nand(nand(nand(a,nand(b,sF0)),sF3),nand(b,sF0)),
inference(superposition,[],[f3237,f3625]) ).
fof(f15456,plain,
nand(a,nand(b,sF0)) = nand(nand(b,sF0),nand(nand(a,nand(b,sF0)),sF3)),
inference(forward_demodulation,[],[f15342,f2492]) ).
fof(f15513,plain,
nand(a,nand(b,sF0)) = nand(nand(b,sF0),nand(sF3,nand(a,nand(b,sF0)))),
inference(forward_demodulation,[],[f15456,f2492]) ).
fof(f15551,plain,
nand(a,nand(sF0,b)) = nand(nand(sF0,b),nand(sF3,nand(a,nand(sF0,b)))),
inference(forward_demodulation,[],[f15513,f2492]) ).
fof(f15569,plain,
nand(a,sF1) = nand(sF1,nand(sF3,nand(a,sF1))),
inference(forward_demodulation,[],[f15551,f2654]) ).
fof(f15574,plain,
nand(sF1,a) = nand(sF1,nand(sF3,nand(sF1,a))),
inference(forward_demodulation,[],[f15569,f2492]) ).
fof(f15579,plain,
sF2 = nand(sF1,nand(sF3,sF2)),
inference(forward_demodulation,[],[f15574,f2669]) ).
fof(f15587,plain,
sF1 = nand(nand(sF1,sF3),sF2),
inference(superposition,[],[f1571,f15579]) ).
fof(f15637,plain,
sF1 = nand(sF2,nand(sF1,sF3)),
inference(forward_demodulation,[],[f15587,f2492]) ).
fof(f15647,plain,
sF1 = nand(sF2,b),
inference(forward_demodulation,[],[f15637,f2726]) ).
fof(f15651,plain,
sF1 = nand(b,sF2),
inference(forward_demodulation,[],[f15647,f2492]) ).
fof(f15669,plain,
nand(nand(sF3,sF3),sF1) = nand(b,nand(sF0,sF2)),
inference(backward_demodulation,[],[f10768,f15651]) ).
fof(f15681,plain,
nand(sF1,nand(sF3,sF1)) = nand(b,nand(sF0,sF2)),
inference(forward_demodulation,[],[f15669,f3956]) ).
fof(f15691,plain,
nand(sF1,nand(sF1,sF3)) = nand(b,nand(sF0,sF2)),
inference(forward_demodulation,[],[f15681,f4542]) ).
fof(f15699,plain,
nand(sF1,b) = nand(b,nand(sF0,sF2)),
inference(forward_demodulation,[],[f15691,f2726]) ).
fof(f15733,plain,
! [X0] : nand(nand(sF2,X0),nand(sF1,X0)) = X0,
inference(superposition,[],[f3192,f15651]) ).
fof(f15736,plain,
nand(sF2,sF2) = nand(sF2,nand(b,sF1)),
inference(superposition,[],[f3728,f15651]) ).
fof(f15742,plain,
nand(sF2,sF2) = nand(sF2,nand(sF1,b)),
inference(forward_demodulation,[],[f15736,f2492]) ).
fof(f15745,plain,
! [X0] : nand(nand(sF1,X0),nand(sF2,X0)) = X0,
inference(forward_demodulation,[],[f15733,f2492]) ).
fof(f15762,plain,
nand(sF0,sF2) = nand(sF2,nand(sF1,b)),
inference(forward_demodulation,[],[f15742,f3876]) ).
fof(f18815,plain,
sF0 = nand(c,nand(sF5,sF0)),
inference(superposition,[],[f3056,f4]) ).
fof(f18943,plain,
! [X0] : nand(nand(sF5,nand(a,X0)),nand(a,X0)) = nand(nand(sF5,nand(a,X0)),nand(X0,X0)),
inference(superposition,[],[f3761,f3056]) ).
fof(f18964,plain,
! [X0] : nand(nand(sF5,nand(a,X0)),nand(X0,X0)) = nand(nand(a,X0),nand(sF5,nand(a,X0))),
inference(forward_demodulation,[],[f18943,f2492]) ).
fof(f19041,plain,
sF0 = nand(c,nand(sF0,sF5)),
inference(forward_demodulation,[],[f18815,f2492]) ).
fof(f19047,plain,
! [X0] : nand(nand(sF5,nand(a,X0)),nand(X0,X0)) = nand(nand(sF0,sF5),nand(a,X0)),
inference(forward_demodulation,[],[f18964,f14545]) ).
fof(f19584,plain,
! [X0] : nand(nand(sF2,X0),nand(X0,a)) = X0,
inference(superposition,[],[f2805,f2673]) ).
fof(f19756,plain,
! [X2,X0,X1] : nand(X1,X0) = nand(nand(nand(X1,X2),nand(X1,X0)),X0),
inference(superposition,[],[f2800,f2805]) ).
fof(f19840,plain,
! [X2,X0,X1] : nand(X1,X0) = nand(X0,nand(nand(X1,X2),nand(X1,X0))),
inference(forward_demodulation,[],[f19756,f2492]) ).
fof(f25721,plain,
nand(nand(sF0,sF2),nand(b,b)) = nand(nand(sF0,sF2),nand(sF1,b)),
inference(superposition,[],[f3761,f15699]) ).
fof(f32269,plain,
sF5 = nand(sF4,nand(sF5,sF2)),
inference(superposition,[],[f2699,f2669]) ).
fof(f32367,plain,
sF5 = nand(sF4,nand(sF2,sF5)),
inference(forward_demodulation,[],[f32269,f2492]) ).
fof(f33536,plain,
! [X2,X0,X1] : nand(X0,nand(X0,X1)) = nand(nand(X1,X1),nand(nand(X0,X2),nand(X0,nand(X0,X1)))),
inference(superposition,[],[f3622,f4089]) ).
fof(f35222,plain,
nand(sF5,sF2) = nand(nand(sF2,nand(sF0,sF5)),nand(nand(sF5,sF2),a)),
inference(superposition,[],[f19584,f14542]) ).
fof(f35245,plain,
! [X0] : nand(sF2,X0) = nand(nand(a,nand(sF2,X0)),X0),
inference(superposition,[],[f2800,f19584]) ).
fof(f35332,plain,
! [X0] : nand(sF2,X0) = nand(X0,nand(a,nand(sF2,X0))),
inference(forward_demodulation,[],[f35245,f2492]) ).
fof(f35350,plain,
nand(sF5,sF2) = nand(nand(sF2,nand(sF0,sF5)),nand(a,nand(sF5,sF2))),
inference(forward_demodulation,[],[f35222,f2492]) ).
fof(f35428,plain,
nand(sF5,sF2) = nand(nand(a,nand(sF5,sF2)),nand(sF2,nand(sF0,sF5))),
inference(forward_demodulation,[],[f35350,f2492]) ).
fof(f35468,plain,
nand(sF2,sF5) = nand(nand(a,nand(sF2,sF5)),nand(sF2,nand(sF0,sF5))),
inference(forward_demodulation,[],[f35428,f2492]) ).
fof(f35615,plain,
nand(nand(sF2,sF5),nand(sF2,sF5)) = nand(a,nand(sF2,sF5)),
inference(superposition,[],[f3056,f35332]) ).
fof(f36112,plain,
a = nand(nand(sF3,a),nand(sF1,a)),
inference(superposition,[],[f2933,f6292]) ).
fof(f36420,plain,
a = nand(nand(sF1,a),nand(sF3,a)),
inference(forward_demodulation,[],[f36112,f2492]) ).
fof(f36484,plain,
a = nand(sF2,nand(sF3,a)),
inference(forward_demodulation,[],[f36420,f2669]) ).
fof(f36543,plain,
sF2 = nand(nand(sF3,sF2),a),
inference(superposition,[],[f2805,f36484]) ).
fof(f36623,plain,
sF2 = nand(a,nand(sF3,sF2)),
inference(forward_demodulation,[],[f36543,f2492]) ).
fof(f36665,plain,
sF2 = nand(nand(sF3,sF2),nand(sF5,sF2)),
inference(superposition,[],[f3056,f36623]) ).
fof(f36733,plain,
sF2 = nand(nand(sF3,sF2),nand(sF2,sF5)),
inference(forward_demodulation,[],[f36665,f2492]) ).
fof(f40951,plain,
! [X0] : nand(X0,nand(sF2,nand(sF1,nand(X0,X0)))) = nand(nand(sF2,nand(sF1,nand(X0,X0))),nand(sF1,nand(X0,X0))),
inference(superposition,[],[f4070,f2902]) ).
fof(f40963,plain,
! [X0] : nand(X0,nand(sF2,nand(sF1,nand(X0,X0)))) = nand(nand(sF1,nand(X0,X0)),nand(sF2,nand(sF1,nand(X0,X0)))),
inference(forward_demodulation,[],[f40951,f2492]) ).
fof(f41097,plain,
! [X0] : nand(X0,nand(sF2,nand(sF1,nand(X0,X0)))) = nand(nand(sF0,sF2),nand(sF1,nand(X0,X0))),
inference(forward_demodulation,[],[f40963,f4605]) ).
fof(f49052,plain,
! [X2,X0,X1] : nand(X2,X2) = nand(X2,nand(nand(X2,nand(X0,nand(X1,X0))),nand(nand(X1,X1),nand(X1,X1)))),
inference(superposition,[],[f3866,f3956]) ).
fof(f49306,plain,
! [X2,X0,X1] : nand(nand(X1,X0),nand(X1,X0)) = nand(nand(X1,X0),nand(X0,nand(nand(X2,X1),nand(X2,X1)))),
inference(superposition,[],[f3866,f3192]) ).
fof(f49796,plain,
! [X2,X0,X1] : nand(X2,X2) = nand(X2,nand(nand(X2,nand(X0,nand(X1,X0))),X1)),
inference(forward_demodulation,[],[f49052,f1316]) ).
fof(f49896,plain,
! [X2,X0,X1] : nand(X2,X2) = nand(X2,nand(X1,nand(X2,nand(X0,nand(X1,X0))))),
inference(forward_demodulation,[],[f49796,f2492]) ).
fof(f50155,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,sF4),nand(nand(sF1,sF1),nand(sF1,sF1)))),
inference(superposition,[],[f12195,f3996]) ).
fof(f50740,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(nand(X0,sF4),sF1)),
inference(forward_demodulation,[],[f50155,f1316]) ).
fof(f50879,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(sF1,nand(X0,sF4))),
inference(forward_demodulation,[],[f50740,f2492]) ).
fof(f50942,plain,
! [X0] : nand(X0,X0) = nand(X0,nand(sF1,nand(sF4,X0))),
inference(superposition,[],[f50879,f2492]) ).
fof(f53914,plain,
nand(nand(sF2,sF5),nand(sF2,sF5)) = nand(nand(sF2,sF5),nand(sF1,sF5)),
inference(superposition,[],[f50942,f32367]) ).
fof(f54310,plain,
nand(nand(sF2,sF5),nand(sF2,sF5)) = nand(nand(sF1,sF5),nand(sF2,sF5)),
inference(forward_demodulation,[],[f53914,f2492]) ).
fof(f54446,plain,
sF5 = nand(nand(sF2,sF5),nand(sF2,sF5)),
inference(forward_demodulation,[],[f54310,f15745]) ).
fof(f54533,plain,
sF5 = nand(a,nand(sF2,sF5)),
inference(backward_demodulation,[],[f35615,f54446]) ).
fof(f54593,plain,
nand(sF2,sF5) = nand(sF5,nand(sF2,nand(sF0,sF5))),
inference(backward_demodulation,[],[f35468,f54533]) ).
fof(f54640,plain,
nand(sF2,sF5) = nand(sF0,sF5),
inference(forward_demodulation,[],[f54593,f14537]) ).
fof(f54724,plain,
sF2 = nand(nand(sF3,sF2),nand(sF0,sF5)),
inference(backward_demodulation,[],[f36733,f54640]) ).
fof(f54797,plain,
sF2 = nand(nand(sF0,sF5),nand(sF3,sF2)),
inference(forward_demodulation,[],[f54724,f2492]) ).
fof(f64042,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X0,X1)) = nand(nand(X1,X0),nand(X0,X1)),
inference(superposition,[],[f3352,f3622]) ).
fof(f69043,plain,
! [X0] : nand(sF4,X0) = nand(X0,nand(sF5,nand(sF4,X0))),
inference(superposition,[],[f19840,f2699]) ).
fof(f73639,plain,
! [X0] : nand(nand(sF5,nand(sF4,X0)),nand(sF4,X0)) = nand(nand(sF5,nand(sF4,X0)),nand(X0,X0)),
inference(superposition,[],[f3761,f69043]) ).
fof(f73680,plain,
! [X0] : nand(nand(sF5,nand(sF4,X0)),nand(X0,X0)) = nand(nand(sF4,X0),nand(sF5,nand(sF4,X0))),
inference(forward_demodulation,[],[f73639,f2492]) ).
fof(f73859,plain,
! [X0] : nand(nand(sF0,sF5),nand(sF4,X0)) = nand(nand(sF5,nand(sF4,X0)),nand(X0,X0)),
inference(forward_demodulation,[],[f73680,f14545]) ).
fof(f75759,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X0,X1)) = nand(nand(X1,X0),nand(X0,nand(nand(X0,X1),nand(X0,X1)))),
inference(superposition,[],[f2769,f64042]) ).
fof(f75858,plain,
! [X0,X1] : nand(nand(X0,X1),nand(X0,X1)) = nand(nand(X1,X0),nand(X1,X0)),
inference(forward_demodulation,[],[f75759,f49306]) ).
fof(f76650,plain,
! [X2,X0,X1] : nand(X2,nand(X1,X0)) = nand(X2,nand(X2,nand(nand(X0,X1),nand(X0,X1)))),
inference(superposition,[],[f4514,f75858]) ).
fof(f76651,plain,
! [X2,X0,X1] : nand(nand(X1,X0),X2) = nand(X2,nand(X2,nand(nand(X0,X1),nand(X0,X1)))),
inference(superposition,[],[f4732,f75858]) ).
fof(f76738,plain,
! [X2,X0,X1] : nand(X2,nand(X0,X1)) = nand(nand(X1,X0),X2),
inference(forward_demodulation,[],[f76651,f4514]) ).
fof(f76739,plain,
! [X2,X0,X1] : nand(X2,nand(X0,X1)) = nand(X2,nand(X1,X0)),
inference(forward_demodulation,[],[f76650,f4514]) ).
fof(f77070,plain,
! [X2,X3,X0,X1] : nand(X3,nand(X0,nand(X1,X2))) = nand(X3,nand(nand(X2,X1),X0)),
inference(superposition,[],[f76739,f76739]) ).
fof(f77077,plain,
! [X2,X0,X1] : nand(X2,nand(X0,nand(X1,X0))) = nand(X2,nand(X0,nand(X1,X1))),
inference(superposition,[],[f76739,f3956]) ).
fof(f77903,plain,
! [X2,X0,X1] : nand(nand(X0,X0),nand(X2,X1)) = nand(nand(X2,X1),nand(X0,nand(X1,X2))),
inference(superposition,[],[f3956,f76739]) ).
fof(f78483,plain,
! [X2,X0,X1] : nand(nand(X0,nand(X1,X0)),X2) = nand(X2,nand(nand(X1,X1),X0)),
inference(superposition,[],[f76738,f3761]) ).
fof(f78568,plain,
! [X2,X3,X0,X1] : nand(nand(X0,nand(X1,X2)),X3) = nand(X3,nand(X0,nand(X2,X1))),
inference(superposition,[],[f76738,f76738]) ).
fof(f78786,plain,
! [X2,X3,X0,X1] : nand(nand(X0,X1),nand(X2,X3)) = nand(nand(X1,X0),nand(X3,X2)),
inference(superposition,[],[f76738,f76738]) ).
fof(f78908,plain,
! [X2,X0,X1] : nand(nand(X0,X1),X2) = nand(nand(X1,X0),X2),
inference(superposition,[],[f2492,f76738]) ).
fof(f78959,plain,
! [X2,X3,X0,X1] : nand(X3,nand(nand(X0,X1),X2)) = nand(X3,nand(nand(X1,X0),X2)),
inference(superposition,[],[f76739,f76738]) ).
fof(f79073,plain,
! [X2,X3,X0,X1] : nand(X3,nand(X0,nand(X1,X2))) = nand(X3,nand(X0,nand(X2,X1))),
inference(superposition,[],[f76739,f76738]) ).
fof(f79140,plain,
! [X2,X3,X0,X1] : nand(nand(X0,X1),nand(X2,X3)) = nand(nand(X3,X2),nand(X1,X0)),
inference(superposition,[],[f76739,f76738]) ).
fof(f85390,plain,
! [X2,X3,X0,X1] : nand(nand(X1,X0),nand(X3,nand(X2,X3))) = nand(nand(X0,X1),nand(nand(X2,X2),X3)),
inference(superposition,[],[f76738,f78483]) ).
fof(f96033,plain,
nand(sF2,nand(sF3,nand(c,nand(sF0,sF2)))) = nand(nand(sF3,nand(c,nand(sF0,sF2))),nand(c,nand(sF0,sF2))),
inference(superposition,[],[f5898,f7572]) ).
fof(f96405,plain,
nand(sF2,nand(sF3,nand(c,nand(sF0,sF2)))) = nand(nand(c,nand(sF0,sF2)),nand(sF3,nand(nand(sF0,sF2),c))),
inference(forward_demodulation,[],[f96033,f78568]) ).
fof(f96590,plain,
nand(sF2,nand(sF3,nand(c,nand(sF0,sF2)))) = nand(nand(sF3,sF3),nand(c,nand(sF0,sF2))),
inference(forward_demodulation,[],[f96405,f77903]) ).
fof(f96735,plain,
nand(nand(sF3,sF3),sF0) = nand(sF2,nand(sF3,sF0)),
inference(forward_demodulation,[],[f96590,f8167]) ).
fof(f96847,plain,
nand(nand(sF3,sF3),sF0) = nand(sF2,nand(sF0,sF3)),
inference(forward_demodulation,[],[f96735,f76739]) ).
fof(f96932,plain,
nand(sF2,nand(sF0,sF3)) = nand(sF0,nand(sF3,sF0)),
inference(forward_demodulation,[],[f96847,f3956]) ).
fof(f96992,plain,
nand(sF0,nand(sF0,sF3)) = nand(sF2,nand(sF0,sF3)),
inference(forward_demodulation,[],[f96932,f4542]) ).
fof(f97140,plain,
sF2 = nand(nand(sF0,sF2),nand(sF0,nand(sF0,sF3))),
inference(superposition,[],[f2805,f96992]) ).
fof(f110575,plain,
nand(sF5,nand(sF3,nand(c,nand(sF0,sF5)))) = nand(nand(sF3,nand(c,nand(sF0,sF5))),nand(c,nand(sF0,sF5))),
inference(superposition,[],[f14546,f7572]) ).
fof(f111007,plain,
nand(sF5,nand(sF3,nand(c,nand(sF0,sF5)))) = nand(nand(c,nand(sF0,sF5)),nand(sF3,nand(nand(sF0,sF5),c))),
inference(forward_demodulation,[],[f110575,f78568]) ).
fof(f111230,plain,
nand(sF5,nand(sF3,nand(c,nand(sF0,sF5)))) = nand(nand(sF3,sF3),nand(c,nand(sF0,sF5))),
inference(forward_demodulation,[],[f111007,f77903]) ).
fof(f111393,plain,
nand(nand(sF3,sF3),sF0) = nand(sF5,nand(sF3,sF0)),
inference(forward_demodulation,[],[f111230,f19041]) ).
fof(f111515,plain,
nand(nand(sF3,sF3),sF0) = nand(sF5,nand(sF0,sF3)),
inference(forward_demodulation,[],[f111393,f76739]) ).
fof(f111605,plain,
nand(sF0,nand(sF3,sF0)) = nand(sF5,nand(sF0,sF3)),
inference(forward_demodulation,[],[f111515,f3956]) ).
fof(f111667,plain,
nand(sF0,nand(sF0,sF3)) = nand(sF5,nand(sF0,sF3)),
inference(forward_demodulation,[],[f111605,f4542]) ).
fof(f111796,plain,
sF5 = nand(nand(sF0,sF5),nand(sF0,nand(sF0,sF3))),
inference(superposition,[],[f2805,f111667]) ).
fof(f113745,plain,
nand(sF0,sF5) = nand(nand(nand(sF0,sF5),sF3),sF2),
inference(superposition,[],[f1571,f54797]) ).
fof(f113882,plain,
nand(sF0,sF5) = nand(sF2,nand(sF3,nand(sF0,sF5))),
inference(forward_demodulation,[],[f113745,f76738]) ).
fof(f134934,plain,
! [X2,X3,X0,X1,X4] : nand(X4,nand(nand(X0,X1),nand(X2,X3))) = nand(X4,nand(nand(X3,X2),nand(X1,X0))),
inference(superposition,[],[f78959,f76738]) ).
fof(f134936,plain,
! [X2,X3,X0,X1,X4] : nand(X4,nand(nand(X0,X1),nand(X2,X3))) = nand(X4,nand(nand(X1,X0),nand(X3,X2))),
inference(superposition,[],[f78959,f76739]) ).
fof(f136110,plain,
! [X2,X3,X0,X1,X4] : nand(nand(X0,X1),nand(nand(X2,X3),X4)) = nand(nand(X1,X0),nand(nand(X3,X2),X4)),
inference(superposition,[],[f78908,f78959]) ).
fof(f155834,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(nand(sF2,b),nand(sF3,sF3))),
inference(superposition,[],[f4605,f3862]) ).
fof(f156025,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(nand(b,sF2),nand(sF3,sF3))),
inference(forward_demodulation,[],[f155834,f134936]) ).
fof(f156175,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(nand(sF3,sF3),nand(sF2,b))),
inference(forward_demodulation,[],[f156025,f134934]) ).
fof(f156292,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(nand(sF3,sF3),nand(b,sF2))),
inference(forward_demodulation,[],[f156175,f134936]) ).
fof(f156391,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(nand(sF3,sF3),sF1)),
inference(forward_demodulation,[],[f156292,f15651]) ).
fof(f156472,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(nand(sF0,sF2),nand(sF1,nand(sF3,sF3))),
inference(forward_demodulation,[],[f156391,f77070]) ).
fof(f156541,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(sF3,nand(sF2,nand(sF1,nand(sF3,sF3)))),
inference(forward_demodulation,[],[f156472,f41097]) ).
fof(f156603,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(sF3,nand(sF2,nand(sF1,nand(sF3,sF1)))),
inference(forward_demodulation,[],[f156541,f77077]) ).
fof(f156656,plain,
nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)) = nand(sF3,nand(sF2,nand(sF1,nand(sF1,sF3)))),
inference(forward_demodulation,[],[f156603,f79073]) ).
fof(f156699,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(nand(sF2,b),nand(sF3,sF3)),nand(sF2,sF2)),
inference(forward_demodulation,[],[f156656,f2726]) ).
fof(f156733,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(nand(sF2,b),nand(sF3,sF3))),
inference(forward_demodulation,[],[f156699,f78568]) ).
fof(f156762,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(nand(b,sF2),nand(sF3,sF3))),
inference(forward_demodulation,[],[f156733,f136110]) ).
fof(f156786,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(nand(sF3,sF3),nand(b,sF2))),
inference(forward_demodulation,[],[f156762,f78786]) ).
fof(f156806,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(nand(sF3,sF3),sF1)),
inference(forward_demodulation,[],[f156786,f15651]) ).
fof(f156820,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(sF1,nand(sF3,sF1))),
inference(forward_demodulation,[],[f156806,f85390]) ).
fof(f156832,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(sF1,nand(sF1,sF3))),
inference(forward_demodulation,[],[f156820,f79073]) ).
fof(f156844,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF2,sF2),nand(sF1,b)),
inference(forward_demodulation,[],[f156832,f2726]) ).
fof(f156855,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(b,sF1),nand(sF2,sF2)),
inference(forward_demodulation,[],[f156844,f79140]) ).
fof(f156864,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF1,b),nand(sF2,sF2)),
inference(forward_demodulation,[],[f156855,f78786]) ).
fof(f156868,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF1,b),nand(sF0,sF2)),
inference(forward_demodulation,[],[f156864,f3876]) ).
fof(f156872,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF0,sF2),nand(b,sF1)),
inference(forward_demodulation,[],[f156868,f76738]) ).
fof(f156875,plain,
nand(sF3,nand(sF2,nand(sF1,b))) = nand(nand(sF0,sF2),nand(sF1,b)),
inference(forward_demodulation,[],[f156872,f76739]) ).
fof(f156878,plain,
nand(sF3,nand(sF0,sF2)) = nand(nand(sF0,sF2),nand(sF1,b)),
inference(forward_demodulation,[],[f156875,f15762]) ).
fof(f156881,plain,
nand(sF3,nand(sF0,sF2)) = nand(nand(sF0,sF2),nand(b,b)),
inference(backward_demodulation,[],[f25721,f156878]) ).
fof(f208938,plain,
! [X0] : nand(nand(sF0,sF2),nand(a,X0)) = nand(nand(sF0,sF2),nand(X0,X0)),
inference(superposition,[],[f2767,f8174]) ).
fof(f209338,plain,
nand(nand(sF0,sF2),nand(a,b)) = nand(sF3,nand(sF0,sF2)),
inference(backward_demodulation,[],[f156881,f208938]) ).
fof(f209621,plain,
nand(a,nand(a,b)) = nand(sF3,nand(sF0,sF2)),
inference(backward_demodulation,[],[f9896,f209338]) ).
fof(f209851,plain,
nand(sF3,nand(sF0,sF2)) = nand(nand(sF0,sF5),nand(a,b)),
inference(backward_demodulation,[],[f14464,f209621]) ).
fof(f222069,plain,
! [X2,X0,X1] : nand(X1,nand(X0,nand(X2,nand(X1,X2)))) = nand(nand(X0,X0),nand(nand(X1,nand(X0,nand(X2,nand(X1,X2)))),nand(X1,nand(X0,nand(X2,nand(X1,X2)))))),
inference(superposition,[],[f1619,f49896]) ).
fof(f222186,plain,
! [X2,X0,X1] : nand(X1,nand(X0,nand(X2,nand(X1,X2)))) = nand(nand(X0,X0),nand(nand(X1,nand(X0,nand(X2,nand(X1,X2)))),nand(X1,nand(X1,X0)))),
inference(forward_demodulation,[],[f222069,f4311]) ).
fof(f222916,plain,
! [X2,X0,X1] : nand(X1,nand(X1,X0)) = nand(X1,nand(X0,nand(X2,nand(X1,X2)))),
inference(forward_demodulation,[],[f222186,f33536]) ).
fof(f231132,plain,
! [X0,X1] : nand(nand(sF0,sF5),nand(nand(sF0,sF5),X1)) = nand(nand(sF0,sF5),nand(X1,nand(sF5,X0))),
inference(superposition,[],[f222916,f14546]) ).
fof(f232233,plain,
! [X0,X1] : nand(nand(sF5,nand(X0,X1)),nand(X1,X1)) = nand(nand(sF0,sF5),nand(nand(sF0,sF5),X1)),
inference(backward_demodulation,[],[f14863,f231132]) ).
fof(f233052,plain,
! [X0] : nand(nand(sF0,sF5),nand(nand(sF0,sF5),X0)) = nand(nand(sF0,sF5),nand(a,X0)),
inference(backward_demodulation,[],[f19047,f232233]) ).
fof(f233053,plain,
! [X0] : nand(nand(sF0,sF5),nand(nand(sF0,sF5),X0)) = nand(nand(sF0,sF5),nand(sF4,X0)),
inference(backward_demodulation,[],[f73859,f232233]) ).
fof(f233613,plain,
! [X0] : nand(nand(sF0,sF5),nand(a,X0)) = nand(nand(sF0,sF5),nand(sF4,X0)),
inference(forward_demodulation,[],[f233052,f233053]) ).
fof(f233952,plain,
nand(sF3,nand(sF0,sF2)) = nand(nand(sF0,sF5),nand(sF4,b)),
inference(backward_demodulation,[],[f209851,f233613]) ).
fof(f234222,plain,
nand(sF3,nand(sF0,sF2)) = nand(nand(sF0,sF5),sF3),
inference(forward_demodulation,[],[f233952,f2341]) ).
fof(f234310,plain,
nand(sF3,nand(sF0,sF2)) = nand(sF3,nand(sF5,sF0)),
inference(forward_demodulation,[],[f234222,f76738]) ).
fof(f234367,plain,
nand(sF3,nand(sF0,sF2)) = nand(sF3,nand(sF0,sF5)),
inference(forward_demodulation,[],[f234310,f76739]) ).
fof(f234402,plain,
nand(sF0,sF5) = nand(sF2,nand(sF3,nand(sF0,sF2))),
inference(backward_demodulation,[],[f113882,f234367]) ).
fof(f234432,plain,
nand(sF0,sF2) = nand(sF0,sF5),
inference(forward_demodulation,[],[f234402,f4598]) ).
fof(f234766,plain,
sF5 = nand(nand(sF0,sF2),nand(sF0,nand(sF0,sF3))),
inference(backward_demodulation,[],[f111796,f234432]) ).
fof(f235382,plain,
sF2 = sF5,
inference(forward_demodulation,[],[f234766,f97140]) ).
fof(f237081,plain,
$false,
inference(forward_subsumption_resolution,[],[f235382,f15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO076-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n005.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 21:07:47 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 87.34/12.72 % (1178440)Detected a unit-equality problem, will run specialized UEQ schedule.
% 87.34/12.72 % (1178475)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1638370574:i=1187:sd=4:av=off:ss=axioms:sgt=32_3000 on theBenchmark for (3000ds/1187Mi)
% 87.34/12.72 % (1178472)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3485843881:i=136:bd=preordered:ins=2:av=off_3000 on theBenchmark for (3000ds/136Mi)
% 87.34/12.72 % (1178470)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3932041862:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/130792Mi)
% 87.34/12.72 % (1178474)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1017704112:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_3000 on theBenchmark for (3000ds/257Mi)
% 87.34/12.72 % (1178471)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=485436033:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_3000 on theBenchmark for (3000ds/130716Mi)
% 87.34/12.72 % (1178469)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=914160756:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_3000 on theBenchmark for (3000ds/138329Mi)
% 87.34/12.72 % (1178473)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2442489839:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_3000 on theBenchmark for (3000ds/181Mi)
% 87.34/12.72 % (1178472)Instruction limit reached!
% 87.34/12.72 % (1178472)------------------------------
% 87.34/12.72 % (1178472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.34/12.72 % (1178472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.34/12.72 % (1178472)CaDiCaL version: 2.1.3
% 87.34/12.72 % (1178472)Termination reason: Instruction limit
% 87.34/12.72 % (1178472)Termination phase: Saturation
% 87.34/12.72 % (1178472)Time elapsed: 0.077 s
% 87.34/12.72 % (1178472)Peak memory usage: 88 MB
% 87.34/12.72 % (1178472)Instructions burned: 137 (million)
% 87.34/12.72 % (1178473)Instruction limit reached!
% 87.34/12.72 % (1178473)------------------------------
% 87.34/12.72 % (1178473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.34/12.72 % (1178473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.34/12.72 % (1178473)CaDiCaL version: 2.1.3
% 87.34/12.72 % (1178473)Termination reason: Instruction limit
% 87.34/12.72 % (1178473)Termination phase: Saturation
% 87.34/12.72 % (1178473)Time elapsed: 0.096 s
% 87.34/12.72 % (1178473)Peak memory usage: 89 MB
% 87.34/12.72 % (1178473)Instructions burned: 182 (million)
% 87.34/12.72 % (1178474)Instruction limit reached!
% 87.34/12.72 % (1178474)------------------------------
% 87.34/12.72 % (1178474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.34/12.72 % (1178474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.34/12.72 % (1178474)CaDiCaL version: 2.1.3
% 87.34/12.72 % (1178474)Termination reason: Instruction limit
% 87.34/12.72 % (1178474)Termination phase: Saturation
% 87.34/12.72 % (1178474)Time elapsed: 0.161 s
% 87.34/12.72 % (1178474)Peak memory usage: 89 MB
% 87.34/12.72 % (1178474)Instructions burned: 258 (million)
% 87.34/12.72 % (1178525)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=906910169:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 87.34/12.72 % (1178526)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1110238463:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 87.34/12.72 % (1178527)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=1246516453:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 87.34/12.72 % (1178475)Instruction limit reached!
% 87.34/12.72 % (1178475)------------------------------
% 87.34/12.72 % (1178475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.34/12.72 % (1178475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.34/12.72 % (1178475)CaDiCaL version: 2.1.3
% 87.34/12.72 % (1178475)Termination reason: Instruction limit
% 87.34/12.72 % (1178475)Termination phase: Saturation
% 87.34/12.72 % (1178475)Time elapsed: 0.365 s
% 140.66/20.27 % (1178475)Peak memory usage: 98 MB
% 140.66/20.27 % (1178475)Instructions burned: 1188 (million)
% 140.66/20.27 % (1178527)Instruction limit reached!
% 140.66/20.27 % (1178527)------------------------------
% 140.66/20.27 % (1178527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.27 % (1178527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.27 % (1178527)CaDiCaL version: 2.1.3
% 140.66/20.27 % (1178527)Termination reason: Instruction limit
% 140.66/20.27 % (1178527)Termination phase: Saturation
% 140.66/20.27 % (1178527)Time elapsed: 0.090 s
% 140.66/20.27 % (1178527)Peak memory usage: 98 MB
% 140.66/20.27 % (1178527)Instructions burned: 217 (million)
% 140.66/20.27 % (1178531)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=3486270577:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 140.66/20.27 % (1178532)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=4107726793:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 140.66/20.27 % (1178531)Instruction limit reached!
% 140.66/20.27 % (1178531)------------------------------
% 140.66/20.27 % (1178531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.27 % (1178531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.27 % (1178531)CaDiCaL version: 2.1.3
% 140.66/20.27 % (1178531)Termination reason: Instruction limit
% 140.66/20.27 % (1178531)Termination phase: Saturation
% 140.66/20.27 % (1178531)Time elapsed: 0.104 s
% 140.66/20.27 % (1178531)Peak memory usage: 94 MB
% 140.66/20.27 % (1178531)Instructions burned: 320 (million)
% 140.66/20.27 % (1178535)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1745885895:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 140.66/20.27 % (1178525)Instruction limit reached!
% 140.66/20.27 % (1178525)------------------------------
% 140.66/20.27 % (1178525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.27 % (1178525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.27 % (1178525)CaDiCaL version: 2.1.3
% 140.66/20.27 % (1178525)Termination reason: Instruction limit
% 140.66/20.27 % (1178525)Termination phase: Saturation
% 140.66/20.27 % (1178525)Time elapsed: 1.295 s
% 140.66/20.27 % (1178525)Peak memory usage: 140 MB
% 140.66/20.27 % (1178525)Instructions burned: 2051 (million)
% 140.66/20.27 % (1178535)Instruction limit reached!
% 140.66/20.27 % (1178535)------------------------------
% 140.66/20.27 % (1178535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.27 % (1178535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.27 % (1178535)CaDiCaL version: 2.1.3
% 140.66/20.27 % (1178535)Termination reason: Instruction limit
% 140.66/20.27 % (1178535)Termination phase: Saturation
% 140.66/20.27 % (1178535)Time elapsed: 0.978 s
% 140.66/20.27 % (1178535)Peak memory usage: 123 MB
% 140.66/20.27 % (1178535)Instructions burned: 2838 (million)
% 140.66/20.27 % (1178537)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=483767458:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 140.66/20.27 % (1178538)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1588135986:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/11832Mi)
% 140.66/20.27 % (1178526)Instruction limit reached!
% 140.66/20.27 % (1178526)------------------------------
% 140.66/20.27 % (1178526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 140.66/20.27 % (1178526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 140.66/20.27 % (1178526)CaDiCaL version: 2.1.3
% 140.66/20.27 % (1178526)Termination reason: Instruction limit
% 140.66/20.27 % (1178526)Termination phase: Saturation
% 140.66/20.27 % (1178526)Time elapsed: 3.076 s
% 140.66/20.27 % (1178526)Peak memory usage: 161 MB
% 140.66/20.27 % (1178526)Instructions burned: 4949 (million)
% 140.66/20.27 % (1178541)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=3562054465:i=2279:fgj=on:bd=all_2965 on theBenchmark for (2965ds/2279Mi)
% 140.66/20.27 % (1178541)Instruction limit reached!
% 140.66/20.27 % (1178541)------------------------------
% 100.90/23.34 % (1178541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178541)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178541)Termination reason: Instruction limit
% 100.90/23.34 % (1178541)Termination phase: Saturation
% 100.90/23.34 % (1178541)Time elapsed: 1.399 s
% 100.90/23.34 % (1178541)Peak memory usage: 138 MB
% 100.90/23.34 % (1178541)Instructions burned: 2280 (million)
% 100.90/23.34 % (1178543)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3134674887:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2950 on theBenchmark for (2950ds/6225Mi)
% 100.90/23.34 % (1178538)Instruction limit reached!
% 100.90/23.34 % (1178538)------------------------------
% 100.90/23.34 % (1178538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178538)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178538)Termination reason: Instruction limit
% 100.90/23.34 % (1178538)Termination phase: Saturation
% 100.90/23.34 % (1178538)Time elapsed: 4.077 s
% 100.90/23.34 % (1178538)Peak memory usage: 205 MB
% 100.90/23.34 % (1178538)Instructions burned: 11832 (million)
% 100.90/23.34 % (1178545)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=1486532304:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2941 on theBenchmark for (2941ds/21755Mi)
% 100.90/23.34 % (1178532)Instruction limit reached!
% 100.90/23.34 % (1178532)------------------------------
% 100.90/23.34 % (1178532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178532)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178532)Termination reason: Instruction limit
% 100.90/23.34 % (1178532)Termination phase: Saturation
% 100.90/23.34 % (1178532)Time elapsed: 7.504 s
% 100.90/23.34 % (1178532)Peak memory usage: 225 MB
% 100.90/23.34 % (1178532)Instructions burned: 12126 (million)
% 100.90/23.34 % (1178547)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=494110638:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2918 on theBenchmark for (2918ds/16427Mi)
% 100.90/23.34 % (1178543)Instruction limit reached!
% 100.90/23.34 % (1178543)------------------------------
% 100.90/23.34 % (1178543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178543)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178543)Termination reason: Instruction limit
% 100.90/23.34 % (1178543)Termination phase: Saturation
% 100.90/23.34 % (1178543)Time elapsed: 3.595 s
% 100.90/23.34 % (1178543)Peak memory usage: 156 MB
% 100.90/23.34 % (1178543)Instructions burned: 6225 (million)
% 100.90/23.34 % (1178549)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=952324229:i=9356:fgj=on:bd=preordered:av=off_2912 on theBenchmark for (2912ds/9356Mi)
% 100.90/23.34 % (1178537)Instruction limit reached!
% 100.90/23.34 % (1178537)------------------------------
% 100.90/23.34 % (1178537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178537)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178537)Termination reason: Instruction limit
% 100.90/23.34 % (1178537)Termination phase: Saturation
% 100.90/23.34 % (1178537)Time elapsed: 9.188 s
% 100.90/23.34 % (1178537)Peak memory usage: 220 MB
% 100.90/23.34 % (1178537)Instructions burned: 14534 (million)
% 100.90/23.34 % (1178551)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=640177182:i=2070:kws=inv_precedence:slsql=off:bd=all_2890 on theBenchmark for (2890ds/2070Mi)
% 100.90/23.34 % (1178551)Instruction limit reached!
% 100.90/23.34 % (1178551)------------------------------
% 100.90/23.34 % (1178551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178551)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178551)Termination reason: Instruction limit
% 100.90/23.34 % (1178551)Termination phase: Saturation
% 100.90/23.34 % (1178551)Time elapsed: 1.194 s
% 100.90/23.34 % (1178551)Peak memory usage: 129 MB
% 100.90/23.34 % (1178551)Instructions burned: 2070 (million)
% 100.90/23.34 % (1178553)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=3390778694:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2876 on theBenchmark for (2876ds/6461Mi)
% 100.90/23.34 % (1178545)Instruction limit reached!
% 100.90/23.34 % (1178545)------------------------------
% 100.90/23.34 % (1178545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178545)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178545)Termination reason: Instruction limit
% 100.90/23.34 % (1178545)Termination phase: Saturation
% 100.90/23.34 % (1178545)Time elapsed: 7.564 s
% 100.90/23.34 % (1178545)Peak memory usage: 287 MB
% 100.90/23.34 % (1178545)Instructions burned: 21759 (million)
% 100.90/23.34 % (1178773)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=1525045306:i=2310:bd=all:ss=included_2864 on theBenchmark for (2864ds/2310Mi)
% 100.90/23.34 % (1178773)Instruction limit reached!
% 100.90/23.34 % (1178773)------------------------------
% 100.90/23.34 % (1178773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178773)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178773)Termination reason: Instruction limit
% 100.90/23.34 % (1178773)Termination phase: Saturation
% 100.90/23.34 % (1178773)Time elapsed: 1.201 s
% 100.90/23.34 % (1178773)Peak memory usage: 115 MB
% 100.90/23.34 % (1178773)Instructions burned: 2311 (million)
% 100.90/23.34 % (1178816)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=1663983333:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2851 on theBenchmark for (2851ds/2616Mi)
% 100.90/23.34 % (1178549)Instruction limit reached!
% 100.90/23.34 % (1178549)------------------------------
% 100.90/23.34 % (1178549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178549)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178549)Termination reason: Instruction limit
% 100.90/23.34 % (1178549)Termination phase: Saturation
% 100.90/23.34 % (1178549)Time elapsed: 6.333 s
% 100.90/23.34 % (1178549)Peak memory usage: 179 MB
% 100.90/23.34 % (1178549)Instructions burned: 9356 (million)
% 100.90/23.34 % (1178818)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2464707980:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2847 on theBenchmark for (2847ds/30521Mi)
% 100.90/23.34 % (1178816)Instruction limit reached!
% 100.90/23.34 % (1178816)------------------------------
% 100.90/23.34 % (1178816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178816)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178816)Termination reason: Instruction limit
% 100.90/23.34 % (1178816)Termination phase: Saturation
% 100.90/23.34 % (1178816)Time elapsed: 1.215 s
% 100.90/23.34 % (1178816)Peak memory usage: 108 MB
% 100.90/23.34 % (1178816)Instructions burned: 2616 (million)
% 100.90/23.34 % (1178820)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=4027610979:i=3258:fgj=on:bd=all:ins=1_2837 on theBenchmark for (2837ds/3258Mi)
% 100.90/23.34 % (1178553)Instruction limit reached!
% 100.90/23.34 % (1178553)------------------------------
% 100.90/23.34 % (1178553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178553)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178553)Termination reason: Instruction limit
% 100.90/23.34 % (1178553)Termination phase: Saturation
% 100.90/23.34 % (1178553)Time elapsed: 5.833 s
% 100.90/23.34 % (1178553)Peak memory usage: 179 MB
% 100.90/23.34 % (1178553)Instructions burned: 6462 (million)
% 100.90/23.34 % (1178822)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=1655359799:i=5037:kws=precedence_2817 on theBenchmark for (2817ds/5037Mi)
% 100.90/23.34 % (1178820)Instruction limit reached!
% 100.90/23.34 % (1178820)------------------------------
% 100.90/23.34 % (1178820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178820)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178820)Termination reason: Instruction limit
% 100.90/23.34 % (1178820)Termination phase: Saturation
% 100.90/23.34 % (1178820)Time elapsed: 3.352 s
% 100.90/23.34 % (1178820)Peak memory usage: 151 MB
% 100.90/23.34 % (1178820)Instructions burned: 3258 (million)
% 100.90/23.34 % (1178824)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=1519652760:i=65240_2801 on theBenchmark for (2801ds/65240Mi)
% 100.90/23.34 % (1178547)Instruction limit reached!
% 100.90/23.34 % (1178547)------------------------------
% 100.90/23.34 % (1178547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/23.34 % (1178547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/23.34 % (1178547)CaDiCaL version: 2.1.3
% 100.90/23.34 % (1178547)Termination reason: Instruction limit
% 100.90/23.34 % (1178547)Termination phase: Saturation
% 100.90/23.34 % (1178547)Time elapsed: 13.032 s
% 100.90/23.34 % (1178547)Peak memory usage: 197 MB
% 100.90/23.34 % (1178547)Instructions burned: 16427 (million)
% 100.90/23.34 % (1178826)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=1105442573:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2786 on theBenchmark for (2786ds/16502Mi)
% 100.90/23.34 % (1178471)First to succeed.
% 100.90/23.34 % (1178471)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1178440"
% 100.90/23.34 % (1178471)Refutation found. Thanks to Tanya!
% 100.90/23.34 % SZS status Unsatisfiable for theBenchmark
% 100.90/23.34 % SZS output start Proof for theBenchmark
% See solution above
% 162.80/23.54 % (1178471)------------------------------
% 162.80/23.54 % (1178471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.80/23.54 % (1178471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.80/23.54 % (1178471)CaDiCaL version: 2.1.3
% 162.80/23.54 % (1178471)Termination reason: Refutation
% 162.80/23.54 % (1178471)Time elapsed: 22.253 s
% 162.80/23.54 % (1178471)Peak memory usage: 293 MB
% 162.80/23.54 % (1178471)Instructions burned: 29903 (million)
% 162.80/23.54 % (1178471)------------------------------
% 162.80/23.54 % (1178471)------------------------------
% 162.80/23.54 % (1178440)Success in time 22.912 s
% 162.80/23.54 % Vampire exiting
%------------------------------------------------------------------------------