%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:35:49 AM UTC 2026
% Result : Unsatisfiable 33.42s 5.46s
% Output : Refutation 34.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 23
% Syntax : Number of formulae : 160 ( 124 unt; 0 def)
% Number of atoms : 229 ( 116 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 139 ( 70 ~; 69 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 266 ( 266 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : sum(X0,X1,add(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_addition) ).
fof(f2,axiom,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_multiplication) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_addition) ).
fof(f4,axiom,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| product(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_multiplication) ).
fof(f5,axiom,
! [X0] : sum(additive_identity,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity1) ).
fof(f6,axiom,
! [X0] : sum(X0,additive_identity,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity2) ).
fof(f7,axiom,
! [X0] : product(multiplicative_identity,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_identity1) ).
fof(f8,axiom,
! [X0] : product(X0,multiplicative_identity,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_identity2) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X5,X6)
| ~ product(X0,X3,X4)
| ~ sum(X1,X3,X5)
| ~ product(X0,X1,X2)
| sum(X2,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity1) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X3,X4)
| ~ product(X0,X1,X2)
| ~ sum(X1,X3,X5)
| ~ sum(X2,X4,X6)
| product(X0,X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity2) ).
fof(f11,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X5,X1,X6)
| ~ product(X3,X1,X4)
| ~ sum(X0,X3,X5)
| ~ product(X0,X1,X2)
| sum(X2,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity3) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X3,X1,X4)
| ~ product(X0,X1,X2)
| ~ sum(X0,X3,X5)
| ~ sum(X2,X4,X6)
| product(X5,X1,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity4) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2)
| ~ sum(X0,X5,X6)
| product(X2,X4,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity5) ).
fof(f17,axiom,
! [X0] : sum(inverse(X0),X0,multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_inverse1) ).
fof(f18,axiom,
! [X0] : sum(X0,inverse(X0),multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_inverse2) ).
fof(f20,axiom,
! [X0] : product(X0,inverse(X0),additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_inverse2) ).
fof(f21,axiom,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addition_is_well_defined) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplication_is_well_defined) ).
fof(f23,axiom,
product(y,z,y_times_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',y_times_z) ).
fof(f24,axiom,
product(x,y_times_z,x_times__y_times_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_times__y_times_z) ).
fof(f25,axiom,
product(x,y,x_times_y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_times_y) ).
fof(f26,axiom,
product(x_times_y,z,x_times_y__times_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_times_y__times_z) ).
fof(f27,negated_conjecture,
x_times__y_times_z != x_times_y__times_z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_equality) ).
fof(f32,plain,
product(y,x,x_times_y),
inference(resolution,[],[f4,f25]) ).
fof(f33,plain,
product(z,x_times_y,x_times_y__times_z),
inference(resolution,[],[f4,f26]) ).
fof(f40,plain,
! [X0,X1] : product(X0,X1,multiply(X1,X0)),
inference(resolution,[],[f2,f4]) ).
fof(f41,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| multiply(X0,X1) = X2 ),
inference(resolution,[],[f2,f22]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| add(X0,X1) = X2 ),
inference(resolution,[],[f1,f21]) ).
fof(f46,plain,
! [X0,X1] :
( ~ product(X0,multiplicative_identity,X1)
| X0 = X1 ),
inference(resolution,[],[f8,f22]) ).
fof(f48,plain,
! [X0] : multiply(X0,multiplicative_identity) = X0,
inference(resolution,[],[f46,f2]) ).
fof(f53,plain,
! [X0] : multiply(multiplicative_identity,X0) = X0,
inference(resolution,[],[f40,f46]) ).
fof(f54,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ product(X0,X1,X2)
| sum(X5,X2,multiply(X0,X4)) ),
inference(resolution,[],[f9,f2]) ).
fof(f74,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[],[f3,f1]) ).
fof(f80,plain,
! [X0,X1] :
( ~ sum(additive_identity,X0,X1)
| X0 = X1 ),
inference(resolution,[],[f5,f21]) ).
fof(f81,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X1,X4)
| ~ sum(X0,X1,X2)
| sum(multiply(X3,X0),X4,multiply(X3,X2)) ),
inference(resolution,[],[f54,f2]) ).
fof(f91,plain,
! [X2,X3,X0,X1] :
( sum(multiply(X3,X0),multiply(X3,X1),multiply(X3,X2))
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f81,f2]) ).
fof(f198,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(resolution,[],[f41,f40]) ).
fof(f200,plain,
! [X0] : additive_identity = multiply(X0,inverse(X0)),
inference(resolution,[],[f41,f20]) ).
fof(f202,plain,
y_times_z = multiply(y,z),
inference(resolution,[],[f41,f23]) ).
fof(f203,plain,
x_times_y = multiply(y,x),
inference(resolution,[],[f41,f32]) ).
fof(f204,plain,
x_times_y__times_z = multiply(z,x_times_y),
inference(resolution,[],[f41,f33]) ).
fof(f206,plain,
x_times__y_times_z = multiply(x,y_times_z),
inference(resolution,[],[f41,f24]) ).
fof(f207,plain,
x_times_y = multiply(x,y),
inference(resolution,[],[f41,f25]) ).
fof(f208,plain,
x_times_y__times_z = multiply(x_times_y,z),
inference(resolution,[],[f41,f26]) ).
fof(f319,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(resolution,[],[f80,f74]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X2,multiply(X3,X1),X5)
| ~ sum(X0,X3,X4)
| ~ product(X0,X1,X2)
| product(X4,X1,X5) ),
inference(resolution,[],[f12,f2]) ).
fof(f337,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X2,multiply(X0,X3),X5)
| ~ sum(X1,X3,X4)
| ~ product(X0,X1,X2)
| product(X0,X4,X5) ),
inference(resolution,[],[f10,f2]) ).
fof(f352,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X1,X4)
| ~ sum(X3,X0,multiplicative_identity)
| ~ product(X0,X1,X2)
| sum(X4,X2,X1) ),
inference(resolution,[],[f7,f11]) ).
fof(f375,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X0,multiply(X3,X1),X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2)
| product(X4,X2,X5) ),
inference(resolution,[],[f13,f2]) ).
fof(f408,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X0,X4)
| ~ sum(X0,X1,X2)
| product(X3,X2,add(X4,multiply(X3,X1))) ),
inference(resolution,[],[f337,f1]) ).
fof(f433,plain,
! [X0,X1] :
( product(x,X1,add(x_times__y_times_z,multiply(x,X0)))
| ~ sum(y_times_z,X0,X1) ),
inference(resolution,[],[f408,f24]) ).
fof(f440,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X0,X3,X4)
| ~ sum(X0,X1,X2)
| product(X2,X3,add(X4,multiply(X1,X3))) ),
inference(resolution,[],[f325,f1]) ).
fof(f465,plain,
! [X0,X1] :
( product(X1,y_times_z,add(x_times__y_times_z,multiply(X0,y_times_z)))
| ~ sum(x,X0,X1) ),
inference(resolution,[],[f440,f24]) ).
fof(f467,plain,
! [X0,X1] :
( product(X1,z,add(x_times_y__times_z,multiply(X0,z)))
| ~ sum(x_times_y,X0,X1) ),
inference(resolution,[],[f440,f26]) ).
fof(f472,plain,
! [X2,X3,X0,X1,X4] :
( product(X2,X4,add(X0,multiply(X1,X3)))
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f375,f1]) ).
fof(f497,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2)
| multiply(X4,X2) = add(X0,multiply(X3,X1)) ),
inference(resolution,[],[f472,f41]) ).
fof(f518,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,X2)
| add(X0,multiply(X3,X1)) = multiply(add(X0,X3),X2) ),
inference(resolution,[],[f497,f1]) ).
fof(f522,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| multiply(multiplicative_identity,X2) = add(X0,multiply(inverse(X0),X1)) ),
inference(resolution,[],[f497,f18]) ).
fof(f530,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| add(X0,multiply(inverse(X0),X1)) = X2 ),
inference(forward_demodulation,[],[f522,f53]) ).
fof(f531,plain,
! [X0,X1] : add(X0,X1) = add(X0,multiply(inverse(X0),X1)),
inference(resolution,[],[f530,f1]) ).
fof(f532,plain,
! [X0,X1] : add(X1,X0) = add(X0,multiply(inverse(X0),X1)),
inference(resolution,[],[f530,f74]) ).
fof(f535,plain,
! [X0] : multiplicative_identity = add(X0,multiply(inverse(X0),inverse(X0))),
inference(resolution,[],[f530,f18]) ).
fof(f542,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(forward_demodulation,[],[f531,f532]) ).
fof(f560,plain,
! [X0] : add(X0,additive_identity) = add(inverse(inverse(X0)),X0),
inference(superposition,[],[f532,f200]) ).
fof(f562,plain,
! [X0] : multiplicative_identity = add(inverse(X0),X0),
inference(superposition,[],[f535,f532]) ).
fof(f566,plain,
! [X0] : add(inverse(inverse(X0)),X0) = X0,
inference(forward_demodulation,[],[f560,f319]) ).
fof(f582,plain,
! [X2,X0,X1] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X0,X2)),
inference(resolution,[],[f518,f1]) ).
fof(f583,plain,
! [X2,X0,X1] : add(X0,multiply(X1,X2)) = multiply(add(X0,X1),add(X2,X0)),
inference(resolution,[],[f518,f74]) ).
fof(f585,plain,
! [X0,X1] : add(X0,multiply(X1,additive_identity)) = multiply(add(X0,X1),X0),
inference(resolution,[],[f518,f6]) ).
fof(f591,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,X0)) = multiply(add(inverse(X0),X1),multiplicative_identity),
inference(resolution,[],[f518,f17]) ).
fof(f592,plain,
! [X0,X1] : add(inverse(X0),multiply(X1,X0)) = add(inverse(X0),X1),
inference(forward_demodulation,[],[f591,f48]) ).
fof(f598,plain,
! [X2,X0,X1] : add(X1,multiply(X0,X2)) = multiply(add(X0,X1),add(X1,X2)),
inference(superposition,[],[f582,f542]) ).
fof(f601,plain,
! [X0,X1] : add(X0,multiply(additive_identity,X1)) = multiply(X0,add(X0,X1)),
inference(superposition,[],[f582,f319]) ).
fof(f654,plain,
! [X0] : add(inverse(inverse(X0)),X0) = add(inverse(inverse(X0)),additive_identity),
inference(superposition,[],[f592,f200]) ).
fof(f673,plain,
! [X0] : inverse(inverse(X0)) = add(inverse(inverse(X0)),X0),
inference(forward_demodulation,[],[f654,f319]) ).
fof(f674,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f673,f566]) ).
fof(f691,plain,
! [X0,X1] : add(X1,multiply(X0,additive_identity)) = multiply(add(X0,X1),X1),
inference(superposition,[],[f585,f542]) ).
fof(f737,plain,
! [X0,X1] : add(X0,multiply(additive_identity,X1)) = multiply(X0,add(X1,X0)),
inference(superposition,[],[f583,f319]) ).
fof(f913,plain,
! [X2,X3,X0,X1] :
( ~ sum(X1,X2,X3)
| multiply(X0,X3) = add(multiply(X0,X1),multiply(X0,X2)) ),
inference(resolution,[],[f42,f91]) ).
fof(f1081,plain,
! [X0] : add(inverse(X0),X0) = add(inverse(X0),multiplicative_identity),
inference(superposition,[],[f592,f53]) ).
fof(f1083,plain,
! [X0] : multiplicative_identity = add(inverse(X0),multiplicative_identity),
inference(forward_demodulation,[],[f1081,f562]) ).
fof(f1092,plain,
! [X0] : multiplicative_identity = add(X0,multiplicative_identity),
inference(superposition,[],[f1083,f674]) ).
fof(f1114,plain,
! [X0] : sum(multiplicative_identity,X0,multiplicative_identity),
inference(superposition,[],[f74,f1092]) ).
fof(f1344,plain,
! [X2,X0,X1] : add(multiply(X0,X2),multiply(X0,X1)) = multiply(X0,add(X1,X2)),
inference(resolution,[],[f913,f74]) ).
fof(f1818,plain,
! [X2,X0,X1] :
( ~ sum(multiplicative_identity,X0,multiplicative_identity)
| ~ product(X0,X1,X2)
| sum(X1,X2,X1) ),
inference(resolution,[],[f352,f7]) ).
fof(f1828,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| sum(X1,X2,X1) ),
inference(forward_subsumption_resolution,[],[f1818,f1114]) ).
fof(f1831,plain,
! [X0,X1] : sum(X0,multiply(X1,X0),X0),
inference(resolution,[],[f1828,f2]) ).
fof(f1846,plain,
sum(y_times_z,x_times__y_times_z,y_times_z),
inference(resolution,[],[f1828,f24]) ).
fof(f1848,plain,
sum(z,x_times_y__times_z,z),
inference(resolution,[],[f1828,f26]) ).
fof(f1858,plain,
! [X0] : multiply(X0,y_times_z) = add(multiply(X0,y_times_z),multiply(X0,x_times__y_times_z)),
inference(resolution,[],[f1846,f913]) ).
fof(f1861,plain,
! [X0] : multiply(X0,y_times_z) = multiply(X0,add(x_times__y_times_z,y_times_z)),
inference(forward_demodulation,[],[f1858,f1344]) ).
fof(f2102,plain,
z = add(z,multiply(inverse(z),x_times_y__times_z)),
inference(resolution,[],[f1848,f530]) ).
fof(f2107,plain,
z = add(x_times_y__times_z,z),
inference(forward_demodulation,[],[f2102,f532]) ).
fof(f2220,plain,
! [X0] : add(x_times_y__times_z,multiply(X0,z)) = multiply(add(x_times_y__times_z,X0),z),
inference(superposition,[],[f582,f2107]) ).
fof(f2354,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = X0,
inference(resolution,[],[f1831,f42]) ).
fof(f2357,plain,
! [X2,X0,X1] : multiply(add(X0,X1),X0) = add(X0,multiply(X1,multiply(X2,X0))),
inference(resolution,[],[f1831,f518]) ).
fof(f2358,plain,
! [X0,X1] : add(X0,multiply(inverse(X0),multiply(X1,X0))) = X0,
inference(resolution,[],[f1831,f530]) ).
fof(f2365,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(resolution,[],[f1831,f80]) ).
fof(f2399,plain,
! [X0,X1] : add(multiply(X1,X0),X0) = X0,
inference(forward_demodulation,[],[f2358,f532]) ).
fof(f2400,plain,
! [X2,X0,X1] : add(X0,multiply(X1,additive_identity)) = add(X0,multiply(X1,multiply(X2,X0))),
inference(forward_demodulation,[],[f2357,f585]) ).
fof(f2403,plain,
! [X2,X0,X1] : add(X0,additive_identity) = add(X0,multiply(X1,multiply(X2,X0))),
inference(forward_demodulation,[],[f2400,f2365]) ).
fof(f2404,plain,
! [X2,X0,X1] : add(X0,multiply(X1,multiply(X2,X0))) = X0,
inference(forward_demodulation,[],[f2403,f319]) ).
fof(f2406,plain,
! [X0,X1] : add(X0,multiply(X0,X1)) = X0,
inference(superposition,[],[f2354,f198]) ).
fof(f2437,plain,
! [X2,X0,X1] : add(X0,multiply(multiply(X1,X0),X2)) = multiply(X0,add(X2,X0)),
inference(superposition,[],[f583,f2354]) ).
fof(f2448,plain,
! [X2,X0,X1] : add(X0,multiply(multiply(X1,X0),X2)) = add(X0,multiply(additive_identity,X2)),
inference(forward_demodulation,[],[f2437,f737]) ).
fof(f2581,plain,
x = add(x_times_y,x),
inference(superposition,[],[f2399,f203]) ).
fof(f2582,plain,
z = add(y_times_z,z),
inference(superposition,[],[f2399,f202]) ).
fof(f2583,plain,
x_times_y = add(x_times_y__times_z,x_times_y),
inference(superposition,[],[f2399,f204]) ).
fof(f2586,plain,
y = add(x_times_y,y),
inference(superposition,[],[f2399,f207]) ).
fof(f2632,plain,
add(x_times_y__times_z,multiply(x_times_y,additive_identity)) = multiply(x_times_y,x_times_y__times_z),
inference(superposition,[],[f585,f2583]) ).
fof(f2640,plain,
multiply(x_times_y,x_times_y__times_z) = add(x_times_y__times_z,additive_identity),
inference(forward_demodulation,[],[f2632,f2365]) ).
fof(f2642,plain,
x_times_y__times_z = multiply(x_times_y,x_times_y__times_z),
inference(forward_demodulation,[],[f2640,f319]) ).
fof(f2780,plain,
! [X2,X0,X1] : add(X1,multiply(multiply(X0,X1),X2)) = X1,
inference(superposition,[],[f2404,f198]) ).
fof(f2820,plain,
! [X2,X1] : add(X1,multiply(additive_identity,X2)) = X1,
inference(forward_demodulation,[],[f2780,f2448]) ).
fof(f2964,plain,
y = add(y,y_times_z),
inference(superposition,[],[f2406,f202]) ).
fof(f3260,plain,
! [X0] : multiply(x,add(x,X0)) = add(x,multiply(x_times_y,X0)),
inference(superposition,[],[f598,f2581]) ).
fof(f3267,plain,
! [X0] : add(x,multiply(additive_identity,X0)) = add(x,multiply(x_times_y,X0)),
inference(forward_demodulation,[],[f3260,f601]) ).
fof(f3270,plain,
! [X0] : x = add(x,multiply(x_times_y,X0)),
inference(forward_demodulation,[],[f3267,f2820]) ).
fof(f3644,plain,
! [X0] : multiply(z,add(z,X0)) = add(z,multiply(y_times_z,X0)),
inference(superposition,[],[f598,f2582]) ).
fof(f3652,plain,
! [X0] : add(z,multiply(additive_identity,X0)) = add(z,multiply(y_times_z,X0)),
inference(forward_demodulation,[],[f3644,f601]) ).
fof(f3655,plain,
! [X0] : z = add(z,multiply(y_times_z,X0)),
inference(forward_demodulation,[],[f3652,f2820]) ).
fof(f3867,plain,
add(x_times__y_times_z,multiply(additive_identity,y_times_z)) = multiply(x_times__y_times_z,y_times_z),
inference(superposition,[],[f1861,f601]) ).
fof(f3942,plain,
x_times__y_times_z = multiply(x_times__y_times_z,y_times_z),
inference(forward_demodulation,[],[f3867,f2820]) ).
fof(f4069,plain,
x_times__y_times_z = multiply(y_times_z,x_times__y_times_z),
inference(superposition,[],[f198,f3942]) ).
fof(f13528,plain,
x = add(x,x_times_y__times_z),
inference(superposition,[],[f3270,f2642]) ).
fof(f13915,plain,
z = add(z,x_times__y_times_z),
inference(superposition,[],[f3655,f4069]) ).
fof(f13974,plain,
! [X0] : multiply(add(X0,z),z) = add(z,multiply(X0,x_times__y_times_z)),
inference(superposition,[],[f598,f13915]) ).
fof(f13985,plain,
! [X0] : add(z,multiply(X0,additive_identity)) = add(z,multiply(X0,x_times__y_times_z)),
inference(forward_demodulation,[],[f13974,f691]) ).
fof(f13990,plain,
! [X0] : add(z,additive_identity) = add(z,multiply(X0,x_times__y_times_z)),
inference(forward_demodulation,[],[f13985,f2365]) ).
fof(f13995,plain,
! [X0] : z = add(z,multiply(X0,x_times__y_times_z)),
inference(forward_demodulation,[],[f13990,f319]) ).
fof(f16887,plain,
! [X0,X1] :
( ~ sum(x,X0,X1)
| multiply(X1,y_times_z) = add(x_times__y_times_z,multiply(X0,y_times_z)) ),
inference(resolution,[],[f465,f41]) ).
fof(f16959,plain,
! [X0] : add(x_times__y_times_z,multiply(X0,y_times_z)) = multiply(add(x,X0),y_times_z),
inference(resolution,[],[f16887,f1]) ).
fof(f16981,plain,
multiply(x,y_times_z) = add(x_times__y_times_z,multiply(x_times_y__times_z,y_times_z)),
inference(superposition,[],[f16959,f13528]) ).
fof(f17115,plain,
x_times__y_times_z = add(x_times__y_times_z,multiply(x_times_y__times_z,y_times_z)),
inference(forward_demodulation,[],[f16981,f206]) ).
fof(f17231,plain,
! [X0] : multiply(add(X0,x_times__y_times_z),x_times__y_times_z) = add(x_times__y_times_z,multiply(X0,multiply(x_times_y__times_z,y_times_z))),
inference(superposition,[],[f598,f17115]) ).
fof(f17244,plain,
! [X0] : add(x_times__y_times_z,multiply(X0,additive_identity)) = add(x_times__y_times_z,multiply(X0,multiply(x_times_y__times_z,y_times_z))),
inference(forward_demodulation,[],[f17231,f691]) ).
fof(f17251,plain,
! [X0] : add(x_times__y_times_z,additive_identity) = add(x_times__y_times_z,multiply(X0,multiply(x_times_y__times_z,y_times_z))),
inference(forward_demodulation,[],[f17244,f2365]) ).
fof(f17257,plain,
! [X0] : x_times__y_times_z = add(x_times__y_times_z,multiply(X0,multiply(x_times_y__times_z,y_times_z))),
inference(forward_demodulation,[],[f17251,f319]) ).
fof(f17335,plain,
x_times__y_times_z = add(multiply(x_times_y__times_z,y_times_z),x_times__y_times_z),
inference(superposition,[],[f532,f17257]) ).
fof(f19226,plain,
! [X0,X1] :
( ~ sum(y_times_z,X0,X1)
| multiply(x,X1) = add(x_times__y_times_z,multiply(x,X0)) ),
inference(resolution,[],[f433,f41]) ).
fof(f19299,plain,
! [X0] : add(x_times__y_times_z,multiply(x,X0)) = multiply(x,add(X0,y_times_z)),
inference(resolution,[],[f19226,f74]) ).
fof(f20636,plain,
! [X0,X1] :
( ~ sum(x_times_y,X0,X1)
| multiply(X1,z) = add(x_times_y__times_z,multiply(X0,z)) ),
inference(resolution,[],[f467,f41]) ).
fof(f20708,plain,
! [X0] : add(x_times_y__times_z,multiply(X0,z)) = multiply(add(x_times_y,X0),z),
inference(resolution,[],[f20636,f1]) ).
fof(f20709,plain,
! [X0] : add(x_times_y__times_z,multiply(X0,z)) = multiply(add(X0,x_times_y),z),
inference(resolution,[],[f20636,f74]) ).
fof(f20725,plain,
multiply(y,z) = add(x_times_y__times_z,multiply(y,z)),
inference(superposition,[],[f20708,f2586]) ).
fof(f20871,plain,
y_times_z = add(x_times_y__times_z,y_times_z),
inference(forward_demodulation,[],[f20725,f202]) ).
fof(f20908,plain,
multiply(x_times_y__times_z,y_times_z) = add(x_times_y__times_z,multiply(additive_identity,y_times_z)),
inference(superposition,[],[f601,f20871]) ).
fof(f20929,plain,
x_times_y__times_z = multiply(x_times_y__times_z,y_times_z),
inference(forward_demodulation,[],[f20908,f2820]) ).
fof(f20982,plain,
x_times__y_times_z = add(x_times_y__times_z,x_times__y_times_z),
inference(superposition,[],[f17335,f20929]) ).
fof(f21075,plain,
multiply(x_times__y_times_z,z) = add(x_times_y__times_z,multiply(x_times__y_times_z,z)),
inference(superposition,[],[f2220,f20982]) ).
fof(f23872,plain,
z = add(x_times__y_times_z,z),
inference(superposition,[],[f532,f13995]) ).
fof(f23929,plain,
multiply(x_times__y_times_z,z) = add(x_times__y_times_z,multiply(additive_identity,z)),
inference(superposition,[],[f601,f23872]) ).
fof(f23951,plain,
x_times__y_times_z = multiply(x_times__y_times_z,z),
inference(forward_demodulation,[],[f23929,f2820]) ).
fof(f51649,plain,
multiply(x,y) = add(x_times__y_times_z,multiply(x,y)),
inference(superposition,[],[f19299,f2964]) ).
fof(f51697,plain,
x_times_y = add(x_times__y_times_z,x_times_y),
inference(forward_demodulation,[],[f51649,f207]) ).
fof(f51715,plain,
multiply(x_times_y,z) = add(x_times_y__times_z,multiply(x_times__y_times_z,z)),
inference(superposition,[],[f20709,f51697]) ).
fof(f51769,plain,
multiply(x_times_y,z) = multiply(x_times__y_times_z,z),
inference(forward_demodulation,[],[f51715,f21075]) ).
fof(f51777,plain,
x_times__y_times_z = multiply(x_times_y,z),
inference(forward_demodulation,[],[f51769,f23951]) ).
fof(f51780,plain,
x_times__y_times_z = x_times_y__times_z,
inference(forward_demodulation,[],[f51777,f208]) ).
fof(f51781,plain,
$false,
inference(forward_subsumption_resolution,[],[f51780,f27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n007.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 21:01:26 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 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
% 14.72/2.83 % (2819654)Input is clausal, will run a generic CNF schedule.
% 14.72/2.83 % (2819747)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=827084020:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 14.72/2.83 % (2819743)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1092888395:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 14.72/2.83 % (2819744)lrs+10_1_sil=8000:sp=occurrence:random_seed=1424588373:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 14.72/2.83 % (2819741)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=501549982:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 14.72/2.83 % (2819742)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=639016024:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 14.72/2.83 % (2819745)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=130110826:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 14.72/2.83 % (2819744)Refutation not found, incomplete strategy
% 14.72/2.83 % (2819744)------------------------------
% 14.72/2.83 % (2819744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.83 % (2819744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.83 % (2819744)CaDiCaL version: 2.1.3
% 14.72/2.83 % (2819744)Termination reason: Refutation not found, incomplete strategy
% 14.72/2.83 % (2819744)Time elapsed: 0.013 s
% 14.72/2.83 % (2819744)Peak memory usage: 88 MB
% 14.72/2.83 % (2819744)Instructions burned: 19 (million)
% 14.72/2.83 % (2819748)dis-21_1_sil=8000:lcm=predicate:random_seed=1670125017: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)
% 14.72/2.83 % (2819747)Instruction limit reached!
% 14.72/2.83 % (2819747)------------------------------
% 14.72/2.83 % (2819747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.83 % (2819747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.83 % (2819747)CaDiCaL version: 2.1.3
% 14.72/2.83 % (2819747)Termination reason: Instruction limit
% 14.72/2.83 % (2819747)Termination phase: Saturation
% 14.72/2.83 % (2819747)Time elapsed: 0.062 s
% 14.72/2.83 % (2819747)Peak memory usage: 89 MB
% 14.72/2.83 % (2819747)Instructions burned: 183 (million)
% 14.72/2.83 % (2819745)Instruction limit reached!
% 14.72/2.83 % (2819745)------------------------------
% 14.72/2.83 % (2819745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.83 % (2819745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.83 % (2819745)CaDiCaL version: 2.1.3
% 14.72/2.83 % (2819745)Termination reason: Instruction limit
% 14.72/2.83 % (2819745)Termination phase: Saturation
% 14.72/2.83 % (2819745)Time elapsed: 0.063 s
% 14.72/2.83 % (2819745)Peak memory usage: 88 MB
% 14.72/2.83 % (2819745)Instructions burned: 115 (million)
% 14.72/2.83 % (2819748)Instruction limit reached!
% 14.72/2.83 % (2819748)------------------------------
% 14.72/2.83 % (2819748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.83 % (2819748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.83 % (2819748)CaDiCaL version: 2.1.3
% 14.72/2.83 % (2819748)Termination reason: Instruction limit
% 14.72/2.83 % (2819748)Termination phase: Saturation
% 14.72/2.83 % (2819748)Time elapsed: 0.067 s
% 14.72/2.83 % (2819748)Peak memory usage: 88 MB
% 14.72/2.83 % (2819748)Instructions burned: 118 (million)
% 14.72/2.83 % (2819790)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=2631091963:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 14.72/2.83 % (2819790)Instruction limit reached!
% 14.72/2.83 % (2819790)------------------------------
% 14.72/2.83 % (2819790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.72/2.83 % (2819790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.83 % (2819790)CaDiCaL version: 2.1.3
% 14.72/2.83 % (2819790)Termination reason: Instruction limit
% 14.72/2.83 % (2819790)Termination phase: Saturation
% 14.72/2.83 % (2819790)Time elapsed: 0.048 s
% 14.72/2.83 % (2819790)Peak memory usage: 89 MB
% 14.72/2.83 % (2819790)Instructions burned: 146 (million)
% 14.72/2.83 % (2819799)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1733638415: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)
% 21.33/3.73 % (2819805)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=575804853:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 21.33/3.73 % (2819799)Instruction limit reached!
% 21.33/3.73 % (2819799)------------------------------
% 21.33/3.73 % (2819799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.73 % (2819799)CaDiCaL version: 2.1.3
% 21.33/3.73 % (2819799)Termination reason: Instruction limit
% 21.33/3.73 % (2819799)Termination phase: Saturation
% 21.33/3.73 % (2819799)Time elapsed: 0.100 s
% 21.33/3.73 % (2819799)Peak memory usage: 89 MB
% 21.33/3.73 % (2819799)Instructions burned: 190 (million)
% 21.33/3.73 % (2819807)lrs+10_64_to=lpo:sil=8000:random_seed=1998999556:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.33/3.73 % (2819807)Instruction limit reached!
% 21.33/3.73 % (2819807)------------------------------
% 21.33/3.73 % (2819807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.73 % (2819807)CaDiCaL version: 2.1.3
% 21.33/3.73 % (2819807)Termination reason: Instruction limit
% 21.33/3.73 % (2819807)Termination phase: Saturation
% 21.33/3.73 % (2819807)Time elapsed: 0.041 s
% 21.33/3.73 % (2819807)Peak memory usage: 88 MB
% 21.33/3.73 % (2819807)Instructions burned: 129 (million)
% 21.33/3.73 % (2819805)Instruction limit reached!
% 21.33/3.73 % (2819805)------------------------------
% 21.33/3.73 % (2819805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.73 % (2819805)CaDiCaL version: 2.1.3
% 21.33/3.73 % (2819805)Termination reason: Instruction limit
% 21.33/3.73 % (2819805)Termination phase: Saturation
% 21.33/3.73 % (2819805)Time elapsed: 0.126 s
% 21.33/3.73 % (2819805)Peak memory usage: 90 MB
% 21.33/3.73 % (2819805)Instructions burned: 220 (million)
% 21.33/3.73 % (2819744)------------------------------
% 21.33/3.73 % (2819744)------------------------------
% 21.33/3.73 % (2819811)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2366981876:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 21.33/3.73 % (2819813)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3860780927:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 21.33/3.73 % (2819812)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2473463775:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 21.33/3.73 % (2819814)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=2205250373:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 21.33/3.73 % (2819811)Instruction limit reached!
% 21.33/3.73 % (2819811)------------------------------
% 21.33/3.73 % (2819811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.73 % (2819811)CaDiCaL version: 2.1.3
% 21.33/3.73 % (2819811)Termination reason: Instruction limit
% 21.33/3.73 % (2819811)Termination phase: Saturation
% 21.33/3.73 % (2819811)Time elapsed: 0.124 s
% 21.33/3.73 % (2819811)Peak memory usage: 88 MB
% 21.33/3.73 % (2819811)Instructions burned: 194 (million)
% 21.33/3.73 % (2819812)Instruction limit reached!
% 21.33/3.73 % (2819812)------------------------------
% 21.33/3.73 % (2819812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.33/3.73 % (2819812)CaDiCaL version: 2.1.3
% 21.33/3.73 % (2819812)Termination reason: Instruction limit
% 21.33/3.73 % (2819812)Termination phase: Saturation
% 21.33/3.73 % (2819812)Time elapsed: 0.100 s
% 21.33/3.73 % (2819812)Peak memory usage: 90 MB
% 21.33/3.73 % (2819812)Instructions burned: 158 (million)
% 21.33/3.73 % (2819814)Instruction limit reached!
% 21.33/3.73 % (2819814)------------------------------
% 21.33/3.73 % (2819814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.33/3.73 % (2819814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.34 % (2819814)CaDiCaL version: 2.1.3
% 32.84/5.34 % (2819814)Termination reason: Instruction limit
% 32.84/5.34 % (2819814)Termination phase: Saturation
% 32.84/5.34 % (2819814)Time elapsed: 0.061 s
% 32.84/5.34 % (2819814)Peak memory usage: 89 MB
% 32.84/5.34 % (2819814)Instructions burned: 106 (million)
% 32.84/5.34 % (2819819)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2846852936:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 32.84/5.34 % (2819820)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2233134696:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 32.84/5.34 % (2819821)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3220179471:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 32.84/5.34 % (2819819)Instruction limit reached!
% 32.84/5.34 % (2819819)------------------------------
% 32.84/5.34 % (2819819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.35 % (2819819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.35 % (2819819)CaDiCaL version: 2.1.3
% 32.84/5.35 % (2819819)Termination reason: Instruction limit
% 32.84/5.35 % (2819819)Termination phase: Saturation
% 32.84/5.35 % (2819819)Time elapsed: 0.109 s
% 32.84/5.35 % (2819819)Peak memory usage: 89 MB
% 32.84/5.35 % (2819819)Instructions burned: 107 (million)
% 32.84/5.35 % (2819820)Instruction limit reached!
% 32.84/5.35 % (2819820)------------------------------
% 32.84/5.35 % (2819820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.35 % (2819820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.35 % (2819820)CaDiCaL version: 2.1.3
% 32.84/5.35 % (2819820)Termination reason: Instruction limit
% 32.84/5.35 % (2819820)Termination phase: Saturation
% 32.84/5.35 % (2819820)Time elapsed: 0.215 s
% 32.84/5.35 % (2819820)Peak memory usage: 88 MB
% 32.84/5.35 % (2819820)Instructions burned: 243 (million)
% 32.84/5.35 % (2819841)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2346614431:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 32.84/5.35 % (2819841)Refutation not found, incomplete strategy
% 32.84/5.35 % (2819841)------------------------------
% 32.84/5.35 % (2819841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.35 % (2819841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.35 % (2819841)CaDiCaL version: 2.1.3
% 32.84/5.35 % (2819841)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.35 % (2819841)Time elapsed: 0.006 s
% 32.84/5.35 % (2819841)Peak memory usage: 88 MB
% 32.84/5.35 % (2819841)Instructions burned: 4 (million)
% 32.84/5.35 % (2819845)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3155403029:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 32.84/5.35 % (2819841)------------------------------
% 32.84/5.35 % (2819841)------------------------------
% 32.84/5.35 % (2819845)Instruction limit reached!
% 32.84/5.35 % (2819845)------------------------------
% 32.84/5.35 % (2819845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.35 % (2819845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.35 % (2819845)CaDiCaL version: 2.1.3
% 32.84/5.35 % (2819845)Termination reason: Instruction limit
% 32.84/5.35 % (2819845)Termination phase: Saturation
% 32.84/5.35 % (2819845)Time elapsed: 0.351 s
% 32.84/5.35 % (2819845)Peak memory usage: 91 MB
% 32.84/5.35 % (2819845)Instructions burned: 500 (million)
% 32.84/5.35 % (2819857)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1034111889:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 32.84/5.35 % (2819858)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=667464168:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi)
% 32.84/5.35 % (2819857)Instruction limit reached!
% 32.84/5.35 % (2819857)------------------------------
% 32.84/5.35 % (2819857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.35 % (2819857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.35 % (2819857)CaDiCaL version: 2.1.3
% 32.84/5.35 % (2819857)Termination reason: Instruction limit
% 32.84/5.35 % (2819857)Termination phase: Saturation
% 32.84/5.35 % (2819857)Time elapsed: 0.168 s
% 33.42/5.46 % (2819857)Peak memory usage: 90 MB
% 33.42/5.46 % (2819857)Instructions burned: 192 (million)
% 33.42/5.46 % (2819858)Instruction limit reached!
% 33.42/5.46 % (2819858)------------------------------
% 33.42/5.46 % (2819858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819858)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819858)Termination reason: Instruction limit
% 33.42/5.46 % (2819858)Termination phase: Saturation
% 33.42/5.46 % (2819858)Time elapsed: 0.161 s
% 33.42/5.46 % (2819858)Peak memory usage: 90 MB
% 33.42/5.46 % (2819858)Instructions burned: 265 (million)
% 33.42/5.46 % (2819862)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=683989355:cond=on:i=156:bs=on:gtg=exists_all:er=known_2978 on theBenchmark for (2978ds/156Mi)
% 33.42/5.46 % (2819865)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=1086636312:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 33.42/5.46 % (2819862)Instruction limit reached!
% 33.42/5.46 % (2819862)------------------------------
% 33.42/5.46 % (2819862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819862)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819862)Termination reason: Instruction limit
% 33.42/5.46 % (2819862)Termination phase: Saturation
% 33.42/5.46 % (2819862)Time elapsed: 0.094 s
% 33.42/5.46 % (2819862)Peak memory usage: 88 MB
% 33.42/5.46 % (2819862)Instructions burned: 156 (million)
% 33.42/5.46 % (2819933)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3803715854:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi)
% 33.42/5.46 % (2819933)Instruction limit reached!
% 33.42/5.46 % (2819933)------------------------------
% 33.42/5.46 % (2819933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819933)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819933)Termination reason: Instruction limit
% 33.42/5.46 % (2819933)Termination phase: Saturation
% 33.42/5.46 % (2819933)Time elapsed: 0.263 s
% 33.42/5.46 % (2819933)Peak memory usage: 88 MB
% 33.42/5.46 % (2819933)Instructions burned: 538 (million)
% 33.42/5.46 % (2819813)Instruction limit reached!
% 33.42/5.46 % (2819813)------------------------------
% 33.42/5.46 % (2819813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819813)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819813)Termination reason: Instruction limit
% 33.42/5.46 % (2819813)Termination phase: Saturation
% 33.42/5.46 % (2819813)Time elapsed: 2.210 s
% 33.42/5.46 % (2819813)Peak memory usage: 151 MB
% 33.42/5.46 % (2819813)Instructions burned: 3395 (million)
% 33.42/5.46 % (2820016)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=376124908:i=180:bd=preordered:av=off_2971 on theBenchmark for (2971ds/180Mi)
% 33.42/5.46 % (2820021)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=3623693498:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/10307Mi)
% 33.42/5.46 % (2819821)Instruction limit reached!
% 33.42/5.46 % (2819821)------------------------------
% 33.42/5.46 % (2819821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819821)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819821)Termination reason: Instruction limit
% 33.42/5.46 % (2819821)Termination phase: Saturation
% 33.42/5.46 % (2819821)Time elapsed: 2.024 s
% 33.42/5.46 % (2819821)Peak memory usage: 154 MB
% 33.42/5.46 % (2819821)Instructions burned: 5209 (million)
% 33.42/5.46 % (2820016)Instruction limit reached!
% 33.42/5.46 % (2820016)------------------------------
% 33.42/5.46 % (2820016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2820016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2820016)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2820016)Termination reason: Instruction limit
% 33.42/5.46 % (2820016)Termination phase: Saturation
% 33.42/5.46 % (2820016)Time elapsed: 0.091 s
% 33.42/5.46 % (2820016)Peak memory usage: 89 MB
% 33.42/5.46 % (2820016)Instructions burned: 182 (million)
% 33.42/5.46 % (2820025)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=754243770:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 33.42/5.46 % (2820024)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=1503847323:i=412:gtgl=4:gtg=exists_all_2969 on theBenchmark for (2969ds/412Mi)
% 33.42/5.46 % (2820024)Instruction limit reached!
% 33.42/5.46 % (2820024)------------------------------
% 33.42/5.46 % (2820024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2820024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2820024)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2820024)Termination reason: Instruction limit
% 33.42/5.46 % (2820024)Termination phase: Saturation
% 33.42/5.46 % (2820024)Time elapsed: 0.263 s
% 33.42/5.46 % (2820024)Peak memory usage: 91 MB
% 33.42/5.46 % (2820024)Instructions burned: 413 (million)
% 33.42/5.46 % (2820028)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=61906907:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2965 on theBenchmark for (2965ds/303Mi)
% 33.42/5.46 % (2820028)Refutation not found, incomplete strategy
% 33.42/5.46 % (2820028)------------------------------
% 33.42/5.46 % (2820028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2820028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2820028)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2820028)Termination reason: Refutation not found, incomplete strategy
% 33.42/5.46 % (2820028)Time elapsed: 0.002 s
% 33.42/5.46 % (2820028)Peak memory usage: 88 MB
% 33.42/5.46 % (2820028)Instructions burned: 1 (million)
% 33.42/5.46 % (2820028)------------------------------
% 33.42/5.46 % (2820028)------------------------------
% 33.42/5.46 % (2820030)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3716417705:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 33.42/5.46 % (2819865)Instruction limit reached!
% 33.42/5.46 % (2819865)------------------------------
% 33.42/5.46 % (2819865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2819865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2819865)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2819865)Termination reason: Instruction limit
% 33.42/5.46 % (2819865)Termination phase: Saturation
% 33.42/5.46 % (2819865)Time elapsed: 1.807 s
% 33.42/5.46 % (2819865)Peak memory usage: 142 MB
% 33.42/5.46 % (2819865)Instructions burned: 3258 (million)
% 33.42/5.46 % (2820032)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=289941211:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi)
% 33.42/5.46 % (2820030)Instruction limit reached!
% 33.42/5.46 % (2820030)------------------------------
% 33.42/5.46 % (2820030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2820030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2820030)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2820030)Termination reason: Instruction limit
% 33.42/5.46 % (2820030)Termination phase: Saturation
% 33.42/5.46 % (2820030)Time elapsed: 0.361 s
% 33.42/5.46 % (2820030)Peak memory usage: 91 MB
% 33.42/5.46 % (2820030)Instructions burned: 720 (million)
% 33.42/5.46 % (2819741)First to succeed.
% 33.42/5.46 % (2819741)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2819654"
% 33.42/5.46 % (2820034)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=732378374:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi)
% 33.42/5.46 % (2820032)Instruction limit reached!
% 33.42/5.46 % (2820032)------------------------------
% 33.42/5.46 % (2820032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.42/5.46 % (2820032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.42/5.46 % (2820032)CaDiCaL version: 2.1.3
% 33.42/5.46 % (2820032)Termination reason: Instruction limit
% 33.42/5.46 % (2820032)Termination phase: Saturation
% 33.42/5.46 % (2820032)Time elapsed: 0.325 s
% 33.42/5.46 % (2820032)Peak memory usage: 90 MB
% 33.42/5.46 % (2820032)Instructions burned: 598 (million)
% 33.42/5.46 % (2819741)Refutation found. Thanks to Tanya!
% 33.42/5.46 % SZS status Unsatisfiable for theBenchmark
% 33.42/5.46 % SZS output start Proof for theBenchmark
% See solution above
% 34.35/5.66 % (2819741)------------------------------
% 34.35/5.66 % (2819741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.35/5.66 % (2819741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.35/5.66 % (2819741)CaDiCaL version: 2.1.3
% 34.35/5.66 % (2819741)Termination reason: Refutation
% 34.35/5.66 % (2819741)Time elapsed: 4.346 s
% 34.35/5.66 % (2819741)Peak memory usage: 175 MB
% 34.35/5.66 % (2819741)Instructions burned: 6372 (million)
% 34.35/5.66 % (2819741)------------------------------
% 34.35/5.66 % (2819741)------------------------------
% 34.35/5.66 % (2819654)Success in time 4.774 s
% 34.35/5.66 % Vampire exiting
%------------------------------------------------------------------------------