%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT041-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 11:45:53 AM UTC 2026
% Result : Unsatisfiable 197.32s 33.38s
% Output : Refutation 230.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 25
% Syntax : Number of formulae : 613 ( 594 unt; 8 def)
% Number of atoms : 635 ( 606 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 47 ( 25 ~; 22 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 19 con; 0-3 aty)
% Number of variables : 849 ( 849 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : big_p(term1,X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term1) ).
fof(f2,axiom,
! [X0,X1] : big_p(term2,X0,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term2) ).
fof(f3,axiom,
! [X0,X1] : big_p(term3,X0,X1) = times(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term3) ).
fof(f4,axiom,
! [X0,X1] : big_p(term4,X0,X1) = times(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term4) ).
fof(f5,axiom,
! [X0,X1] : big_p(term5,X0,X1) = plus(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term5) ).
fof(f6,axiom,
! [X0,X1] : big_p(term6,X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_term6) ).
fof(f7,axiom,
! [X2,X0,X1] : big_t(X0,X1,X2) = big_p(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',big_p_and_big_t) ).
fof(f8,axiom,
term(term1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term1) ).
fof(f9,axiom,
term(term2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term2) ).
fof(f10,axiom,
term(term3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term3) ).
fof(f11,axiom,
term(term4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term4) ).
fof(f12,axiom,
term(term5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term5) ).
fof(f13,axiom,
term(term6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',term6) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(X0,big_p(X0,X1,X2),X3) = big_p(X0,X1,big_p(X0,X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q2) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X4] :
( ~ term(X0)
| big_p(X0,big_p(X0,X1,X2),big_p(X0,X3,X4)) = big_p(X0,big_p(X0,X1,X3),big_p(X0,X2,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q5) ).
fof(f16,axiom,
! [X2,X3,X0,X1,X4] :
( ~ term(X0)
| ~ term(X1)
| big_t(X0,big_p(X1,big_t(X0,X2,X3),X4),big_p(X1,X3,X4)) = big_p(X1,big_t(X0,X2,X3),X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',q3) ).
fof(f17,plain,
! [X2,X3,X0,X1,X4] :
( ~ term(X0)
| ~ term(X1)
| big_p(X1,big_t(X0,X2,X3),X4) = big_t(X0,big_p(X1,big_t(X0,X2,X3),X4),big_p(X1,X3,X4)) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
times(a,plus(b,times(d,times(c,e)))) != times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_q4) ).
fof(f19,plain,
! [X0,X1] : big_p(term4,X0,X1) = big_p(term3,X1,X0),
inference(definition_unfolding,[],[f4,f3]) ).
fof(f20,plain,
! [X0,X1] : big_p(term6,X0,X1) = big_p(term5,X1,X0),
inference(definition_unfolding,[],[f6,f5]) ).
fof(f21,plain,
! [X2,X3,X0,X1,X4] :
( ~ term(X1)
| ~ term(X0)
| big_p(X1,big_p(X0,X2,X3),X4) = big_p(X0,big_p(X1,big_p(X0,X2,X3),X4),big_p(X1,X3,X4)) ),
inference(definition_unfolding,[],[f17,f7,f7,f7]) ).
fof(f22,plain,
big_p(term3,a,big_p(term5,b,big_p(term3,d,big_p(term3,c,e)))) != big_p(term3,a,big_p(term5,b,big_p(term3,big_p(term5,b,c),big_p(term3,d,big_p(term3,c,e))))),
inference(definition_unfolding,[],[f18,f3,f5,f3,f3,f3,f5,f3,f5,f3,f3]) ).
fof(f23,definition,
sF0 = big_p(term3,c,e),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f24,plain,
big_p(term3,c,e) = sF0,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF1 = big_p(term3,d,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f26,plain,
big_p(term3,d,sF0) = sF1,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF2 = big_p(term5,b,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f28,plain,
big_p(term5,b,sF1) = sF2,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF3 = big_p(term3,a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f30,plain,
big_p(term3,a,sF2) = sF3,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF4 = big_p(term5,b,c),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f32,plain,
big_p(term5,b,c) = sF4,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF5 = big_p(term3,sF4,sF1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f34,plain,
big_p(term3,sF4,sF1) = sF5,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF6 = big_p(term5,b,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f36,plain,
big_p(term5,b,sF5) = sF6,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF7 = big_p(term3,a,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f38,plain,
big_p(term3,a,sF6) = sF7,
inference(reorient_equations,[],[f37]) ).
fof(f39,plain,
sF3 != sF7,
inference(definition_folding,[],[f22,f38,f36,f34,f26,f24,f32,f30,f28,f26,f24]) ).
fof(f40,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,X1),big_p(term5,X2,X3)) = big_p(term5,big_p(term5,X0,X2),big_p(term5,X1,X3)),
inference(resolution,[],[f12,f15]) ).
fof(f41,plain,
! [X2,X0,X1] : big_p(term5,big_p(term5,X0,X1),X2) = big_p(term5,X0,big_p(term5,X1,X2)),
inference(resolution,[],[f12,f14]) ).
fof(f42,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term5,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term5,big_p(X0,X1,X2),X3),big_p(term5,X2,X3)) ),
inference(resolution,[],[f12,f21]) ).
fof(f43,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,X1),big_p(term5,X2,X3)) = big_p(term5,X0,big_p(term5,X2,big_p(term5,X1,X3))),
inference(forward_demodulation,[],[f40,f41]) ).
fof(f44,plain,
! [X2,X3,X0,X1] : big_p(term5,X0,big_p(term5,X2,big_p(term5,X1,X3))) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,X3))),
inference(forward_demodulation,[],[f43,f41]) ).
fof(f45,plain,
! [X0] : big_p(term5,b,big_p(term5,c,X0)) = big_p(term5,sF4,X0),
inference(superposition,[],[f41,f32]) ).
fof(f46,plain,
! [X0] : big_p(term5,b,big_p(term5,sF1,X0)) = big_p(term5,sF2,X0),
inference(superposition,[],[f41,f28]) ).
fof(f47,plain,
! [X0] : big_p(term5,b,big_p(term5,sF5,X0)) = big_p(term5,sF6,X0),
inference(superposition,[],[f41,f36]) ).
fof(f61,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,b,big_p(term5,X1,c))) = big_p(term5,X0,big_p(term5,X1,sF4)),
inference(superposition,[],[f44,f32]) ).
fof(f62,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,b,big_p(term5,X1,sF1))) = big_p(term5,X0,big_p(term5,X1,sF2)),
inference(superposition,[],[f44,f28]) ).
fof(f63,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,b,big_p(term5,X1,sF5))) = big_p(term5,X0,big_p(term5,X1,sF6)),
inference(superposition,[],[f44,f36]) ).
fof(f93,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,X1),big_p(term3,X2,X3)) = big_p(term3,big_p(term3,X0,X2),big_p(term3,X1,X3)),
inference(resolution,[],[f10,f15]) ).
fof(f94,plain,
! [X2,X0,X1] : big_p(term3,big_p(term3,X0,X1),X2) = big_p(term3,X0,big_p(term3,X1,X2)),
inference(resolution,[],[f10,f14]) ).
fof(f95,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term3,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term3,big_p(X0,X1,X2),X3),big_p(term3,X2,X3)) ),
inference(resolution,[],[f10,f21]) ).
fof(f96,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,X1),big_p(term3,X2,X3)) = big_p(term3,X0,big_p(term3,X2,big_p(term3,X1,X3))),
inference(forward_demodulation,[],[f93,f94]) ).
fof(f97,plain,
! [X2,X3,X0,X1] : big_p(term3,X0,big_p(term3,X2,big_p(term3,X1,X3))) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,X3))),
inference(forward_demodulation,[],[f96,f94]) ).
fof(f99,plain,
! [X0] : big_p(term3,a,big_p(term3,sF2,X0)) = big_p(term3,sF3,X0),
inference(superposition,[],[f94,f30]) ).
fof(f100,plain,
! [X0] : big_p(term3,a,big_p(term3,sF6,X0)) = big_p(term3,sF7,X0),
inference(superposition,[],[f94,f38]) ).
fof(f101,plain,
! [X0] : big_p(term3,d,big_p(term3,sF0,X0)) = big_p(term3,sF1,X0),
inference(superposition,[],[f94,f26]) ).
fof(f102,plain,
! [X0] : big_p(term3,sF0,X0) = big_p(term3,c,big_p(term3,e,X0)),
inference(superposition,[],[f94,f24]) ).
fof(f103,plain,
! [X0] : big_p(term3,sF4,big_p(term3,sF1,X0)) = big_p(term3,sF5,X0),
inference(superposition,[],[f94,f34]) ).
fof(f121,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,a,big_p(term3,X1,sF2))) = big_p(term3,X0,big_p(term3,X1,sF3)),
inference(superposition,[],[f97,f30]) ).
fof(f122,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,a,big_p(term3,X1,sF6))) = big_p(term3,X0,big_p(term3,X1,sF7)),
inference(superposition,[],[f97,f38]) ).
fof(f123,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,d,big_p(term3,X1,sF0))) = big_p(term3,X0,big_p(term3,X1,sF1)),
inference(superposition,[],[f97,f26]) ).
fof(f124,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,c,big_p(term3,X1,e))) = big_p(term3,X0,big_p(term3,X1,sF0)),
inference(superposition,[],[f97,f24]) ).
fof(f125,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF4,big_p(term3,X1,sF1))) = big_p(term3,X0,big_p(term3,X1,sF5)),
inference(superposition,[],[f97,f34]) ).
fof(f152,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),X2) = big_p(term5,big_p(term3,big_p(term5,X0,X1),X2),big_p(term3,X1,X2)),
inference(resolution,[],[f95,f12]) ).
fof(f153,plain,
! [X2,X0,X1] : big_p(term3,big_p(term3,X0,X1),X2) = big_p(term3,big_p(term3,big_p(term3,X0,X1),X2),big_p(term3,X1,X2)),
inference(resolution,[],[f95,f10]) ).
fof(f154,plain,
! [X2,X0,X1] : big_p(term3,big_p(term3,X0,X1),X2) = big_p(term3,big_p(term3,X0,X1),big_p(term3,X2,big_p(term3,X1,X2))),
inference(forward_demodulation,[],[f153,f94]) ).
fof(f155,plain,
! [X2,X0,X1] : big_p(term3,big_p(term3,X0,X1),X2) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X1,X2)))),
inference(forward_demodulation,[],[f154,f94]) ).
fof(f156,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X1,X2)))),
inference(forward_demodulation,[],[f155,f94]) ).
fof(f161,plain,
! [X0] : big_p(term3,X0,sF3) = big_p(term3,X0,big_p(term3,a,big_p(term3,sF2,sF3))),
inference(superposition,[],[f156,f30]) ).
fof(f162,plain,
! [X0] : big_p(term3,X0,sF7) = big_p(term3,X0,big_p(term3,a,big_p(term3,sF6,sF7))),
inference(superposition,[],[f156,f38]) ).
fof(f163,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,d,big_p(term3,sF0,sF1))),
inference(superposition,[],[f156,f26]) ).
fof(f164,plain,
! [X0] : big_p(term3,X0,sF0) = big_p(term3,X0,big_p(term3,c,big_p(term3,e,sF0))),
inference(superposition,[],[f156,f24]) ).
fof(f165,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,sF4,big_p(term3,sF1,sF5))),
inference(superposition,[],[f156,f34]) ).
fof(f171,plain,
! [X2,X0,X1] : big_p(term3,X2,big_p(term3,X0,X1)) = big_p(term3,X2,big_p(term3,X0,big_p(term3,X0,big_p(term3,X1,X1)))),
inference(superposition,[],[f156,f97]) ).
fof(f177,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,X2,big_p(term3,X1,big_p(term3,X1,X2)))),
inference(superposition,[],[f97,f156]) ).
fof(f193,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,sF5,sF5)),
inference(forward_demodulation,[],[f165,f103]) ).
fof(f194,plain,
! [X0] : big_p(term3,X0,sF0) = big_p(term3,X0,big_p(term3,sF0,sF0)),
inference(forward_demodulation,[],[f164,f102]) ).
fof(f195,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,sF1,sF1)),
inference(forward_demodulation,[],[f163,f101]) ).
fof(f196,plain,
! [X0] : big_p(term3,X0,sF7) = big_p(term3,X0,big_p(term3,sF7,sF7)),
inference(forward_demodulation,[],[f162,f100]) ).
fof(f197,plain,
! [X0] : big_p(term3,X0,sF3) = big_p(term3,X0,big_p(term3,sF3,sF3)),
inference(forward_demodulation,[],[f161,f99]) ).
fof(f235,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,big_p(term3,sF5,sF5),X1)) = big_p(term3,big_p(term3,X0,sF5),X1),
inference(superposition,[],[f94,f193]) ).
fof(f238,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,big_p(term3,sF5,sF5),X1)) = big_p(term3,X0,big_p(term3,sF5,X1)),
inference(forward_demodulation,[],[f235,f94]) ).
fof(f243,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF5,X1)) = big_p(term3,X0,big_p(term3,sF5,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f238,f94]) ).
fof(f247,plain,
! [X0,X1] : big_p(term3,X1,big_p(term3,sF3,big_p(term3,X0,sF3))) = big_p(term3,X1,big_p(term3,X0,sF3)),
inference(superposition,[],[f97,f197]) ).
fof(f262,plain,
! [X0] : big_p(term3,sF4,X0) = big_p(term5,big_p(term3,sF4,X0),big_p(term3,c,X0)),
inference(superposition,[],[f152,f32]) ).
fof(f263,plain,
! [X0] : big_p(term3,sF2,X0) = big_p(term5,big_p(term3,sF2,X0),big_p(term3,sF1,X0)),
inference(superposition,[],[f152,f28]) ).
fof(f264,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term5,big_p(term3,sF6,X0),big_p(term3,sF5,X0)),
inference(superposition,[],[f152,f36]) ).
fof(f289,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,big_p(term5,X0,X1),X2),big_p(term5,big_p(term3,X1,X2),X3)) = big_p(term5,big_p(term3,big_p(term5,X0,X1),X2),X3),
inference(superposition,[],[f41,f152]) ).
fof(f342,plain,
! [X2,X0,X1] : big_p(term5,big_p(term5,X0,X1),X2) = big_p(term5,big_p(term5,big_p(term5,X0,X1),X2),big_p(term5,X1,X2)),
inference(resolution,[],[f42,f12]) ).
fof(f343,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term3,big_p(term5,big_p(term3,X0,X1),X2),big_p(term5,X1,X2)),
inference(resolution,[],[f42,f10]) ).
fof(f344,plain,
! [X2,X0,X1] : big_p(term5,big_p(term5,X0,X1),X2) = big_p(term5,big_p(term5,X0,X1),big_p(term5,X2,big_p(term5,X1,X2))),
inference(forward_demodulation,[],[f342,f41]) ).
fof(f345,plain,
! [X2,X0,X1] : big_p(term5,big_p(term5,X0,X1),X2) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,X2)))),
inference(forward_demodulation,[],[f344,f41]) ).
fof(f346,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,X2)))),
inference(forward_demodulation,[],[f345,f41]) ).
fof(f361,plain,
! [X2,X0,X1] : big_p(term5,X2,big_p(term5,X0,X1)) = big_p(term5,X2,big_p(term5,X0,big_p(term5,X0,big_p(term5,X1,X1)))),
inference(superposition,[],[f346,f44]) ).
fof(f366,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,X2,big_p(term5,X1,big_p(term5,X1,X2)))),
inference(superposition,[],[f44,f346]) ).
fof(f372,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,X2))),X3)),
inference(superposition,[],[f41,f346]) ).
fof(f375,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,big_p(term5,X2,big_p(term5,X1,X2)),X3))),
inference(forward_demodulation,[],[f372,f41]) ).
fof(f391,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,big_p(term5,X1,X2),X3)))),
inference(forward_demodulation,[],[f375,f41]) ).
fof(f396,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,big_p(term5,X2,X3))))),
inference(forward_demodulation,[],[f391,f41]) ).
fof(f398,plain,
! [X2,X3,X0,X1] : big_p(term5,X0,big_p(term5,big_p(term5,X1,X2),X3)) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,big_p(term5,X2,X3))))),
inference(forward_demodulation,[],[f396,f41]) ).
fof(f399,plain,
! [X2,X3,X0,X1] : big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,X3))) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,big_p(term5,X2,X3))))),
inference(forward_demodulation,[],[f398,f41]) ).
fof(f411,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term3,big_p(term5,sF7,X0),big_p(term5,sF6,X0)),
inference(superposition,[],[f343,f38]) ).
fof(f421,plain,
! [X0] : big_p(term5,big_p(term3,X0,b),sF5) = big_p(term3,big_p(term5,big_p(term3,X0,b),sF5),sF6),
inference(superposition,[],[f343,f36]) ).
fof(f427,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term5,big_p(term3,X0,X1),X2),big_p(term3,X2,big_p(term5,X1,X2))),
inference(superposition,[],[f152,f343]) ).
fof(f434,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term5,X2,big_p(term3,X2,big_p(term5,X1,X2)))),
inference(forward_demodulation,[],[f427,f41]) ).
fof(f581,plain,
! [X0] : big_p(term3,X0,big_p(term3,d,sF0)) = big_p(term3,X0,big_p(term3,sF0,sF1)),
inference(superposition,[],[f123,f194]) ).
fof(f609,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,sF0,sF1)),
inference(forward_demodulation,[],[f581,f26]) ).
fof(f631,plain,
big_p(term3,d,sF0) = big_p(term3,sF1,sF0),
inference(superposition,[],[f194,f101]) ).
fof(f649,plain,
sF1 = big_p(term3,sF1,sF0),
inference(forward_demodulation,[],[f631,f26]) ).
fof(f675,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF4,sF1)) = big_p(term3,X0,big_p(term3,sF1,sF5)),
inference(superposition,[],[f125,f195]) ).
fof(f705,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,sF1,sF5)),
inference(forward_demodulation,[],[f675,f34]) ).
fof(f712,plain,
big_p(term3,sF4,sF1) = big_p(term3,sF5,sF0),
inference(superposition,[],[f103,f649]) ).
fof(f729,plain,
big_p(term3,sF4,sF1) = big_p(term3,sF5,sF1),
inference(superposition,[],[f195,f103]) ).
fof(f731,plain,
! [X0,X1] : big_p(term3,X1,big_p(term3,sF1,big_p(term3,sF4,X0))) = big_p(term3,X1,big_p(term3,sF5,X0)),
inference(superposition,[],[f97,f103]) ).
fof(f733,plain,
! [X0,X1] : big_p(term3,sF4,big_p(term3,X0,big_p(term3,sF1,X1))) = big_p(term3,sF5,big_p(term3,X0,X1)),
inference(superposition,[],[f97,f103]) ).
fof(f747,plain,
sF5 = big_p(term3,sF5,sF1),
inference(forward_demodulation,[],[f729,f34]) ).
fof(f762,plain,
sF5 = big_p(term3,sF5,sF0),
inference(forward_demodulation,[],[f712,f34]) ).
fof(f774,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF5,sF5)) = big_p(term3,X0,big_p(term3,sF4,sF5)),
inference(superposition,[],[f125,f747]) ).
fof(f782,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,sF4,sF5)),
inference(forward_demodulation,[],[f774,f193]) ).
fof(f892,plain,
! [X0] : big_p(term5,X0,big_p(term5,c,sF6)) = big_p(term5,X0,big_p(term5,sF4,sF5)),
inference(superposition,[],[f63,f45]) ).
fof(f895,plain,
! [X0,X1] : big_p(term5,b,big_p(term5,X0,big_p(term5,c,X1))) = big_p(term5,sF4,big_p(term5,X0,X1)),
inference(superposition,[],[f44,f45]) ).
fof(f977,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF5,sF4)) = big_p(term5,X0,big_p(term5,sF6,c)),
inference(superposition,[],[f61,f47]) ).
fof(f979,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF5,sF2)) = big_p(term5,X0,big_p(term5,sF6,sF1)),
inference(superposition,[],[f62,f47]) ).
fof(f984,plain,
! [X0] : big_p(term5,b,big_p(term5,sF5,X0)) = big_p(term5,sF6,big_p(term5,X0,big_p(term5,sF5,X0))),
inference(superposition,[],[f346,f47]) ).
fof(f996,plain,
! [X0] : big_p(term5,sF6,X0) = big_p(term5,sF6,big_p(term5,X0,big_p(term5,sF5,X0))),
inference(forward_demodulation,[],[f984,f47]) ).
fof(f1102,plain,
! [X0,X1] : big_p(term3,a,big_p(term3,X0,big_p(term3,sF6,X1))) = big_p(term3,sF7,big_p(term3,X0,X1)),
inference(superposition,[],[f97,f100]) ).
fof(f1103,plain,
! [X0] : big_p(term3,a,big_p(term3,sF6,X0)) = big_p(term3,sF7,big_p(term3,X0,big_p(term3,sF6,X0))),
inference(superposition,[],[f156,f100]) ).
fof(f1110,plain,
! [X2,X0,X1] : big_p(term3,X1,big_p(term3,a,big_p(term3,X2,big_p(term3,sF6,X0)))) = big_p(term3,X1,big_p(term3,X2,big_p(term3,sF7,X0))),
inference(superposition,[],[f97,f100]) ).
fof(f1115,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,sF7,big_p(term3,X0,big_p(term3,sF6,X0))),
inference(forward_demodulation,[],[f1103,f100]) ).
fof(f1141,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF1),X1) = big_p(term3,X0,big_p(term3,big_p(term3,sF0,sF1),X1)),
inference(superposition,[],[f94,f609]) ).
fof(f1159,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF1),X1) = big_p(term3,X0,big_p(term3,sF0,big_p(term3,sF1,X1))),
inference(forward_demodulation,[],[f1141,f94]) ).
fof(f1165,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF1,X1)) = big_p(term3,X0,big_p(term3,sF0,big_p(term3,sF1,X1))),
inference(forward_demodulation,[],[f1159,f94]) ).
fof(f1177,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,big_p(term3,sF1,sF5),X1)),
inference(superposition,[],[f94,f705]) ).
fof(f1184,plain,
big_p(term3,sF5,sF5) = big_p(term3,sF4,sF5),
inference(superposition,[],[f103,f705]) ).
fof(f1193,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,sF1,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f1177,f94]) ).
fof(f1199,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF5,X1)) = big_p(term3,X0,big_p(term3,sF1,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f1193,f94]) ).
fof(f1219,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,big_p(term5,sF7,X0),big_p(term3,X0,big_p(term5,sF6,X0))),
inference(superposition,[],[f152,f411]) ).
fof(f1228,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,X0,big_p(term3,X0,big_p(term5,sF6,X0)))),
inference(forward_demodulation,[],[f1219,f41]) ).
fof(f1510,plain,
sF5 = big_p(term5,sF5,big_p(term3,c,sF1)),
inference(superposition,[],[f262,f34]) ).
fof(f1609,plain,
big_p(term3,sF6,sF1) = big_p(term5,big_p(term3,sF6,sF1),sF5),
inference(superposition,[],[f264,f747]) ).
fof(f1815,plain,
! [X0] : big_p(term3,sF5,big_p(term3,sF5,X0)) = big_p(term3,big_p(term3,sF4,sF5),X0),
inference(superposition,[],[f94,f1184]) ).
fof(f1816,plain,
! [X0] : big_p(term3,sF5,big_p(term3,sF5,X0)) = big_p(term3,sF4,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f1815,f94]) ).
fof(f1838,plain,
! [X2,X3,X0,X1] : big_p(term3,X2,big_p(term3,X3,big_p(term3,X0,X1))) = big_p(term3,X2,big_p(term3,X3,big_p(term3,X3,big_p(term3,X0,big_p(term3,X1,big_p(term3,X0,X1)))))),
inference(superposition,[],[f171,f94]) ).
fof(f1846,plain,
! [X0,X1] : big_p(term3,X1,big_p(term3,X0,sF7)) = big_p(term3,X1,big_p(term3,X0,big_p(term3,X0,sF7))),
inference(superposition,[],[f171,f196]) ).
fof(f1877,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),X3) = big_p(term3,X0,big_p(term3,big_p(term3,X1,big_p(term3,X1,big_p(term3,X2,X2))),X3)),
inference(superposition,[],[f94,f171]) ).
fof(f1914,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),X3) = big_p(term3,X0,big_p(term3,X1,big_p(term3,big_p(term3,X1,big_p(term3,X2,X2)),X3))),
inference(forward_demodulation,[],[f1877,f94]) ).
fof(f1943,plain,
! [X2,X3,X0,X1] : big_p(term3,X2,big_p(term3,X3,big_p(term3,X0,X1))) = big_p(term3,X2,big_p(term3,X3,big_p(term3,X3,big_p(term3,X0,X1)))),
inference(forward_demodulation,[],[f1838,f156]) ).
fof(f1964,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),X3) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X1,big_p(term3,big_p(term3,X2,X2),X3)))),
inference(forward_demodulation,[],[f1914,f94]) ).
fof(f2003,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),X3) = big_p(term3,X0,big_p(term3,X1,big_p(term3,big_p(term3,X2,X2),X3))),
inference(forward_demodulation,[],[f1964,f1943]) ).
fof(f2023,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),X3) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X2,X3)))),
inference(forward_demodulation,[],[f2003,f94]) ).
fof(f2038,plain,
! [X2,X3,X0,X1] : big_p(term3,X0,big_p(term3,big_p(term3,X1,X2),X3)) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X2,X3)))),
inference(forward_demodulation,[],[f2023,f94]) ).
fof(f2045,plain,
! [X2,X3,X0,X1] : big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,X3))) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X2,X3)))),
inference(forward_demodulation,[],[f2038,f94]) ).
fof(f2247,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,big_p(term3,sF4,sF5),X1)),
inference(superposition,[],[f94,f782]) ).
fof(f2274,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,sF4,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f2247,f94]) ).
fof(f2285,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF5,X1)) = big_p(term3,X0,big_p(term3,sF4,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f2274,f94]) ).
fof(f2357,plain,
big_p(term5,b,sF5) = big_p(term5,sF6,big_p(term3,c,sF1)),
inference(superposition,[],[f47,f1510]) ).
fof(f2359,plain,
! [X0] : big_p(term5,X0,sF5) = big_p(term5,X0,big_p(term5,sF5,big_p(term5,big_p(term3,c,sF1),sF5))),
inference(superposition,[],[f346,f1510]) ).
fof(f2363,plain,
! [X0] : big_p(term5,sF5,X0) = big_p(term5,sF5,big_p(term5,big_p(term3,c,sF1),X0)),
inference(superposition,[],[f41,f1510]) ).
fof(f2365,plain,
! [X0] : big_p(term5,X0,sF5) = big_p(term5,X0,big_p(term5,sF5,sF5)),
inference(forward_demodulation,[],[f2359,f2363]) ).
fof(f2366,plain,
sF6 = big_p(term5,sF6,big_p(term3,c,sF1)),
inference(forward_demodulation,[],[f2357,f36]) ).
fof(f2377,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,big_p(term5,sF5,sF5),X1)) = big_p(term5,big_p(term5,X0,sF5),X1),
inference(superposition,[],[f41,f2365]) ).
fof(f2380,plain,
big_p(term5,b,sF5) = big_p(term5,sF6,sF5),
inference(superposition,[],[f47,f2365]) ).
fof(f2381,plain,
! [X0] : big_p(term5,X0,big_p(term5,b,sF5)) = big_p(term5,X0,big_p(term5,sF5,sF6)),
inference(superposition,[],[f63,f2365]) ).
fof(f2408,plain,
! [X0] : big_p(term5,X0,sF6) = big_p(term5,X0,big_p(term5,sF5,sF6)),
inference(forward_demodulation,[],[f2381,f36]) ).
fof(f2409,plain,
sF6 = big_p(term5,sF6,sF5),
inference(forward_demodulation,[],[f2380,f36]) ).
fof(f2412,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,sF5,X1)) = big_p(term5,X0,big_p(term5,big_p(term5,sF5,sF5),X1)),
inference(forward_demodulation,[],[f2377,f41]) ).
fof(f2419,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,sF5,X1)) = big_p(term5,X0,big_p(term5,sF5,big_p(term5,sF5,X1))),
inference(forward_demodulation,[],[f2412,f41]) ).
fof(f2428,plain,
! [X0] : big_p(term5,sF6,X0) = big_p(term5,sF6,big_p(term5,sF5,X0)),
inference(superposition,[],[f41,f2409]) ).
fof(f2444,plain,
big_p(term5,sF6,sF6) = big_p(term5,b,sF6),
inference(superposition,[],[f47,f2408]) ).
fof(f2536,plain,
! [X0] : big_p(term5,b,big_p(term5,sF6,X0)) = big_p(term5,big_p(term5,sF6,sF6),X0),
inference(superposition,[],[f41,f2444]) ).
fof(f2537,plain,
! [X0] : big_p(term5,b,big_p(term5,sF6,X0)) = big_p(term5,sF6,big_p(term5,sF6,X0)),
inference(forward_demodulation,[],[f2536,f41]) ).
fof(f2554,plain,
! [X2,X3,X0,X1] : big_p(term5,X2,big_p(term5,X3,big_p(term5,X0,X1))) = big_p(term5,X2,big_p(term5,X3,big_p(term5,X3,big_p(term5,X0,big_p(term5,X1,big_p(term5,X0,X1)))))),
inference(superposition,[],[f361,f41]) ).
fof(f2585,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,big_p(term5,X1,big_p(term5,X1,big_p(term5,X2,X2))),X3)),
inference(superposition,[],[f41,f361]) ).
fof(f2622,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,big_p(term5,X1,big_p(term5,X2,X2)),X3))),
inference(forward_demodulation,[],[f2585,f41]) ).
fof(f2644,plain,
! [X2,X3,X0,X1] : big_p(term5,X2,big_p(term5,X3,big_p(term5,X0,X1))) = big_p(term5,X2,big_p(term5,X3,big_p(term5,X3,big_p(term5,X0,X1)))),
inference(forward_demodulation,[],[f2554,f346]) ).
fof(f2659,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X1,big_p(term5,big_p(term5,X2,X2),X3)))),
inference(forward_demodulation,[],[f2622,f41]) ).
fof(f2688,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,big_p(term5,X2,X2),X3))),
inference(forward_demodulation,[],[f2659,f2644]) ).
fof(f2704,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),X3) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X2,X3)))),
inference(forward_demodulation,[],[f2688,f41]) ).
fof(f2715,plain,
! [X2,X3,X0,X1] : big_p(term5,X0,big_p(term5,big_p(term5,X1,X2),X3)) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X2,X3)))),
inference(forward_demodulation,[],[f2704,f41]) ).
fof(f2719,plain,
! [X2,X3,X0,X1] : big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,X3))) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X2,X3)))),
inference(forward_demodulation,[],[f2715,f41]) ).
fof(f2870,plain,
! [X2,X3,X0,X1] : big_p(term3,X3,big_p(term3,X2,big_p(term3,X0,X1))) = big_p(term3,X3,big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X2,big_p(term3,X0,X1)))))),
inference(superposition,[],[f177,f94]) ).
fof(f2888,plain,
! [X2,X3,X0,X1] : big_p(term3,X3,big_p(term3,X0,big_p(term3,X1,X2))) = big_p(term3,X3,big_p(term3,X2,big_p(term3,X0,big_p(term3,X1,big_p(term3,X1,X2))))),
inference(superposition,[],[f97,f177]) ).
fof(f2939,plain,
! [X2,X3,X0,X1] : big_p(term3,X3,big_p(term3,X0,big_p(term3,X1,X2))) = big_p(term3,X3,big_p(term3,X2,big_p(term3,X0,big_p(term3,X1,X2)))),
inference(forward_demodulation,[],[f2888,f2045]) ).
fof(f2947,plain,
! [X2,X3,X0,X1] : big_p(term3,X3,big_p(term3,X2,big_p(term3,X0,X1))) = big_p(term3,X3,big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X0,X1))))),
inference(forward_demodulation,[],[f2870,f2045]) ).
fof(f3018,plain,
! [X2,X3,X0,X1] : big_p(term3,X3,big_p(term3,X2,big_p(term3,X0,X1))) = big_p(term3,X3,big_p(term3,X0,big_p(term3,X2,big_p(term3,X0,X1)))),
inference(forward_demodulation,[],[f2947,f2939]) ).
fof(f3222,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term1,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term1,big_p(X0,X1,X2),X3),big_p(term1,X2,X3)) ),
inference(resolution,[],[f8,f21]) ).
fof(f3223,plain,
! [X2,X3,X0,X1] :
( big_p(term1,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term1,big_p(X0,X1,X2),X3),X2)
| ~ term(X0) ),
inference(forward_demodulation,[],[f3222,f1]) ).
fof(f3226,plain,
! [X2,X0,X1] :
( ~ term(X0)
| big_p(X0,X1,X2) = big_p(X0,big_p(X0,X1,X2),X2) ),
inference(forward_demodulation,[],[f3223,f1]) ).
fof(f3230,plain,
! [X0,X1] : big_p(term5,X0,X1) = big_p(term5,big_p(term5,X0,X1),X1),
inference(resolution,[],[f3226,f12]) ).
fof(f3231,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,big_p(term3,X0,X1),X1),
inference(resolution,[],[f3226,f10]) ).
fof(f3233,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,X0,big_p(term3,X1,X1)),
inference(forward_demodulation,[],[f3231,f94]) ).
fof(f3234,plain,
! [X0,X1] : big_p(term5,X0,X1) = big_p(term5,X0,big_p(term5,X1,X1)),
inference(forward_demodulation,[],[f3230,f41]) ).
fof(f3273,plain,
! [X2,X0,X1] : big_p(term3,X2,big_p(term3,X0,X1)) = big_p(term3,X2,big_p(term3,X1,big_p(term3,X0,X1))),
inference(superposition,[],[f97,f3233]) ).
fof(f3288,plain,
big_p(term3,a,sF2) = big_p(term3,sF3,sF2),
inference(superposition,[],[f99,f3233]) ).
fof(f3289,plain,
big_p(term3,a,sF6) = big_p(term3,sF7,sF6),
inference(superposition,[],[f100,f3233]) ).
fof(f3290,plain,
! [X0] : big_p(term3,X0,big_p(term3,a,sF2)) = big_p(term3,X0,big_p(term3,sF2,sF3)),
inference(superposition,[],[f121,f3233]) ).
fof(f3291,plain,
! [X0] : big_p(term3,X0,big_p(term3,a,sF6)) = big_p(term3,X0,big_p(term3,sF6,sF7)),
inference(superposition,[],[f122,f3233]) ).
fof(f3294,plain,
big_p(term3,c,e) = big_p(term3,sF0,e),
inference(superposition,[],[f102,f3233]) ).
fof(f3321,plain,
sF0 = big_p(term3,sF0,e),
inference(forward_demodulation,[],[f3294,f24]) ).
fof(f3324,plain,
! [X0] : big_p(term3,X0,sF7) = big_p(term3,X0,big_p(term3,sF6,sF7)),
inference(forward_demodulation,[],[f3291,f38]) ).
fof(f3325,plain,
! [X0] : big_p(term3,X0,sF3) = big_p(term3,X0,big_p(term3,sF2,sF3)),
inference(forward_demodulation,[],[f3290,f30]) ).
fof(f3326,plain,
sF7 = big_p(term3,sF7,sF6),
inference(forward_demodulation,[],[f3289,f38]) ).
fof(f3327,plain,
sF3 = big_p(term3,sF3,sF2),
inference(forward_demodulation,[],[f3288,f30]) ).
fof(f3448,plain,
! [X2,X0,X1] : big_p(term5,X2,big_p(term5,X0,X1)) = big_p(term5,X2,big_p(term5,X1,big_p(term5,X0,X1))),
inference(superposition,[],[f44,f3234]) ).
fof(f3463,plain,
! [X0] : big_p(term5,X0,big_p(term5,b,sF1)) = big_p(term5,X0,big_p(term5,sF1,sF2)),
inference(superposition,[],[f62,f3234]) ).
fof(f3464,plain,
big_p(term5,b,c) = big_p(term5,sF4,c),
inference(superposition,[],[f45,f3234]) ).
fof(f3465,plain,
big_p(term5,b,sF1) = big_p(term5,sF2,sF1),
inference(superposition,[],[f46,f3234]) ).
fof(f3493,plain,
sF2 = big_p(term5,sF2,sF1),
inference(forward_demodulation,[],[f3465,f28]) ).
fof(f3494,plain,
sF4 = big_p(term5,sF4,c),
inference(forward_demodulation,[],[f3464,f32]) ).
fof(f3495,plain,
! [X0] : big_p(term5,X0,sF2) = big_p(term5,X0,big_p(term5,sF1,sF2)),
inference(forward_demodulation,[],[f3463,f28]) ).
fof(f3553,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF3,sF3)) = big_p(term3,X0,big_p(term3,a,sF3)),
inference(superposition,[],[f121,f3327]) ).
fof(f3554,plain,
! [X0] : big_p(term3,sF3,X0) = big_p(term3,sF3,big_p(term3,sF2,X0)),
inference(superposition,[],[f94,f3327]) ).
fof(f3563,plain,
! [X0] : big_p(term3,X0,sF3) = big_p(term3,X0,big_p(term3,a,sF3)),
inference(forward_demodulation,[],[f3553,f197]) ).
fof(f3564,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF7,sF7)) = big_p(term3,X0,big_p(term3,a,sF7)),
inference(superposition,[],[f122,f3326]) ).
fof(f3574,plain,
! [X0] : big_p(term3,X0,sF7) = big_p(term3,X0,big_p(term3,a,sF7)),
inference(forward_demodulation,[],[f3564,f196]) ).
fof(f3575,plain,
big_p(term3,d,sF0) = big_p(term3,sF1,e),
inference(superposition,[],[f101,f3321]) ).
fof(f3587,plain,
sF1 = big_p(term3,sF1,e),
inference(forward_demodulation,[],[f3575,f26]) ).
fof(f3591,plain,
big_p(term3,sF4,sF1) = big_p(term3,sF5,e),
inference(superposition,[],[f103,f3587]) ).
fof(f3592,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF1,sF0)) = big_p(term3,X0,big_p(term3,c,sF1)),
inference(superposition,[],[f124,f3587]) ).
fof(f3598,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,e,big_p(term3,sF1,sF1))),
inference(superposition,[],[f177,f3587]) ).
fof(f3600,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,e,sF1)),
inference(forward_demodulation,[],[f3598,f195]) ).
fof(f3602,plain,
! [X0] : big_p(term3,X0,sF1) = big_p(term3,X0,big_p(term3,c,sF1)),
inference(forward_demodulation,[],[f3592,f649]) ).
fof(f3603,plain,
sF5 = big_p(term3,sF5,e),
inference(forward_demodulation,[],[f3591,f34]) ).
fof(f3605,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF5,sF0)) = big_p(term3,X0,big_p(term3,c,sF5)),
inference(superposition,[],[f124,f3603]) ).
fof(f3611,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,e,big_p(term3,sF5,sF5))),
inference(superposition,[],[f177,f3603]) ).
fof(f3613,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,e,sF5)),
inference(forward_demodulation,[],[f3611,f193]) ).
fof(f3615,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term3,c,sF5)),
inference(forward_demodulation,[],[f3605,f762]) ).
fof(f3621,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,X1,sF4)) = big_p(term5,X0,big_p(term5,sF4,big_p(term5,X1,c))),
inference(superposition,[],[f44,f3494]) ).
fof(f3622,plain,
! [X0] : big_p(term5,sF4,X0) = big_p(term5,sF4,big_p(term5,c,X0)),
inference(superposition,[],[f41,f3494]) ).
fof(f3632,plain,
! [X0,X1] : big_p(term5,X0,big_p(term5,X1,sF2)) = big_p(term5,X0,big_p(term5,sF2,big_p(term5,X1,sF1))),
inference(superposition,[],[f44,f3493]) ).
fof(f3640,plain,
! [X0,X1] : big_p(term5,X1,big_p(term5,X0,sF2)) = big_p(term5,X1,big_p(term5,sF1,big_p(term5,X0,sF2))),
inference(superposition,[],[f44,f3495]) ).
fof(f3708,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF1),X1) = big_p(term3,X0,big_p(term3,big_p(term3,c,sF1),X1)),
inference(superposition,[],[f94,f3602]) ).
fof(f3748,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF1),X1) = big_p(term3,X0,big_p(term3,c,big_p(term3,sF1,X1))),
inference(forward_demodulation,[],[f3708,f94]) ).
fof(f3760,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF1,X1)) = big_p(term3,X0,big_p(term3,c,big_p(term3,sF1,X1))),
inference(forward_demodulation,[],[f3748,f94]) ).
fof(f3780,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,big_p(term3,c,sF5),X1)),
inference(superposition,[],[f94,f3615]) ).
fof(f3818,plain,
! [X0,X1] : big_p(term3,big_p(term3,X0,sF5),X1) = big_p(term3,X0,big_p(term3,c,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f3780,f94]) ).
fof(f3828,plain,
! [X0,X1] : big_p(term3,X0,big_p(term3,sF5,X1)) = big_p(term3,X0,big_p(term3,c,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f3818,f94]) ).
fof(f3858,plain,
big_p(term3,sF3,sF3) = big_p(term3,a,sF3),
inference(superposition,[],[f99,f3325]) ).
fof(f3927,plain,
big_p(term3,sF7,sF7) = big_p(term3,a,sF7),
inference(superposition,[],[f100,f3324]) ).
fof(f4094,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF7,X0)) = big_p(term3,big_p(term3,a,sF7),X0),
inference(superposition,[],[f94,f3927]) ).
fof(f4105,plain,
! [X0] : big_p(term3,a,big_p(term3,sF7,X0)) = big_p(term3,sF7,big_p(term3,sF7,X0)),
inference(forward_demodulation,[],[f4094,f94]) ).
fof(f4260,plain,
big_p(term3,sF0,sF5) = big_p(term3,c,sF5),
inference(superposition,[],[f102,f3613]) ).
fof(f4313,plain,
! [X0] : big_p(term3,c,big_p(term3,sF5,X0)) = big_p(term3,big_p(term3,sF0,sF5),X0),
inference(superposition,[],[f94,f4260]) ).
fof(f4324,plain,
! [X0] : big_p(term3,c,big_p(term3,sF5,X0)) = big_p(term3,sF0,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f4313,f94]) ).
fof(f4344,plain,
big_p(term3,sF0,sF1) = big_p(term3,c,sF1),
inference(superposition,[],[f102,f3600]) ).
fof(f4353,plain,
big_p(term3,sF4,sF1) = big_p(term5,big_p(term3,sF4,sF1),big_p(term3,c,big_p(term3,e,sF1))),
inference(superposition,[],[f262,f3600]) ).
fof(f4360,plain,
big_p(term3,sF4,sF1) = big_p(term5,big_p(term3,sF4,sF1),big_p(term3,sF0,sF1)),
inference(forward_demodulation,[],[f4353,f102]) ).
fof(f4385,plain,
sF5 = big_p(term5,sF5,big_p(term3,sF0,sF1)),
inference(forward_demodulation,[],[f4360,f34]) ).
fof(f4401,plain,
big_p(term5,b,sF5) = big_p(term5,sF6,big_p(term3,sF0,sF1)),
inference(superposition,[],[f47,f4385]) ).
fof(f4410,plain,
sF6 = big_p(term5,sF6,big_p(term3,sF0,sF1)),
inference(forward_demodulation,[],[f4401,f36]) ).
fof(f4414,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term5,big_p(term3,sF6,X0),big_p(term3,big_p(term3,sF0,sF1),X0)),
inference(superposition,[],[f152,f4410]) ).
fof(f4418,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term5,big_p(term3,sF6,X0),big_p(term3,sF0,big_p(term3,sF1,X0))),
inference(forward_demodulation,[],[f4414,f94]) ).
fof(f4424,plain,
! [X0] : big_p(term3,c,big_p(term3,sF1,X0)) = big_p(term3,big_p(term3,sF0,sF1),X0),
inference(superposition,[],[f94,f4344]) ).
fof(f4435,plain,
! [X0] : big_p(term3,c,big_p(term3,sF1,X0)) = big_p(term3,sF0,big_p(term3,sF1,X0)),
inference(forward_demodulation,[],[f4424,f94]) ).
fof(f5242,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,sF7,big_p(term3,X0,sF6)),
inference(superposition,[],[f100,f3273]) ).
fof(f5540,plain,
! [X2,X3,X0,X1] : big_p(term5,X3,big_p(term5,X2,big_p(term5,X0,X1))) = big_p(term5,X3,big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X2,big_p(term5,X0,X1)))))),
inference(superposition,[],[f366,f41]) ).
fof(f5554,plain,
! [X2,X3,X0,X1] : big_p(term5,X3,big_p(term5,X0,big_p(term5,X1,X2))) = big_p(term5,X3,big_p(term5,X2,big_p(term5,X0,big_p(term5,X1,big_p(term5,X1,X2))))),
inference(superposition,[],[f44,f366]) ).
fof(f5609,plain,
! [X2,X3,X0,X1] : big_p(term5,X3,big_p(term5,X0,big_p(term5,X1,X2))) = big_p(term5,X3,big_p(term5,X2,big_p(term5,X0,big_p(term5,X1,X2)))),
inference(forward_demodulation,[],[f5554,f2719]) ).
fof(f5619,plain,
! [X2,X3,X0,X1] : big_p(term5,X3,big_p(term5,X2,big_p(term5,X0,X1))) = big_p(term5,X3,big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X0,X1))))),
inference(forward_demodulation,[],[f5540,f2719]) ).
fof(f5680,plain,
! [X2,X3,X0,X1] : big_p(term5,X3,big_p(term5,X2,big_p(term5,X0,X1))) = big_p(term5,X3,big_p(term5,X0,big_p(term5,X2,big_p(term5,X0,X1)))),
inference(forward_demodulation,[],[f5619,f5609]) ).
fof(f5787,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term2,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term2,big_p(X0,X1,X2),X3),big_p(term2,X2,X3)) ),
inference(resolution,[],[f9,f21]) ).
fof(f5788,plain,
! [X2,X3,X0,X1] :
( big_p(term2,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term2,big_p(X0,X1,X2),X3),X3)
| ~ term(X0) ),
inference(forward_demodulation,[],[f5787,f2]) ).
fof(f5794,plain,
! [X3,X0] :
( ~ term(X0)
| big_p(X0,X3,X3) = X3 ),
inference(forward_demodulation,[],[f5788,f2]) ).
fof(f5800,plain,
! [X0] : big_p(term3,X0,X0) = X0,
inference(resolution,[],[f5794,f10]) ).
fof(f5801,plain,
! [X0] : big_p(term5,X0,X0) = X0,
inference(resolution,[],[f5794,f12]) ).
fof(f5840,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,X0,big_p(term3,X0,X1)),
inference(superposition,[],[f94,f5800]) ).
fof(f5845,plain,
! [X0,X1] : big_p(term3,big_p(term5,X1,X0),X0) = big_p(term5,big_p(term3,big_p(term5,X1,X0),X0),X0),
inference(superposition,[],[f152,f5800]) ).
fof(f5859,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,big_p(term3,X0,big_p(term3,X1,X2)),big_p(term3,X1,big_p(term3,X0,X2))),
inference(superposition,[],[f97,f5800]) ).
fof(f5867,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,big_p(term3,a,big_p(term3,X0,sF6)),big_p(term3,X0,sF7)),
inference(superposition,[],[f122,f5800]) ).
fof(f5896,plain,
! [X0,X1] : big_p(term5,X0,X1) = big_p(term5,big_p(term5,X0,X1),big_p(term3,X1,big_p(term5,X0,X1))),
inference(superposition,[],[f152,f5800]) ).
fof(f5904,plain,
sF3 = big_p(term3,a,sF3),
inference(superposition,[],[f3858,f5800]) ).
fof(f5906,plain,
sF5 = big_p(term3,sF4,sF5),
inference(superposition,[],[f1184,f5800]) ).
fof(f5910,plain,
sF7 = big_p(term3,a,sF7),
inference(superposition,[],[f3927,f5800]) ).
fof(f5916,plain,
! [X0,X1] : big_p(term5,X0,X1) = big_p(term5,X0,big_p(term5,X1,big_p(term3,X1,big_p(term5,X0,X1)))),
inference(forward_demodulation,[],[f5896,f41]) ).
fof(f5945,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,a,big_p(term3,big_p(term3,X0,sF6),big_p(term3,X0,sF7))),
inference(forward_demodulation,[],[f5867,f94]) ).
fof(f5953,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,big_p(term3,X1,X2),big_p(term3,X1,big_p(term3,X0,X2)))),
inference(forward_demodulation,[],[f5859,f94]) ).
fof(f6004,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,a,big_p(term3,X0,big_p(term3,sF6,big_p(term3,X0,sF7)))),
inference(forward_demodulation,[],[f5945,f94]) ).
fof(f6011,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X2,big_p(term3,X1,big_p(term3,X0,X2))))),
inference(forward_demodulation,[],[f5953,f94]) ).
fof(f6035,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,sF7,big_p(term3,X0,big_p(term3,X0,sF7))),
inference(forward_demodulation,[],[f6004,f1102]) ).
fof(f6042,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,X2,big_p(term3,X1,big_p(term3,X0,X2)))),
inference(forward_demodulation,[],[f6011,f3018]) ).
fof(f6061,plain,
! [X0] : big_p(term3,sF7,big_p(term3,X0,sF7)) = big_p(term3,a,big_p(term3,X0,sF6)),
inference(forward_demodulation,[],[f6035,f1846]) ).
fof(f6068,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term3,X1,X2)) = big_p(term3,X0,big_p(term3,X1,big_p(term3,X0,X2))),
inference(forward_demodulation,[],[f6042,f2939]) ).
fof(f6113,plain,
! [X0,X1] : big_p(term5,X0,X1) = big_p(term5,X0,big_p(term5,X0,X1)),
inference(superposition,[],[f41,f5801]) ).
fof(f6117,plain,
! [X0,X1] : big_p(term5,big_p(term3,X1,X0),X0) = big_p(term3,big_p(term5,big_p(term3,X1,X0),X0),X0),
inference(superposition,[],[f343,f5801]) ).
fof(f6125,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,big_p(term5,X0,big_p(term5,X1,X2)),big_p(term5,X1,big_p(term5,X0,X2))),
inference(superposition,[],[f44,f5801]) ).
fof(f6145,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,big_p(term3,X0,X1),big_p(term5,X1,big_p(term3,X0,X1))),
inference(superposition,[],[f343,f5801]) ).
fof(f6162,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,X0,big_p(term3,X1,big_p(term5,X1,big_p(term3,X0,X1)))),
inference(forward_demodulation,[],[f6145,f94]) ).
fof(f6182,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,big_p(term5,X1,X2),big_p(term5,X1,big_p(term5,X0,X2)))),
inference(forward_demodulation,[],[f6125,f41]) ).
fof(f6216,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X2,big_p(term5,X1,big_p(term5,X0,X2))))),
inference(forward_demodulation,[],[f6182,f41]) ).
fof(f6233,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,X2,big_p(term5,X1,big_p(term5,X0,X2)))),
inference(forward_demodulation,[],[f6216,f5680]) ).
fof(f6249,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term5,X1,X2)) = big_p(term5,X0,big_p(term5,X1,big_p(term5,X0,X2))),
inference(forward_demodulation,[],[f6233,f5609]) ).
fof(f6267,plain,
! [X0] : big_p(term3,sF3,X0) = big_p(term3,a,big_p(term3,sF3,X0)),
inference(superposition,[],[f94,f5904]) ).
fof(f6279,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,a,big_p(term3,sF7,X0)),
inference(superposition,[],[f94,f5910]) ).
fof(f6355,plain,
! [X0] : big_p(term3,sF5,X0) = big_p(term3,sF4,big_p(term3,sF5,X0)),
inference(superposition,[],[f5840,f103]) ).
fof(f6392,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF2)) = big_p(term3,a,big_p(term3,X0,sF3)),
inference(superposition,[],[f121,f5840]) ).
fof(f6524,plain,
sF4 = big_p(term5,b,sF4),
inference(superposition,[],[f6113,f32]) ).
fof(f9031,plain,
! [X2,X0,X1] : big_p(term3,X2,big_p(term5,big_p(term3,X0,X1),X1)) = big_p(term3,X2,big_p(term3,X1,big_p(term5,big_p(term3,X0,X1),X1))),
inference(superposition,[],[f3273,f6117]) ).
fof(f9406,plain,
! [X2,X0,X1] : big_p(term5,X2,big_p(term3,big_p(term5,X0,X1),X1)) = big_p(term5,X2,big_p(term5,X1,big_p(term3,big_p(term5,X0,X1),X1))),
inference(superposition,[],[f3448,f5845]) ).
fof(f10074,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term6,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term6,big_p(X0,X1,X2),X3),big_p(term6,X2,X3)) ),
inference(resolution,[],[f13,f21]) ).
fof(f10076,plain,
! [X2,X0,X1] : big_p(term3,big_p(term6,X0,X1),X2) = big_p(term6,big_p(term3,big_p(term6,X0,X1),X2),big_p(term3,X1,X2)),
inference(resolution,[],[f13,f95]) ).
fof(f10081,plain,
! [X2,X0,X1] : big_p(term3,big_p(term6,X0,X1),X2) = big_p(term5,big_p(term3,X1,X2),big_p(term3,big_p(term6,X0,X1),X2)),
inference(forward_demodulation,[],[f10076,f20]) ).
fof(f10083,plain,
! [X2,X3,X0,X1] :
( big_p(term6,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term6,big_p(X0,X1,X2),X3),big_p(term5,X3,X2))
| ~ term(X0) ),
inference(forward_demodulation,[],[f10074,f20]) ).
fof(f10087,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X1,X0),X2) = big_p(term5,big_p(term3,X1,X2),big_p(term3,big_p(term5,X1,X0),X2)),
inference(forward_demodulation,[],[f10081,f20]) ).
fof(f10089,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term5,X3,big_p(X0,X1,X2)) = big_p(X0,big_p(term5,X3,big_p(X0,X1,X2)),big_p(term5,X3,X2)) ),
inference(forward_demodulation,[],[f10083,f20]) ).
fof(f10105,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term3,X1,X2)) = big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),big_p(term5,X0,X2)),
inference(resolution,[],[f10089,f10]) ).
fof(f10202,plain,
! [X0] : big_p(term5,X0,sF7) = big_p(term3,big_p(term5,X0,sF7),big_p(term5,X0,sF6)),
inference(superposition,[],[f10105,f3326]) ).
fof(f10205,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,big_p(term3,X0,X1),big_p(term5,big_p(term3,X0,X1),X1)),
inference(superposition,[],[f10105,f5801]) ).
fof(f10215,plain,
sF6 = big_p(term3,sF6,big_p(term5,sF6,sF1)),
inference(superposition,[],[f10105,f2366]) ).
fof(f10251,plain,
! [X0] : big_p(term5,b,big_p(term3,X0,sF1)) = big_p(term3,big_p(term5,b,big_p(term3,X0,sF1)),sF2),
inference(superposition,[],[f10105,f28]) ).
fof(f10254,plain,
! [X0] : big_p(term5,b,big_p(term3,X0,sF5)) = big_p(term3,big_p(term5,b,big_p(term3,X0,sF5)),sF6),
inference(superposition,[],[f10105,f36]) ).
fof(f10266,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),X3) = big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),big_p(term3,big_p(term5,X0,X2),X3)),
inference(superposition,[],[f94,f10105]) ).
fof(f10313,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,X0,big_p(term3,X1,big_p(term5,big_p(term3,X0,X1),X1))),
inference(forward_demodulation,[],[f10205,f94]) ).
fof(f10350,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,X0,big_p(term5,big_p(term3,X0,X1),X1)),
inference(forward_demodulation,[],[f10313,f9031]) ).
fof(f10433,plain,
! [X0] : big_p(term3,big_p(term5,sF4,X0),sF1) = big_p(term5,sF5,big_p(term3,big_p(term5,sF4,X0),sF1)),
inference(superposition,[],[f10087,f34]) ).
fof(f10445,plain,
! [X0] : big_p(term3,big_p(term5,sF5,X0),sF1) = big_p(term5,sF5,big_p(term3,big_p(term5,sF5,X0),sF1)),
inference(superposition,[],[f10087,f747]) ).
fof(f10486,plain,
! [X0] : big_p(term3,sF2,X0) = big_p(term5,big_p(term3,b,X0),big_p(term3,sF2,X0)),
inference(superposition,[],[f10087,f28]) ).
fof(f10488,plain,
! [X0] : big_p(term3,sF4,X0) = big_p(term5,big_p(term3,b,X0),big_p(term3,sF4,X0)),
inference(superposition,[],[f10087,f6524]) ).
fof(f10489,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term5,big_p(term3,b,X0),big_p(term3,sF6,X0)),
inference(superposition,[],[f10087,f36]) ).
fof(f10547,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),X2) = big_p(term3,big_p(term3,big_p(term5,X0,X1),X2),big_p(term5,big_p(term3,X0,X2),X2)),
inference(superposition,[],[f10105,f10087]) ).
fof(f10566,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),X2) = big_p(term3,big_p(term5,X0,X1),big_p(term3,X2,big_p(term5,big_p(term3,X0,X2),X2))),
inference(forward_demodulation,[],[f10547,f94]) ).
fof(f10653,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),X2) = big_p(term3,big_p(term5,X0,X1),big_p(term5,big_p(term3,X0,X2),X2)),
inference(forward_demodulation,[],[f10566,f9031]) ).
fof(f10748,plain,
! [X0] : big_p(term3,sF2,X0) = big_p(term3,big_p(term3,sF2,X0),big_p(term5,big_p(term3,b,X0),X0)),
inference(superposition,[],[f10105,f10486]) ).
fof(f10769,plain,
! [X0] : big_p(term3,sF2,X0) = big_p(term3,sF2,big_p(term3,X0,big_p(term5,big_p(term3,b,X0),X0))),
inference(forward_demodulation,[],[f10748,f94]) ).
fof(f10836,plain,
! [X0] : big_p(term3,sF2,X0) = big_p(term3,sF2,big_p(term5,big_p(term3,b,X0),X0)),
inference(forward_demodulation,[],[f10769,f9031]) ).
fof(f10921,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term3,big_p(term3,sF6,X0),big_p(term5,big_p(term3,b,X0),X0)),
inference(superposition,[],[f10105,f10489]) ).
fof(f10942,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term3,sF6,big_p(term3,X0,big_p(term5,big_p(term3,b,X0),X0))),
inference(forward_demodulation,[],[f10921,f94]) ).
fof(f11009,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term3,sF6,big_p(term5,big_p(term3,b,X0),X0)),
inference(forward_demodulation,[],[f10942,f9031]) ).
fof(f11092,plain,
sF7 = big_p(term3,a,big_p(term5,sF7,sF6)),
inference(superposition,[],[f10350,f38]) ).
fof(f11128,plain,
sF7 = big_p(term3,sF7,big_p(term5,sF7,sF6)),
inference(superposition,[],[f10350,f3326]) ).
fof(f12553,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term4,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term4,big_p(X0,X1,X2),X3),big_p(term4,X2,X3)) ),
inference(resolution,[],[f11,f21]) ).
fof(f12554,plain,
! [X2,X0,X1] : big_p(term5,big_p(term4,X0,X1),X2) = big_p(term4,big_p(term5,big_p(term4,X0,X1),X2),big_p(term5,X1,X2)),
inference(resolution,[],[f11,f42]) ).
fof(f12558,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term4,X1,X2)) = big_p(term4,big_p(term5,X0,big_p(term4,X1,X2)),big_p(term5,X0,X2)),
inference(resolution,[],[f11,f10089]) ).
fof(f12559,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term4,X1,X2)) = big_p(term3,big_p(term5,X0,X2),big_p(term5,X0,big_p(term4,X1,X2))),
inference(forward_demodulation,[],[f12558,f19]) ).
fof(f12563,plain,
! [X2,X0,X1] : big_p(term5,big_p(term4,X0,X1),X2) = big_p(term3,big_p(term5,X1,X2),big_p(term5,big_p(term4,X0,X1),X2)),
inference(forward_demodulation,[],[f12554,f19]) ).
fof(f12564,plain,
! [X2,X3,X0,X1] :
( big_p(term4,big_p(X0,X1,X2),X3) = big_p(X0,big_p(term4,big_p(X0,X1,X2),X3),big_p(term3,X3,X2))
| ~ term(X0) ),
inference(forward_demodulation,[],[f12553,f19]) ).
fof(f12567,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term3,X2,X1)) = big_p(term3,big_p(term5,X0,X2),big_p(term5,X0,big_p(term3,X2,X1))),
inference(forward_demodulation,[],[f12559,f19]) ).
fof(f12570,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X1,X0),X2) = big_p(term3,big_p(term5,X1,X2),big_p(term5,big_p(term3,X1,X0),X2)),
inference(forward_demodulation,[],[f12563,f19]) ).
fof(f12571,plain,
! [X2,X3,X0,X1] :
( ~ term(X0)
| big_p(term3,X3,big_p(X0,X1,X2)) = big_p(X0,big_p(term3,X3,big_p(X0,X1,X2)),big_p(term3,X3,X2)) ),
inference(forward_demodulation,[],[f12564,f19]) ).
fof(f12589,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term5,X1,X2)) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),big_p(term3,X0,X2)),
inference(resolution,[],[f12571,f12]) ).
fof(f12590,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term6,X1,X2)) = big_p(term6,big_p(term3,X0,big_p(term6,X1,X2)),big_p(term3,X0,X2)),
inference(resolution,[],[f12571,f13]) ).
fof(f12591,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term6,X1,X2)) = big_p(term5,big_p(term3,X0,X2),big_p(term3,X0,big_p(term6,X1,X2))),
inference(forward_demodulation,[],[f12590,f20]) ).
fof(f12595,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term5,X2,X1)) = big_p(term5,big_p(term3,X0,X2),big_p(term3,X0,big_p(term5,X2,X1))),
inference(forward_demodulation,[],[f12591,f20]) ).
fof(f12750,plain,
! [X0] : big_p(term3,X0,sF2) = big_p(term5,big_p(term3,X0,b),big_p(term3,X0,sF2)),
inference(superposition,[],[f12595,f28]) ).
fof(f12753,plain,
! [X0] : big_p(term3,X0,sF6) = big_p(term5,big_p(term3,X0,b),big_p(term3,X0,sF6)),
inference(superposition,[],[f12595,f36]) ).
fof(f12803,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),X3) = big_p(term5,big_p(term3,X0,X1),big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),X3)),
inference(superposition,[],[f41,f12595]) ).
fof(f12995,plain,
! [X0] : big_p(term3,X0,sF2) = big_p(term5,big_p(term3,X0,sF2),big_p(term3,X0,sF1)),
inference(superposition,[],[f12589,f3493]) ).
fof(f12998,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term5,big_p(term3,X0,sF5),big_p(term3,X0,big_p(term3,sF0,sF1))),
inference(superposition,[],[f12589,f4385]) ).
fof(f13079,plain,
! [X0,X1] : big_p(term3,X0,big_p(term5,X1,X0)) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X0)),X0),
inference(superposition,[],[f12589,f5800]) ).
fof(f13095,plain,
! [X0] : big_p(term3,a,big_p(term5,X0,sF2)) = big_p(term5,big_p(term3,a,big_p(term5,X0,sF2)),sF3),
inference(superposition,[],[f12589,f30]) ).
fof(f13152,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term5,X1,X2)) = big_p(term3,big_p(term3,X0,big_p(term5,X1,X2)),big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),X2)),
inference(superposition,[],[f10105,f12589]) ).
fof(f13153,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),X3) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),big_p(term5,big_p(term3,X0,X2),X3)),
inference(superposition,[],[f41,f12589]) ).
fof(f13175,plain,
! [X2,X0,X1] : big_p(term3,X0,big_p(term5,X1,X2)) = big_p(term3,X0,big_p(term3,big_p(term5,X1,X2),big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),X2))),
inference(forward_demodulation,[],[f13152,f94]) ).
fof(f13241,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term5,big_p(term3,X0,sF5),big_p(term3,X0,sF1)),
inference(forward_demodulation,[],[f12998,f609]) ).
fof(f13385,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X2),big_p(term5,X0,X1)) = big_p(term3,big_p(term5,X0,X1),big_p(term5,big_p(term3,X0,X2),big_p(term5,X0,X1))),
inference(superposition,[],[f12570,f6113]) ).
fof(f13564,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term3,big_p(term5,X0,big_p(term5,big_p(term3,X0,X1),X2)),big_p(term5,big_p(term3,X0,X1),X2)),
inference(superposition,[],[f12570,f6113]) ).
fof(f13586,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,big_p(term5,X0,big_p(term3,X0,X1)),big_p(term3,X0,X1)),
inference(superposition,[],[f12570,f5801]) ).
fof(f13588,plain,
! [X0,X1] : big_p(term3,big_p(term5,X0,X1),X1) = big_p(term5,big_p(term3,X0,X1),X1),
inference(superposition,[],[f10653,f12570]) ).
fof(f13591,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term5,big_p(term3,X0,X1),X2),big_p(term3,big_p(term5,X0,X2),X2)),
inference(superposition,[],[f12589,f12570]) ).
fof(f13592,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,big_p(term5,X0,X2),big_p(term3,X0,X1)),big_p(term5,big_p(term3,X0,X1),X2)),
inference(superposition,[],[f12595,f12570]) ).
fof(f13593,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term5,big_p(term3,X0,X1),X2),X3) = big_p(term3,big_p(term5,X0,X2),big_p(term3,big_p(term5,big_p(term3,X0,X1),X2),X3)),
inference(superposition,[],[f94,f12570]) ).
fof(f13622,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term5,X2,big_p(term3,big_p(term5,X0,X2),X2))),
inference(forward_demodulation,[],[f13591,f41]) ).
fof(f13689,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term3,big_p(term5,X0,X2),X2)),
inference(forward_demodulation,[],[f13622,f9406]) ).
fof(f13881,plain,
! [X0,X1] : big_p(term3,X0,X1) = big_p(term3,big_p(term5,big_p(term3,X0,X1),X0),big_p(term3,X0,X1)),
inference(superposition,[],[f12567,f5801]) ).
fof(f13902,plain,
! [X2,X0,X1] : big_p(term5,X0,big_p(term3,X1,X2)) = big_p(term5,big_p(term3,big_p(term5,X0,X1),X0),big_p(term5,X0,big_p(term3,X1,X2))),
inference(superposition,[],[f12595,f12567]) ).
fof(f13903,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),X3) = big_p(term3,big_p(term5,X0,X1),big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),X3)),
inference(superposition,[],[f94,f12567]) ).
fof(f14586,plain,
sF3 = big_p(term5,big_p(term3,sF3,b),sF3),
inference(superposition,[],[f12750,f3327]) ).
fof(f14676,plain,
sF7 = big_p(term5,big_p(term3,a,b),sF7),
inference(superposition,[],[f12753,f38]) ).
fof(f14729,plain,
sF7 = big_p(term3,sF7,big_p(term5,b,sF7)),
inference(superposition,[],[f343,f14676]) ).
fof(f14793,plain,
! [X0] : big_p(term5,sF3,X0) = big_p(term5,big_p(term3,sF3,b),big_p(term5,sF3,X0)),
inference(superposition,[],[f41,f14586]) ).
fof(f15604,plain,
! [X2,X3,X0,X1] : big_p(term3,big_p(term5,X0,X1),big_p(term5,X2,X3)) = big_p(term5,big_p(term3,X0,X2),big_p(term3,big_p(term5,X0,X1),big_p(term5,X2,X3))),
inference(superposition,[],[f12803,f10087]) ).
fof(f15661,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term5,X3,big_p(term3,X0,big_p(term5,X1,X2)))) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X2)),big_p(term5,X3,big_p(term3,X0,big_p(term5,X1,X2)))),
inference(superposition,[],[f3448,f12803]) ).
fof(f15978,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF4,sF1),sF1),
inference(superposition,[],[f13588,f34]) ).
fof(f16037,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term5,X1,X2)) = big_p(term5,big_p(term3,big_p(term5,X0,X1),X1),X2),
inference(superposition,[],[f41,f13588]) ).
fof(f16428,plain,
sF7 = big_p(term3,sF7,big_p(term5,sF7,big_p(term5,b,sF7))),
inference(superposition,[],[f10350,f14729]) ).
fof(f16694,plain,
! [X2,X0,X1] : big_p(term5,X2,big_p(term3,X0,big_p(term5,X1,X0))) = big_p(term5,X2,big_p(term5,X0,big_p(term3,X0,big_p(term5,X1,X0)))),
inference(superposition,[],[f3448,f13079]) ).
fof(f16696,plain,
! [X0,X1] : big_p(term3,X0,big_p(term5,X1,X0)) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X0)),big_p(term5,X0,big_p(term3,X0,big_p(term3,X0,big_p(term5,X1,X0))))),
inference(superposition,[],[f5916,f13079]) ).
fof(f16769,plain,
! [X0,X1] : big_p(term3,X0,big_p(term5,X1,X0)) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X0)),big_p(term5,X0,big_p(term3,X0,big_p(term5,X1,X0)))),
inference(forward_demodulation,[],[f16696,f5840]) ).
fof(f16868,plain,
! [X0,X1] : big_p(term3,X0,big_p(term5,X1,X0)) = big_p(term5,big_p(term3,X0,X1),big_p(term5,X0,big_p(term3,X0,big_p(term5,X1,X0)))),
inference(forward_demodulation,[],[f16769,f15661]) ).
fof(f16926,plain,
! [X0,X1] : big_p(term3,X0,big_p(term5,X1,X0)) = big_p(term5,big_p(term3,X0,X1),X0),
inference(forward_demodulation,[],[f16868,f434]) ).
fof(f17360,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,big_p(term3,X0,X1),X2),X3) = big_p(term5,big_p(term3,X0,X1),big_p(term5,big_p(term3,big_p(term5,X0,X2),X2),X3)),
inference(superposition,[],[f41,f13689]) ).
fof(f17392,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term5,big_p(term3,X0,X1),X2),X3) = big_p(term5,big_p(term3,X0,X1),big_p(term5,big_p(term3,X0,X2),big_p(term5,X2,X3))),
inference(forward_demodulation,[],[f17360,f16037]) ).
fof(f17494,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term5,X2,X3)) = big_p(term5,big_p(term3,X0,X1),big_p(term5,big_p(term3,X0,X2),big_p(term5,X2,X3))),
inference(forward_demodulation,[],[f17392,f41]) ).
fof(f17830,plain,
! [X2,X3,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term3,X2,X3)) = big_p(term3,big_p(term5,X0,X2),big_p(term5,big_p(term3,X0,X1),big_p(term3,X2,X3))),
inference(superposition,[],[f13593,f12567]) ).
fof(f20034,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,sF7,big_p(term3,big_p(term3,a,sF3),big_p(term3,sF6,sF3))),
inference(superposition,[],[f1115,f3563]) ).
fof(f20155,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,sF7,big_p(term3,a,big_p(term3,sF3,big_p(term3,sF6,sF3)))),
inference(forward_demodulation,[],[f20034,f94]) ).
fof(f20212,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,sF7,big_p(term3,sF3,big_p(term3,sF7,sF3))),
inference(forward_demodulation,[],[f20155,f1110]) ).
fof(f20267,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,sF7,big_p(term3,sF7,sF3)),
inference(forward_demodulation,[],[f20212,f247]) ).
fof(f20306,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,a,big_p(term3,sF7,sF3)),
inference(forward_demodulation,[],[f20267,f4105]) ).
fof(f20328,plain,
big_p(term3,sF7,big_p(term3,a,sF3)) = big_p(term3,a,big_p(term3,sF7,sF2)),
inference(forward_demodulation,[],[f20306,f6392]) ).
fof(f20340,plain,
big_p(term3,sF7,sF2) = big_p(term3,sF7,big_p(term3,a,sF3)),
inference(forward_demodulation,[],[f20328,f6279]) ).
fof(f20349,plain,
big_p(term3,sF7,sF3) = big_p(term3,sF7,sF2),
inference(forward_demodulation,[],[f20340,f3563]) ).
fof(f20353,plain,
! [X0] : big_p(term3,big_p(term3,sF7,sF2),X0) = big_p(term3,sF7,big_p(term3,sF3,X0)),
inference(superposition,[],[f94,f20349]) ).
fof(f20390,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF2,X0)) = big_p(term3,sF7,big_p(term3,sF3,X0)),
inference(forward_demodulation,[],[f20353,f94]) ).
fof(f22412,plain,
! [X0,X1] : big_p(term3,big_p(term5,b,big_p(term3,c,X0)),X1) = big_p(term3,sF4,big_p(term3,big_p(term5,b,big_p(term3,c,X0)),X1)),
inference(superposition,[],[f13903,f32]) ).
fof(f22416,plain,
! [X0,X1] : big_p(term3,big_p(term5,b,big_p(term3,sF5,X0)),X1) = big_p(term3,sF6,big_p(term3,big_p(term5,b,big_p(term3,sF5,X0)),X1)),
inference(superposition,[],[f13903,f36]) ).
fof(f23592,plain,
! [X0] : big_p(term3,sF7,big_p(term3,X0,sF7)) = big_p(term3,sF7,big_p(term3,X0,big_p(term5,sF7,sF6))),
inference(superposition,[],[f6068,f11128]) ).
fof(f23855,plain,
! [X0] : big_p(term3,a,big_p(term3,X0,sF6)) = big_p(term3,sF7,big_p(term3,X0,big_p(term5,sF7,sF6))),
inference(forward_demodulation,[],[f23592,f6061]) ).
fof(f28442,plain,
! [X0,X1] : big_p(term5,big_p(term3,b,X0),big_p(term3,sF5,X1)) = big_p(term3,sF6,big_p(term5,big_p(term3,b,X0),big_p(term3,sF5,X1))),
inference(superposition,[],[f22416,f12570]) ).
fof(f28814,plain,
! [X0] : big_p(term5,b,big_p(term5,sF1,X0)) = big_p(term5,sF2,big_p(term5,b,X0)),
inference(superposition,[],[f46,f6249]) ).
fof(f28816,plain,
! [X0] : big_p(term5,b,big_p(term5,sF5,X0)) = big_p(term5,sF6,big_p(term5,b,X0)),
inference(superposition,[],[f47,f6249]) ).
fof(f28867,plain,
! [X0] : big_p(term5,sF6,X0) = big_p(term5,sF6,big_p(term5,b,X0)),
inference(forward_demodulation,[],[f28816,f47]) ).
fof(f28869,plain,
! [X0] : big_p(term5,sF2,X0) = big_p(term5,sF2,big_p(term5,b,X0)),
inference(forward_demodulation,[],[f28814,f46]) ).
fof(f29062,plain,
big_p(term5,sF2,sF5) = big_p(term5,sF2,sF6),
inference(superposition,[],[f28869,f36]) ).
fof(f29330,plain,
big_p(term5,sF6,c) = big_p(term5,sF6,sF4),
inference(superposition,[],[f28867,f32]) ).
fof(f29331,plain,
big_p(term5,sF6,sF1) = big_p(term5,sF6,sF2),
inference(superposition,[],[f28867,f28]) ).
fof(f29372,plain,
! [X0] : big_p(term5,sF6,big_p(term5,X0,sF4)) = big_p(term5,sF6,big_p(term5,X0,c)),
inference(superposition,[],[f61,f28867]) ).
fof(f32240,plain,
! [X0,X1] : big_p(term3,big_p(term5,b,big_p(term3,X0,sF1)),X1) = big_p(term3,big_p(term5,b,big_p(term3,X0,sF1)),big_p(term3,sF2,X1)),
inference(superposition,[],[f10266,f28]) ).
fof(f33164,plain,
! [X0] : big_p(term3,big_p(term5,b,sF5),X0) = big_p(term3,big_p(term5,b,sF5),big_p(term3,sF2,X0)),
inference(superposition,[],[f32240,f747]) ).
fof(f33353,plain,
! [X0] : big_p(term3,sF6,X0) = big_p(term3,sF6,big_p(term3,sF2,X0)),
inference(forward_demodulation,[],[f33164,f36]) ).
fof(f33431,plain,
! [X0] : big_p(term3,a,big_p(term3,sF6,X0)) = big_p(term3,sF7,big_p(term3,sF2,X0)),
inference(superposition,[],[f100,f33353]) ).
fof(f33433,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF6,sF6)) = big_p(term3,X0,big_p(term3,sF2,sF6)),
inference(superposition,[],[f3273,f33353]) ).
fof(f33497,plain,
! [X0] : big_p(term3,X0,sF6) = big_p(term3,X0,big_p(term3,sF2,sF6)),
inference(forward_demodulation,[],[f33433,f3233]) ).
fof(f33498,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,sF7,big_p(term3,sF2,X0)),
inference(forward_demodulation,[],[f33431,f100]) ).
fof(f33603,plain,
big_p(term3,sF7,big_p(term3,a,sF7)) = big_p(term3,sF7,big_p(term3,sF2,sF7)),
inference(superposition,[],[f33498,f3574]) ).
fof(f33604,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF2,X0)) = big_p(term3,sF7,big_p(term5,big_p(term3,sF2,X0),X0)),
inference(superposition,[],[f33498,f10350]) ).
fof(f33688,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF2,X0)) = big_p(term3,sF7,big_p(term3,big_p(term5,sF2,X0),X0)),
inference(forward_demodulation,[],[f33604,f13588]) ).
fof(f33689,plain,
big_p(term3,a,big_p(term3,sF2,sF6)) = big_p(term3,sF7,big_p(term3,a,sF7)),
inference(forward_demodulation,[],[f33603,f6061]) ).
fof(f33736,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,sF7,big_p(term3,big_p(term5,sF2,X0),X0)),
inference(forward_demodulation,[],[f33688,f33498]) ).
fof(f33737,plain,
big_p(term3,a,big_p(term3,a,sF6)) = big_p(term3,a,big_p(term3,sF2,sF6)),
inference(forward_demodulation,[],[f33689,f6061]) ).
fof(f33744,plain,
big_p(term3,a,big_p(term3,a,sF6)) = big_p(term3,sF3,sF6),
inference(forward_demodulation,[],[f33737,f99]) ).
fof(f33748,plain,
big_p(term3,a,sF6) = big_p(term3,sF3,sF6),
inference(forward_demodulation,[],[f33744,f5840]) ).
fof(f33751,plain,
sF7 = big_p(term3,sF3,sF6),
inference(forward_demodulation,[],[f33748,f38]) ).
fof(f33755,plain,
sF7 = big_p(term5,big_p(term3,sF3,b),sF7),
inference(superposition,[],[f12753,f33751]) ).
fof(f33757,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,sF3,big_p(term3,sF6,X0)),
inference(superposition,[],[f94,f33751]) ).
fof(f35319,plain,
big_p(term5,sF4,sF6) = big_p(term5,sF4,big_p(term5,sF4,sF5)),
inference(superposition,[],[f3622,f892]) ).
fof(f35335,plain,
big_p(term5,sF4,sF5) = big_p(term5,sF4,sF6),
inference(forward_demodulation,[],[f35319,f6113]) ).
fof(f35446,plain,
! [X0] : big_p(term5,big_p(term5,sF4,sF5),X0) = big_p(term5,sF4,big_p(term5,sF6,X0)),
inference(superposition,[],[f41,f35335]) ).
fof(f35483,plain,
! [X0] : big_p(term5,sF4,big_p(term5,sF5,X0)) = big_p(term5,sF4,big_p(term5,sF6,X0)),
inference(forward_demodulation,[],[f35446,f41]) ).
fof(f38360,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF5,sF4)) = big_p(term5,X0,big_p(term5,sF6,sF4)),
inference(superposition,[],[f977,f29330]) ).
fof(f46132,plain,
big_p(term3,sF1,sF5) = big_p(term5,big_p(term3,sF1,sF5),sF1),
inference(superposition,[],[f13241,f5800]) ).
fof(f46210,plain,
big_p(term3,sF1,sF5) = big_p(term3,sF1,big_p(term5,sF5,sF1)),
inference(forward_demodulation,[],[f46132,f16926]) ).
fof(f50085,plain,
big_p(term5,b,sF5) = big_p(term3,big_p(term5,b,sF5),sF2),
inference(superposition,[],[f10251,f747]) ).
fof(f50159,plain,
sF6 = big_p(term3,sF6,sF2),
inference(forward_demodulation,[],[f50085,f36]) ).
fof(f50192,plain,
big_p(term3,a,sF6) = big_p(term3,sF7,sF2),
inference(superposition,[],[f100,f50159]) ).
fof(f50215,plain,
sF6 = big_p(term3,sF6,big_p(term3,sF2,big_p(term5,sF2,sF6))),
inference(superposition,[],[f6162,f50159]) ).
fof(f50237,plain,
sF6 = big_p(term3,sF6,big_p(term5,sF2,sF6)),
inference(forward_demodulation,[],[f50215,f33353]) ).
fof(f50245,plain,
sF7 = big_p(term3,sF7,sF2),
inference(forward_demodulation,[],[f50192,f38]) ).
fof(f50250,plain,
sF6 = big_p(term3,sF6,big_p(term5,sF2,sF5)),
inference(forward_demodulation,[],[f50237,f29062]) ).
fof(f50744,plain,
big_p(term3,a,sF6) = big_p(term3,sF7,big_p(term5,sF2,sF5)),
inference(superposition,[],[f100,f50250]) ).
fof(f50808,plain,
sF7 = big_p(term3,sF7,big_p(term5,sF2,sF5)),
inference(forward_demodulation,[],[f50744,f38]) ).
fof(f50834,plain,
sF7 = big_p(term5,sF7,big_p(term3,sF7,sF5)),
inference(superposition,[],[f12589,f50808]) ).
fof(f51951,plain,
! [X2,X0,X1] : big_p(term3,X2,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,X0)),X1))) = big_p(term3,X2,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,c,X0)),X1))),
inference(superposition,[],[f731,f22412]) ).
fof(f70647,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term5,X2,big_p(term3,X2,big_p(term5,big_p(term3,X1,X1),X2)))),
inference(superposition,[],[f434,f3233]) ).
fof(f71514,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term3,X2,big_p(term5,big_p(term3,X1,X1),X2))),
inference(forward_demodulation,[],[f70647,f16694]) ).
fof(f71765,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),X2) = big_p(term5,big_p(term3,X0,X1),big_p(term3,X2,big_p(term5,X1,X2))),
inference(forward_demodulation,[],[f71514,f5800]) ).
fof(f75884,plain,
! [X0] : big_p(term3,X0,big_p(term5,sF5,sF1)) = big_p(term3,X0,big_p(term3,sF1,big_p(term5,sF5,sF1))),
inference(superposition,[],[f3273,f15978]) ).
fof(f75924,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF1,sF5)) = big_p(term3,X0,big_p(term5,sF5,sF1)),
inference(forward_demodulation,[],[f75884,f46210]) ).
fof(f75956,plain,
! [X0] : big_p(term3,X0,sF5) = big_p(term3,X0,big_p(term5,sF5,sF1)),
inference(forward_demodulation,[],[f75924,f705]) ).
fof(f87157,plain,
! [X0] : big_p(term5,big_p(term5,big_p(term3,X0,b),sF5),sF6) = big_p(term3,big_p(term5,big_p(term5,big_p(term3,X0,b),sF5),sF6),sF6),
inference(superposition,[],[f13588,f421]) ).
fof(f87163,plain,
! [X0] : big_p(term5,big_p(term3,X0,b),big_p(term5,sF5,sF6)) = big_p(term3,big_p(term5,big_p(term3,X0,b),big_p(term5,sF5,sF6)),sF6),
inference(forward_demodulation,[],[f87157,f41]) ).
fof(f87194,plain,
! [X0] : big_p(term5,big_p(term3,X0,b),sF6) = big_p(term3,big_p(term5,big_p(term3,X0,b),sF6),sF6),
inference(forward_demodulation,[],[f87163,f2408]) ).
fof(f87221,plain,
sF7 = big_p(term3,sF7,big_p(term5,big_p(term3,sF3,b),sF6)),
inference(superposition,[],[f10202,f33755]) ).
fof(f90930,plain,
big_p(term3,sF7,big_p(term3,sF2,sF6)) = big_p(term3,sF7,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6)),
inference(superposition,[],[f33736,f33497]) ).
fof(f91047,plain,
big_p(term3,sF7,big_p(term3,sF2,sF6)) = big_p(term3,a,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6)),
inference(forward_demodulation,[],[f90930,f5242]) ).
fof(f91160,plain,
big_p(term3,a,big_p(term3,sF2,sF6)) = big_p(term3,a,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6)),
inference(forward_demodulation,[],[f91047,f5242]) ).
fof(f91218,plain,
big_p(term3,sF3,sF6) = big_p(term3,a,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6)),
inference(forward_demodulation,[],[f91160,f99]) ).
fof(f91244,plain,
sF7 = big_p(term3,a,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6)),
inference(forward_demodulation,[],[f91218,f33751]) ).
fof(f99225,plain,
big_p(term3,sF2,sF6) = big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6),
inference(superposition,[],[f33497,f13586]) ).
fof(f108690,plain,
sF3 = big_p(term5,sF3,big_p(term3,sF3,sF1)),
inference(superposition,[],[f12995,f3327]) ).
fof(f130038,plain,
! [X0] : big_p(term3,sF3,big_p(term3,sF2,X0)) = big_p(term3,sF3,big_p(term5,big_p(term3,b,X0),X0)),
inference(superposition,[],[f3554,f10836]) ).
fof(f130043,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF2,X0)) = big_p(term3,sF7,big_p(term5,big_p(term3,b,X0),X0)),
inference(superposition,[],[f33498,f10836]) ).
fof(f130152,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF2,X0)) = big_p(term3,sF7,big_p(term3,big_p(term5,b,X0),X0)),
inference(forward_demodulation,[],[f130043,f13588]) ).
fof(f130157,plain,
! [X0] : big_p(term3,sF3,big_p(term3,sF2,X0)) = big_p(term3,sF3,big_p(term3,big_p(term5,b,X0),X0)),
inference(forward_demodulation,[],[f130038,f13588]) ).
fof(f130315,plain,
! [X0] : big_p(term3,sF7,X0) = big_p(term3,sF7,big_p(term3,big_p(term5,b,X0),X0)),
inference(forward_demodulation,[],[f130152,f33498]) ).
fof(f130316,plain,
! [X0] : big_p(term3,sF3,X0) = big_p(term3,sF3,big_p(term3,big_p(term5,b,X0),X0)),
inference(forward_demodulation,[],[f130157,f3554]) ).
fof(f132154,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,big_p(term3,sF5,X0))) = big_p(term3,sF6,big_p(term5,big_p(term3,b,big_p(term3,sF5,X0)),big_p(term3,sF5,big_p(term3,sF5,X0)))),
inference(superposition,[],[f11009,f243]) ).
fof(f132187,plain,
big_p(term3,sF6,big_p(term3,sF5,sF5)) = big_p(term3,sF6,big_p(term5,big_p(term3,b,sF5),big_p(term3,sF5,sF5))),
inference(superposition,[],[f11009,f193]) ).
fof(f132460,plain,
big_p(term3,sF6,big_p(term3,sF5,sF5)) = big_p(term5,big_p(term3,b,sF5),big_p(term3,sF5,sF5)),
inference(forward_demodulation,[],[f132187,f28442]) ).
fof(f132486,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,big_p(term3,sF5,X0))) = big_p(term5,big_p(term3,b,big_p(term3,sF5,X0)),big_p(term3,sF5,big_p(term3,sF5,X0))),
inference(forward_demodulation,[],[f132154,f28442]) ).
fof(f132592,plain,
big_p(term3,sF6,big_p(term3,sF4,sF5)) = big_p(term5,big_p(term3,b,sF5),big_p(term3,sF4,sF5)),
inference(forward_demodulation,[],[f132460,f1184]) ).
fof(f132610,plain,
! [X0] : big_p(term5,big_p(term3,b,big_p(term3,sF5,X0)),big_p(term3,sF4,big_p(term3,sF5,X0))) = big_p(term3,sF6,big_p(term3,sF4,big_p(term3,sF5,X0))),
inference(forward_demodulation,[],[f132486,f1816]) ).
fof(f132669,plain,
big_p(term3,sF4,sF5) = big_p(term3,sF6,big_p(term3,sF4,sF5)),
inference(forward_demodulation,[],[f132592,f10488]) ).
fof(f132678,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,X0)) = big_p(term5,big_p(term3,b,big_p(term3,sF5,X0)),big_p(term3,sF4,big_p(term3,sF5,X0))),
inference(forward_demodulation,[],[f132610,f2285]) ).
fof(f132703,plain,
big_p(term3,sF4,sF5) = big_p(term3,sF6,sF5),
inference(forward_demodulation,[],[f132669,f782]) ).
fof(f132708,plain,
! [X0] : big_p(term3,sF4,big_p(term3,sF5,X0)) = big_p(term3,sF6,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f132678,f10488]) ).
fof(f132719,plain,
sF5 = big_p(term3,sF6,sF5),
inference(forward_demodulation,[],[f132703,f5906]) ).
fof(f132721,plain,
! [X0] : big_p(term3,sF5,X0) = big_p(term3,sF6,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f132708,f6355]) ).
fof(f132726,plain,
big_p(term3,sF7,sF5) = big_p(term3,a,sF5),
inference(superposition,[],[f100,f132719]) ).
fof(f132732,plain,
big_p(term3,sF3,sF5) = big_p(term3,sF7,sF5),
inference(superposition,[],[f33757,f132719]) ).
fof(f132791,plain,
sF5 = big_p(term3,big_p(term5,sF5,sF6),sF5),
inference(superposition,[],[f13881,f132719]) ).
fof(f132819,plain,
big_p(term3,sF3,sF5) = big_p(term3,a,sF5),
inference(forward_demodulation,[],[f132726,f132732]) ).
fof(f132839,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF5,X0)) = big_p(term3,big_p(term3,sF3,sF5),X0),
inference(superposition,[],[f94,f132732]) ).
fof(f132941,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF5,X0)) = big_p(term3,sF3,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f132839,f94]) ).
fof(f132994,plain,
! [X0] : big_p(term3,sF3,big_p(term3,sF5,X0)) = big_p(term3,big_p(term3,a,sF5),X0),
inference(superposition,[],[f94,f132819]) ).
fof(f133067,plain,
! [X0] : big_p(term3,a,big_p(term3,sF5,X0)) = big_p(term3,sF3,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f132994,f94]) ).
fof(f133594,plain,
sF5 = big_p(term5,sF5,big_p(term3,big_p(term5,sF5,sF6),sF1)),
inference(superposition,[],[f13241,f132791]) ).
fof(f133684,plain,
sF5 = big_p(term3,big_p(term5,sF5,sF6),sF1),
inference(forward_demodulation,[],[f133594,f10445]) ).
fof(f133780,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,big_p(term5,sF5,sF6),sF1),sF1),
inference(superposition,[],[f13588,f133684]) ).
fof(f133794,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,big_p(term5,sF6,sF1)),sF1),
inference(forward_demodulation,[],[f133780,f41]) ).
fof(f133824,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,big_p(term5,sF5,sF2)),sF1),
inference(forward_demodulation,[],[f133794,f979]) ).
fof(f133833,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,sF2),sF1),
inference(forward_demodulation,[],[f133824,f6113]) ).
fof(f133908,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,big_p(term5,sF5,sF1),big_p(term5,sF5,sF2)),big_p(term5,sF5,sF1)),
inference(superposition,[],[f13881,f133833]) ).
fof(f133914,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,big_p(term5,sF5,sF1),big_p(term5,sF5,sF2)),sF5),
inference(forward_demodulation,[],[f133908,f75956]) ).
fof(f133966,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,big_p(term5,sF1,big_p(term5,sF5,sF2))),sF5),
inference(forward_demodulation,[],[f133914,f41]) ).
fof(f133997,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,big_p(term5,sF5,sF2)),sF5),
inference(forward_demodulation,[],[f133966,f3640]) ).
fof(f134013,plain,
big_p(term5,sF5,sF1) = big_p(term3,big_p(term5,sF5,sF2),sF5),
inference(forward_demodulation,[],[f133997,f6113]) ).
fof(f134034,plain,
big_p(term5,b,big_p(term5,sF5,sF1)) = big_p(term3,big_p(term5,b,big_p(term5,sF5,sF1)),sF6),
inference(superposition,[],[f10254,f134013]) ).
fof(f134146,plain,
big_p(term5,sF6,sF1) = big_p(term3,big_p(term5,sF6,sF1),sF6),
inference(forward_demodulation,[],[f134034,f47]) ).
fof(f134257,plain,
! [X0] : big_p(term3,X0,big_p(term3,sF6,big_p(term5,sF6,sF1))) = big_p(term3,X0,big_p(term5,sF6,sF1)),
inference(superposition,[],[f3273,f134146]) ).
fof(f134316,plain,
! [X0] : big_p(term3,X0,sF6) = big_p(term3,X0,big_p(term5,sF6,sF1)),
inference(forward_demodulation,[],[f134257,f10215]) ).
fof(f134599,plain,
big_p(term3,sF2,sF6) = big_p(term5,big_p(term3,sF2,sF6),big_p(term3,sF1,big_p(term5,sF6,sF1))),
inference(superposition,[],[f263,f134316]) ).
fof(f134654,plain,
big_p(term3,sF2,sF6) = big_p(term5,big_p(term3,sF2,sF6),sF1),
inference(forward_demodulation,[],[f134599,f71765]) ).
fof(f136451,plain,
sF7 = big_p(term3,a,big_p(term5,sF7,big_p(term3,big_p(term5,sF2,big_p(term3,sF2,sF6)),sF6))),
inference(superposition,[],[f10350,f91244]) ).
fof(f136485,plain,
sF7 = big_p(term3,a,big_p(term5,sF7,big_p(term3,sF2,sF6))),
inference(forward_demodulation,[],[f136451,f99225]) ).
fof(f178332,plain,
! [X0,X1] : big_p(term5,sF4,big_p(term5,X0,big_p(term5,X1,sF4))) = big_p(term5,sF4,big_p(term5,X0,big_p(term5,X1,c))),
inference(superposition,[],[f6249,f3621]) ).
fof(f186769,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term5,X1,X2)) = big_p(term3,big_p(term5,X0,big_p(term5,X1,X2)),big_p(term5,X1,X2)),
inference(superposition,[],[f13689,f15604]) ).
fof(f195051,plain,
! [X0] : big_p(term5,X0,big_p(term5,big_p(term3,sF2,sF6),sF2)) = big_p(term5,X0,big_p(term5,sF2,big_p(term3,sF2,sF6))),
inference(superposition,[],[f3632,f134654]) ).
fof(f195457,plain,
! [X0] : big_p(term5,X0,big_p(term3,sF2,big_p(term5,sF6,sF2))) = big_p(term5,X0,big_p(term5,sF2,big_p(term3,sF2,sF6))),
inference(forward_demodulation,[],[f195051,f16926]) ).
fof(f195529,plain,
! [X0] : big_p(term5,X0,big_p(term3,sF2,big_p(term5,sF6,sF1))) = big_p(term5,X0,big_p(term5,sF2,big_p(term3,sF2,sF6))),
inference(forward_demodulation,[],[f195457,f29331]) ).
fof(f195574,plain,
! [X0] : big_p(term5,X0,big_p(term3,sF2,sF6)) = big_p(term5,X0,big_p(term5,sF2,big_p(term3,sF2,sF6))),
inference(forward_demodulation,[],[f195529,f134316]) ).
fof(f209292,plain,
! [X2,X0,X1] : big_p(term5,big_p(term3,X0,X1),big_p(term5,X0,X2)) = big_p(term5,big_p(term3,X0,big_p(term5,X1,X0)),X2),
inference(superposition,[],[f41,f16926]) ).
fof(f226981,plain,
big_p(term5,sF7,sF2) = big_p(term5,sF7,big_p(term5,sF2,big_p(term3,sF2,big_p(term5,sF6,sF1)))),
inference(superposition,[],[f1228,f29331]) ).
fof(f227286,plain,
big_p(term5,sF7,sF2) = big_p(term5,sF7,big_p(term5,sF2,big_p(term3,sF2,sF6))),
inference(forward_demodulation,[],[f226981,f134316]) ).
fof(f227411,plain,
big_p(term5,sF7,sF2) = big_p(term5,sF7,big_p(term3,sF2,sF6)),
inference(forward_demodulation,[],[f227286,f195574]) ).
fof(f227710,plain,
sF7 = big_p(term3,a,big_p(term5,sF7,sF2)),
inference(superposition,[],[f136485,f227411]) ).
fof(f227834,plain,
sF7 = big_p(term5,sF7,sF3),
inference(superposition,[],[f13095,f227710]) ).
fof(f227844,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,big_p(term3,a,sF2),X0)),
inference(superposition,[],[f13153,f227710]) ).
fof(f227941,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,sF3,X0)),
inference(forward_demodulation,[],[f227844,f30]) ).
fof(f291382,plain,
! [X0,X1] : big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,X0)),X1)) = big_p(term3,big_p(term5,b,big_p(term3,c,X0)),big_p(term3,sF1,X1)),
inference(superposition,[],[f22412,f733]) ).
fof(f305056,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,big_p(term3,sF7,big_p(term5,b,sF7)),X0)),
inference(superposition,[],[f13153,f16428]) ).
fof(f305187,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,big_p(term3,sF7,b),big_p(term5,sF7,X0))),
inference(forward_demodulation,[],[f305056,f209292]) ).
fof(f305223,plain,
! [X0] : big_p(term5,sF7,X0) = big_p(term5,sF7,big_p(term5,big_p(term3,sF7,b),X0)),
inference(forward_demodulation,[],[f305187,f6249]) ).
fof(f339354,plain,
! [X0,X1] : big_p(term5,big_p(term3,sF7,X0),X1) = big_p(term5,big_p(term3,sF7,X0),big_p(term5,big_p(term3,sF3,X0),X1)),
inference(superposition,[],[f289,f227834]) ).
fof(f379136,plain,
sF7 = big_p(term3,sF7,big_p(term3,big_p(term5,big_p(term3,sF3,b),sF6),big_p(term5,sF7,sF6))),
inference(superposition,[],[f13175,f87221]) ).
fof(f379199,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term3,big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(superposition,[],[f13588,f87221]) ).
fof(f379221,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term5,big_p(term3,sF7,big_p(term3,sF3,b)),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379199,f186769]) ).
fof(f379254,plain,
sF7 = big_p(term3,a,big_p(term3,big_p(term5,big_p(term3,sF3,b),sF6),sF6)),
inference(forward_demodulation,[],[f379136,f23855]) ).
fof(f379266,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term5,big_p(term3,sF7,big_p(term3,sF2,b)),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379221,f20390]) ).
fof(f379279,plain,
sF7 = big_p(term3,a,big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379254,f87194]) ).
fof(f379285,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term5,big_p(term3,sF7,b),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379266,f33498]) ).
fof(f379296,plain,
big_p(term5,big_p(term3,sF7,b),sF6) = big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379285,f339354]) ).
fof(f379364,plain,
sF7 = big_p(term3,a,big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6))),
inference(superposition,[],[f10350,f379279]) ).
fof(f379383,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term3,big_p(term5,a,big_p(term5,big_p(term3,sF3,b),sF6)),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(superposition,[],[f13588,f379279]) ).
fof(f379401,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term5,big_p(term3,a,big_p(term3,sF3,b)),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379383,f186769]) ).
fof(f379409,plain,
sF7 = big_p(term3,a,big_p(term5,big_p(term3,sF7,b),sF6)),
inference(forward_demodulation,[],[f379364,f379296]) ).
fof(f379448,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)) = big_p(term5,big_p(term3,sF3,b),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379401,f6267]) ).
fof(f379463,plain,
big_p(term5,big_p(term3,sF3,b),sF6) = big_p(term5,sF7,big_p(term5,big_p(term3,sF3,b),sF6)),
inference(forward_demodulation,[],[f379448,f6113]) ).
fof(f379471,plain,
big_p(term5,big_p(term3,sF7,b),sF6) = big_p(term5,big_p(term3,sF3,b),sF6),
inference(forward_demodulation,[],[f379463,f379296]) ).
fof(f379527,plain,
big_p(term5,sF7,big_p(term5,big_p(term3,sF7,b),sF6)) = big_p(term3,big_p(term5,sF7,big_p(term5,big_p(term3,sF7,b),sF6)),big_p(term5,big_p(term3,sF7,b),sF6)),
inference(superposition,[],[f6117,f379409]) ).
fof(f379596,plain,
big_p(term5,big_p(term3,sF7,b),sF6) = big_p(term5,sF7,big_p(term5,big_p(term3,sF7,b),sF6)),
inference(forward_demodulation,[],[f379527,f13564]) ).
fof(f379648,plain,
big_p(term5,sF7,sF6) = big_p(term5,big_p(term3,sF7,b),sF6),
inference(forward_demodulation,[],[f379596,f305223]) ).
fof(f379675,plain,
big_p(term5,sF7,sF6) = big_p(term5,big_p(term3,sF3,b),sF6),
inference(forward_demodulation,[],[f379648,f379471]) ).
fof(f395838,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),big_p(term3,X1,X2)) = big_p(term5,big_p(term3,X0,big_p(term3,X1,X2)),big_p(term3,X1,X2)),
inference(superposition,[],[f10653,f17830]) ).
fof(f396026,plain,
! [X2,X0,X1] : big_p(term3,big_p(term5,X0,X1),big_p(term3,X1,X2)) = big_p(term3,big_p(term5,X0,big_p(term3,X1,X2)),big_p(term3,X1,X2)),
inference(forward_demodulation,[],[f395838,f13588]) ).
fof(f398187,plain,
! [X0,X1] : big_p(term5,big_p(term3,X0,big_p(term3,sF5,X1)),big_p(term3,c,big_p(term3,sF5,X1))) = big_p(term3,big_p(term5,X0,big_p(term3,c,big_p(term3,sF5,X1))),big_p(term3,c,big_p(term3,sF5,X1))),
inference(superposition,[],[f13588,f3828]) ).
fof(f398574,plain,
! [X0,X1] : big_p(term5,big_p(term3,X0,big_p(term3,sF5,X1)),big_p(term3,c,big_p(term3,sF5,X1))) = big_p(term3,big_p(term5,X0,c),big_p(term3,c,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f398187,f396026]) ).
fof(f398773,plain,
! [X0,X1] : big_p(term5,big_p(term3,X0,big_p(term3,sF5,X1)),big_p(term3,c,big_p(term3,sF5,X1))) = big_p(term3,big_p(term5,X0,c),big_p(term3,sF5,X1)),
inference(forward_demodulation,[],[f398574,f3828]) ).
fof(f398855,plain,
! [X0,X1] : big_p(term3,big_p(term5,X0,c),big_p(term3,sF5,X1)) = big_p(term5,big_p(term3,X0,big_p(term3,sF5,X1)),big_p(term3,sF0,big_p(term3,sF5,X1))),
inference(forward_demodulation,[],[f398773,f4324]) ).
fof(f427391,plain,
! [X0,X1] : big_p(term5,big_p(term3,X0,X1),sF6) = big_p(term5,big_p(term3,X0,X1),big_p(term5,big_p(term3,X0,b),sF6)),
inference(superposition,[],[f17494,f36]) ).
fof(f431528,plain,
big_p(term5,big_p(term3,a,sF3),sF6) = big_p(term5,big_p(term3,a,sF3),big_p(term5,big_p(term3,sF3,b),sF6)),
inference(superposition,[],[f427391,f3858]) ).
fof(f432063,plain,
big_p(term5,big_p(term3,a,sF3),sF6) = big_p(term5,big_p(term3,a,sF3),big_p(term5,sF7,sF6)),
inference(forward_demodulation,[],[f431528,f379675]) ).
fof(f432247,plain,
big_p(term5,sF3,sF6) = big_p(term5,sF3,big_p(term5,sF7,sF6)),
inference(forward_demodulation,[],[f432063,f5904]) ).
fof(f432522,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF3,sF6)) = big_p(term5,X0,big_p(term5,sF3,big_p(term5,sF7,big_p(term5,sF3,sF6)))),
inference(superposition,[],[f399,f432247]) ).
fof(f432638,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF3,sF6)) = big_p(term5,X0,big_p(term5,sF7,big_p(term5,sF3,sF6))),
inference(forward_demodulation,[],[f432522,f5680]) ).
fof(f432660,plain,
! [X0] : big_p(term5,X0,big_p(term5,sF7,sF6)) = big_p(term5,X0,big_p(term5,sF3,sF6)),
inference(forward_demodulation,[],[f432638,f227941]) ).
fof(f440101,plain,
big_p(term5,sF7,sF6) = big_p(term5,big_p(term3,big_p(term5,sF3,sF6),big_p(term3,sF3,b)),big_p(term5,sF7,sF6)),
inference(superposition,[],[f13592,f379675]) ).
fof(f440581,plain,
big_p(term5,sF7,sF6) = big_p(term5,big_p(term3,big_p(term5,sF3,sF6),big_p(term3,sF3,b)),big_p(term5,sF3,sF6)),
inference(forward_demodulation,[],[f440101,f432660]) ).
fof(f441343,plain,
big_p(term5,sF7,sF6) = big_p(term3,big_p(term5,sF3,sF6),big_p(term5,big_p(term3,sF3,b),big_p(term5,sF3,sF6))),
inference(forward_demodulation,[],[f440581,f16926]) ).
fof(f441871,plain,
big_p(term5,sF7,sF6) = big_p(term5,big_p(term3,sF3,b),big_p(term5,sF3,sF6)),
inference(forward_demodulation,[],[f441343,f13385]) ).
fof(f442193,plain,
big_p(term5,sF7,sF6) = big_p(term5,sF3,sF6),
inference(forward_demodulation,[],[f441871,f14793]) ).
fof(f442556,plain,
sF7 = big_p(term3,a,big_p(term5,sF3,sF6)),
inference(superposition,[],[f11092,f442193]) ).
fof(f442707,plain,
sF7 = big_p(term5,big_p(term3,a,sF3),sF7),
inference(superposition,[],[f12595,f442556]) ).
fof(f442848,plain,
sF7 = big_p(term5,sF3,sF7),
inference(forward_demodulation,[],[f442707,f5904]) ).
fof(f442969,plain,
! [X0] : big_p(term5,sF3,big_p(term3,sF7,X0)) = big_p(term5,big_p(term3,sF7,sF3),big_p(term5,sF3,big_p(term3,sF7,X0))),
inference(superposition,[],[f13902,f442848]) ).
fof(f442992,plain,
! [X0] : big_p(term5,sF3,big_p(term3,sF7,X0)) = big_p(term5,big_p(term3,sF7,sF2),big_p(term5,sF3,big_p(term3,sF7,X0))),
inference(forward_demodulation,[],[f442969,f20349]) ).
fof(f443027,plain,
! [X0] : big_p(term5,sF3,big_p(term3,sF7,X0)) = big_p(term5,sF7,big_p(term5,sF3,big_p(term3,sF7,X0))),
inference(forward_demodulation,[],[f442992,f50245]) ).
fof(f443038,plain,
! [X0] : big_p(term5,sF7,big_p(term3,sF7,X0)) = big_p(term5,sF3,big_p(term3,sF7,X0)),
inference(forward_demodulation,[],[f443027,f227941]) ).
fof(f444968,plain,
sF7 = big_p(term5,sF3,big_p(term3,sF7,sF5)),
inference(superposition,[],[f50834,f443038]) ).
fof(f445132,plain,
sF7 = big_p(term5,sF3,big_p(term3,sF3,sF5)),
inference(forward_demodulation,[],[f444968,f132732]) ).
fof(f445286,plain,
sF7 = big_p(term5,sF3,big_p(term3,a,sF5)),
inference(forward_demodulation,[],[f445132,f132819]) ).
fof(f487143,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,X0)) = big_p(term5,big_p(term3,sF6,big_p(term3,sF5,X0)),big_p(term3,sF0,big_p(term3,sF5,X0))),
inference(superposition,[],[f4418,f1199]) ).
fof(f487400,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,X0)) = big_p(term3,big_p(term5,sF6,c),big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f487143,f398855]) ).
fof(f487785,plain,
! [X0] : big_p(term3,sF6,big_p(term3,sF5,X0)) = big_p(term3,big_p(term5,sF6,sF4),big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f487400,f29330]) ).
fof(f487984,plain,
! [X0] : big_p(term3,sF5,X0) = big_p(term3,big_p(term5,sF6,sF4),big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f487785,f132721]) ).
fof(f491492,plain,
sF5 = big_p(term3,big_p(term5,sF6,sF4),sF5),
inference(superposition,[],[f487984,f5800]) ).
fof(f491956,plain,
sF5 = big_p(term5,sF5,big_p(term3,big_p(term5,sF6,sF4),sF1)),
inference(superposition,[],[f13241,f491492]) ).
fof(f514202,plain,
big_p(term5,b,big_p(term5,sF6,c)) = big_p(term5,sF4,big_p(term5,sF6,big_p(term5,sF5,c))),
inference(superposition,[],[f895,f996]) ).
fof(f514560,plain,
big_p(term5,b,big_p(term5,sF6,c)) = big_p(term5,sF4,big_p(term5,sF6,big_p(term5,sF5,sF4))),
inference(forward_demodulation,[],[f514202,f178332]) ).
fof(f514773,plain,
big_p(term5,b,big_p(term5,sF6,c)) = big_p(term5,sF4,big_p(term5,sF5,big_p(term5,sF5,sF4))),
inference(forward_demodulation,[],[f514560,f35483]) ).
fof(f514865,plain,
big_p(term5,b,big_p(term5,sF6,c)) = big_p(term5,sF4,big_p(term5,sF5,sF4)),
inference(forward_demodulation,[],[f514773,f2419]) ).
fof(f514900,plain,
big_p(term5,sF6,big_p(term5,sF6,c)) = big_p(term5,sF4,big_p(term5,sF5,sF4)),
inference(forward_demodulation,[],[f514865,f2537]) ).
fof(f514913,plain,
big_p(term5,sF6,big_p(term5,sF6,sF4)) = big_p(term5,sF4,big_p(term5,sF5,sF4)),
inference(forward_demodulation,[],[f514900,f29372]) ).
fof(f514922,plain,
big_p(term5,sF6,big_p(term5,sF5,sF4)) = big_p(term5,sF4,big_p(term5,sF5,sF4)),
inference(forward_demodulation,[],[f514913,f38360]) ).
fof(f514925,plain,
big_p(term5,sF6,sF4) = big_p(term5,sF4,big_p(term5,sF5,sF4)),
inference(forward_demodulation,[],[f514922,f2428]) ).
fof(f514931,plain,
big_p(term3,big_p(term5,sF6,sF4),sF1) = big_p(term5,sF5,big_p(term3,big_p(term5,sF6,sF4),sF1)),
inference(superposition,[],[f10433,f514925]) ).
fof(f515097,plain,
sF5 = big_p(term3,big_p(term5,sF6,sF4),sF1),
inference(forward_demodulation,[],[f514931,f491956]) ).
fof(f515169,plain,
sF5 = big_p(term5,big_p(term3,sF6,sF1),sF5),
inference(superposition,[],[f10087,f515097]) ).
fof(f515326,plain,
sF5 = big_p(term3,sF6,sF1),
inference(forward_demodulation,[],[f515169,f1609]) ).
fof(f515367,plain,
big_p(term3,sF7,sF1) = big_p(term3,a,sF5),
inference(superposition,[],[f100,f515326]) ).
fof(f515562,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF1,X0)) = big_p(term3,big_p(term3,a,sF5),X0),
inference(superposition,[],[f94,f515367]) ).
fof(f515673,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF1,X0)) = big_p(term3,a,big_p(term3,sF5,X0)),
inference(forward_demodulation,[],[f515562,f94]) ).
fof(f524416,plain,
! [X0] : big_p(term3,sF3,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,sF3,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),big_p(term3,sF1,X0))),
inference(superposition,[],[f130316,f3760]) ).
fof(f524417,plain,
! [X0] : big_p(term3,sF7,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,sF7,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),big_p(term3,sF1,X0))),
inference(superposition,[],[f130315,f3760]) ).
fof(f524826,plain,
! [X0] : big_p(term3,sF7,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,sF7,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f524417,f291382]) ).
fof(f524827,plain,
! [X0] : big_p(term3,sF3,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,sF3,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f524416,f291382]) ).
fof(f525077,plain,
! [X0] : big_p(term3,sF7,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,sF3,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f524826,f132941]) ).
fof(f525078,plain,
! [X0] : big_p(term3,sF3,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f524827,f133067]) ).
fof(f525182,plain,
! [X0] : big_p(term3,sF7,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF5,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525077,f133067]) ).
fof(f525183,plain,
! [X0] : big_p(term3,sF3,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525078,f51951]) ).
fof(f525226,plain,
! [X0] : big_p(term3,sF7,big_p(term3,c,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,c,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525182,f51951]) ).
fof(f525227,plain,
! [X0] : big_p(term3,sF3,big_p(term3,sF0,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,sF0,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525183,f4435]) ).
fof(f525253,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF0,big_p(term3,sF1,X0))) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,sF0,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525226,f4435]) ).
fof(f525254,plain,
! [X0] : big_p(term3,sF3,big_p(term3,sF1,X0)) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,sF0,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525227,f1165]) ).
fof(f525266,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF1,X0)) = big_p(term3,a,big_p(term3,sF1,big_p(term3,big_p(term5,b,big_p(term3,sF0,big_p(term3,sF1,X0))),X0))),
inference(forward_demodulation,[],[f525253,f1165]) ).
fof(f525273,plain,
! [X0] : big_p(term3,sF7,big_p(term3,sF1,X0)) = big_p(term3,sF3,big_p(term3,sF1,X0)),
inference(forward_demodulation,[],[f525266,f525254]) ).
fof(f525280,plain,
! [X0] : big_p(term3,a,big_p(term3,sF5,X0)) = big_p(term3,sF3,big_p(term3,sF1,X0)),
inference(forward_demodulation,[],[f525273,f515673]) ).
fof(f525548,plain,
big_p(term3,sF3,sF1) = big_p(term3,a,big_p(term3,sF5,sF1)),
inference(superposition,[],[f3233,f525280]) ).
fof(f525795,plain,
big_p(term3,sF3,sF1) = big_p(term3,a,sF5),
inference(forward_demodulation,[],[f525548,f747]) ).
fof(f526559,plain,
sF3 = big_p(term5,sF3,big_p(term3,a,sF5)),
inference(superposition,[],[f108690,f525795]) ).
fof(f526719,plain,
sF3 = sF7,
inference(forward_demodulation,[],[f526559,f445286]) ).
fof(f526741,plain,
$false,
inference(forward_subsumption_resolution,[],[f526719,f39]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT041-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 13:57:45 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 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
% 10.46/2.31 % (2429758)Input is clausal, will run a generic CNF schedule.
% 10.46/2.31 % (2429764)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1998211723:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.46/2.31 % (2429768)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3193283448:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.46/2.31 % (2429769)dis-21_1_sil=8000:lcm=predicate:random_seed=802019273: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)
% 10.46/2.31 % (2429765)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1507105850:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.46/2.31 % (2429763)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=3749570701:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.46/2.31 % (2429769)Refutation not found, incomplete strategy
% 10.46/2.31 % (2429769)------------------------------
% 10.46/2.31 % (2429769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (2429769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (2429769)CaDiCaL version: 2.1.3
% 10.46/2.31 % (2429769)Termination reason: Refutation not found, incomplete strategy
% 10.46/2.31 % (2429769)Time elapsed: 0.002 s
% 10.46/2.31 % (2429769)Peak memory usage: 88 MB
% 10.46/2.31 % (2429769)Instructions burned: 1 (million)
% 10.46/2.31 % (2429766)lrs+10_1_sil=8000:sp=occurrence:random_seed=3031483611:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.46/2.31 % (2429767)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1769528703:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.46/2.31 % (2429766)Instruction limit reached!
% 10.46/2.31 % (2429766)------------------------------
% 10.46/2.31 % (2429766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (2429766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (2429766)CaDiCaL version: 2.1.3
% 10.46/2.31 % (2429766)Termination reason: Instruction limit
% 10.46/2.31 % (2429766)Termination phase: Saturation
% 10.46/2.31 % (2429766)Time elapsed: 0.060 s
% 10.46/2.31 % (2429766)Peak memory usage: 88 MB
% 10.46/2.31 % (2429766)Instructions burned: 109 (million)
% 10.46/2.31 % (2429767)Instruction limit reached!
% 10.46/2.31 % (2429767)------------------------------
% 10.46/2.31 % (2429767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (2429767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (2429767)CaDiCaL version: 2.1.3
% 10.46/2.31 % (2429767)Termination reason: Instruction limit
% 10.46/2.31 % (2429767)Termination phase: Saturation
% 10.46/2.31 % (2429767)Time elapsed: 0.065 s
% 10.46/2.31 % (2429767)Peak memory usage: 89 MB
% 10.46/2.31 % (2429767)Instructions burned: 116 (million)
% 10.46/2.31 % (2429768)Instruction limit reached!
% 10.46/2.31 % (2429768)------------------------------
% 10.46/2.31 % (2429768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (2429768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (2429768)CaDiCaL version: 2.1.3
% 10.46/2.31 % (2429768)Termination reason: Instruction limit
% 10.46/2.31 % (2429768)Termination phase: Saturation
% 10.46/2.31 % (2429768)Time elapsed: 0.106 s
% 10.46/2.31 % (2429768)Peak memory usage: 89 MB
% 10.46/2.31 % (2429768)Instructions burned: 181 (million)
% 10.46/2.31 % (2429777)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=2989063196:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.46/2.31 % (2429778)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1848776633:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 10.46/2.31 % (2429779)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3040844229:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.46/2.31 % (2429769)------------------------------
% 10.46/2.31 % (2429769)------------------------------
% 10.46/2.31 % (2429777)Instruction limit reached!
% 10.46/2.31 % (2429777)------------------------------
% 19.56/3.70 % (2429777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429777)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429777)Termination reason: Instruction limit
% 19.56/3.70 % (2429777)Termination phase: Saturation
% 19.56/3.70 % (2429777)Time elapsed: 0.084 s
% 19.56/3.70 % (2429777)Peak memory usage: 89 MB
% 19.56/3.70 % (2429777)Instructions burned: 144 (million)
% 19.56/3.70 % (2429778)Instruction limit reached!
% 19.56/3.70 % (2429778)------------------------------
% 19.56/3.70 % (2429778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429778)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429778)Termination reason: Instruction limit
% 19.56/3.70 % (2429778)Termination phase: Saturation
% 19.56/3.70 % (2429778)Time elapsed: 0.107 s
% 19.56/3.70 % (2429778)Peak memory usage: 89 MB
% 19.56/3.70 % (2429778)Instructions burned: 189 (million)
% 19.56/3.70 % (2429779)Instruction limit reached!
% 19.56/3.70 % (2429779)------------------------------
% 19.56/3.70 % (2429779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429779)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429779)Termination reason: Instruction limit
% 19.56/3.70 % (2429779)Termination phase: Saturation
% 19.56/3.70 % (2429779)Time elapsed: 0.117 s
% 19.56/3.70 % (2429779)Peak memory usage: 89 MB
% 19.56/3.70 % (2429779)Instructions burned: 219 (million)
% 19.56/3.70 % (2429784)lrs+10_64_to=lpo:sil=8000:random_seed=1109338971:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 19.56/3.70 % (2429785)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3082899890:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.56/3.70 % (2429786)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3506068847:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.56/3.70 % (2429784)Instruction limit reached!
% 19.56/3.70 % (2429784)------------------------------
% 19.56/3.70 % (2429784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429784)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429784)Termination reason: Instruction limit
% 19.56/3.70 % (2429784)Termination phase: Saturation
% 19.56/3.70 % (2429784)Time elapsed: 0.077 s
% 19.56/3.70 % (2429784)Peak memory usage: 89 MB
% 19.56/3.70 % (2429784)Instructions burned: 127 (million)
% 19.56/3.70 % (2429787)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1134444208:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 19.56/3.70 % (2429786)Instruction limit reached!
% 19.56/3.70 % (2429786)------------------------------
% 19.56/3.70 % (2429786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429786)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429786)Termination reason: Instruction limit
% 19.56/3.70 % (2429786)Termination phase: Saturation
% 19.56/3.70 % (2429786)Time elapsed: 0.089 s
% 19.56/3.70 % (2429786)Peak memory usage: 90 MB
% 19.56/3.70 % (2429786)Instructions burned: 159 (million)
% 19.56/3.70 % (2429785)Instruction limit reached!
% 19.56/3.70 % (2429785)------------------------------
% 19.56/3.70 % (2429785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.56/3.70 % (2429785)CaDiCaL version: 2.1.3
% 19.56/3.70 % (2429785)Termination reason: Instruction limit
% 19.56/3.70 % (2429785)Termination phase: Saturation
% 19.56/3.70 % (2429785)Time elapsed: 0.121 s
% 19.56/3.70 % (2429785)Peak memory usage: 89 MB
% 19.56/3.70 % (2429785)Instructions burned: 195 (million)
% 19.56/3.70 % (2429791)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=2465412416:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.56/3.70 % (2429791)Instruction limit reached!
% 19.56/3.70 % (2429791)------------------------------
% 19.56/3.70 % (2429791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.56/3.70 % (2429791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429791)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429791)Termination reason: Instruction limit
% 32.38/5.45 % (2429791)Termination phase: Saturation
% 32.38/5.45 % (2429791)Time elapsed: 0.060 s
% 32.38/5.45 % (2429791)Peak memory usage: 89 MB
% 32.38/5.45 % (2429791)Instructions burned: 106 (million)
% 32.38/5.45 % (2429794)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3498609655:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 32.38/5.45 % (2429793)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2982430564:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 32.38/5.45 % (2429793)Instruction limit reached!
% 32.38/5.45 % (2429793)------------------------------
% 32.38/5.45 % (2429793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.38/5.45 % (2429793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429793)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429793)Termination reason: Instruction limit
% 32.38/5.45 % (2429793)Termination phase: Saturation
% 32.38/5.45 % (2429793)Time elapsed: 0.060 s
% 32.38/5.45 % (2429793)Peak memory usage: 88 MB
% 32.38/5.45 % (2429793)Instructions burned: 107 (million)
% 32.38/5.45 % (2429796)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2133845619:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 32.38/5.45 % (2429794)Instruction limit reached!
% 32.38/5.45 % (2429794)------------------------------
% 32.38/5.45 % (2429794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.38/5.45 % (2429794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429794)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429794)Termination reason: Instruction limit
% 32.38/5.45 % (2429794)Termination phase: Saturation
% 32.38/5.45 % (2429794)Time elapsed: 0.132 s
% 32.38/5.45 % (2429794)Peak memory usage: 90 MB
% 32.38/5.45 % (2429794)Instructions burned: 242 (million)
% 32.38/5.45 % (2429799)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2230070620:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 32.38/5.45 % (2429801)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=921970445:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 32.38/5.45 % (2429799)Instruction limit reached!
% 32.38/5.45 % (2429799)------------------------------
% 32.38/5.45 % (2429799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.38/5.45 % (2429799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429799)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429799)Termination reason: Instruction limit
% 32.38/5.45 % (2429799)Termination phase: Saturation
% 32.38/5.45 % (2429799)Time elapsed: 0.076 s
% 32.38/5.45 % (2429799)Peak memory usage: 89 MB
% 32.38/5.45 % (2429799)Instructions burned: 135 (million)
% 32.38/5.45 % (2429804)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2816959677:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 32.38/5.45 % (2429804)Instruction limit reached!
% 32.38/5.45 % (2429804)------------------------------
% 32.38/5.45 % (2429804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.38/5.45 % (2429804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429804)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429804)Termination reason: Instruction limit
% 32.38/5.45 % (2429804)Termination phase: Saturation
% 32.38/5.45 % (2429804)Time elapsed: 0.120 s
% 32.38/5.45 % (2429804)Peak memory usage: 90 MB
% 32.38/5.45 % (2429804)Instructions burned: 192 (million)
% 32.38/5.45 % (2429801)Instruction limit reached!
% 32.38/5.45 % (2429801)------------------------------
% 32.38/5.45 % (2429801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.38/5.45 % (2429801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.38/5.45 % (2429801)CaDiCaL version: 2.1.3
% 32.38/5.45 % (2429801)Termination reason: Instruction limit
% 32.38/5.45 % (2429801)Termination phase: Saturation
% 32.38/5.45 % (2429801)Time elapsed: 0.314 s
% 32.38/5.45 % (2429801)Peak memory usage: 93 MB
% 32.38/5.45 % (2429801)Instructions burned: 500 (million)
% 32.38/5.45 % (2429806)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2246177379:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 54.90/8.71 % (2429807)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=863969947:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 54.90/8.71 % (2429807)Instruction limit reached!
% 54.90/8.71 % (2429807)------------------------------
% 54.90/8.71 % (2429807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429807)CaDiCaL version: 2.1.3
% 54.90/8.71 % (2429807)Termination reason: Instruction limit
% 54.90/8.71 % (2429807)Termination phase: Saturation
% 54.90/8.71 % (2429807)Time elapsed: 0.090 s
% 54.90/8.71 % (2429807)Peak memory usage: 89 MB
% 54.90/8.71 % (2429807)Instructions burned: 156 (million)
% 54.90/8.71 % (2429806)Instruction limit reached!
% 54.90/8.71 % (2429806)------------------------------
% 54.90/8.71 % (2429806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429806)CaDiCaL version: 2.1.3
% 54.90/8.71 % (2429806)Termination reason: Instruction limit
% 54.90/8.71 % (2429806)Termination phase: Saturation
% 54.90/8.71 % (2429806)Time elapsed: 0.157 s
% 54.90/8.71 % (2429806)Peak memory usage: 92 MB
% 54.90/8.71 % (2429806)Instructions burned: 264 (million)
% 54.90/8.71 % (2429810)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=3375216867:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 54.90/8.71 % (2429811)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=729814836:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 54.90/8.71 % (2429811)Instruction limit reached!
% 54.90/8.71 % (2429811)------------------------------
% 54.90/8.71 % (2429811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429811)CaDiCaL version: 2.1.3
% 54.90/8.71 % (2429811)Termination reason: Instruction limit
% 54.90/8.71 % (2429811)Termination phase: Saturation
% 54.90/8.71 % (2429811)Time elapsed: 0.273 s
% 54.90/8.71 % (2429811)Peak memory usage: 92 MB
% 54.90/8.71 % (2429811)Instructions burned: 538 (million)
% 54.90/8.71 % (2429814)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1114932840:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 54.90/8.71 % (2429814)Instruction limit reached!
% 54.90/8.71 % (2429814)------------------------------
% 54.90/8.71 % (2429814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429814)CaDiCaL version: 2.1.3
% 54.90/8.71 % (2429814)Termination reason: Instruction limit
% 54.90/8.71 % (2429814)Termination phase: Saturation
% 54.90/8.71 % (2429814)Time elapsed: 0.089 s
% 54.90/8.71 % (2429814)Peak memory usage: 88 MB
% 54.90/8.71 % (2429814)Instructions burned: 181 (million)
% 54.90/8.71 % (2429816)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=226999201:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 54.90/8.71 % (2429787)Instruction limit reached!
% 54.90/8.71 % (2429787)------------------------------
% 54.90/8.71 % (2429787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429787)CaDiCaL version: 2.1.3
% 54.90/8.71 % (2429787)Termination reason: Instruction limit
% 54.90/8.71 % (2429787)Termination phase: Saturation
% 54.90/8.71 % (2429787)Time elapsed: 1.824 s
% 54.90/8.71 % (2429787)Peak memory usage: 144 MB
% 54.90/8.71 % (2429787)Instructions burned: 3394 (million)
% 54.90/8.71 % (2429818)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=3507164130:i=412:gtgl=4:gtg=exists_all_2975 on theBenchmark for (2975ds/412Mi)
% 54.90/8.71 % (2429818)Instruction limit reached!
% 54.90/8.71 % (2429818)------------------------------
% 54.90/8.71 % (2429818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.90/8.71 % (2429818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.90/8.71 % (2429818)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429818)Termination reason: Instruction limit
% 77.26/11.86 % (2429818)Termination phase: Saturation
% 77.26/11.86 % (2429818)Time elapsed: 0.255 s
% 77.26/11.86 % (2429818)Peak memory usage: 94 MB
% 77.26/11.86 % (2429818)Instructions burned: 413 (million)
% 77.26/11.86 % (2429820)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=2460735319:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 77.26/11.86 % (2429810)Instruction limit reached!
% 77.26/11.86 % (2429810)------------------------------
% 77.26/11.86 % (2429810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.26/11.86 % (2429810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.26/11.86 % (2429810)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429810)Termination reason: Instruction limit
% 77.26/11.86 % (2429810)Termination phase: Saturation
% 77.26/11.86 % (2429810)Time elapsed: 1.859 s
% 77.26/11.86 % (2429810)Peak memory usage: 151 MB
% 77.26/11.86 % (2429810)Instructions burned: 3256 (million)
% 77.26/11.86 % (2429822)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=1259987172:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2963 on theBenchmark for (2963ds/303Mi)
% 77.26/11.86 % (2429822)Refutation not found, incomplete strategy
% 77.26/11.86 % (2429822)------------------------------
% 77.26/11.86 % (2429822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.26/11.86 % (2429822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.26/11.86 % (2429822)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429822)Termination reason: Refutation not found, incomplete strategy
% 77.26/11.86 % (2429822)Time elapsed: 0.006 s
% 77.26/11.86 % (2429822)Peak memory usage: 88 MB
% 77.26/11.86 % (2429822)Instructions burned: 8 (million)
% 77.26/11.86 % (2429796)Instruction limit reached!
% 77.26/11.86 % (2429796)------------------------------
% 77.26/11.86 % (2429796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.26/11.86 % (2429796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.26/11.86 % (2429796)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429796)Termination reason: Instruction limit
% 77.26/11.86 % (2429796)Termination phase: Saturation
% 77.26/11.86 % (2429796)Time elapsed: 3.019 s
% 77.26/11.86 % (2429796)Peak memory usage: 158 MB
% 77.26/11.86 % (2429796)Instructions burned: 5209 (million)
% 77.26/11.86 % (2429822)------------------------------
% 77.26/11.86 % (2429822)------------------------------
% 77.26/11.86 % (2429824)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2169231187:st=4:i=720:sd=3:fsr=off:ss=axioms_2960 on theBenchmark for (2960ds/720Mi)
% 77.26/11.86 % (2429825)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=890844242:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 77.26/11.86 % (2429825)Refutation not found, incomplete strategy
% 77.26/11.86 % (2429825)------------------------------
% 77.26/11.86 % (2429825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.26/11.86 % (2429825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.26/11.86 % (2429825)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429825)Termination reason: Refutation not found, incomplete strategy
% 77.26/11.86 % (2429825)Time elapsed: 0.001 s
% 77.26/11.86 % (2429825)Peak memory usage: 88 MB
% 77.26/11.86 % (2429825)Instructions burned: 1 (million)
% 77.26/11.86 % (2429825)------------------------------
% 77.26/11.86 % (2429825)------------------------------
% 77.26/11.86 % (2429824)Instruction limit reached!
% 77.26/11.86 % (2429824)------------------------------
% 77.26/11.86 % (2429824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.26/11.86 % (2429824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.26/11.86 % (2429824)CaDiCaL version: 2.1.3
% 77.26/11.86 % (2429824)Termination reason: Instruction limit
% 77.26/11.86 % (2429824)Termination phase: Saturation
% 77.26/11.86 % (2429824)Time elapsed: 0.386 s
% 77.26/11.86 % (2429824)Peak memory usage: 92 MB
% 77.26/11.86 % (2429824)Instructions burned: 720 (million)
% 77.26/11.86 % (2429828)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2354471932:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 77.26/11.86 % (2429829)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=852464321:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 116.29/17.28 % (2429829)Instruction limit reached!
% 116.29/17.28 % (2429829)------------------------------
% 116.29/17.28 % (2429829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.29/17.28 % (2429829)CaDiCaL version: 2.1.3
% 116.29/17.28 % (2429829)Termination reason: Instruction limit
% 116.29/17.28 % (2429829)Termination phase: Saturation
% 116.29/17.28 % (2429829)Time elapsed: 1.198 s
% 116.29/17.28 % (2429829)Peak memory usage: 137 MB
% 116.29/17.28 % (2429829)Instructions burned: 1997 (million)
% 116.29/17.28 % (2429832)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=3585664418:i=2088:bd=preordered:av=off_2941 on theBenchmark for (2941ds/2088Mi)
% 116.29/17.28 % (2429828)Instruction limit reached!
% 116.29/17.28 % (2429828)------------------------------
% 116.29/17.28 % (2429828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.29/17.28 % (2429828)CaDiCaL version: 2.1.3
% 116.29/17.28 % (2429828)Termination reason: Instruction limit
% 116.29/17.28 % (2429828)Termination phase: Saturation
% 116.29/17.28 % (2429828)Time elapsed: 1.686 s
% 116.29/17.28 % (2429828)Peak memory usage: 149 MB
% 116.29/17.28 % (2429828)Instructions burned: 2990 (million)
% 116.29/17.28 % (2429834)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1020223686:i=1098:nicw=on_2937 on theBenchmark for (2937ds/1098Mi)
% 116.29/17.28 % (2429834)Instruction limit reached!
% 116.29/17.28 % (2429834)------------------------------
% 116.29/17.28 % (2429834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.29/17.28 % (2429834)CaDiCaL version: 2.1.3
% 116.29/17.28 % (2429834)Termination reason: Instruction limit
% 116.29/17.28 % (2429834)Termination phase: Saturation
% 116.29/17.28 % (2429834)Time elapsed: 0.646 s
% 116.29/17.28 % (2429834)Peak memory usage: 100 MB
% 116.29/17.28 % (2429834)Instructions burned: 1099 (million)
% 116.29/17.28 % (2429836)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4000570679:i=433:bd=preordered_2930 on theBenchmark for (2930ds/433Mi)
% 116.29/17.28 % (2429832)Instruction limit reached!
% 116.29/17.28 % (2429832)------------------------------
% 116.29/17.28 % (2429832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.29/17.28 % (2429832)CaDiCaL version: 2.1.3
% 116.29/17.28 % (2429832)Termination reason: Instruction limit
% 116.29/17.28 % (2429832)Termination phase: Saturation
% 116.29/17.28 % (2429832)Time elapsed: 1.254 s
% 116.29/17.28 % (2429832)Peak memory usage: 139 MB
% 116.29/17.28 % (2429832)Instructions burned: 2089 (million)
% 116.29/17.28 % (2429838)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4000243682:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2927 on theBenchmark for (2927ds/2942Mi)
% 116.29/17.28 % (2429836)Instruction limit reached!
% 116.29/17.28 % (2429836)------------------------------
% 116.29/17.28 % (2429836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.29/17.28 % (2429836)CaDiCaL version: 2.1.3
% 116.29/17.28 % (2429836)Termination reason: Instruction limit
% 116.29/17.28 % (2429836)Termination phase: Saturation
% 116.29/17.28 % (2429836)Time elapsed: 0.242 s
% 116.29/17.28 % (2429836)Peak memory usage: 92 MB
% 116.29/17.28 % (2429836)Instructions burned: 433 (million)
% 116.29/17.28 % (2429840)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=132384205:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2926 on theBenchmark for (2926ds/6922Mi)
% 116.29/17.28 % (2429820)Instruction limit reached!
% 116.29/17.28 % (2429820)------------------------------
% 116.29/17.28 % (2429820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.29/17.28 % (2429820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429820)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429820)Termination reason: Instruction limit
% 135.32/19.99 % (2429820)Termination phase: Saturation
% 135.32/19.99 % (2429820)Time elapsed: 4.880 s
% 135.32/19.99 % (2429820)Peak memory usage: 180 MB
% 135.32/19.99 % (2429820)Instructions burned: 8479 (million)
% 135.32/19.99 % (2429842)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=965946097:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2921 on theBenchmark for (2921ds/596Mi)
% 135.32/19.99 % (2429842)Refutation not found, incomplete strategy
% 135.32/19.99 % (2429842)------------------------------
% 135.32/19.99 % (2429842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.32/19.99 % (2429842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429842)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429842)Termination reason: Refutation not found, incomplete strategy
% 135.32/19.99 % (2429842)Time elapsed: 0.003 s
% 135.32/19.99 % (2429842)Peak memory usage: 88 MB
% 135.32/19.99 % (2429842)Instructions burned: 4 (million)
% 135.32/19.99 % (2429842)------------------------------
% 135.32/19.99 % (2429842)------------------------------
% 135.32/19.99 % (2429844)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1238078475:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2917 on theBenchmark for (2917ds/4123Mi)
% 135.32/19.99 % (2429816)Instruction limit reached!
% 135.32/19.99 % (2429816)------------------------------
% 135.32/19.99 % (2429816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.32/19.99 % (2429816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429816)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429816)Termination reason: Instruction limit
% 135.32/19.99 % (2429816)Termination phase: Saturation
% 135.32/19.99 % (2429816)Time elapsed: 6.329 s
% 135.32/19.99 % (2429816)Peak memory usage: 194 MB
% 135.32/19.99 % (2429816)Instructions burned: 10307 (million)
% 135.32/19.99 % (2429846)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1554957505:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2912 on theBenchmark for (2912ds/16411Mi)
% 135.32/19.99 % (2429838)Instruction limit reached!
% 135.32/19.99 % (2429838)------------------------------
% 135.32/19.99 % (2429838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.32/19.99 % (2429838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429838)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429838)Termination reason: Instruction limit
% 135.32/19.99 % (2429838)Termination phase: Saturation
% 135.32/19.99 % (2429838)Time elapsed: 1.722 s
% 135.32/19.99 % (2429838)Peak memory usage: 145 MB
% 135.32/19.99 % (2429838)Instructions burned: 2943 (million)
% 135.32/19.99 % (2429848)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2049726047:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2909 on theBenchmark for (2909ds/1670Mi)
% 135.32/19.99 % (2429848)Instruction limit reached!
% 135.32/19.99 % (2429848)------------------------------
% 135.32/19.99 % (2429848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.32/19.99 % (2429848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429848)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429848)Termination reason: Instruction limit
% 135.32/19.99 % (2429848)Termination phase: Saturation
% 135.32/19.99 % (2429848)Time elapsed: 1.050 s
% 135.32/19.99 % (2429848)Peak memory usage: 135 MB
% 135.32/19.99 % (2429848)Instructions burned: 1670 (million)
% 135.32/19.99 % (2429850)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=1230751924:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2897 on theBenchmark for (2897ds/1722Mi)
% 135.32/19.99 % (2429844)Instruction limit reached!
% 135.32/19.99 % (2429844)------------------------------
% 135.32/19.99 % (2429844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.32/19.99 % (2429844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.32/19.99 % (2429844)CaDiCaL version: 2.1.3
% 135.32/19.99 % (2429844)Termination reason: Instruction limit
% 135.32/19.99 % (2429844)Termination phase: Saturation
% 135.32/19.99 % (2429844)Time elapsed: 2.488 s
% 135.32/19.99 % (2429844)Peak memory usage: 158 MB
% 135.32/19.99 % (2429844)Instructions burned: 4123 (million)
% 135.32/19.99 % (2429852)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1700415739:cts=off:cond=on:i=9530:bs=on:fsd=on_2891 on theBenchmark for (2891ds/9530Mi)
% 152.25/22.38 % (2429850)Instruction limit reached!
% 152.25/22.38 % (2429850)------------------------------
% 152.25/22.38 % (2429850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.25/22.38 % (2429850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.25/22.38 % (2429850)CaDiCaL version: 2.1.3
% 152.25/22.38 % (2429850)Termination reason: Instruction limit
% 152.25/22.38 % (2429850)Termination phase: Saturation
% 152.25/22.38 % (2429850)Time elapsed: 1.047 s
% 152.25/22.38 % (2429850)Peak memory usage: 134 MB
% 152.25/22.38 % (2429850)Instructions burned: 1723 (million)
% 152.25/22.38 % (2429854)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=921490354:st=2:i=4495:sd=10:ss=included_2885 on theBenchmark for (2885ds/4495Mi)
% 152.25/22.38 % (2429840)Instruction limit reached!
% 152.25/22.38 % (2429840)------------------------------
% 152.25/22.38 % (2429840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.25/22.38 % (2429840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.25/22.38 % (2429840)CaDiCaL version: 2.1.3
% 152.25/22.38 % (2429840)Termination reason: Instruction limit
% 152.25/22.38 % (2429840)Termination phase: Saturation
% 152.25/22.38 % (2429840)Time elapsed: 4.139 s
% 152.25/22.38 % (2429840)Peak memory usage: 173 MB
% 152.25/22.38 % (2429840)Instructions burned: 6923 (million)
% 152.25/22.38 % (2429856)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1655725943:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2883 on theBenchmark for (2883ds/4920Mi)
% 152.25/22.38 % (2429854)Instruction limit reached!
% 152.25/22.38 % (2429854)------------------------------
% 152.25/22.38 % (2429854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.25/22.38 % (2429854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.25/22.38 % (2429854)CaDiCaL version: 2.1.3
% 152.25/22.38 % (2429854)Termination reason: Instruction limit
% 152.25/22.38 % (2429854)Termination phase: Saturation
% 152.25/22.38 % (2429854)Time elapsed: 2.489 s
% 152.25/22.38 % (2429854)Peak memory usage: 153 MB
% 152.25/22.38 % (2429854)Instructions burned: 4495 (million)
% 152.25/22.38 % (2430102)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=896419266:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2859 on theBenchmark for (2859ds/2083Mi)
% 152.25/22.38 % (2429856)Instruction limit reached!
% 152.25/22.38 % (2429856)------------------------------
% 152.25/22.38 % (2429856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.25/22.38 % (2429856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.25/22.38 % (2429856)CaDiCaL version: 2.1.3
% 152.25/22.38 % (2429856)Termination reason: Instruction limit
% 152.25/22.38 % (2429856)Termination phase: Saturation
% 152.25/22.38 % (2429856)Time elapsed: 2.938 s
% 152.25/22.38 % (2429856)Peak memory usage: 163 MB
% 152.25/22.38 % (2429856)Instructions burned: 4921 (million)
% 152.25/22.38 % (2430202)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2861872115:i=4629:av=off:gsp=on_2852 on theBenchmark for (2852ds/4629Mi)
% 152.25/22.38 % (2430102)Instruction limit reached!
% 152.25/22.38 % (2430102)------------------------------
% 152.25/22.38 % (2430102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.25/22.38 % (2430102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.25/22.38 % (2430102)CaDiCaL version: 2.1.3
% 152.25/22.38 % (2430102)Termination reason: Instruction limit
% 152.25/22.38 % (2430102)Termination phase: Saturation
% 152.25/22.38 % (2430102)Time elapsed: 1.314 s
% 152.25/22.38 % (2430102)Peak memory usage: 138 MB
% 152.25/22.38 % (2430102)Instructions burned: 2084 (million)
% 152.25/22.38 % (2430289)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3751201590:i=1258:av=off_2843 on theBenchmark for (2843ds/1258Mi)
% 152.25/22.38 % (2430289)Instruction limit reached!
% 152.25/22.38 % (2430289)------------------------------
% 152.25/22.38 % (2430289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2430289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2430289)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2430289)Termination reason: Instruction limit
% 181.51/26.42 % (2430289)Termination phase: Saturation
% 181.51/26.42 % (2430289)Time elapsed: 0.678 s
% 181.51/26.42 % (2430289)Peak memory usage: 99 MB
% 181.51/26.42 % (2430289)Instructions burned: 1259 (million)
% 181.51/26.42 % (2430291)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4106879839:i=7343:av=off:ss=included_2835 on theBenchmark for (2835ds/7343Mi)
% 181.51/26.42 % (2429852)Instruction limit reached!
% 181.51/26.42 % (2429852)------------------------------
% 181.51/26.42 % (2429852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2429852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2429852)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2429852)Termination reason: Instruction limit
% 181.51/26.42 % (2429852)Termination phase: Saturation
% 181.51/26.42 % (2429852)Time elapsed: 6.032 s
% 181.51/26.42 % (2429852)Peak memory usage: 205 MB
% 181.51/26.42 % (2429852)Instructions burned: 9530 (million)
% 181.51/26.42 % (2430293)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3332300294:i=1325:sd=2:ss=axioms:sgt=16_2829 on theBenchmark for (2829ds/1325Mi)
% 181.51/26.42 % (2430202)Instruction limit reached!
% 181.51/26.42 % (2430202)------------------------------
% 181.51/26.42 % (2430202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2430202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2430202)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2430202)Termination reason: Instruction limit
% 181.51/26.42 % (2430202)Termination phase: Saturation
% 181.51/26.42 % (2430202)Time elapsed: 2.712 s
% 181.51/26.42 % (2430202)Peak memory usage: 158 MB
% 181.51/26.42 % (2430202)Instructions burned: 4629 (million)
% 181.51/26.42 % (2430295)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2932421529:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2824 on theBenchmark for (2824ds/2646Mi)
% 181.51/26.42 % (2430293)Instruction limit reached!
% 181.51/26.42 % (2430293)------------------------------
% 181.51/26.42 % (2430293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2430293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2430293)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2430293)Termination reason: Instruction limit
% 181.51/26.42 % (2430293)Termination phase: Saturation
% 181.51/26.42 % (2430293)Time elapsed: 0.783 s
% 181.51/26.42 % (2430293)Peak memory usage: 99 MB
% 181.51/26.42 % (2430293)Instructions burned: 1326 (million)
% 181.51/26.42 % (2430297)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=35641476:i=1489:sd=2:ep=R:ss=axioms_2820 on theBenchmark for (2820ds/1489Mi)
% 181.51/26.42 % (2430297)Refutation not found, incomplete strategy
% 181.51/26.42 % (2430297)------------------------------
% 181.51/26.42 % (2430297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2430297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2430297)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2430297)Termination reason: Refutation not found, incomplete strategy
% 181.51/26.42 % (2430297)Time elapsed: 0.568 s
% 181.51/26.42 % (2430297)Peak memory usage: 127 MB
% 181.51/26.42 % (2430297)Instructions burned: 857 (million)
% 181.51/26.42 % (2430297)------------------------------
% 181.51/26.42 % (2430297)------------------------------
% 181.51/26.42 % (2429846)Instruction limit reached!
% 181.51/26.42 % (2429846)------------------------------
% 181.51/26.42 % (2429846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.51/26.42 % (2429846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.51/26.42 % (2429846)CaDiCaL version: 2.1.3
% 181.51/26.42 % (2429846)Termination reason: Instruction limit
% 181.51/26.42 % (2429846)Termination phase: Saturation
% 181.51/26.42 % (2429846)Time elapsed: 10.164 s
% 181.51/26.42 % (2429846)Peak memory usage: 239 MB
% 181.51/26.42 % (2429846)Instructions burned: 16411 (million)
% 181.51/26.42 % (2430299)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=328615155:i=1503_2810 on theBenchmark for (2810ds/1503Mi)
% 181.51/26.42 % (2430300)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2716380025:i=13942:kws=frequency_2809 on theBenchmark for (2809ds/13942Mi)
% 208.47/30.21 % (2430295)Instruction limit reached!
% 208.47/30.21 % (2430295)------------------------------
% 208.47/30.21 % (2430295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.47/30.21 % (2430295)CaDiCaL version: 2.1.3
% 208.47/30.21 % (2430295)Termination reason: Instruction limit
% 208.47/30.21 % (2430295)Termination phase: Saturation
% 208.47/30.21 % (2430295)Time elapsed: 1.454 s
% 208.47/30.21 % (2430295)Peak memory usage: 142 MB
% 208.47/30.21 % (2430295)Instructions burned: 2646 (million)
% 208.47/30.21 % (2430303)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3300763251:i=3604:fsr=off:er=filter_2808 on theBenchmark for (2808ds/3604Mi)
% 208.47/30.21 % (2430299)Instruction limit reached!
% 208.47/30.21 % (2430299)------------------------------
% 208.47/30.21 % (2430299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.47/30.21 % (2430299)CaDiCaL version: 2.1.3
% 208.47/30.21 % (2430299)Termination reason: Instruction limit
% 208.47/30.21 % (2430299)Termination phase: Saturation
% 208.47/30.21 % (2430299)Time elapsed: 0.933 s
% 208.47/30.21 % (2430299)Peak memory usage: 134 MB
% 208.47/30.21 % (2430299)Instructions burned: 1503 (million)
% 208.47/30.21 % (2430305)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3328581953:i=1876:sd=1:ss=included:sgt=32_2800 on theBenchmark for (2800ds/1876Mi)
% 208.47/30.21 % (2430291)Instruction limit reached!
% 208.47/30.21 % (2430291)------------------------------
% 208.47/30.21 % (2430291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.47/30.21 % (2430291)CaDiCaL version: 2.1.3
% 208.47/30.21 % (2430291)Termination reason: Instruction limit
% 208.47/30.21 % (2430291)Termination phase: Saturation
% 208.47/30.21 % (2430291)Time elapsed: 4.246 s
% 208.47/30.21 % (2430291)Peak memory usage: 188 MB
% 208.47/30.21 % (2430291)Instructions burned: 7344 (million)
% 208.47/30.21 % (2430307)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3286668365:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2791 on theBenchmark for (2791ds/1932Mi)
% 208.47/30.21 % (2430303)Instruction limit reached!
% 208.47/30.21 % (2430303)------------------------------
% 208.47/30.21 % (2430303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.47/30.21 % (2430303)CaDiCaL version: 2.1.3
% 208.47/30.21 % (2430303)Termination reason: Instruction limit
% 208.47/30.21 % (2430303)Termination phase: Saturation
% 208.47/30.21 % (2430303)Time elapsed: 1.798 s
% 208.47/30.21 % (2430303)Peak memory usage: 133 MB
% 208.47/30.21 % (2430303)Instructions burned: 3606 (million)
% 208.47/30.21 % (2430309)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=145621963:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2788 on theBenchmark for (2788ds/1980Mi)
% 208.47/30.21 % (2430305)Instruction limit reached!
% 208.47/30.21 % (2430305)------------------------------
% 208.47/30.21 % (2430305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.47/30.21 % (2430305)CaDiCaL version: 2.1.3
% 208.47/30.21 % (2430305)Termination reason: Instruction limit
% 208.47/30.21 % (2430305)Termination phase: Saturation
% 208.47/30.21 % (2430305)Time elapsed: 1.112 s
% 208.47/30.21 % (2430305)Peak memory usage: 134 MB
% 208.47/30.21 % (2430305)Instructions burned: 1878 (million)
% 208.47/30.21 % (2430311)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=906355067:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2787 on theBenchmark for (2787ds/3902Mi)
% 208.47/30.21 % (2430307)Refutation not found, incomplete strategy
% 208.47/30.21 % (2430307)------------------------------
% 208.47/30.21 % (2430307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 208.47/30.21 % (2430307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430307)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430307)Termination reason: Refutation not found, incomplete strategy
% 197.32/33.38 % (2430307)Time elapsed: 0.571 s
% 197.32/33.38 % (2430307)Peak memory usage: 127 MB
% 197.32/33.38 % (2430307)Instructions burned: 856 (million)
% 197.32/33.38 % (2430307)------------------------------
% 197.32/33.38 % (2430307)------------------------------
% 197.32/33.38 % (2430313)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2786633985:avsq=on:i=3916:aac=none:amm=off_2782 on theBenchmark for (2782ds/3916Mi)
% 197.32/33.38 % (2430309)Instruction limit reached!
% 197.32/33.38 % (2430309)------------------------------
% 197.32/33.38 % (2430309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430309)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430309)Termination reason: Instruction limit
% 197.32/33.38 % (2430309)Termination phase: Saturation
% 197.32/33.38 % (2430309)Time elapsed: 1.139 s
% 197.32/33.38 % (2430309)Peak memory usage: 138 MB
% 197.32/33.38 % (2430309)Instructions burned: 1982 (million)
% 197.32/33.38 % (2430315)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2010596300:cond=on:i=3940:av=off:er=known_2776 on theBenchmark for (2776ds/3940Mi)
% 197.32/33.38 % (2430311)Instruction limit reached!
% 197.32/33.38 % (2430311)------------------------------
% 197.32/33.38 % (2430311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430311)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430311)Termination reason: Instruction limit
% 197.32/33.38 % (2430311)Termination phase: Saturation
% 197.32/33.38 % (2430311)Time elapsed: 2.296 s
% 197.32/33.38 % (2430311)Peak memory usage: 155 MB
% 197.32/33.38 % (2430311)Instructions burned: 3902 (million)
% 197.32/33.38 % (2430317)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1710226717:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2763 on theBenchmark for (2763ds/3980Mi)
% 197.32/33.38 % (2430313)Instruction limit reached!
% 197.32/33.38 % (2430313)------------------------------
% 197.32/33.38 % (2430313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430313)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430313)Termination reason: Instruction limit
% 197.32/33.38 % (2430313)Termination phase: Saturation
% 197.32/33.38 % (2430313)Time elapsed: 2.191 s
% 197.32/33.38 % (2430313)Peak memory usage: 141 MB
% 197.32/33.38 % (2430313)Instructions burned: 3917 (million)
% 197.32/33.38 % (2430319)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2324433463:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2758 on theBenchmark for (2758ds/2087Mi)
% 197.32/33.38 % (2430315)Instruction limit reached!
% 197.32/33.38 % (2430315)------------------------------
% 197.32/33.38 % (2430315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430315)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430315)Termination reason: Instruction limit
% 197.32/33.38 % (2430315)Termination phase: Saturation
% 197.32/33.38 % (2430315)Time elapsed: 2.229 s
% 197.32/33.38 % (2430315)Peak memory usage: 155 MB
% 197.32/33.38 % (2430315)Instructions burned: 3940 (million)
% 197.32/33.38 % (2430321)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3802056889:cts=off:cond=on:i=4272:bs=on:fsd=on_2752 on theBenchmark for (2752ds/4272Mi)
% 197.32/33.38 % (2430319)Instruction limit reached!
% 197.32/33.38 % (2430319)------------------------------
% 197.32/33.38 % (2430319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430319)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430319)Termination reason: Instruction limit
% 197.32/33.38 % (2430319)Termination phase: Saturation
% 197.32/33.38 % (2430319)Time elapsed: 1.330 s
% 197.32/33.38 % (2430319)Peak memory usage: 139 MB
% 197.32/33.38 % (2430319)Instructions burned: 2088 (million)
% 197.32/33.38 % (2430323)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2022851181:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2744 on theBenchmark for (2744ds/2197Mi)
% 197.32/33.38 % (2430317)Instruction limit reached!
% 197.32/33.38 % (2430317)------------------------------
% 197.32/33.38 % (2430317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430317)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430317)Termination reason: Instruction limit
% 197.32/33.38 % (2430317)Termination phase: Saturation
% 197.32/33.38 % (2430317)Time elapsed: 2.358 s
% 197.32/33.38 % (2430317)Peak memory usage: 155 MB
% 197.32/33.38 % (2430317)Instructions burned: 3981 (million)
% 197.32/33.38 % (2430325)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2315773616:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2738 on theBenchmark for (2738ds/6508Mi)
% 197.32/33.38 % (2430323)Instruction limit reached!
% 197.32/33.38 % (2430323)------------------------------
% 197.32/33.38 % (2430323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430323)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430323)Termination reason: Instruction limit
% 197.32/33.38 % (2430323)Termination phase: Saturation
% 197.32/33.38 % (2430323)Time elapsed: 1.326 s
% 197.32/33.38 % (2430323)Peak memory usage: 139 MB
% 197.32/33.38 % (2430323)Instructions burned: 2197 (million)
% 197.32/33.38 % (2430327)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3785354765:i=2330:fgj=on:av=off:fsr=off_2729 on theBenchmark for (2729ds/2330Mi)
% 197.32/33.38 % (2430300)Instruction limit reached!
% 197.32/33.38 % (2430300)------------------------------
% 197.32/33.38 % (2430300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430300)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430300)Termination reason: Instruction limit
% 197.32/33.38 % (2430300)Termination phase: Saturation
% 197.32/33.38 % (2430300)Time elapsed: 8.213 s
% 197.32/33.38 % (2430300)Peak memory usage: 242 MB
% 197.32/33.38 % (2430300)Instructions burned: 13943 (million)
% 197.32/33.38 % (2430329)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=4048270390:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2726 on theBenchmark for (2726ds/7592Mi)
% 197.32/33.38 % (2430321)Instruction limit reached!
% 197.32/33.38 % (2430321)------------------------------
% 197.32/33.38 % (2430321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430321)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430321)Termination reason: Instruction limit
% 197.32/33.38 % (2430321)Termination phase: Saturation
% 197.32/33.38 % (2430321)Time elapsed: 2.747 s
% 197.32/33.38 % (2430321)Peak memory usage: 161 MB
% 197.32/33.38 % (2430321)Instructions burned: 4273 (million)
% 197.32/33.38 % (2430336)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=2350329484:i=2693:kws=precedence:ins=1:av=off_2723 on theBenchmark for (2723ds/2693Mi)
% 197.32/33.38 % (2430327)Instruction limit reached!
% 197.32/33.38 % (2430327)------------------------------
% 197.32/33.38 % (2430327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430327)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430327)Termination reason: Instruction limit
% 197.32/33.38 % (2430327)Termination phase: Saturation
% 197.32/33.38 % (2430327)Time elapsed: 1.332 s
% 197.32/33.38 % (2430327)Peak memory usage: 141 MB
% 197.32/33.38 % (2430327)Instructions burned: 2330 (million)
% 197.32/33.38 % (2430569)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3330782401:i=28651:sd=4:ss=included:sgt=64_2714 on theBenchmark for (2714ds/28651Mi)
% 197.32/33.38 % (2430336)Instruction limit reached!
% 197.32/33.38 % (2430336)------------------------------
% 197.32/33.38 % (2430336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430336)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430336)Termination reason: Instruction limit
% 197.32/33.38 % (2430336)Termination phase: Saturation
% 197.32/33.38 % (2430336)Time elapsed: 1.598 s
% 197.32/33.38 % (2430336)Peak memory usage: 144 MB
% 197.32/33.38 % (2430336)Instructions burned: 2695 (million)
% 197.32/33.38 % (2430752)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1609347491:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2706 on theBenchmark for (2706ds/2700Mi)
% 197.32/33.38 % (2430325)Instruction limit reached!
% 197.32/33.38 % (2430325)------------------------------
% 197.32/33.38 % (2430325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430325)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430325)Termination reason: Instruction limit
% 197.32/33.38 % (2430325)Termination phase: Saturation
% 197.32/33.38 % (2430325)Time elapsed: 3.429 s
% 197.32/33.38 % (2430325)Peak memory usage: 142 MB
% 197.32/33.38 % (2430325)Instructions burned: 6509 (million)
% 197.32/33.38 % (2430754)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=13555132:i=3196:nm=4_2702 on theBenchmark for (2702ds/3196Mi)
% 197.32/33.38 % (2430752)Instruction limit reached!
% 197.32/33.38 % (2430752)------------------------------
% 197.32/33.38 % (2430752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430752)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430752)Termination reason: Instruction limit
% 197.32/33.38 % (2430752)Termination phase: Saturation
% 197.32/33.38 % (2430752)Time elapsed: 1.725 s
% 197.32/33.38 % (2430752)Peak memory usage: 144 MB
% 197.32/33.38 % (2430752)Instructions burned: 2701 (million)
% 197.32/33.38 % (2430756)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3880837795:cts=off:i=3254:av=off_2687 on theBenchmark for (2687ds/3254Mi)
% 197.32/33.38 % (2430329)Instruction limit reached!
% 197.32/33.38 % (2430329)------------------------------
% 197.32/33.38 % (2430329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430329)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430329)Termination reason: Instruction limit
% 197.32/33.38 % (2430329)Termination phase: Saturation
% 197.32/33.38 % (2430329)Time elapsed: 3.887 s
% 197.32/33.38 % (2430329)Peak memory usage: 147 MB
% 197.32/33.38 % (2430329)Instructions burned: 7593 (million)
% 197.32/33.38 % (2430758)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=2020121824:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2685 on theBenchmark for (2685ds/3264Mi)
% 197.32/33.38 % (2430754)Instruction limit reached!
% 197.32/33.38 % (2430754)------------------------------
% 197.32/33.38 % (2430754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.32/33.38 % (2430754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.32/33.38 % (2430754)CaDiCaL version: 2.1.3
% 197.32/33.38 % (2430754)Termination reason: Instruction limit
% 197.32/33.38 % (2430754)Termination phase: Saturation
% 197.32/33.38 % (2430754)Time elapsed: 1.878 s
% 197.32/33.38 % (2430754)Peak memory usage: 147 MB
% 197.32/33.38 % (2430754)Instructions burned: 3197 (million)
% 197.32/33.38 % (2430760)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=1065471122:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2682 on theBenchmark for (2682ds/9708Mi)
% 197.32/33.38 % (2429763)First to succeed.
% 197.32/33.38 % (2429763)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2429758"
% 197.32/33.38 % (2429763)Refutation found. Thanks to Tanya!
% 197.32/33.38 % SZS status Unsatisfiable for theBenchmark
% 197.32/33.38 % SZS output start Proof for theBenchmark
% See solution above
% 230.54/33.57 % (2429763)------------------------------
% 230.54/33.57 % (2429763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 230.54/33.57 % (2429763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 230.54/33.57 % (2429763)CaDiCaL version: 2.1.3
% 230.54/33.57 % (2429763)Termination reason: Refutation
% 230.54/33.57 % (2429763)Time elapsed: 31.920 s
% 230.54/33.57 % (2429763)Peak memory usage: 604 MB
% 230.54/33.57 % (2429763)Instructions burned: 53685 (million)
% 230.54/33.57 % (2429763)------------------------------
% 230.54/33.57 % (2429763)------------------------------
% 230.54/33.57 % (2429758)Success in time 32.527 s
% 230.54/33.57 % Vampire exiting
%------------------------------------------------------------------------------