%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG009-5 : 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 : 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 12:35:42 PM UTC 2026
% Result : Unsatisfiable 175.15s 29.30s
% Output : Refutation 204.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 103
% Number of leaves : 9
% Syntax : Number of formulae : 275 ( 275 unt; 0 def)
% Number of atoms : 275 ( 274 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 570 ( 570 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : add(X0,additive_identity) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_identity) ).
fof(f2,axiom,
! [X0] : add(X0,additive_inverse(X0)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_additive_inverse) ).
fof(f3,plain,
! [X0] : additive_identity = add(X0,additive_inverse(X0)),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = add(multiply(X0,X1),multiply(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distribute1) ).
fof(f5,axiom,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = add(multiply(X0,X2),multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distribute2) ).
fof(f6,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_addition) ).
fof(f7,axiom,
! [X0,X1] : add(X0,X1) = add(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutative_addition) ).
fof(f8,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_multiplication) ).
fof(f9,axiom,
! [X0] : multiply(X0,multiply(X0,X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_cubed_is_x) ).
fof(f10,negated_conjecture,
multiply(a,b) != multiply(b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_commutativity) ).
fof(f11,plain,
! [X0] : add(additive_identity,X0) = X0,
inference(superposition,[],[f7,f1]) ).
fof(f23,plain,
! [X0,X1] : add(additive_identity,X1) = add(X0,add(additive_inverse(X0),X1)),
inference(superposition,[],[f6,f3]) ).
fof(f37,plain,
! [X0,X1] : add(X0,add(additive_inverse(X0),X1)) = X1,
inference(forward_demodulation,[],[f23,f11]) ).
fof(f40,plain,
! [X0,X1] : add(X1,add(X0,additive_inverse(X1))) = X0,
inference(superposition,[],[f37,f7]) ).
fof(f44,plain,
! [X0] : add(X0,additive_identity) = additive_inverse(additive_inverse(X0)),
inference(superposition,[],[f37,f3]) ).
fof(f53,plain,
! [X0] : additive_inverse(additive_inverse(X0)) = X0,
inference(forward_demodulation,[],[f44,f1]) ).
fof(f56,plain,
! [X0,X1] : add(additive_inverse(X0),add(X0,X1)) = X1,
inference(superposition,[],[f37,f53]) ).
fof(f60,plain,
! [X0,X1] : add(additive_inverse(X0),add(X1,X0)) = X1,
inference(superposition,[],[f40,f53]) ).
fof(f669,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(superposition,[],[f8,f9]) ).
fof(f673,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))),
inference(superposition,[],[f9,f8]) ).
fof(f674,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X1))))),
inference(forward_demodulation,[],[f673,f8]) ).
fof(f678,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f669,f8]) ).
fof(f686,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),multiply(multiply(X0,X1),X2)))),
inference(superposition,[],[f8,f678]) ).
fof(f687,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X0,X1),X2))))),
inference(forward_demodulation,[],[f686,f8]) ).
fof(f692,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X1,X2)))))),
inference(forward_demodulation,[],[f687,f8]) ).
fof(f706,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,X1)) = multiply(X2,multiply(X0,multiply(X1,multiply(X2,multiply(multiply(X0,X1),multiply(X2,multiply(X0,X1))))))),
inference(superposition,[],[f674,f8]) ).
fof(f717,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,X1)) = multiply(X2,multiply(X0,multiply(X1,multiply(X2,multiply(X0,multiply(X1,multiply(X2,multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f706,f8]) ).
fof(f1966,plain,
! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,X1))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1))))))),
inference(superposition,[],[f678,f717]) ).
fof(f1970,plain,
! [X0,X1] : multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X1,X0))))) = multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,X0))))))),
inference(superposition,[],[f692,f717]) ).
fof(f1980,plain,
! [X0,X1] : multiply(X1,X0) = multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,X0))))))),
inference(forward_demodulation,[],[f1970,f674]) ).
fof(f1981,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f1966,f678]) ).
fof(f2103,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))),
inference(superposition,[],[f1980,f678]) ).
fof(f2136,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),X2)),
inference(superposition,[],[f8,f1980]) ).
fof(f2137,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X2,multiply(X2,multiply(multiply(X0,X1),multiply(X2,multiply(X2,multiply(multiply(X0,X1),X2)))))))),
inference(superposition,[],[f8,f1980]) ).
fof(f2138,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X2,multiply(X2,multiply(X0,multiply(X1,multiply(X2,multiply(X2,multiply(multiply(X0,X1),X2))))))))),
inference(forward_demodulation,[],[f2137,f8]) ).
fof(f2139,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),X2))),
inference(forward_demodulation,[],[f2136,f8]) ).
fof(f2154,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f2103,f8]) ).
fof(f2156,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X0,multiply(X1,multiply(X2,multiply(X2,multiply(X0,multiply(X1,multiply(X2,multiply(X2,multiply(X0,multiply(X1,X2)))))))))),
inference(forward_demodulation,[],[f2138,f8]) ).
fof(f2157,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),X2)))),
inference(forward_demodulation,[],[f2139,f8]) ).
fof(f2172,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X0,multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,X1)),multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f2154,f8]) ).
fof(f2174,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),X2))))),
inference(forward_demodulation,[],[f2157,f8]) ).
fof(f2186,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,X1)),multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))),
inference(forward_demodulation,[],[f2172,f678]) ).
fof(f2188,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),X2)))))),
inference(forward_demodulation,[],[f2174,f8]) ).
fof(f2196,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,X1),multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f2186,f8]) ).
fof(f2198,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),X2))))))),
inference(forward_demodulation,[],[f2188,f8]) ).
fof(f2206,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,multiply(X0,X1)),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f2196,f8]) ).
fof(f2208,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,X2)))))))),
inference(forward_demodulation,[],[f2198,f8]) ).
fof(f2216,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f2206,f8]) ).
fof(f2225,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f2216,f8]) ).
fof(f2234,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,X1)),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f2225,f678]) ).
fof(f2243,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,X1),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f2234,f8]) ).
fof(f2251,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f2243,f8]) ).
fof(f2350,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1)))))),X2)),
inference(superposition,[],[f8,f1981]) ).
fof(f2361,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1))))),X2))),
inference(forward_demodulation,[],[f2350,f8]) ).
fof(f2387,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1)))),X2)))),
inference(forward_demodulation,[],[f2361,f8]) ).
fof(f2411,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X0,multiply(X0,X1))),X2))))),
inference(forward_demodulation,[],[f2387,f8]) ).
fof(f2435,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,X1)),X2)))))),
inference(forward_demodulation,[],[f2411,f8]) ).
fof(f2457,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,X1),X2))))))),
inference(forward_demodulation,[],[f2435,f8]) ).
fof(f2474,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,X2)))))))),
inference(forward_demodulation,[],[f2457,f8]) ).
fof(f4000,plain,
! [X0,X1] : multiply(X0,multiply(X0,multiply(X0,X1))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,X1))))))))),
inference(superposition,[],[f678,f2156]) ).
fof(f4048,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f4000,f678]) ).
fof(f4905,plain,
! [X0,X1] : multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))) = multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,X1))))))),
inference(superposition,[],[f2474,f4048]) ).
fof(f6346,plain,
! [X0,X1] : multiply(X1,multiply(X0,multiply(X0,X1))) = multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X1))))))),
inference(superposition,[],[f2208,f2251]) ).
fof(f7342,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,X0))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,X0))))),
inference(superposition,[],[f692,f6346]) ).
fof(f7366,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,X0)))))),X2)),
inference(superposition,[],[f8,f6346]) ).
fof(f7390,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,X0))))),X2))),
inference(forward_demodulation,[],[f7366,f8]) ).
fof(f7427,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,X0)))),X2)))),
inference(forward_demodulation,[],[f7390,f8]) ).
fof(f7464,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,X0))),X2))))),
inference(forward_demodulation,[],[f7427,f8]) ).
fof(f7500,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,X0)),X2)))))),
inference(forward_demodulation,[],[f7464,f8]) ).
fof(f7533,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,X0),X2))))))),
inference(forward_demodulation,[],[f7500,f8]) ).
fof(f7562,plain,
! [X2,X0,X1] : multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X2)))))))),
inference(forward_demodulation,[],[f7533,f8]) ).
fof(f7591,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,X0)),X2)) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X2)))))))),
inference(forward_demodulation,[],[f7562,f8]) ).
fof(f7619,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,X0),X2))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X2)))))))),
inference(forward_demodulation,[],[f7591,f8]) ).
fof(f7647,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,X2)))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X2)))))))),
inference(forward_demodulation,[],[f7619,f8]) ).
fof(f8159,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,X0)))))))),
inference(superposition,[],[f2208,f7342]) ).
fof(f13553,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)) = multiply(multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,X0))))),X2),
inference(superposition,[],[f8,f4905]) ).
fof(f13586,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)) = multiply(X0,multiply(multiply(X1,multiply(X0,multiply(X0,multiply(X1,X0)))),X2)),
inference(forward_demodulation,[],[f13553,f8]) ).
fof(f13655,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)) = multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X0,multiply(X1,X0))),X2))),
inference(forward_demodulation,[],[f13586,f8]) ).
fof(f13724,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X0,multiply(X1,X0)),X2)))),
inference(forward_demodulation,[],[f13655,f8]) ).
fof(f13793,plain,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,X0),X2))))),
inference(forward_demodulation,[],[f13724,f8]) ).
fof(f13862,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))))),X2)),
inference(forward_demodulation,[],[f13793,f8]) ).
fof(f13926,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0))))),X2))),
inference(forward_demodulation,[],[f13862,f8]) ).
fof(f13987,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0)))),X2)))),
inference(forward_demodulation,[],[f13926,f8]) ).
fof(f14047,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X0,multiply(X1,multiply(X1,X0))),X2))))),
inference(forward_demodulation,[],[f13987,f8]) ).
fof(f14106,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,X0)),X2)))))),
inference(forward_demodulation,[],[f14047,f8]) ).
fof(f14165,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(multiply(X1,X0),X2))))))),
inference(forward_demodulation,[],[f14106,f8]) ).
fof(f14224,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,X2)))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X2)))))))),
inference(forward_demodulation,[],[f14165,f8]) ).
fof(f19262,plain,
! [X0,X1] : multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,X0))))))) = multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,X0))))))),
inference(superposition,[],[f7647,f6346]) ).
fof(f67251,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))),
inference(superposition,[],[f19262,f1980]) ).
fof(f67550,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f67251,f8]) ).
fof(f67695,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f67550,f8]) ).
fof(f67827,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f67695,f8]) ).
fof(f67958,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f67827,f8]) ).
fof(f68089,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))))))),
inference(forward_demodulation,[],[f67958,f8]) ).
fof(f68217,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))))))),
inference(forward_demodulation,[],[f68089,f8]) ).
fof(f68336,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))),
inference(forward_demodulation,[],[f68217,f2208]) ).
fof(f68452,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f68336,f8]) ).
fof(f68568,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f68452,f8]) ).
fof(f68683,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f68568,f8]) ).
fof(f68795,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f68683,f8]) ).
fof(f68904,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))))))),
inference(forward_demodulation,[],[f68795,f8]) ).
fof(f69002,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))))))),
inference(forward_demodulation,[],[f68904,f8]) ).
fof(f69093,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))),
inference(forward_demodulation,[],[f69002,f2208]) ).
fof(f69180,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f69093,f8]) ).
fof(f69263,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f69180,f8]) ).
fof(f69340,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))),
inference(forward_demodulation,[],[f69263,f678]) ).
fof(f69417,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f69340,f8]) ).
fof(f69494,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f69417,f8]) ).
fof(f69571,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f69494,f8]) ).
fof(f69648,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f69571,f8]) ).
fof(f69725,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f69648,f7647]) ).
fof(f69802,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f69725,f8]) ).
fof(f69879,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f69802,f8]) ).
fof(f69955,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f69879,f8]) ).
fof(f70031,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f69955,f8]) ).
fof(f70106,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1)))))))))))),
inference(forward_demodulation,[],[f70031,f8]) ).
fof(f70179,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))))))))),
inference(forward_demodulation,[],[f70106,f8]) ).
fof(f70249,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70179,f2474]) ).
fof(f70318,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(X0,multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f70249,f8]) ).
fof(f70378,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f70318,f8]) ).
fof(f70432,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70378,f678]) ).
fof(f70483,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(X0,multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f70432,f8]) ).
fof(f70534,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f70483,f8]) ).
fof(f70585,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))))),multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70534,f692]) ).
fof(f70634,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f70585,f8]) ).
fof(f70683,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f70634,f8]) ).
fof(f70730,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f70683,f8]) ).
fof(f70777,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(multiply(X1,multiply(X1,multiply(X0,X1))),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f70730,f14224]) ).
fof(f70821,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,X1))))))))),
inference(forward_demodulation,[],[f70777,f8]) ).
fof(f70862,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))))))))),
inference(forward_demodulation,[],[f70821,f8]) ).
fof(f70903,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,X1))))))))))),
inference(forward_demodulation,[],[f70862,f8]) ).
fof(f70942,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(multiply(X1,multiply(X0,X1)),multiply(X0,multiply(X0,X1))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70903,f7647]) ).
fof(f70981,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X0,multiply(X0,X1)))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70942,f8]) ).
fof(f71016,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,multiply(X1,multiply(X0,multiply(X0,X1))))))) = multiply(X0,multiply(X1,multiply(X0,multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1))))))),
inference(forward_demodulation,[],[f70981,f8]) ).
fof(f164999,plain,
! [X0,X1] : multiply(X0,add(multiply(X0,X0),X1)) = add(X0,multiply(X0,X1)),
inference(superposition,[],[f4,f9]) ).
fof(f165072,plain,
! [X2,X0,X1] : multiply(X0,add(X2,multiply(X0,multiply(X0,X1)))) = add(multiply(X0,X2),multiply(X0,X1)),
inference(superposition,[],[f4,f678]) ).
fof(f165143,plain,
! [X2,X0,X1] : add(multiply(X0,X1),multiply(X0,X2)) = multiply(X0,add(X2,X1)),
inference(superposition,[],[f4,f7]) ).
fof(f165145,plain,
! [X2,X3,X0,X1] : add(multiply(X0,X1),add(multiply(X0,X2),X3)) = add(multiply(X0,add(X1,X2)),X3),
inference(superposition,[],[f6,f4]) ).
fof(f165251,plain,
! [X2,X0,X1] : multiply(X0,add(X2,multiply(X0,multiply(X0,X1)))) = multiply(X0,add(X2,X1)),
inference(forward_demodulation,[],[f165072,f4]) ).
fof(f165340,plain,
! [X0,X1] : multiply(add(X0,X1),multiply(X0,X0)) = add(X0,multiply(X1,multiply(X0,X0))),
inference(superposition,[],[f5,f9]) ).
fof(f165411,plain,
! [X2,X3,X0,X1] : multiply(add(multiply(X0,X1),X3),X2) = add(multiply(X0,multiply(X1,X2)),multiply(X3,X2)),
inference(superposition,[],[f5,f8]) ).
fof(f165484,plain,
! [X0,X1] : multiply(X0,add(X1,X1)) = multiply(add(X0,X0),X1),
inference(superposition,[],[f5,f4]) ).
fof(f165485,plain,
! [X2,X0,X1] : add(multiply(X0,X1),multiply(X2,X1)) = multiply(add(X2,X0),X1),
inference(superposition,[],[f5,f7]) ).
fof(f165495,plain,
! [X2,X0,X1] : multiply(X1,X2) = add(additive_inverse(multiply(X0,X2)),multiply(add(X0,X1),X2)),
inference(superposition,[],[f56,f5]) ).
fof(f165496,plain,
! [X2,X0,X1] : multiply(X0,X2) = add(additive_inverse(multiply(X1,X2)),multiply(add(X0,X1),X2)),
inference(superposition,[],[f60,f5]) ).
fof(f165841,plain,
! [X0] : multiply(X0,multiply(X0,X0)) = add(X0,multiply(X0,additive_identity)),
inference(superposition,[],[f164999,f1]) ).
fof(f165842,plain,
! [X0,X1] : multiply(X1,X0) = add(X1,multiply(X1,add(additive_inverse(multiply(X1,X1)),X0))),
inference(superposition,[],[f164999,f37]) ).
fof(f165861,plain,
! [X0] : multiply(X0,additive_identity) = add(X0,multiply(X0,additive_inverse(multiply(X0,X0)))),
inference(superposition,[],[f164999,f3]) ).
fof(f165871,plain,
! [X2,X0,X1] : multiply(X0,multiply(add(multiply(X0,X0),X1),X2)) = multiply(add(X0,multiply(X0,X1)),X2),
inference(superposition,[],[f8,f164999]) ).
fof(f165951,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = X0,
inference(forward_demodulation,[],[f165841,f9]) ).
fof(f165967,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(superposition,[],[f165951,f11]) ).
fof(f165978,plain,
! [X0] : add(additive_inverse(X0),X0) = multiply(X0,additive_identity),
inference(superposition,[],[f56,f165951]) ).
fof(f166036,plain,
! [X0] : add(X0,additive_inverse(X0)) = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f165978,f7]) ).
fof(f166054,plain,
! [X0] : additive_identity = multiply(X0,additive_identity),
inference(forward_demodulation,[],[f166036,f3]) ).
fof(f166068,plain,
! [X0] : multiply(additive_identity,X0) = multiply(additive_identity,multiply(additive_identity,X0)),
inference(superposition,[],[f8,f165967]) ).
fof(f166146,plain,
! [X0,X1] : multiply(additive_identity,X1) = multiply(X0,multiply(additive_identity,X1)),
inference(superposition,[],[f8,f166054]) ).
fof(f167004,plain,
! [X0,X1] : multiply(additive_identity,add(multiply(additive_identity,X0),X1)) = add(multiply(additive_identity,X0),multiply(additive_identity,X1)),
inference(superposition,[],[f4,f166068]) ).
fof(f167103,plain,
! [X0,X1] : multiply(additive_identity,add(multiply(additive_identity,X0),X1)) = multiply(additive_identity,add(X0,X1)),
inference(forward_demodulation,[],[f167004,f4]) ).
fof(f168693,plain,
! [X0,X1] : multiply(additive_identity,X0) = multiply(X1,add(multiply(additive_identity,X0),multiply(additive_identity,X0))),
inference(superposition,[],[f165484,f166146]) ).
fof(f168696,plain,
! [X0,X1] : multiply(additive_identity,X0) = multiply(X1,multiply(additive_identity,add(X0,X0))),
inference(forward_demodulation,[],[f168693,f4]) ).
fof(f169301,plain,
! [X0] : multiply(additive_identity,add(X0,X0)) = multiply(additive_identity,X0),
inference(forward_demodulation,[],[f168696,f166146]) ).
fof(f173280,plain,
! [X0] : additive_identity = add(X0,multiply(X0,additive_inverse(multiply(X0,X0)))),
inference(forward_demodulation,[],[f165861,f166054]) ).
fof(f173296,plain,
! [X0] : add(additive_inverse(X0),additive_identity) = multiply(X0,additive_inverse(multiply(X0,X0))),
inference(superposition,[],[f56,f173280]) ).
fof(f173357,plain,
! [X0] : additive_inverse(X0) = multiply(X0,additive_inverse(multiply(X0,X0))),
inference(forward_demodulation,[],[f173296,f1]) ).
fof(f173456,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(additive_inverse(multiply(X0,X0)),X1)),
inference(superposition,[],[f8,f173357]) ).
fof(f173458,plain,
! [X0] : additive_inverse(X0) = multiply(X0,multiply(X0,additive_inverse(X0))),
inference(superposition,[],[f678,f173357]) ).
fof(f173546,plain,
! [X0] : multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0)) = X0,
inference(superposition,[],[f173458,f53]) ).
fof(f173593,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(multiply(X0,additive_inverse(X0)),X1)),
inference(superposition,[],[f8,f173458]) ).
fof(f173694,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),X1))),
inference(forward_demodulation,[],[f173593,f8]) ).
fof(f173995,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(X0),multiply(multiply(additive_inverse(X0),X0),X1)),
inference(superposition,[],[f8,f173546]) ).
fof(f174088,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,X1))),
inference(forward_demodulation,[],[f173995,f8]) ).
fof(f176768,plain,
! [X2,X0,X1] : multiply(X0,add(X1,X2)) = multiply(X0,add(X2,X1)),
inference(superposition,[],[f165143,f4]) ).
fof(f177467,plain,
! [X2,X0,X1] : multiply(add(X0,X1),X2) = multiply(add(X1,X0),X2),
inference(superposition,[],[f165485,f5]) ).
fof(f182357,plain,
! [X0] : multiply(additive_identity,additive_identity) = multiply(additive_identity,add(X0,additive_inverse(multiply(additive_identity,X0)))),
inference(superposition,[],[f167103,f3]) ).
fof(f182506,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,additive_inverse(multiply(additive_identity,X0)))),
inference(forward_demodulation,[],[f182357,f166054]) ).
fof(f183367,plain,
! [X0] : additive_identity = multiply(additive_identity,add(add(X0,X0),additive_inverse(multiply(additive_identity,X0)))),
inference(superposition,[],[f182506,f169301]) ).
fof(f183675,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,add(X0,additive_inverse(multiply(additive_identity,X0))))),
inference(forward_demodulation,[],[f183367,f6]) ).
fof(f185186,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,add(multiply(additive_identity,X0),additive_inverse(multiply(additive_identity,multiply(additive_identity,X0)))))),
inference(superposition,[],[f167103,f183675]) ).
fof(f185305,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,add(multiply(additive_identity,X0),additive_inverse(multiply(additive_identity,X0))))),
inference(forward_demodulation,[],[f185186,f166146]) ).
fof(f185450,plain,
! [X0] : additive_identity = multiply(additive_identity,add(X0,additive_identity)),
inference(forward_demodulation,[],[f185305,f3]) ).
fof(f185589,plain,
! [X0] : additive_identity = multiply(additive_identity,X0),
inference(forward_demodulation,[],[f185450,f1]) ).
fof(f194465,plain,
! [X0] : multiply(X0,multiply(additive_inverse(X0),X0)) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0)))))),
inference(superposition,[],[f8159,f174088]) ).
fof(f194874,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0)))) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f194465,f173694]) ).
fof(f195126,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,X0)) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f194874,f173546]) ).
fof(f198125,plain,
! [X0] : multiply(add(X0,additive_inverse(X0)),multiply(X0,X0)) = add(X0,multiply(X0,multiply(additive_inverse(X0),X0))),
inference(superposition,[],[f165340,f195126]) ).
fof(f198285,plain,
! [X0] : multiply(additive_identity,multiply(X0,X0)) = add(X0,multiply(X0,multiply(additive_inverse(X0),X0))),
inference(forward_demodulation,[],[f198125,f3]) ).
fof(f198357,plain,
! [X0] : additive_identity = add(X0,multiply(X0,multiply(additive_inverse(X0),X0))),
inference(forward_demodulation,[],[f198285,f185589]) ).
fof(f198732,plain,
! [X0] : add(additive_inverse(X0),additive_identity) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(superposition,[],[f56,f198357]) ).
fof(f198818,plain,
! [X0] : additive_inverse(X0) = multiply(X0,multiply(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f198732,f1]) ).
fof(f199055,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,additive_inverse(X0)))))) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0))))))),
inference(superposition,[],[f71016,f198818]) ).
fof(f199234,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,additive_inverse(X0)))))) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0))))),
inference(forward_demodulation,[],[f199055,f173694]) ).
fof(f199315,plain,
! [X0] : multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,additive_inverse(X0)))))) = multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X0))),
inference(forward_demodulation,[],[f199234,f174088]) ).
fof(f199379,plain,
! [X0] : multiply(X0,X0) = multiply(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X0,additive_inverse(X0)))))),
inference(forward_demodulation,[],[f199315,f173546]) ).
fof(f199434,plain,
! [X0] : multiply(X0,X0) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,additive_inverse(X0)))),
inference(forward_demodulation,[],[f199379,f174088]) ).
fof(f199480,plain,
! [X0] : multiply(X0,X0) = multiply(additive_inverse(X0),additive_inverse(X0)),
inference(forward_demodulation,[],[f199434,f173458]) ).
fof(f201962,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = multiply(X0,multiply(additive_inverse(multiply(X0,X0)),additive_inverse(multiply(additive_inverse(multiply(X0,X0)),additive_inverse(multiply(X0,X0)))))),
inference(superposition,[],[f165842,f173280]) ).
fof(f202087,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = multiply(additive_inverse(X0),additive_inverse(multiply(additive_inverse(multiply(X0,X0)),additive_inverse(multiply(X0,X0))))),
inference(forward_demodulation,[],[f201962,f173456]) ).
fof(f202138,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = multiply(additive_inverse(X0),additive_inverse(multiply(multiply(X0,X0),multiply(X0,X0)))),
inference(forward_demodulation,[],[f202087,f199480]) ).
fof(f202161,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = multiply(additive_inverse(X0),additive_inverse(multiply(X0,multiply(X0,multiply(X0,X0))))),
inference(forward_demodulation,[],[f202138,f8]) ).
fof(f202169,plain,
! [X0] : add(X0,multiply(X0,additive_identity)) = multiply(additive_inverse(X0),additive_inverse(multiply(X0,X0))),
inference(forward_demodulation,[],[f202161,f678]) ).
fof(f202173,plain,
! [X0] : multiply(additive_inverse(X0),additive_inverse(multiply(X0,X0))) = X0,
inference(forward_demodulation,[],[f202169,f165951]) ).
fof(f202202,plain,
! [X0,X1] : multiply(X0,X1) = multiply(additive_inverse(X0),multiply(additive_inverse(multiply(X0,X0)),X1)),
inference(superposition,[],[f8,f202173]) ).
fof(f202638,plain,
! [X0,X1] : multiply(additive_inverse(X0),multiply(multiply(X0,X0),X1)) = multiply(X0,multiply(additive_inverse(multiply(multiply(X0,X0),multiply(X0,X0))),X1)),
inference(superposition,[],[f202202,f202202]) ).
fof(f203626,plain,
! [X0,X1] : multiply(additive_inverse(X0),multiply(multiply(X0,X0),X1)) = multiply(X0,multiply(additive_inverse(multiply(X0,multiply(X0,multiply(X0,X0)))),X1)),
inference(forward_demodulation,[],[f202638,f8]) ).
fof(f204017,plain,
! [X0,X1] : multiply(X0,multiply(additive_inverse(multiply(X0,X0)),X1)) = multiply(additive_inverse(X0),multiply(multiply(X0,X0),X1)),
inference(forward_demodulation,[],[f203626,f678]) ).
fof(f204305,plain,
! [X0,X1] : multiply(X0,multiply(additive_inverse(multiply(X0,X0)),X1)) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f204017,f8]) ).
fof(f204552,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = multiply(additive_inverse(X0),multiply(X0,multiply(X0,X1))),
inference(forward_demodulation,[],[f204305,f173456]) ).
fof(f205535,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(additive_inverse(X0),multiply(additive_inverse(X0),X1))),
inference(superposition,[],[f204552,f53]) ).
fof(f207310,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),X1)),
inference(superposition,[],[f173694,f205535]) ).
fof(f222808,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(X0,add(X1,X2)),multiply(multiply(X0,X2),additive_inverse(multiply(multiply(X0,X2),multiply(X0,X2))))),
inference(superposition,[],[f165145,f173280]) ).
fof(f223011,plain,
! [X2,X0,X1] : add(multiply(X0,X1),additive_identity) = add(multiply(X0,add(X1,X2)),additive_inverse(multiply(X0,X2))),
inference(forward_demodulation,[],[f222808,f173357]) ).
fof(f223270,plain,
! [X2,X0,X1] : add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))) = add(multiply(X0,X1),additive_identity),
inference(forward_demodulation,[],[f223011,f7]) ).
fof(f223341,plain,
! [X2,X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,X2)),multiply(X0,add(X1,X2))),
inference(forward_demodulation,[],[f223270,f1]) ).
fof(f227462,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,additive_inverse(X1))),multiply(X0,additive_identity)),
inference(superposition,[],[f223341,f3]) ).
fof(f227645,plain,
! [X0,X1] : multiply(X0,X1) = add(multiply(X0,additive_identity),additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f227462,f7]) ).
fof(f227733,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_identity,additive_inverse(multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f227645,f166054]) ).
fof(f227770,plain,
! [X0,X1] : multiply(X0,X1) = additive_inverse(multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f227733,f11]) ).
fof(f227808,plain,
! [X0,X1] : multiply(X1,additive_inverse(X0)) = additive_inverse(multiply(X1,X0)),
inference(superposition,[],[f227770,f53]) ).
fof(f257630,plain,
! [X0,X1] : add(X0,multiply(X1,X0)) = multiply(add(multiply(X0,X0),X1),X0),
inference(superposition,[],[f165411,f9]) ).
fof(f257890,plain,
! [X2,X0,X1] : multiply(add(multiply(X0,X1),X0),X2) = multiply(X0,add(X2,multiply(X1,X2))),
inference(superposition,[],[f165143,f165411]) ).
fof(f258022,plain,
! [X2,X0,X1] : multiply(add(X0,multiply(X0,X1)),X2) = multiply(X0,add(X2,multiply(X1,X2))),
inference(forward_demodulation,[],[f257890,f177467]) ).
fof(f258430,plain,
! [X0,X1] : multiply(X0,X1) = add(X1,multiply(add(X0,additive_inverse(multiply(X1,X1))),X1)),
inference(superposition,[],[f257630,f40]) ).
fof(f258754,plain,
! [X0,X1] : multiply(X0,X1) = add(X1,multiply(add(X0,multiply(X1,additive_inverse(X1))),X1)),
inference(forward_demodulation,[],[f258430,f227808]) ).
fof(f259594,plain,
! [X0,X1] : multiply(add(X0,multiply(X1,additive_inverse(X1))),X1) = add(additive_inverse(X1),multiply(X0,X1)),
inference(superposition,[],[f56,f258754]) ).
fof(f291327,plain,
! [X2,X0,X1] : multiply(X1,X2) = add(multiply(X0,additive_inverse(X2)),multiply(add(X0,X1),X2)),
inference(forward_demodulation,[],[f165495,f227808]) ).
fof(f291408,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(X0,additive_inverse(X1)),multiply(additive_identity,X1)),
inference(superposition,[],[f291327,f3]) ).
fof(f291937,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(multiply(additive_identity,X1),multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f291408,f7]) ).
fof(f292168,plain,
! [X0,X1] : multiply(additive_inverse(X0),X1) = add(additive_identity,multiply(X0,additive_inverse(X1))),
inference(forward_demodulation,[],[f291937,f185589]) ).
fof(f292351,plain,
! [X0,X1] : multiply(X0,additive_inverse(X1)) = multiply(additive_inverse(X0),X1),
inference(forward_demodulation,[],[f292168,f11]) ).
fof(f301212,plain,
! [X2,X0,X1] : multiply(X0,X2) = add(multiply(X1,additive_inverse(X2)),multiply(add(X0,X1),X2)),
inference(forward_demodulation,[],[f165496,f227808]) ).
fof(f327506,plain,
! [X0,X1] : multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0) = multiply(X1,add(additive_inverse(X0),multiply(multiply(X1,X1),X0))),
inference(superposition,[],[f165871,f259594]) ).
fof(f328686,plain,
! [X0,X1] : multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0) = multiply(X1,add(additive_inverse(X0),multiply(X1,multiply(X1,X0)))),
inference(forward_demodulation,[],[f327506,f8]) ).
fof(f329204,plain,
! [X0,X1] : multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0) = multiply(X1,add(additive_inverse(X0),X0)),
inference(forward_demodulation,[],[f328686,f165251]) ).
fof(f329522,plain,
! [X0,X1] : multiply(X1,add(X0,additive_inverse(X0))) = multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0),
inference(forward_demodulation,[],[f329204,f176768]) ).
fof(f329759,plain,
! [X0,X1] : multiply(X1,additive_identity) = multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0),
inference(forward_demodulation,[],[f329522,f3]) ).
fof(f329885,plain,
! [X0,X1] : additive_identity = multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X0),
inference(forward_demodulation,[],[f329759,f166054]) ).
fof(f330340,plain,
! [X2,X0,X1] : multiply(additive_identity,X2) = multiply(add(X0,multiply(X0,multiply(X1,additive_inverse(X1)))),multiply(X1,X2)),
inference(superposition,[],[f8,f329885]) ).
fof(f330629,plain,
! [X2,X0,X1] : additive_identity = multiply(add(X0,multiply(X0,multiply(X1,additive_inverse(X1)))),multiply(X1,X2)),
inference(forward_demodulation,[],[f330340,f185589]) ).
fof(f333263,plain,
! [X2,X0,X1] : multiply(X0,additive_identity) = multiply(X0,multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X2)),
inference(superposition,[],[f2474,f330629]) ).
fof(f333266,plain,
! [X0,X1] : multiply(X0,additive_identity) = multiply(X0,add(X1,multiply(X1,multiply(X0,additive_inverse(X0))))),
inference(superposition,[],[f2251,f330629]) ).
fof(f333552,plain,
! [X0,X1] : additive_identity = multiply(X0,add(X1,multiply(X1,multiply(X0,additive_inverse(X0))))),
inference(forward_demodulation,[],[f333266,f166054]) ).
fof(f333554,plain,
! [X2,X0,X1] : additive_identity = multiply(X0,multiply(add(X1,multiply(X1,multiply(X0,additive_inverse(X0)))),X2)),
inference(forward_demodulation,[],[f333263,f166054]) ).
fof(f334527,plain,
! [X0,X1] : multiply(X0,X1) = add(additive_inverse(multiply(X0,multiply(X1,multiply(X0,additive_inverse(X0))))),additive_identity),
inference(superposition,[],[f223341,f333552]) ).
fof(f334758,plain,
! [X0,X1] : multiply(X0,X1) = additive_inverse(multiply(X0,multiply(X1,multiply(X0,additive_inverse(X0))))),
inference(forward_demodulation,[],[f334527,f1]) ).
fof(f334892,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,additive_inverse(multiply(X1,multiply(X0,additive_inverse(X0))))),
inference(forward_demodulation,[],[f334758,f227808]) ).
fof(f334981,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,additive_inverse(multiply(X0,additive_inverse(X0))))),
inference(forward_demodulation,[],[f334892,f227808]) ).
fof(f335044,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X0,X0))),
inference(forward_demodulation,[],[f334981,f227770]) ).
fof(f463534,plain,
! [X2,X0,X1] : additive_identity = multiply(X2,multiply(X0,add(X1,multiply(multiply(X2,additive_inverse(X2)),X1)))),
inference(superposition,[],[f333554,f258022]) ).
fof(f464180,plain,
! [X2,X0,X1] : additive_identity = multiply(X2,multiply(X0,add(X1,multiply(X2,multiply(additive_inverse(X2),X1))))),
inference(forward_demodulation,[],[f463534,f8]) ).
fof(f464797,plain,
! [X2,X0,X1] : additive_identity = multiply(X2,multiply(X0,add(X1,multiply(X2,multiply(X2,additive_inverse(X1)))))),
inference(forward_demodulation,[],[f464180,f292351]) ).
fof(f466378,plain,
! [X0,X1] : multiply(add(X0,multiply(X1,multiply(X1,additive_inverse(X0)))),additive_identity) = multiply(add(X0,multiply(X1,multiply(X1,additive_inverse(X0)))),X1),
inference(superposition,[],[f335044,f464797]) ).
fof(f466746,plain,
! [X0,X1] : additive_identity = multiply(add(X0,multiply(X1,multiply(X1,additive_inverse(X0)))),X1),
inference(forward_demodulation,[],[f466378,f166054]) ).
fof(f468110,plain,
! [X0,X1] : multiply(X0,X1) = add(multiply(multiply(X1,multiply(X1,additive_inverse(X0))),additive_inverse(X1)),additive_identity),
inference(superposition,[],[f301212,f466746]) ).
fof(f468535,plain,
! [X0,X1] : multiply(X0,X1) = multiply(multiply(X1,multiply(X1,additive_inverse(X0))),additive_inverse(X1)),
inference(forward_demodulation,[],[f468110,f1]) ).
fof(f468814,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(multiply(X1,additive_inverse(X0)),additive_inverse(X1))),
inference(forward_demodulation,[],[f468535,f8]) ).
fof(f469022,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X1,multiply(additive_inverse(X0),additive_inverse(X1)))),
inference(forward_demodulation,[],[f468814,f8]) ).
fof(f469161,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X1,multiply(X0,additive_inverse(additive_inverse(X1))))),
inference(forward_demodulation,[],[f469022,f292351]) ).
fof(f469276,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X1,multiply(X0,X1))),
inference(forward_demodulation,[],[f469161,f53]) ).
fof(f469835,plain,
! [X0,X1] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,X1))) = multiply(multiply(X0,X1),multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1))))))),
inference(superposition,[],[f8159,f469276]) ).
fof(f470173,plain,
! [X0,X1] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,X1))) = multiply(X0,multiply(X1,multiply(X1,multiply(X1,multiply(multiply(X0,X1),multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f469835,f8]) ).
fof(f470498,plain,
! [X0,X1] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,X1))) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),multiply(X1,multiply(multiply(X0,X1),multiply(X0,X1)))))),
inference(forward_demodulation,[],[f470173,f678]) ).
fof(f470756,plain,
! [X0,X1] : multiply(multiply(X0,X1),multiply(X1,multiply(X0,X1))) = multiply(X0,multiply(X1,multiply(multiply(X0,X1),X1))),
inference(forward_demodulation,[],[f470498,f335044]) ).
fof(f470977,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X0,multiply(X1,X1)))) = multiply(multiply(X0,X1),multiply(X1,multiply(X0,X1))),
inference(forward_demodulation,[],[f470756,f8]) ).
fof(f471152,plain,
! [X0,X1] : multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))) = multiply(X0,multiply(X1,multiply(X0,multiply(X1,X1)))),
inference(forward_demodulation,[],[f470977,f8]) ).
fof(f471300,plain,
! [X0,X1] : multiply(X0,multiply(X1,X0)) = multiply(X0,multiply(X1,multiply(X1,multiply(X0,X1)))),
inference(forward_demodulation,[],[f471152,f335044]) ).
fof(f471436,plain,
! [X0,X1] : multiply(X0,multiply(X0,X1)) = multiply(X0,multiply(X1,X0)),
inference(forward_demodulation,[],[f471300,f469276]) ).
fof(f472815,plain,
! [X0,X1] : multiply(X0,multiply(X0,multiply(additive_inverse(X0),X1))) = multiply(additive_inverse(X0),multiply(additive_inverse(X0),multiply(X1,additive_inverse(X0)))),
inference(superposition,[],[f207310,f471436]) ).
fof(f473210,plain,
! [X0,X1] : multiply(X1,additive_inverse(X0)) = multiply(X0,multiply(X0,multiply(additive_inverse(X0),X1))),
inference(forward_demodulation,[],[f472815,f469276]) ).
fof(f473572,plain,
! [X0,X1] : multiply(X1,additive_inverse(X0)) = multiply(X0,multiply(X0,multiply(X0,additive_inverse(X1)))),
inference(forward_demodulation,[],[f473210,f292351]) ).
fof(f473807,plain,
! [X0,X1] : multiply(X1,additive_inverse(X0)) = multiply(X0,additive_inverse(X1)),
inference(forward_demodulation,[],[f473572,f678]) ).
fof(f474987,plain,
! [X0,X1] : multiply(X1,additive_inverse(additive_inverse(X0))) = multiply(X0,additive_inverse(additive_inverse(X1))),
inference(superposition,[],[f292351,f473807]) ).
fof(f475013,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,additive_inverse(additive_inverse(X0))),
inference(forward_demodulation,[],[f474987,f53]) ).
fof(f475396,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(forward_demodulation,[],[f475013,f53]) ).
fof(f477670,plain,
multiply(a,b) != multiply(a,b),
inference(superposition,[],[f10,f475396]) ).
fof(f477671,plain,
$false,
inference(trivial_inequality_removal,[],[f477670]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG009-5 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 % Computer : n011.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 22:58:30 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 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
% 20.21/3.36 % (2861634)Will run a generic schedule for satisfiability detection.
% 20.21/3.36 % (2861655)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3360898557:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 20.21/3.36 % (2861652)% WARNING: option uhcvi not known.
% 20.21/3.36 % (2861651)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1266027746_2999 on theBenchmark for (2999ds/0Mi)
% 20.21/3.36 % (2861652)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2870028738:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 20.21/3.36 % (2861653)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2954484887:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 20.21/3.36 % (2861654)dis+10_1_sil=32000:sp=arity:random_seed=3283088239:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 20.21/3.36 % (2861656)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3814532604:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 20.21/3.36 % (2861657)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=948589614:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 20.21/3.36 % TRYING [1]
% 20.21/3.36 % TRYING [2]
% 20.21/3.36 % TRYING [3]
% 20.21/3.36 % TRYING [4]
% 20.21/3.36 % (2861655)Instruction limit reached!
% 20.21/3.36 % (2861655)------------------------------
% 20.21/3.36 % (2861655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.21/3.36 % (2861655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.36 % (2861655)CaDiCaL version: 2.1.3
% 20.21/3.36 % (2861655)Termination reason: Instruction limit
% 20.21/3.36 % (2861655)Termination phase: Saturation
% 20.21/3.36 % (2861655)Time elapsed: 0.037 s
% 20.21/3.36 % (2861655)Peak memory usage: 12 MB
% 20.21/3.36 % (2861655)Instructions burned: 118 (million)
% 20.21/3.36 % TRYING [5]
% 20.21/3.36 % (2861685)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4154738535:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 20.21/3.36 % TRYING [1]
% 20.21/3.36 % TRYING [2]
% 20.21/3.36 % TRYING [3]
% 20.21/3.36 % TRYING [4]
% 20.21/3.36 % TRYING [5]
% 20.21/3.36 % (2861654)Instruction limit reached!
% 20.21/3.36 % (2861654)------------------------------
% 20.21/3.36 % (2861654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.21/3.36 % (2861654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.36 % (2861654)CaDiCaL version: 2.1.3
% 20.21/3.36 % (2861654)Termination reason: Instruction limit
% 20.21/3.36 % (2861654)Termination phase: Saturation
% 20.21/3.36 % (2861654)Time elapsed: 0.058 s
% 20.21/3.36 % (2861654)Peak memory usage: 12 MB
% 20.21/3.36 % (2861654)Instructions burned: 104 (million)
% 20.21/3.36 % (2861656)Instruction limit reached!
% 20.21/3.36 % (2861656)------------------------------
% 20.21/3.36 % (2861656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.21/3.36 % (2861656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.36 % (2861656)CaDiCaL version: 2.1.3
% 20.21/3.36 % (2861656)Termination reason: Instruction limit
% 20.21/3.36 % (2861656)Termination phase: Saturation
% 20.21/3.36 % (2861656)Time elapsed: 0.067 s
% 20.21/3.36 % (2861656)Peak memory usage: 12 MB
% 20.21/3.36 % (2861656)Instructions burned: 133 (million)
% 20.21/3.36 % (2861691)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=51932870:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 20.21/3.36 % (2861695)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=341495780:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 20.21/3.36 % (2861657)Instruction limit reached!
% 20.21/3.36 % (2861657)------------------------------
% 20.21/3.36 % (2861657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.21/3.36 % (2861657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.36 % (2861657)CaDiCaL version: 2.1.3
% 20.21/3.36 % (2861657)Termination reason: Instruction limit
% 20.21/3.36 % (2861657)Termination phase: Saturation
% 20.21/3.36 % (2861657)Time elapsed: 0.094 s
% 20.21/3.36 % (2861657)Peak memory usage: 12 MB
% 20.21/3.36 % (2861657)Instructions burned: 160 (million)
% 20.21/3.36 % TRYING [6]
% 20.21/3.36 % TRYING [6]
% 20.21/3.36 % (2861705)ott-21_1_sil=16000:fs=off:random_seed=3845205730:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 20.21/3.36 % (2861691)Instruction limit reached!
% 20.21/3.36 % (2861691)------------------------------
% 20.21/3.36 % (2861691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861691)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861691)Termination reason: Instruction limit
% 78.54/11.57 % (2861691)Termination phase: Saturation
% 78.54/11.57 % (2861691)Time elapsed: 0.085 s
% 78.54/11.57 % (2861691)Peak memory usage: 12 MB
% 78.54/11.57 % (2861691)Instructions burned: 132 (million)
% 78.54/11.57 % (2861717)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=665291360:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 78.54/11.57 % (2861705)Instruction limit reached!
% 78.54/11.57 % (2861705)------------------------------
% 78.54/11.57 % (2861705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861705)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861705)Termination reason: Instruction limit
% 78.54/11.57 % (2861705)Termination phase: Saturation
% 78.54/11.57 % (2861705)Time elapsed: 0.078 s
% 78.54/11.57 % (2861705)Peak memory usage: 11 MB
% 78.54/11.57 % (2861705)Instructions burned: 180 (million)
% 78.54/11.57 % (2861720)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3601472545:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 78.54/11.57 % TRYING [1]
% 78.54/11.57 % TRYING [2]
% 78.54/11.57 % TRYING [3]
% 78.54/11.57 % (2861685)Instruction limit reached!
% 78.54/11.57 % (2861685)------------------------------
% 78.54/11.57 % (2861685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861685)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861685)Termination reason: Instruction limit
% 78.54/11.57 % (2861685)Termination phase: Finite model building SAT solving
% 78.54/11.57 % (2861685)Time elapsed: 0.186 s
% 78.54/11.57 % (2861685)Peak memory usage: 29 MB
% 78.54/11.57 % (2861685)Instructions burned: 717 (million)
% 78.54/11.57 % TRYING [4]
% 78.54/11.57 % (2861731)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=424468753:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 78.54/11.57 % TRYING [5]
% 78.54/11.57 % TRYING [6]
% 78.54/11.57 % (2861695)Instruction limit reached!
% 78.54/11.57 % (2861695)------------------------------
% 78.54/11.57 % (2861695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861695)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861695)Termination reason: Instruction limit
% 78.54/11.57 % (2861695)Termination phase: Saturation
% 78.54/11.57 % (2861695)Time elapsed: 0.330 s
% 78.54/11.57 % (2861695)Peak memory usage: 16 MB
% 78.54/11.57 % (2861695)Instructions burned: 685 (million)
% 78.54/11.57 % (2861717)Instruction limit reached!
% 78.54/11.57 % (2861717)------------------------------
% 78.54/11.57 % (2861717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861717)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861717)Termination reason: Instruction limit
% 78.54/11.57 % (2861717)Termination phase: Saturation
% 78.54/11.57 % (2861717)Time elapsed: 0.252 s
% 78.54/11.57 % (2861717)Peak memory usage: 15 MB
% 78.54/11.57 % (2861717)Instructions burned: 479 (million)
% 78.54/11.57 % (2861734)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3614146440:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 78.54/11.57 % (2861735)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=588573228:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 78.54/11.57 % (2861720)Instruction limit reached!
% 78.54/11.57 % (2861720)------------------------------
% 78.54/11.57 % (2861720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.54/11.57 % (2861720)CaDiCaL version: 2.1.3
% 78.54/11.57 % (2861720)Termination reason: Instruction limit
% 78.54/11.57 % (2861720)Termination phase: Finite model building SAT solving
% 78.54/11.57 % (2861720)Time elapsed: 0.329 s
% 78.54/11.57 % (2861720)Peak memory usage: 22 MB
% 78.54/11.57 % (2861720)Instructions burned: 868 (million)
% 78.54/11.57 % (2861731)Instruction limit reached!
% 78.54/11.57 % (2861731)------------------------------
% 78.54/11.57 % (2861731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.54/11.57 % (2861731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861731)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861731)Termination reason: Instruction limit
% 168.32/24.19 % (2861731)Termination phase: Saturation
% 168.32/24.19 % (2861731)Time elapsed: 0.309 s
% 168.32/24.19 % (2861731)Peak memory usage: 16 MB
% 168.32/24.19 % (2861731)Instructions burned: 1180 (million)
% 168.32/24.19 % (2861767)fmb+10_1_sil=64000:random_seed=747766961:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 168.32/24.19 % TRYING [1]
% 168.32/24.19 % TRYING [2]
% 168.32/24.19 % TRYING [3]
% 168.32/24.19 % TRYING [7]
% 168.32/24.19 % (2861766)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3294369497:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 168.32/24.19 % TRYING [4]
% 168.32/24.19 % TRYING [5]
% 168.32/24.19 % TRYING [14]
% 168.32/24.19 % TRYING [6]
% 168.32/24.19 % (2861735)Instruction limit reached!
% 168.32/24.19 % (2861735)------------------------------
% 168.32/24.19 % (2861735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.32/24.19 % (2861735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861735)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861735)Termination reason: Instruction limit
% 168.32/24.19 % (2861735)Termination phase: Saturation
% 168.32/24.19 % (2861735)Time elapsed: 0.557 s
% 168.32/24.19 % (2861735)Peak memory usage: 16 MB
% 168.32/24.19 % (2861735)Instructions burned: 693 (million)
% 168.32/24.19 % (2861784)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3445307448:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 168.32/24.19 % TRYING [20]
% 168.32/24.19 % (2861734)Instruction limit reached!
% 168.32/24.19 % (2861734)------------------------------
% 168.32/24.19 % (2861734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.32/24.19 % (2861734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861734)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861734)Termination reason: Instruction limit
% 168.32/24.19 % (2861734)Termination phase: Finite model building constraint generation
% 168.32/24.19 % (2861734)Time elapsed: 0.643 s
% 168.32/24.19 % (2861734)Peak memory usage: 80 MB
% 168.32/24.19 % (2861734)Instructions burned: 889 (million)
% 168.32/24.19 % (2861786)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1987499409:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 168.32/24.19 % TRYING [8]
% 168.32/24.19 % TRYING [7]
% 168.32/24.19 % (2861766)Instruction limit reached!
% 168.32/24.19 % (2861766)------------------------------
% 168.32/24.19 % (2861766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.32/24.19 % (2861766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861766)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861766)Termination reason: Instruction limit
% 168.32/24.19 % (2861766)Termination phase: Saturation
% 168.32/24.19 % (2861766)Time elapsed: 0.795 s
% 168.32/24.19 % (2861766)Peak memory usage: 18 MB
% 168.32/24.19 % (2861766)Instructions burned: 880 (million)
% 168.32/24.19 % (2861791)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1934478976:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 168.32/24.19 % (2861786)Instruction limit reached!
% 168.32/24.19 % (2861786)------------------------------
% 168.32/24.19 % (2861786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.32/24.19 % (2861786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861786)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861786)Termination reason: Instruction limit
% 168.32/24.19 % (2861786)Termination phase: Finite model building constraint generation
% 168.32/24.19 % (2861786)Time elapsed: 0.722 s
% 168.32/24.19 % (2861786)Peak memory usage: 65 MB
% 168.32/24.19 % (2861786)Instructions burned: 921 (million)
% 168.32/24.19 % (2861798)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3518536352:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 168.32/24.19 % TRYING [8]
% 168.32/24.19 % TRYING [8]
% 168.32/24.19 % (2861798)Instruction limit reached!
% 168.32/24.19 % (2861798)------------------------------
% 168.32/24.19 % (2861798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 168.32/24.19 % (2861798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 168.32/24.19 % (2861798)CaDiCaL version: 2.1.3
% 168.32/24.19 % (2861798)Termination reason: Instruction limit
% 168.32/24.19 % (2861798)Termination phase: Saturation
% 168.32/24.19 % (2861798)Time elapsed: 0.917 s
% 168.32/24.19 % (2861798)Peak memory usage: 35 MB
% 168.32/24.19 % (2861798)Instructions burned: 1473 (million)
% 168.32/24.19 % (2861808)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3653310482:i=6324_2971 on theBenchmark for (2971ds/6324Mi)
% 175.15/29.30 % TRYING [77]
% 175.15/29.30 % (2861808)Instruction limit reached!
% 175.15/29.30 % (2861808)------------------------------
% 175.15/29.30 % (2861808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861808)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861808)Termination reason: Instruction limit
% 175.15/29.30 % (2861808)Termination phase: Finite model building constraint generation
% 175.15/29.30 % (2861808)Time elapsed: 2.415 s
% 175.15/29.30 % (2861808)Peak memory usage: 419 MB
% 175.15/29.30 % (2861808)Instructions burned: 6324 (million)
% 175.15/29.30 % (2861812)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2312747551:fmbsr=2.30978:i=2174_2946 on theBenchmark for (2946ds/2174Mi)
% 175.15/29.30 % TRYING [16]
% 175.15/29.30 % (2861812)Instruction limit reached!
% 175.15/29.30 % (2861812)------------------------------
% 175.15/29.30 % (2861812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861812)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861812)Termination reason: Instruction limit
% 175.15/29.30 % (2861812)Termination phase: Finite model building constraint generation
% 175.15/29.30 % (2861812)Time elapsed: 0.759 s
% 175.15/29.30 % (2861812)Peak memory usage: 134 MB
% 175.15/29.30 % (2861812)Instructions burned: 2175 (million)
% 175.15/29.30 % (2861791)Instruction limit reached!
% 175.15/29.30 % (2861791)------------------------------
% 175.15/29.30 % (2861791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861791)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861791)Termination reason: Instruction limit
% 175.15/29.30 % (2861791)Termination phase: Saturation
% 175.15/29.30 % (2861791)Time elapsed: 4.752 s
% 175.15/29.30 % (2861791)Peak memory usage: 49 MB
% 175.15/29.30 % (2861791)Instructions burned: 5132 (million)
% 175.15/29.30 % (2861814)ott-2_1_sil=16000:newcnf=on:random_seed=3599278958:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2938 on theBenchmark for (2938ds/869Mi)
% 175.15/29.30 % (2861816)ott+10_1_sil=32000:tgt=ground:random_seed=3269326675:i=5114:av=off_2937 on theBenchmark for (2937ds/5114Mi)
% 175.15/29.30 % (2861814)Instruction limit reached!
% 175.15/29.30 % (2861814)------------------------------
% 175.15/29.30 % (2861814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861814)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861814)Termination reason: Instruction limit
% 175.15/29.30 % (2861814)Termination phase: Saturation
% 175.15/29.30 % (2861814)Time elapsed: 0.439 s
% 175.15/29.30 % (2861814)Peak memory usage: 18 MB
% 175.15/29.30 % (2861814)Instructions burned: 869 (million)
% 175.15/29.30 % (2861820)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3107103870:i=54282_2933 on theBenchmark for (2933ds/54282Mi)
% 175.15/29.30 % TRYING [1]
% 175.15/29.30 % TRYING [2]
% 175.15/29.30 % TRYING [3]
% 175.15/29.30 % TRYING [4]
% 175.15/29.30 % TRYING [5]
% 175.15/29.30 % TRYING [6]
% 175.15/29.30 % TRYING [7]
% 175.15/29.30 % (2861784)Instruction limit reached!
% 175.15/29.30 % (2861784)------------------------------
% 175.15/29.30 % (2861784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861784)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861784)Termination reason: Instruction limit
% 175.15/29.30 % (2861784)Termination phase: Finite model building constraint generation
% 175.15/29.30 % (2861784)Time elapsed: 7.091 s
% 175.15/29.30 % (2861784)Peak memory usage: 671 MB
% 175.15/29.30 % (2861784)Instructions burned: 9515 (million)
% 175.15/29.30 % TRYING [8]
% 175.15/29.30 % (2861826)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1118568730:i=3512:aac=none_2916 on theBenchmark for (2916ds/3512Mi)
% 175.15/29.30 % (2861816)Instruction limit reached!
% 175.15/29.30 % (2861816)------------------------------
% 175.15/29.30 % (2861816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861816)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861816)Termination reason: Instruction limit
% 175.15/29.30 % (2861816)Termination phase: Saturation
% 175.15/29.30 % (2861816)Time elapsed: 4.824 s
% 175.15/29.30 % (2861816)Peak memory usage: 45 MB
% 175.15/29.30 % (2861816)Instructions burned: 5115 (million)
% 175.15/29.30 % (2861834)dis+21_1_sil=32000:sas=cadical:random_seed=150165586:i=3773:amm=off_2889 on theBenchmark for (2889ds/3773Mi)
% 175.15/29.30 % (2861826)Instruction limit reached!
% 175.15/29.30 % (2861826)------------------------------
% 175.15/29.30 % (2861826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861826)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861826)Termination reason: Instruction limit
% 175.15/29.30 % (2861826)Termination phase: Saturation
% 175.15/29.30 % (2861826)Time elapsed: 3.294 s
% 175.15/29.30 % (2861826)Peak memory usage: 36 MB
% 175.15/29.30 % (2861826)Instructions burned: 3512 (million)
% 175.15/29.30 % (2861837)ott+11_1_sil=16000:gs=on:random_seed=1044103587:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2883 on theBenchmark for (2883ds/2251Mi)
% 175.15/29.30 % (2861837)Instruction limit reached!
% 175.15/29.30 % (2861837)------------------------------
% 175.15/29.30 % (2861837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861837)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861837)Termination reason: Instruction limit
% 175.15/29.30 % (2861837)Termination phase: Saturation
% 175.15/29.30 % (2861837)Time elapsed: 2.141 s
% 175.15/29.30 % (2861837)Peak memory usage: 25 MB
% 175.15/29.30 % (2861837)Instructions burned: 2251 (million)
% 175.15/29.30 % (2861844)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1124513994:fmbsr=1.6:i=67534_2861 on theBenchmark for (2861ds/67534Mi)
% 175.15/29.30 % TRYING [7]
% 175.15/29.30 % (2861834)Instruction limit reached!
% 175.15/29.30 % (2861834)------------------------------
% 175.15/29.30 % (2861834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861834)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861834)Termination reason: Instruction limit
% 175.15/29.30 % (2861834)Termination phase: Saturation
% 175.15/29.30 % (2861834)Time elapsed: 3.303 s
% 175.15/29.30 % (2861834)Peak memory usage: 37 MB
% 175.15/29.30 % (2861834)Instructions burned: 3774 (million)
% 175.15/29.30 % (2861848)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=696383164:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2855 on theBenchmark for (2855ds/4591Mi)
% 175.15/29.30 % (2861767)Instruction limit reached!
% 175.15/29.30 % (2861767)------------------------------
% 175.15/29.30 % (2861767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861767)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861767)Termination reason: Instruction limit
% 175.15/29.30 % (2861767)Termination phase: Finite model building SAT solving
% 175.15/29.30 % (2861767)Time elapsed: 15.151 s
% 175.15/29.30 % (2861767)Peak memory usage: 76 MB
% 175.15/29.30 % (2861767)Instructions burned: 22062 (million)
% 175.15/29.30 % (2861850)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2546497140:i=29340_2842 on theBenchmark for (2842ds/29340Mi)
% 175.15/29.30 % TRYING [8]
% 175.15/29.30 % (2861848)Instruction limit reached!
% 175.15/29.30 % (2861848)------------------------------
% 175.15/29.30 % (2861848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861848)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861848)Termination reason: Instruction limit
% 175.15/29.30 % (2861848)Termination phase: Saturation
% 175.15/29.30 % (2861848)Time elapsed: 4.418 s
% 175.15/29.30 % (2861848)Peak memory usage: 73 MB
% 175.15/29.30 % (2861848)Instructions burned: 4592 (million)
% 175.15/29.30 % (2861854)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3465682655:i=5211_2810 on theBenchmark for (2810ds/5211Mi)
% 175.15/29.30 % TRYING [9]
% 175.15/29.30 % (2861854)Instruction limit reached!
% 175.15/29.30 % (2861854)------------------------------
% 175.15/29.30 % (2861854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861854)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861854)Termination reason: Instruction limit
% 175.15/29.30 % (2861854)Termination phase: Saturation
% 175.15/29.30 % (2861854)Time elapsed: 4.754 s
% 175.15/29.30 % (2861854)Peak memory usage: 47 MB
% 175.15/29.30 % (2861854)Instructions burned: 5211 (million)
% 175.15/29.30 % (2861858)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2037009102:i=5497:nm=2_2762 on theBenchmark for (2762ds/5497Mi)
% 175.15/29.30 % TRYING [17]
% 175.15/29.30 % TRYING [9]
% 175.15/29.30 % (2861858)Instruction limit reached!
% 175.15/29.30 % (2861858)------------------------------
% 175.15/29.30 % (2861858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861858)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861858)Termination reason: Instruction limit
% 175.15/29.30 % (2861858)Termination phase: Finite model building constraint generation
% 175.15/29.30 % (2861858)Time elapsed: 4.054 s
% 175.15/29.30 % (2861858)Peak memory usage: 391 MB
% 175.15/29.30 % (2861858)Instructions burned: 5498 (million)
% 175.15/29.30 % (2861862)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3930853126:fmbsr=2:i=46332_2721 on theBenchmark for (2721ds/46332Mi)
% 175.15/29.30 % TRYING [15]
% 175.15/29.30 % (2861850)Instruction limit reached!
% 175.15/29.30 % (2861850)------------------------------
% 175.15/29.30 % (2861850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 175.15/29.30 % (2861850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.15/29.30 % (2861850)CaDiCaL version: 2.1.3
% 175.15/29.30 % (2861850)Termination reason: Instruction limit
% 175.15/29.30 % (2861850)Termination phase: Saturation
% 175.15/29.30 % (2861850)Time elapsed: 12.737 s
% 175.15/29.30 % (2861850)Peak memory usage: 135 MB
% 175.15/29.30 % (2861850)Instructions burned: 29340 (million)
% 175.15/29.30 % (2861864)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1188314013:i=14071_2714 on theBenchmark for (2714ds/14071Mi)
% 175.15/29.30 % TRYING [12]
% 175.15/29.30 % (2861653) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2861634-2861653"...
% 175.15/29.30 % (2861653)...printing done.
% 175.15/29.30 % (2861653)Refutation found. Thanks to Tanya!
% 175.15/29.30 % SZS status Unsatisfiable for theBenchmark
% 175.15/29.30 % SZS output start Proof for theBenchmark
% See solution above
% 204.74/29.30 % (2861653)------------------------------
% 204.74/29.30 % (2861653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 204.74/29.30 % (2861653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.74/29.30 % (2861653)CaDiCaL version: 2.1.3
% 204.74/29.30 % (2861653)Termination reason: Refutation
% 204.74/29.30 % (2861653)Time elapsed: 28.698 s
% 204.74/29.30 % (2861653)Peak memory usage: 199 MB
% 204.74/29.30 % (2861653)Instructions burned: 40681 (million)
% 204.74/29.30 % (2861634)Success in time 28.861 s
% 204.74/29.30 % Vampire exiting
%------------------------------------------------------------------------------