%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:09 AM UTC 2026
% Result : Unsatisfiable 43.44s 12.05s
% Output : Refutation 78.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 70
% Syntax : Number of formulae : 738 ( 730 unt; 34 def)
% Number of atoms : 746 ( 731 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 17 ( 9 ~; 6 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 52 ( 52 usr; 48 con; 0-2 aty)
% Number of variables : 631 ( 0 sgn 631 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : or(X0,X1) = or(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_commutative) ).
fof(f2,axiom,
! [X0,X1] : and(X0,X1) = and(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_commutative) ).
fof(f3,axiom,
! [X2,X0,X1] : or(or(X0,X1),X2) = or(X0,or(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_associative) ).
fof(f4,axiom,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X0,and(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_associative) ).
fof(f5,axiom,
! [X0] : or(X0,ll0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_identity) ).
fof(f6,axiom,
! [X0] : and(X0,ll1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_identity) ).
fof(f7,axiom,
! [X2,X0,X1] : and(X0,or(X1,X2)) = or(and(X0,X1),and(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_distributive) ).
fof(f8,axiom,
! [X2,X0,X1] : or(X0,and(X1,X2)) = and(or(X0,X1),or(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_distributive) ).
fof(f9,axiom,
! [X0] : or(X0,not(X0)) = ll1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_complement) ).
fof(f10,plain,
! [X0] : ll1 = or(X0,not(X0)),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : and(X0,not(X0)) = ll0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_complement) ).
fof(f12,plain,
! [X0] : ll0 = and(X0,not(X0)),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X0] : or(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_idempotent) ).
fof(f14,axiom,
! [X0] : and(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_idempotent) ).
fof(f15,axiom,
! [X0] : not(not(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_involution) ).
fof(f16,axiom,
not(ll0) = ll1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ll0_inverse) ).
fof(f17,plain,
ll1 = not(ll0),
inference(reorient_equations,[],[f16]) ).
fof(f18,axiom,
not(ll1) = ll0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ll1_inverse) ).
fof(f19,plain,
ll0 = not(ll1),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X0] : or(X0,ll1) = ll1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_boundedness) ).
fof(f21,plain,
! [X0] : ll1 = or(X0,ll1),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0] : and(X0,ll0) = ll0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_boundedness) ).
fof(f23,plain,
! [X0] : ll0 = and(X0,ll0),
inference(reorient_equations,[],[f22]) ).
fof(f24,axiom,
! [X0,X1] : or(X0,and(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_absorption) ).
fof(f25,axiom,
! [X0,X1] : and(X0,or(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_absorption) ).
fof(f26,axiom,
! [X0,X1] : not(or(X0,X1)) = and(not(X0),not(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_demorgan) ).
fof(f27,axiom,
! [X0,X1] : not(and(X0,X1)) = or(not(X0),not(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_demorgan) ).
fof(f28,axiom,
! [X0,X1] : or(and(not(X0),X1),and(X0,not(X1))) = xor(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xor_definition) ).
fof(f29,axiom,
! [X0,X1] : xor(X0,X1) = xor(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xor_commutative) ).
fof(f30,axiom,
! [X2,X0,X1] : xor(X0,xor(X1,X2)) = xor(xor(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xor_associative) ).
fof(f31,negated_conjecture,
xor(xor(a,b),cin) = sum_def,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_def) ).
fof(f32,negated_conjecture,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',carry_def) ).
fof(f33,negated_conjecture,
not(and(a,b)) = t1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1) ).
fof(f34,negated_conjecture,
not(and(a,t1)) = t2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2) ).
fof(f35,negated_conjecture,
not(and(b,t1)) = t3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3) ).
fof(f36,negated_conjecture,
not(and(t2,t3)) = t4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4) ).
fof(f37,negated_conjecture,
not(and(t4,cin)) = t5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5) ).
fof(f38,negated_conjecture,
not(and(t4,t5)) = t6,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6) ).
fof(f39,negated_conjecture,
not(and(t5,cin)) = t7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7) ).
fof(f40,negated_conjecture,
not(and(t6,t7)) = sum,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum) ).
fof(f41,negated_conjecture,
not(and(t1,t5)) = carry,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',carry) ).
fof(f42,negated_conjecture,
( sum != sum_def
| carry != carry_def ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_circuit) ).
fof(f43,plain,
( sum_def != sum
| carry_def != carry ),
inference(reorient_equations,[],[f42]) ).
fof(f44,plain,
! [X0,X1] : or(and(not(X0),X1),and(X0,not(X1))) = or(and(not(X1),X0),and(X1,not(X0))),
inference(definition_unfolding,[],[f29,f28,f28]) ).
fof(f45,plain,
! [X2,X0,X1] : or(and(not(X0),or(and(not(X1),X2),and(X1,not(X2)))),and(X0,not(or(and(not(X1),X2),and(X1,not(X2)))))) = or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X2),and(or(and(not(X0),X1),and(X0,not(X1))),not(X2))),
inference(definition_unfolding,[],[f30,f28,f28,f28,f28]) ).
fof(f46,plain,
sum_def = or(and(not(or(and(not(a),b),and(a,not(b)))),cin),and(or(and(not(a),b),and(a,not(b))),not(cin))),
inference(definition_unfolding,[],[f31,f28,f28]) ).
fof(f47,definition,
sF0 = not(a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f48,plain,
not(a) = sF0,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF1 = and(sF0,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f50,plain,
and(sF0,b) = sF1,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF2 = not(b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f52,plain,
not(b) = sF2,
inference(reorient_equations,[],[f51]) ).
fof(f53,definition,
sF3 = and(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f54,plain,
and(a,sF2) = sF3,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF4 = or(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f56,plain,
or(sF1,sF3) = sF4,
inference(reorient_equations,[],[f55]) ).
fof(f57,definition,
sF5 = not(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f58,plain,
not(sF4) = sF5,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF6 = and(sF5,cin),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f60,plain,
and(sF5,cin) = sF6,
inference(reorient_equations,[],[f59]) ).
fof(f61,definition,
sF7 = not(cin),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f62,plain,
not(cin) = sF7,
inference(reorient_equations,[],[f61]) ).
fof(f63,definition,
sF8 = and(sF4,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f64,plain,
and(sF4,sF7) = sF8,
inference(reorient_equations,[],[f63]) ).
fof(f65,definition,
sF9 = or(sF6,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f66,plain,
or(sF6,sF8) = sF9,
inference(reorient_equations,[],[f65]) ).
fof(f67,plain,
sum_def = sF9,
inference(definition_folding,[],[f46,f66,f64,f62,f56,f54,f52,f50,f48,f60,f58,f56,f54,f52,f50,f48]) ).
fof(f68,definition,
sF10 = or(a,b),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f69,plain,
or(a,b) = sF10,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF11 = and(cin,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f71,plain,
and(cin,sF10) = sF11,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF12 = and(a,b),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f73,plain,
and(a,b) = sF12,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF13 = and(sF7,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f75,plain,
and(sF7,sF12) = sF13,
inference(reorient_equations,[],[f74]) ).
fof(f76,definition,
sF14 = or(sF11,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f77,plain,
or(sF11,sF13) = sF14,
inference(reorient_equations,[],[f76]) ).
fof(f78,plain,
carry_def = sF14,
inference(definition_folding,[],[f32,f77,f75,f73,f62,f71,f69]) ).
fof(f79,definition,
sF15 = not(sF12),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f80,plain,
not(sF12) = sF15,
inference(reorient_equations,[],[f79]) ).
fof(f81,plain,
t1 = sF15,
inference(definition_folding,[],[f33,f80,f73]) ).
fof(f82,definition,
sF16 = and(a,t1),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f83,plain,
and(a,t1) = sF16,
inference(reorient_equations,[],[f82]) ).
fof(f84,definition,
sF17 = not(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f85,plain,
not(sF16) = sF17,
inference(reorient_equations,[],[f84]) ).
fof(f86,plain,
t2 = sF17,
inference(definition_folding,[],[f34,f85,f83]) ).
fof(f87,definition,
sF18 = and(b,t1),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f88,plain,
and(b,t1) = sF18,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF19 = not(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f90,plain,
not(sF18) = sF19,
inference(reorient_equations,[],[f89]) ).
fof(f91,plain,
t3 = sF19,
inference(definition_folding,[],[f35,f90,f88]) ).
fof(f92,definition,
sF20 = and(t2,t3),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f93,plain,
and(t2,t3) = sF20,
inference(reorient_equations,[],[f92]) ).
fof(f94,definition,
sF21 = not(sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f95,plain,
not(sF20) = sF21,
inference(reorient_equations,[],[f94]) ).
fof(f96,plain,
t4 = sF21,
inference(definition_folding,[],[f36,f95,f93]) ).
fof(f97,definition,
sF22 = and(t4,cin),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f98,plain,
and(t4,cin) = sF22,
inference(reorient_equations,[],[f97]) ).
fof(f99,definition,
sF23 = not(sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f100,plain,
not(sF22) = sF23,
inference(reorient_equations,[],[f99]) ).
fof(f101,plain,
t5 = sF23,
inference(definition_folding,[],[f37,f100,f98]) ).
fof(f102,definition,
sF24 = and(t4,t5),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f103,plain,
and(t4,t5) = sF24,
inference(reorient_equations,[],[f102]) ).
fof(f104,definition,
sF25 = not(sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f105,plain,
not(sF24) = sF25,
inference(reorient_equations,[],[f104]) ).
fof(f106,plain,
t6 = sF25,
inference(definition_folding,[],[f38,f105,f103]) ).
fof(f107,definition,
sF26 = and(t5,cin),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f108,plain,
and(t5,cin) = sF26,
inference(reorient_equations,[],[f107]) ).
fof(f109,definition,
sF27 = not(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f110,plain,
not(sF26) = sF27,
inference(reorient_equations,[],[f109]) ).
fof(f111,plain,
t7 = sF27,
inference(definition_folding,[],[f39,f110,f108]) ).
fof(f112,definition,
sF28 = and(t6,t7),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f113,plain,
and(t6,t7) = sF28,
inference(reorient_equations,[],[f112]) ).
fof(f114,definition,
sF29 = not(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f115,plain,
not(sF28) = sF29,
inference(reorient_equations,[],[f114]) ).
fof(f116,plain,
sum = sF29,
inference(definition_folding,[],[f40,f115,f113]) ).
fof(f117,definition,
sF30 = and(t1,t5),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f118,plain,
and(t1,t5) = sF30,
inference(reorient_equations,[],[f117]) ).
fof(f119,definition,
sF31 = not(sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f120,plain,
not(sF30) = sF31,
inference(reorient_equations,[],[f119]) ).
fof(f121,plain,
carry = sF31,
inference(definition_folding,[],[f41,f120,f118]) ).
fof(f123,definition,
( spl32_1
<=> carry_def = carry ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f125,plain,
( carry_def != carry
| spl32_1 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f127,definition,
( spl32_2
<=> sum_def = sum ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f130,plain,
( ~ spl32_1
| ~ spl32_2 ),
inference(avatar_split_clause,[],[f43,f127,f123]) ).
fof(f131,plain,
sF1 = and(b,sF0),
inference(forward_demodulation,[],[f50,f2]) ).
fof(f132,plain,
sF6 = and(cin,sF5),
inference(forward_demodulation,[],[f60,f2]) ).
fof(f133,plain,
sF8 = and(sF4,not(cin)),
inference(forward_demodulation,[],[f64,f62]) ).
fof(f134,plain,
sum_def = or(sF6,sF8),
inference(forward_demodulation,[],[f66,f67]) ).
fof(f135,plain,
sF13 = and(sF7,and(a,b)),
inference(forward_demodulation,[],[f75,f73]) ).
fof(f136,plain,
carry_def = or(sF11,sF13),
inference(forward_demodulation,[],[f77,f78]) ).
fof(f137,plain,
t1 = not(sF12),
inference(forward_demodulation,[],[f80,f81]) ).
fof(f138,plain,
sF16 = and(t1,a),
inference(forward_demodulation,[],[f83,f2]) ).
fof(f139,plain,
t2 = not(sF16),
inference(forward_demodulation,[],[f85,f86]) ).
fof(f140,plain,
sF18 = and(t1,b),
inference(forward_demodulation,[],[f88,f2]) ).
fof(f141,plain,
t3 = not(sF18),
inference(forward_demodulation,[],[f90,f91]) ).
fof(f142,plain,
t4 = not(sF20),
inference(forward_demodulation,[],[f95,f96]) ).
fof(f143,plain,
t5 = not(sF22),
inference(forward_demodulation,[],[f100,f101]) ).
fof(f144,plain,
t6 = not(sF24),
inference(forward_demodulation,[],[f105,f106]) ).
fof(f145,plain,
t7 = not(sF26),
inference(forward_demodulation,[],[f110,f111]) ).
fof(f146,plain,
sum = not(sF28),
inference(forward_demodulation,[],[f115,f116]) ).
fof(f147,plain,
carry = not(sF30),
inference(forward_demodulation,[],[f120,f121]) ).
fof(f148,plain,
sF8 = and(not(cin),sF4),
inference(forward_demodulation,[],[f133,f2]) ).
fof(f149,plain,
sF13 = and(and(a,b),sF7),
inference(forward_demodulation,[],[f135,f2]) ).
fof(f150,plain,
not(and(a,b)) = t1,
inference(forward_demodulation,[],[f137,f73]) ).
fof(f151,plain,
not(and(t2,t3)) = t4,
inference(forward_demodulation,[],[f142,f93]) ).
fof(f152,plain,
not(and(t4,t5)) = t6,
inference(forward_demodulation,[],[f144,f103]) ).
fof(f153,plain,
not(and(t6,t7)) = sum,
inference(forward_demodulation,[],[f146,f113]) ).
fof(f154,plain,
not(and(t1,t5)) = carry,
inference(forward_demodulation,[],[f147,f118]) ).
fof(f155,plain,
sF13 = and(a,and(b,sF7)),
inference(forward_demodulation,[],[f149,f4]) ).
fof(f156,plain,
sF13 = and(a,and(b,not(cin))),
inference(forward_demodulation,[],[f155,f62]) ).
fof(f182,plain,
! [X0,X1] : or(X1,and(X0,X1)) = X1,
inference(superposition,[],[f24,f2]) ).
fof(f189,plain,
! [X0] : or(sF11,and(sF13,X0)) = and(carry_def,or(sF11,X0)),
inference(superposition,[],[f8,f136]) ).
fof(f211,plain,
! [X2,X0,X1] : and(X1,or(X0,X2)) = or(and(X0,X1),and(X1,X2)),
inference(superposition,[],[f7,f2]) ).
fof(f214,plain,
! [X2,X0,X1] : and(not(X0),or(X2,not(X1))) = or(and(not(X0),X2),not(or(X0,X1))),
inference(superposition,[],[f7,f26]) ).
fof(f231,plain,
! [X0,X1] : or(X0,X1) = or(or(X0,X1),X0),
inference(superposition,[],[f182,f25]) ).
fof(f237,plain,
! [X2,X0,X1] : and(or(X0,X1),X0) = or(X0,and(X1,and(X2,X0))),
inference(superposition,[],[f8,f182]) ).
fof(f242,plain,
! [X2,X0,X1] : and(X0,or(X0,X1)) = or(X0,and(X1,and(X2,X0))),
inference(forward_demodulation,[],[f237,f2]) ).
fof(f245,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X1,X0)),
inference(forward_demodulation,[],[f231,f3]) ).
fof(f247,plain,
! [X2,X0,X1] : or(X0,and(X1,and(X2,X0))) = X0,
inference(forward_demodulation,[],[f242,f25]) ).
fof(f252,plain,
! [X0] : not(or(a,X0)) = and(sF0,not(X0)),
inference(superposition,[],[f26,f48]) ).
fof(f257,plain,
! [X0] : not(or(b,X0)) = and(sF2,not(X0)),
inference(superposition,[],[f26,f52]) ).
fof(f264,plain,
! [X0] : and(ll1,X0) = X0,
inference(superposition,[],[f2,f6]) ).
fof(f275,plain,
! [X0] : not(and(a,X0)) = or(sF0,not(X0)),
inference(superposition,[],[f27,f48]) ).
fof(f276,plain,
! [X0] : not(and(b,X0)) = or(sF2,not(X0)),
inference(superposition,[],[f27,f52]) ).
fof(f285,plain,
! [X0] : not(and(X0,a)) = or(not(X0),sF0),
inference(superposition,[],[f27,f48]) ).
fof(f316,plain,
! [X2,X0,X1] : or(X1,and(X2,X0)) = and(or(X1,X2),or(X0,X1)),
inference(superposition,[],[f8,f1]) ).
fof(f317,plain,
! [X2,X0,X1] : or(X1,and(X0,X2)) = and(or(X0,X1),or(X1,X2)),
inference(superposition,[],[f8,f1]) ).
fof(f318,plain,
! [X0,X1] : and(X1,or(X0,X1)) = X1,
inference(superposition,[],[f25,f1]) ).
fof(f321,plain,
! [X0,X1] : and(X0,X1) = and(and(X0,X1),X0),
inference(superposition,[],[f318,f24]) ).
fof(f325,plain,
! [X2,X0,X1] : and(X0,X2) = and(and(X0,X2),and(X0,or(X1,X2))),
inference(superposition,[],[f318,f7]) ).
fof(f341,plain,
! [X2,X0,X1] : and(X0,X2) = and(X0,and(X2,and(X0,or(X1,X2)))),
inference(forward_demodulation,[],[f325,f4]) ).
fof(f343,plain,
! [X0,X1] : and(X0,X1) = and(X0,and(X1,X0)),
inference(forward_demodulation,[],[f321,f4]) ).
fof(f352,plain,
! [X0] : and(t1,or(b,X0)) = or(sF18,and(t1,X0)),
inference(superposition,[],[f7,f140]) ).
fof(f358,plain,
! [X0] : or(ll0,X0) = X0,
inference(superposition,[],[f1,f5]) ).
fof(f421,plain,
and(a,b) = not(t1),
inference(superposition,[],[f15,f150]) ).
fof(f422,plain,
and(t1,t5) = not(carry),
inference(superposition,[],[f15,f154]) ).
fof(f423,plain,
and(t2,t3) = not(t4),
inference(superposition,[],[f15,f151]) ).
fof(f424,plain,
and(t4,t5) = not(t6),
inference(superposition,[],[f15,f152]) ).
fof(f425,plain,
and(t6,t7) = not(sum),
inference(superposition,[],[f15,f153]) ).
fof(f426,plain,
a = not(sF0),
inference(superposition,[],[f15,f48]) ).
fof(f428,plain,
sF4 = not(sF5),
inference(superposition,[],[f15,f58]) ).
fof(f429,plain,
sF16 = not(t2),
inference(superposition,[],[f15,f139]) ).
fof(f430,plain,
sF18 = not(t3),
inference(superposition,[],[f15,f141]) ).
fof(f431,plain,
sF22 = not(t5),
inference(superposition,[],[f15,f143]) ).
fof(f432,plain,
sF26 = not(t7),
inference(superposition,[],[f15,f145]) ).
fof(f433,plain,
! [X0,X1] : not(and(X1,not(X0))) = or(not(X1),X0),
inference(superposition,[],[f27,f15]) ).
fof(f434,plain,
! [X0,X1] : or(X0,not(X1)) = not(and(not(X0),X1)),
inference(superposition,[],[f27,f15]) ).
fof(f435,plain,
! [X0,X1] : and(not(X1),X0) = not(or(X1,not(X0))),
inference(superposition,[],[f26,f15]) ).
fof(f436,plain,
! [X0,X1] : and(X0,not(X1)) = not(or(not(X0),X1)),
inference(superposition,[],[f26,f15]) ).
fof(f437,plain,
and(t5,cin) = not(t7),
inference(backward_demodulation,[],[f108,f432]) ).
fof(f447,plain,
and(t4,cin) = not(t5),
inference(backward_demodulation,[],[f98,f431]) ).
fof(f457,plain,
and(t1,b) = not(t3),
inference(backward_demodulation,[],[f140,f430]) ).
fof(f465,plain,
! [X0] : and(t1,or(b,X0)) = or(not(t3),and(t1,X0)),
inference(backward_demodulation,[],[f352,f430]) ).
fof(f467,plain,
and(t1,a) = not(t2),
inference(backward_demodulation,[],[f138,f429]) ).
fof(f477,plain,
or(sF1,sF3) = not(sF5),
inference(backward_demodulation,[],[f56,f428]) ).
fof(f479,plain,
sF8 = and(not(cin),not(sF5)),
inference(backward_demodulation,[],[f148,f428]) ).
fof(f521,plain,
sF8 = not(or(cin,sF5)),
inference(forward_demodulation,[],[f479,f26]) ).
fof(f532,plain,
or(cin,sF5) = not(sF8),
inference(superposition,[],[f15,f521]) ).
fof(f542,plain,
! [X2,X0,X1] : or(X0,X2) = or(X0,or(and(X0,X1),X2)),
inference(superposition,[],[f3,f24]) ).
fof(f543,plain,
! [X2,X0,X1] : or(X0,X2) = or(X0,or(and(X1,X0),X2)),
inference(superposition,[],[f3,f182]) ).
fof(f562,plain,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(X2,or(X0,X1)),
inference(superposition,[],[f1,f3]) ).
fof(f584,plain,
! [X0,X1] : or(X0,and(not(X0),X1)) = and(ll1,or(X0,X1)),
inference(superposition,[],[f8,f10]) ).
fof(f585,plain,
! [X0,X1] : or(X0,and(X1,not(X0))) = and(or(X0,X1),ll1),
inference(superposition,[],[f8,f10]) ).
fof(f592,plain,
! [X0,X1] : or(X0,X1) = or(X0,and(X1,not(X0))),
inference(forward_demodulation,[],[f585,f6]) ).
fof(f593,plain,
! [X0,X1] : or(X0,X1) = or(X0,and(not(X0),X1)),
inference(forward_demodulation,[],[f584,f264]) ).
fof(f604,plain,
! [X0,X1] : and(X0,or(X1,not(X0))) = or(and(X0,X1),ll0),
inference(superposition,[],[f7,f12]) ).
fof(f605,plain,
! [X0,X1] : or(ll0,and(X0,X1)) = and(X0,or(not(X0),X1)),
inference(superposition,[],[f7,f12]) ).
fof(f609,plain,
! [X0,X1] : and(X0,X1) = and(X0,or(not(X0),X1)),
inference(forward_demodulation,[],[f605,f358]) ).
fof(f610,plain,
! [X0,X1] : and(X0,X1) = and(X0,or(X1,not(X0))),
inference(forward_demodulation,[],[f604,f5]) ).
fof(f615,plain,
! [X0,X1] : and(not(X0),X1) = and(not(X0),or(X1,X0)),
inference(superposition,[],[f610,f15]) ).
fof(f623,plain,
! [X0,X1] : and(X1,not(X0)) = and(X1,not(and(X0,X1))),
inference(superposition,[],[f610,f27]) ).
fof(f645,plain,
! [X2,X0,X1] : and(X0,X2) = and(X0,and(or(X0,X1),X2)),
inference(superposition,[],[f4,f25]) ).
fof(f646,plain,
! [X2,X3,X0,X1] : and(or(X0,X1),and(or(X0,X2),X3)) = and(or(X0,and(X1,X2)),X3),
inference(superposition,[],[f4,f8]) ).
fof(f647,plain,
! [X2,X0,X1] : and(X0,X2) = and(X0,and(or(X1,X0),X2)),
inference(superposition,[],[f4,f318]) ).
fof(f651,plain,
! [X2,X0,X1] : and(not(X0),and(not(X1),X2)) = and(not(or(X0,X1)),X2),
inference(superposition,[],[f4,f26]) ).
fof(f663,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X2,and(X0,X1)),
inference(superposition,[],[f2,f4]) ).
fof(f670,plain,
! [X2,X0,X1] : and(and(X0,X1),X2) = and(X0,and(X1,or(X2,not(and(X0,X1))))),
inference(superposition,[],[f610,f4]) ).
fof(f674,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X0,and(X1,or(X2,not(and(X0,X1))))),
inference(forward_demodulation,[],[f670,f4]) ).
fof(f844,plain,
! [X0] : and(cin,and(sF10,X0)) = and(sF11,X0),
inference(superposition,[],[f4,f71]) ).
fof(f853,plain,
a = or(a,sF3),
inference(superposition,[],[f24,f54]) ).
fof(f856,plain,
! [X0,X1] : or(not(X0),X1) = or(not(X0),and(X1,X0)),
inference(superposition,[],[f592,f15]) ).
fof(f859,plain,
! [X0,X1] : or(X1,not(X0)) = or(X1,not(or(X0,X1))),
inference(superposition,[],[f592,f26]) ).
fof(f899,plain,
! [X0,X1] : and(X0,X1) = and(X0,and(X0,X1)),
inference(superposition,[],[f4,f14]) ).
fof(f943,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X0,X1)),
inference(superposition,[],[f3,f13]) ).
fof(f1068,plain,
! [X2,X3,X0,X1] : and(or(X0,X1),and(X0,X3)) = and(or(X0,and(X1,and(X2,X0))),X3),
inference(superposition,[],[f646,f182]) ).
fof(f1091,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(or(X0,X2))) = and(or(X0,X1),ll0),
inference(superposition,[],[f646,f12]) ).
fof(f1107,plain,
! [X2,X0,X1] : ll0 = and(or(X0,and(X1,X2)),not(or(X0,X2))),
inference(forward_demodulation,[],[f1091,f23]) ).
fof(f1127,plain,
! [X3,X0,X1] : and(X0,X3) = and(or(X0,X1),and(X0,X3)),
inference(forward_demodulation,[],[f1068,f247]) ).
fof(f1145,plain,
! [X2,X0,X1] : ll0 = and(not(or(X0,X2)),or(X0,and(X1,X2))),
inference(forward_demodulation,[],[f1107,f2]) ).
fof(f1158,plain,
! [X3,X0,X1] : and(X0,X3) = and(X0,and(X3,or(X0,X1))),
inference(forward_demodulation,[],[f1127,f663]) ).
fof(f1208,plain,
! [X2,X0,X1] : or(and(X0,X1),and(X0,X2)) = and(X0,or(and(X0,X1),X2)),
inference(superposition,[],[f7,f899]) ).
fof(f1218,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(X0,or(and(X0,X1),X2)),
inference(forward_demodulation,[],[f1208,f7]) ).
fof(f1264,plain,
! [X0,X1] : and(X0,ll0) = and(X0,not(or(X0,X1))),
inference(superposition,[],[f645,f12]) ).
fof(f1283,plain,
! [X0,X1] : ll0 = and(X0,not(or(X0,X1))),
inference(forward_demodulation,[],[f1264,f23]) ).
fof(f1346,plain,
! [X2,X0,X1] : or(X1,X0) = or(X1,or(X0,and(X1,X2))),
inference(superposition,[],[f542,f1]) ).
fof(f1352,plain,
! [X0,X1] : or(X0,ll1) = or(X0,not(and(X0,X1))),
inference(superposition,[],[f542,f10]) ).
fof(f1373,plain,
! [X0,X1] : ll1 = or(X0,not(and(X0,X1))),
inference(forward_demodulation,[],[f1352,f21]) ).
fof(f1490,plain,
! [X0] : and(X0,not(t3)) = and(t1,and(b,X0)),
inference(superposition,[],[f663,f457]) ).
fof(f1512,plain,
! [X2,X3,X0,X1] : and(X1,or(X3,and(X2,X0))) = or(and(X1,X3),and(X0,and(X1,X2))),
inference(superposition,[],[f7,f663]) ).
fof(f1516,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X1,and(X0,and(X1,X2))),
inference(superposition,[],[f899,f663]) ).
fof(f1553,plain,
! [X2,X0,X1] : and(X0,X2) = and(X2,and(X0,or(X1,X2))),
inference(backward_demodulation,[],[f341,f1516]) ).
fof(f1626,plain,
! [X0] : or(b,not(X0)) = not(and(sF2,X0)),
inference(superposition,[],[f434,f52]) ).
fof(f1644,plain,
! [X2,X0,X1] : not(or(and(not(X0),X1),X2)) = and(or(X0,not(X1)),not(X2)),
inference(superposition,[],[f26,f434]) ).
fof(f1645,plain,
! [X2,X0,X1] : not(or(X2,and(not(X0),X1))) = and(not(X2),or(X0,not(X1))),
inference(superposition,[],[f26,f434]) ).
fof(f1656,plain,
! [X2,X0,X1] : or(and(not(X0),X2),not(or(X0,X1))) = not(or(X0,and(not(X2),X1))),
inference(backward_demodulation,[],[f214,f1645]) ).
fof(f1697,plain,
! [X0,X1] : or(not(X0),X1) = or(not(X0),and(X0,X1)),
inference(superposition,[],[f593,f15]) ).
fof(f1829,plain,
! [X0] : and(not(X0),a) = not(or(X0,sF0)),
inference(superposition,[],[f435,f48]) ).
fof(f1844,plain,
! [X2,X0,X1] : not(and(X2,or(X0,not(X1)))) = or(not(X2),and(not(X0),X1)),
inference(superposition,[],[f27,f435]) ).
fof(f1866,plain,
! [X0] : and(a,not(X0)) = not(or(X0,sF0)),
inference(forward_demodulation,[],[f1829,f2]) ).
fof(f2107,plain,
! [X0,X1] : ll1 = or(X1,not(and(X0,X1))),
inference(superposition,[],[f1373,f2]) ).
fof(f2127,plain,
ll1 = or(t4,not(not(t5))),
inference(superposition,[],[f1373,f447]) ).
fof(f2168,plain,
ll1 = or(t4,t5),
inference(forward_demodulation,[],[f2127,f15]) ).
fof(f2506,plain,
! [X0,X1] : and(X0,ll0) = and(X0,not(or(X1,X0))),
inference(superposition,[],[f647,f12]) ).
fof(f2545,plain,
! [X0,X1] : ll0 = and(X0,not(or(X1,X0))),
inference(forward_demodulation,[],[f2506,f23]) ).
fof(f2772,plain,
! [X2,X0,X1] : and(or(X0,X2),or(X0,X1)) = or(X0,and(X2,or(X0,X1))),
inference(superposition,[],[f8,f943]) ).
fof(f2788,plain,
! [X2,X0,X1] : or(X0,and(X2,X1)) = or(X0,and(X2,or(X0,X1))),
inference(forward_demodulation,[],[f2772,f8]) ).
fof(f2824,plain,
not(and(a,b)) = or(sF0,sF2),
inference(superposition,[],[f275,f52]) ).
fof(f2861,plain,
not(not(t1)) = or(sF0,sF2),
inference(forward_demodulation,[],[f2824,f421]) ).
fof(f2875,plain,
t1 = or(sF0,sF2),
inference(forward_demodulation,[],[f2861,f15]) ).
fof(f2909,plain,
ll1 = or(cin,not(not(t5))),
inference(superposition,[],[f2107,f447]) ).
fof(f2933,plain,
! [X2,X0,X1] : or(and(not(X0),X1),not(ll1)) = not(or(X0,and(not(X1),not(and(X2,X0))))),
inference(superposition,[],[f1656,f2107]) ).
fof(f2946,plain,
! [X2,X0,X1] : or(and(not(X0),X1),not(ll1)) = not(or(X0,not(or(X1,and(X2,X0))))),
inference(forward_demodulation,[],[f2933,f26]) ).
fof(f2961,plain,
ll1 = or(cin,t5),
inference(forward_demodulation,[],[f2909,f15]) ).
fof(f2978,plain,
! [X2,X0,X1] : or(and(not(X0),X1),not(ll1)) = and(not(X0),or(X1,and(X2,X0))),
inference(forward_demodulation,[],[f2946,f435]) ).
fof(f2984,plain,
ll1 = or(t5,cin),
inference(forward_demodulation,[],[f2961,f1]) ).
fof(f2994,plain,
! [X2,X0,X1] : or(not(ll1),and(not(X0),X1)) = and(not(X0),or(X1,and(X2,X0))),
inference(forward_demodulation,[],[f2978,f1]) ).
fof(f2998,plain,
! [X2,X0,X1] : or(ll0,and(not(X0),X1)) = and(not(X0),or(X1,and(X2,X0))),
inference(forward_demodulation,[],[f2994,f19]) ).
fof(f2999,plain,
! [X2,X0,X1] : and(not(X0),X1) = and(not(X0),or(X1,and(X2,X0))),
inference(forward_demodulation,[],[f2998,f358]) ).
fof(f3476,plain,
t1 = or(sF0,t1),
inference(superposition,[],[f943,f2875]) ).
fof(f3483,plain,
t1 = or(t1,sF0),
inference(forward_demodulation,[],[f3476,f1]) ).
fof(f3782,plain,
! [X2,X0,X1] : not(or(not(X0),X1)) = and(X0,not(or(and(X2,not(X0)),X1))),
inference(superposition,[],[f436,f543]) ).
fof(f3785,plain,
! [X2,X0,X1] : and(X0,not(X1)) = and(X0,not(or(and(X2,not(X0)),X1))),
inference(forward_demodulation,[],[f3782,f436]) ).
fof(f4046,plain,
! [X0] : and(a,and(b,X0)) = and(X0,not(t1)),
inference(superposition,[],[f663,f421]) ).
fof(f4048,plain,
not(t1) = and(a,not(t1)),
inference(superposition,[],[f899,f421]) ).
fof(f4054,plain,
sF13 = and(not(cin),not(t1)),
inference(backward_demodulation,[],[f156,f4046]) ).
fof(f4064,plain,
sF13 = not(or(cin,t1)),
inference(forward_demodulation,[],[f4054,f26]) ).
fof(f4067,plain,
sF13 = not(or(t1,cin)),
inference(forward_demodulation,[],[f4064,f1]) ).
fof(f4074,plain,
not(sF13) = or(t1,cin),
inference(superposition,[],[f15,f4067]) ).
fof(f4145,plain,
! [X0] : and(sF13,X0) = and(sF13,or(or(t1,cin),X0)),
inference(superposition,[],[f609,f4074]) ).
fof(f4148,plain,
! [X0] : and(sF13,X0) = and(sF13,or(t1,or(cin,X0))),
inference(forward_demodulation,[],[f4145,f3]) ).
fof(f4167,plain,
! [X2,X0,X1] : and(or(X0,X2),not(or(X0,X1))) = and(or(X0,X2),not(or(X0,and(X1,X2)))),
inference(superposition,[],[f623,f8]) ).
fof(f4182,plain,
and(a,not(t1)) = and(a,not(not(t2))),
inference(superposition,[],[f623,f467]) ).
fof(f4184,plain,
and(b,not(a)) = and(b,not(not(t1))),
inference(superposition,[],[f623,f421]) ).
fof(f4186,plain,
and(cin,not(t4)) = and(cin,not(not(t5))),
inference(superposition,[],[f623,f447]) ).
fof(f4188,plain,
and(sF0,not(b)) = and(sF0,not(sF1)),
inference(superposition,[],[f623,f131]) ).
fof(f4201,plain,
! [X2,X0,X1] : or(and(X0,X2),and(X0,not(X1))) = and(X0,or(X2,not(and(X1,X0)))),
inference(superposition,[],[f7,f623]) ).
fof(f4235,plain,
! [X2,X0,X1] : and(X0,or(X2,not(X1))) = and(X0,or(X2,not(and(X1,X0)))),
inference(forward_demodulation,[],[f4201,f7]) ).
fof(f4245,plain,
and(sF0,not(b)) = not(or(a,sF1)),
inference(forward_demodulation,[],[f4188,f252]) ).
fof(f4247,plain,
and(cin,t5) = and(cin,not(t4)),
inference(forward_demodulation,[],[f4186,f15]) ).
fof(f4249,plain,
and(b,t1) = and(b,not(a)),
inference(forward_demodulation,[],[f4184,f15]) ).
fof(f4251,plain,
and(a,not(t1)) = and(a,t2),
inference(forward_demodulation,[],[f4182,f15]) ).
fof(f4275,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X0,and(X1,or(X2,not(X0)))),
inference(backward_demodulation,[],[f674,f4235]) ).
fof(f4280,plain,
not(or(a,b)) = not(or(a,sF1)),
inference(forward_demodulation,[],[f4245,f252]) ).
fof(f4282,plain,
and(t5,cin) = and(cin,not(t4)),
inference(forward_demodulation,[],[f4247,f2]) ).
fof(f4284,plain,
and(b,t1) = and(b,sF0),
inference(forward_demodulation,[],[f4249,f48]) ).
fof(f4286,plain,
and(a,not(t1)) = and(t2,a),
inference(forward_demodulation,[],[f4251,f2]) ).
fof(f4306,plain,
not(sF10) = not(or(a,sF1)),
inference(forward_demodulation,[],[f4280,f69]) ).
fof(f4307,plain,
not(t7) = and(cin,not(t4)),
inference(forward_demodulation,[],[f4282,f437]) ).
fof(f4308,plain,
and(b,t1) = sF1,
inference(forward_demodulation,[],[f4284,f131]) ).
fof(f4309,plain,
not(t1) = and(t2,a),
inference(forward_demodulation,[],[f4286,f4048]) ).
fof(f4321,plain,
sF1 = and(t1,b),
inference(forward_demodulation,[],[f4308,f2]) ).
fof(f4328,plain,
sF1 = not(t3),
inference(backward_demodulation,[],[f457,f4321]) ).
fof(f4336,plain,
! [X0] : and(t1,or(b,X0)) = or(sF1,and(t1,X0)),
inference(backward_demodulation,[],[f465,f4328]) ).
fof(f4342,plain,
! [X0] : and(t1,and(b,X0)) = and(X0,sF1),
inference(backward_demodulation,[],[f1490,f4328]) ).
fof(f4355,plain,
t3 = not(sF1),
inference(superposition,[],[f15,f4328]) ).
fof(f4358,plain,
! [X0] : not(and(t3,X0)) = or(sF1,not(X0)),
inference(superposition,[],[f27,f4328]) ).
fof(f4364,plain,
! [X0] : or(not(X0),t3) = not(and(X0,sF1)),
inference(superposition,[],[f433,f4328]) ).
fof(f4366,plain,
! [X0] : and(not(X0),t3) = not(or(X0,sF1)),
inference(superposition,[],[f435,f4328]) ).
fof(f4367,plain,
! [X0] : and(t3,not(X0)) = not(or(sF1,X0)),
inference(superposition,[],[f436,f4328]) ).
fof(f4374,plain,
! [X0] : and(t3,not(X0)) = not(or(X0,sF1)),
inference(forward_demodulation,[],[f4366,f2]) ).
fof(f4375,plain,
! [X0] : or(t3,not(X0)) = not(and(X0,sF1)),
inference(forward_demodulation,[],[f4364,f1]) ).
fof(f4384,plain,
not(sF10) = and(t3,not(a)),
inference(backward_demodulation,[],[f4306,f4374]) ).
fof(f4392,plain,
not(sF10) = and(t3,sF0),
inference(forward_demodulation,[],[f4384,f48]) ).
fof(f4440,plain,
! [X0] : not(or(X0,sF10)) = and(not(X0),and(t3,sF0)),
inference(superposition,[],[f26,f4392]) ).
fof(f4442,plain,
! [X0] : not(and(X0,sF10)) = or(not(X0),and(t3,sF0)),
inference(superposition,[],[f27,f4392]) ).
fof(f4449,plain,
! [X0] : and(not(X0),sF10) = not(or(X0,and(t3,sF0))),
inference(superposition,[],[f435,f4392]) ).
fof(f4463,plain,
! [X0] : not(or(X0,sF10)) = and(t3,and(sF0,not(X0))),
inference(forward_demodulation,[],[f4440,f663]) ).
fof(f4471,plain,
! [X0] : not(or(X0,sF10)) = and(t3,not(or(a,X0))),
inference(forward_demodulation,[],[f4463,f252]) ).
fof(f4677,plain,
not(not(sF5)) = and(t3,not(sF3)),
inference(superposition,[],[f4367,f477]) ).
fof(f4704,plain,
! [X0,X1] : not(and(X1,or(sF1,X0))) = or(not(X1),and(t3,not(X0))),
inference(superposition,[],[f27,f4367]) ).
fof(f4747,plain,
sF5 = and(t3,not(sF3)),
inference(forward_demodulation,[],[f4677,f15]) ).
fof(f5191,plain,
and(t1,or(b,a)) = or(sF1,not(t2)),
inference(superposition,[],[f4336,f467]) ).
fof(f5232,plain,
and(t1,or(b,a)) = not(and(t3,t2)),
inference(forward_demodulation,[],[f5191,f4358]) ).
fof(f5267,plain,
not(and(t2,t3)) = and(t1,or(b,a)),
inference(forward_demodulation,[],[f5232,f2]) ).
fof(f5288,plain,
not(and(t2,t3)) = and(t1,or(a,b)),
inference(forward_demodulation,[],[f5267,f1]) ).
fof(f5297,plain,
not(and(t2,t3)) = and(t1,sF10),
inference(forward_demodulation,[],[f5288,f69]) ).
fof(f5301,plain,
not(not(t4)) = and(t1,sF10),
inference(forward_demodulation,[],[f5297,f423]) ).
fof(f5302,plain,
t4 = and(t1,sF10),
inference(forward_demodulation,[],[f5301,f15]) ).
fof(f5316,plain,
t4 = and(t1,t4),
inference(superposition,[],[f899,f5302]) ).
fof(f5317,plain,
ll1 = or(t1,not(t4)),
inference(superposition,[],[f1373,f5302]) ).
fof(f5320,plain,
t4 = and(t4,t1),
inference(forward_demodulation,[],[f5316,f2]) ).
fof(f5631,plain,
! [X2,X0,X1] : or(and(X0,X2),and(X0,X1)) = and(X0,or(X2,and(X1,X0))),
inference(superposition,[],[f7,f343]) ).
fof(f5676,plain,
! [X2,X0,X1] : and(X0,or(X2,X1)) = and(X0,or(X2,and(X1,X0))),
inference(forward_demodulation,[],[f5631,f7]) ).
fof(f5897,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(not(X0),or(and(not(X1),X1),ll0)),and(X0,not(or(and(not(X1),X1),ll0)))),
inference(superposition,[],[f45,f12]) ).
fof(f5997,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(not(or(and(not(not(X0)),X0),not(X0))),X1),and(or(and(not(not(X0)),X0),not(X0)),not(X1))),
inference(superposition,[],[f45,f14]) ).
fof(f6150,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(or(and(not(not(X0)),X0),not(X0)),not(X1)),and(not(or(and(not(not(X0)),X0),not(X0))),X1)),
inference(forward_demodulation,[],[f5997,f1]) ).
fof(f6250,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,not(or(and(not(X1),X1),ll0))),and(not(X0),or(and(not(X1),X1),ll0))),
inference(forward_demodulation,[],[f5897,f1]) ).
fof(f6350,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(or(and(not(not(X0)),X0),not(X0)),not(X1)),and(and(not(and(not(not(X0)),X0)),X0),X1)),
inference(forward_demodulation,[],[f6150,f435]) ).
fof(f6450,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,not(and(not(X1),X1))),and(not(X0),and(not(X1),X1))),
inference(forward_demodulation,[],[f6250,f5]) ).
fof(f6550,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(and(not(and(not(not(X0)),X0)),X0),X1),and(or(and(not(not(X0)),X0),not(X0)),not(X1))),
inference(forward_demodulation,[],[f6350,f1]) ).
fof(f6647,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,not(and(not(X1),X1))),and(not(or(X0,X1)),X1)),
inference(forward_demodulation,[],[f6450,f651]) ).
fof(f6733,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(and(not(and(not(not(X0)),X0)),X0),X1),not(or(and(not(and(not(not(X0)),X0)),X0),X1))),
inference(forward_demodulation,[],[f6550,f1644]) ).
fof(f6819,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(not(or(X0,X1)),X1),and(X0,not(and(not(X1),X1)))),
inference(forward_demodulation,[],[f6647,f1]) ).
fof(f6877,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(and(X0,not(and(not(not(X0)),X0))),X1),not(or(and(X0,not(and(not(not(X0)),X0))),X1))),
inference(forward_demodulation,[],[f6733,f2]) ).
fof(f6944,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(not(or(X0,X1)),X1),and(X0,or(X1,not(X1)))),
inference(forward_demodulation,[],[f6819,f434]) ).
fof(f6989,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(and(X0,not(not(not(X0)))),X1),not(or(and(X0,not(not(not(X0)))),X1))),
inference(forward_demodulation,[],[f6877,f623]) ).
fof(f7055,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,or(X1,not(X1))),and(not(or(X0,X1)),X1)),
inference(forward_demodulation,[],[f6944,f1]) ).
fof(f7093,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(and(X0,not(X0)),X1),not(or(and(X0,not(X0)),X1))),
inference(forward_demodulation,[],[f6989,f15]) ).
fof(f7156,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,or(X1,not(X1))),and(X1,not(or(X0,X1)))),
inference(forward_demodulation,[],[f7055,f2]) ).
fof(f7188,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(ll0,X1),not(or(ll0,X1))),
inference(forward_demodulation,[],[f7093,f12]) ).
fof(f7246,plain,
! [X0,X1] : or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))) = or(and(X0,or(X1,not(X1))),ll0),
inference(forward_demodulation,[],[f7156,f2545]) ).
fof(f7274,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(and(ll0,X1),not(X1)),
inference(forward_demodulation,[],[f7188,f358]) ).
fof(f7329,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(or(and(not(X0),X1),and(X0,not(X1)))),X1),and(or(and(not(X0),X1),and(X0,not(X1))),not(X1))),
inference(forward_demodulation,[],[f7246,f5]) ).
fof(f7357,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(not(X1),and(ll0,X1)),
inference(forward_demodulation,[],[f7274,f1]) ).
fof(f7399,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),or(and(not(X0),X1),and(X0,not(X1)))),and(X1,not(or(and(not(X0),X1),and(X0,not(X1)))))),
inference(forward_demodulation,[],[f7329,f44]) ).
fof(f7427,plain,
! [X0,X1] : or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))) = or(not(X1),ll0),
inference(forward_demodulation,[],[f7357,f856]) ).
fof(f7468,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,not(or(and(not(X0),X1),and(X0,not(X1))))),and(not(X1),or(and(not(X0),X1),and(X0,not(X1))))),
inference(forward_demodulation,[],[f7399,f1]) ).
fof(f7494,plain,
! [X0,X1] : not(X1) = or(and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1)))),and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1)))))),
inference(forward_demodulation,[],[f7427,f5]) ).
fof(f7534,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,not(or(and(not(X0),X1),and(X0,not(X1))))),and(not(X1),or(and(not(X0),X1),X0))),
inference(forward_demodulation,[],[f7468,f5676]) ).
fof(f7557,plain,
! [X0,X1] : not(X1) = or(and(not(X0),not(or(and(not(X0),X1),and(X0,not(X1))))),and(not(not(X0)),or(and(not(X0),X1),and(X0,not(X1))))),
inference(forward_demodulation,[],[f7494,f1]) ).
fof(f7592,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),or(and(not(X0),X1),X0)),and(X1,not(or(and(not(X0),X1),and(X0,not(X1)))))),
inference(forward_demodulation,[],[f7534,f1]) ).
fof(f7609,plain,
! [X0,X1] : not(X1) = or(and(not(X0),not(or(and(X0,not(X1)),and(not(X0),X1)))),and(not(not(X0)),or(and(X0,not(X1)),and(not(X0),X1)))),
inference(forward_demodulation,[],[f7557,f1]) ).
fof(f7639,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),or(and(not(X0),X1),X0)),and(X1,not(or(and(X0,not(X1)),and(not(X0),X1))))),
inference(forward_demodulation,[],[f7592,f1]) ).
fof(f7656,plain,
! [X0,X1] : not(X1) = or(and(not(X0),not(or(and(X0,not(X1)),and(not(X0),X1)))),and(X0,or(and(X0,not(X1)),and(not(X0),X1)))),
inference(forward_demodulation,[],[f7609,f15]) ).
fof(f7756,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),or(and(not(X0),X1),X0)),and(X1,not(and(not(X0),X1)))),
inference(forward_demodulation,[],[f7639,f3785]) ).
fof(f7773,plain,
! [X0,X1] : not(X1) = or(and(X0,or(and(X0,not(X1)),and(not(X0),X1))),and(not(X0),not(or(and(X0,not(X1)),and(not(X0),X1))))),
inference(forward_demodulation,[],[f7656,f1]) ).
fof(f7858,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,not(and(not(X0),X1))),and(not(X1),or(and(not(X0),X1),X0))),
inference(forward_demodulation,[],[f7756,f1]) ).
fof(f7873,plain,
! [X0,X1] : not(X1) = or(and(X0,or(and(X0,not(X1)),and(not(X0),X1))),not(or(X0,or(and(X0,not(X1)),and(not(X0),X1))))),
inference(forward_demodulation,[],[f7773,f26]) ).
fof(f7914,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,not(and(not(X0),X1))),and(not(X1),or(X0,and(not(X0),X1)))),
inference(forward_demodulation,[],[f7858,f1]) ).
fof(f7927,plain,
! [X0,X1] : not(X1) = or(and(X0,or(and(X0,not(X1)),and(not(X0),X1))),not(or(X0,and(not(X0),X1)))),
inference(forward_demodulation,[],[f7873,f542]) ).
fof(f7950,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,not(and(not(X0),X1))),and(not(X1),X0)),
inference(forward_demodulation,[],[f7914,f2999]) ).
fof(f7961,plain,
! [X0,X1] : not(X1) = or(not(or(X0,and(not(X0),X1))),and(X0,or(and(X0,not(X1)),and(not(X0),X1)))),
inference(forward_demodulation,[],[f7927,f1]) ).
fof(f7981,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),X0),and(X1,not(and(not(X0),X1)))),
inference(forward_demodulation,[],[f7950,f1]) ).
fof(f7990,plain,
! [X0,X1] : not(X1) = or(not(or(X0,and(not(X0),X1))),and(X0,or(not(X1),and(not(X0),X1)))),
inference(forward_demodulation,[],[f7961,f1218]) ).
fof(f8004,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),X0),and(X1,not(not(X0)))),
inference(forward_demodulation,[],[f7981,f623]) ).
fof(f8012,plain,
! [X0,X1] : not(X1) = or(not(or(X0,and(not(X0),X1))),and(X0,or(not(X1),not(X0)))),
inference(forward_demodulation,[],[f7990,f856]) ).
fof(f8026,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(not(X1),X0),and(X1,X0)),
inference(forward_demodulation,[],[f8004,f15]) ).
fof(f8033,plain,
! [X0,X1] : not(X1) = or(not(or(X0,and(not(X0),X1))),and(X0,not(X1))),
inference(forward_demodulation,[],[f8012,f610]) ).
fof(f8045,plain,
! [X0,X1] : and(X0,or(X1,not(X1))) = or(and(X1,X0),and(not(X1),X0)),
inference(forward_demodulation,[],[f8026,f1]) ).
fof(f8052,plain,
! [X0,X1] : not(X1) = or(and(X0,not(X1)),not(or(X0,and(not(X0),X1)))),
inference(forward_demodulation,[],[f8033,f1]) ).
fof(f8063,plain,
! [X0,X1] : and(X0,ll1) = or(and(X1,X0),and(not(X1),X0)),
inference(forward_demodulation,[],[f8045,f10]) ).
fof(f8067,plain,
! [X0,X1] : not(X1) = or(and(X0,not(X1)),not(or(X0,X1))),
inference(forward_demodulation,[],[f8052,f593]) ).
fof(f8078,plain,
! [X0,X1] : or(and(X1,X0),and(not(X1),X0)) = X0,
inference(forward_demodulation,[],[f8063,f6]) ).
fof(f8081,plain,
! [X0,X1] : not(X1) = or(not(or(X0,X1)),and(X0,not(X1))),
inference(forward_demodulation,[],[f8067,f1]) ).
fof(f8148,plain,
! [X0,X1] : not(X0) = or(not(or(X0,X1)),and(X1,not(X0))),
inference(superposition,[],[f8081,f1]) ).
fof(f8153,plain,
! [X0,X1] : not(and(X1,X0)) = or(not(X0),and(X0,not(and(X1,X0)))),
inference(superposition,[],[f8081,f182]) ).
fof(f8154,plain,
! [X0,X1] : not(and(X1,not(X0))) = or(not(or(X0,X1)),and(X0,not(and(X1,not(X0))))),
inference(superposition,[],[f8081,f592]) ).
fof(f8172,plain,
not(b) = or(not(sF10),and(a,not(b))),
inference(superposition,[],[f8081,f69]) ).
fof(f8238,plain,
! [X0,X1] : not(not(X0)) = and(or(X1,X0),not(and(X1,not(X0)))),
inference(superposition,[],[f436,f8081]) ).
fof(f8266,plain,
! [X0,X1] : not(not(X0)) = and(or(X1,X0),or(not(X1),X0)),
inference(forward_demodulation,[],[f8238,f433]) ).
fof(f8320,plain,
sF2 = or(not(sF10),and(a,sF2)),
inference(forward_demodulation,[],[f8172,f52]) ).
fof(f8335,plain,
! [X0,X1] : or(not(X1),X0) = or(not(or(X0,X1)),and(X0,or(not(X1),X0))),
inference(forward_demodulation,[],[f8154,f433]) ).
fof(f8336,plain,
! [X0,X1] : not(and(X1,X0)) = or(not(X0),not(and(X1,X0))),
inference(forward_demodulation,[],[f8153,f1697]) ).
fof(f8349,plain,
! [X0,X1] : and(or(X1,X0),or(not(X1),X0)) = X0,
inference(forward_demodulation,[],[f8266,f15]) ).
fof(f8393,plain,
sF2 = or(not(sF10),sF3),
inference(forward_demodulation,[],[f8320,f54]) ).
fof(f8406,plain,
! [X0,X1] : or(not(X1),X0) = or(not(or(X0,X1)),X0),
inference(forward_demodulation,[],[f8335,f318]) ).
fof(f8407,plain,
! [X0,X1] : not(and(X1,X0)) = not(and(X0,and(X1,X0))),
inference(forward_demodulation,[],[f8336,f27]) ).
fof(f8445,plain,
sF2 = or(sF3,not(sF10)),
inference(forward_demodulation,[],[f8393,f1]) ).
fof(f8457,plain,
! [X0,X1] : or(not(X1),X0) = or(X0,not(or(X0,X1))),
inference(forward_demodulation,[],[f8406,f1]) ).
fof(f8458,plain,
! [X0,X1] : not(and(X0,X1)) = not(and(X1,X0)),
inference(forward_demodulation,[],[f8407,f343]) ).
fof(f8481,plain,
sF2 = or(sF3,and(t3,sF0)),
inference(forward_demodulation,[],[f8445,f4392]) ).
fof(f8586,plain,
! [X0,X1] : and(X1,X0) = and(X0,or(not(X0),and(X1,X0))),
inference(superposition,[],[f8349,f182]) ).
fof(f8656,plain,
! [X0,X1] : and(X1,not(X0)) = and(or(or(X1,X0),and(X1,not(X0))),not(X0)),
inference(superposition,[],[f8349,f8081]) ).
fof(f8722,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(or(X1,X0),and(X1,not(X0)))),
inference(forward_demodulation,[],[f8656,f2]) ).
fof(f8780,plain,
! [X0,X1] : and(X1,X0) = and(X0,or(not(X0),X1)),
inference(forward_demodulation,[],[f8586,f5676]) ).
fof(f8805,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(or(X1,X0),X1)),
inference(forward_demodulation,[],[f8722,f5676]) ).
fof(f8854,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(X1,or(X0,X1))),
inference(forward_demodulation,[],[f8805,f3]) ).
fof(f8874,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(X1,X0)),
inference(forward_demodulation,[],[f8854,f245]) ).
fof(f9256,plain,
! [X0,X1] : or(X1,not(X0)) = or(and(X0,X1),and(not(X0),or(X1,not(X0)))),
inference(superposition,[],[f8078,f610]) ).
fof(f9276,plain,
a = or(not(t2),and(not(t1),a)),
inference(superposition,[],[f8078,f467]) ).
fof(f9350,plain,
! [X0,X1] : not(and(not(X1),X0)) = or(not(X0),and(and(X1,X0),not(and(not(X1),X0)))),
inference(superposition,[],[f8081,f8078]) ).
fof(f9353,plain,
! [X0,X1] : not(and(not(X1),X0)) = or(not(X0),and(X1,and(X0,not(and(not(X1),X0))))),
inference(forward_demodulation,[],[f9350,f4]) ).
fof(f9416,plain,
a = or(not(t2),and(a,not(t1))),
inference(forward_demodulation,[],[f9276,f2]) ).
fof(f9431,plain,
! [X0,X1] : or(X1,not(X0)) = or(and(X0,X1),not(or(X0,and(not(X1),X0)))),
inference(forward_demodulation,[],[f9256,f1645]) ).
fof(f9440,plain,
! [X0,X1] : not(and(not(X1),X0)) = or(not(X0),and(X1,and(X0,not(not(X1))))),
inference(forward_demodulation,[],[f9353,f623]) ).
fof(f9482,plain,
a = or(not(t2),not(t1)),
inference(forward_demodulation,[],[f9416,f4048]) ).
fof(f9495,plain,
! [X0,X1] : or(X1,not(X0)) = or(and(X0,X1),not(X0)),
inference(forward_demodulation,[],[f9431,f182]) ).
fof(f9501,plain,
! [X0,X1] : not(and(not(X1),X0)) = or(not(X0),and(X1,and(X0,X1))),
inference(forward_demodulation,[],[f9440,f15]) ).
fof(f9524,plain,
a = not(and(t2,t1)),
inference(forward_demodulation,[],[f9482,f27]) ).
fof(f9533,plain,
! [X0,X1] : or(X1,not(X0)) = or(not(X0),and(X0,X1)),
inference(forward_demodulation,[],[f9495,f1]) ).
fof(f9537,plain,
! [X0,X1] : or(not(X0),and(X1,X0)) = not(and(not(X1),X0)),
inference(forward_demodulation,[],[f9501,f343]) ).
fof(f9554,plain,
! [X0,X1] : or(X1,not(X0)) = or(not(X0),and(X1,X0)),
inference(forward_demodulation,[],[f9537,f434]) ).
fof(f9825,plain,
or(sF2,a) = not(and(b,and(t2,t1))),
inference(superposition,[],[f276,f9524]) ).
fof(f9847,plain,
or(sF2,a) = not(and(t1,and(b,t2))),
inference(forward_demodulation,[],[f9825,f663]) ).
fof(f9867,plain,
or(sF2,a) = not(and(t2,sF1)),
inference(forward_demodulation,[],[f9847,f4342]) ).
fof(f9888,plain,
or(sF2,a) = or(t3,not(t2)),
inference(forward_demodulation,[],[f9867,f4375]) ).
fof(f9898,plain,
or(a,sF2) = or(t3,not(t2)),
inference(forward_demodulation,[],[f9888,f1]) ).
fof(f10528,plain,
! [X2,X0,X1] : and(X0,or(X2,X1)) = or(and(X0,X1),and(not(X1),and(X0,or(X2,X1)))),
inference(superposition,[],[f8078,f1553]) ).
fof(f10529,plain,
! [X2,X3,X0,X1] : and(or(X0,X1),or(X0,X2)) = and(or(X0,and(X2,X1)),or(X3,or(X0,X2))),
inference(superposition,[],[f646,f1553]) ).
fof(f10558,plain,
! [X2,X3,X0,X1] : or(X0,and(X1,X2)) = and(or(X0,and(X2,X1)),or(X3,or(X0,X2))),
inference(forward_demodulation,[],[f10529,f8]) ).
fof(f10559,plain,
! [X2,X0,X1] : and(X0,or(X2,X1)) = and(X0,or(X1,and(or(X2,X1),not(X1)))),
inference(forward_demodulation,[],[f10528,f1512]) ).
fof(f10644,plain,
! [X2,X0,X1] : and(X0,or(X2,X1)) = and(X0,or(X1,or(X2,X1))),
inference(forward_demodulation,[],[f10559,f592]) ).
fof(f10687,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(X0,or(X2,X1)),
inference(forward_demodulation,[],[f10644,f245]) ).
fof(f10747,plain,
! [X2,X3,X0,X1] : and(X3,or(X0,or(X1,X2))) = and(X3,or(X2,or(X0,X1))),
inference(superposition,[],[f10687,f3]) ).
fof(f10829,plain,
! [X2,X0,X1] : and(X0,or(X1,X2)) = and(or(X2,X1),X0),
inference(superposition,[],[f2,f10687]) ).
fof(f10861,plain,
! [X2,X0,X1] : or(X0,or(X2,X1)) = or(X0,and(not(X0),or(X1,X2))),
inference(superposition,[],[f593,f10687]) ).
fof(f10875,plain,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(X0,or(X2,X1)),
inference(forward_demodulation,[],[f10861,f593]) ).
fof(f11080,plain,
! [X0] : and(or(t1,X0),t1) = or(t1,and(X0,sF0)),
inference(superposition,[],[f8,f3483]) ).
fof(f11103,plain,
! [X0] : and(t1,or(X0,t1)) = or(t1,and(X0,sF0)),
inference(forward_demodulation,[],[f11080,f10829]) ).
fof(f11110,plain,
! [X0] : t1 = or(t1,and(X0,sF0)),
inference(forward_demodulation,[],[f11103,f318]) ).
fof(f11130,plain,
not(or(a,b)) = and(sF0,sF2),
inference(superposition,[],[f252,f52]) ).
fof(f11204,plain,
not(sF10) = and(sF0,sF2),
inference(forward_demodulation,[],[f11130,f69]) ).
fof(f11237,plain,
and(t3,sF0) = and(sF0,sF2),
inference(forward_demodulation,[],[f11204,f4392]) ).
fof(f11367,plain,
not(sF3) = or(not(sF2),and(and(t3,sF0),not(sF3))),
inference(superposition,[],[f8148,f8481]) ).
fof(f11373,plain,
not(t1) = or(sF13,and(cin,not(t1))),
inference(superposition,[],[f8148,f4067]) ).
fof(f11478,plain,
not(sF3) = or(not(sF2),and(t3,and(sF0,not(sF3)))),
inference(forward_demodulation,[],[f11367,f4]) ).
fof(f11569,plain,
not(sF3) = or(not(sF2),and(t3,not(or(a,sF3)))),
inference(forward_demodulation,[],[f11478,f252]) ).
fof(f11649,plain,
not(sF3) = not(and(sF2,or(sF1,or(a,sF3)))),
inference(forward_demodulation,[],[f11569,f4704]) ).
fof(f11720,plain,
not(sF3) = or(b,not(or(sF1,or(a,sF3)))),
inference(forward_demodulation,[],[f11649,f1626]) ).
fof(f11758,plain,
not(sF3) = or(b,and(t3,not(or(a,sF3)))),
inference(forward_demodulation,[],[f11720,f4367]) ).
fof(f11784,plain,
not(sF3) = or(b,not(or(sF3,sF10))),
inference(forward_demodulation,[],[f11758,f4471]) ).
fof(f11849,plain,
and(sF2,not(sF0)) = and(sF2,not(and(t3,sF0))),
inference(superposition,[],[f623,f11237]) ).
fof(f11860,plain,
and(sF2,not(sF0)) = not(or(b,and(t3,sF0))),
inference(forward_demodulation,[],[f11849,f257]) ).
fof(f11871,plain,
and(sF2,not(sF0)) = and(not(b),sF10),
inference(forward_demodulation,[],[f11860,f4449]) ).
fof(f11877,plain,
and(sF2,not(sF0)) = and(sF10,not(b)),
inference(forward_demodulation,[],[f11871,f2]) ).
fof(f11881,plain,
and(sF2,not(sF0)) = and(sF10,sF2),
inference(forward_demodulation,[],[f11877,f52]) ).
fof(f11884,plain,
and(sF2,not(sF0)) = and(sF2,sF10),
inference(forward_demodulation,[],[f11881,f2]) ).
fof(f11885,plain,
not(or(b,sF0)) = and(sF2,sF10),
inference(forward_demodulation,[],[f11884,f257]) ).
fof(f11886,plain,
and(a,not(b)) = and(sF2,sF10),
inference(forward_demodulation,[],[f11885,f1866]) ).
fof(f11887,plain,
and(a,sF2) = and(sF2,sF10),
inference(forward_demodulation,[],[f11886,f52]) ).
fof(f11888,plain,
sF3 = and(sF2,sF10),
inference(forward_demodulation,[],[f11887,f54]) ).
fof(f11948,plain,
sF10 = or(sF10,sF3),
inference(superposition,[],[f182,f11888]) ).
fof(f11959,plain,
ll1 = or(sF10,not(sF3)),
inference(superposition,[],[f2107,f11888]) ).
fof(f11968,plain,
sF10 = or(sF3,sF10),
inference(forward_demodulation,[],[f11948,f1]) ).
fof(f11975,plain,
not(sF3) = or(b,not(sF10)),
inference(backward_demodulation,[],[f11784,f11968]) ).
fof(f11980,plain,
not(sF3) = or(b,and(t3,sF0)),
inference(forward_demodulation,[],[f11975,f4392]) ).
fof(f12278,plain,
! [X2,X0,X1] : not(and(not(X0),and(X1,X2))) = or(X0,not(and(X1,or(X2,not(not(X0)))))),
inference(superposition,[],[f434,f4275]) ).
fof(f12293,plain,
! [X2,X0,X1] : not(and(not(X0),and(X1,X2))) = or(X0,or(not(X1),and(not(X2),not(X0)))),
inference(forward_demodulation,[],[f12278,f1844]) ).
fof(f12355,plain,
! [X2,X0,X1] : not(and(not(X0),and(X1,X2))) = or(X0,or(not(X1),not(or(X2,X0)))),
inference(forward_demodulation,[],[f12293,f26]) ).
fof(f12387,plain,
! [X2,X0,X1] : not(and(not(X0),and(X1,X2))) = or(X0,not(and(X1,or(X2,X0)))),
inference(forward_demodulation,[],[f12355,f27]) ).
fof(f12406,plain,
! [X2,X0,X1] : or(X0,not(and(X1,X2))) = or(X0,not(and(X1,or(X2,X0)))),
inference(forward_demodulation,[],[f12387,f434]) ).
fof(f14333,plain,
! [X2,X0,X1] : or(not(and(X0,or(X2,X1))),X1) = or(not(and(X0,or(X2,X1))),and(X0,X1)),
inference(superposition,[],[f856,f1553]) ).
fof(f14349,plain,
or(not(b),a) = or(not(b),not(t1)),
inference(superposition,[],[f856,f421]) ).
fof(f14368,plain,
or(not(sF2),sF0) = or(not(sF2),and(t3,sF0)),
inference(superposition,[],[f856,f11237]) ).
fof(f14373,plain,
or(not(sF10),t1) = or(not(sF10),t4),
inference(superposition,[],[f856,f5302]) ).
fof(f14400,plain,
! [X0,X1] : and(X1,X0) = and(or(not(X0),X1),or(not(not(X0)),and(X1,X0))),
inference(superposition,[],[f8349,f856]) ).
fof(f14401,plain,
! [X0,X1] : and(X1,X0) = and(or(not(X0),X1),or(X0,and(X1,X0))),
inference(forward_demodulation,[],[f14400,f15]) ).
fof(f14422,plain,
or(not(sF10),t1) = or(t4,not(sF10)),
inference(forward_demodulation,[],[f14373,f1]) ).
fof(f14427,plain,
not(and(sF2,sF10)) = or(not(sF2),sF0),
inference(forward_demodulation,[],[f14368,f4442]) ).
fof(f14446,plain,
not(and(b,t1)) = or(not(b),a),
inference(forward_demodulation,[],[f14349,f27]) ).
fof(f14462,plain,
! [X2,X0,X1] : or(not(and(X0,or(X2,X1))),X1) = or(and(X0,X1),not(and(X0,or(X2,X1)))),
inference(forward_demodulation,[],[f14333,f1]) ).
fof(f14486,plain,
! [X0,X1] : and(X1,X0) = and(or(not(X0),X1),X0),
inference(forward_demodulation,[],[f14401,f182]) ).
fof(f14502,plain,
or(and(t3,sF0),t1) = or(t4,and(t3,sF0)),
inference(forward_demodulation,[],[f14422,f4392]) ).
fof(f14507,plain,
not(and(sF2,sF10)) = not(and(sF2,a)),
inference(forward_demodulation,[],[f14427,f285]) ).
fof(f14526,plain,
not(and(b,t1)) = or(a,not(b)),
inference(forward_demodulation,[],[f14446,f1]) ).
fof(f14541,plain,
! [X2,X0,X1] : or(and(X0,X1),not(and(X0,or(X2,X1)))) = or(X1,not(and(X0,or(X2,X1)))),
inference(forward_demodulation,[],[f14462,f1]) ).
fof(f14563,plain,
! [X0,X1] : and(X1,X0) = and(X0,or(X1,not(X0))),
inference(forward_demodulation,[],[f14486,f10829]) ).
fof(f14574,plain,
or(t4,and(t3,sF0)) = or(t1,and(t3,sF0)),
inference(forward_demodulation,[],[f14502,f1]) ).
fof(f14577,plain,
or(b,not(a)) = not(and(sF2,sF10)),
inference(forward_demodulation,[],[f14507,f1626]) ).
fof(f14596,plain,
not(and(b,t1)) = or(a,sF2),
inference(forward_demodulation,[],[f14526,f52]) ).
fof(f14609,plain,
! [X2,X0,X1] : or(X1,not(and(X0,X2))) = or(and(X0,X1),not(and(X0,or(X2,X1)))),
inference(forward_demodulation,[],[f14541,f12406]) ).
fof(f14632,plain,
t1 = or(t4,and(t3,sF0)),
inference(forward_demodulation,[],[f14574,f11110]) ).
fof(f14634,plain,
or(b,not(a)) = or(b,not(sF10)),
inference(forward_demodulation,[],[f14577,f1626]) ).
fof(f14652,plain,
not(and(b,t1)) = or(t3,not(t2)),
inference(forward_demodulation,[],[f14596,f9898]) ).
fof(f14676,plain,
or(b,not(a)) = or(b,and(t3,sF0)),
inference(forward_demodulation,[],[f14634,f4392]) ).
fof(f14690,plain,
not(and(t1,b)) = or(t3,not(t2)),
inference(forward_demodulation,[],[f14652,f8458]) ).
fof(f14706,plain,
not(sF3) = or(b,not(a)),
inference(forward_demodulation,[],[f14676,f11980]) ).
fof(f14710,plain,
not(sF1) = or(t3,not(t2)),
inference(forward_demodulation,[],[f14690,f4321]) ).
fof(f14722,plain,
not(sF3) = or(b,sF0),
inference(forward_demodulation,[],[f14706,f48]) ).
fof(f14724,plain,
t3 = or(t3,not(t2)),
inference(forward_demodulation,[],[f14710,f4355]) ).
fof(f14880,plain,
! [X0,X1] : and(not(X0),X1) = and(X1,not(and(X0,X1))),
inference(superposition,[],[f14563,f27]) ).
fof(f16099,plain,
! [X2,X3,X0,X1] : or(X1,and(X3,or(X2,X0))) = and(or(X1,X3),or(X0,or(X1,X2))),
inference(superposition,[],[f8,f562]) ).
fof(f16191,plain,
! [X2,X3,X0,X1] : or(X0,and(X1,X2)) = or(X0,and(and(X2,X1),or(X2,X3))),
inference(backward_demodulation,[],[f10558,f16099]) ).
fof(f16320,plain,
! [X2,X3,X0,X1] : or(X0,and(X1,X2)) = or(X0,and(X2,and(X1,or(X2,X3)))),
inference(forward_demodulation,[],[f16191,f4]) ).
fof(f16368,plain,
! [X2,X0,X1] : or(X0,and(X1,X2)) = or(X0,and(X2,X1)),
inference(forward_demodulation,[],[f16320,f1158]) ).
fof(f16429,plain,
! [X2,X0,X1] : or(and(X0,X2),not(and(X0,X1))) = or(and(X0,X2),not(and(X0,or(X1,X2)))),
inference(superposition,[],[f859,f7]) ).
fof(f16449,plain,
or(sF0,not(b)) = or(sF0,not(not(sF3))),
inference(superposition,[],[f859,f14722]) ).
fof(f16478,plain,
or(sF3,not(sF1)) = or(sF3,not(not(sF5))),
inference(superposition,[],[f859,f477]) ).
fof(f16591,plain,
or(sF3,sF5) = or(sF3,not(sF1)),
inference(forward_demodulation,[],[f16478,f15]) ).
fof(f16620,plain,
or(sF0,not(b)) = not(and(a,not(sF3))),
inference(forward_demodulation,[],[f16449,f275]) ).
fof(f16640,plain,
! [X2,X0,X1] : or(X2,not(and(X0,X1))) = or(and(X0,X2),not(and(X0,X1))),
inference(forward_demodulation,[],[f16429,f14609]) ).
fof(f16685,plain,
or(sF3,sF5) = or(sF3,t3),
inference(forward_demodulation,[],[f16591,f4355]) ).
fof(f16711,plain,
or(sF0,not(b)) = or(not(a),sF3),
inference(forward_demodulation,[],[f16620,f433]) ).
fof(f16769,plain,
or(t3,sF3) = or(sF3,sF5),
inference(forward_demodulation,[],[f16685,f1]) ).
fof(f16781,plain,
or(sF0,not(b)) = or(sF3,not(a)),
inference(forward_demodulation,[],[f16711,f1]) ).
fof(f16833,plain,
or(sF0,not(b)) = or(sF3,sF0),
inference(forward_demodulation,[],[f16781,f48]) ).
fof(f16870,plain,
or(sF0,not(b)) = or(sF0,sF3),
inference(forward_demodulation,[],[f16833,f1]) ).
fof(f16891,plain,
not(and(a,b)) = or(sF0,sF3),
inference(forward_demodulation,[],[f16870,f275]) ).
fof(f16906,plain,
not(not(t1)) = or(sF0,sF3),
inference(forward_demodulation,[],[f16891,f421]) ).
fof(f16916,plain,
t1 = or(sF0,sF3),
inference(forward_demodulation,[],[f16906,f15]) ).
fof(f16941,plain,
sF5 = and(sF5,or(t3,sF3)),
inference(superposition,[],[f318,f16769]) ).
fof(f17001,plain,
sF3 = and(t1,or(not(sF0),sF3)),
inference(superposition,[],[f8349,f16916]) ).
fof(f17002,plain,
sF3 = and(t1,or(sF3,not(sF0))),
inference(forward_demodulation,[],[f17001,f10687]) ).
fof(f17020,plain,
sF3 = and(t1,or(sF3,a)),
inference(forward_demodulation,[],[f17002,f426]) ).
fof(f17030,plain,
sF3 = and(t1,or(a,sF3)),
inference(forward_demodulation,[],[f17020,f10687]) ).
fof(f17038,plain,
sF3 = and(t1,a),
inference(forward_demodulation,[],[f17030,f853]) ).
fof(f17043,plain,
sF3 = not(t2),
inference(forward_demodulation,[],[f17038,f467]) ).
fof(f17070,plain,
sF5 = and(t3,not(not(t2))),
inference(backward_demodulation,[],[f4747,f17043]) ).
fof(f17090,plain,
ll1 = or(sF10,not(not(t2))),
inference(backward_demodulation,[],[f11959,f17043]) ).
fof(f17137,plain,
sF5 = and(sF5,or(t3,not(t2))),
inference(backward_demodulation,[],[f16941,f17043]) ).
fof(f17172,plain,
sF5 = and(sF5,t3),
inference(forward_demodulation,[],[f17137,f14724]) ).
fof(f17195,plain,
ll1 = or(sF10,t2),
inference(forward_demodulation,[],[f17090,f15]) ).
fof(f17203,plain,
sF5 = and(t3,t2),
inference(forward_demodulation,[],[f17070,f15]) ).
fof(f17230,plain,
sF5 = and(t3,sF5),
inference(forward_demodulation,[],[f17172,f2]) ).
fof(f17245,plain,
ll1 = or(t2,sF10),
inference(forward_demodulation,[],[f17195,f1]) ).
fof(f17252,plain,
and(t2,t3) = sF5,
inference(forward_demodulation,[],[f17203,f2]) ).
fof(f17280,plain,
sF5 = not(t4),
inference(backward_demodulation,[],[f423,f17252]) ).
fof(f17297,plain,
and(cin,sF5) = not(t7),
inference(backward_demodulation,[],[f4307,f17280]) ).
fof(f17305,plain,
ll1 = or(t1,sF5),
inference(backward_demodulation,[],[f5317,f17280]) ).
fof(f17341,plain,
sF6 = not(t7),
inference(backward_demodulation,[],[f132,f17297]) ).
fof(f17353,plain,
sum_def = or(not(t7),sF8),
inference(backward_demodulation,[],[f134,f17341]) ).
fof(f17398,plain,
not(sum_def) = and(t7,not(sF8)),
inference(superposition,[],[f436,f17353]) ).
fof(f17487,plain,
not(sF10) = or(not(ll1),and(t2,not(sF10))),
inference(superposition,[],[f8081,f17245]) ).
fof(f17492,plain,
and(t3,sF0) = or(not(ll1),and(t2,and(t3,sF0))),
inference(forward_demodulation,[],[f17487,f4392]) ).
fof(f17508,plain,
and(t3,sF0) = or(ll0,and(t2,and(t3,sF0))),
inference(forward_demodulation,[],[f17492,f19]) ).
fof(f17518,plain,
and(t3,sF0) = and(t2,and(t3,sF0)),
inference(forward_demodulation,[],[f17508,f358]) ).
fof(f17528,plain,
t4 = not(sF5),
inference(superposition,[],[f15,f17280]) ).
fof(f17529,plain,
! [X0] : and(sF5,not(X0)) = not(or(t4,X0)),
inference(superposition,[],[f26,f17280]) ).
fof(f17531,plain,
! [X0] : or(sF5,not(X0)) = not(and(t4,X0)),
inference(superposition,[],[f27,f17280]) ).
fof(f17545,plain,
! [X0] : and(t4,not(X0)) = not(or(sF5,X0)),
inference(superposition,[],[f436,f17280]) ).
fof(f18173,plain,
! [X0] : and(t2,and(t3,X0)) = and(X0,sF5),
inference(superposition,[],[f663,f17252]) ).
fof(f18186,plain,
and(t3,sF0) = and(sF0,sF5),
inference(backward_demodulation,[],[f17518,f18173]) ).
fof(f19466,plain,
! [X0] : or(X0,not(not(t5))) = or(and(t4,X0),not(not(t5))),
inference(superposition,[],[f16640,f447]) ).
fof(f19491,plain,
! [X0] : or(X0,not(sF5)) = or(and(t3,X0),not(sF5)),
inference(superposition,[],[f16640,f17230]) ).
fof(f19571,plain,
! [X0] : or(X0,t4) = or(and(t3,X0),t4),
inference(forward_demodulation,[],[f19491,f17528]) ).
fof(f19596,plain,
! [X0] : or(X0,t5) = or(and(t4,X0),t5),
inference(forward_demodulation,[],[f19466,f15]) ).
fof(f19708,plain,
! [X0] : or(X0,t4) = or(t4,and(t3,X0)),
inference(forward_demodulation,[],[f19571,f1]) ).
fof(f19732,plain,
! [X0] : or(X0,t5) = or(t5,and(t4,X0)),
inference(forward_demodulation,[],[f19596,f1]) ).
fof(f19818,plain,
t1 = or(sF0,t4),
inference(backward_demodulation,[],[f14632,f19708]) ).
fof(f19870,plain,
t1 = or(t4,sF0),
inference(forward_demodulation,[],[f19818,f1]) ).
fof(f19945,plain,
and(not(sF0),t1) = and(not(sF0),t4),
inference(superposition,[],[f615,f19870]) ).
fof(f19968,plain,
and(not(sF0),t1) = and(t4,not(sF0)),
inference(forward_demodulation,[],[f19945,f2]) ).
fof(f19978,plain,
and(a,t1) = and(t4,a),
inference(forward_demodulation,[],[f19968,f426]) ).
fof(f19986,plain,
and(t1,a) = and(t4,a),
inference(forward_demodulation,[],[f19978,f2]) ).
fof(f19991,plain,
not(t2) = and(t4,a),
inference(forward_demodulation,[],[f19986,f467]) ).
fof(f20016,plain,
and(a,not(not(t2))) = and(a,not(t4)),
inference(superposition,[],[f623,f19991]) ).
fof(f20033,plain,
and(a,not(not(t2))) = and(a,sF5),
inference(forward_demodulation,[],[f20016,f17280]) ).
fof(f20043,plain,
and(a,t2) = and(a,sF5),
inference(forward_demodulation,[],[f20033,f15]) ).
fof(f20048,plain,
and(t2,a) = and(a,sF5),
inference(forward_demodulation,[],[f20043,f2]) ).
fof(f20051,plain,
not(t1) = and(a,sF5),
inference(forward_demodulation,[],[f20048,f4309]) ).
fof(f20714,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(not(or(X0,X2)))) = and(or(X0,and(X1,X2)),not(ll0)),
inference(superposition,[],[f623,f1145]) ).
fof(f20732,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(not(or(X0,X2)))) = and(not(ll0),or(and(X1,X2),X0)),
inference(forward_demodulation,[],[f20714,f10829]) ).
fof(f20946,plain,
! [X2,X0,X1] : and(or(X0,and(X1,X2)),not(not(or(X0,X2)))) = and(ll1,or(and(X1,X2),X0)),
inference(forward_demodulation,[],[f20732,f17]) ).
fof(f21093,plain,
! [X2,X0,X1] : or(and(X1,X2),X0) = and(or(X0,and(X1,X2)),not(not(or(X0,X2)))),
inference(forward_demodulation,[],[f20946,f264]) ).
fof(f21183,plain,
! [X2,X0,X1] : or(and(X1,X2),X0) = and(or(X0,and(X1,X2)),or(X0,X2)),
inference(forward_demodulation,[],[f21093,f15]) ).
fof(f21259,plain,
! [X2,X0,X1] : or(and(X1,X2),X0) = or(X0,and(and(X1,X2),X2)),
inference(forward_demodulation,[],[f21183,f8]) ).
fof(f21317,plain,
! [X2,X0,X1] : or(and(X1,X2),X0) = or(X0,and(X2,and(X1,X2))),
inference(forward_demodulation,[],[f21259,f16368]) ).
fof(f21356,plain,
! [X2,X0,X1] : or(X0,and(X2,X1)) = or(and(X1,X2),X0),
inference(forward_demodulation,[],[f21317,f343]) ).
fof(f22561,plain,
and(sF5,not(sF0)) = and(sF5,not(and(t3,sF0))),
inference(superposition,[],[f623,f18186]) ).
fof(f22578,plain,
and(sF5,not(sF0)) = not(or(t4,and(t3,sF0))),
inference(forward_demodulation,[],[f22561,f17529]) ).
fof(f22592,plain,
and(not(t4),sF10) = and(sF5,not(sF0)),
inference(forward_demodulation,[],[f22578,f4449]) ).
fof(f22601,plain,
and(not(t4),sF10) = not(or(t4,sF0)),
inference(forward_demodulation,[],[f22592,f17529]) ).
fof(f22610,plain,
and(not(t4),sF10) = and(a,not(t4)),
inference(forward_demodulation,[],[f22601,f1866]) ).
fof(f22619,plain,
and(sF5,sF10) = and(a,sF5),
inference(forward_demodulation,[],[f22610,f17280]) ).
fof(f22625,plain,
not(t1) = and(sF5,sF10),
inference(forward_demodulation,[],[f22619,f20051]) ).
fof(f23001,plain,
and(not(sF5),cin) = and(not(sF5),not(sF8)),
inference(superposition,[],[f615,f532]) ).
fof(f23006,plain,
or(sF5,not(cin)) = or(sF5,not(not(sF8))),
inference(superposition,[],[f859,f532]) ).
fof(f23013,plain,
not(sF5) = or(not(not(sF8)),and(cin,not(sF5))),
inference(superposition,[],[f8081,f532]) ).
fof(f23018,plain,
t4 = or(not(not(sF8)),and(cin,t4)),
inference(forward_demodulation,[],[f23013,f17528]) ).
fof(f23023,plain,
or(sF5,not(cin)) = not(and(t4,not(sF8))),
inference(forward_demodulation,[],[f23006,f17531]) ).
fof(f23024,plain,
and(not(sF5),cin) = not(or(sF5,sF8)),
inference(forward_demodulation,[],[f23001,f26]) ).
fof(f23030,plain,
t4 = or(not(not(sF8)),and(t4,cin)),
inference(forward_demodulation,[],[f23018,f16368]) ).
fof(f23033,plain,
or(sF5,not(cin)) = or(not(t4),sF8),
inference(forward_demodulation,[],[f23023,f433]) ).
fof(f23034,plain,
and(not(sF5),cin) = and(t4,not(sF8)),
inference(forward_demodulation,[],[f23024,f17545]) ).
fof(f23037,plain,
t4 = or(and(cin,t4),not(not(sF8))),
inference(forward_demodulation,[],[f23030,f21356]) ).
fof(f23040,plain,
or(sF5,not(cin)) = or(sF8,not(t4)),
inference(forward_demodulation,[],[f23033,f1]) ).
fof(f23041,plain,
and(cin,not(sF5)) = and(t4,not(sF8)),
inference(forward_demodulation,[],[f23034,f2]) ).
fof(f23044,plain,
t4 = or(and(cin,t4),sF8),
inference(forward_demodulation,[],[f23037,f15]) ).
fof(f23047,plain,
or(sF5,not(cin)) = or(sF8,sF5),
inference(forward_demodulation,[],[f23040,f17280]) ).
fof(f23048,plain,
and(cin,t4) = and(t4,not(sF8)),
inference(forward_demodulation,[],[f23041,f17528]) ).
fof(f23050,plain,
t4 = or(sF8,and(t4,cin)),
inference(forward_demodulation,[],[f23044,f21356]) ).
fof(f23052,plain,
or(sF5,not(cin)) = or(sF5,sF8),
inference(forward_demodulation,[],[f23047,f1]) ).
fof(f23053,plain,
and(t4,cin) = and(t4,not(sF8)),
inference(forward_demodulation,[],[f23048,f2]) ).
fof(f23055,plain,
t4 = or(sF8,not(t5)),
inference(forward_demodulation,[],[f23050,f447]) ).
fof(f23056,plain,
not(and(t4,cin)) = or(sF5,sF8),
inference(forward_demodulation,[],[f23052,f17531]) ).
fof(f23057,plain,
not(t5) = and(t4,not(sF8)),
inference(forward_demodulation,[],[f23053,f447]) ).
fof(f23058,plain,
not(not(t5)) = or(sF5,sF8),
inference(forward_demodulation,[],[f23056,f447]) ).
fof(f23059,plain,
t5 = or(sF5,sF8),
inference(forward_demodulation,[],[f23058,f15]) ).
fof(f23072,plain,
or(sF8,not(t5)) = or(sF8,not(sF5)),
inference(superposition,[],[f859,f23059]) ).
fof(f23081,plain,
sF8 = and(t5,or(not(sF5),sF8)),
inference(superposition,[],[f8349,f23059]) ).
fof(f23082,plain,
sF8 = and(t5,or(sF8,not(sF5))),
inference(forward_demodulation,[],[f23081,f10687]) ).
fof(f23089,plain,
or(sF8,not(t5)) = or(sF8,t4),
inference(forward_demodulation,[],[f23072,f17528]) ).
fof(f23099,plain,
sF8 = and(t5,or(sF8,t4)),
inference(forward_demodulation,[],[f23082,f17528]) ).
fof(f23104,plain,
or(t4,sF8) = or(sF8,not(t5)),
inference(forward_demodulation,[],[f23089,f1]) ).
fof(f23108,plain,
sF8 = and(t5,or(t4,sF8)),
inference(forward_demodulation,[],[f23099,f10687]) ).
fof(f23111,plain,
t4 = or(t4,sF8),
inference(forward_demodulation,[],[f23104,f23055]) ).
fof(f23116,plain,
sF8 = and(t5,t4),
inference(backward_demodulation,[],[f23108,f23111]) ).
fof(f23119,plain,
and(t4,t5) = sF8,
inference(forward_demodulation,[],[f23116,f2]) ).
fof(f23121,plain,
sF8 = not(t6),
inference(forward_demodulation,[],[f23119,f424]) ).
fof(f23134,plain,
not(sum_def) = and(t7,not(not(t6))),
inference(backward_demodulation,[],[f17398,f23121]) ).
fof(f23160,plain,
not(t5) = and(t4,not(not(t6))),
inference(backward_demodulation,[],[f23057,f23121]) ).
fof(f23178,plain,
not(t5) = and(t4,t6),
inference(forward_demodulation,[],[f23160,f15]) ).
fof(f23198,plain,
and(t7,t6) = not(sum_def),
inference(forward_demodulation,[],[f23134,f15]) ).
fof(f23210,plain,
not(t5) = and(t6,t4),
inference(forward_demodulation,[],[f23178,f2]) ).
fof(f23226,plain,
and(t6,t7) = not(sum_def),
inference(forward_demodulation,[],[f23198,f2]) ).
fof(f23238,plain,
not(sum) = not(sum_def),
inference(backward_demodulation,[],[f425,f23226]) ).
fof(f23407,plain,
sum = not(not(sum_def)),
inference(superposition,[],[f15,f23238]) ).
fof(f23467,plain,
sum_def = sum,
inference(forward_demodulation,[],[f23407,f15]) ).
fof(f23491,plain,
spl32_2,
inference(avatar_split_clause,[],[f23467,f127]) ).
fof(f24630,plain,
! [X2,X0,X1] : and(not(or(X0,X1)),or(X0,X2)) = or(ll0,and(not(or(X0,X1)),X2)),
inference(superposition,[],[f211,f1283]) ).
fof(f25040,plain,
! [X2,X0,X1] : and(not(or(X0,X1)),X2) = and(not(or(X0,X1)),or(X0,X2)),
inference(forward_demodulation,[],[f24630,f358]) ).
fof(f27876,plain,
! [X0,X1] : and(X1,not(X0)) = and(not(X0),or(X0,X1)),
inference(superposition,[],[f8780,f15]) ).
fof(f31838,plain,
! [X2,X0,X1] : and(or(X0,X2),not(or(X0,and(X1,X2)))) = and(not(or(X0,X1)),or(X0,X2)),
inference(superposition,[],[f14880,f8]) ).
fof(f32155,plain,
! [X2,X0,X1] : and(not(or(X0,X1)),X2) = and(or(X0,X2),not(or(X0,and(X1,X2)))),
inference(forward_demodulation,[],[f31838,f25040]) ).
fof(f32269,plain,
! [X2,X0,X1] : and(not(or(X0,X1)),X2) = and(or(X0,X2),not(or(X0,X1))),
inference(backward_demodulation,[],[f4167,f32155]) ).
fof(f32889,plain,
! [X0] : and(sF13,X0) = and(or(t1,X0),sF13),
inference(superposition,[],[f32269,f4067]) ).
fof(f33837,plain,
! [X0] : and(sF13,X0) = and(sF13,or(t1,X0)),
inference(superposition,[],[f2,f32889]) ).
fof(f33889,plain,
! [X0] : and(sF13,X0) = and(sF13,or(cin,X0)),
inference(backward_demodulation,[],[f4148,f33837]) ).
fof(f36008,plain,
! [X0] : or(cin,and(X0,t5)) = and(or(cin,X0),ll1),
inference(superposition,[],[f316,f2984]) ).
fof(f36038,plain,
! [X0] : or(sF13,and(X0,sF11)) = and(or(sF13,X0),carry_def),
inference(superposition,[],[f316,f136]) ).
fof(f36139,plain,
! [X0] : or(sF13,and(X0,sF11)) = and(carry_def,or(X0,sF13)),
inference(forward_demodulation,[],[f36038,f10829]) ).
fof(f36169,plain,
! [X0] : or(cin,and(X0,t5)) = and(ll1,or(X0,cin)),
inference(forward_demodulation,[],[f36008,f10829]) ).
fof(f36406,plain,
! [X0] : or(X0,cin) = or(cin,and(X0,t5)),
inference(forward_demodulation,[],[f36169,f264]) ).
fof(f36760,plain,
! [X0] : or(sF5,and(t1,X0)) = and(ll1,or(sF5,X0)),
inference(superposition,[],[f317,f17305]) ).
fof(f37184,plain,
! [X0] : or(sF5,X0) = or(sF5,and(t1,X0)),
inference(forward_demodulation,[],[f36760,f264]) ).
fof(f39405,plain,
! [X0] : or(cin,X0) = or(cin,or(X0,sF11)),
inference(superposition,[],[f1346,f71]) ).
fof(f40896,plain,
! [X0] : or(sF11,and(sF13,X0)) = and(carry_def,or(sF11,or(cin,X0))),
inference(superposition,[],[f189,f33889]) ).
fof(f40907,plain,
or(sF11,ll0) = and(carry_def,or(sF11,not(sF13))),
inference(superposition,[],[f189,f12]) ).
fof(f40936,plain,
! [X0] : and(carry_def,or(sF11,X0)) = or(sF11,and(carry_def,or(sF11,X0))),
inference(superposition,[],[f943,f189]) ).
fof(f40953,plain,
! [X0] : and(carry_def,or(sF11,X0)) = or(sF11,and(carry_def,X0)),
inference(forward_demodulation,[],[f40936,f2788]) ).
fof(f40980,plain,
or(sF11,ll0) = and(carry_def,or(sF11,or(t1,cin))),
inference(forward_demodulation,[],[f40907,f4074]) ).
fof(f40990,plain,
! [X0] : or(sF11,and(sF13,X0)) = and(carry_def,or(cin,or(X0,sF11))),
inference(forward_demodulation,[],[f40896,f10747]) ).
fof(f41008,plain,
! [X0] : or(sF11,and(sF13,X0)) = or(sF11,and(carry_def,X0)),
inference(backward_demodulation,[],[f189,f40953]) ).
fof(f41038,plain,
or(sF11,ll0) = or(sF11,and(carry_def,or(t1,cin))),
inference(forward_demodulation,[],[f40980,f40953]) ).
fof(f41047,plain,
! [X0] : or(sF11,and(sF13,X0)) = and(carry_def,or(cin,X0)),
inference(forward_demodulation,[],[f40990,f39405]) ).
fof(f41076,plain,
sF11 = or(sF11,and(carry_def,or(t1,cin))),
inference(forward_demodulation,[],[f41038,f5]) ).
fof(f41085,plain,
! [X0] : or(sF11,and(carry_def,X0)) = and(carry_def,or(cin,X0)),
inference(backward_demodulation,[],[f41008,f41047]) ).
fof(f41111,plain,
sF11 = and(carry_def,or(cin,or(t1,cin))),
inference(backward_demodulation,[],[f41076,f41085]) ).
fof(f41133,plain,
sF11 = and(carry_def,or(t1,or(cin,cin))),
inference(forward_demodulation,[],[f41111,f10747]) ).
fof(f41145,plain,
sF11 = and(carry_def,or(t1,cin)),
inference(forward_demodulation,[],[f41133,f13]) ).
fof(f41185,plain,
or(not(or(t1,cin)),sF11) = or(carry_def,not(or(t1,cin))),
inference(superposition,[],[f9554,f41145]) ).
fof(f41193,plain,
or(sF13,sF11) = or(carry_def,sF13),
inference(forward_demodulation,[],[f41185,f4067]) ).
fof(f41212,plain,
or(sF11,sF13) = or(carry_def,sF13),
inference(forward_demodulation,[],[f41193,f1]) ).
fof(f41228,plain,
carry_def = or(carry_def,sF13),
inference(forward_demodulation,[],[f41212,f136]) ).
fof(f41248,plain,
! [X0] : and(or(sF13,X0),carry_def) = or(sF13,and(X0,carry_def)),
inference(superposition,[],[f316,f41228]) ).
fof(f41265,plain,
or(not(sF13),carry_def) = or(carry_def,not(carry_def)),
inference(superposition,[],[f8457,f41228]) ).
fof(f41272,plain,
ll1 = or(not(sF13),carry_def),
inference(forward_demodulation,[],[f41265,f10]) ).
fof(f41285,plain,
! [X0] : and(carry_def,or(X0,sF13)) = or(sF13,and(X0,carry_def)),
inference(forward_demodulation,[],[f41248,f10829]) ).
fof(f41290,plain,
ll1 = or(carry_def,not(sF13)),
inference(forward_demodulation,[],[f41272,f1]) ).
fof(f41295,plain,
! [X0] : or(sF13,and(X0,sF11)) = or(sF13,and(X0,carry_def)),
inference(backward_demodulation,[],[f36139,f41285]) ).
fof(f41298,plain,
ll1 = or(carry_def,or(t1,cin)),
inference(forward_demodulation,[],[f41290,f4074]) ).
fof(f42911,plain,
! [X0] : and(sF11,X0) = and(cin,and(X0,sF10)),
inference(superposition,[],[f844,f2]) ).
fof(f44684,plain,
or(t5,t4) = or(t1,t5),
inference(superposition,[],[f19732,f5320]) ).
fof(f44753,plain,
or(t4,t5) = or(t1,t5),
inference(forward_demodulation,[],[f44684,f1]) ).
fof(f44800,plain,
ll1 = or(t1,t5),
inference(forward_demodulation,[],[f44753,f2168]) ).
fof(f45888,plain,
! [X0] : and(ll1,or(X0,t1)) = or(t1,and(t5,X0)),
inference(superposition,[],[f316,f44800]) ).
fof(f45909,plain,
and(t5,not(t1)) = and(not(t1),ll1),
inference(superposition,[],[f27876,f44800]) ).
fof(f45914,plain,
not(t1) = and(t5,not(t1)),
inference(forward_demodulation,[],[f45909,f6]) ).
fof(f45930,plain,
! [X0] : or(X0,t1) = or(t1,and(t5,X0)),
inference(forward_demodulation,[],[f45888,f264]) ).
fof(f89702,plain,
and(cin,t4) = and(sF11,t1),
inference(superposition,[],[f42911,f5302]) ).
fof(f89708,plain,
and(cin,not(t1)) = and(sF11,sF5),
inference(superposition,[],[f42911,f22625]) ).
fof(f89811,plain,
and(cin,not(t1)) = and(sF5,sF11),
inference(forward_demodulation,[],[f89708,f2]) ).
fof(f89817,plain,
and(cin,t4) = and(t1,sF11),
inference(forward_demodulation,[],[f89702,f2]) ).
fof(f89843,plain,
and(t4,cin) = and(t1,sF11),
inference(forward_demodulation,[],[f89817,f2]) ).
fof(f89856,plain,
not(t5) = and(t1,sF11),
inference(forward_demodulation,[],[f89843,f447]) ).
fof(f89864,plain,
or(sF5,not(t5)) = or(sF5,sF11),
inference(superposition,[],[f37184,f89856]) ).
fof(f89896,plain,
or(not(t1),not(t5)) = or(sF11,not(t1)),
inference(superposition,[],[f9533,f89856]) ).
fof(f89919,plain,
or(not(t1),not(t5)) = or(not(t1),sF11),
inference(forward_demodulation,[],[f89896,f1]) ).
fof(f89940,plain,
not(and(t4,t5)) = or(sF5,sF11),
inference(forward_demodulation,[],[f89864,f17531]) ).
fof(f89953,plain,
not(and(t1,t5)) = or(not(t1),sF11),
inference(forward_demodulation,[],[f89919,f27]) ).
fof(f89968,plain,
not(not(t6)) = or(sF5,sF11),
inference(forward_demodulation,[],[f89940,f424]) ).
fof(f89973,plain,
not(not(carry)) = or(not(t1),sF11),
inference(forward_demodulation,[],[f89953,f422]) ).
fof(f89978,plain,
t6 = or(sF5,sF11),
inference(forward_demodulation,[],[f89968,f15]) ).
fof(f89980,plain,
carry = or(not(t1),sF11),
inference(forward_demodulation,[],[f89973,f15]) ).
fof(f90543,plain,
and(not(sF5),t6) = and(sF11,not(sF5)),
inference(superposition,[],[f27876,f89978]) ).
fof(f90556,plain,
and(t4,t6) = and(sF11,t4),
inference(forward_demodulation,[],[f90543,f17528]) ).
fof(f90589,plain,
and(t4,t6) = and(t4,sF11),
inference(forward_demodulation,[],[f90556,f2]) ).
fof(f90606,plain,
and(t6,t4) = and(t4,sF11),
inference(forward_demodulation,[],[f90589,f2]) ).
fof(f90618,plain,
not(t5) = and(t4,sF11),
inference(forward_demodulation,[],[f90606,f23210]) ).
fof(f90662,plain,
and(sF11,not(not(t5))) = and(not(t4),sF11),
inference(superposition,[],[f14880,f90618]) ).
fof(f90681,plain,
and(sF5,sF11) = and(sF11,not(not(t5))),
inference(forward_demodulation,[],[f90662,f17280]) ).
fof(f90712,plain,
and(sF5,sF11) = and(sF11,t5),
inference(forward_demodulation,[],[f90681,f15]) ).
fof(f90732,plain,
and(sF5,sF11) = and(t5,sF11),
inference(forward_demodulation,[],[f90712,f2]) ).
fof(f90739,plain,
and(cin,not(t1)) = and(t5,sF11),
inference(backward_demodulation,[],[f89811,f90732]) ).
fof(f90745,plain,
not(t1) = or(sF13,and(t5,sF11)),
inference(backward_demodulation,[],[f11373,f90739]) ).
fof(f90747,plain,
not(t1) = or(sF13,and(t5,carry_def)),
inference(forward_demodulation,[],[f90745,f41295]) ).
fof(f90748,plain,
not(t1) = or(sF13,and(carry_def,t5)),
inference(forward_demodulation,[],[f90747,f16368]) ).
fof(f90763,plain,
and(carry_def,t5) = and(and(carry_def,t5),not(t1)),
inference(superposition,[],[f318,f90748]) ).
fof(f90771,plain,
or(and(carry_def,t5),not(sF13)) = or(and(carry_def,t5),not(not(t1))),
inference(superposition,[],[f859,f90748]) ).
fof(f90808,plain,
or(and(carry_def,t5),not(sF13)) = or(and(carry_def,t5),t1),
inference(forward_demodulation,[],[f90771,f15]) ).
fof(f90815,plain,
and(carry_def,t5) = and(carry_def,and(t5,not(t1))),
inference(forward_demodulation,[],[f90763,f4]) ).
fof(f90841,plain,
or(and(carry_def,t5),not(sF13)) = or(t1,and(t5,carry_def)),
inference(forward_demodulation,[],[f90808,f21356]) ).
fof(f90845,plain,
and(carry_def,t5) = and(carry_def,not(t1)),
inference(forward_demodulation,[],[f90815,f45914]) ).
fof(f90859,plain,
or(and(carry_def,t5),not(sF13)) = or(carry_def,t1),
inference(forward_demodulation,[],[f90841,f45930]) ).
fof(f90873,plain,
or(carry_def,t1) = or(and(carry_def,t5),or(t1,cin)),
inference(forward_demodulation,[],[f90859,f4074]) ).
fof(f90882,plain,
or(carry_def,t1) = or(cin,or(and(carry_def,t5),t1)),
inference(forward_demodulation,[],[f90873,f562]) ).
fof(f90888,plain,
or(t1,or(cin,and(carry_def,t5))) = or(carry_def,t1),
inference(forward_demodulation,[],[f90882,f562]) ).
fof(f90893,plain,
or(carry_def,t1) = or(t1,or(carry_def,cin)),
inference(forward_demodulation,[],[f90888,f36406]) ).
fof(f90897,plain,
or(carry_def,t1) = or(carry_def,or(cin,t1)),
inference(forward_demodulation,[],[f90893,f562]) ).
fof(f90900,plain,
or(carry_def,or(t1,cin)) = or(carry_def,t1),
inference(forward_demodulation,[],[f90897,f10875]) ).
fof(f90903,plain,
ll1 = or(carry_def,t1),
inference(forward_demodulation,[],[f90900,f41298]) ).
fof(f90944,plain,
and(not(t1),ll1) = and(carry_def,not(t1)),
inference(superposition,[],[f8874,f90903]) ).
fof(f90964,plain,
and(not(t1),ll1) = and(carry_def,t5),
inference(forward_demodulation,[],[f90944,f90845]) ).
fof(f90995,plain,
not(t1) = and(carry_def,t5),
inference(forward_demodulation,[],[f90964,f6]) ).
fof(f91081,plain,
or(sF11,not(t1)) = and(carry_def,or(cin,t5)),
inference(superposition,[],[f41085,f90995]) ).
fof(f91145,plain,
or(sF11,not(t1)) = and(carry_def,or(t5,cin)),
inference(forward_demodulation,[],[f91081,f10687]) ).
fof(f91163,plain,
and(carry_def,ll1) = or(sF11,not(t1)),
inference(forward_demodulation,[],[f91145,f2984]) ).
fof(f91171,plain,
and(carry_def,ll1) = or(not(t1),sF11),
inference(forward_demodulation,[],[f91163,f1]) ).
fof(f91177,plain,
carry = and(carry_def,ll1),
inference(forward_demodulation,[],[f91171,f89980]) ).
fof(f91181,plain,
carry_def = carry,
inference(forward_demodulation,[],[f91177,f6]) ).
fof(f91182,plain,
( $false
| spl32_1 ),
inference(forward_subsumption_resolution,[],[f91181,f125]) ).
fof(f91183,plain,
spl32_1,
inference(avatar_contradiction_clause,[],[f91182]) ).
cnf(s1,plain,
( ~ spl32_1
| ~ spl32_2 ),
inference(sat_conversion,[],[f130]) ).
cnf(s2,plain,
spl32_2,
inference(sat_conversion,[],[f23491]) ).
cnf(s4,plain,
spl32_1,
inference(sat_conversion,[],[f91183]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s1,s2,s4]) ).
fof(f91184,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.48 % Computer : n006.cluster.edu
% 0.20/0.48 % Model : x86_64 x86_64
% 0.20/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.48 % Memory : 8046.5625MB
% 0.20/0.48 % OS : Linux 6.8.0-71-generic
% 0.20/0.48 % CPULimit : 300
% 0.20/0.48 % WCLimit : 300
% 0.20/0.48 % DateTime : Sun Sep 27 10:51:26 UTC 2026
% 0.20/0.49 % CPUTime :
% 0.20/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.54 Running first-order theorem proving
% 0.25/0.54 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.03/3.80 % (2802459)Input is clausal, will run a generic CNF schedule.
% 20.03/3.80 % (2802464)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=2647803347:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 20.03/3.80 % (2802466)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2360229026:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 20.03/3.80 % (2802468)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1691048043:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 20.03/3.80 % (2802465)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=897283119:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 20.03/3.80 % (2802470)dis-21_1_sil=8000:lcm=predicate:random_seed=3346193939: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)
% 20.03/3.80 % (2802467)lrs+10_1_sil=8000:sp=occurrence:random_seed=903118702:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 20.03/3.80 % (2802469)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2788795238:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 20.03/3.80 % (2802470)Refutation not found, incomplete strategy
% 20.03/3.80 % (2802470)------------------------------
% 20.03/3.80 % (2802470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.80 % (2802470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.80 % (2802470)CaDiCaL version: 2.1.3
% 20.03/3.80 % (2802470)Termination reason: Refutation not found, incomplete strategy
% 20.03/3.80 % (2802470)Time elapsed: 0.003 s
% 20.03/3.80 % (2802470)Peak memory usage: 88 MB
% 20.03/3.80 % (2802470)Instructions burned: 2 (million)
% 20.03/3.80 % (2802467)Instruction limit reached!
% 20.03/3.80 % (2802467)------------------------------
% 20.03/3.80 % (2802467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.80 % (2802467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.80 % (2802467)CaDiCaL version: 2.1.3
% 20.03/3.80 % (2802467)Termination reason: Instruction limit
% 20.03/3.80 % (2802467)Termination phase: Saturation
% 20.03/3.80 % (2802467)Time elapsed: 0.103 s
% 20.03/3.80 % (2802467)Peak memory usage: 89 MB
% 20.03/3.80 % (2802467)Instructions burned: 107 (million)
% 20.03/3.80 % (2802468)Instruction limit reached!
% 20.03/3.80 % (2802468)------------------------------
% 20.03/3.80 % (2802468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.80 % (2802468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.80 % (2802468)CaDiCaL version: 2.1.3
% 20.03/3.80 % (2802468)Termination reason: Instruction limit
% 20.03/3.80 % (2802468)Termination phase: Saturation
% 20.03/3.80 % (2802468)Time elapsed: 0.104 s
% 20.03/3.80 % (2802468)Peak memory usage: 89 MB
% 20.03/3.80 % (2802468)Instructions burned: 114 (million)
% 20.03/3.80 % (2802469)Instruction limit reached!
% 20.03/3.80 % (2802469)------------------------------
% 20.03/3.80 % (2802469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.80 % (2802469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.80 % (2802469)CaDiCaL version: 2.1.3
% 20.03/3.80 % (2802469)Termination reason: Instruction limit
% 20.03/3.80 % (2802469)Termination phase: Saturation
% 20.03/3.80 % (2802469)Time elapsed: 0.171 s
% 20.03/3.80 % (2802469)Peak memory usage: 90 MB
% 20.03/3.80 % (2802469)Instructions burned: 180 (million)
% 20.03/3.80 % (2802470)------------------------------
% 20.03/3.80 % (2802470)------------------------------
% 20.03/3.80 % (2802478)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=2048785651:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 20.03/3.80 % (2802479)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4211589357: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)
% 20.03/3.80 % (2802479)Refutation not found, incomplete strategy
% 20.03/3.80 % (2802479)------------------------------
% 20.03/3.80 % (2802479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.80 % (2802479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802479)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802479)Termination reason: Refutation not found, incomplete strategy
% 36.51/6.11 % (2802479)Time elapsed: 0.011 s
% 36.51/6.11 % (2802479)Peak memory usage: 88 MB
% 36.51/6.11 % (2802479)Instructions burned: 10 (million)
% 36.51/6.11 % (2802480)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3587818511:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 36.51/6.11 % (2802478)Instruction limit reached!
% 36.51/6.11 % (2802478)------------------------------
% 36.51/6.11 % (2802478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.11 % (2802478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802478)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802478)Termination reason: Instruction limit
% 36.51/6.11 % (2802478)Termination phase: Saturation
% 36.51/6.11 % (2802478)Time elapsed: 0.142 s
% 36.51/6.11 % (2802478)Peak memory usage: 90 MB
% 36.51/6.11 % (2802478)Instructions burned: 143 (million)
% 36.51/6.11 % (2802480)Instruction limit reached!
% 36.51/6.11 % (2802480)------------------------------
% 36.51/6.11 % (2802480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.11 % (2802480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802480)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802480)Termination reason: Instruction limit
% 36.51/6.11 % (2802480)Termination phase: Saturation
% 36.51/6.11 % (2802480)Time elapsed: 0.182 s
% 36.51/6.11 % (2802480)Peak memory usage: 89 MB
% 36.51/6.11 % (2802480)Instructions burned: 219 (million)
% 36.51/6.11 % (2802482)lrs+10_64_to=lpo:sil=8000:random_seed=605298332:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 36.51/6.11 % (2802482)Instruction limit reached!
% 36.51/6.11 % (2802482)------------------------------
% 36.51/6.11 % (2802482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.11 % (2802482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802482)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802482)Termination reason: Instruction limit
% 36.51/6.11 % (2802482)Termination phase: Saturation
% 36.51/6.11 % (2802482)Time elapsed: 0.118 s
% 36.51/6.11 % (2802482)Peak memory usage: 89 MB
% 36.51/6.11 % (2802482)Instructions burned: 130 (million)
% 36.51/6.11 % (2802479)------------------------------
% 36.51/6.11 % (2802479)------------------------------
% 36.51/6.11 % (2802485)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=966859741:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 36.51/6.11 % (2802486)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1513962620:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 36.51/6.11 % (2802485)Instruction limit reached!
% 36.51/6.11 % (2802485)------------------------------
% 36.51/6.11 % (2802485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.11 % (2802485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802485)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802485)Termination reason: Instruction limit
% 36.51/6.11 % (2802485)Termination phase: Saturation
% 36.51/6.11 % (2802485)Time elapsed: 0.184 s
% 36.51/6.11 % (2802485)Peak memory usage: 91 MB
% 36.51/6.11 % (2802485)Instructions burned: 194 (million)
% 36.51/6.11 % (2802488)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=606976401:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 36.51/6.11 % (2802486)Instruction limit reached!
% 36.51/6.11 % (2802486)------------------------------
% 36.51/6.11 % (2802486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.51/6.11 % (2802486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.51/6.11 % (2802486)CaDiCaL version: 2.1.3
% 36.51/6.11 % (2802486)Termination reason: Instruction limit
% 36.51/6.11 % (2802486)Termination phase: Saturation
% 36.51/6.11 % (2802486)Time elapsed: 0.156 s
% 36.51/6.11 % (2802486)Peak memory usage: 91 MB
% 36.51/6.11 % (2802486)Instructions burned: 157 (million)
% 36.51/6.11 % (2802490)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=312758377:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 36.51/6.11 % (2802490)Instruction limit reached!
% 36.51/6.11 % (2802490)------------------------------
% 36.51/6.11 % (2802490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802490)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802490)Termination reason: Instruction limit
% 54.55/8.71 % (2802490)Termination phase: Saturation
% 54.55/8.71 % (2802490)Time elapsed: 0.092 s
% 54.55/8.71 % (2802490)Peak memory usage: 89 MB
% 54.55/8.71 % (2802490)Instructions burned: 107 (million)
% 54.55/8.71 % (2802492)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3294580933:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 54.55/8.71 % (2802494)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3163162005:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 54.55/8.71 % (2802492)Instruction limit reached!
% 54.55/8.71 % (2802492)------------------------------
% 54.55/8.71 % (2802492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802492)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802492)Termination reason: Instruction limit
% 54.55/8.71 % (2802492)Termination phase: Saturation
% 54.55/8.71 % (2802492)Time elapsed: 0.104 s
% 54.55/8.71 % (2802492)Peak memory usage: 89 MB
% 54.55/8.71 % (2802492)Instructions burned: 107 (million)
% 54.55/8.71 % (2802496)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1677173232:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 54.55/8.71 % (2802494)Instruction limit reached!
% 54.55/8.71 % (2802494)------------------------------
% 54.55/8.71 % (2802494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802494)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802494)Termination reason: Instruction limit
% 54.55/8.71 % (2802494)Termination phase: Saturation
% 54.55/8.71 % (2802494)Time elapsed: 0.238 s
% 54.55/8.71 % (2802494)Peak memory usage: 91 MB
% 54.55/8.71 % (2802494)Instructions burned: 242 (million)
% 54.55/8.71 % (2802499)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1805309303:i=134:sd=2:doe=on:ss=axioms:sgt=14_2983 on theBenchmark for (2983ds/134Mi)
% 54.55/8.71 % (2802499)Instruction limit reached!
% 54.55/8.71 % (2802499)------------------------------
% 54.55/8.71 % (2802499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802499)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802499)Termination reason: Instruction limit
% 54.55/8.71 % (2802499)Termination phase: Saturation
% 54.55/8.71 % (2802499)Time elapsed: 0.131 s
% 54.55/8.71 % (2802499)Peak memory usage: 90 MB
% 54.55/8.71 % (2802499)Instructions burned: 134 (million)
% 54.55/8.71 % (2802501)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1225076873:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 54.55/8.71 % (2802503)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1813496747:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 54.55/8.71 % (2802501)Instruction limit reached!
% 54.55/8.71 % (2802501)------------------------------
% 54.55/8.71 % (2802501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802501)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802501)Termination reason: Instruction limit
% 54.55/8.71 % (2802501)Termination phase: Saturation
% 54.55/8.71 % (2802501)Time elapsed: 0.364 s
% 54.55/8.71 % (2802501)Peak memory usage: 90 MB
% 54.55/8.71 % (2802501)Instructions burned: 499 (million)
% 54.55/8.71 % (2802503)Instruction limit reached!
% 54.55/8.71 % (2802503)------------------------------
% 54.55/8.71 % (2802503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.55/8.71 % (2802503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.55/8.71 % (2802503)CaDiCaL version: 2.1.3
% 54.55/8.71 % (2802503)Termination reason: Instruction limit
% 54.55/8.71 % (2802503)Termination phase: Saturation
% 54.55/8.71 % (2802503)Time elapsed: 0.199 s
% 54.55/8.71 % (2802503)Peak memory usage: 92 MB
% 54.55/8.71 % (2802503)Instructions burned: 192 (million)
% 54.55/8.71 % (2802506)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4134356135:i=264:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/264Mi)
% 43.44/12.05 % (2802507)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1228175458:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 43.44/12.05 % (2802507)Instruction limit reached!
% 43.44/12.05 % (2802507)------------------------------
% 43.44/12.05 % (2802507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802507)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802507)Termination reason: Instruction limit
% 43.44/12.05 % (2802507)Termination phase: Saturation
% 43.44/12.05 % (2802507)Time elapsed: 0.149 s
% 43.44/12.05 % (2802507)Peak memory usage: 89 MB
% 43.44/12.05 % (2802507)Instructions burned: 156 (million)
% 43.44/12.05 % (2802506)Instruction limit reached!
% 43.44/12.05 % (2802506)------------------------------
% 43.44/12.05 % (2802506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802506)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802506)Termination reason: Instruction limit
% 43.44/12.05 % (2802506)Termination phase: Saturation
% 43.44/12.05 % (2802506)Time elapsed: 0.251 s
% 43.44/12.05 % (2802506)Peak memory usage: 92 MB
% 43.44/12.05 % (2802506)Instructions burned: 264 (million)
% 43.44/12.05 % (2802510)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=4220458209:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 43.44/12.05 % (2802511)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=721774943:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 43.44/12.05 % (2802511)Instruction limit reached!
% 43.44/12.05 % (2802511)------------------------------
% 43.44/12.05 % (2802511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802511)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802511)Termination reason: Instruction limit
% 43.44/12.05 % (2802511)Termination phase: Saturation
% 43.44/12.05 % (2802511)Time elapsed: 0.477 s
% 43.44/12.05 % (2802511)Peak memory usage: 95 MB
% 43.44/12.05 % (2802511)Instructions burned: 537 (million)
% 43.44/12.05 % (2802514)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2636563326:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 43.44/12.05 % (2802514)Instruction limit reached!
% 43.44/12.05 % (2802514)------------------------------
% 43.44/12.05 % (2802514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802514)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802514)Termination reason: Instruction limit
% 43.44/12.05 % (2802514)Termination phase: Saturation
% 43.44/12.05 % (2802514)Time elapsed: 0.154 s
% 43.44/12.05 % (2802514)Peak memory usage: 88 MB
% 43.44/12.05 % (2802514)Instructions burned: 180 (million)
% 43.44/12.05 % (2802516)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=2417009835:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2956 on theBenchmark for (2956ds/10307Mi)
% 43.44/12.05 % (2802488)Instruction limit reached!
% 43.44/12.05 % (2802488)------------------------------
% 43.44/12.05 % (2802488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802488)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802488)Termination reason: Instruction limit
% 43.44/12.05 % (2802488)Termination phase: Saturation
% 43.44/12.05 % (2802488)Time elapsed: 3.351 s
% 43.44/12.05 % (2802488)Peak memory usage: 152 MB
% 43.44/12.05 % (2802488)Instructions burned: 3394 (million)
% 43.44/12.05 % (2802521)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=3534416640:i=412:gtgl=4:gtg=exists_all_2952 on theBenchmark for (2952ds/412Mi)
% 43.44/12.05 % (2802521)Instruction limit reached!
% 43.44/12.05 % (2802521)------------------------------
% 43.44/12.05 % (2802521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802521)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802521)Termination reason: Instruction limit
% 43.44/12.05 % (2802521)Termination phase: Saturation
% 43.44/12.05 % (2802521)Time elapsed: 0.213 s
% 43.44/12.05 % (2802521)Peak memory usage: 95 MB
% 43.44/12.05 % (2802521)Instructions burned: 412 (million)
% 43.44/12.05 % (2802526)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=486948436:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 43.44/12.05 % (2802496)Instruction limit reached!
% 43.44/12.05 % (2802496)------------------------------
% 43.44/12.05 % (2802496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802496)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802496)Termination reason: Instruction limit
% 43.44/12.05 % (2802496)Termination phase: Saturation
% 43.44/12.05 % (2802496)Time elapsed: 4.621 s
% 43.44/12.05 % (2802496)Peak memory usage: 170 MB
% 43.44/12.05 % (2802496)Instructions burned: 5208 (million)
% 43.44/12.05 % (2802528)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=1296716963:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2935 on theBenchmark for (2935ds/303Mi)
% 43.44/12.05 % (2802528)Refutation not found, incomplete strategy
% 43.44/12.05 % (2802528)------------------------------
% 43.44/12.05 % (2802528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802528)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802528)Termination reason: Refutation not found, incomplete strategy
% 43.44/12.05 % (2802528)Time elapsed: 0.003 s
% 43.44/12.05 % (2802528)Peak memory usage: 88 MB
% 43.44/12.05 % (2802528)Instructions burned: 3 (million)
% 43.44/12.05 % (2802528)------------------------------
% 43.44/12.05 % (2802528)------------------------------
% 43.44/12.05 % (2802510)Instruction limit reached!
% 43.44/12.05 % (2802510)------------------------------
% 43.44/12.05 % (2802510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802510)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802510)Termination reason: Instruction limit
% 43.44/12.05 % (2802510)Termination phase: Saturation
% 43.44/12.05 % (2802510)Time elapsed: 3.469 s
% 43.44/12.05 % (2802510)Peak memory usage: 150 MB
% 43.44/12.05 % (2802510)Instructions burned: 3257 (million)
% 43.44/12.05 % (2802530)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2447143418:st=4:i=720:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/720Mi)
% 43.44/12.05 % (2802531)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2921902666:i=598:bs=on:bd=preordered:av=off:ss=axioms_2931 on theBenchmark for (2931ds/598Mi)
% 43.44/12.05 % (2802530)Instruction limit reached!
% 43.44/12.05 % (2802530)------------------------------
% 43.44/12.05 % (2802530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802530)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802530)Termination reason: Instruction limit
% 43.44/12.05 % (2802530)Termination phase: Saturation
% 43.44/12.05 % (2802530)Time elapsed: 0.379 s
% 43.44/12.05 % (2802530)Peak memory usage: 92 MB
% 43.44/12.05 % (2802530)Instructions burned: 721 (million)
% 43.44/12.05 % (2802534)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3007399547:i=2989:sd=3:ss=axioms:sgt=60_2926 on theBenchmark for (2926ds/2989Mi)
% 43.44/12.05 % (2802531)Instruction limit reached!
% 43.44/12.05 % (2802531)------------------------------
% 43.44/12.05 % (2802531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802531)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802531)Termination reason: Instruction limit
% 43.44/12.05 % (2802531)Termination phase: Saturation
% 43.44/12.05 % (2802531)Time elapsed: 0.523 s
% 43.44/12.05 % (2802531)Peak memory usage: 93 MB
% 43.44/12.05 % (2802531)Instructions burned: 598 (million)
% 43.44/12.05 % (2802536)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=1930089306:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2924 on theBenchmark for (2924ds/1997Mi)
% 43.44/12.05 % (2802536)Instruction limit reached!
% 43.44/12.05 % (2802536)------------------------------
% 43.44/12.05 % (2802536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802536)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802536)Termination reason: Instruction limit
% 43.44/12.05 % (2802536)Termination phase: Saturation
% 43.44/12.05 % (2802536)Time elapsed: 1.547 s
% 43.44/12.05 % (2802536)Peak memory usage: 138 MB
% 43.44/12.05 % (2802536)Instructions burned: 1997 (million)
% 43.44/12.05 % (2802534)Instruction limit reached!
% 43.44/12.05 % (2802534)------------------------------
% 43.44/12.05 % (2802534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802534)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802534)Termination reason: Instruction limit
% 43.44/12.05 % (2802534)Termination phase: Saturation
% 43.44/12.05 % (2802534)Time elapsed: 1.814 s
% 43.44/12.05 % (2802534)Peak memory usage: 148 MB
% 43.44/12.05 % (2802534)Instructions burned: 2989 (million)
% 43.44/12.05 % (2802538)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=3669058361:i=2088:bd=preordered:av=off_2906 on theBenchmark for (2906ds/2088Mi)
% 43.44/12.05 % (2802539)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1974117761:i=1098:nicw=on_2906 on theBenchmark for (2906ds/1098Mi)
% 43.44/12.05 % (2802539)Instruction limit reached!
% 43.44/12.05 % (2802539)------------------------------
% 43.44/12.05 % (2802539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802539)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802539)Termination reason: Instruction limit
% 43.44/12.05 % (2802539)Termination phase: Saturation
% 43.44/12.05 % (2802539)Time elapsed: 0.558 s
% 43.44/12.05 % (2802539)Peak memory usage: 94 MB
% 43.44/12.05 % (2802539)Instructions burned: 1099 (million)
% 43.44/12.05 % (2802542)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=516054964:i=433:bd=preordered_2899 on theBenchmark for (2899ds/433Mi)
% 43.44/12.05 % (2802542)Instruction limit reached!
% 43.44/12.05 % (2802542)------------------------------
% 43.44/12.05 % (2802542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802542)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802542)Termination reason: Instruction limit
% 43.44/12.05 % (2802542)Termination phase: Saturation
% 43.44/12.05 % (2802542)Time elapsed: 0.237 s
% 43.44/12.05 % (2802542)Peak memory usage: 93 MB
% 43.44/12.05 % (2802542)Instructions burned: 435 (million)
% 43.44/12.05 % (2802466)First to succeed.
% 43.44/12.05 % (2802466)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2802459"
% 43.44/12.05 % (2802544)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2872952101:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2895 on theBenchmark for (2895ds/2942Mi)
% 43.44/12.05 % (2802538)Instruction limit reached!
% 43.44/12.05 % (2802538)------------------------------
% 43.44/12.05 % (2802538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.44/12.05 % (2802538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.44/12.05 % (2802538)CaDiCaL version: 2.1.3
% 43.44/12.05 % (2802538)Termination reason: Instruction limit
% 43.44/12.05 % (2802538)Termination phase: Saturation
% 43.44/12.05 % (2802538)Time elapsed: 1.337 s
% 43.44/12.05 % (2802538)Peak memory usage: 138 MB
% 43.44/12.05 % (2802538)Instructions burned: 2088 (million)
% 43.44/12.05 % (2802466)Refutation found. Thanks to Tanya!
% 43.44/12.05 % SZS status Unsatisfiable for theBenchmark
% 43.44/12.05 % SZS output start Proof for theBenchmark
% See solution above
% 78.65/12.29 % (2802466)------------------------------
% 78.65/12.29 % (2802466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.65/12.29 % (2802466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.65/12.29 % (2802466)CaDiCaL version: 2.1.3
% 78.65/12.29 % (2802466)Termination reason: Refutation
% 78.65/12.29 % (2802466)Time elapsed: 10.356 s
% 78.65/12.29 % (2802466)Peak memory usage: 207 MB
% 78.65/12.29 % (2802466)Instructions burned: 9767 (million)
% 78.65/12.29 % (2802466)------------------------------
% 78.65/12.29 % (2802466)------------------------------
% 78.65/12.29 % (2802459)Success in time 11.093 s
% 78.65/12.29 % Vampire exiting
%------------------------------------------------------------------------------