%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG008-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 12:35:41 PM UTC 2026
% Result : Unsatisfiable 6.75s 2.18s
% Output : Refutation 6.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 19
% Syntax : Number of formulae : 125 ( 74 unt; 0 def)
% Number of atoms : 224 ( 25 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 199 ( 100 ~; 99 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 252 ( 252 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : sum(additive_identity,X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',additive_identity1) ).
fof(f2,axiom,
! [X0] : sum(X0,additive_identity,X0),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',additive_identity2) ).
fof(f3,axiom,
! [X0,X1] : product(X0,X1,multiply(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',closure_of_multiplication) ).
fof(f4,axiom,
! [X0,X1] : sum(X0,X1,add(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',closure_of_addition) ).
fof(f5,axiom,
! [X0] : sum(additive_inverse(X0),X0,additive_identity),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',left_inverse) ).
fof(f6,axiom,
! [X0] : sum(X0,additive_inverse(X0),additive_identity),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',right_inverse) ).
fof(f7,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X2,X3,X5)
| ~ sum(X1,X3,X4)
| ~ sum(X0,X1,X2)
| sum(X0,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',associativity_of_addition1) ).
fof(f8,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X0,X4,X5)
| ~ sum(X1,X3,X4)
| ~ sum(X0,X1,X2)
| sum(X2,X3,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',associativity_of_addition2) ).
fof(f9,axiom,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(X1,X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',commutativity_of_addition) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X2,X3,X5)
| ~ product(X1,X3,X4)
| ~ product(X0,X1,X2)
| product(X0,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',associativity_of_multiplication1) ).
fof(f12,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/Axioms/RNG001-0.ax',distributivity1) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X1,X2)
| ~ product(X0,X3,X4)
| ~ sum(X1,X3,X5)
| ~ sum(X2,X4,X6)
| product(X0,X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',distributivity2) ).
fof(f14,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/Axioms/RNG001-0.ax',distributivity3) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(X0,X1,X2)
| ~ product(X3,X1,X4)
| ~ sum(X0,X3,X5)
| ~ sum(X2,X4,X6)
| product(X5,X1,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',distributivity4) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',addition_is_well_defined) ).
fof(f17,axiom,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/RNG001-0.ax',multiplication_is_well_defined) ).
fof(f18,axiom,
! [X0] : product(X0,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_squared_is_x) ).
fof(f19,axiom,
product(a,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_b_is_c) ).
fof(f20,negated_conjecture,
~ product(b,a,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_b_times_a_is_c) ).
fof(f25,plain,
! [X0,X1] : sum(X0,X1,add(X1,X0)),
inference(resolution,[],[f9,f4]) ).
fof(f27,plain,
! [X0,X1] :
( ~ sum(additive_identity,X0,X1)
| X0 = X1 ),
inference(resolution,[],[f16,f1]) ).
fof(f28,plain,
! [X0,X1] :
( ~ sum(X0,additive_identity,X1)
| X0 = X1 ),
inference(resolution,[],[f16,f2]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| add(X0,X1) = X2 ),
inference(resolution,[],[f16,f4]) ).
fof(f34,plain,
! [X2,X0,X1] :
( ~ product(X0,X1,X2)
| multiply(X0,X1) = X2 ),
inference(resolution,[],[f17,f3]) ).
fof(f46,plain,
! [X0] : add(X0,additive_identity) = X0,
inference(resolution,[],[f27,f25]) ).
fof(f47,plain,
! [X2,X3,X0,X1] :
( ~ sum(X3,X0,additive_identity)
| ~ sum(X0,X1,X2)
| sum(X3,X2,X1) ),
inference(resolution,[],[f7,f1]) ).
fof(f55,plain,
! [X2,X3,X0,X1] :
( ~ sum(additive_inverse(X2),X0,X3)
| ~ sum(X0,X1,X2)
| sum(X3,X1,additive_identity) ),
inference(resolution,[],[f8,f5]) ).
fof(f59,plain,
! [X2,X3,X0,X1] :
( ~ product(X3,X0,X1)
| ~ product(X0,X1,X2)
| product(X3,X2,X1) ),
inference(resolution,[],[f10,f18]) ).
fof(f60,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X0,X4)
| ~ product(X0,X1,X2)
| product(X3,X2,multiply(X4,X1)) ),
inference(resolution,[],[f10,f3]) ).
fof(f61,plain,
! [X2,X0,X1] :
( ~ product(X2,X0,a)
| ~ product(X0,b,X1)
| product(X2,X1,c) ),
inference(resolution,[],[f10,f19]) ).
fof(f67,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X0,X3,X4)
| ~ sum(X3,X1,X0)
| ~ product(X0,X1,X2)
| sum(X4,X2,X0) ),
inference(resolution,[],[f12,f18]) ).
fof(f68,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,[],[f12,f3]) ).
fof(f70,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X0,X1,X2)
| ~ sum(X0,X1,X3)
| ~ sum(X0,X2,X4)
| product(X0,X3,X4) ),
inference(resolution,[],[f13,f18]) ).
fof(f71,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X0,X1,X2)
| ~ sum(X3,X1,X4)
| ~ sum(multiply(X0,X3),X2,X5)
| product(X0,X4,X5) ),
inference(resolution,[],[f13,f3]) ).
fof(f73,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X3,X1,X4)
| ~ sum(X3,X0,X1)
| ~ product(X0,X1,X2)
| sum(X4,X2,X1) ),
inference(resolution,[],[f14,f18]) ).
fof(f74,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(X3,X1,X5)
| ~ sum(X3,X0,X4)
| ~ product(X0,X1,X2)
| sum(X5,X2,multiply(X4,X1)) ),
inference(resolution,[],[f14,f3]) ).
fof(f76,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X0,X1,X2)
| ~ sum(X1,X0,X3)
| ~ sum(X1,X2,X4)
| product(X3,X1,X4) ),
inference(resolution,[],[f15,f18]) ).
fof(f99,plain,
! [X0,X1] : add(X0,X1) = add(X1,X0),
inference(resolution,[],[f31,f25]) ).
fof(f108,plain,
! [X2,X0,X1] :
( ~ product(X0,multiply(X1,X0),X2)
| product(X1,X2,multiply(X1,X0)) ),
inference(resolution,[],[f59,f3]) ).
fof(f110,plain,
! [X0] :
( ~ product(a,b,X0)
| product(a,X0,c) ),
inference(resolution,[],[f61,f18]) ).
fof(f115,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(additive_inverse(X0),X2,X1) ),
inference(resolution,[],[f47,f5]) ).
fof(f116,plain,
! [X2,X0,X1] :
( ~ sum(additive_inverse(X0),X1,X2)
| sum(X0,X2,X1) ),
inference(resolution,[],[f47,f6]) ).
fof(f175,plain,
! [X0,X1] :
( ~ sum(X0,X1,X0)
| sum(additive_identity,X1,additive_identity) ),
inference(resolution,[],[f55,f5]) ).
fof(f203,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X2)
| product(X3,X2,multiply(multiply(X3,X0),X1)) ),
inference(resolution,[],[f60,f3]) ).
fof(f204,plain,
! [X0,X1] :
( ~ product(b,X0,X1)
| product(a,X1,multiply(c,X0)) ),
inference(resolution,[],[f60,f19]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X0)
| ~ product(X0,X1,X2)
| sum(X0,X2,X0) ),
inference(resolution,[],[f67,f18]) ).
fof(f227,plain,
product(a,c,c),
inference(resolution,[],[f110,f19]) ).
fof(f231,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,multiply(X0,X1),X3)
| ~ sum(X0,X1,X2)
| product(X0,X2,X3) ),
inference(resolution,[],[f70,f3]) ).
fof(f241,plain,
c = multiply(a,c),
inference(resolution,[],[f227,f34]) ).
fof(f252,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X0)
| ~ product(X1,X0,X2)
| sum(X0,X2,X0) ),
inference(resolution,[],[f73,f18]) ).
fof(f261,plain,
! [X2,X3,X0,X1] :
( ~ sum(X0,multiply(X1,X0),X3)
| ~ sum(X0,X1,X2)
| product(X2,X0,X3) ),
inference(resolution,[],[f76,f3]) ).
fof(f262,plain,
! [X0,X1] :
( ~ sum(b,c,X1)
| ~ sum(b,a,X0)
| product(X0,b,X1) ),
inference(resolution,[],[f76,f19]) ).
fof(f268,plain,
! [X2,X3,X0,X1] :
( ~ product(X0,X1,X3)
| ~ sum(X0,X1,X2)
| sum(X0,X3,multiply(X0,X2)) ),
inference(resolution,[],[f68,f18]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( ~ sum(multiply(X1,X0),X1,X3)
| ~ sum(X0,X1,X2)
| product(X1,X2,X3) ),
inference(resolution,[],[f71,f18]) ).
fof(f278,plain,
! [X2,X3,X0,X1] :
( ~ product(X1,X0,X3)
| ~ sum(X0,X1,X2)
| sum(X0,X3,multiply(X2,X0)) ),
inference(resolution,[],[f74,f18]) ).
fof(f279,plain,
! [X2,X3,X0,X1,X4] :
( ~ product(X1,X3,X4)
| ~ sum(X0,X1,X2)
| sum(multiply(X0,X3),X4,multiply(X2,X3)) ),
inference(resolution,[],[f74,f3]) ).
fof(f350,plain,
! [X0] : sum(additive_inverse(additive_inverse(X0)),additive_identity,X0),
inference(resolution,[],[f115,f5]) ).
fof(f359,plain,
! [X0,X1] : sum(X0,add(X1,additive_inverse(X0)),X1),
inference(resolution,[],[f116,f25]) ).
fof(f365,plain,
! [X0] : additive_inverse(additive_inverse(X0)) = X0,
inference(resolution,[],[f350,f28]) ).
fof(f515,plain,
! [X0] : product(a,multiply(b,X0),multiply(c,X0)),
inference(resolution,[],[f204,f3]) ).
fof(f1084,plain,
! [X0,X1] :
( ~ product(X0,additive_identity,X1)
| sum(X0,X1,X0) ),
inference(resolution,[],[f221,f2]) ).
fof(f1112,plain,
! [X0,X1] :
( ~ product(additive_identity,X0,X1)
| sum(X0,X1,X0) ),
inference(resolution,[],[f252,f2]) ).
fof(f1135,plain,
! [X0] :
( ~ sum(b,a,X0)
| product(X0,b,add(b,c)) ),
inference(resolution,[],[f262,f4]) ).
fof(f1231,plain,
! [X0,X1] : product(X0,X1,multiply(multiply(X0,X1),X1)),
inference(resolution,[],[f203,f18]) ).
fof(f1232,plain,
! [X2,X0,X1] : product(X0,multiply(X1,X2),multiply(multiply(X0,X1),X2)),
inference(resolution,[],[f203,f3]) ).
fof(f1256,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| product(X0,X2,add(X0,multiply(X0,X1))) ),
inference(resolution,[],[f231,f4]) ).
fof(f1286,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| product(X2,X0,add(X0,multiply(X1,X0))) ),
inference(resolution,[],[f261,f4]) ).
fof(f1303,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(X0,multiply(X0,X1),multiply(X0,X2)) ),
inference(resolution,[],[f268,f3]) ).
fof(f1317,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| product(X1,X2,add(X1,multiply(X1,X0))) ),
inference(resolution,[],[f273,f25]) ).
fof(f1336,plain,
! [X0] :
( ~ sum(b,a,X0)
| sum(b,c,multiply(X0,b)) ),
inference(resolution,[],[f278,f19]) ).
fof(f1419,plain,
! [X2,X0,X1] :
( ~ sum(X0,X1,X2)
| sum(multiply(X0,X1),X1,multiply(X2,X1)) ),
inference(resolution,[],[f279,f18]) ).
fof(f1488,plain,
product(b,multiply(c,a),multiply(b,a)),
inference(resolution,[],[f515,f108]) ).
fof(f1661,plain,
! [X0] : sum(X0,multiply(X0,additive_identity),X0),
inference(resolution,[],[f1084,f3]) ).
fof(f1668,plain,
! [X0] : sum(additive_identity,multiply(X0,additive_identity),additive_identity),
inference(resolution,[],[f1661,f175]) ).
fof(f1734,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(resolution,[],[f1668,f27]) ).
fof(f1796,plain,
! [X0] : sum(X0,multiply(additive_identity,X0),X0),
inference(resolution,[],[f1112,f3]) ).
fof(f1892,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X1),X1),
inference(resolution,[],[f1231,f34]) ).
fof(f2232,plain,
! [X0] : sum(additive_identity,multiply(additive_identity,X0),additive_identity),
inference(resolution,[],[f1796,f175]) ).
fof(f2628,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(resolution,[],[f2232,f27]) ).
fof(f3776,plain,
product(add(a,b),b,add(b,c)),
inference(resolution,[],[f1135,f25]) ).
fof(f3913,plain,
sum(b,c,multiply(add(a,b),b)),
inference(resolution,[],[f1336,f25]) ).
fof(f4579,plain,
! [X0,X1] : product(X0,multiply(multiply(X1,X0),X1),multiply(X0,X1)),
inference(resolution,[],[f1232,f108]) ).
fof(f5137,plain,
! [X0,X1] : product(X0,X1,add(X0,multiply(X0,add(X1,additive_inverse(X0))))),
inference(resolution,[],[f1256,f359]) ).
fof(f5331,plain,
! [X0,X1] : product(X0,X1,add(X1,multiply(add(X0,additive_inverse(X1)),X1))),
inference(resolution,[],[f1286,f359]) ).
fof(f5342,plain,
! [X0,X1] : product(add(X0,X1),X0,add(X0,multiply(X1,X0))),
inference(resolution,[],[f1286,f4]) ).
fof(f5448,plain,
! [X0] : sum(X0,multiply(X0,additive_inverse(X0)),multiply(X0,additive_identity)),
inference(resolution,[],[f1303,f6]) ).
fof(f5493,plain,
! [X0] : sum(X0,multiply(X0,additive_inverse(X0)),additive_identity),
inference(forward_demodulation,[],[f5448,f1734]) ).
fof(f5547,plain,
! [X0] : sum(X0,additive_identity,multiply(additive_inverse(X0),additive_inverse(additive_inverse(X0)))),
inference(resolution,[],[f5493,f116]) ).
fof(f5556,plain,
! [X0] : sum(X0,additive_identity,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f5547,f365]) ).
fof(f6292,plain,
! [X0] : sum(multiply(additive_inverse(X0),X0),X0,multiply(additive_identity,X0)),
inference(resolution,[],[f1419,f5]) ).
fof(f6327,plain,
! [X0] : sum(multiply(additive_inverse(X0),X0),X0,additive_identity),
inference(forward_demodulation,[],[f6292,f2628]) ).
fof(f7577,plain,
! [X0] : multiply(additive_inverse(X0),X0) = X0,
inference(resolution,[],[f5556,f28]) ).
fof(f7799,plain,
! [X0] : sum(X0,X0,additive_identity),
inference(superposition,[],[f6327,f7577]) ).
fof(f8090,plain,
! [X0] : additive_identity = add(X0,X0),
inference(resolution,[],[f7799,f31]) ).
fof(f8096,plain,
! [X0] : sum(additive_inverse(X0),additive_identity,X0),
inference(resolution,[],[f7799,f115]) ).
fof(f8496,plain,
! [X0] : additive_inverse(X0) = X0,
inference(resolution,[],[f8096,f28]) ).
fof(f8720,plain,
add(b,c) = multiply(add(a,b),b),
inference(resolution,[],[f3776,f34]) ).
fof(f8933,plain,
sum(additive_inverse(b),multiply(add(a,b),b),c),
inference(resolution,[],[f3913,f115]) ).
fof(f8983,plain,
sum(b,multiply(add(a,b),b),c),
inference(forward_demodulation,[],[f8933,f8496]) ).
fof(f12498,plain,
product(add(c,a),c,add(c,c)),
inference(superposition,[],[f5342,f241]) ).
fof(f12504,plain,
product(add(c,a),c,additive_identity),
inference(forward_demodulation,[],[f12498,f8090]) ).
fof(f12524,plain,
product(add(a,c),c,additive_identity),
inference(forward_demodulation,[],[f12504,f99]) ).
fof(f12829,plain,
additive_identity = multiply(add(a,c),c),
inference(resolution,[],[f12524,f34]) ).
fof(f13596,plain,
product(c,multiply(additive_identity,add(a,c)),multiply(c,add(a,c))),
inference(superposition,[],[f4579,f12829]) ).
fof(f13609,plain,
product(c,additive_identity,multiply(c,add(a,c))),
inference(forward_demodulation,[],[f13596,f2628]) ).
fof(f17943,plain,
product(multiply(add(a,b),b),c,add(multiply(add(a,b),b),multiply(multiply(add(a,b),b),b))),
inference(resolution,[],[f8983,f1317]) ).
fof(f17966,plain,
product(multiply(add(a,b),b),c,add(multiply(add(a,b),b),multiply(add(a,b),b))),
inference(forward_demodulation,[],[f17943,f1892]) ).
fof(f17979,plain,
product(multiply(add(a,b),b),c,additive_identity),
inference(forward_demodulation,[],[f17966,f8090]) ).
fof(f20653,plain,
! [X0,X1] : product(X0,X1,add(X0,multiply(X0,add(X1,X0)))),
inference(forward_demodulation,[],[f5137,f8496]) ).
fof(f21763,plain,
! [X0,X1] : product(X0,X1,add(X1,multiply(add(X0,X1),X1))),
inference(forward_demodulation,[],[f5331,f8496]) ).
fof(f45325,plain,
multiply(c,additive_identity) = multiply(c,add(a,c)),
inference(resolution,[],[f13609,f34]) ).
fof(f45359,plain,
additive_identity = multiply(c,add(a,c)),
inference(forward_demodulation,[],[f45325,f1734]) ).
fof(f45396,plain,
product(c,a,add(c,additive_identity)),
inference(superposition,[],[f20653,f45359]) ).
fof(f45503,plain,
product(c,a,c),
inference(forward_demodulation,[],[f45396,f46]) ).
fof(f45681,plain,
c = multiply(c,a),
inference(resolution,[],[f45503,f34]) ).
fof(f45865,plain,
product(b,c,multiply(b,a)),
inference(superposition,[],[f1488,f45681]) ).
fof(f50362,plain,
multiply(b,c) = multiply(b,a),
inference(resolution,[],[f45865,f34]) ).
fof(f104100,plain,
product(add(b,c),c,additive_identity),
inference(superposition,[],[f17979,f8720]) ).
fof(f104520,plain,
additive_identity = multiply(add(b,c),c),
inference(resolution,[],[f104100,f34]) ).
fof(f104558,plain,
product(b,c,add(c,additive_identity)),
inference(superposition,[],[f21763,f104520]) ).
fof(f104839,plain,
product(b,c,c),
inference(forward_demodulation,[],[f104558,f46]) ).
fof(f104948,plain,
c = multiply(b,c),
inference(resolution,[],[f104839,f34]) ).
fof(f105861,plain,
c = multiply(b,a),
inference(superposition,[],[f104948,f50362]) ).
fof(f107264,plain,
product(b,a,c),
inference(superposition,[],[f3,f105861]) ).
fof(f107430,plain,
$false,
inference(forward_subsumption_resolution,[],[f107264,f20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.20/0.46 % Computer : n026.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Sun Sep 27 23:01:11 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.24/0.51 Running first-order model finding
% 0.24/0.51 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.75/2.18 % (3310313)Will run a generic schedule for satisfiability detection.
% 6.75/2.18 % (3310321)dis+10_1_sil=32000:sp=arity:random_seed=754034791:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.75/2.18 % (3310318)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2083226800_2999 on theBenchmark for (2999ds/0Mi)
% 6.75/2.18 % (3310320)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1751429224:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.75/2.18 % (3310323)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=761800779:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.75/2.18 % (3310324)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2110662699:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.75/2.18 % (3310322)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2059166150:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.75/2.18 % TRYING [1]
% 6.75/2.18 % TRYING [2]
% 6.75/2.18 % (3310319)% WARNING: option uhcvi not known.
% 6.75/2.18 % TRYING [3]
% 6.75/2.18 % (3310319)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3469279841:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.75/2.18 % TRYING [4]
% 6.75/2.18 % TRYING [5]
% 6.75/2.18 % (3310322)Instruction limit reached!
% 6.75/2.18 % (3310322)------------------------------
% 6.75/2.18 % (3310322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310322)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310322)Termination reason: Instruction limit
% 6.75/2.18 % (3310322)Termination phase: Saturation
% 6.75/2.18 % (3310322)Time elapsed: 0.098 s
% 6.75/2.18 % (3310322)Peak memory usage: 12 MB
% 6.75/2.18 % (3310322)Instructions burned: 116 (million)
% 6.75/2.18 % (3310321)Instruction limit reached!
% 6.75/2.18 % (3310321)------------------------------
% 6.75/2.18 % (3310321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310321)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310321)Termination reason: Instruction limit
% 6.75/2.18 % (3310321)Termination phase: Saturation
% 6.75/2.18 % (3310321)Time elapsed: 0.101 s
% 6.75/2.18 % (3310321)Peak memory usage: 12 MB
% 6.75/2.18 % (3310321)Instructions burned: 103 (million)
% 6.75/2.18 % (3310323)Instruction limit reached!
% 6.75/2.18 % (3310323)------------------------------
% 6.75/2.18 % (3310323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310323)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310323)Termination reason: Instruction limit
% 6.75/2.18 % (3310323)Termination phase: Saturation
% 6.75/2.18 % (3310323)Time elapsed: 0.121 s
% 6.75/2.18 % (3310323)Peak memory usage: 12 MB
% 6.75/2.18 % (3310323)Instructions burned: 131 (million)
% 6.75/2.18 % (3310333)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1061927057:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.75/2.18 % (3310332)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2833684340:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.75/2.18 % TRYING [1]
% 6.75/2.18 % TRYING [2]
% 6.75/2.18 % TRYING [3]
% 6.75/2.18 % (3310334)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=375916146:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.75/2.18 % (3310324)Instruction limit reached!
% 6.75/2.18 % (3310324)------------------------------
% 6.75/2.18 % (3310324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310324)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310324)Termination reason: Instruction limit
% 6.75/2.18 % (3310324)Termination phase: Saturation
% 6.75/2.18 % (3310324)Time elapsed: 0.159 s
% 6.75/2.18 % (3310324)Peak memory usage: 12 MB
% 6.75/2.18 % (3310324)Instructions burned: 159 (million)
% 6.75/2.18 % TRYING [4]
% 6.75/2.18 % (3310338)ott-21_1_sil=16000:fs=off:random_seed=2686594825:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 6.75/2.18 % TRYING [6]
% 6.75/2.18 % TRYING [5]
% 6.75/2.18 % (3310333)Instruction limit reached!
% 6.75/2.18 % (3310333)------------------------------
% 6.75/2.18 % (3310333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310333)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310333)Termination reason: Instruction limit
% 6.75/2.18 % (3310333)Termination phase: Saturation
% 6.75/2.18 % (3310333)Time elapsed: 0.138 s
% 6.75/2.18 % (3310333)Peak memory usage: 12 MB
% 6.75/2.18 % (3310333)Instructions burned: 132 (million)
% 6.75/2.18 % (3310340)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1311111414:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 6.75/2.18 % (3310338)Instruction limit reached!
% 6.75/2.18 % (3310338)------------------------------
% 6.75/2.18 % (3310338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310338)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310338)Termination reason: Instruction limit
% 6.75/2.18 % (3310338)Termination phase: Saturation
% 6.75/2.18 % (3310338)Time elapsed: 0.158 s
% 6.75/2.18 % (3310338)Peak memory usage: 12 MB
% 6.75/2.18 % (3310338)Instructions burned: 181 (million)
% 6.75/2.18 % (3310342)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2857153281:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 6.75/2.18 % TRYING [1]
% 6.75/2.18 % TRYING [2]
% 6.75/2.18 % TRYING [3]
% 6.75/2.18 % TRYING [6]
% 6.75/2.18 % TRYING [4]
% 6.75/2.18 % TRYING [5]
% 6.75/2.18 % TRYING [7]
% 6.75/2.18 % (3310332)Instruction limit reached!
% 6.75/2.18 % (3310332)------------------------------
% 6.75/2.18 % (3310332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310332)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310332)Termination reason: Instruction limit
% 6.75/2.18 % (3310332)Termination phase: Finite model building constraint generation
% 6.75/2.18 % (3310332)Time elapsed: 0.519 s
% 6.75/2.18 % (3310332)Peak memory usage: 31 MB
% 6.75/2.18 % (3310332)Instructions burned: 715 (million)
% 6.75/2.18 % (3310344)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3342853184:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 6.75/2.18 % (3310334)Instruction limit reached!
% 6.75/2.18 % (3310334)------------------------------
% 6.75/2.18 % (3310334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310334)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310334)Termination reason: Instruction limit
% 6.75/2.18 % (3310334)Termination phase: Saturation
% 6.75/2.18 % (3310334)Time elapsed: 0.623 s
% 6.75/2.18 % (3310334)Peak memory usage: 17 MB
% 6.75/2.18 % (3310334)Instructions burned: 684 (million)
% 6.75/2.18 % (3310340)Instruction limit reached!
% 6.75/2.18 % (3310340)------------------------------
% 6.75/2.18 % (3310340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310340)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310340)Termination reason: Instruction limit
% 6.75/2.18 % (3310340)Termination phase: Saturation
% 6.75/2.18 % (3310340)Time elapsed: 0.483 s
% 6.75/2.18 % (3310340)Peak memory usage: 13 MB
% 6.75/2.18 % (3310340)Instructions burned: 478 (million)
% 6.75/2.18 % (3310346)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2094931655:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 6.75/2.18 % (3310347)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=4036674469:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 6.75/2.18 % TRYING [6]
% 6.75/2.18 % (3310342)Instruction limit reached!
% 6.75/2.18 % (3310342)------------------------------
% 6.75/2.18 % (3310342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310342)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310342)Termination reason: Instruction limit
% 6.75/2.18 % (3310342)Termination phase: Finite model building constraint generation
% 6.75/2.18 % (3310342)Time elapsed: 0.587 s
% 6.75/2.18 % (3310342)Peak memory usage: 23 MB
% 6.75/2.18 % (3310342)Instructions burned: 866 (million)
% 6.75/2.18 % (3310350)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2899678476:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 6.75/2.18 % TRYING [14]
% 6.75/2.18 % TRYING [8]
% 6.75/2.18 % (3310347)Instruction limit reached!
% 6.75/2.18 % (3310347)------------------------------
% 6.75/2.18 % (3310347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310347)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310347)Termination reason: Instruction limit
% 6.75/2.18 % (3310347)Termination phase: Saturation
% 6.75/2.18 % (3310347)Time elapsed: 0.648 s
% 6.75/2.18 % (3310347)Peak memory usage: 16 MB
% 6.75/2.18 % (3310347)Instructions burned: 692 (million)
% 6.75/2.18 % (3310352)fmb+10_1_sil=64000:random_seed=1140041639:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 6.75/2.18 % TRYING [1]
% 6.75/2.18 % TRYING [2]
% 6.75/2.18 % TRYING [3]
% 6.75/2.18 % (3310346)Instruction limit reached!
% 6.75/2.18 % (3310346)------------------------------
% 6.75/2.18 % (3310346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310346)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310346)Termination reason: Instruction limit
% 6.75/2.18 % (3310346)Termination phase: Finite model building constraint generation
% 6.75/2.18 % (3310346)Time elapsed: 0.708 s
% 6.75/2.18 % (3310346)Peak memory usage: 93 MB
% 6.75/2.18 % (3310346)Instructions burned: 889 (million)
% 6.75/2.18 % TRYING [4]
% 6.75/2.18 % (3310319) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3310313-3310319"...
% 6.75/2.18 % (3310319)...printing done.
% 6.75/2.18 % (3310354)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2041579370:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 6.75/2.18 % (3310319)Refutation found. Thanks to Tanya!
% 6.75/2.18 % SZS status Unsatisfiable for theBenchmark
% 6.75/2.18 % SZS output start Proof for theBenchmark
% See solution above
% 6.75/2.18 % (3310319)------------------------------
% 6.75/2.18 % (3310319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.75/2.18 % (3310319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.75/2.18 % (3310319)CaDiCaL version: 2.1.3
% 6.75/2.18 % (3310319)Termination reason: Refutation
% 6.75/2.18 % (3310319)Time elapsed: 1.580 s
% 6.75/2.18 % (3310319)Peak memory usage: 34 MB
% 6.75/2.18 % (3310319)Instructions burned: 3092 (million)
% 6.75/2.18 % (3310313)Success in time 1.654 s
% 6.75/2.18 % Vampire exiting
%------------------------------------------------------------------------------