%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 10:19:58 AM UTC 2026
% Result : Unsatisfiable 13.64s 2.78s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 53
% Syntax : Number of formulae : 398 ( 398 unt; 17 def)
% Number of atoms : 398 ( 383 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 41 ( 41 usr; 36 con; 0-2 aty)
% Number of variables : 152 ( 152 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : and(X0,n1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_definition2) ).
fof(f5,axiom,
! [X0] : or(X0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_definition2) ).
fof(f6,plain,
! [X0] : n1 = or(X0,n1),
inference(reorient_equations,[],[f5]) ).
fof(f11,axiom,
! [X0,X1] : and(X0,X1) = and(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutativity) ).
fof(f12,axiom,
! [X0,X1] : or(X0,X1) = or(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutativity) ).
fof(f13,axiom,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(and(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_associativity) ).
fof(f14,axiom,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(or(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_associativity) ).
fof(f15,axiom,
! [X2,X0,X1] : or(or(X0,X1),X2) = or(or(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_sorting) ).
fof(f17,axiom,
! [X0,X1] : not(and(X0,X1)) = or(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization1) ).
fof(f18,axiom,
! [X0,X1] : not(or(X0,X1)) = and(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization2) ).
fof(f19,axiom,
! [X2,X0,X1] : and(or(X0,X1),X2) = or(and(X0,X2),and(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_canonicalization) ).
fof(f20,axiom,
! [X0] : and(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification1) ).
fof(f23,axiom,
! [X0,X1] : and(and(X0,X1),X0) = and(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification3) ).
fof(f24,plain,
! [X0,X1] : and(X0,X1) = and(and(X0,X1),X0),
inference(reorient_equations,[],[f23]) ).
fof(f28,axiom,
! [X0,X1] : or(or(X0,X1),X0) = or(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_simplification3) ).
fof(f29,plain,
! [X0,X1] : or(X0,X1) = or(or(X0,X1),X0),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
! [X0] : and(X0,not(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification1) ).
fof(f31,plain,
! [X0] : n0 = and(X0,not(X0)),
inference(reorient_equations,[],[f30]) ).
fof(f36,axiom,
! [X0] : or(X0,not(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification1) ).
fof(f37,plain,
! [X0] : n1 = or(X0,not(X0)),
inference(reorient_equations,[],[f36]) ).
fof(f40,axiom,
! [X0,X1] : or(or(X0,X1),not(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification3) ).
fof(f41,plain,
! [X0,X1] : n1 = or(or(X0,X1),not(X0)),
inference(reorient_equations,[],[f40]) ).
fof(f42,axiom,
! [X0] : not(not(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_simplification) ).
fof(f43,axiom,
! [X0,X1] : or(and(X0,X1),and(X0,not(X1))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification1) ).
fof(f44,axiom,
! [X0,X1] : or(and(X0,X1),and(X1,not(X0))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification2) ).
fof(f45,negated_conjecture,
a1 = and(b1,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor1) ).
fof(f46,negated_conjecture,
a2 = and(b2,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor2) ).
fof(f47,negated_conjecture,
b1 = not(d1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor3) ).
fof(f48,negated_conjecture,
b2 = not(d2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor4) ).
fof(f49,negated_conjecture,
b3 = or(c1,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor5) ).
fof(f50,negated_conjecture,
c1 = or(d1,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor6) ).
fof(f51,negated_conjecture,
c2 = or(d2,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor7) ).
fof(f52,negated_conjecture,
d3 = f3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor8) ).
fof(f53,negated_conjecture,
d1 = not(e1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor9) ).
fof(f54,negated_conjecture,
d2 = not(e2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor10) ).
fof(f55,negated_conjecture,
e1 = or(f1,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor11) ).
fof(f56,negated_conjecture,
e2 = or(f2,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor12) ).
fof(f57,negated_conjecture,
f1 = not(i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor13) ).
fof(f58,negated_conjecture,
f2 = not(i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor14) ).
fof(f59,negated_conjecture,
f3 = and(i1,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor15) ).
fof(f60,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit_description) ).
fof(f61,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_interchange) ).
fof(f62,plain,
c1 = or(d1,f3),
inference(definition_unfolding,[],[f50,f52]) ).
fof(f63,plain,
c2 = or(d2,f3),
inference(definition_unfolding,[],[f51,f52]) ).
fof(f64,definition,
sF0 = and(b1,b3),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f65,plain,
and(b1,b3) = sF0,
inference(reorient_equations,[],[f64]) ).
fof(f66,plain,
a1 = sF0,
inference(definition_folding,[],[f45,f65]) ).
fof(f67,definition,
sF1 = and(b2,b3),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f68,plain,
and(b2,b3) = sF1,
inference(reorient_equations,[],[f67]) ).
fof(f69,plain,
a2 = sF1,
inference(definition_folding,[],[f46,f68]) ).
fof(f70,definition,
sF2 = not(d1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f71,plain,
not(d1) = sF2,
inference(reorient_equations,[],[f70]) ).
fof(f72,plain,
b1 = sF2,
inference(definition_folding,[],[f47,f71]) ).
fof(f73,definition,
sF3 = not(d2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f74,plain,
not(d2) = sF3,
inference(reorient_equations,[],[f73]) ).
fof(f75,plain,
b2 = sF3,
inference(definition_folding,[],[f48,f74]) ).
fof(f76,definition,
sF4 = or(c1,c2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f77,plain,
or(c1,c2) = sF4,
inference(reorient_equations,[],[f76]) ).
fof(f78,plain,
b3 = sF4,
inference(definition_folding,[],[f49,f77]) ).
fof(f79,definition,
sF5 = or(d1,f3),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f80,plain,
or(d1,f3) = sF5,
inference(reorient_equations,[],[f79]) ).
fof(f81,plain,
c1 = sF5,
inference(definition_folding,[],[f62,f80]) ).
fof(f82,definition,
sF6 = or(d2,f3),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f83,plain,
or(d2,f3) = sF6,
inference(reorient_equations,[],[f82]) ).
fof(f84,plain,
c2 = sF6,
inference(definition_folding,[],[f63,f83]) ).
fof(f85,definition,
sF7 = not(e1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f86,plain,
not(e1) = sF7,
inference(reorient_equations,[],[f85]) ).
fof(f87,plain,
d1 = sF7,
inference(definition_folding,[],[f53,f86]) ).
fof(f88,definition,
sF8 = not(e2),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f89,plain,
not(e2) = sF8,
inference(reorient_equations,[],[f88]) ).
fof(f90,plain,
d2 = sF8,
inference(definition_folding,[],[f54,f89]) ).
fof(f91,definition,
sF9 = or(f1,f3),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f92,plain,
or(f1,f3) = sF9,
inference(reorient_equations,[],[f91]) ).
fof(f93,plain,
e1 = sF9,
inference(definition_folding,[],[f55,f92]) ).
fof(f94,definition,
sF10 = or(f2,f3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f95,plain,
or(f2,f3) = sF10,
inference(reorient_equations,[],[f94]) ).
fof(f96,plain,
e2 = sF10,
inference(definition_folding,[],[f56,f95]) ).
fof(f97,definition,
sF11 = not(i1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f98,plain,
not(i1) = sF11,
inference(reorient_equations,[],[f97]) ).
fof(f99,plain,
f1 = sF11,
inference(definition_folding,[],[f57,f98]) ).
fof(f100,definition,
sF12 = not(i2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f101,plain,
not(i2) = sF12,
inference(reorient_equations,[],[f100]) ).
fof(f102,plain,
f2 = sF12,
inference(definition_folding,[],[f58,f101]) ).
fof(f103,definition,
sF13 = and(i1,i2),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f104,plain,
and(i1,i2) = sF13,
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
f3 = sF13,
inference(definition_folding,[],[f59,f104]) ).
fof(f106,definition,
sF14 = input(i1,i2),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f107,plain,
input(i1,i2) = sF14,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF15 = output(a1,a2),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f109,plain,
output(a1,a2) = sF15,
inference(reorient_equations,[],[f108]) ).
fof(f110,plain,
circuit(sF14,sF15),
inference(definition_folding,[],[f60,f109,f107]) ).
fof(f111,definition,
sF16 = output(i2,i1),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f112,plain,
output(i2,i1) = sF16,
inference(reorient_equations,[],[f111]) ).
fof(f113,plain,
~ circuit(sF14,sF16),
inference(definition_folding,[],[f61,f112,f107]) ).
fof(f114,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X1,X0)),
inference(backward_demodulation,[],[f29,f14]) ).
fof(f116,plain,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(or(X0,X2),X1),
inference(backward_demodulation,[],[f15,f14]) ).
fof(f117,plain,
! [X0,X1] : n1 = or(X0,or(X1,not(X0))),
inference(backward_demodulation,[],[f41,f14]) ).
fof(f119,plain,
! [X0,X1] : and(X0,X1) = and(X0,and(X1,X0)),
inference(backward_demodulation,[],[f24,f13]) ).
fof(f124,plain,
a1 = and(b1,b3),
inference(forward_demodulation,[],[f65,f66]) ).
fof(f125,plain,
a2 = and(b2,b3),
inference(forward_demodulation,[],[f68,f69]) ).
fof(f126,plain,
b1 = not(d1),
inference(forward_demodulation,[],[f71,f72]) ).
fof(f127,plain,
b2 = not(d2),
inference(forward_demodulation,[],[f74,f75]) ).
fof(f128,plain,
b3 = or(c1,c2),
inference(forward_demodulation,[],[f77,f78]) ).
fof(f129,plain,
c1 = or(d1,f3),
inference(forward_demodulation,[],[f80,f81]) ).
fof(f130,plain,
c2 = or(d2,f3),
inference(forward_demodulation,[],[f83,f84]) ).
fof(f131,plain,
d1 = not(e1),
inference(forward_demodulation,[],[f86,f87]) ).
fof(f132,plain,
d2 = not(e2),
inference(forward_demodulation,[],[f89,f90]) ).
fof(f133,plain,
e1 = or(f1,f3),
inference(forward_demodulation,[],[f92,f93]) ).
fof(f134,plain,
e2 = or(f2,f3),
inference(forward_demodulation,[],[f95,f96]) ).
fof(f135,plain,
f1 = not(i1),
inference(forward_demodulation,[],[f98,f99]) ).
fof(f136,plain,
f2 = not(i2),
inference(forward_demodulation,[],[f101,f102]) ).
fof(f137,plain,
f3 = and(i1,i2),
inference(forward_demodulation,[],[f104,f105]) ).
fof(f138,plain,
circuit(input(i1,i2),sF15),
inference(backward_demodulation,[],[f110,f107]) ).
fof(f139,plain,
~ circuit(input(i1,i2),sF16),
inference(backward_demodulation,[],[f113,f107]) ).
fof(f142,plain,
circuit(input(i1,i2),output(a1,a2)),
inference(forward_demodulation,[],[f138,f109]) ).
fof(f147,plain,
i1 = or(f3,and(i1,not(i2))),
inference(superposition,[],[f43,f137]) ).
fof(f150,plain,
i1 = or(f3,and(i1,f2)),
inference(forward_demodulation,[],[f147,f136]) ).
fof(f152,plain,
i1 = or(f3,and(f2,i1)),
inference(forward_demodulation,[],[f150,f11]) ).
fof(f166,plain,
! [X0,X1] : or(and(X0,X1),and(not(X0),X1)) = X1,
inference(superposition,[],[f44,f11]) ).
fof(f167,plain,
! [X0,X1] : and(or(X0,not(X0)),X1) = X1,
inference(forward_demodulation,[],[f166,f19]) ).
fof(f169,plain,
! [X1] : and(n1,X1) = X1,
inference(forward_demodulation,[],[f167,f37]) ).
fof(f189,plain,
! [X0] : or(n0,and(X0,not(not(X0)))) = X0,
inference(superposition,[],[f43,f31]) ).
fof(f192,plain,
! [X0] : or(n0,and(X0,X0)) = X0,
inference(forward_demodulation,[],[f189,f42]) ).
fof(f197,plain,
! [X0] : or(n0,X0) = X0,
inference(forward_demodulation,[],[f192,f20]) ).
fof(f200,plain,
n0 = and(i1,f1),
inference(superposition,[],[f31,f135]) ).
fof(f201,plain,
n1 = or(i1,f1),
inference(superposition,[],[f37,f135]) ).
fof(f206,plain,
n1 = or(f1,i1),
inference(forward_demodulation,[],[f201,f12]) ).
fof(f207,plain,
n0 = and(f1,i1),
inference(forward_demodulation,[],[f200,f11]) ).
fof(f222,plain,
or(c2,c1) = or(c2,b3),
inference(superposition,[],[f114,f128]) ).
fof(f223,plain,
or(f3,d1) = or(f3,c1),
inference(superposition,[],[f114,f129]) ).
fof(f224,plain,
or(f3,d2) = or(f3,c2),
inference(superposition,[],[f114,f130]) ).
fof(f225,plain,
or(f3,f1) = or(f3,e1),
inference(superposition,[],[f114,f133]) ).
fof(f226,plain,
or(f3,f2) = or(f3,e2),
inference(superposition,[],[f114,f134]) ).
fof(f227,plain,
or(f3,f2) = or(e2,f3),
inference(forward_demodulation,[],[f226,f12]) ).
fof(f228,plain,
or(f3,f1) = or(e1,f3),
inference(forward_demodulation,[],[f225,f12]) ).
fof(f229,plain,
or(f3,d2) = or(c2,f3),
inference(forward_demodulation,[],[f224,f12]) ).
fof(f230,plain,
or(f3,d1) = or(c1,f3),
inference(forward_demodulation,[],[f223,f12]) ).
fof(f231,plain,
or(c1,c2) = or(c2,b3),
inference(forward_demodulation,[],[f222,f12]) ).
fof(f236,plain,
or(f2,f3) = or(e2,f3),
inference(forward_demodulation,[],[f227,f12]) ).
fof(f237,plain,
or(f1,f3) = or(e1,f3),
inference(forward_demodulation,[],[f228,f12]) ).
fof(f238,plain,
or(d2,f3) = or(c2,f3),
inference(forward_demodulation,[],[f229,f12]) ).
fof(f239,plain,
or(d1,f3) = or(c1,f3),
inference(forward_demodulation,[],[f230,f12]) ).
fof(f240,plain,
b3 = or(c2,b3),
inference(forward_demodulation,[],[f231,f128]) ).
fof(f245,plain,
e2 = or(e2,f3),
inference(forward_demodulation,[],[f236,f134]) ).
fof(f246,plain,
e1 = or(e1,f3),
inference(forward_demodulation,[],[f237,f133]) ).
fof(f247,plain,
c2 = or(c2,f3),
inference(forward_demodulation,[],[f238,f130]) ).
fof(f248,plain,
c1 = or(c1,f3),
inference(forward_demodulation,[],[f239,f129]) ).
fof(f254,plain,
d1 = not(b1),
inference(superposition,[],[f42,f126]) ).
fof(f255,plain,
d2 = not(b2),
inference(superposition,[],[f42,f127]) ).
fof(f256,plain,
not(d1) = e1,
inference(superposition,[],[f42,f131]) ).
fof(f257,plain,
not(d2) = e2,
inference(superposition,[],[f42,f132]) ).
fof(f258,plain,
i1 = not(f1),
inference(superposition,[],[f42,f135]) ).
fof(f259,plain,
i2 = not(f2),
inference(superposition,[],[f42,f136]) ).
fof(f268,plain,
b2 = e2,
inference(forward_demodulation,[],[f257,f127]) ).
fof(f269,plain,
b1 = e1,
inference(forward_demodulation,[],[f256,f126]) ).
fof(f274,plain,
b2 = or(f2,f3),
inference(backward_demodulation,[],[f134,f268]) ).
fof(f279,plain,
b2 = or(b2,f3),
inference(backward_demodulation,[],[f245,f268]) ).
fof(f282,plain,
b1 = or(f1,f3),
inference(backward_demodulation,[],[f133,f269]) ).
fof(f287,plain,
b1 = or(b1,f3),
inference(backward_demodulation,[],[f246,f269]) ).
fof(f316,plain,
and(i2,i1) = and(i2,f3),
inference(superposition,[],[f119,f137]) ).
fof(f320,plain,
and(i1,i2) = and(i2,f3),
inference(forward_demodulation,[],[f316,f11]) ).
fof(f326,plain,
f3 = and(i2,f3),
inference(forward_demodulation,[],[f320,f137]) ).
fof(f378,plain,
! [X0,X1] : or(X0,not(X1)) = not(and(not(X0),X1)),
inference(superposition,[],[f17,f42]) ).
fof(f383,plain,
! [X0,X1] : not(and(X1,not(X0))) = or(not(X1),X0),
inference(superposition,[],[f17,f42]) ).
fof(f387,plain,
! [X0] : not(and(X0,i2)) = or(not(X0),f2),
inference(superposition,[],[f17,f136]) ).
fof(f400,plain,
! [X0] : or(f2,not(X0)) = not(and(X0,i2)),
inference(forward_demodulation,[],[f387,f12]) ).
fof(f405,plain,
! [X0,X1] : and(X0,not(X1)) = not(or(not(X0),X1)),
inference(superposition,[],[f18,f42]) ).
fof(f410,plain,
! [X0,X1] : and(not(X1),X0) = not(or(X1,not(X0))),
inference(superposition,[],[f18,f42]) ).
fof(f411,plain,
! [X0] : not(or(X0,d1)) = and(not(X0),b1),
inference(superposition,[],[f18,f126]) ).
fof(f412,plain,
! [X0] : not(or(X0,d2)) = and(not(X0),b2),
inference(superposition,[],[f18,f127]) ).
fof(f437,plain,
! [X0] : and(b2,not(X0)) = not(or(X0,d2)),
inference(forward_demodulation,[],[f412,f11]) ).
fof(f438,plain,
! [X0] : and(b1,not(X0)) = not(or(X0,d1)),
inference(forward_demodulation,[],[f411,f11]) ).
fof(f487,plain,
! [X0,X1] : or(X0,and(X1,X0)) = and(or(X0,X1),X0),
inference(superposition,[],[f19,f20]) ).
fof(f492,plain,
! [X0,X1] : and(or(X0,X1),not(X0)) = or(n0,and(X1,not(X0))),
inference(superposition,[],[f19,f31]) ).
fof(f498,plain,
! [X0,X1] : and(or(X1,n1),X0) = or(and(X1,X0),X0),
inference(superposition,[],[f19,f169]) ).
fof(f499,plain,
! [X0,X1] : or(and(X1,X0),X0) = and(or(X1,X0),X0),
inference(superposition,[],[f19,f20]) ).
fof(f504,plain,
! [X0,X1] : and(or(X0,X1),not(X1)) = or(and(X0,not(X1)),n0),
inference(superposition,[],[f19,f31]) ).
fof(f527,plain,
! [X0,X1] : and(or(X0,X1),not(X1)) = or(n0,and(X0,not(X1))),
inference(forward_demodulation,[],[f504,f12]) ).
fof(f533,plain,
! [X0,X1] : or(and(X1,X0),X0) = and(X0,or(X1,X0)),
inference(forward_demodulation,[],[f499,f11]) ).
fof(f534,plain,
! [X0,X1] : or(X0,and(X1,X0)) = and(or(X1,n1),X0),
inference(forward_demodulation,[],[f498,f12]) ).
fof(f539,plain,
! [X0,X1] : and(X1,not(X0)) = and(or(X0,X1),not(X0)),
inference(forward_demodulation,[],[f492,f197]) ).
fof(f546,plain,
! [X0,X1] : or(X0,and(X1,X0)) = and(X0,or(X0,X1)),
inference(forward_demodulation,[],[f487,f11]) ).
fof(f554,plain,
! [X0,X1] : and(X0,not(X1)) = and(or(X0,X1),not(X1)),
inference(forward_demodulation,[],[f527,f197]) ).
fof(f558,plain,
! [X0,X1] : or(X0,and(X1,X0)) = and(X0,or(X1,X0)),
inference(forward_demodulation,[],[f533,f12]) ).
fof(f559,plain,
! [X0,X1] : and(n1,X0) = or(X0,and(X1,X0)),
inference(forward_demodulation,[],[f534,f6]) ).
fof(f561,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(X0,X1)),
inference(forward_demodulation,[],[f539,f11]) ).
fof(f567,plain,
! [X0,X1] : and(X0,not(X1)) = and(not(X1),or(X0,X1)),
inference(forward_demodulation,[],[f554,f11]) ).
fof(f568,plain,
! [X0,X1] : or(X0,and(X1,X0)) = X0,
inference(forward_demodulation,[],[f559,f169]) ).
fof(f570,plain,
! [X0,X1] : and(X0,or(X1,X0)) = X0,
inference(backward_demodulation,[],[f558,f568]) ).
fof(f571,plain,
! [X0,X1] : and(X0,or(X0,X1)) = X0,
inference(backward_demodulation,[],[f546,f568]) ).
fof(f628,plain,
! [X0,X1] : or(X0,or(X1,not(X0))) = or(n1,X1),
inference(superposition,[],[f116,f37]) ).
fof(f634,plain,
! [X0] : or(b2,X0) = or(f2,or(X0,f3)),
inference(superposition,[],[f116,f274]) ).
fof(f658,plain,
! [X1] : n1 = or(n1,X1),
inference(forward_demodulation,[],[f628,f117]) ).
fof(f871,plain,
! [X0,X1] : and(not(X0),not(not(X1))) = and(not(not(X1)),not(and(X0,X1))),
inference(superposition,[],[f567,f17]) ).
fof(f873,plain,
and(c1,not(c2)) = and(not(c2),b3),
inference(superposition,[],[f567,f128]) ).
fof(f874,plain,
and(d1,not(f3)) = and(not(f3),c1),
inference(superposition,[],[f567,f129]) ).
fof(f875,plain,
and(d2,not(f3)) = and(not(f3),c2),
inference(superposition,[],[f567,f130]) ).
fof(f876,plain,
and(f1,not(f3)) = and(not(f3),b1),
inference(superposition,[],[f567,f282]) ).
fof(f877,plain,
and(f2,not(f3)) = and(not(f3),b2),
inference(superposition,[],[f567,f274]) ).
fof(f890,plain,
and(f2,not(f3)) = and(b2,not(f3)),
inference(forward_demodulation,[],[f877,f11]) ).
fof(f891,plain,
and(f1,not(f3)) = and(b1,not(f3)),
inference(forward_demodulation,[],[f876,f11]) ).
fof(f892,plain,
and(d2,not(f3)) = and(c2,not(f3)),
inference(forward_demodulation,[],[f875,f11]) ).
fof(f893,plain,
and(d1,not(f3)) = and(c1,not(f3)),
inference(forward_demodulation,[],[f874,f11]) ).
fof(f894,plain,
and(c1,not(c2)) = and(b3,not(c2)),
inference(forward_demodulation,[],[f873,f11]) ).
fof(f896,plain,
! [X0,X1] : and(not(X0),not(not(X1))) = not(or(not(X1),and(X0,X1))),
inference(forward_demodulation,[],[f871,f18]) ).
fof(f906,plain,
! [X0,X1] : and(not(X0),not(not(X1))) = and(X1,not(and(X0,X1))),
inference(forward_demodulation,[],[f896,f405]) ).
fof(f913,plain,
! [X0,X1] : not(or(X0,not(X1))) = and(X1,not(and(X0,X1))),
inference(forward_demodulation,[],[f906,f18]) ).
fof(f918,plain,
! [X0,X1] : and(not(X0),X1) = and(X1,not(and(X0,X1))),
inference(forward_demodulation,[],[f913,f410]) ).
fof(f942,plain,
and(not(i2),f3) = and(f3,not(f3)),
inference(superposition,[],[f918,f326]) ).
fof(f943,plain,
and(i2,not(f3)) = and(not(i1),i2),
inference(superposition,[],[f918,f137]) ).
fof(f972,plain,
and(i2,not(i1)) = and(i2,not(f3)),
inference(forward_demodulation,[],[f943,f11]) ).
fof(f973,plain,
n0 = and(not(i2),f3),
inference(forward_demodulation,[],[f942,f31]) ).
fof(f992,plain,
and(i2,f1) = and(i2,not(f3)),
inference(forward_demodulation,[],[f972,f135]) ).
fof(f993,plain,
n0 = and(f3,not(i2)),
inference(forward_demodulation,[],[f973,f11]) ).
fof(f1005,plain,
and(f1,i2) = and(i2,not(f3)),
inference(forward_demodulation,[],[f992,f11]) ).
fof(f1006,plain,
n0 = and(f3,f2),
inference(forward_demodulation,[],[f993,f136]) ).
fof(f1014,plain,
n0 = and(f2,f3),
inference(forward_demodulation,[],[f1006,f11]) ).
fof(f1025,plain,
f2 = or(n0,and(f2,not(f3))),
inference(superposition,[],[f43,f1014]) ).
fof(f1032,plain,
f2 = and(f2,not(f3)),
inference(forward_demodulation,[],[f1025,f197]) ).
fof(f1038,plain,
f2 = and(b2,not(f3)),
inference(backward_demodulation,[],[f890,f1032]) ).
fof(f1092,plain,
! [X0,X1] : or(X0,and(X0,X1)) = X0,
inference(superposition,[],[f568,f11]) ).
fof(f1144,plain,
i1 = or(i1,f3),
inference(superposition,[],[f1092,f137]) ).
fof(f1213,plain,
! [X0] : not(and(f1,X0)) = or(i1,not(X0)),
inference(superposition,[],[f17,f258]) ).
fof(f1226,plain,
! [X0] : not(and(b2,X0)) = or(d2,not(X0)),
inference(superposition,[],[f17,f255]) ).
fof(f1228,plain,
! [X0] : not(or(b2,X0)) = and(d2,not(X0)),
inference(superposition,[],[f18,f255]) ).
fof(f1238,plain,
and(c2,not(f3)) = not(or(b2,f3)),
inference(backward_demodulation,[],[f892,f1228]) ).
fof(f1240,plain,
not(b2) = and(c2,not(f3)),
inference(forward_demodulation,[],[f1238,f279]) ).
fof(f1241,plain,
d2 = and(c2,not(f3)),
inference(forward_demodulation,[],[f1240,f255]) ).
fof(f1244,plain,
! [X0] : not(or(f2,X0)) = and(i2,not(X0)),
inference(superposition,[],[f18,f259]) ).
fof(f1254,plain,
and(f1,i2) = not(or(f2,f3)),
inference(backward_demodulation,[],[f1005,f1244]) ).
fof(f1256,plain,
not(b2) = and(f1,i2),
inference(forward_demodulation,[],[f1254,f274]) ).
fof(f1257,plain,
d2 = and(f1,i2),
inference(forward_demodulation,[],[f1256,f255]) ).
fof(f1261,plain,
f1 = or(d2,and(f1,not(i2))),
inference(superposition,[],[f43,f1257]) ).
fof(f1265,plain,
and(not(f1),i2) = and(i2,not(d2)),
inference(superposition,[],[f918,f1257]) ).
fof(f1267,plain,
and(not(f1),i2) = not(or(f2,d2)),
inference(forward_demodulation,[],[f1265,f1244]) ).
fof(f1270,plain,
f1 = or(d2,and(f1,f2)),
inference(forward_demodulation,[],[f1261,f136]) ).
fof(f1273,plain,
and(not(f1),i2) = and(b2,not(f2)),
inference(forward_demodulation,[],[f1267,f437]) ).
fof(f1276,plain,
and(not(f1),i2) = and(b2,i2),
inference(forward_demodulation,[],[f1273,f259]) ).
fof(f1279,plain,
and(b2,i2) = and(i2,not(f1)),
inference(forward_demodulation,[],[f1276,f11]) ).
fof(f1280,plain,
and(b2,i2) = not(or(f2,f1)),
inference(forward_demodulation,[],[f1279,f1244]) ).
fof(f1281,plain,
and(b2,i2) = not(or(f1,f2)),
inference(forward_demodulation,[],[f1280,f12]) ).
fof(f1427,plain,
! [X0] : not(and(b1,X0)) = or(d1,not(X0)),
inference(superposition,[],[f17,f254]) ).
fof(f1429,plain,
! [X0] : not(or(b1,X0)) = and(d1,not(X0)),
inference(superposition,[],[f18,f254]) ).
fof(f1440,plain,
and(c1,not(f3)) = not(or(b1,f3)),
inference(backward_demodulation,[],[f893,f1429]) ).
fof(f1442,plain,
not(b1) = and(c1,not(f3)),
inference(forward_demodulation,[],[f1440,f287]) ).
fof(f1443,plain,
d1 = and(c1,not(f3)),
inference(forward_demodulation,[],[f1442,f254]) ).
fof(f1533,plain,
c2 = and(c2,b3),
inference(superposition,[],[f571,f240]) ).
fof(f1537,plain,
f1 = and(f1,b1),
inference(superposition,[],[f571,f282]) ).
fof(f1563,plain,
f1 = and(b1,f1),
inference(forward_demodulation,[],[f1537,f11]) ).
fof(f1737,plain,
! [X0,X1] : not(and(not(X0),not(X1))) = or(X1,not(not(and(X0,not(X1))))),
inference(superposition,[],[f378,f918]) ).
fof(f1765,plain,
! [X0,X1] : not(and(not(X0),not(X1))) = or(X1,and(X0,not(X1))),
inference(forward_demodulation,[],[f1737,f42]) ).
fof(f1786,plain,
! [X0,X1] : or(X1,and(X0,not(X1))) = or(not(not(X0)),X1),
inference(forward_demodulation,[],[f1765,f383]) ).
fof(f1800,plain,
! [X0,X1] : or(X0,X1) = or(X1,and(X0,not(X1))),
inference(forward_demodulation,[],[f1786,f42]) ).
fof(f1809,plain,
! [X0,X1] : or(X1,not(X0)) = or(not(X0),and(X1,X0)),
inference(superposition,[],[f1800,f42]) ).
fof(f1913,plain,
and(f3,not(f1)) = and(not(f1),b1),
inference(superposition,[],[f561,f282]) ).
fof(f1914,plain,
and(f3,not(f2)) = and(not(f2),b2),
inference(superposition,[],[f561,f274]) ).
fof(f1937,plain,
and(f3,not(f2)) = and(b2,not(f2)),
inference(forward_demodulation,[],[f1914,f11]) ).
fof(f1938,plain,
and(f3,not(f1)) = and(b1,not(f1)),
inference(forward_demodulation,[],[f1913,f11]) ).
fof(f1961,plain,
and(f3,i2) = and(b2,i2),
inference(forward_demodulation,[],[f1937,f259]) ).
fof(f1962,plain,
and(f3,i1) = and(b1,i1),
inference(forward_demodulation,[],[f1938,f258]) ).
fof(f1982,plain,
and(i2,f3) = and(b2,i2),
inference(forward_demodulation,[],[f1961,f11]) ).
fof(f1983,plain,
and(b1,i1) = and(i1,f3),
inference(forward_demodulation,[],[f1962,f11]) ).
fof(f1997,plain,
f3 = and(b2,i2),
inference(forward_demodulation,[],[f1982,f326]) ).
fof(f2007,plain,
f3 = not(or(f1,f2)),
inference(backward_demodulation,[],[f1281,f1997]) ).
fof(f2138,plain,
or(not(i2),f3) = or(i1,not(i2)),
inference(superposition,[],[f1809,f137]) ).
fof(f2156,plain,
not(and(f1,i2)) = or(not(i2),f3),
inference(forward_demodulation,[],[f2138,f1213]) ).
fof(f2186,plain,
not(and(f1,i2)) = or(f3,not(i2)),
inference(forward_demodulation,[],[f2156,f12]) ).
fof(f2209,plain,
or(f3,f2) = not(and(f1,i2)),
inference(forward_demodulation,[],[f2186,f136]) ).
fof(f2224,plain,
or(f3,f2) = or(f2,not(f1)),
inference(forward_demodulation,[],[f2209,f400]) ).
fof(f2233,plain,
or(f3,f2) = or(f2,i1),
inference(forward_demodulation,[],[f2224,f258]) ).
fof(f2237,plain,
or(f2,f3) = or(f2,i1),
inference(forward_demodulation,[],[f2233,f12]) ).
fof(f2241,plain,
b2 = or(f2,i1),
inference(forward_demodulation,[],[f2237,f274]) ).
fof(f2249,plain,
and(f2,not(i1)) = and(not(i1),b2),
inference(superposition,[],[f567,f2241]) ).
fof(f2254,plain,
and(f2,not(i1)) = and(b2,not(i1)),
inference(forward_demodulation,[],[f2249,f11]) ).
fof(f2257,plain,
and(f2,f1) = and(b2,f1),
inference(forward_demodulation,[],[f2254,f135]) ).
fof(f2260,plain,
and(f1,f2) = and(b2,f1),
inference(forward_demodulation,[],[f2257,f11]) ).
fof(f2263,plain,
f1 = or(d2,and(b2,f1)),
inference(backward_demodulation,[],[f1270,f2260]) ).
fof(f3053,plain,
and(f3,not(i1)) = and(not(i1),i1),
inference(superposition,[],[f561,f1144]) ).
fof(f3055,plain,
f3 = and(f3,i1),
inference(superposition,[],[f570,f1144]) ).
fof(f3057,plain,
f3 = and(i1,f3),
inference(forward_demodulation,[],[f3055,f11]) ).
fof(f3058,plain,
and(i1,not(i1)) = and(f3,not(i1)),
inference(forward_demodulation,[],[f3053,f11]) ).
fof(f3059,plain,
f3 = and(b1,i1),
inference(backward_demodulation,[],[f1983,f3057]) ).
fof(f3060,plain,
and(i1,f1) = and(f3,f1),
inference(forward_demodulation,[],[f3058,f135]) ).
fof(f3061,plain,
and(i1,f1) = and(f1,f3),
inference(forward_demodulation,[],[f3060,f11]) ).
fof(f3062,plain,
and(f1,i1) = and(f1,f3),
inference(forward_demodulation,[],[f3061,f11]) ).
fof(f3063,plain,
n0 = and(f1,f3),
inference(forward_demodulation,[],[f3062,f207]) ).
fof(f3066,plain,
! [X0] : and(or(b1,X0),i1) = or(f3,and(X0,i1)),
inference(superposition,[],[f19,f3059]) ).
fof(f3078,plain,
! [X0] : or(f3,and(X0,i1)) = and(i1,or(b1,X0)),
inference(forward_demodulation,[],[f3066,f11]) ).
fof(f3084,plain,
i1 = and(i1,or(b1,f2)),
inference(backward_demodulation,[],[f152,f3078]) ).
fof(f3215,plain,
f1 = or(n0,and(f1,not(f3))),
inference(superposition,[],[f43,f3063]) ).
fof(f3226,plain,
f1 = and(f1,not(f3)),
inference(forward_demodulation,[],[f3215,f197]) ).
fof(f3233,plain,
f1 = and(b1,not(f3)),
inference(backward_demodulation,[],[f891,f3226]) ).
fof(f3389,plain,
and(not(f1),f2) = and(f2,not(and(b2,f1))),
inference(superposition,[],[f918,f2260]) ).
fof(f3391,plain,
or(f1,not(f2)) = or(not(f2),and(b2,f1)),
inference(superposition,[],[f1809,f2260]) ).
fof(f3392,plain,
or(f1,i2) = or(i2,and(b2,f1)),
inference(forward_demodulation,[],[f3391,f259]) ).
fof(f3393,plain,
and(f2,not(and(b2,f1))) = and(f2,not(f1)),
inference(forward_demodulation,[],[f3389,f11]) ).
fof(f3400,plain,
and(f2,i1) = and(f2,not(and(b2,f1))),
inference(forward_demodulation,[],[f3393,f258]) ).
fof(f3414,plain,
or(b1,not(f1)) = or(not(f1),f1),
inference(superposition,[],[f1809,f1563]) ).
fof(f3415,plain,
or(f1,not(f1)) = or(b1,not(f1)),
inference(forward_demodulation,[],[f3414,f12]) ).
fof(f3421,plain,
or(f1,i1) = or(b1,i1),
inference(forward_demodulation,[],[f3415,f258]) ).
fof(f3426,plain,
n1 = or(b1,i1),
inference(forward_demodulation,[],[f3421,f206]) ).
fof(f3431,plain,
! [X0] : or(n1,X0) = or(b1,or(X0,i1)),
inference(superposition,[],[f116,f3426]) ).
fof(f3439,plain,
! [X0] : n1 = or(b1,or(X0,i1)),
inference(forward_demodulation,[],[f3431,f658]) ).
fof(f3946,plain,
or(b1,f2) = or(or(b1,f2),i1),
inference(superposition,[],[f568,f3084]) ).
fof(f3950,plain,
or(b1,f2) = or(b1,or(f2,i1)),
inference(forward_demodulation,[],[f3946,f14]) ).
fof(f3953,plain,
n1 = or(b1,f2),
inference(forward_demodulation,[],[f3950,f3439]) ).
fof(f4595,plain,
or(f2,b1) = or(b2,b1),
inference(superposition,[],[f634,f287]) ).
fof(f4597,plain,
or(b2,d1) = or(f2,c1),
inference(superposition,[],[f634,f129]) ).
fof(f4599,plain,
or(f2,c1) = or(b2,c1),
inference(superposition,[],[f634,f248]) ).
fof(f4647,plain,
or(b2,c1) = or(c1,f2),
inference(forward_demodulation,[],[f4599,f12]) ).
fof(f4649,plain,
or(b2,d1) = or(c1,f2),
inference(forward_demodulation,[],[f4597,f12]) ).
fof(f4651,plain,
or(f2,b1) = or(b1,b2),
inference(forward_demodulation,[],[f4595,f12]) ).
fof(f4661,plain,
or(b2,d1) = or(b2,c1),
inference(forward_demodulation,[],[f4649,f4647]) ).
fof(f4663,plain,
or(b1,f2) = or(b1,b2),
inference(forward_demodulation,[],[f4651,f12]) ).
fof(f4667,plain,
n1 = or(b1,b2),
inference(forward_demodulation,[],[f4663,f3953]) ).
fof(f4729,plain,
and(not(b1),n1) = and(b2,not(b1)),
inference(superposition,[],[f561,f4667]) ).
fof(f4739,plain,
and(d1,n1) = and(b2,d1),
inference(forward_demodulation,[],[f4729,f254]) ).
fof(f4745,plain,
d1 = and(b2,d1),
inference(forward_demodulation,[],[f4739,f3]) ).
fof(f4787,plain,
b2 = or(b2,d1),
inference(superposition,[],[f1092,f4745]) ).
fof(f4792,plain,
b2 = or(b2,c1),
inference(backward_demodulation,[],[f4661,f4787]) ).
fof(f4800,plain,
b2 = or(c1,f2),
inference(backward_demodulation,[],[f4647,f4792]) ).
fof(f4861,plain,
and(not(c1),b2) = and(f2,not(c1)),
inference(superposition,[],[f561,f4800]) ).
fof(f4874,plain,
and(b2,not(c1)) = and(f2,not(c1)),
inference(forward_demodulation,[],[f4861,f11]) ).
fof(f4948,plain,
and(not(c2),not(f3)) = and(not(f3),not(d2)),
inference(superposition,[],[f918,f1241]) ).
fof(f4954,plain,
and(not(c2),not(f3)) = not(or(f3,d2)),
inference(forward_demodulation,[],[f4948,f18]) ).
fof(f4965,plain,
and(b2,not(f3)) = and(not(c2),not(f3)),
inference(forward_demodulation,[],[f4954,f437]) ).
fof(f4973,plain,
and(b2,not(f3)) = not(or(c2,f3)),
inference(forward_demodulation,[],[f4965,f18]) ).
fof(f4976,plain,
not(c2) = and(b2,not(f3)),
inference(forward_demodulation,[],[f4973,f247]) ).
fof(f4979,plain,
f2 = not(c2),
inference(forward_demodulation,[],[f4976,f1038]) ).
fof(f4987,plain,
and(c1,f2) = and(b3,f2),
inference(backward_demodulation,[],[f894,f4979]) ).
fof(f4989,plain,
and(c1,f2) = and(f2,b3),
inference(forward_demodulation,[],[f4987,f11]) ).
fof(f4993,plain,
! [X0] : or(f2,not(X0)) = not(and(c2,X0)),
inference(superposition,[],[f17,f4979]) ).
fof(f4995,plain,
! [X0] : and(f2,not(X0)) = not(or(c2,X0)),
inference(superposition,[],[f18,f4979]) ).
fof(f4999,plain,
c2 = not(f2),
inference(superposition,[],[f42,f4979]) ).
fof(f5006,plain,
! [X0] : not(or(X0,f2)) = and(not(X0),c2),
inference(superposition,[],[f410,f4979]) ).
fof(f5018,plain,
! [X0] : not(or(X0,f2)) = and(c2,not(X0)),
inference(forward_demodulation,[],[f5006,f11]) ).
fof(f5022,plain,
c2 = i2,
inference(backward_demodulation,[],[f259,f4999]) ).
fof(f5026,plain,
and(f2,i1) = not(or(c2,and(b2,f1))),
inference(backward_demodulation,[],[f3400,f4995]) ).
fof(f5029,plain,
and(b2,not(c1)) = not(or(c2,c1)),
inference(backward_demodulation,[],[f4874,f4995]) ).
fof(f5036,plain,
f3 = and(c2,not(f1)),
inference(backward_demodulation,[],[f2007,f5018]) ).
fof(f5039,plain,
sF16 = output(c2,i1),
inference(backward_demodulation,[],[f112,f5022]) ).
fof(f5042,plain,
~ circuit(input(i1,c2),sF16),
inference(backward_demodulation,[],[f139,f5022]) ).
fof(f5043,plain,
circuit(input(i1,c2),output(a1,a2)),
inference(backward_demodulation,[],[f142,f5022]) ).
fof(f5090,plain,
or(c2,and(b2,f1)) = or(f1,c2),
inference(backward_demodulation,[],[f3392,f5022]) ).
fof(f5114,plain,
not(or(c1,c2)) = and(b2,not(c1)),
inference(forward_demodulation,[],[f5029,f12]) ).
fof(f5119,plain,
f3 = and(c2,i1),
inference(forward_demodulation,[],[f5036,f258]) ).
fof(f5120,plain,
or(c2,and(b2,f1)) = or(c2,f1),
inference(forward_demodulation,[],[f5090,f12]) ).
fof(f5140,plain,
~ circuit(input(i1,c2),output(c2,i1)),
inference(backward_demodulation,[],[f5042,f5039]) ).
fof(f5141,plain,
not(b3) = and(b2,not(c1)),
inference(forward_demodulation,[],[f5114,f128]) ).
fof(f5143,plain,
and(f2,i1) = not(or(c2,f1)),
inference(backward_demodulation,[],[f5026,f5120]) ).
fof(f5154,plain,
or(not(i1),f3) = or(c2,not(i1)),
inference(superposition,[],[f1809,f5119]) ).
fof(f5156,plain,
or(f1,f3) = or(c2,f1),
inference(forward_demodulation,[],[f5154,f135]) ).
fof(f5162,plain,
b1 = or(c2,f1),
inference(forward_demodulation,[],[f5156,f282]) ).
fof(f5168,plain,
not(b1) = and(f2,i1),
inference(backward_demodulation,[],[f5143,f5162]) ).
fof(f5173,plain,
d1 = and(f2,i1),
inference(forward_demodulation,[],[f5168,f254]) ).
fof(f5220,plain,
and(f1,not(c2)) = and(not(c2),b1),
inference(superposition,[],[f561,f5162]) ).
fof(f5233,plain,
and(f1,not(c2)) = and(b1,not(c2)),
inference(forward_demodulation,[],[f5220,f11]) ).
fof(f5238,plain,
and(f1,f2) = and(b1,f2),
inference(forward_demodulation,[],[f5233,f4979]) ).
fof(f5242,plain,
and(b2,f1) = and(b1,f2),
inference(backward_demodulation,[],[f2260,f5238]) ).
fof(f5245,plain,
f1 = or(d2,and(b1,f2)),
inference(backward_demodulation,[],[f2263,f5242]) ).
fof(f5560,plain,
or(f2,not(b3)) = or(not(b3),and(c1,f2)),
inference(superposition,[],[f1809,f4989]) ).
fof(f5562,plain,
not(and(c2,b3)) = or(not(b3),and(c1,f2)),
inference(forward_demodulation,[],[f5560,f4993]) ).
fof(f5570,plain,
not(c2) = or(not(b3),and(c1,f2)),
inference(forward_demodulation,[],[f5562,f1533]) ).
fof(f5574,plain,
f2 = or(not(b3),and(c1,f2)),
inference(forward_demodulation,[],[f5570,f4979]) ).
fof(f5647,plain,
and(not(c1),not(f3)) = and(not(f3),not(d1)),
inference(superposition,[],[f918,f1443]) ).
fof(f5653,plain,
and(not(c1),not(f3)) = not(or(f3,d1)),
inference(forward_demodulation,[],[f5647,f18]) ).
fof(f5664,plain,
and(b1,not(f3)) = and(not(c1),not(f3)),
inference(forward_demodulation,[],[f5653,f438]) ).
fof(f5672,plain,
and(b1,not(f3)) = not(or(c1,f3)),
inference(forward_demodulation,[],[f5664,f18]) ).
fof(f5675,plain,
and(b1,not(f3)) = not(c1),
inference(forward_demodulation,[],[f5672,f248]) ).
fof(f5678,plain,
f1 = not(c1),
inference(forward_demodulation,[],[f5675,f3233]) ).
fof(f5686,plain,
not(b3) = and(b2,f1),
inference(backward_demodulation,[],[f5141,f5678]) ).
fof(f5691,plain,
not(b3) = and(b1,f2),
inference(backward_demodulation,[],[f5242,f5686]) ).
fof(f5696,plain,
f1 = or(d2,not(b3)),
inference(backward_demodulation,[],[f5245,f5691]) ).
fof(f5705,plain,
f1 = not(and(b2,b3)),
inference(forward_demodulation,[],[f5696,f1226]) ).
fof(f5707,plain,
f1 = not(a2),
inference(forward_demodulation,[],[f5705,f125]) ).
fof(f5719,plain,
a2 = not(f1),
inference(superposition,[],[f42,f5707]) ).
fof(f5742,plain,
a2 = i1,
inference(backward_demodulation,[],[f258,f5719]) ).
fof(f5801,plain,
circuit(input(a2,c2),output(a1,a2)),
inference(backward_demodulation,[],[f5043,f5742]) ).
fof(f5804,plain,
f3 = and(c2,a2),
inference(backward_demodulation,[],[f5119,f5742]) ).
fof(f5807,plain,
~ circuit(input(a2,c2),output(c2,a2)),
inference(backward_demodulation,[],[f5140,f5742]) ).
fof(f5810,plain,
d1 = and(f2,a2),
inference(backward_demodulation,[],[f5173,f5742]) ).
fof(f5840,plain,
d1 = and(a2,f2),
inference(forward_demodulation,[],[f5810,f11]) ).
fof(f5843,plain,
f3 = and(a2,c2),
inference(forward_demodulation,[],[f5804,f11]) ).
fof(f5872,plain,
a2 = or(f3,and(a2,not(c2))),
inference(superposition,[],[f43,f5843]) ).
fof(f5884,plain,
a2 = or(f3,and(a2,f2)),
inference(forward_demodulation,[],[f5872,f4979]) ).
fof(f5890,plain,
a2 = or(f3,d1),
inference(forward_demodulation,[],[f5884,f5840]) ).
fof(f5893,plain,
a2 = or(d1,f3),
inference(forward_demodulation,[],[f5890,f12]) ).
fof(f5894,plain,
a2 = c1,
inference(backward_demodulation,[],[f129,f5893]) ).
fof(f5959,plain,
f2 = or(not(b3),and(a2,f2)),
inference(backward_demodulation,[],[f5574,f5894]) ).
fof(f5966,plain,
f2 = or(not(b3),d1),
inference(forward_demodulation,[],[f5959,f5840]) ).
fof(f5984,plain,
f2 = or(d1,not(b3)),
inference(forward_demodulation,[],[f5966,f12]) ).
fof(f5988,plain,
f2 = not(and(b1,b3)),
inference(forward_demodulation,[],[f5984,f1427]) ).
fof(f5989,plain,
f2 = not(a1),
inference(forward_demodulation,[],[f5988,f124]) ).
fof(f6001,plain,
a1 = not(f2),
inference(superposition,[],[f42,f5989]) ).
fof(f6024,plain,
a1 = c2,
inference(backward_demodulation,[],[f4999,f6001]) ).
fof(f6120,plain,
circuit(input(a2,a1),output(a1,a2)),
inference(backward_demodulation,[],[f5801,f6024]) ).
fof(f6123,plain,
~ circuit(input(a2,a1),output(a1,a2)),
inference(backward_demodulation,[],[f5807,f6024]) ).
fof(f6149,plain,
$false,
inference(forward_subsumption_resolution,[],[f6120,f6123]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n004.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Sun Sep 27 10:51:52 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.44 Running first-order theorem proving
% 0.14/0.44 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
% 13.64/2.78 % (3339806)Input is clausal, will run a generic CNF schedule.
% 13.64/2.78 % (3339828)dis-21_1_sil=8000:lcm=predicate:random_seed=2200345711:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 13.64/2.78 % (3339828)Refutation not found, incomplete strategy
% 13.64/2.78 % (3339828)------------------------------
% 13.64/2.78 % (3339828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339828)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339828)Termination reason: Refutation not found, incomplete strategy
% 13.64/2.78 % (3339828)Time elapsed: 0.001 s
% 13.64/2.78 % (3339828)Peak memory usage: 88 MB
% 13.64/2.78 % (3339828)Instructions burned: 1 (million)
% 13.64/2.78 % (3339827)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=222474378:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.64/2.78 % (3339823)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3083798295:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.64/2.78 % (3339824)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1161088096:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.64/2.78 % (3339825)lrs+10_1_sil=8000:sp=occurrence:random_seed=3669851141:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.64/2.78 % (3339826)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2122251176:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.64/2.78 % (3339822)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2177826437:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.64/2.78 % (3339825)Instruction limit reached!
% 13.64/2.78 % (3339825)------------------------------
% 13.64/2.78 % (3339825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339825)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339825)Termination reason: Instruction limit
% 13.64/2.78 % (3339825)Termination phase: Saturation
% 13.64/2.78 % (3339825)Time elapsed: 0.065 s
% 13.64/2.78 % (3339825)Peak memory usage: 89 MB
% 13.64/2.78 % (3339825)Instructions burned: 108 (million)
% 13.64/2.78 % (3339826)Instruction limit reached!
% 13.64/2.78 % (3339826)------------------------------
% 13.64/2.78 % (3339826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339826)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339826)Termination reason: Instruction limit
% 13.64/2.78 % (3339826)Termination phase: Saturation
% 13.64/2.78 % (3339826)Time elapsed: 0.067 s
% 13.64/2.78 % (3339826)Peak memory usage: 88 MB
% 13.64/2.78 % (3339826)Instructions burned: 115 (million)
% 13.64/2.78 % (3339827)Instruction limit reached!
% 13.64/2.78 % (3339827)------------------------------
% 13.64/2.78 % (3339827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339827)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339827)Termination reason: Instruction limit
% 13.64/2.78 % (3339827)Termination phase: Saturation
% 13.64/2.78 % (3339827)Time elapsed: 0.100 s
% 13.64/2.78 % (3339827)Peak memory usage: 89 MB
% 13.64/2.78 % (3339827)Instructions burned: 182 (million)
% 13.64/2.78 % (3339828)------------------------------
% 13.64/2.78 % (3339828)------------------------------
% 13.64/2.78 % (3339850)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2087290945:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 13.64/2.78 % (3339849)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2804182259:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.64/2.78 % (3339851)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2180948694:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.64/2.78 % (3339849)Instruction limit reached!
% 13.64/2.78 % (3339849)------------------------------
% 13.64/2.78 % (3339849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339849)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339849)Termination reason: Instruction limit
% 13.64/2.78 % (3339849)Termination phase: Saturation
% 13.64/2.78 % (3339849)Time elapsed: 0.081 s
% 13.64/2.78 % (3339849)Peak memory usage: 89 MB
% 13.64/2.78 % (3339849)Instructions burned: 143 (million)
% 13.64/2.78 % (3339852)lrs+10_64_to=lpo:sil=8000:random_seed=2236309020:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 13.64/2.78 % (3339850)Instruction limit reached!
% 13.64/2.78 % (3339850)------------------------------
% 13.64/2.78 % (3339850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339850)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339850)Termination reason: Instruction limit
% 13.64/2.78 % (3339850)Termination phase: Saturation
% 13.64/2.78 % (3339850)Time elapsed: 0.121 s
% 13.64/2.78 % (3339850)Peak memory usage: 89 MB
% 13.64/2.78 % (3339850)Instructions burned: 192 (million)
% 13.64/2.78 % (3339852)Instruction limit reached!
% 13.64/2.78 % (3339852)------------------------------
% 13.64/2.78 % (3339852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339852)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339852)Termination reason: Instruction limit
% 13.64/2.78 % (3339852)Termination phase: Saturation
% 13.64/2.78 % (3339852)Time elapsed: 0.041 s
% 13.64/2.78 % (3339852)Peak memory usage: 89 MB
% 13.64/2.78 % (3339852)Instructions burned: 128 (million)
% 13.64/2.78 % (3339851)Instruction limit reached!
% 13.64/2.78 % (3339851)------------------------------
% 13.64/2.78 % (3339851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339851)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339851)Termination reason: Instruction limit
% 13.64/2.78 % (3339851)Termination phase: Saturation
% 13.64/2.78 % (3339851)Time elapsed: 0.131 s
% 13.64/2.78 % (3339851)Peak memory usage: 90 MB
% 13.64/2.78 % (3339851)Instructions burned: 220 (million)
% 13.64/2.78 % (3339856)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=573045534:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.64/2.78 % (3339858)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1543613476:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 13.64/2.78 % (3339867)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1140250521:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 13.64/2.78 % (3339868)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=657337351:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 13.64/2.78 % (3339856)Instruction limit reached!
% 13.64/2.78 % (3339856)------------------------------
% 13.64/2.78 % (3339856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339856)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339856)Termination reason: Instruction limit
% 13.64/2.78 % (3339856)Termination phase: Saturation
% 13.64/2.78 % (3339856)Time elapsed: 0.183 s
% 13.64/2.78 % (3339856)Peak memory usage: 90 MB
% 13.64/2.78 % (3339856)Instructions burned: 194 (million)
% 13.64/2.78 % (3339858)Instruction limit reached!
% 13.64/2.78 % (3339858)------------------------------
% 13.64/2.78 % (3339858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339858)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339858)Termination reason: Instruction limit
% 13.64/2.78 % (3339858)Termination phase: Saturation
% 13.64/2.78 % (3339858)Time elapsed: 0.164 s
% 13.64/2.78 % (3339858)Peak memory usage: 91 MB
% 13.64/2.78 % (3339858)Instructions burned: 157 (million)
% 13.64/2.78 % (3339868)Instruction limit reached!
% 13.64/2.78 % (3339868)------------------------------
% 13.64/2.78 % (3339868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339868)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339868)Termination reason: Instruction limit
% 13.64/2.78 % (3339868)Termination phase: Saturation
% 13.64/2.78 % (3339868)Time elapsed: 0.109 s
% 13.64/2.78 % (3339868)Peak memory usage: 90 MB
% 13.64/2.78 % (3339868)Instructions burned: 106 (million)
% 13.64/2.78 % (3339883)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=201792535:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 13.64/2.78 % (3339885)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2247588721:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 13.64/2.78 % (3339884)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3680905999:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 13.64/2.78 % (3339883)Instruction limit reached!
% 13.64/2.78 % (3339883)------------------------------
% 13.64/2.78 % (3339883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339883)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339883)Termination reason: Instruction limit
% 13.64/2.78 % (3339883)Termination phase: Saturation
% 13.64/2.78 % (3339883)Time elapsed: 0.101 s
% 13.64/2.78 % (3339883)Peak memory usage: 89 MB
% 13.64/2.78 % (3339883)Instructions burned: 107 (million)
% 13.64/2.78 % (3339884)Instruction limit reached!
% 13.64/2.78 % (3339884)------------------------------
% 13.64/2.78 % (3339884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339884)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339884)Termination reason: Instruction limit
% 13.64/2.78 % (3339884)Termination phase: Saturation
% 13.64/2.78 % (3339884)Time elapsed: 0.230 s
% 13.64/2.78 % (3339884)Peak memory usage: 90 MB
% 13.64/2.78 % (3339884)Instructions burned: 242 (million)
% 13.64/2.78 % (3339895)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3511701870:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 13.64/2.78 % (3339895)Instruction limit reached!
% 13.64/2.78 % (3339895)------------------------------
% 13.64/2.78 % (3339895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.64/2.78 % (3339895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.64/2.78 % (3339895)CaDiCaL version: 2.1.3
% 13.64/2.78 % (3339895)Termination reason: Instruction limit
% 13.64/2.78 % (3339895)Termination phase: Saturation
% 13.64/2.78 % (3339895)Time elapsed: 0.107 s
% 13.64/2.78 % (3339895)Peak memory usage: 89 MB
% 13.64/2.78 % (3339895)Instructions burned: 134 (million)
% 13.64/2.78 % (3339824)First to succeed.
% 13.64/2.78 % (3339824)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3339806"
% 13.64/2.78 % (3339902)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=446521361:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 13.64/2.78 % (3339822)Also succeeded, but the first one will report.
% 13.64/2.78 % (3339867)Also succeeded, but the first one will report.
% 13.64/2.78 % (3339908)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=645922625:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 13.64/2.78 % (3339824)Refutation found. Thanks to Tanya!
% 13.64/2.78 % SZS status Unsatisfiable for theBenchmark
% 13.64/2.78 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/3.06 % (3339824)------------------------------
% 0.18/3.06 % (3339824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/3.06 % (3339824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/3.06 % (3339824)CaDiCaL version: 2.1.3
% 0.18/3.06 % (3339824)Termination reason: Refutation
% 0.18/3.06 % (3339824)Time elapsed: 1.507 s
% 0.18/3.06 % (3339824)Peak memory usage: 134 MB
% 0.18/3.06 % (3339824)Instructions burned: 1636 (million)
% 0.18/3.06 % (3339824)------------------------------
% 0.18/3.06 % (3339824)------------------------------
% 0.18/3.06 % (3339806)Success in time 2.132 s
% 0.18/3.06 % Vampire exiting
%------------------------------------------------------------------------------