%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV003-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 : n015.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:20:08 AM UTC 2026
% Result : Unsatisfiable 59.34s 14.06s
% Output : Refutation 92.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 74
% Syntax : Number of formulae : 753 ( 753 unt; 33 def)
% Number of atoms : 753 ( 746 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 53 ( 53 usr; 47 con; 0-3 aty)
% Number of variables : 927 ( 927 !; 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(f7,axiom,
not(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_definition1) ).
fof(f8,plain,
n1 = not(n0),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_definition2) ).
fof(f10,plain,
n0 = not(n1),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0,X1] : not(and(X0,X1)) = or(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan1) ).
fof(f12,axiom,
! [X0,X1] : not(or(X0,X1)) = and(not(X0),not(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',demorgan2) ).
fof(f13,axiom,
! [X0] : not(not(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_involution) ).
fof(f14,negated_conjecture,
! [X0,X1] : and(X0,X1) = and(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_symmetry) ).
fof(f15,negated_conjecture,
! [X0,X1] : or(X0,X1) = or(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_symmetry) ).
fof(f16,negated_conjecture,
! [X2,X0,X1] : and(or(X0,X1),X2) = or(and(X0,X2),and(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_simplification) ).
fof(f17,negated_conjecture,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(and(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutativity) ).
fof(f18,negated_conjecture,
! [X2,X0,X1] : or(or(X0,X1),X2) = or(or(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutativity) ).
fof(f19,axiom,
! [X0] : and(X0,not(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_evaluation1) ).
fof(f20,plain,
! [X0] : n0 = and(X0,not(X0)),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0] : or(X0,not(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_evaluation1) ).
fof(f22,plain,
! [X0] : n1 = or(X0,not(X0)),
inference(reorient_equations,[],[f21]) ).
fof(f23,axiom,
! [X0] : and(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_idempotency) ).
fof(f24,axiom,
! [X0] : or(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_idempotency) ).
fof(f25,axiom,
! [X0,X1] : and(and(X0,X1),not(X1)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_evaluation2) ).
fof(f26,plain,
! [X0,X1] : n0 = and(and(X0,X1),not(X1)),
inference(reorient_equations,[],[f25]) ).
fof(f27,axiom,
! [X0,X1] : and(and(X0,X1),not(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_evaluation3) ).
fof(f28,plain,
! [X0,X1] : n0 = and(and(X0,X1),not(X0)),
inference(reorient_equations,[],[f27]) ).
fof(f29,axiom,
! [X0,X1] : or(or(X0,X1),not(X1)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_evaluation2) ).
fof(f30,plain,
! [X0,X1] : n1 = or(or(X0,X1),not(X1)),
inference(reorient_equations,[],[f29]) ).
fof(f31,axiom,
! [X0,X1] : or(or(X0,X1),not(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_evaluation3) ).
fof(f32,plain,
! [X0,X1] : n1 = or(or(X0,X1),not(X0)),
inference(reorient_equations,[],[f31]) ).
fof(f33,axiom,
! [X0,X1] : and(and(X0,X1),X1) = and(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_evaluation1) ).
fof(f34,plain,
! [X0,X1] : and(X0,X1) = and(and(X0,X1),X1),
inference(reorient_equations,[],[f33]) ).
fof(f41,axiom,
! [X0,X1] : or(and(X0,X1),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_subsumption1) ).
fof(f42,axiom,
! [X0,X1] : or(and(X0,X1),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_subsumption2) ).
fof(f43,axiom,
! [X2,X0,X1] : or(or(and(X0,X1),X2),X1) = or(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_subsumption3) ).
fof(f44,axiom,
! [X2,X0,X1] : or(or(X0,and(X1,X2)),X2) = or(X0,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_subsumption4) ).
fof(f45,plain,
! [X2,X0,X1] : or(X0,X2) = or(or(X0,and(X1,X2)),X2),
inference(reorient_equations,[],[f44]) ).
fof(f46,axiom,
! [X0,X1] : or(and(X0,not(X1)),X1) = or(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',karnaugh1) ).
fof(f47,plain,
! [X0,X1] : or(X0,X1) = or(and(X0,not(X1)),X1),
inference(reorient_equations,[],[f46]) ).
fof(f49,axiom,
! [X2,X0,X1] : or(and(and(X0,X1),not(X2)),and(X0,X2)) = or(and(X0,X1),and(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',karnaugh3) ).
fof(f50,axiom,
! [X0,X1] : xor(X0,X1) = or(and(X0,not(X1)),and(X1,not(X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xor_definition) ).
fof(f51,negated_conjecture,
! [X2,X0,X1] : carryout(X0,X1,X2) = or(and(X0,or(X1,X2)),and(not(X0),and(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',carryout_definition) ).
fof(f52,negated_conjecture,
! [X2,X0,X1] : sum(X0,X1,X2) = xor(xor(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_definition) ).
fof(f53,negated_conjecture,
a11 = not(and(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit1) ).
fof(f54,negated_conjecture,
a12 = not(and(a11,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit2) ).
fof(f55,negated_conjecture,
a13 = not(and(a11,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit3) ).
fof(f56,negated_conjecture,
a14 = not(and(a12,a13)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit4) ).
fof(f57,negated_conjecture,
a15 = not(and(a14,carryin)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit5) ).
fof(f58,negated_conjecture,
a16 = not(and(a14,a15)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit6) ).
fof(f59,negated_conjecture,
a17 = not(and(a15,carryin)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit7) ).
fof(f60,negated_conjecture,
s1 = not(and(a16,a17)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit8) ).
fof(f61,negated_conjecture,
c1 = not(and(a11,a15)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit9) ).
fof(f62,negated_conjecture,
circuit(s1,c1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_output_circuit) ).
fof(f63,negated_conjecture,
~ circuit(sum(a,b,carryin),carryout(a,b,carryin)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_circuit) ).
fof(f64,plain,
! [X2,X0,X1] : sum(X0,X1,X2) = or(and(or(and(X0,not(X1)),and(X1,not(X0))),not(X2)),and(X2,not(or(and(X0,not(X1)),and(X1,not(X0)))))),
inference(definition_unfolding,[],[f52,f50,f50]) ).
fof(f65,plain,
~ circuit(or(and(or(and(a,not(b)),and(b,not(a))),not(carryin)),and(carryin,not(or(and(a,not(b)),and(b,not(a)))))),or(and(a,or(b,carryin)),and(not(a),and(b,carryin)))),
inference(definition_unfolding,[],[f63,f64,f51]) ).
fof(f66,definition,
sF0 = and(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f67,plain,
and(a,b) = sF0,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF1 = not(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f69,plain,
not(sF0) = sF1,
inference(reorient_equations,[],[f68]) ).
fof(f70,plain,
a11 = sF1,
inference(definition_folding,[],[f53,f69,f67]) ).
fof(f71,definition,
sF2 = and(a11,a),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f72,plain,
and(a11,a) = sF2,
inference(reorient_equations,[],[f71]) ).
fof(f73,definition,
sF3 = not(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f74,plain,
not(sF2) = sF3,
inference(reorient_equations,[],[f73]) ).
fof(f75,plain,
a12 = sF3,
inference(definition_folding,[],[f54,f74,f72]) ).
fof(f76,definition,
sF4 = and(a11,b),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f77,plain,
and(a11,b) = sF4,
inference(reorient_equations,[],[f76]) ).
fof(f78,definition,
sF5 = not(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f79,plain,
not(sF4) = sF5,
inference(reorient_equations,[],[f78]) ).
fof(f80,plain,
a13 = sF5,
inference(definition_folding,[],[f55,f79,f77]) ).
fof(f81,definition,
sF6 = and(a12,a13),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f82,plain,
and(a12,a13) = sF6,
inference(reorient_equations,[],[f81]) ).
fof(f83,definition,
sF7 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f84,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f83]) ).
fof(f85,plain,
a14 = sF7,
inference(definition_folding,[],[f56,f84,f82]) ).
fof(f86,definition,
sF8 = and(a14,carryin),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f87,plain,
and(a14,carryin) = sF8,
inference(reorient_equations,[],[f86]) ).
fof(f88,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f89,plain,
not(sF8) = sF9,
inference(reorient_equations,[],[f88]) ).
fof(f90,plain,
a15 = sF9,
inference(definition_folding,[],[f57,f89,f87]) ).
fof(f91,definition,
sF10 = and(a14,a15),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f92,plain,
and(a14,a15) = sF10,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF11 = not(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f94,plain,
not(sF10) = sF11,
inference(reorient_equations,[],[f93]) ).
fof(f95,plain,
a16 = sF11,
inference(definition_folding,[],[f58,f94,f92]) ).
fof(f96,definition,
sF12 = and(a15,carryin),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f97,plain,
and(a15,carryin) = sF12,
inference(reorient_equations,[],[f96]) ).
fof(f98,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f99,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f98]) ).
fof(f100,plain,
a17 = sF13,
inference(definition_folding,[],[f59,f99,f97]) ).
fof(f101,definition,
sF14 = and(a16,a17),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f102,plain,
and(a16,a17) = sF14,
inference(reorient_equations,[],[f101]) ).
fof(f103,definition,
sF15 = not(sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f104,plain,
not(sF14) = sF15,
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
s1 = sF15,
inference(definition_folding,[],[f60,f104,f102]) ).
fof(f106,definition,
sF16 = and(a11,a15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f107,plain,
and(a11,a15) = sF16,
inference(reorient_equations,[],[f106]) ).
fof(f108,definition,
sF17 = not(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f109,plain,
not(sF16) = sF17,
inference(reorient_equations,[],[f108]) ).
fof(f110,plain,
c1 = sF17,
inference(definition_folding,[],[f61,f109,f107]) ).
fof(f111,definition,
sF18 = not(b),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f112,plain,
not(b) = sF18,
inference(reorient_equations,[],[f111]) ).
fof(f113,definition,
sF19 = and(a,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f114,plain,
and(a,sF18) = sF19,
inference(reorient_equations,[],[f113]) ).
fof(f115,definition,
sF20 = not(a),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f116,plain,
not(a) = sF20,
inference(reorient_equations,[],[f115]) ).
fof(f117,definition,
sF21 = and(b,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f118,plain,
and(b,sF20) = sF21,
inference(reorient_equations,[],[f117]) ).
fof(f119,definition,
sF22 = or(sF19,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f120,plain,
or(sF19,sF21) = sF22,
inference(reorient_equations,[],[f119]) ).
fof(f121,definition,
sF23 = not(carryin),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f122,plain,
not(carryin) = sF23,
inference(reorient_equations,[],[f121]) ).
fof(f123,definition,
sF24 = and(sF22,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f124,plain,
and(sF22,sF23) = sF24,
inference(reorient_equations,[],[f123]) ).
fof(f125,definition,
sF25 = not(sF22),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f126,plain,
not(sF22) = sF25,
inference(reorient_equations,[],[f125]) ).
fof(f127,definition,
sF26 = and(carryin,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f128,plain,
and(carryin,sF25) = sF26,
inference(reorient_equations,[],[f127]) ).
fof(f129,definition,
sF27 = or(sF24,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f130,plain,
or(sF24,sF26) = sF27,
inference(reorient_equations,[],[f129]) ).
fof(f131,definition,
sF28 = or(b,carryin),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f132,plain,
or(b,carryin) = sF28,
inference(reorient_equations,[],[f131]) ).
fof(f133,definition,
sF29 = and(a,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f134,plain,
and(a,sF28) = sF29,
inference(reorient_equations,[],[f133]) ).
fof(f135,definition,
sF30 = and(b,carryin),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f136,plain,
and(b,carryin) = sF30,
inference(reorient_equations,[],[f135]) ).
fof(f137,definition,
sF31 = and(sF20,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f138,plain,
and(sF20,sF30) = sF31,
inference(reorient_equations,[],[f137]) ).
fof(f139,definition,
sF32 = or(sF29,sF31),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f140,plain,
or(sF29,sF31) = sF32,
inference(reorient_equations,[],[f139]) ).
fof(f141,plain,
~ circuit(sF27,sF32),
inference(definition_folding,[],[f65,f140,f138,f136,f116,f134,f132,f130,f128,f126,f120,f118,f116,f114,f112,f124,f122,f120,f118,f116,f114,f112]) ).
fof(f143,plain,
a11 = not(sF0),
inference(forward_demodulation,[],[f69,f70]) ).
fof(f144,plain,
a12 = not(sF2),
inference(forward_demodulation,[],[f74,f75]) ).
fof(f145,plain,
a13 = not(sF4),
inference(forward_demodulation,[],[f79,f80]) ).
fof(f146,plain,
a14 = not(sF6),
inference(forward_demodulation,[],[f84,f85]) ).
fof(f147,plain,
a15 = not(sF8),
inference(forward_demodulation,[],[f89,f90]) ).
fof(f148,plain,
a16 = not(sF10),
inference(forward_demodulation,[],[f94,f95]) ).
fof(f149,plain,
a17 = not(sF12),
inference(forward_demodulation,[],[f99,f100]) ).
fof(f150,plain,
s1 = not(sF14),
inference(forward_demodulation,[],[f104,f105]) ).
fof(f151,plain,
c1 = not(sF16),
inference(forward_demodulation,[],[f109,f110]) ).
fof(f152,plain,
and(a,not(b)) = sF19,
inference(forward_demodulation,[],[f114,f112]) ).
fof(f153,plain,
and(b,not(a)) = sF21,
inference(forward_demodulation,[],[f118,f116]) ).
fof(f154,plain,
sF24 = and(sF23,sF22),
inference(forward_demodulation,[],[f124,f14]) ).
fof(f155,plain,
sF31 = and(sF30,sF20),
inference(forward_demodulation,[],[f138,f14]) ).
fof(f156,plain,
s1 = not(and(a16,a17)),
inference(forward_demodulation,[],[f150,f102]) ).
fof(f157,plain,
sF24 = and(not(carryin),sF22),
inference(forward_demodulation,[],[f154,f122]) ).
fof(f158,plain,
sF31 = and(sF30,not(a)),
inference(forward_demodulation,[],[f155,f116]) ).
fof(f159,plain,
sF31 = and(not(a),sF30),
inference(forward_demodulation,[],[f158,f14]) ).
fof(f160,plain,
and(not(a),and(b,carryin)) = sF31,
inference(forward_demodulation,[],[f159,f136]) ).
fof(f162,plain,
! [X0,X1] : and(X0,X1) = or(n0,and(X0,X1)),
inference(superposition,[],[f42,f28]) ).
fof(f191,plain,
! [X2,X0,X1] : or(and(and(and(X0,X1),X2),not(not(X0))),n0) = or(and(and(X0,X1),X2),n0),
inference(superposition,[],[f49,f28]) ).
fof(f192,plain,
! [X2,X0,X1] : or(and(and(X0,X1),X2),n0) = or(and(and(and(X0,X1),X2),not(not(X1))),n0),
inference(superposition,[],[f49,f26]) ).
fof(f197,plain,
! [X2,X0,X1] : or(and(and(X0,X1),X2),n0) = or(n0,and(and(and(X0,X1),X2),not(not(X1)))),
inference(forward_demodulation,[],[f192,f15]) ).
fof(f198,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = or(and(and(and(X0,X1),X2),not(not(X0))),n0),
inference(forward_demodulation,[],[f191,f15]) ).
fof(f204,plain,
! [X2,X0,X1] : or(and(and(X0,X1),X2),n0) = and(and(and(X0,X1),X2),not(not(X1))),
inference(forward_demodulation,[],[f197,f162]) ).
fof(f205,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = or(n0,and(and(and(X0,X1),X2),not(not(X0)))),
inference(forward_demodulation,[],[f198,f15]) ).
fof(f210,plain,
! [X2,X0,X1] : or(and(and(X0,X1),X2),n0) = and(not(not(X1)),and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f204,f14]) ).
fof(f211,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = and(and(and(X0,X1),X2),not(not(X0))),
inference(forward_demodulation,[],[f205,f162]) ).
fof(f212,plain,
! [X2,X0,X1] : or(and(and(X0,X1),X2),n0) = and(X1,and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f210,f13]) ).
fof(f213,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = and(not(not(X0)),and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f211,f14]) ).
fof(f214,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = and(X1,and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f212,f15]) ).
fof(f215,plain,
! [X2,X0,X1] : or(n0,and(and(X0,X1),X2)) = and(X0,and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f213,f13]) ).
fof(f216,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X1,and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f214,f162]) ).
fof(f217,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X0,and(and(X0,X1),X2)),
inference(forward_demodulation,[],[f215,f162]) ).
fof(f230,plain,
! [X0,X1] : n1 = or(X0,not(and(X1,X0))),
inference(superposition,[],[f32,f41]) ).
fof(f231,plain,
! [X0,X1] : n1 = or(X0,not(and(X0,X1))),
inference(superposition,[],[f32,f42]) ).
fof(f246,plain,
! [X0] : or(n0,X0) = X0,
inference(superposition,[],[f42,f20]) ).
fof(f249,plain,
! [X0,X1] : or(and(and(X0,X1),not(not(X0))),n0) = or(and(X0,X1),n0),
inference(superposition,[],[f49,f20]) ).
fof(f252,plain,
! [X0,X1] : or(n0,and(X0,X1)) = or(and(and(X0,X1),not(not(X0))),n0),
inference(forward_demodulation,[],[f249,f15]) ).
fof(f254,plain,
! [X0,X1] : or(n0,and(X0,X1)) = or(n0,and(and(X0,X1),not(not(X0)))),
inference(forward_demodulation,[],[f252,f15]) ).
fof(f255,plain,
! [X0,X1] : or(n0,and(X0,X1)) = and(and(X0,X1),not(not(X0))),
inference(forward_demodulation,[],[f254,f246]) ).
fof(f256,plain,
! [X0,X1] : or(n0,and(X0,X1)) = and(and(X0,X1),X0),
inference(forward_demodulation,[],[f255,f13]) ).
fof(f257,plain,
! [X0,X1] : or(n0,and(X0,X1)) = and(X0,and(X0,X1)),
inference(forward_demodulation,[],[f256,f14]) ).
fof(f258,plain,
! [X0,X1] : and(X0,X1) = and(X0,and(X0,X1)),
inference(forward_demodulation,[],[f257,f246]) ).
fof(f351,plain,
! [X0] : not(or(X0,sF0)) = and(not(X0),a11),
inference(superposition,[],[f12,f143]) ).
fof(f376,plain,
! [X0] : and(a11,not(X0)) = not(or(X0,sF0)),
inference(forward_demodulation,[],[f351,f14]) ).
fof(f406,plain,
! [X0,X1] : and(or(X0,X1),not(X0)) = or(n0,and(X1,not(X0))),
inference(superposition,[],[f16,f20]) ).
fof(f410,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(X1)) = or(and(X0,not(X1)),n0),
inference(superposition,[],[f16,f28]) ).
fof(f411,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(X2)) = or(and(X0,not(X2)),n0),
inference(superposition,[],[f16,f26]) ).
fof(f412,plain,
! [X0,X1] : or(and(X0,not(X1)),n0) = and(or(X0,X1),not(X1)),
inference(superposition,[],[f16,f20]) ).
fof(f428,plain,
! [X0,X1] : or(and(X0,not(X1)),n0) = and(not(X1),or(X0,X1)),
inference(forward_demodulation,[],[f412,f14]) ).
fof(f429,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(X2)) = or(n0,and(X0,not(X2))),
inference(forward_demodulation,[],[f411,f15]) ).
fof(f430,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(X1)) = or(n0,and(X0,not(X1))),
inference(forward_demodulation,[],[f410,f15]) ).
fof(f432,plain,
! [X0,X1] : and(X1,not(X0)) = and(or(X0,X1),not(X0)),
inference(forward_demodulation,[],[f406,f246]) ).
fof(f438,plain,
! [X0,X1] : and(not(X1),or(X0,X1)) = or(n0,and(X0,not(X1))),
inference(forward_demodulation,[],[f428,f15]) ).
fof(f439,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(X2)) = and(X0,not(X2)),
inference(forward_demodulation,[],[f429,f246]) ).
fof(f440,plain,
! [X2,X0,X1] : and(X0,not(X1)) = and(or(X0,and(X1,X2)),not(X1)),
inference(forward_demodulation,[],[f430,f246]) ).
fof(f441,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(X0,X1)),
inference(forward_demodulation,[],[f432,f14]) ).
fof(f444,plain,
! [X0,X1] : and(X0,not(X1)) = and(not(X1),or(X0,X1)),
inference(forward_demodulation,[],[f438,f246]) ).
fof(f445,plain,
! [X2,X0,X1] : and(X0,not(X2)) = and(not(X2),or(X0,and(X1,X2))),
inference(forward_demodulation,[],[f439,f14]) ).
fof(f446,plain,
! [X2,X0,X1] : and(X0,not(X1)) = and(not(X1),or(X0,and(X1,X2))),
inference(forward_demodulation,[],[f440,f14]) ).
fof(f571,plain,
! [X0] : or(and(sF2,not(X0)),and(a11,X0)) = or(sF2,and(a11,X0)),
inference(superposition,[],[f49,f72]) ).
fof(f572,plain,
! [X0] : or(and(and(a11,X0),not(a)),sF2) = or(and(a11,X0),sF2),
inference(superposition,[],[f49,f72]) ).
fof(f574,plain,
! [X0] : or(sF2,and(a11,X0)) = or(and(and(a11,X0),not(a)),sF2),
inference(forward_demodulation,[],[f572,f15]) ).
fof(f575,plain,
! [X0] : or(sF2,and(a11,X0)) = or(and(a11,X0),and(sF2,not(X0))),
inference(forward_demodulation,[],[f571,f15]) ).
fof(f581,plain,
! [X0] : or(sF2,and(a11,X0)) = or(sF2,and(and(a11,X0),not(a))),
inference(forward_demodulation,[],[f574,f15]) ).
fof(f584,plain,
! [X0] : or(sF2,and(a11,X0)) = or(sF2,and(not(a),and(a11,X0))),
inference(forward_demodulation,[],[f581,f14]) ).
fof(f594,plain,
sF10 = and(a14,sF10),
inference(superposition,[],[f258,f92]) ).
fof(f658,plain,
! [X0] : or(X0,sF8) = or(and(X0,a15),sF8),
inference(superposition,[],[f47,f147]) ).
fof(f664,plain,
! [X0,X1] : or(not(X0),X1) = or(not(or(X0,X1)),X1),
inference(superposition,[],[f47,f12]) ).
fof(f673,plain,
! [X0,X1] : or(not(X0),X1) = or(X1,not(or(X0,X1))),
inference(forward_demodulation,[],[f664,f15]) ).
fof(f677,plain,
! [X0] : or(X0,sF8) = or(sF8,and(X0,a15)),
inference(forward_demodulation,[],[f658,f15]) ).
fof(f690,plain,
! [X0] : or(and(sF8,not(X0)),and(a14,X0)) = or(sF8,and(a14,X0)),
inference(superposition,[],[f49,f87]) ).
fof(f691,plain,
! [X0] : or(and(and(a14,X0),not(carryin)),sF8) = or(and(a14,X0),sF8),
inference(superposition,[],[f49,f87]) ).
fof(f692,plain,
sF8 = and(a14,sF8),
inference(superposition,[],[f258,f87]) ).
fof(f693,plain,
! [X0] : or(sF8,and(a14,X0)) = or(and(and(a14,X0),not(carryin)),sF8),
inference(forward_demodulation,[],[f691,f15]) ).
fof(f694,plain,
! [X0] : or(sF8,and(a14,X0)) = or(and(a14,X0),and(sF8,not(X0))),
inference(forward_demodulation,[],[f690,f15]) ).
fof(f701,plain,
! [X0] : or(sF8,and(a14,X0)) = or(sF8,and(and(a14,X0),not(carryin))),
inference(forward_demodulation,[],[f693,f15]) ).
fof(f726,plain,
and(a16,a17) = not(s1),
inference(superposition,[],[f13,f156]) ).
fof(f727,plain,
sF0 = not(a11),
inference(superposition,[],[f13,f143]) ).
fof(f728,plain,
sF2 = not(a12),
inference(superposition,[],[f13,f144]) ).
fof(f729,plain,
sF4 = not(a13),
inference(superposition,[],[f13,f145]) ).
fof(f730,plain,
sF6 = not(a14),
inference(superposition,[],[f13,f146]) ).
fof(f731,plain,
sF8 = not(a15),
inference(superposition,[],[f13,f147]) ).
fof(f732,plain,
sF10 = not(a16),
inference(superposition,[],[f13,f148]) ).
fof(f733,plain,
sF12 = not(a17),
inference(superposition,[],[f13,f149]) ).
fof(f734,plain,
! [X0,X1] : and(X0,not(X1)) = not(or(not(X0),X1)),
inference(superposition,[],[f12,f13]) ).
fof(f735,plain,
! [X0,X1] : not(or(X1,not(X0))) = and(not(X1),X0),
inference(superposition,[],[f12,f13]) ).
fof(f741,plain,
! [X0,X1] : n1 = or(or(not(X0),X1),X0),
inference(superposition,[],[f32,f13]) ).
fof(f742,plain,
! [X0,X1] : or(X1,not(X0)) = or(and(X1,X0),not(X0)),
inference(superposition,[],[f47,f13]) ).
fof(f746,plain,
! [X0,X1] : or(X1,not(X0)) = or(not(X0),and(X1,X0)),
inference(forward_demodulation,[],[f742,f15]) ).
fof(f747,plain,
! [X0,X1] : n1 = or(X0,or(not(X0),X1)),
inference(forward_demodulation,[],[f741,f15]) ).
fof(f753,plain,
and(a15,carryin) = not(a17),
inference(backward_demodulation,[],[f97,f733]) ).
fof(f776,plain,
and(a14,a15) = not(a16),
inference(backward_demodulation,[],[f92,f732]) ).
fof(f788,plain,
not(a16) = and(a14,not(a16)),
inference(backward_demodulation,[],[f594,f732]) ).
fof(f802,plain,
and(a11,b) = not(a13),
inference(backward_demodulation,[],[f77,f729]) ).
fof(f825,plain,
and(a11,a) = not(a12),
inference(backward_demodulation,[],[f72,f728]) ).
fof(f840,plain,
! [X0] : or(not(a12),and(a11,X0)) = or(and(a11,X0),and(not(a12),not(X0))),
inference(backward_demodulation,[],[f575,f728]) ).
fof(f846,plain,
! [X0] : or(not(a12),and(a11,X0)) = or(not(a12),and(not(a),and(a11,X0))),
inference(backward_demodulation,[],[f584,f728]) ).
fof(f880,plain,
! [X0] : or(not(a12),and(a11,X0)) = or(and(a11,X0),not(or(a12,X0))),
inference(forward_demodulation,[],[f840,f12]) ).
fof(f892,plain,
! [X0,X1] : or(X0,not(X1)) = not(and(not(X0),X1)),
inference(superposition,[],[f11,f13]) ).
fof(f896,plain,
! [X0,X1] : not(and(X1,not(X0))) = or(not(X1),X0),
inference(superposition,[],[f11,f13]) ).
fof(f899,plain,
! [X0] : not(and(X0,sF8)) = or(not(X0),a15),
inference(superposition,[],[f11,f147]) ).
fof(f902,plain,
! [X0,X1] : and(not(X1),not(not(X0))) = and(not(not(X0)),not(and(X0,X1))),
inference(superposition,[],[f441,f11]) ).
fof(f907,plain,
! [X0,X1] : and(not(X1),not(not(X0))) = not(or(not(X0),and(X0,X1))),
inference(forward_demodulation,[],[f902,f12]) ).
fof(f910,plain,
! [X0] : or(a15,not(X0)) = not(and(X0,sF8)),
inference(forward_demodulation,[],[f899,f15]) ).
fof(f919,plain,
! [X0,X1] : and(X0,not(and(X0,X1))) = and(not(X1),not(not(X0))),
inference(forward_demodulation,[],[f907,f734]) ).
fof(f923,plain,
! [X0,X1] : and(X0,not(and(X0,X1))) = not(or(X1,not(X0))),
inference(forward_demodulation,[],[f919,f12]) ).
fof(f924,plain,
! [X0,X1] : and(X0,not(and(X0,X1))) = and(not(X1),X0),
inference(forward_demodulation,[],[f923,f735]) ).
fof(f928,plain,
! [X0,X1] : and(not(not(X0)),and(X0,X1)) = and(and(X0,X1),not(n0)),
inference(superposition,[],[f924,f28]) ).
fof(f929,plain,
! [X0,X1] : and(and(X0,X1),not(n0)) = and(not(not(X1)),and(X0,X1)),
inference(superposition,[],[f924,f26]) ).
fof(f931,plain,
! [X0,X1] : and(not(not(and(X1,X0))),X1) = and(X1,not(and(not(X0),X1))),
inference(superposition,[],[f924,f924]) ).
fof(f933,plain,
and(not(a13),a12) = and(a12,not(sF6)),
inference(superposition,[],[f924,f82]) ).
fof(f935,plain,
and(not(carryin),a14) = and(a14,not(sF8)),
inference(superposition,[],[f924,f87]) ).
fof(f960,plain,
and(a14,a15) = and(not(carryin),a14),
inference(forward_demodulation,[],[f935,f147]) ).
fof(f962,plain,
and(not(a13),a12) = and(a12,a14),
inference(forward_demodulation,[],[f933,f146]) ).
fof(f964,plain,
! [X0,X1] : and(not(not(and(X1,X0))),X1) = and(X1,or(X0,not(X1))),
inference(forward_demodulation,[],[f931,f892]) ).
fof(f966,plain,
! [X0,X1] : and(and(X0,X1),not(n0)) = and(X1,and(X0,X1)),
inference(forward_demodulation,[],[f929,f13]) ).
fof(f967,plain,
! [X0,X1] : and(not(not(X0)),and(X0,X1)) = and(and(X0,X1),n1),
inference(forward_demodulation,[],[f928,f8]) ).
fof(f974,plain,
and(a14,a15) = and(a14,not(carryin)),
inference(forward_demodulation,[],[f960,f14]) ).
fof(f976,plain,
and(a12,a14) = and(a12,not(a13)),
inference(forward_demodulation,[],[f962,f14]) ).
fof(f978,plain,
! [X0,X1] : and(X1,or(X0,not(X1))) = and(X1,not(not(and(X1,X0)))),
inference(forward_demodulation,[],[f964,f14]) ).
fof(f980,plain,
! [X0,X1] : and(X1,and(X0,X1)) = and(and(X0,X1),n1),
inference(forward_demodulation,[],[f966,f8]) ).
fof(f981,plain,
! [X0,X1] : and(not(not(X0)),and(X0,X1)) = and(n1,and(X0,X1)),
inference(forward_demodulation,[],[f967,f14]) ).
fof(f984,plain,
not(a16) = and(a14,not(carryin)),
inference(forward_demodulation,[],[f974,f776]) ).
fof(f987,plain,
! [X0,X1] : and(X1,or(X0,not(X1))) = and(X1,and(X1,X0)),
inference(forward_demodulation,[],[f978,f13]) ).
fof(f989,plain,
! [X0,X1] : and(X1,and(X0,X1)) = and(n1,and(X0,X1)),
inference(forward_demodulation,[],[f980,f14]) ).
fof(f990,plain,
! [X0,X1] : and(X0,and(X0,X1)) = and(n1,and(X0,X1)),
inference(forward_demodulation,[],[f981,f13]) ).
fof(f995,plain,
! [X0,X1] : and(X1,X0) = and(X1,or(X0,not(X1))),
inference(forward_demodulation,[],[f987,f258]) ).
fof(f997,plain,
! [X0,X1] : and(X0,X1) = and(n1,and(X0,X1)),
inference(forward_demodulation,[],[f990,f258]) ).
fof(f999,plain,
! [X0,X1] : and(X0,X1) = and(X1,and(X0,X1)),
inference(backward_demodulation,[],[f989,f997]) ).
fof(f1036,plain,
and(not(b),a) = and(a,not(sF0)),
inference(superposition,[],[f924,f67]) ).
fof(f1038,plain,
and(not(b),a) = and(a,a11),
inference(forward_demodulation,[],[f1036,f143]) ).
fof(f1046,plain,
and(a11,a) = and(not(b),a),
inference(forward_demodulation,[],[f1038,f14]) ).
fof(f1050,plain,
and(a11,a) = and(a,not(b)),
inference(forward_demodulation,[],[f1046,f14]) ).
fof(f1052,plain,
and(a11,a) = sF19,
inference(forward_demodulation,[],[f1050,f152]) ).
fof(f1053,plain,
sF19 = not(a12),
inference(forward_demodulation,[],[f1052,f825]) ).
fof(f1054,plain,
and(a,not(b)) = not(a12),
inference(backward_demodulation,[],[f152,f1053]) ).
fof(f1055,plain,
sF22 = or(not(a12),sF21),
inference(backward_demodulation,[],[f120,f1053]) ).
fof(f1071,plain,
! [X2,X0,X1] : or(and(X0,X2),not(X2)) = or(or(and(X0,X1),and(X0,X2)),not(X2)),
inference(superposition,[],[f43,f49]) ).
fof(f1086,plain,
! [X2,X0,X1] : or(and(X0,X2),not(X2)) = or(or(and(X0,X1),not(X2)),and(X0,X2)),
inference(forward_demodulation,[],[f1071,f18]) ).
fof(f1101,plain,
! [X2,X0,X1] : or(and(X0,X2),not(X2)) = or(and(X0,X2),or(and(X0,X1),not(X2))),
inference(forward_demodulation,[],[f1086,f15]) ).
fof(f1102,plain,
! [X2,X0,X1] : or(and(X0,X2),or(and(X0,X1),not(X2))) = or(not(X2),and(X0,X2)),
inference(forward_demodulation,[],[f1101,f15]) ).
fof(f1103,plain,
! [X2,X0,X1] : or(X0,not(X2)) = or(and(X0,X2),or(and(X0,X1),not(X2))),
inference(forward_demodulation,[],[f1102,f746]) ).
fof(f1155,plain,
! [X0,X1] : and(and(X0,X1),not(and(X0,X1))) = and(not(X1),and(X0,X1)),
inference(superposition,[],[f924,f34]) ).
fof(f1157,plain,
! [X0,X1] : n0 = and(not(X1),and(X0,X1)),
inference(forward_demodulation,[],[f1155,f20]) ).
fof(f1256,plain,
sF16 = not(c1),
inference(superposition,[],[f13,f151]) ).
fof(f1273,plain,
and(a11,a15) = not(c1),
inference(backward_demodulation,[],[f107,f1256]) ).
fof(f1328,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X2,and(X0,and(X1,X2))),
inference(superposition,[],[f216,f999]) ).
fof(f1442,plain,
! [X0,X1] : or(X0,and(X0,X1)) = X0,
inference(superposition,[],[f42,f15]) ).
fof(f1443,plain,
! [X0,X1] : or(X0,and(X1,X0)) = X0,
inference(superposition,[],[f41,f15]) ).
fof(f1447,plain,
! [X2,X0,X1] : or(and(X0,X2),and(X0,X1)) = or(and(X0,X1),and(and(X0,X2),not(X1))),
inference(superposition,[],[f49,f15]) ).
fof(f1596,plain,
! [X0] : and(n1,X0) = X0,
inference(superposition,[],[f999,f3]) ).
fof(f2015,plain,
! [X2,X0,X1] : and(or(X1,X2),X0) = or(and(X0,X1),and(X2,X0)),
inference(superposition,[],[f16,f14]) ).
fof(f2024,plain,
! [X2,X0,X1] : or(X2,X0) = or(or(and(X0,X1),X2),X0),
inference(superposition,[],[f43,f14]) ).
fof(f2025,plain,
! [X2,X0,X1] : or(X2,X0) = or(or(X2,and(X0,X1)),X0),
inference(superposition,[],[f45,f14]) ).
fof(f2027,plain,
! [X2,X0,X1] : or(and(X1,X2),and(X0,X1)) = or(and(and(X1,X2),not(X0)),and(X0,X1)),
inference(superposition,[],[f49,f14]) ).
fof(f2030,plain,
! [X0,X1] : and(not(X0),X1) = and(X1,not(and(X0,X1))),
inference(superposition,[],[f924,f14]) ).
fof(f2037,plain,
! [X0,X1] : n0 = and(not(X0),and(X0,X1)),
inference(superposition,[],[f28,f14]) ).
fof(f2039,plain,
! [X2,X0,X1] : or(and(X1,X2),and(X1,X0)) = or(and(not(X0),and(X1,X2)),and(X1,X0)),
inference(superposition,[],[f49,f14]) ).
fof(f2052,plain,
! [X2,X0,X1] : or(and(X1,X2),and(X1,X0)) = or(and(X1,X0),and(not(X0),and(X1,X2))),
inference(forward_demodulation,[],[f2039,f15]) ).
fof(f2054,plain,
! [X2,X0,X1] : or(and(X1,X2),and(X0,X1)) = or(and(X0,X1),and(and(X1,X2),not(X0))),
inference(forward_demodulation,[],[f2027,f15]) ).
fof(f2056,plain,
! [X2,X0,X1] : or(X2,X0) = or(or(X2,X0),and(X0,X1)),
inference(forward_demodulation,[],[f2025,f18]) ).
fof(f2057,plain,
! [X2,X0,X1] : or(X2,X0) = or(X0,or(and(X0,X1),X2)),
inference(forward_demodulation,[],[f2024,f15]) ).
fof(f2072,plain,
! [X2,X0,X1] : and(or(X2,X0),X1) = or(and(X0,X1),and(and(X1,X2),not(X0))),
inference(forward_demodulation,[],[f2054,f2015]) ).
fof(f2078,plain,
! [X0,X1] : and(or(X0,X1),X0) = or(X0,and(X1,X0)),
inference(superposition,[],[f16,f23]) ).
fof(f2079,plain,
! [X0,X1] : or(and(X1,X0),X0) = and(or(X1,X0),X0),
inference(superposition,[],[f16,f23]) ).
fof(f2106,plain,
! [X0,X1] : or(and(X1,X0),X0) = and(X0,or(X1,X0)),
inference(forward_demodulation,[],[f2079,f14]) ).
fof(f2107,plain,
! [X0,X1] : and(or(X0,X1),X0) = X0,
inference(forward_demodulation,[],[f2078,f1443]) ).
fof(f2109,plain,
! [X0,X1] : and(X0,or(X1,X0)) = X0,
inference(forward_demodulation,[],[f2106,f41]) ).
fof(f2110,plain,
! [X0,X1] : and(X0,or(X0,X1)) = X0,
inference(forward_demodulation,[],[f2107,f14]) ).
fof(f2115,plain,
n0 = and(sF24,not(not(carryin))),
inference(superposition,[],[f28,f157]) ).
fof(f2142,plain,
n0 = and(sF24,carryin),
inference(forward_demodulation,[],[f2115,f13]) ).
fof(f2149,plain,
n0 = and(carryin,sF24),
inference(forward_demodulation,[],[f2142,f14]) ).
fof(f2180,plain,
! [X0] : and(sF29,X0) = and(a,and(sF29,X0)),
inference(superposition,[],[f217,f134]) ).
fof(f2274,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(and(X1,X2),X0),
inference(superposition,[],[f17,f14]) ).
fof(f2351,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X1,and(X0,X2)),
inference(superposition,[],[f14,f17]) ).
fof(f2465,plain,
! [X0,X1] : n0 = and(X1,and(X0,not(X1))),
inference(backward_demodulation,[],[f26,f2351]) ).
fof(f2466,plain,
! [X2,X0,X1] : and(or(X2,X0),X1) = or(and(X0,X1),and(X2,and(X1,not(X0)))),
inference(backward_demodulation,[],[f2072,f2351]) ).
fof(f2468,plain,
! [X2,X0,X1] : or(and(X0,X2),and(X0,X1)) = or(and(X0,X1),and(X2,and(X0,not(X1)))),
inference(backward_demodulation,[],[f1447,f2351]) ).
fof(f2474,plain,
! [X0] : or(sF8,and(a14,X0)) = or(sF8,and(X0,and(a14,not(carryin)))),
inference(backward_demodulation,[],[f701,f2351]) ).
fof(f2546,plain,
! [X2,X0,X1] : and(and(X1,X2),X0) = and(X1,and(X0,X2)),
inference(forward_demodulation,[],[f2274,f2351]) ).
fof(f2593,plain,
! [X0] : or(sF8,and(a14,X0)) = or(sF8,and(X0,not(a16))),
inference(forward_demodulation,[],[f2474,f984]) ).
fof(f2679,plain,
! [X2,X0,X1] : and(and(X0,X2),X1) = and(X0,and(X2,X1)),
inference(backward_demodulation,[],[f17,f2546]) ).
fof(f2889,plain,
! [X2,X0,X1] : and(or(X0,X1),and(X2,not(X0))) = or(n0,and(X1,and(X2,not(X0)))),
inference(superposition,[],[f16,f2465]) ).
fof(f2906,plain,
! [X2,X0,X1] : and(or(X0,X1),and(X2,not(X0))) = and(X1,and(X2,not(X0))),
inference(forward_demodulation,[],[f2889,f246]) ).
fof(f2927,plain,
! [X0] : and(sF21,X0) = and(not(a),and(b,X0)),
inference(superposition,[],[f2351,f153]) ).
fof(f2931,plain,
! [X0] : and(sF24,X0) = and(sF22,and(not(carryin),X0)),
inference(superposition,[],[f2351,f157]) ).
fof(f2945,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X2,and(X1,X0)),
inference(superposition,[],[f14,f2351]) ).
fof(f2987,plain,
sF31 = and(sF21,carryin),
inference(backward_demodulation,[],[f160,f2927]) ).
fof(f3003,plain,
sF31 = and(carryin,sF21),
inference(forward_demodulation,[],[f2987,f14]) ).
fof(f3205,plain,
! [X0,X1] : and(X1,X0) = and(X0,or(X1,not(X0))),
inference(superposition,[],[f444,f13]) ).
fof(f3221,plain,
! [X2,X0,X1] : and(and(X0,X2),not(and(X1,X2))) = and(not(and(X1,X2)),and(or(X0,X1),X2)),
inference(superposition,[],[f444,f16]) ).
fof(f3238,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(or(and(X0,not(X1)),X2),or(X0,X1)),
inference(superposition,[],[f43,f444]) ).
fof(f3250,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(or(X0,X1),or(and(X0,not(X1)),X2)),
inference(forward_demodulation,[],[f3238,f15]) ).
fof(f3261,plain,
! [X2,X0,X1] : and(and(X0,X2),not(and(X1,X2))) = and(X2,and(or(X0,X1),not(and(X1,X2)))),
inference(forward_demodulation,[],[f3221,f2945]) ).
fof(f3274,plain,
! [X2,X0,X1] : and(X2,and(or(X0,X1),not(and(X1,X2)))) = and(X2,and(X0,not(and(X1,X2)))),
inference(forward_demodulation,[],[f3261,f2351]) ).
fof(f3518,plain,
! [X2,X0,X1] : or(or(X0,X1),X2) = or(or(X1,X2),X0),
inference(superposition,[],[f18,f15]) ).
fof(f3529,plain,
! [X2,X3,X0,X1] : or(or(or(X0,and(X2,X1)),X3),X1) = or(or(X0,X1),X3),
inference(superposition,[],[f18,f45]) ).
fof(f3564,plain,
! [X2,X0,X1] : or(or(X0,X1),X2) = or(X1,or(X0,X2)),
inference(superposition,[],[f15,f18]) ).
fof(f3578,plain,
! [X2,X0,X1] : or(X0,X2) = or(and(X1,X2),or(X0,X2)),
inference(backward_demodulation,[],[f45,f3564]) ).
fof(f3583,plain,
! [X2,X0,X1] : or(X2,X0) = or(X0,or(X2,and(X0,X1))),
inference(backward_demodulation,[],[f2056,f3564]) ).
fof(f3588,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(X1,or(X0,or(and(X0,not(X1)),X2))),
inference(backward_demodulation,[],[f3250,f3564]) ).
fof(f3595,plain,
! [X0,X1] : n1 = or(X1,or(X0,not(X1))),
inference(backward_demodulation,[],[f30,f3564]) ).
fof(f3629,plain,
! [X2,X3,X0,X1] : or(or(or(X0,and(X2,X1)),X3),X1) = or(X1,or(X0,X3)),
inference(forward_demodulation,[],[f3529,f3564]) ).
fof(f3639,plain,
! [X2,X0,X1] : or(or(X1,X2),X0) = or(X1,or(X0,X2)),
inference(forward_demodulation,[],[f3518,f3564]) ).
fof(f3678,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(X1,or(X2,X0)),
inference(forward_demodulation,[],[f3588,f2057]) ).
fof(f3697,plain,
! [X2,X3,X0,X1] : or(X1,or(X0,X3)) = or(X3,or(or(X0,and(X2,X1)),X1)),
inference(forward_demodulation,[],[f3629,f3564]) ).
fof(f3707,plain,
! [X2,X0,X1] : or(or(X0,X2),X1) = or(X0,or(X2,X1)),
inference(backward_demodulation,[],[f18,f3639]) ).
fof(f3741,plain,
! [X2,X3,X0,X1] : or(X1,or(X0,X3)) = or(X3,or(and(X2,X1),or(X0,X1))),
inference(forward_demodulation,[],[f3697,f3564]) ).
fof(f3756,plain,
! [X3,X0,X1] : or(X1,or(X0,X3)) = or(X3,or(X0,X1)),
inference(forward_demodulation,[],[f3741,f3578]) ).
fof(f3839,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(X1,or(and(X0,not(X1)),X2)),
inference(superposition,[],[f3756,f47]) ).
fof(f3840,plain,
! [X2,X0,X1] : or(X2,not(and(X0,X1))) = or(not(X1),or(not(X0),X2)),
inference(superposition,[],[f3756,f11]) ).
fof(f4084,plain,
! [X2,X0,X1] : or(not(X0),not(X2)) = or(and(not(X0),X2),or(not(or(X0,X1)),not(X2))),
inference(superposition,[],[f1103,f12]) ).
fof(f4093,plain,
! [X2,X0,X1] : or(X1,X0) = or(and(X1,not(X0)),or(and(X1,X2),X0)),
inference(superposition,[],[f1103,f13]) ).
fof(f4132,plain,
! [X2,X0,X1] : or(X1,X0) = or(X0,or(and(X1,not(X0)),and(X1,X2))),
inference(forward_demodulation,[],[f4093,f3678]) ).
fof(f4141,plain,
! [X2,X0,X1] : or(not(X0),not(X2)) = or(not(X2),or(and(not(X0),X2),not(or(X0,X1)))),
inference(forward_demodulation,[],[f4084,f3678]) ).
fof(f4187,plain,
! [X2,X0,X1] : or(X1,X0) = or(and(X1,X2),or(X1,X0)),
inference(forward_demodulation,[],[f4132,f3839]) ).
fof(f4191,plain,
! [X2,X0,X1] : not(and(X0,X2)) = or(not(X2),or(and(not(X0),X2),not(or(X0,X1)))),
inference(forward_demodulation,[],[f4141,f11]) ).
fof(f4219,plain,
! [X2,X0,X1] : or(X1,X0) = or(X1,or(X0,and(X1,X2))),
inference(forward_demodulation,[],[f4187,f3678]) ).
fof(f4300,plain,
and(not(a15),a14) = and(a14,not(not(a16))),
inference(superposition,[],[f924,f776]) ).
fof(f4311,plain,
and(not(a15),a14) = and(a14,a16),
inference(forward_demodulation,[],[f4300,f13]) ).
fof(f4320,plain,
and(not(a15),a14) = and(a16,a14),
inference(forward_demodulation,[],[f4311,f14]) ).
fof(f4325,plain,
and(a16,a14) = and(a14,not(a15)),
inference(forward_demodulation,[],[f4320,f14]) ).
fof(f4327,plain,
and(a14,sF8) = and(a16,a14),
inference(forward_demodulation,[],[f4325,f731]) ).
fof(f4329,plain,
sF8 = and(a16,a14),
inference(forward_demodulation,[],[f4327,f692]) ).
fof(f4380,plain,
not(a12) = and(a,not(a12)),
inference(superposition,[],[f999,f825]) ).
fof(f4514,plain,
! [X0,X1] : and(not(X0),X1) = and(not(X0),or(X1,X0)),
inference(superposition,[],[f995,f13]) ).
fof(f4526,plain,
! [X0,X1] : and(X1,not(X0)) = and(X1,not(and(X0,X1))),
inference(superposition,[],[f995,f11]) ).
fof(f4624,plain,
! [X0,X1] : and(not(not(X1)),not(X0)) = and(not(not(X1)),not(and(X0,X1))),
inference(superposition,[],[f4514,f11]) ).
fof(f4668,plain,
! [X0,X1] : and(not(not(X1)),not(X0)) = not(or(not(X1),and(X0,X1))),
inference(forward_demodulation,[],[f4624,f12]) ).
fof(f4686,plain,
! [X0,X1] : and(not(not(X1)),not(X0)) = and(X1,not(and(X0,X1))),
inference(forward_demodulation,[],[f4668,f734]) ).
fof(f4700,plain,
! [X0,X1] : and(not(X0),X1) = and(not(not(X1)),not(X0)),
inference(forward_demodulation,[],[f4686,f2030]) ).
fof(f4707,plain,
! [X0,X1] : and(not(X0),X1) = not(or(not(X1),X0)),
inference(forward_demodulation,[],[f4700,f12]) ).
fof(f4867,plain,
! [X2,X3,X0,X1] : or(X3,or(X2,or(X0,X1))) = or(X0,or(X1,or(X2,X3))),
inference(superposition,[],[f3756,f3707]) ).
fof(f4953,plain,
! [X2,X0,X1] : and(or(X2,X1),X0) = or(and(X0,X1),and(X2,and(X0,not(X1)))),
inference(superposition,[],[f2466,f14]) ).
fof(f5081,plain,
! [X2,X0,X1] : or(and(X0,X2),and(X0,X1)) = and(or(X2,X1),X0),
inference(backward_demodulation,[],[f2468,f4953]) ).
fof(f5132,plain,
! [X2,X0,X1] : and(or(X2,X0),X1) = or(and(X1,X0),and(not(X0),and(X1,X2))),
inference(backward_demodulation,[],[f2052,f5081]) ).
fof(f5247,plain,
! [X2,X0,X1] : or(and(not(X0),X1),not(X2)) = not(and(or(X0,not(X1)),X2)),
inference(superposition,[],[f892,f892]) ).
fof(f5262,plain,
! [X0,X1] : not(and(X0,not(X1))) = or(X1,not(or(X1,X0))),
inference(superposition,[],[f892,f441]) ).
fof(f5271,plain,
not(sF24) = or(carryin,not(sF22)),
inference(superposition,[],[f892,f157]) ).
fof(f5276,plain,
! [X2,X0,X1] : not(or(X2,and(not(X0),X1))) = and(not(X2),or(X0,not(X1))),
inference(superposition,[],[f12,f892]) ).
fof(f5308,plain,
not(sF24) = or(carryin,sF25),
inference(forward_demodulation,[],[f5271,f126]) ).
fof(f5317,plain,
! [X0,X1] : or(not(X0),X1) = or(X1,not(or(X1,X0))),
inference(forward_demodulation,[],[f5262,f896]) ).
fof(f5325,plain,
! [X2,X0,X1] : not(and(X0,X2)) = or(not(X2),not(and(or(X0,not(X2)),or(X0,X1)))),
inference(backward_demodulation,[],[f4191,f5247]) ).
fof(f5346,plain,
! [X2,X0,X1] : not(and(X0,X2)) = not(and(X2,and(or(X0,not(X2)),or(X0,X1)))),
inference(forward_demodulation,[],[f5325,f11]) ).
fof(f5371,plain,
! [X0] : and(or(X0,a16),a14) = or(sF8,and(X0,and(a14,not(a16)))),
inference(superposition,[],[f2466,f4329]) ).
fof(f5374,plain,
! [X0] : or(sF8,and(X0,not(a16))) = and(or(X0,a16),a14),
inference(forward_demodulation,[],[f5371,f788]) ).
fof(f5383,plain,
! [X0] : or(sF8,and(X0,not(a16))) = and(a14,or(X0,a16)),
inference(forward_demodulation,[],[f5374,f14]) ).
fof(f5387,plain,
! [X0] : or(sF8,and(a14,X0)) = and(a14,or(X0,a16)),
inference(backward_demodulation,[],[f2593,f5383]) ).
fof(f5390,plain,
! [X0] : or(and(a14,X0),and(sF8,not(X0))) = and(a14,or(X0,a16)),
inference(backward_demodulation,[],[f694,f5387]) ).
fof(f5410,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X0,and(or(X1,not(X0)),X2)),
inference(superposition,[],[f2679,f995]) ).
fof(f5418,plain,
! [X0] : and(sF6,X0) = and(a12,and(a13,X0)),
inference(superposition,[],[f2679,f82]) ).
fof(f5444,plain,
! [X2,X0,X1] : and(X2,and(X0,X1)) = and(X0,and(X1,X2)),
inference(superposition,[],[f14,f2679]) ).
fof(f5503,plain,
! [X2,X0,X1] : and(X1,and(X0,X2)) = and(X0,and(or(X1,not(X0)),X2)),
inference(forward_demodulation,[],[f5410,f2351]) ).
fof(f5531,plain,
! [X2,X0,X1] : not(and(X0,X2)) = not(and(X0,and(X2,or(X0,X1)))),
inference(backward_demodulation,[],[f5346,f5503]) ).
fof(f5570,plain,
! [X2,X0,X1] : and(X2,not(not(X0))) = and(not(not(X0)),or(X2,not(or(X0,X1)))),
inference(superposition,[],[f446,f12]) ).
fof(f5623,plain,
! [X2,X3,X0,X1] : or(X2,or(X0,and(X1,X3))) = or(and(X0,not(X1)),or(X2,or(X0,and(X1,X3)))),
inference(superposition,[],[f3578,f446]) ).
fof(f5624,plain,
! [X2,X3,X0,X1] : or(X2,or(X0,and(X1,X3))) = or(X0,or(and(X1,X3),or(X2,and(X0,not(X1))))),
inference(forward_demodulation,[],[f5623,f4867]) ).
fof(f5654,plain,
! [X2,X0,X1] : and(X2,not(not(X0))) = not(or(not(X0),and(not(X2),or(X0,X1)))),
inference(forward_demodulation,[],[f5570,f5276]) ).
fof(f5682,plain,
! [X2,X0,X1] : and(X2,not(not(X0))) = and(X0,not(and(not(X2),or(X0,X1)))),
inference(forward_demodulation,[],[f5654,f734]) ).
fof(f5698,plain,
! [X2,X0,X1] : and(X2,not(not(X0))) = and(X0,or(X2,not(or(X0,X1)))),
inference(forward_demodulation,[],[f5682,f892]) ).
fof(f5707,plain,
! [X2,X0,X1] : and(X2,X0) = and(X0,or(X2,not(or(X0,X1)))),
inference(forward_demodulation,[],[f5698,f13]) ).
fof(f5750,plain,
! [X2,X0,X1] : and(and(X0,not(not(or(X1,X2)))),X1) = and(X1,or(X0,not(or(X1,X2)))),
inference(superposition,[],[f5707,f47]) ).
fof(f5811,plain,
! [X2,X0,X1] : and(X0,X1) = and(and(X0,not(not(or(X1,X2)))),X1),
inference(forward_demodulation,[],[f5750,f5707]) ).
fof(f5846,plain,
! [X2,X0,X1] : and(X0,X1) = and(not(not(or(X1,X2))),and(X0,X1)),
inference(forward_demodulation,[],[f5811,f2351]) ).
fof(f5867,plain,
! [X2,X0,X1] : and(X0,X1) = and(X1,and(X0,not(not(or(X1,X2))))),
inference(forward_demodulation,[],[f5846,f2945]) ).
fof(f5877,plain,
! [X2,X0,X1] : and(X0,X1) = and(X1,and(X0,or(X1,X2))),
inference(forward_demodulation,[],[f5867,f13]) ).
fof(f5882,plain,
! [X2,X0] : not(and(X0,X2)) = not(and(X2,X0)),
inference(backward_demodulation,[],[f5531,f5877]) ).
fof(f6013,plain,
! [X2,X0,X1] : and(X2,X1) = and(X1,and(X2,or(X0,X1))),
inference(superposition,[],[f5877,f15]) ).
fof(f6079,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = or(and(X0,or(X1,X2)),and(X0,X1)),
inference(superposition,[],[f1443,f5877]) ).
fof(f6105,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(or(or(X1,X2),X1),X0),
inference(forward_demodulation,[],[f6079,f5081]) ).
fof(f6141,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(or(X2,or(X1,X1)),X0),
inference(forward_demodulation,[],[f6105,f3564]) ).
fof(f6154,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(or(X2,X1),X0),
inference(forward_demodulation,[],[f6141,f24]) ).
fof(f6401,plain,
! [X2,X0,X1] : and(not(X2),not(and(X0,X1))) = not(or(X2,and(X1,X0))),
inference(superposition,[],[f12,f5882]) ).
fof(f6411,plain,
! [X2,X0,X1] : or(and(X1,X0),not(X2)) = not(and(not(and(X0,X1)),X2)),
inference(superposition,[],[f892,f5882]) ).
fof(f6422,plain,
! [X2,X0,X1] : or(and(X0,X1),not(X2)) = or(and(X1,X0),not(X2)),
inference(forward_demodulation,[],[f6411,f892]) ).
fof(f6428,plain,
! [X2,X0,X1] : not(or(X2,and(X0,X1))) = not(or(X2,and(X1,X0))),
inference(forward_demodulation,[],[f6401,f12]) ).
fof(f6502,plain,
! [X0] : or(X0,a12) = or(a12,or(X0,sF6)),
inference(superposition,[],[f3583,f82]) ).
fof(f6524,plain,
! [X2,X3,X0,X1] : or(or(X0,X1),X2) = or(X2,or(X0,or(X1,and(X2,X3)))),
inference(superposition,[],[f3583,f3707]) ).
fof(f6550,plain,
! [X2,X3,X0,X1] : or(X1,or(X0,X2)) = or(X2,or(X0,or(X1,and(X2,X3)))),
inference(forward_demodulation,[],[f6524,f3564]) ).
fof(f6570,plain,
! [X2,X3,X0,X1] : or(X2,or(and(X1,X3),X0)) = or(X2,or(X0,and(X1,X3))),
inference(backward_demodulation,[],[f5624,f6550]) ).
fof(f6842,plain,
! [X0] : and(X0,not(a15)) = and(not(a15),or(X0,not(a16))),
inference(superposition,[],[f445,f776]) ).
fof(f6846,plain,
! [X0] : and(X0,not(sF21)) = and(not(sF21),or(X0,sF31)),
inference(superposition,[],[f445,f3003]) ).
fof(f6859,plain,
! [X2,X0,X1] : and(and(X1,X2),not(and(X2,not(X1)))) = and(not(and(X2,not(X1))),and(or(X0,X1),X2)),
inference(superposition,[],[f445,f2466]) ).
fof(f6919,plain,
! [X2,X0,X1] : and(and(X1,X2),not(and(X2,not(X1)))) = and(X2,and(or(X0,X1),not(and(X2,not(X1))))),
inference(forward_demodulation,[],[f6859,f2945]) ).
fof(f6926,plain,
! [X0] : and(X0,not(a15)) = not(or(a15,and(not(X0),a16))),
inference(forward_demodulation,[],[f6842,f5276]) ).
fof(f6960,plain,
! [X2,X0,X1] : and(and(X1,X2),or(not(X2),X1)) = and(X2,and(or(X0,X1),or(not(X2),X1))),
inference(forward_demodulation,[],[f6919,f896]) ).
fof(f6964,plain,
! [X0] : and(X0,not(a15)) = not(or(a15,and(a16,not(X0)))),
inference(forward_demodulation,[],[f6926,f6428]) ).
fof(f6985,plain,
! [X2,X0,X1] : and(X2,and(or(X0,X1),or(not(X2),X1))) = and(X2,and(X1,or(not(X2),X1))),
inference(forward_demodulation,[],[f6960,f2351]) ).
fof(f6987,plain,
! [X0] : and(X0,sF8) = not(or(a15,and(a16,not(X0)))),
inference(forward_demodulation,[],[f6964,f731]) ).
fof(f6999,plain,
! [X2,X0,X1] : and(X2,X1) = and(X2,and(or(X0,X1),or(not(X2),X1))),
inference(forward_demodulation,[],[f6985,f2109]) ).
fof(f7511,plain,
! [X0] : and(or(carryin,X0),sF24) = or(n0,and(X0,sF24)),
inference(superposition,[],[f16,f2149]) ).
fof(f7547,plain,
! [X0] : and(X0,sF24) = and(or(carryin,X0),sF24),
inference(forward_demodulation,[],[f7511,f246]) ).
fof(f7834,plain,
! [X0] : and(sF8,not(X0)) = not(or(a15,X0)),
inference(superposition,[],[f734,f147]) ).
fof(f7837,plain,
not(sF22) = and(a12,not(sF21)),
inference(superposition,[],[f734,f1055]) ).
fof(f7848,plain,
! [X2,X0,X1] : and(X2,not(or(X1,X0))) = not(or(X0,or(X1,not(X2)))),
inference(superposition,[],[f734,f3756]) ).
fof(f7857,plain,
! [X2,X0,X1] : not(or(X2,or(not(X0),X1))) = and(not(X2),and(X0,not(X1))),
inference(superposition,[],[f12,f734]) ).
fof(f7912,plain,
sF25 = and(a12,not(sF21)),
inference(forward_demodulation,[],[f7837,f126]) ).
fof(f7916,plain,
! [X0] : and(a14,or(X0,a16)) = or(and(a14,X0),not(or(a15,X0))),
inference(backward_demodulation,[],[f5390,f7834]) ).
fof(f7972,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X1,X0)),
inference(superposition,[],[f4219,f3]) ).
fof(f8115,plain,
or(sF21,not(a12)) = or(sF21,sF22),
inference(superposition,[],[f7972,f1055]) ).
fof(f8167,plain,
or(not(a12),sF21) = or(sF21,sF22),
inference(forward_demodulation,[],[f8115,f15]) ).
fof(f8202,plain,
sF22 = or(sF21,sF22),
inference(forward_demodulation,[],[f8167,f1055]) ).
fof(f8259,plain,
! [X0] : and(X0,sF21) = and(sF21,or(X0,not(sF22))),
inference(superposition,[],[f5707,f8202]) ).
fof(f8265,plain,
! [X0] : and(X0,sF21) = and(sF21,or(X0,sF25)),
inference(forward_demodulation,[],[f8259,f126]) ).
fof(f8450,plain,
! [X2,X0,X1] : and(X1,X2) = and(and(X1,X2),and(or(X0,X1),X2)),
inference(superposition,[],[f2110,f2466]) ).
fof(f8546,plain,
! [X2,X0,X1] : and(X1,X2) = and(X2,and(X1,and(or(X0,X1),X2))),
inference(forward_demodulation,[],[f8450,f2351]) ).
fof(f8561,plain,
! [X2,X0,X1] : and(X1,X2) = and(X1,and(or(X0,X1),X2)),
inference(forward_demodulation,[],[f8546,f1328]) ).
fof(f9069,plain,
! [X2,X0,X1] : and(or(not(X0),X1),and(X2,X0)) = or(n0,and(X1,and(X2,X0))),
inference(superposition,[],[f16,f1157]) ).
fof(f9108,plain,
! [X2,X0,X1] : and(X1,and(X2,X0)) = and(or(not(X0),X1),and(X2,X0)),
inference(forward_demodulation,[],[f9069,f246]) ).
fof(f9166,plain,
! [X2,X0,X1] : and(X1,and(X2,X0)) = and(X0,and(X2,or(not(X0),X1))),
inference(forward_demodulation,[],[f9108,f2945]) ).
fof(f9208,plain,
! [X2,X0,X1] : and(X2,X1) = and(X1,and(or(X0,X1),X2)),
inference(backward_demodulation,[],[f6999,f9166]) ).
fof(f9564,plain,
! [X2,X0,X1] : and(not(X1),and(X2,not(not(X0)))) = and(not(and(X0,X1)),and(X2,not(not(X0)))),
inference(superposition,[],[f2906,f11]) ).
fof(f9701,plain,
! [X2,X0,X1] : and(not(X1),and(X2,not(not(X0)))) = not(or(and(X0,X1),or(not(X2),not(X0)))),
inference(forward_demodulation,[],[f9564,f7857]) ).
fof(f9755,plain,
! [X2,X0,X1] : and(not(X1),and(X2,not(not(X0)))) = and(X0,not(or(not(X2),and(X0,X1)))),
inference(forward_demodulation,[],[f9701,f7848]) ).
fof(f9782,plain,
! [X2,X0,X1] : and(X0,and(X2,not(and(X0,X1)))) = and(not(X1),and(X2,not(not(X0)))),
inference(forward_demodulation,[],[f9755,f734]) ).
fof(f9795,plain,
! [X2,X0,X1] : and(X0,and(X2,not(and(X0,X1)))) = not(or(X1,or(not(X2),not(X0)))),
inference(forward_demodulation,[],[f9782,f7857]) ).
fof(f9802,plain,
! [X2,X0,X1] : and(X0,and(X2,not(and(X0,X1)))) = and(X0,not(or(not(X2),X1))),
inference(forward_demodulation,[],[f9795,f7848]) ).
fof(f9804,plain,
! [X2,X0,X1] : and(X0,and(X2,not(X1))) = and(X0,and(X2,not(and(X0,X1)))),
inference(forward_demodulation,[],[f9802,f734]) ).
fof(f10338,plain,
! [X0] : and(or(X0,b),a) = or(and(b,a),and(X0,not(a12))),
inference(superposition,[],[f2466,f1054]) ).
fof(f10348,plain,
! [X0] : and(X0,not(not(b))) = and(not(not(b)),or(X0,not(a12))),
inference(superposition,[],[f445,f1054]) ).
fof(f10350,plain,
and(not(not(b)),a) = and(a,not(not(a12))),
inference(superposition,[],[f924,f1054]) ).
fof(f10352,plain,
! [X0] : or(a,not(X0)) = or(and(a,X0),or(not(a12),not(X0))),
inference(superposition,[],[f1103,f1054]) ).
fof(f10374,plain,
! [X0] : or(a,not(X0)) = or(not(X0),or(and(a,X0),not(a12))),
inference(forward_demodulation,[],[f10352,f3678]) ).
fof(f10376,plain,
and(a,a12) = and(not(not(b)),a),
inference(forward_demodulation,[],[f10350,f13]) ).
fof(f10378,plain,
! [X0] : and(X0,not(not(b))) = not(or(not(b),and(not(X0),a12))),
inference(forward_demodulation,[],[f10348,f5276]) ).
fof(f10385,plain,
! [X0] : and(or(X0,b),a) = or(and(a,b),and(X0,not(a12))),
inference(forward_demodulation,[],[f10338,f14]) ).
fof(f10392,plain,
! [X0] : or(a,not(X0)) = or(not(X0),or(not(a12),and(a,X0))),
inference(forward_demodulation,[],[f10374,f6570]) ).
fof(f10394,plain,
and(a,a12) = and(a,not(not(b))),
inference(forward_demodulation,[],[f10376,f14]) ).
fof(f10396,plain,
! [X0] : and(X0,not(not(b))) = and(b,not(and(not(X0),a12))),
inference(forward_demodulation,[],[f10378,f734]) ).
fof(f10399,plain,
! [X0] : and(or(X0,b),a) = or(sF0,and(X0,not(a12))),
inference(forward_demodulation,[],[f10385,f67]) ).
fof(f10402,plain,
! [X0] : or(a,not(X0)) = or(and(a,X0),not(and(a12,X0))),
inference(forward_demodulation,[],[f10392,f3840]) ).
fof(f10403,plain,
and(a,b) = and(a,a12),
inference(forward_demodulation,[],[f10394,f13]) ).
fof(f10404,plain,
! [X0] : and(X0,not(not(b))) = and(b,or(X0,not(a12))),
inference(forward_demodulation,[],[f10396,f892]) ).
fof(f10407,plain,
! [X0] : or(sF0,and(X0,not(a12))) = and(a,or(b,X0)),
inference(forward_demodulation,[],[f10399,f6154]) ).
fof(f10410,plain,
and(a,b) = and(a12,a),
inference(forward_demodulation,[],[f10403,f14]) ).
fof(f10411,plain,
! [X0] : and(X0,b) = and(b,or(X0,not(a12))),
inference(forward_demodulation,[],[f10404,f13]) ).
fof(f10414,plain,
sF0 = and(a12,a),
inference(forward_demodulation,[],[f10410,f67]) ).
fof(f10439,plain,
! [X0] : and(or(X0,a12),a) = or(sF0,and(X0,and(a,not(a12)))),
inference(superposition,[],[f2466,f10414]) ).
fof(f10447,plain,
! [X0] : or(sF0,and(X0,not(a12))) = and(or(X0,a12),a),
inference(forward_demodulation,[],[f10439,f4380]) ).
fof(f10458,plain,
! [X0] : or(sF0,and(X0,not(a12))) = and(a,or(a12,X0)),
inference(forward_demodulation,[],[f10447,f6154]) ).
fof(f10463,plain,
! [X0] : and(a,or(b,X0)) = and(a,or(a12,X0)),
inference(backward_demodulation,[],[f10407,f10458]) ).
fof(f10464,plain,
and(a12,b) = and(b,n1),
inference(superposition,[],[f10411,f22]) ).
fof(f10471,plain,
! [X0] : and(b,or(X0,not(a12))) = and(and(X0,not(not(a12))),b),
inference(superposition,[],[f10411,f47]) ).
fof(f10524,plain,
! [X0] : and(b,or(X0,not(a12))) = and(not(not(a12)),and(X0,b)),
inference(forward_demodulation,[],[f10471,f2351]) ).
fof(f10528,plain,
b = and(a12,b),
inference(forward_demodulation,[],[f10464,f3]) ).
fof(f10541,plain,
! [X0] : and(b,or(X0,not(a12))) = and(b,and(X0,not(not(a12)))),
inference(forward_demodulation,[],[f10524,f2945]) ).
fof(f10551,plain,
! [X0] : and(b,or(X0,not(a12))) = and(b,and(X0,a12)),
inference(forward_demodulation,[],[f10541,f13]) ).
fof(f10557,plain,
! [X0] : and(b,or(X0,not(a12))) = and(a12,and(X0,b)),
inference(forward_demodulation,[],[f10551,f2945]) ).
fof(f10561,plain,
! [X0] : and(X0,b) = and(a12,and(X0,b)),
inference(forward_demodulation,[],[f10557,f10411]) ).
fof(f11292,plain,
! [X2,X0,X1] : not(and(X2,or(X0,not(X1)))) = or(not(X2),and(not(X0),X1)),
inference(superposition,[],[f11,f735]) ).
fof(f11340,plain,
! [X0] : or(not(a12),and(a11,X0)) = not(and(a12,or(a,not(and(a11,X0))))),
inference(backward_demodulation,[],[f846,f11292]) ).
fof(f11859,plain,
! [X2,X0,X1] : and(X2,not(or(X0,X1))) = and(not(X1),and(X2,not(X0))),
inference(superposition,[],[f5444,f12]) ).
fof(f11864,plain,
! [X0] : and(X0,sF0) = and(b,and(X0,a)),
inference(superposition,[],[f5444,f67]) ).
fof(f12111,plain,
! [X0] : and(X0,sF0) = and(a,and(X0,b)),
inference(forward_demodulation,[],[f11864,f2945]) ).
fof(f12116,plain,
! [X2,X0,X1] : and(X0,not(or(X1,X2))) = not(or(X2,or(not(X0),X1))),
inference(backward_demodulation,[],[f7857,f11859]) ).
fof(f12485,plain,
! [X0] : or(X0,not(sF24)) = or(sF25,or(carryin,X0)),
inference(superposition,[],[f3756,f5308]) ).
fof(f12496,plain,
! [X0] : or(X0,not(sF24)) = or(carryin,or(X0,sF25)),
inference(forward_demodulation,[],[f12485,f3678]) ).
fof(f12524,plain,
and(carryin,sF21) = and(sF21,not(sF24)),
inference(superposition,[],[f8265,f5308]) ).
fof(f12574,plain,
sF31 = and(sF21,not(sF24)),
inference(forward_demodulation,[],[f12524,f3003]) ).
fof(f14394,plain,
! [X0] : and(n1,sF24) = and(or(X0,not(carryin)),sF24),
inference(superposition,[],[f7547,f3595]) ).
fof(f14457,plain,
! [X0] : and(n1,sF24) = and(sF24,or(not(carryin),X0)),
inference(forward_demodulation,[],[f14394,f6154]) ).
fof(f14481,plain,
! [X0] : sF24 = and(sF24,or(not(carryin),X0)),
inference(forward_demodulation,[],[f14457,f1596]) ).
fof(f15547,plain,
! [X2,X0,X1] : and(and(not(X0),X1),not(X2)) = not(or(or(not(X1),X0),X2)),
inference(superposition,[],[f12,f4707]) ).
fof(f15596,plain,
! [X2,X0,X1] : and(and(not(X0),X1),not(X2)) = not(or(X0,or(not(X1),X2))),
inference(forward_demodulation,[],[f15547,f3564]) ).
fof(f15631,plain,
! [X2,X0,X1] : and(and(not(X0),X1),not(X2)) = and(X1,not(or(X2,X0))),
inference(forward_demodulation,[],[f15596,f12116]) ).
fof(f15659,plain,
! [X2,X0,X1] : and(X1,not(or(X2,X0))) = and(X1,and(not(X0),not(X2))),
inference(forward_demodulation,[],[f15631,f2351]) ).
fof(f15668,plain,
! [X2,X0,X1] : and(X1,not(or(X0,X2))) = and(X1,not(or(X2,X0))),
inference(forward_demodulation,[],[f15659,f12]) ).
fof(f15712,plain,
! [X2,X0,X1] : and(X2,not(or(not(X1),not(X0)))) = and(X2,not(not(and(X0,X1)))),
inference(superposition,[],[f15668,f11]) ).
fof(f15802,plain,
! [X2,X0,X1] : and(not(not(or(X2,X1))),X0) = and(X0,not(and(X0,not(or(X1,X2))))),
inference(superposition,[],[f924,f15668]) ).
fof(f15860,plain,
! [X2,X0,X1] : and(not(not(or(X1,X2))),X0) = and(not(not(or(X2,X1))),X0),
inference(forward_demodulation,[],[f15802,f924]) ).
fof(f15904,plain,
! [X2,X0,X1] : and(X2,and(X0,X1)) = and(X2,not(or(not(X1),not(X0)))),
inference(forward_demodulation,[],[f15712,f13]) ).
fof(f15926,plain,
! [X2,X0,X1] : and(or(X2,X1),X0) = and(not(not(or(X1,X2))),X0),
inference(forward_demodulation,[],[f15860,f13]) ).
fof(f15945,plain,
! [X2,X0,X1] : and(X2,and(X0,X1)) = and(X2,and(X1,not(not(X0)))),
inference(forward_demodulation,[],[f15904,f734]) ).
fof(f15955,plain,
! [X2,X0,X1] : and(or(X1,X2),X0) = and(or(X2,X1),X0),
inference(forward_demodulation,[],[f15926,f13]) ).
fof(f15967,plain,
! [X2,X0,X1] : and(X2,and(X0,X1)) = and(X2,and(X1,X0)),
inference(forward_demodulation,[],[f15945,f13]) ).
fof(f16160,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(and(X2,X1),X0),
inference(superposition,[],[f14,f15967]) ).
fof(f16205,plain,
! [X2,X0,X1] : or(X0,not(and(X2,X1))) = not(and(not(X0),and(X1,X2))),
inference(superposition,[],[f892,f15967]) ).
fof(f16223,plain,
! [X2,X0,X1] : or(X0,not(and(X1,X2))) = or(X0,not(and(X2,X1))),
inference(forward_demodulation,[],[f16205,f892]) ).
fof(f16729,plain,
! [X2,X0,X1] : not(and(and(X0,X1),not(X2))) = or(X2,not(and(X1,X0))),
inference(superposition,[],[f892,f16160]) ).
fof(f16834,plain,
! [X2,X0,X1] : or(not(and(X0,X1)),X2) = or(X2,not(and(X1,X0))),
inference(forward_demodulation,[],[f16729,f896]) ).
fof(f17497,plain,
! [X2,X3,X0,X1] : and(X3,and(or(X0,X1),X2)) = and(X3,and(X2,or(X1,X0))),
inference(superposition,[],[f15967,f15955]) ).
fof(f17508,plain,
! [X2,X3,X0,X1] : and(or(X0,X1),and(X2,X3)) = and(X2,and(X3,or(X1,X0))),
inference(superposition,[],[f5444,f15955]) ).
fof(f18190,plain,
! [X2,X0,X1] : and(X0,or(not(X1),X2)) = and(or(not(X1),X2),and(n1,X0)),
inference(superposition,[],[f9208,f747]) ).
fof(f18233,plain,
! [X2,X0,X1] : and(X0,or(not(X1),X2)) = and(n1,and(X0,or(X2,not(X1)))),
inference(forward_demodulation,[],[f18190,f17508]) ).
fof(f18281,plain,
! [X2,X0,X1] : and(X0,or(not(X1),X2)) = and(X0,or(X2,not(X1))),
inference(forward_demodulation,[],[f18233,f1596]) ).
fof(f19749,plain,
n1 = or(a14,not(sF8)),
inference(superposition,[],[f230,f4329]) ).
fof(f19878,plain,
n1 = or(a14,a15),
inference(forward_demodulation,[],[f19749,f147]) ).
fof(f20095,plain,
! [X0] : or(X0,n1) = or(a15,or(a14,X0)),
inference(superposition,[],[f3756,f19878]) ).
fof(f20109,plain,
! [X0] : or(X0,n1) = or(a14,or(X0,a15)),
inference(forward_demodulation,[],[f20095,f3678]) ).
fof(f20120,plain,
! [X0] : n1 = or(a14,or(X0,a15)),
inference(forward_demodulation,[],[f20109,f6]) ).
fof(f20704,plain,
! [X0] : not(and(X0,a11)) = or(not(X0),sF0),
inference(superposition,[],[f896,f143]) ).
fof(f22140,plain,
a12 = or(a12,b),
inference(superposition,[],[f1442,f10528]) ).
fof(f23020,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(X0,or(X2,X1)),
inference(superposition,[],[f14,f6154]) ).
fof(f23061,plain,
! [X2,X3,X0,X1] : and(X3,and(X0,or(X2,X1))) = and(X3,and(X0,or(X1,X2))),
inference(superposition,[],[f15967,f6154]) ).
fof(f23510,plain,
! [X2,X0,X1] : and(X2,not(and(X0,X1))) = and(X2,or(not(X1),not(X0))),
inference(superposition,[],[f23020,f11]) ).
fof(f23796,plain,
! [X2,X0,X1] : and(X2,not(and(X1,X0))) = and(X2,not(and(X0,X1))),
inference(forward_demodulation,[],[f23510,f11]) ).
fof(f24053,plain,
! [X2,X0,X1] : or(X0,not(not(and(X2,X1)))) = not(and(not(X0),not(and(X1,X2)))),
inference(superposition,[],[f892,f23796]) ).
fof(f24072,plain,
! [X2,X0,X1] : or(X0,not(not(and(X2,X1)))) = or(X0,not(not(and(X1,X2)))),
inference(forward_demodulation,[],[f24053,f892]) ).
fof(f24199,plain,
! [X2,X0,X1] : or(X0,and(X1,X2)) = or(X0,not(not(and(X2,X1)))),
inference(forward_demodulation,[],[f24072,f13]) ).
fof(f24259,plain,
! [X2,X0,X1] : or(X0,and(X1,X2)) = or(X0,and(X2,X1)),
inference(forward_demodulation,[],[f24199,f13]) ).
fof(f24470,plain,
! [X2,X0,X1] : or(X0,and(X1,X2)) = or(and(X2,X1),X0),
inference(superposition,[],[f15,f24259]) ).
fof(f27064,plain,
! [X2,X0,X1] : and(and(or(X2,X0),X1),not(X0)) = and(and(or(X2,X0),X1),not(and(X0,X1))),
inference(superposition,[],[f4526,f8561]) ).
fof(f27126,plain,
and(b,not(a)) = and(b,not(sF0)),
inference(superposition,[],[f4526,f67]) ).
fof(f27132,plain,
and(a15,not(a11)) = and(a15,not(not(c1))),
inference(superposition,[],[f4526,f1273]) ).
fof(f27134,plain,
and(carryin,not(a14)) = and(carryin,not(sF8)),
inference(superposition,[],[f4526,f87]) ).
fof(f27228,plain,
! [X0,X1] : not(and(not(X0),not(X1))) = or(X0,not(not(and(X1,not(X0))))),
inference(superposition,[],[f892,f4526]) ).
fof(f27247,plain,
! [X0,X1] : or(X0,and(X1,not(X0))) = not(and(not(X0),not(X1))),
inference(forward_demodulation,[],[f27228,f13]) ).
fof(f27308,plain,
and(carryin,a15) = and(carryin,not(a14)),
inference(forward_demodulation,[],[f27134,f147]) ).
fof(f27310,plain,
and(a15,c1) = and(a15,not(a11)),
inference(forward_demodulation,[],[f27132,f13]) ).
fof(f27316,plain,
and(b,not(a)) = and(b,a11),
inference(forward_demodulation,[],[f27126,f143]) ).
fof(f27374,plain,
! [X2,X0,X1] : and(and(or(X2,X0),X1),not(X0)) = and(X1,and(or(X2,X0),not(and(X0,X1)))),
inference(forward_demodulation,[],[f27064,f2351]) ).
fof(f27397,plain,
! [X0,X1] : or(X0,and(X1,not(X0))) = or(X0,not(not(X1))),
inference(forward_demodulation,[],[f27247,f892]) ).
fof(f27445,plain,
and(carryin,a15) = and(carryin,sF6),
inference(forward_demodulation,[],[f27308,f730]) ).
fof(f27447,plain,
and(a15,c1) = and(a15,sF0),
inference(forward_demodulation,[],[f27310,f727]) ).
fof(f27452,plain,
and(a11,b) = and(b,not(a)),
inference(forward_demodulation,[],[f27316,f14]) ).
fof(f27509,plain,
! [X2,X0,X1] : and(X1,and(or(X2,X0),not(and(X0,X1)))) = and(X1,and(or(X2,X0),not(X0))),
inference(forward_demodulation,[],[f27374,f2351]) ).
fof(f27526,plain,
! [X0,X1] : or(X0,X1) = or(X0,and(X1,not(X0))),
inference(forward_demodulation,[],[f27397,f13]) ).
fof(f27557,plain,
and(a15,carryin) = and(carryin,sF6),
inference(forward_demodulation,[],[f27445,f14]) ).
fof(f27559,plain,
and(c1,a15) = and(a15,sF0),
inference(forward_demodulation,[],[f27447,f14]) ).
fof(f27562,plain,
and(a11,b) = sF21,
inference(forward_demodulation,[],[f27452,f153]) ).
fof(f27608,plain,
! [X2,X0,X1] : and(X1,and(not(X0),or(X0,X2))) = and(X1,and(or(X2,X0),not(and(X0,X1)))),
inference(forward_demodulation,[],[f27509,f17497]) ).
fof(f27639,plain,
not(a17) = and(carryin,sF6),
inference(forward_demodulation,[],[f27557,f753]) ).
fof(f27643,plain,
sF21 = not(a13),
inference(forward_demodulation,[],[f27562,f802]) ).
fof(f27681,plain,
! [X2,X0,X1] : and(X1,and(X2,not(X0))) = and(X1,and(or(X2,X0),not(and(X0,X1)))),
inference(forward_demodulation,[],[f27608,f441]) ).
fof(f27701,plain,
sF22 = or(not(a12),not(a13)),
inference(backward_demodulation,[],[f1055,f27643]) ).
fof(f27773,plain,
! [X0] : and(X0,not(not(a13))) = and(not(not(a13)),or(X0,sF31)),
inference(backward_demodulation,[],[f6846,f27643]) ).
fof(f27800,plain,
sF25 = and(a12,not(not(a13))),
inference(backward_demodulation,[],[f7912,f27643]) ).
fof(f27885,plain,
sF31 = and(not(a13),not(sF24)),
inference(backward_demodulation,[],[f12574,f27643]) ).
fof(f28023,plain,
! [X2,X0,X1] : and(X2,and(X0,not(X1))) = and(X2,and(X0,not(and(X1,X2)))),
inference(backward_demodulation,[],[f3274,f27681]) ).
fof(f28073,plain,
sF31 = not(or(a13,sF24)),
inference(forward_demodulation,[],[f27885,f12]) ).
fof(f28101,plain,
and(a12,a13) = sF25,
inference(forward_demodulation,[],[f27800,f13]) ).
fof(f28111,plain,
! [X0] : and(X0,a13) = and(a13,or(X0,sF31)),
inference(forward_demodulation,[],[f27773,f13]) ).
fof(f28150,plain,
not(and(a12,a13)) = sF22,
inference(forward_demodulation,[],[f27701,f11]) ).
fof(f28217,plain,
sF6 = sF25,
inference(forward_demodulation,[],[f28101,f82]) ).
fof(f28244,plain,
not(sF6) = sF22,
inference(forward_demodulation,[],[f28150,f82]) ).
fof(f28285,plain,
sF26 = and(carryin,sF6),
inference(backward_demodulation,[],[f128,f28217]) ).
fof(f28324,plain,
not(sF24) = or(carryin,sF6),
inference(backward_demodulation,[],[f5308,f28217]) ).
fof(f28370,plain,
! [X0] : or(X0,not(sF24)) = or(carryin,or(X0,sF6)),
inference(backward_demodulation,[],[f12496,f28217]) ).
fof(f28521,plain,
a14 = sF22,
inference(forward_demodulation,[],[f28244,f146]) ).
fof(f28615,plain,
sF26 = not(a17),
inference(forward_demodulation,[],[f28285,f27639]) ).
fof(f28630,plain,
! [X0] : and(sF24,X0) = and(a14,and(not(carryin),X0)),
inference(backward_demodulation,[],[f2931,f28521]) ).
fof(f28811,plain,
sF27 = or(sF24,not(a17)),
inference(backward_demodulation,[],[f130,f28615]) ).
fof(f29120,plain,
sF27 = or(not(a17),sF24),
inference(forward_demodulation,[],[f28811,f15]) ).
fof(f30248,plain,
! [X0,X1] : or(not(X0),X1) = or(not(X0),and(X1,X0)),
inference(superposition,[],[f27526,f13]) ).
fof(f30286,plain,
! [X0,X1] : or(X0,X1) = or(X0,and(not(X0),X1)),
inference(superposition,[],[f24259,f27526]) ).
fof(f30494,plain,
! [X2,X0,X1] : or(not(and(X0,X1)),X2) = or(not(and(X0,X1)),and(X0,and(X1,X2))),
inference(superposition,[],[f30248,f5444]) ).
fof(f30583,plain,
! [X0,X1] : or(not(X0),X1) = or(not(X0),and(X0,X1)),
inference(superposition,[],[f24259,f30248]) ).
fof(f31342,plain,
and(sF29,a13) = and(a13,sF32),
inference(superposition,[],[f28111,f140]) ).
fof(f31427,plain,
and(a13,sF32) = and(a13,sF29),
inference(forward_demodulation,[],[f31342,f14]) ).
fof(f33340,plain,
! [X0,X1] : or(X0,not(X1)) = or(X0,not(or(X0,X1))),
inference(superposition,[],[f30286,f12]) ).
fof(f34516,plain,
! [X0] : and(a14,not(carryin)) = and(sF24,or(not(carryin),X0)),
inference(superposition,[],[f28630,f2110]) ).
fof(f34661,plain,
sF24 = and(a14,not(carryin)),
inference(forward_demodulation,[],[f34516,f14481]) ).
fof(f34851,plain,
sF24 = not(a16),
inference(forward_demodulation,[],[f34661,f984]) ).
fof(f35040,plain,
sF31 = not(or(a13,not(a16))),
inference(backward_demodulation,[],[f28073,f34851]) ).
fof(f35043,plain,
not(not(a16)) = or(carryin,sF6),
inference(backward_demodulation,[],[f28324,f34851]) ).
fof(f35056,plain,
! [X0] : or(carryin,or(X0,sF6)) = or(X0,not(not(a16))),
inference(backward_demodulation,[],[f28370,f34851]) ).
fof(f35096,plain,
sF27 = or(not(a17),not(a16)),
inference(backward_demodulation,[],[f29120,f34851]) ).
fof(f35341,plain,
sF27 = not(and(a17,a16)),
inference(forward_demodulation,[],[f35096,f11]) ).
fof(f35360,plain,
! [X0] : or(X0,a16) = or(carryin,or(X0,sF6)),
inference(forward_demodulation,[],[f35056,f13]) ).
fof(f35364,plain,
a16 = or(carryin,sF6),
inference(forward_demodulation,[],[f35043,f13]) ).
fof(f35366,plain,
sF31 = and(not(a13),a16),
inference(forward_demodulation,[],[f35040,f735]) ).
fof(f35489,plain,
not(and(a16,a17)) = sF27,
inference(forward_demodulation,[],[f35341,f5882]) ).
fof(f35504,plain,
sF31 = and(a16,not(a13)),
inference(forward_demodulation,[],[f35366,f14]) ).
fof(f35560,plain,
sF27 = not(not(s1)),
inference(forward_demodulation,[],[f35489,f726]) ).
fof(f35571,plain,
sF32 = or(sF29,and(a16,not(a13))),
inference(backward_demodulation,[],[f140,f35504]) ).
fof(f35987,plain,
s1 = sF27,
inference(forward_demodulation,[],[f35560,f13]) ).
fof(f36254,plain,
~ circuit(s1,sF32),
inference(backward_demodulation,[],[f141,f35987]) ).
fof(f40122,plain,
not(a13) = and(a12,not(a13)),
inference(superposition,[],[f10561,f802]) ).
fof(f40241,plain,
not(a13) = and(a12,a14),
inference(backward_demodulation,[],[f976,f40122]) ).
fof(f41336,plain,
and(sF29,b) = and(sF29,sF0),
inference(superposition,[],[f2180,f12111]) ).
fof(f41438,plain,
and(sF29,b) = and(sF0,sF29),
inference(forward_demodulation,[],[f41336,f14]) ).
fof(f41493,plain,
and(sF0,sF29) = and(b,sF29),
inference(forward_demodulation,[],[f41438,f14]) ).
fof(f43886,plain,
! [X2,X0,X1] : and(X1,and(X2,not(and(not(X0),X1)))) = and(X1,and(X2,not(not(and(X1,X0))))),
inference(superposition,[],[f9804,f924]) ).
fof(f44169,plain,
! [X2,X0,X1] : and(X1,and(X2,and(X1,X0))) = and(X1,and(X2,not(and(not(X0),X1)))),
inference(forward_demodulation,[],[f43886,f13]) ).
fof(f44311,plain,
! [X2,X0,X1] : and(X1,and(X2,and(X1,X0))) = and(X1,and(X2,not(not(X0)))),
inference(forward_demodulation,[],[f44169,f28023]) ).
fof(f44405,plain,
! [X2,X0,X1] : and(X1,and(X2,X0)) = and(X1,and(X2,and(X1,X0))),
inference(forward_demodulation,[],[f44311,f13]) ).
fof(f55116,plain,
and(a,sF28) = and(a,or(a12,carryin)),
inference(superposition,[],[f10463,f132]) ).
fof(f55291,plain,
sF29 = and(a,or(a12,carryin)),
inference(forward_demodulation,[],[f55116,f134]) ).
fof(f55365,plain,
and(a,a12) = and(a12,sF29),
inference(superposition,[],[f5877,f55291]) ).
fof(f55448,plain,
and(a12,a) = and(a12,sF29),
inference(forward_demodulation,[],[f55365,f14]) ).
fof(f55473,plain,
sF0 = and(a12,sF29),
inference(forward_demodulation,[],[f55448,f10414]) ).
fof(f63347,plain,
! [X0] : or(not(a12),and(not(a),and(a11,X0))) = and(or(X0,a),a11),
inference(superposition,[],[f5132,f825]) ).
fof(f63857,plain,
! [X0] : or(not(a12),and(not(a),and(a11,X0))) = and(a11,or(a,X0)),
inference(forward_demodulation,[],[f63347,f6154]) ).
fof(f64154,plain,
! [X0] : not(and(a12,or(a,not(and(a11,X0))))) = and(a11,or(a,X0)),
inference(forward_demodulation,[],[f63857,f11292]) ).
fof(f64369,plain,
! [X0] : or(not(a12),and(a11,X0)) = and(a11,or(a,X0)),
inference(backward_demodulation,[],[f11340,f64154]) ).
fof(f64549,plain,
! [X0] : or(and(a11,X0),not(or(a12,X0))) = and(a11,or(a,X0)),
inference(backward_demodulation,[],[f880,f64369]) ).
fof(f67558,plain,
and(a11,or(a,b)) = or(not(a13),not(or(a12,b))),
inference(superposition,[],[f64549,f802]) ).
fof(f67717,plain,
and(a11,or(a,b)) = not(and(a13,or(a12,b))),
inference(forward_demodulation,[],[f67558,f11]) ).
fof(f67830,plain,
not(and(a13,a12)) = and(a11,or(a,b)),
inference(forward_demodulation,[],[f67717,f22140]) ).
fof(f67921,plain,
not(and(a12,a13)) = and(a11,or(a,b)),
inference(forward_demodulation,[],[f67830,f5882]) ).
fof(f67993,plain,
not(sF6) = and(a11,or(a,b)),
inference(forward_demodulation,[],[f67921,f82]) ).
fof(f68053,plain,
a14 = and(a11,or(a,b)),
inference(forward_demodulation,[],[f67993,f146]) ).
fof(f68150,plain,
and(a11,a) = and(a,a14),
inference(superposition,[],[f5877,f68053]) ).
fof(f68156,plain,
n1 = or(a11,not(a14)),
inference(superposition,[],[f231,f68053]) ).
fof(f68175,plain,
n0 = and(not(a11),a14),
inference(superposition,[],[f2037,f68053]) ).
fof(f68176,plain,
! [X0] : and(a14,X0) = and(or(a,b),and(a11,X0)),
inference(superposition,[],[f2351,f68053]) ).
fof(f68207,plain,
! [X0] : and(a11,and(X0,or(a,b))) = and(a11,and(X0,a14)),
inference(superposition,[],[f44405,f68053]) ).
fof(f68210,plain,
! [X0] : and(a11,and(X0,or(a,b))) = and(a14,and(X0,a11)),
inference(forward_demodulation,[],[f68207,f2945]) ).
fof(f68236,plain,
! [X0] : and(a14,X0) = and(a11,and(X0,or(b,a))),
inference(forward_demodulation,[],[f68176,f17508]) ).
fof(f68237,plain,
n0 = and(a14,not(a11)),
inference(forward_demodulation,[],[f68175,f14]) ).
fof(f68255,plain,
n1 = or(a11,sF6),
inference(forward_demodulation,[],[f68156,f730]) ).
fof(f68261,plain,
and(a11,a) = and(a14,a),
inference(forward_demodulation,[],[f68150,f14]) ).
fof(f68282,plain,
! [X0] : and(a14,X0) = and(a11,and(X0,or(a,b))),
inference(forward_demodulation,[],[f68236,f23061]) ).
fof(f68283,plain,
n0 = and(a14,sF0),
inference(forward_demodulation,[],[f68237,f727]) ).
fof(f68300,plain,
not(a12) = and(a14,a),
inference(forward_demodulation,[],[f68261,f825]) ).
fof(f68318,plain,
! [X0] : and(a14,X0) = and(a14,and(X0,a11)),
inference(backward_demodulation,[],[f68210,f68282]) ).
fof(f68600,plain,
! [X0] : and(or(X0,sF0),a14) = or(n0,and(not(sF0),and(a14,X0))),
inference(superposition,[],[f5132,f68283]) ).
fof(f68634,plain,
! [X0] : and(or(X0,sF0),a14) = and(not(sF0),and(a14,X0)),
inference(forward_demodulation,[],[f68600,f246]) ).
fof(f68677,plain,
! [X0] : and(or(X0,sF0),a14) = and(a14,and(X0,not(sF0))),
inference(forward_demodulation,[],[f68634,f5444]) ).
fof(f68701,plain,
! [X0] : and(a14,and(X0,a11)) = and(or(X0,sF0),a14),
inference(forward_demodulation,[],[f68677,f143]) ).
fof(f68716,plain,
! [X0] : and(a14,and(X0,a11)) = and(a14,or(sF0,X0)),
inference(forward_demodulation,[],[f68701,f6154]) ).
fof(f68725,plain,
! [X0] : and(a14,X0) = and(a14,or(sF0,X0)),
inference(forward_demodulation,[],[f68716,f68318]) ).
fof(f71899,plain,
or(a12,a16) = or(carryin,a12),
inference(superposition,[],[f6502,f35364]) ).
fof(f71989,plain,
or(a12,a16) = or(a12,carryin),
inference(forward_demodulation,[],[f71899,f15]) ).
fof(f72023,plain,
sF29 = and(a,or(a12,a16)),
inference(backward_demodulation,[],[f55291,f71989]) ).
fof(f72698,plain,
sF0 = and(sF29,sF0),
inference(superposition,[],[f999,f55473]) ).
fof(f72771,plain,
sF0 = and(sF0,sF29),
inference(forward_demodulation,[],[f72698,f14]) ).
fof(f72799,plain,
sF0 = and(b,sF29),
inference(backward_demodulation,[],[f41493,f72771]) ).
fof(f74125,plain,
and(a14,or(sF0,a16)) = or(n0,not(or(a15,sF0))),
inference(superposition,[],[f7916,f68283]) ).
fof(f74296,plain,
and(a14,or(sF0,a16)) = not(or(a15,sF0)),
inference(forward_demodulation,[],[f74125,f246]) ).
fof(f74423,plain,
and(a11,not(a15)) = and(a14,or(sF0,a16)),
inference(forward_demodulation,[],[f74296,f376]) ).
fof(f74533,plain,
and(a11,not(a15)) = and(a14,a16),
inference(forward_demodulation,[],[f74423,f68725]) ).
fof(f74618,plain,
and(a11,not(a15)) = and(a16,a14),
inference(forward_demodulation,[],[f74533,f14]) ).
fof(f74685,plain,
sF8 = and(a11,not(a15)),
inference(forward_demodulation,[],[f74618,f4329]) ).
fof(f74743,plain,
sF8 = and(a11,sF8),
inference(forward_demodulation,[],[f74685,f731]) ).
fof(f74839,plain,
n1 = or(a11,not(sF8)),
inference(superposition,[],[f231,f74743]) ).
fof(f74922,plain,
n1 = or(a11,a15),
inference(forward_demodulation,[],[f74839,f147]) ).
fof(f74977,plain,
and(a15,not(a11)) = and(not(a11),n1),
inference(superposition,[],[f441,f74922]) ).
fof(f75036,plain,
and(a15,not(a11)) = and(n1,not(a11)),
inference(forward_demodulation,[],[f74977,f14]) ).
fof(f75055,plain,
not(a11) = and(a15,not(a11)),
inference(forward_demodulation,[],[f75036,f1596]) ).
fof(f75063,plain,
sF0 = and(a15,sF0),
inference(forward_demodulation,[],[f75055,f727]) ).
fof(f75068,plain,
sF0 = and(c1,a15),
inference(backward_demodulation,[],[f27559,f75063]) ).
fof(f75599,plain,
or(c1,not(a15)) = or(not(a15),sF0),
inference(superposition,[],[f746,f75068]) ).
fof(f75679,plain,
not(and(a15,a11)) = or(c1,not(a15)),
inference(forward_demodulation,[],[f75599,f20704]) ).
fof(f75714,plain,
not(and(a15,a11)) = or(c1,sF8),
inference(forward_demodulation,[],[f75679,f731]) ).
fof(f75727,plain,
not(and(a11,a15)) = or(c1,sF8),
inference(forward_demodulation,[],[f75714,f5882]) ).
fof(f75732,plain,
not(not(c1)) = or(c1,sF8),
inference(forward_demodulation,[],[f75727,f1273]) ).
fof(f75734,plain,
c1 = or(c1,sF8),
inference(forward_demodulation,[],[f75732,f13]) ).
fof(f81776,plain,
or(not(a14),a) = or(not(a14),not(a12)),
inference(superposition,[],[f30583,f68300]) ).
fof(f81798,plain,
or(not(b),sF0) = or(not(b),sF29),
inference(superposition,[],[f30583,f72799]) ).
fof(f81811,plain,
! [X2,X0,X1] : or(and(X0,X1),not(and(X0,X2))) = or(not(X2),or(not(X0),X1)),
inference(superposition,[],[f3840,f30583]) ).
fof(f81902,plain,
! [X2,X0,X1] : or(X1,not(and(X0,X2))) = or(and(X0,X1),not(and(X0,X2))),
inference(forward_demodulation,[],[f81811,f3840]) ).
fof(f81908,plain,
not(and(b,a11)) = or(not(b),sF29),
inference(forward_demodulation,[],[f81798,f20704]) ).
fof(f81929,plain,
not(and(a14,a12)) = or(not(a14),a),
inference(forward_demodulation,[],[f81776,f11]) ).
fof(f82078,plain,
not(and(a11,b)) = or(not(b),sF29),
inference(forward_demodulation,[],[f81908,f5882]) ).
fof(f82099,plain,
not(and(a14,a12)) = or(a,not(a14)),
inference(forward_demodulation,[],[f81929,f15]) ).
fof(f82201,plain,
not(not(a13)) = or(not(b),sF29),
inference(forward_demodulation,[],[f82078,f802]) ).
fof(f82221,plain,
or(a,sF6) = not(and(a14,a12)),
inference(forward_demodulation,[],[f82099,f730]) ).
fof(f82292,plain,
a13 = or(not(b),sF29),
inference(forward_demodulation,[],[f82201,f13]) ).
fof(f82311,plain,
or(a,sF6) = not(and(a12,a14)),
inference(forward_demodulation,[],[f82221,f5882]) ).
fof(f82358,plain,
not(not(a13)) = or(a,sF6),
inference(forward_demodulation,[],[f82311,f40241]) ).
fof(f82382,plain,
a13 = or(a,sF6),
inference(forward_demodulation,[],[f82358,f13]) ).
fof(f82414,plain,
a = and(a,a13),
inference(superposition,[],[f2110,f82382]) ).
fof(f82463,plain,
a = and(a13,a),
inference(forward_demodulation,[],[f82414,f14]) ).
fof(f83247,plain,
or(carryin,n1) = or(a11,a16),
inference(superposition,[],[f35360,f68255]) ).
fof(f83349,plain,
or(carryin,n1) = or(a16,a11),
inference(forward_demodulation,[],[f83247,f15]) ).
fof(f83393,plain,
n1 = or(a16,a11),
inference(forward_demodulation,[],[f83349,f6]) ).
fof(f87989,plain,
or(a,not(a13)) = or(and(a,a13),not(sF6)),
inference(superposition,[],[f10402,f82]) ).
fof(f88116,plain,
or(a,not(a13)) = or(and(a13,a),not(sF6)),
inference(forward_demodulation,[],[f87989,f6422]) ).
fof(f88282,plain,
or(a,not(a13)) = or(and(a13,a),a14),
inference(forward_demodulation,[],[f88116,f146]) ).
fof(f88418,plain,
or(a,not(a13)) = or(a14,and(a,a13)),
inference(forward_demodulation,[],[f88282,f24470]) ).
fof(f88517,plain,
or(a,not(a13)) = or(a14,and(a13,a)),
inference(forward_demodulation,[],[f88418,f24259]) ).
fof(f88596,plain,
or(a14,a) = or(a,not(a13)),
inference(forward_demodulation,[],[f88517,f82463]) ).
fof(f102691,plain,
! [X0] : not(and(X0,sF8)) = or(a15,and(a16,not(X0))),
inference(superposition,[],[f13,f6987]) ).
fof(f102789,plain,
! [X0] : or(a15,not(X0)) = or(a15,and(a16,not(X0))),
inference(forward_demodulation,[],[f102691,f910]) ).
fof(f111846,plain,
! [X2,X0,X1] : or(and(X2,X0),not(and(X2,X1))) = or(and(X2,X0),not(and(or(X0,X1),X2))),
inference(superposition,[],[f33340,f5081]) ).
fof(f111849,plain,
! [X2,X0,X1] : or(X0,not(and(X2,X1))) = or(and(X2,X0),not(and(or(X0,X1),X2))),
inference(forward_demodulation,[],[f111846,f81902]) ).
fof(f119168,plain,
! [X2,X0,X1] : or(and(X2,X0),not(and(or(X0,X1),X2))) = or(not(and(X2,X1)),and(X2,X0)),
inference(superposition,[],[f5317,f5081]) ).
fof(f119580,plain,
! [X2,X0,X1] : or(X0,not(and(X2,X1))) = or(not(and(X2,X1)),and(X2,X0)),
inference(forward_demodulation,[],[f119168,f111849]) ).
fof(f119777,plain,
! [X2,X0,X1] : or(not(and(X0,X1)),X2) = or(and(X1,X2),not(and(X0,X1))),
inference(backward_demodulation,[],[f30494,f119580]) ).
fof(f127732,plain,
sF29 = and(sF29,a13),
inference(superposition,[],[f2109,f82292]) ).
fof(f127807,plain,
sF29 = and(a13,sF29),
inference(forward_demodulation,[],[f127732,f14]) ).
fof(f127846,plain,
sF29 = and(a13,sF32),
inference(backward_demodulation,[],[f31427,f127807]) ).
fof(f127892,plain,
and(a12,sF29) = and(sF6,sF32),
inference(superposition,[],[f5418,f127846]) ).
fof(f127997,plain,
sF0 = and(sF6,sF32),
inference(forward_demodulation,[],[f127892,f55473]) ).
fof(f144684,plain,
! [X0] : or(a15,X0) = or(a15,and(a16,X0)),
inference(superposition,[],[f102789,f13]) ).
fof(f145716,plain,
! [X2,X0,X1] : or(and(X2,X1),not(and(or(X0,X1),X2))) = or(not(and(X2,X0)),and(X2,X1)),
inference(superposition,[],[f673,f5081]) ).
fof(f146196,plain,
! [X2,X0,X1] : or(X1,not(and(X2,X0))) = or(and(X2,X1),not(and(or(X0,X1),X2))),
inference(forward_demodulation,[],[f145716,f119580]) ).
fof(f146420,plain,
! [X2,X0,X1] : or(X1,not(and(X2,X0))) = or(not(and(or(X0,X1),X2)),X1),
inference(forward_demodulation,[],[f146196,f119777]) ).
fof(f146594,plain,
! [X2,X0,X1] : or(X1,not(and(X2,X0))) = or(X1,not(and(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f146420,f16834]) ).
fof(f147139,plain,
or(a16,not(sF29)) = or(a16,not(and(a,a12))),
inference(superposition,[],[f146594,f72023]) ).
fof(f147413,plain,
or(a16,not(sF29)) = or(a16,not(and(a12,a))),
inference(forward_demodulation,[],[f147139,f16223]) ).
fof(f147680,plain,
or(a16,not(sF29)) = or(a16,not(sF0)),
inference(forward_demodulation,[],[f147413,f10414]) ).
fof(f147887,plain,
or(a16,not(sF29)) = or(a16,a11),
inference(forward_demodulation,[],[f147680,f143]) ).
fof(f148042,plain,
n1 = or(a16,not(sF29)),
inference(forward_demodulation,[],[f147887,f83393]) ).
fof(f152123,plain,
or(c1,sF8) = or(sF8,sF0),
inference(superposition,[],[f677,f75068]) ).
fof(f152277,plain,
or(c1,sF8) = or(sF0,sF8),
inference(forward_demodulation,[],[f152123,f15]) ).
fof(f152330,plain,
c1 = or(sF0,sF8),
inference(forward_demodulation,[],[f152277,f75734]) ).
fof(f186615,plain,
and(a16,sF29) = and(a,a16),
inference(superposition,[],[f6013,f72023]) ).
fof(f187155,plain,
and(a16,sF29) = and(a16,a),
inference(forward_demodulation,[],[f186615,f14]) ).
fof(f187827,plain,
and(sF29,n1) = and(a16,sF29),
inference(superposition,[],[f3205,f148042]) ).
fof(f187941,plain,
and(sF29,n1) = and(a16,a),
inference(forward_demodulation,[],[f187827,f187155]) ).
fof(f187989,plain,
and(n1,sF29) = and(a16,a),
inference(forward_demodulation,[],[f187941,f14]) ).
fof(f188026,plain,
sF29 = and(a16,a),
inference(forward_demodulation,[],[f187989,f1596]) ).
fof(f188348,plain,
sF32 = or(and(a16,a),and(a16,not(a13))),
inference(backward_demodulation,[],[f35571,f188026]) ).
fof(f189219,plain,
sF32 = and(or(a,not(a13)),a16),
inference(forward_demodulation,[],[f188348,f5081]) ).
fof(f189626,plain,
sF32 = and(a16,or(not(a13),a)),
inference(forward_demodulation,[],[f189219,f6154]) ).
fof(f189895,plain,
sF32 = and(a16,or(a,not(a13))),
inference(forward_demodulation,[],[f189626,f18281]) ).
fof(f190073,plain,
sF32 = and(a16,or(a14,a)),
inference(forward_demodulation,[],[f189895,f88596]) ).
fof(f190250,plain,
or(a15,or(a14,a)) = or(a15,sF32),
inference(superposition,[],[f144684,f190073]) ).
fof(f190252,plain,
and(a16,a14) = and(a14,sF32),
inference(superposition,[],[f5877,f190073]) ).
fof(f190381,plain,
sF8 = and(a14,sF32),
inference(forward_demodulation,[],[f190252,f4329]) ).
fof(f190383,plain,
or(a14,or(a,a15)) = or(a15,sF32),
inference(forward_demodulation,[],[f190250,f3678]) ).
fof(f190431,plain,
n1 = or(a15,sF32),
inference(forward_demodulation,[],[f190383,f20120]) ).
fof(f190622,plain,
or(not(a15),sF32) = or(sF32,not(n1)),
inference(superposition,[],[f673,f190431]) ).
fof(f190726,plain,
or(not(a15),sF32) = or(not(n1),sF32),
inference(forward_demodulation,[],[f190622,f15]) ).
fof(f190760,plain,
or(not(a15),sF32) = or(n0,sF32),
inference(forward_demodulation,[],[f190726,f10]) ).
fof(f190777,plain,
sF32 = or(not(a15),sF32),
inference(forward_demodulation,[],[f190760,f246]) ).
fof(f190783,plain,
sF32 = or(sF8,sF32),
inference(forward_demodulation,[],[f190777,f731]) ).
fof(f191612,plain,
and(sF32,not(sF8)) = and(not(a14),sF32),
inference(superposition,[],[f2030,f190381]) ).
fof(f191697,plain,
and(sF6,sF32) = and(sF32,not(sF8)),
inference(forward_demodulation,[],[f191612,f730]) ).
fof(f191746,plain,
and(sF6,sF32) = and(not(sF8),sF32),
inference(forward_demodulation,[],[f191697,f14]) ).
fof(f191765,plain,
and(sF6,sF32) = and(a15,sF32),
inference(forward_demodulation,[],[f191746,f147]) ).
fof(f191779,plain,
sF0 = and(a15,sF32),
inference(forward_demodulation,[],[f191765,f127997]) ).
fof(f191867,plain,
or(not(a15),sF0) = or(not(a15),sF32),
inference(superposition,[],[f30583,f191779]) ).
fof(f191882,plain,
or(sF8,sF0) = or(sF8,sF32),
inference(forward_demodulation,[],[f191867,f731]) ).
fof(f191939,plain,
sF32 = or(sF8,sF0),
inference(forward_demodulation,[],[f191882,f190783]) ).
fof(f191969,plain,
sF32 = or(sF0,sF8),
inference(forward_demodulation,[],[f191939,f15]) ).
fof(f191987,plain,
c1 = sF32,
inference(forward_demodulation,[],[f191969,f152330]) ).
fof(f191999,plain,
~ circuit(s1,c1),
inference(backward_demodulation,[],[f36254,f191987]) ).
fof(f192697,plain,
$false,
inference(forward_subsumption_resolution,[],[f191999,f62]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-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.15/0.42 % Computer : n015.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 27 10:55:01 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.47 Running first-order theorem proving
% 0.15/0.47 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
% 16.60/3.43 % (1482661)Input is clausal, will run a generic CNF schedule.
% 16.60/3.43 % (1482669)lrs+10_1_sil=8000:sp=occurrence:random_seed=418375461:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.60/3.43 % (1482672)dis-21_1_sil=8000:lcm=predicate:random_seed=4266706977: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)
% 16.60/3.43 % (1482672)Refutation not found, incomplete strategy
% 16.60/3.43 % (1482672)------------------------------
% 16.60/3.43 % (1482672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.60/3.43 % (1482672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/3.43 % (1482672)CaDiCaL version: 2.1.3
% 16.60/3.43 % (1482672)Termination reason: Refutation not found, incomplete strategy
% 16.60/3.43 % (1482672)Time elapsed: 0.002 s
% 16.60/3.43 % (1482672)Peak memory usage: 88 MB
% 16.60/3.43 % (1482672)Instructions burned: 2 (million)
% 16.60/3.43 % (1482669)Instruction limit reached!
% 16.60/3.43 % (1482669)------------------------------
% 16.60/3.43 % (1482669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.60/3.43 % (1482669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/3.43 % (1482669)CaDiCaL version: 2.1.3
% 16.60/3.43 % (1482669)Termination reason: Instruction limit
% 16.60/3.43 % (1482669)Termination phase: Saturation
% 16.60/3.43 % (1482669)Time elapsed: 0.058 s
% 16.60/3.43 % (1482669)Peak memory usage: 89 MB
% 16.60/3.43 % (1482669)Instructions burned: 107 (million)
% 16.60/3.43 % (1482668)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3410352340:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.60/3.43 % (1482667)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3208385549:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.60/3.43 % (1482666)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=2354888988:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.60/3.43 % (1482670)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3298194963:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.60/3.43 % (1482671)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2451772507:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.60/3.43 % (1482670)Instruction limit reached!
% 16.60/3.43 % (1482670)------------------------------
% 16.60/3.43 % (1482670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.60/3.43 % (1482670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/3.43 % (1482670)CaDiCaL version: 2.1.3
% 16.60/3.43 % (1482670)Termination reason: Instruction limit
% 16.60/3.43 % (1482670)Termination phase: Saturation
% 16.60/3.43 % (1482670)Time elapsed: 0.112 s
% 16.60/3.43 % (1482670)Peak memory usage: 89 MB
% 16.60/3.43 % (1482670)Instructions burned: 115 (million)
% 16.60/3.43 % (1482676)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=1076070284:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 16.60/3.43 % (1482671)Instruction limit reached!
% 16.60/3.43 % (1482671)------------------------------
% 16.60/3.43 % (1482671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.60/3.43 % (1482671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/3.43 % (1482671)CaDiCaL version: 2.1.3
% 16.60/3.43 % (1482671)Termination reason: Instruction limit
% 16.60/3.43 % (1482671)Termination phase: Saturation
% 16.60/3.43 % (1482671)Time elapsed: 0.158 s
% 16.60/3.43 % (1482671)Peak memory usage: 89 MB
% 16.60/3.43 % (1482671)Instructions burned: 180 (million)
% 16.60/3.43 % (1482676)Instruction limit reached!
% 16.60/3.43 % (1482676)------------------------------
% 16.60/3.43 % (1482676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.60/3.43 % (1482676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/3.43 % (1482676)CaDiCaL version: 2.1.3
% 16.60/3.43 % (1482676)Termination reason: Instruction limit
% 16.60/3.43 % (1482676)Termination phase: Saturation
% 16.60/3.43 % (1482676)Time elapsed: 0.077 s
% 16.60/3.43 % (1482676)Peak memory usage: 89 MB
% 16.60/3.43 % (1482676)Instructions burned: 144 (million)
% 16.60/3.43 % (1482672)------------------------------
% 31.93/5.56 % (1482672)------------------------------
% 31.93/5.56 % (1482683)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3479733195:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 31.93/5.56 % (1482686)lrs+10_64_to=lpo:sil=8000:random_seed=3346421910:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 31.93/5.56 % (1482685)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2092540438:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 31.93/5.56 % (1482686)Instruction limit reached!
% 31.93/5.56 % (1482686)------------------------------
% 31.93/5.56 % (1482686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.56 % (1482686)CaDiCaL version: 2.1.3
% 31.93/5.56 % (1482686)Termination reason: Instruction limit
% 31.93/5.56 % (1482686)Termination phase: Saturation
% 31.93/5.56 % (1482686)Time elapsed: 0.096 s
% 31.93/5.56 % (1482686)Peak memory usage: 89 MB
% 31.93/5.56 % (1482686)Instructions burned: 126 (million)
% 31.93/5.56 % (1482687)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=651544072:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 31.93/5.56 % (1482683)Instruction limit reached!
% 31.93/5.56 % (1482683)------------------------------
% 31.93/5.56 % (1482683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.56 % (1482683)CaDiCaL version: 2.1.3
% 31.93/5.56 % (1482683)Termination reason: Instruction limit
% 31.93/5.56 % (1482683)Termination phase: Saturation
% 31.93/5.56 % (1482683)Time elapsed: 0.190 s
% 31.93/5.56 % (1482683)Peak memory usage: 89 MB
% 31.93/5.56 % (1482683)Instructions burned: 190 (million)
% 31.93/5.56 % (1482687)Instruction limit reached!
% 31.93/5.56 % (1482687)------------------------------
% 31.93/5.56 % (1482687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.56 % (1482687)CaDiCaL version: 2.1.3
% 31.93/5.56 % (1482687)Termination reason: Instruction limit
% 31.93/5.56 % (1482687)Termination phase: Saturation
% 31.93/5.56 % (1482687)Time elapsed: 0.106 s
% 31.93/5.56 % (1482687)Peak memory usage: 91 MB
% 31.93/5.56 % (1482687)Instructions burned: 195 (million)
% 31.93/5.56 % (1482685)Instruction limit reached!
% 31.93/5.56 % (1482685)------------------------------
% 31.93/5.56 % (1482685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.56 % (1482685)CaDiCaL version: 2.1.3
% 31.93/5.56 % (1482685)Termination reason: Instruction limit
% 31.93/5.56 % (1482685)Termination phase: Saturation
% 31.93/5.56 % (1482685)Time elapsed: 0.214 s
% 31.93/5.56 % (1482685)Peak memory usage: 90 MB
% 31.93/5.56 % (1482685)Instructions burned: 219 (million)
% 31.93/5.56 % (1482694)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=992149798:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 31.93/5.56 % (1482696)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=3627079939:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 31.93/5.56 % (1482695)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4040839402:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 31.93/5.56 % (1482696)Instruction limit reached!
% 31.93/5.56 % (1482696)------------------------------
% 31.93/5.56 % (1482696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.93/5.56 % (1482696)CaDiCaL version: 2.1.3
% 31.93/5.56 % (1482696)Termination reason: Instruction limit
% 31.93/5.56 % (1482696)Termination phase: Saturation
% 31.93/5.56 % (1482696)Time elapsed: 0.058 s
% 31.93/5.56 % (1482696)Peak memory usage: 89 MB
% 31.93/5.56 % (1482696)Instructions burned: 107 (million)
% 31.93/5.56 % (1482694)Instruction limit reached!
% 31.93/5.56 % (1482694)------------------------------
% 31.93/5.56 % (1482694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.93/5.56 % (1482694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482694)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482694)Termination reason: Instruction limit
% 49.92/8.04 % (1482694)Termination phase: Saturation
% 49.92/8.04 % (1482694)Time elapsed: 0.165 s
% 49.92/8.04 % (1482694)Peak memory usage: 91 MB
% 49.92/8.04 % (1482694)Instructions burned: 157 (million)
% 49.92/8.04 % (1482697)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1707680978:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 49.92/8.04 % (1482697)Instruction limit reached!
% 49.92/8.04 % (1482697)------------------------------
% 49.92/8.04 % (1482697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.92/8.04 % (1482697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482697)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482697)Termination reason: Instruction limit
% 49.92/8.04 % (1482697)Termination phase: Saturation
% 49.92/8.04 % (1482697)Time elapsed: 0.105 s
% 49.92/8.04 % (1482697)Peak memory usage: 89 MB
% 49.92/8.04 % (1482697)Instructions burned: 108 (million)
% 49.92/8.04 % (1482701)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2336493759:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 49.92/8.04 % (1482702)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=72542416:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 49.92/8.04 % (1482705)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3772149172:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 49.92/8.04 % (1482701)Instruction limit reached!
% 49.92/8.04 % (1482701)------------------------------
% 49.92/8.04 % (1482701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.92/8.04 % (1482701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482701)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482701)Termination reason: Instruction limit
% 49.92/8.04 % (1482701)Termination phase: Saturation
% 49.92/8.04 % (1482701)Time elapsed: 0.208 s
% 49.92/8.04 % (1482701)Peak memory usage: 91 MB
% 49.92/8.04 % (1482701)Instructions burned: 242 (million)
% 49.92/8.04 % (1482705)Instruction limit reached!
% 49.92/8.04 % (1482705)------------------------------
% 49.92/8.04 % (1482705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.92/8.04 % (1482705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482705)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482705)Termination reason: Instruction limit
% 49.92/8.04 % (1482705)Termination phase: Saturation
% 49.92/8.04 % (1482705)Time elapsed: 0.063 s
% 49.92/8.04 % (1482705)Peak memory usage: 89 MB
% 49.92/8.04 % (1482705)Instructions burned: 136 (million)
% 49.92/8.04 % (1482710)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2034576592:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 49.92/8.04 % (1482711)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4050267100:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 49.92/8.04 % (1482710)Instruction limit reached!
% 49.92/8.04 % (1482710)------------------------------
% 49.92/8.04 % (1482710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.92/8.04 % (1482710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482710)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482710)Termination reason: Instruction limit
% 49.92/8.04 % (1482710)Termination phase: Saturation
% 49.92/8.04 % (1482710)Time elapsed: 0.257 s
% 49.92/8.04 % (1482710)Peak memory usage: 92 MB
% 49.92/8.04 % (1482710)Instructions burned: 500 (million)
% 49.92/8.04 % (1482711)Instruction limit reached!
% 49.92/8.04 % (1482711)------------------------------
% 49.92/8.04 % (1482711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.92/8.04 % (1482711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.92/8.04 % (1482711)CaDiCaL version: 2.1.3
% 49.92/8.04 % (1482711)Termination reason: Instruction limit
% 49.92/8.04 % (1482711)Termination phase: Saturation
% 49.92/8.04 % (1482711)Time elapsed: 0.196 s
% 49.92/8.04 % (1482711)Peak memory usage: 91 MB
% 49.92/8.04 % (1482711)Instructions burned: 191 (million)
% 49.92/8.04 % (1482714)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1489180178:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 67.67/10.68 % (1482715)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=287363663:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 67.67/10.68 % (1482715)Instruction limit reached!
% 67.67/10.68 % (1482715)------------------------------
% 67.67/10.68 % (1482715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482715)CaDiCaL version: 2.1.3
% 67.67/10.68 % (1482715)Termination reason: Instruction limit
% 67.67/10.68 % (1482715)Termination phase: Saturation
% 67.67/10.68 % (1482715)Time elapsed: 0.147 s
% 67.67/10.68 % (1482715)Peak memory usage: 88 MB
% 67.67/10.68 % (1482715)Instructions burned: 156 (million)
% 67.67/10.68 % (1482714)Instruction limit reached!
% 67.67/10.68 % (1482714)------------------------------
% 67.67/10.68 % (1482714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482714)CaDiCaL version: 2.1.3
% 67.67/10.68 % (1482714)Termination reason: Instruction limit
% 67.67/10.68 % (1482714)Termination phase: Saturation
% 67.67/10.68 % (1482714)Time elapsed: 0.215 s
% 67.67/10.68 % (1482714)Peak memory usage: 90 MB
% 67.67/10.68 % (1482714)Instructions burned: 264 (million)
% 67.67/10.68 % (1482720)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1621428074:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi)
% 67.67/10.68 % (1482721)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3368770434:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 67.67/10.68 % (1482721)Instruction limit reached!
% 67.67/10.68 % (1482721)------------------------------
% 67.67/10.68 % (1482721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482721)CaDiCaL version: 2.1.3
% 67.67/10.68 % (1482721)Termination reason: Instruction limit
% 67.67/10.68 % (1482721)Termination phase: Saturation
% 67.67/10.68 % (1482721)Time elapsed: 0.448 s
% 67.67/10.68 % (1482721)Peak memory usage: 94 MB
% 67.67/10.68 % (1482721)Instructions burned: 538 (million)
% 67.67/10.68 % (1482695)Instruction limit reached!
% 67.67/10.68 % (1482695)------------------------------
% 67.67/10.68 % (1482695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482695)CaDiCaL version: 2.1.3
% 67.67/10.68 % (1482695)Termination reason: Instruction limit
% 67.67/10.68 % (1482695)Termination phase: Saturation
% 67.67/10.68 % (1482695)Time elapsed: 2.351 s
% 67.67/10.68 % (1482695)Peak memory usage: 152 MB
% 67.67/10.68 % (1482695)Instructions burned: 3395 (million)
% 67.67/10.68 % (1482726)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=556310573:i=180:bd=preordered:av=off_2966 on theBenchmark for (2966ds/180Mi)
% 67.67/10.68 % (1482727)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=1539438413:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 67.67/10.68 % (1482726)Instruction limit reached!
% 67.67/10.68 % (1482726)------------------------------
% 67.67/10.68 % (1482726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482726)CaDiCaL version: 2.1.3
% 67.67/10.68 % (1482726)Termination reason: Instruction limit
% 67.67/10.68 % (1482726)Termination phase: Saturation
% 67.67/10.68 % (1482726)Time elapsed: 0.177 s
% 67.67/10.68 % (1482726)Peak memory usage: 89 MB
% 67.67/10.68 % (1482726)Instructions burned: 180 (million)
% 67.67/10.68 % (1482730)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1168440888:i=412:gtgl=4:gtg=exists_all_2962 on theBenchmark for (2962ds/412Mi)
% 67.67/10.68 % (1482730)Instruction limit reached!
% 67.67/10.68 % (1482730)------------------------------
% 67.67/10.68 % (1482730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.67/10.68 % (1482730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.67/10.68 % (1482730)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482730)Termination reason: Instruction limit
% 81.38/12.58 % (1482730)Termination phase: Saturation
% 81.38/12.58 % (1482730)Time elapsed: 0.400 s
% 81.38/12.58 % (1482730)Peak memory usage: 95 MB
% 81.38/12.58 % (1482730)Instructions burned: 413 (million)
% 81.38/12.58 % (1482735)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1652471576:s2pl=no:i=8478:s2at=4:nm=6_2955 on theBenchmark for (2955ds/8478Mi)
% 81.38/12.58 % (1482720)Instruction limit reached!
% 81.38/12.58 % (1482720)------------------------------
% 81.38/12.58 % (1482720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.58 % (1482720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.58 % (1482720)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482720)Termination reason: Instruction limit
% 81.38/12.58 % (1482720)Termination phase: Saturation
% 81.38/12.58 % (1482720)Time elapsed: 3.024 s
% 81.38/12.58 % (1482720)Peak memory usage: 149 MB
% 81.38/12.58 % (1482720)Instructions burned: 3256 (million)
% 81.38/12.58 % (1482744)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2925949121:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2941 on theBenchmark for (2941ds/303Mi)
% 81.38/12.58 % (1482744)Refutation not found, incomplete strategy
% 81.38/12.58 % (1482744)------------------------------
% 81.38/12.58 % (1482744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.58 % (1482744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.58 % (1482744)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482744)Termination reason: Refutation not found, incomplete strategy
% 81.38/12.58 % (1482744)Time elapsed: 0.003 s
% 81.38/12.58 % (1482744)Peak memory usage: 88 MB
% 81.38/12.58 % (1482744)Instructions burned: 4 (million)
% 81.38/12.58 % (1482702)Instruction limit reached!
% 81.38/12.58 % (1482702)------------------------------
% 81.38/12.58 % (1482702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.58 % (1482702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.58 % (1482702)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482702)Termination reason: Instruction limit
% 81.38/12.58 % (1482702)Termination phase: Saturation
% 81.38/12.58 % (1482702)Time elapsed: 4.731 s
% 81.38/12.58 % (1482702)Peak memory usage: 171 MB
% 81.38/12.58 % (1482702)Instructions burned: 5208 (million)
% 81.38/12.58 % (1482744)------------------------------
% 81.38/12.58 % (1482744)------------------------------
% 81.38/12.58 % (1482822)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=734459022:st=4:i=720:sd=3:fsr=off:ss=axioms_2937 on theBenchmark for (2937ds/720Mi)
% 81.38/12.58 % (1482823)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1947863909:i=598:bs=on:bd=preordered:av=off:ss=axioms_2937 on theBenchmark for (2937ds/598Mi)
% 81.38/12.58 % (1482823)Instruction limit reached!
% 81.38/12.58 % (1482823)------------------------------
% 81.38/12.58 % (1482823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.58 % (1482823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.58 % (1482823)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482823)Termination reason: Instruction limit
% 81.38/12.58 % (1482823)Termination phase: Saturation
% 81.38/12.58 % (1482823)Time elapsed: 0.354 s
% 81.38/12.58 % (1482823)Peak memory usage: 93 MB
% 81.38/12.58 % (1482823)Instructions burned: 599 (million)
% 81.38/12.58 % (1482822)Instruction limit reached!
% 81.38/12.58 % (1482822)------------------------------
% 81.38/12.58 % (1482822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.58 % (1482822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.58 % (1482822)CaDiCaL version: 2.1.3
% 81.38/12.58 % (1482822)Termination reason: Instruction limit
% 81.38/12.58 % (1482822)Termination phase: Saturation
% 81.38/12.58 % (1482822)Time elapsed: 0.420 s
% 81.38/12.58 % (1482822)Peak memory usage: 93 MB
% 81.38/12.58 % (1482822)Instructions burned: 722 (million)
% 81.38/12.58 % (1482880)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1766822840:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 81.38/12.58 % (1482896)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2128635614:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2931 on theBenchmark for (2931ds/1997Mi)
% 59.34/14.06 % (1482896)Instruction limit reached!
% 59.34/14.06 % (1482896)------------------------------
% 59.34/14.06 % (1482896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482896)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482896)Termination reason: Instruction limit
% 59.34/14.06 % (1482896)Termination phase: Saturation
% 59.34/14.06 % (1482896)Time elapsed: 1.202 s
% 59.34/14.06 % (1482896)Peak memory usage: 139 MB
% 59.34/14.06 % (1482896)Instructions burned: 1998 (million)
% 59.34/14.06 % (1482727)Instruction limit reached!
% 59.34/14.06 % (1482727)------------------------------
% 59.34/14.06 % (1482727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482727)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482727)Termination reason: Instruction limit
% 59.34/14.06 % (1482727)Termination phase: Saturation
% 59.34/14.06 % (1482727)Time elapsed: 4.496 s
% 59.34/14.06 % (1482727)Peak memory usage: 208 MB
% 59.34/14.06 % (1482727)Instructions burned: 10309 (million)
% 59.34/14.06 % (1482904)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4292396263:i=1098:nicw=on_2917 on theBenchmark for (2917ds/1098Mi)
% 59.34/14.06 % (1482903)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=327463223:i=2088:bd=preordered:av=off_2918 on theBenchmark for (2918ds/2088Mi)
% 59.34/14.06 % (1482880)Instruction limit reached!
% 59.34/14.06 % (1482880)------------------------------
% 59.34/14.06 % (1482880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482880)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482880)Termination reason: Instruction limit
% 59.34/14.06 % (1482880)Termination phase: Saturation
% 59.34/14.06 % (1482880)Time elapsed: 1.707 s
% 59.34/14.06 % (1482880)Peak memory usage: 148 MB
% 59.34/14.06 % (1482880)Instructions burned: 2990 (million)
% 59.34/14.06 % (1482904)Instruction limit reached!
% 59.34/14.06 % (1482904)------------------------------
% 59.34/14.06 % (1482904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482904)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482904)Termination reason: Instruction limit
% 59.34/14.06 % (1482904)Termination phase: Saturation
% 59.34/14.06 % (1482904)Time elapsed: 0.344 s
% 59.34/14.06 % (1482904)Peak memory usage: 101 MB
% 59.34/14.06 % (1482904)Instructions burned: 1100 (million)
% 59.34/14.06 % (1482907)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=657698855:i=433:bd=preordered_2913 on theBenchmark for (2913ds/433Mi)
% 59.34/14.06 % (1482908)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=597341699:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2913 on theBenchmark for (2913ds/2942Mi)
% 59.34/14.06 % (1482907)Instruction limit reached!
% 59.34/14.06 % (1482907)------------------------------
% 59.34/14.06 % (1482907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482907)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482907)Termination reason: Instruction limit
% 59.34/14.06 % (1482907)Termination phase: Saturation
% 59.34/14.06 % (1482907)Time elapsed: 0.271 s
% 59.34/14.06 % (1482907)Peak memory usage: 95 MB
% 59.34/14.06 % (1482907)Instructions burned: 435 (million)
% 59.34/14.06 % (1482911)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1899854666:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2909 on theBenchmark for (2909ds/6922Mi)
% 59.34/14.06 % (1482903)Instruction limit reached!
% 59.34/14.06 % (1482903)------------------------------
% 59.34/14.06 % (1482903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482903)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482903)Termination reason: Instruction limit
% 59.34/14.06 % (1482903)Termination phase: Saturation
% 59.34/14.06 % (1482903)Time elapsed: 1.284 s
% 59.34/14.06 % (1482903)Peak memory usage: 139 MB
% 59.34/14.06 % (1482903)Instructions burned: 2090 (million)
% 59.34/14.06 % (1482913)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3540238497:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2903 on theBenchmark for (2903ds/596Mi)
% 59.34/14.06 % (1482913)Refutation not found, incomplete strategy
% 59.34/14.06 % (1482913)------------------------------
% 59.34/14.06 % (1482913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482913)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482913)Termination reason: Refutation not found, incomplete strategy
% 59.34/14.06 % (1482913)Time elapsed: 0.003 s
% 59.34/14.06 % (1482913)Peak memory usage: 88 MB
% 59.34/14.06 % (1482913)Instructions burned: 4 (million)
% 59.34/14.06 % (1482908)Instruction limit reached!
% 59.34/14.06 % (1482908)------------------------------
% 59.34/14.06 % (1482908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482908)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482908)Termination reason: Instruction limit
% 59.34/14.06 % (1482908)Termination phase: Saturation
% 59.34/14.06 % (1482908)Time elapsed: 1.053 s
% 59.34/14.06 % (1482908)Peak memory usage: 154 MB
% 59.34/14.06 % (1482908)Instructions burned: 2943 (million)
% 59.34/14.06 % (1482915)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=57325944:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2901 on theBenchmark for (2901ds/4123Mi)
% 59.34/14.06 % (1482735)Instruction limit reached!
% 59.34/14.06 % (1482735)------------------------------
% 59.34/14.06 % (1482735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482735)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482735)Termination reason: Instruction limit
% 59.34/14.06 % (1482735)Termination phase: Saturation
% 59.34/14.06 % (1482735)Time elapsed: 5.217 s
% 59.34/14.06 % (1482735)Peak memory usage: 194 MB
% 59.34/14.06 % (1482735)Instructions burned: 8480 (million)
% 59.34/14.06 % (1482913)------------------------------
% 59.34/14.06 % (1482913)------------------------------
% 59.34/14.06 % (1482917)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2838916834:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2899 on theBenchmark for (2899ds/16411Mi)
% 59.34/14.06 % (1482918)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1318964361:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2899 on theBenchmark for (2899ds/1670Mi)
% 59.34/14.06 % (1482918)Instruction limit reached!
% 59.34/14.06 % (1482918)------------------------------
% 59.34/14.06 % (1482918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482918)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482918)Termination reason: Instruction limit
% 59.34/14.06 % (1482918)Termination phase: Saturation
% 59.34/14.06 % (1482918)Time elapsed: 1.064 s
% 59.34/14.06 % (1482918)Peak memory usage: 136 MB
% 59.34/14.06 % (1482918)Instructions burned: 1670 (million)
% 59.34/14.06 % (1482915)Instruction limit reached!
% 59.34/14.06 % (1482915)------------------------------
% 59.34/14.06 % (1482915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482915)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482915)Termination reason: Instruction limit
% 59.34/14.06 % (1482915)Termination phase: Saturation
% 59.34/14.06 % (1482915)Time elapsed: 1.373 s
% 59.34/14.06 % (1482915)Peak memory usage: 160 MB
% 59.34/14.06 % (1482915)Instructions burned: 4123 (million)
% 59.34/14.06 % (1482921)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=324987420:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2887 on theBenchmark for (2887ds/1722Mi)
% 59.34/14.06 % (1482922)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=365298252:cts=off:cond=on:i=9530:bs=on:fsd=on_2886 on theBenchmark for (2886ds/9530Mi)
% 59.34/14.06 % (1482921)Instruction limit reached!
% 59.34/14.06 % (1482921)------------------------------
% 59.34/14.06 % (1482921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.34/14.06 % (1482921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.34/14.06 % (1482921)CaDiCaL version: 2.1.3
% 59.34/14.06 % (1482921)Termination reason: Instruction limit
% 59.34/14.06 % (1482921)Termination phase: Saturation
% 59.34/14.06 % (1482921)Time elapsed: 1.074 s
% 59.34/14.06 % (1482921)Peak memory usage: 136 MB
% 59.34/14.06 % (1482921)Instructions burned: 1723 (million)
% 59.34/14.06 % (1482668)First to succeed.
% 59.34/14.06 % (1482668)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1482661"
% 59.34/14.06 % (1483055)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=430733330:st=2:i=4495:sd=10:ss=included_2874 on theBenchmark for (2874ds/4495Mi)
% 59.34/14.06 % (1482668)Refutation found. Thanks to Tanya!
% 59.34/14.06 % SZS status Unsatisfiable for theBenchmark
% 59.34/14.06 % SZS output start Proof for theBenchmark
% See solution above
% 92.71/14.25 % (1482668)------------------------------
% 92.71/14.25 % (1482668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 92.71/14.25 % (1482668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 92.71/14.25 % (1482668)CaDiCaL version: 2.1.3
% 92.71/14.25 % (1482668)Termination reason: Refutation
% 92.71/14.25 % (1482668)Time elapsed: 12.413 s
% 92.71/14.25 % (1482668)Peak memory usage: 260 MB
% 92.71/14.25 % (1482668)Instructions burned: 16418 (million)
% 92.71/14.25 % (1482668)------------------------------
% 92.71/14.25 % (1482668)------------------------------
% 92.71/14.25 % (1482661)Success in time 12.984 s
% 92.71/14.25 % Vampire exiting
%------------------------------------------------------------------------------