%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP701-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:18:35 AM UTC 2026
% Result : Unsatisfiable 118.28s 17.85s
% Output : Refutation 118.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 11
% Syntax : Number of formulae : 277 ( 277 unt; 0 def)
% Number of atoms : 277 ( 276 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 513 ( 513 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : mult(X0,ld(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c01) ).
fof(f2,axiom,
! [X0,X1] : ld(X0,mult(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c02) ).
fof(f3,axiom,
! [X0,X1] : mult(rd(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c03) ).
fof(f4,axiom,
! [X0,X1] : rd(mult(X0,X1),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c04) ).
fof(f5,axiom,
! [X0] : mult(X0,unit) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c05) ).
fof(f6,axiom,
! [X0] : mult(unit,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c06) ).
fof(f7,axiom,
! [X2,X0,X1] : mult(mult(mult(X0,X1),X0),mult(X0,X2)) = mult(X0,mult(mult(mult(X1,X0),X0),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c07) ).
fof(f8,axiom,
! [X2,X0,X1] : mult(mult(X0,X1),mult(X1,mult(X2,X1))) = mult(mult(X0,mult(X1,mult(X1,X2))),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c08) ).
fof(f9,axiom,
! [X0] : mult(X0,i(X0)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c09) ).
fof(f10,plain,
! [X0] : unit = mult(X0,i(X0)),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0] : mult(i(X0),X0) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f12,plain,
! [X0] : unit = mult(i(X0),X0),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
mult(a,i(mult(b,a))) != i(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f23,plain,
! [X0] : unit = ld(X0,X0),
inference(superposition,[],[f2,f5]) ).
fof(f24,plain,
! [X0] : i(X0) = ld(X0,unit),
inference(superposition,[],[f2,f10]) ).
fof(f26,plain,
! [X0] : ld(i(X0),unit) = X0,
inference(superposition,[],[f2,f12]) ).
fof(f35,plain,
! [X0] : i(i(X0)) = X0,
inference(forward_demodulation,[],[f26,f24]) ).
fof(f40,plain,
! [X0,X1] : ld(rd(X0,X1),X0) = X1,
inference(superposition,[],[f2,f3]) ).
fof(f45,plain,
! [X0,X1] : rd(X0,ld(X1,X0)) = X1,
inference(superposition,[],[f4,f1]) ).
fof(f46,plain,
! [X0] : unit = rd(X0,X0),
inference(superposition,[],[f4,f6]) ).
fof(f47,plain,
! [X0] : i(X0) = rd(unit,X0),
inference(superposition,[],[f4,f12]) ).
fof(f81,plain,
! [X0,X1] : mult(X0,mult(mult(mult(unit,X0),X0),X1)) = mult(mult(X0,X0),mult(X0,X1)),
inference(superposition,[],[f7,f5]) ).
fof(f83,plain,
! [X2,X0,X1] : mult(X1,mult(mult(mult(ld(X1,X0),X1),X1),X2)) = mult(mult(X0,X1),mult(X1,X2)),
inference(superposition,[],[f7,f1]) ).
fof(f90,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,X0),X0),unit)) = mult(mult(mult(X0,X1),X0),X0),
inference(superposition,[],[f7,f5]) ).
fof(f91,plain,
! [X0,X1] : mult(X0,mult(mult(mult(X1,X0),X0),i(X0))) = mult(mult(mult(X0,X1),X0),unit),
inference(superposition,[],[f7,f10]) ).
fof(f101,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = mult(X0,mult(mult(mult(X1,X0),X0),i(X0))),
inference(forward_demodulation,[],[f91,f5]) ).
fof(f102,plain,
! [X0,X1] : mult(mult(mult(X0,X1),X0),X0) = mult(X0,mult(mult(X1,X0),X0)),
inference(forward_demodulation,[],[f90,f5]) ).
fof(f107,plain,
! [X0,X1] : mult(mult(X0,X0),mult(X0,X1)) = mult(X0,mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f81,f6]) ).
fof(f120,plain,
! [X0,X1] : mult(X1,mult(mult(ld(X1,X0),X1),X1)) = mult(mult(X0,X1),X1),
inference(superposition,[],[f102,f1]) ).
fof(f131,plain,
! [X0,X1] : mult(mult(X0,X1),X0) = rd(mult(X0,mult(mult(X1,X0),X0)),X0),
inference(superposition,[],[f4,f102]) ).
fof(f173,plain,
! [X0] : mult(mult(X0,X0),unit) = mult(X0,mult(mult(X0,X0),i(X0))),
inference(superposition,[],[f107,f10]) ).
fof(f196,plain,
! [X0] : mult(X0,X0) = mult(X0,mult(mult(X0,X0),i(X0))),
inference(forward_demodulation,[],[f173,f5]) ).
fof(f224,plain,
! [X0] : mult(mult(X0,X0),i(X0)) = ld(X0,mult(X0,X0)),
inference(superposition,[],[f2,f196]) ).
fof(f227,plain,
! [X0] : mult(mult(X0,X0),i(X0)) = X0,
inference(forward_demodulation,[],[f224,f2]) ).
fof(f244,plain,
! [X0] : i(X0) = mult(mult(i(X0),i(X0)),X0),
inference(superposition,[],[f227,f35]) ).
fof(f249,plain,
! [X0] : mult(X0,X0) = rd(X0,i(X0)),
inference(superposition,[],[f4,f227]) ).
fof(f256,plain,
! [X0] : mult(i(X0),i(X0)) = rd(i(X0),X0),
inference(superposition,[],[f249,f35]) ).
fof(f327,plain,
! [X2,X0,X1] : mult(mult(X1,X2),mult(X2,mult(ld(X2,X0),X2))) = mult(mult(X1,mult(X2,X0)),X2),
inference(superposition,[],[f8,f1]) ).
fof(f329,plain,
! [X0,X1] : mult(mult(X1,X0),mult(X0,mult(unit,X0))) = mult(mult(X1,mult(X0,X0)),X0),
inference(superposition,[],[f8,f5]) ).
fof(f350,plain,
! [X0,X1] : mult(mult(unit,X0),mult(X0,mult(X1,X0))) = mult(mult(X0,mult(X0,X1)),X0),
inference(superposition,[],[f8,f6]) ).
fof(f351,plain,
! [X0,X1] : mult(unit,X0) = mult(mult(i(mult(X0,mult(X0,X1))),X0),mult(X0,mult(X1,X0))),
inference(superposition,[],[f8,f12]) ).
fof(f366,plain,
! [X0,X1] : mult(mult(i(mult(X0,mult(X0,X1))),X0),mult(X0,mult(X1,X0))) = X0,
inference(forward_demodulation,[],[f351,f6]) ).
fof(f367,plain,
! [X0,X1] : mult(mult(X0,mult(X0,X1)),X0) = mult(X0,mult(X0,mult(X1,X0))),
inference(forward_demodulation,[],[f350,f6]) ).
fof(f383,plain,
! [X0,X1] : mult(mult(X1,mult(X0,X0)),X0) = mult(mult(X1,X0),mult(X0,X0)),
inference(forward_demodulation,[],[f329,f6]) ).
fof(f411,plain,
! [X0,X1] : mult(X1,mult(X1,mult(ld(X1,X0),X1))) = mult(mult(X1,X0),X1),
inference(superposition,[],[f367,f1]) ).
fof(f503,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(rd(X0,mult(X1,X1)),X1),mult(X1,X1)),
inference(superposition,[],[f383,f3]) ).
fof(f505,plain,
! [X0] : mult(unit,X0) = mult(mult(i(mult(X0,X0)),X0),mult(X0,X0)),
inference(superposition,[],[f383,f12]) ).
fof(f511,plain,
! [X0,X1] : ld(mult(X0,mult(X1,X1)),mult(mult(X0,X1),mult(X1,X1))) = X1,
inference(superposition,[],[f2,f383]) ).
fof(f512,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = rd(mult(mult(X0,X1),mult(X1,X1)),X1),
inference(superposition,[],[f4,f383]) ).
fof(f527,plain,
! [X0] : mult(mult(i(mult(X0,X0)),X0),mult(X0,X0)) = X0,
inference(forward_demodulation,[],[f505,f6]) ).
fof(f571,plain,
! [X0] : mult(i(mult(X0,X0)),X0) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f4,f527]) ).
fof(f606,plain,
! [X0] : i(mult(X0,X0)) = rd(rd(X0,mult(X0,X0)),X0),
inference(superposition,[],[f4,f571]) ).
fof(f659,plain,
! [X0,X1] : mult(mult(ld(X1,X0),X1),X1) = ld(X1,mult(mult(X0,X1),X1)),
inference(superposition,[],[f2,f120]) ).
fof(f700,plain,
! [X0] : mult(mult(X0,mult(i(X0),i(X0))),X0) = rd(mult(X0,mult(i(X0),X0)),X0),
inference(superposition,[],[f131,f244]) ).
fof(f704,plain,
! [X0,X1] : mult(mult(X1,rd(X0,X1)),X1) = rd(mult(X1,mult(X0,X1)),X1),
inference(superposition,[],[f131,f3]) ).
fof(f728,plain,
! [X0] : mult(mult(X0,mult(i(X0),i(X0))),X0) = rd(mult(X0,unit),X0),
inference(forward_demodulation,[],[f700,f12]) ).
fof(f741,plain,
! [X0] : rd(X0,X0) = mult(mult(X0,mult(i(X0),i(X0))),X0),
inference(forward_demodulation,[],[f728,f5]) ).
fof(f753,plain,
! [X0] : rd(X0,X0) = mult(mult(X0,rd(i(X0),X0)),X0),
inference(forward_demodulation,[],[f741,f256]) ).
fof(f763,plain,
! [X0] : unit = mult(mult(X0,rd(i(X0),X0)),X0),
inference(forward_demodulation,[],[f753,f46]) ).
fof(f865,plain,
! [X0] : rd(unit,X0) = mult(X0,rd(i(X0),X0)),
inference(superposition,[],[f4,f763]) ).
fof(f888,plain,
! [X0] : i(X0) = mult(X0,rd(i(X0),X0)),
inference(forward_demodulation,[],[f865,f47]) ).
fof(f911,plain,
! [X0] : mult(i(X0),rd(X0,i(X0))) = X0,
inference(superposition,[],[f888,f35]) ).
fof(f915,plain,
! [X0] : rd(i(X0),X0) = ld(X0,i(X0)),
inference(superposition,[],[f2,f888]) ).
fof(f933,plain,
! [X0] : mult(i(X0),mult(X0,X0)) = X0,
inference(forward_demodulation,[],[f911,f249]) ).
fof(f953,plain,
! [X0] : i(X0) = rd(X0,mult(X0,X0)),
inference(superposition,[],[f4,f933]) ).
fof(f1006,plain,
! [X0] : i(mult(X0,X0)) = rd(i(X0),X0),
inference(superposition,[],[f606,f953]) ).
fof(f1074,plain,
! [X0] : i(mult(X0,X0)) = ld(X0,i(X0)),
inference(superposition,[],[f1006,f915]) ).
fof(f2255,plain,
! [X0,X1] : mult(X0,mult(ld(X0,X1),X0)) = ld(X0,mult(mult(X0,X1),X0)),
inference(superposition,[],[f2,f411]) ).
fof(f2735,plain,
! [X0,X1] : mult(rd(X0,mult(X1,X1)),X1) = rd(mult(X0,X1),mult(X1,X1)),
inference(superposition,[],[f4,f503]) ).
fof(f2997,plain,
! [X0,X1] : mult(rd(X0,X1),mult(X1,X1)) = rd(mult(X0,mult(X1,X1)),X1),
inference(superposition,[],[f512,f3]) ).
fof(f3010,plain,
! [X0,X1] : mult(mult(X0,X1),mult(X0,X0)) = rd(mult(X0,mult(mult(mult(X1,X0),X0),X0)),X0),
inference(superposition,[],[f512,f7]) ).
fof(f3025,plain,
! [X0,X1] : mult(mult(X0,X1),mult(X0,X0)) = mult(mult(X0,mult(X1,X0)),X0),
inference(forward_demodulation,[],[f3010,f131]) ).
fof(f3124,plain,
! [X0,X1] : mult(mult(ld(X1,rd(X0,X1)),X1),X1) = ld(X1,mult(X0,X1)),
inference(superposition,[],[f659,f3]) ).
fof(f3131,plain,
! [X0] : mult(mult(ld(X0,i(mult(X0,X0))),X0),X0) = ld(X0,mult(rd(X0,mult(X0,X0)),X0)),
inference(superposition,[],[f659,f571]) ).
fof(f3149,plain,
! [X0] : ld(X0,mult(i(X0),X0)) = mult(mult(ld(X0,i(mult(X0,X0))),X0),X0),
inference(forward_demodulation,[],[f3131,f953]) ).
fof(f3173,plain,
! [X0] : ld(X0,unit) = mult(mult(ld(X0,i(mult(X0,X0))),X0),X0),
inference(forward_demodulation,[],[f3149,f12]) ).
fof(f3192,plain,
! [X0] : i(X0) = mult(mult(ld(X0,i(mult(X0,X0))),X0),X0),
inference(forward_demodulation,[],[f3173,f24]) ).
fof(f3228,plain,
! [X0,X1] : mult(mult(i(mult(X0,X0)),X0),mult(X0,X1)) = mult(X0,mult(i(X0),X1)),
inference(superposition,[],[f83,f3192]) ).
fof(f3278,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(rd(X0,mult(X0,X0)),mult(X0,X1)),
inference(forward_demodulation,[],[f3228,f571]) ).
fof(f3303,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(i(X0),mult(X0,X1)),
inference(forward_demodulation,[],[f3278,f953]) ).
fof(f11999,plain,
! [X0,X1] : mult(mult(X0,ld(X0,rd(X1,X0))),X0) = mult(X0,mult(ld(X0,mult(X1,X0)),i(X0))),
inference(superposition,[],[f101,f3124]) ).
fof(f12072,plain,
! [X0,X1] : mult(rd(X1,X0),X0) = mult(X0,mult(ld(X0,mult(X1,X0)),i(X0))),
inference(forward_demodulation,[],[f11999,f1]) ).
fof(f12124,plain,
! [X0,X1] : mult(X0,mult(ld(X0,mult(X1,X0)),i(X0))) = X1,
inference(forward_demodulation,[],[f12072,f3]) ).
fof(f12258,plain,
! [X0,X1] : rd(X0,X1) = mult(X1,mult(ld(X1,X0),i(X1))),
inference(superposition,[],[f12124,f3]) ).
fof(f12287,plain,
! [X0,X1] : ld(X1,X0) = mult(ld(X1,mult(X0,X1)),i(X1)),
inference(superposition,[],[f2,f12124]) ).
fof(f12469,plain,
! [X0,X1] : rd(mult(X1,X0),X1) = mult(X1,mult(X0,i(X1))),
inference(superposition,[],[f12258,f2]) ).
fof(f12696,plain,
! [X0,X1] : ld(X0,mult(X0,mult(X0,X1))) = mult(ld(X0,mult(X0,mult(X0,mult(X1,X0)))),i(X0)),
inference(superposition,[],[f12287,f367]) ).
fof(f12719,plain,
! [X0,X1] : ld(X0,mult(X0,X1)) = mult(mult(X0,mult(ld(X0,X1),X0)),i(X0)),
inference(superposition,[],[f12287,f2255]) ).
fof(f12732,plain,
! [X0,X1] : i(X0) = ld(ld(X0,mult(X1,X0)),ld(X0,X1)),
inference(superposition,[],[f2,f12287]) ).
fof(f12733,plain,
! [X0,X1] : ld(X0,mult(X1,X0)) = rd(ld(X0,X1),i(X0)),
inference(superposition,[],[f4,f12287]) ).
fof(f12794,plain,
! [X0,X1] : mult(mult(X0,mult(ld(X0,X1),X0)),i(X0)) = X1,
inference(forward_demodulation,[],[f12719,f2]) ).
fof(f12813,plain,
! [X0,X1] : ld(X0,mult(X0,mult(X0,X1))) = mult(mult(X0,mult(X1,X0)),i(X0)),
inference(forward_demodulation,[],[f12696,f2]) ).
fof(f12860,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,mult(X1,X0)),i(X0)),
inference(forward_demodulation,[],[f12813,f2]) ).
fof(f12969,plain,
! [X0,X1] : mult(X1,i(X0)) = ld(X0,rd(mult(X0,X1),X0)),
inference(superposition,[],[f2,f12469]) ).
fof(f12998,plain,
! [X0,X1] : mult(X0,mult(ld(X0,mult(X1,i(X0))),X0)) = ld(X0,mult(rd(mult(X0,X1),X0),X0)),
inference(superposition,[],[f2255,f12469]) ).
fof(f13038,plain,
! [X0,X1] : ld(X0,mult(X0,X1)) = mult(X0,mult(ld(X0,mult(X1,i(X0))),X0)),
inference(forward_demodulation,[],[f12998,f3]) ).
fof(f13100,plain,
! [X0,X1] : mult(X0,mult(ld(X0,mult(X1,i(X0))),X0)) = X1,
inference(forward_demodulation,[],[f13038,f2]) ).
fof(f13918,plain,
! [X0,X1] : mult(X1,mult(ld(X1,X0),X1)) = rd(X0,i(X1)),
inference(superposition,[],[f4,f12794]) ).
fof(f14144,plain,
! [X0,X1] : mult(X1,rd(X0,X1)) = mult(mult(X1,X0),i(X1)),
inference(superposition,[],[f12860,f3]) ).
fof(f14171,plain,
! [X0,X1] : mult(X0,mult(X1,X0)) = rd(mult(X0,X1),i(X0)),
inference(superposition,[],[f4,f12860]) ).
fof(f15099,plain,
! [X0,X1] : mult(mult(i(mult(X1,mult(X1,ld(X1,mult(X0,i(X1)))))),X1),X0) = X1,
inference(superposition,[],[f366,f13100]) ).
fof(f15104,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X1,ld(X1,mult(X0,i(X1)))),mult(X1,X1)),
inference(superposition,[],[f3025,f13100]) ).
fof(f15106,plain,
! [X0,X1] : ld(X1,X0) = mult(ld(X1,mult(X0,i(X1))),X1),
inference(superposition,[],[f2,f13100]) ).
fof(f15183,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,i(X1)),mult(X1,X1)),
inference(forward_demodulation,[],[f15104,f1]) ).
fof(f15186,plain,
! [X0,X1] : mult(mult(i(mult(X1,mult(X0,i(X1)))),X1),X0) = X1,
inference(forward_demodulation,[],[f15099,f1]) ).
fof(f15228,plain,
! [X0,X1] : mult(mult(i(rd(mult(X1,X0),X1)),X1),X0) = X1,
inference(forward_demodulation,[],[f15186,f12469]) ).
fof(f16455,plain,
! [X0,X1] : mult(rd(X0,i(X1)),X1) = mult(mult(X1,ld(X1,X0)),mult(X1,X1)),
inference(superposition,[],[f3025,f13918]) ).
fof(f16543,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = mult(rd(X0,i(X1)),X1),
inference(forward_demodulation,[],[f16455,f1]) ).
fof(f18118,plain,
! [X0,X1] : rd(mult(X0,X1),X1) = mult(rd(mult(X0,i(X1)),X1),mult(X1,X1)),
inference(superposition,[],[f2997,f15183]) ).
fof(f18122,plain,
! [X0,X1] : mult(X1,X1) = ld(mult(X0,i(X1)),mult(X0,X1)),
inference(superposition,[],[f2,f15183]) ).
fof(f18123,plain,
! [X0,X1] : mult(X0,i(X1)) = rd(mult(X0,X1),mult(X1,X1)),
inference(superposition,[],[f4,f15183]) ).
fof(f18188,plain,
! [X0,X1] : mult(rd(mult(X0,i(X1)),X1),mult(X1,X1)) = X0,
inference(forward_demodulation,[],[f18118,f4]) ).
fof(f18328,plain,
! [X0,X1] : mult(mult(i(rd(X0,X1)),X1),ld(X1,X0)) = X1,
inference(superposition,[],[f15228,f1]) ).
fof(f18425,plain,
! [X0,X1] : rd(X0,X1) = mult(i(rd(mult(X0,X1),X0)),X0),
inference(superposition,[],[f4,f15228]) ).
fof(f20358,plain,
! [X0,X1] : mult(mult(X0,mult(i(X1),i(X1))),mult(X1,X1)) = mult(rd(X0,i(i(X1))),X1),
inference(superposition,[],[f15183,f16543]) ).
fof(f20367,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(mult(X0,mult(i(X1),i(X1))),mult(X1,X1)),
inference(forward_demodulation,[],[f20358,f35]) ).
fof(f20429,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(mult(X0,rd(i(X1),X1)),mult(X1,X1)),
inference(forward_demodulation,[],[f20367,f256]) ).
fof(f20468,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(mult(X0,ld(X1,i(X1))),mult(X1,X1)),
inference(forward_demodulation,[],[f20429,f915]) ).
fof(f20498,plain,
! [X0,X1] : mult(rd(X0,X1),X1) = mult(mult(X0,i(mult(X1,X1))),mult(X1,X1)),
inference(forward_demodulation,[],[f20468,f1074]) ).
fof(f20510,plain,
! [X0,X1] : mult(mult(X0,i(mult(X1,X1))),mult(X1,X1)) = X0,
inference(forward_demodulation,[],[f20498,f3]) ).
fof(f21465,plain,
! [X0,X1] : mult(i(X1),i(X1)) = ld(mult(mult(X1,mult(ld(X1,X0),X1)),i(i(X1))),X0),
inference(superposition,[],[f18122,f12794]) ).
fof(f21535,plain,
! [X0,X1] : mult(i(X1),i(X1)) = ld(mult(mult(X1,mult(ld(X1,X0),X1)),X1),X0),
inference(forward_demodulation,[],[f21465,f35]) ).
fof(f21613,plain,
! [X0,X1] : mult(i(X1),i(X1)) = ld(mult(mult(X1,ld(X1,X0)),mult(X1,X1)),X0),
inference(forward_demodulation,[],[f21535,f3025]) ).
fof(f21669,plain,
! [X0,X1] : mult(i(X1),i(X1)) = ld(mult(X0,mult(X1,X1)),X0),
inference(forward_demodulation,[],[f21613,f1]) ).
fof(f21708,plain,
! [X0,X1] : rd(i(X1),X1) = ld(mult(X0,mult(X1,X1)),X0),
inference(forward_demodulation,[],[f21669,f256]) ).
fof(f21734,plain,
! [X0,X1] : ld(X1,i(X1)) = ld(mult(X0,mult(X1,X1)),X0),
inference(forward_demodulation,[],[f21708,f915]) ).
fof(f21752,plain,
! [X0,X1] : i(mult(X1,X1)) = ld(mult(X0,mult(X1,X1)),X0),
inference(forward_demodulation,[],[f21734,f1074]) ).
fof(f21817,plain,
! [X0,X1] : rd(mult(mult(X0,X1),mult(X1,X1)),mult(X1,X1)) = mult(mult(X0,mult(X1,X1)),i(X1)),
inference(superposition,[],[f18123,f383]) ).
fof(f21822,plain,
! [X0,X1] : rd(X0,mult(i(X1),i(X1))) = mult(mult(X1,mult(ld(X1,X0),X1)),i(i(X1))),
inference(superposition,[],[f18123,f12794]) ).
fof(f21847,plain,
! [X0,X1] : mult(X0,i(X1)) = mult(rd(X0,mult(X1,X1)),X1),
inference(superposition,[],[f18123,f2735]) ).
fof(f21888,plain,
! [X0,X1] : mult(mult(X1,mult(ld(X1,X0),X1)),X1) = rd(X0,mult(i(X1),i(X1))),
inference(forward_demodulation,[],[f21822,f35]) ).
fof(f21893,plain,
! [X0,X1] : mult(X0,X1) = mult(mult(X0,mult(X1,X1)),i(X1)),
inference(forward_demodulation,[],[f21817,f4]) ).
fof(f21933,plain,
! [X0,X1] : mult(mult(X1,mult(ld(X1,X0),X1)),X1) = rd(X0,rd(i(X1),X1)),
inference(forward_demodulation,[],[f21888,f256]) ).
fof(f21961,plain,
! [X0,X1] : mult(mult(X1,mult(ld(X1,X0),X1)),X1) = rd(X0,ld(X1,i(X1))),
inference(forward_demodulation,[],[f21933,f915]) ).
fof(f21982,plain,
! [X0,X1] : mult(mult(X1,mult(ld(X1,X0),X1)),X1) = rd(X0,i(mult(X1,X1))),
inference(forward_demodulation,[],[f21961,f1074]) ).
fof(f22000,plain,
! [X0,X1] : rd(X0,i(mult(X1,X1))) = mult(mult(X1,ld(X1,X0)),mult(X1,X1)),
inference(forward_demodulation,[],[f21982,f3025]) ).
fof(f22012,plain,
! [X0,X1] : mult(X0,mult(X1,X1)) = rd(X0,i(mult(X1,X1))),
inference(forward_demodulation,[],[f22000,f1]) ).
fof(f22053,plain,
! [X0,X1] : mult(rd(X0,X1),mult(X1,X1)) = rd(X0,i(X1)),
inference(superposition,[],[f18188,f3]) ).
fof(f22077,plain,
! [X0,X1] : rd(X0,mult(X1,X1)) = rd(mult(X0,i(X1)),X1),
inference(superposition,[],[f4,f18188]) ).
fof(f22279,plain,
! [X0,X1] : mult(mult(i(X0),X1),ld(X1,mult(X0,X1))) = X1,
inference(superposition,[],[f18328,f4]) ).
fof(f22368,plain,
! [X0,X1] : mult(i(rd(X1,X0)),X0) = rd(X0,ld(X0,X1)),
inference(superposition,[],[f4,f18328]) ).
fof(f23969,plain,
! [X0,X1] : rd(X0,mult(X1,X1)) = mult(X0,i(mult(X1,X1))),
inference(superposition,[],[f4,f20510]) ).
fof(f24874,plain,
! [X0,X1] : i(mult(X1,X1)) = ld(X0,rd(X0,mult(X1,X1))),
inference(superposition,[],[f21752,f3]) ).
fof(f26987,plain,
! [X0,X1] : mult(mult(i(i(rd(mult(X0,X1),X0))),X0),ld(X0,rd(X0,X1))) = X0,
inference(superposition,[],[f22279,f18425]) ).
fof(f27101,plain,
! [X0,X1] : mult(mult(rd(mult(X0,X1),X0),X0),ld(X0,rd(X0,X1))) = X0,
inference(forward_demodulation,[],[f26987,f35]) ).
fof(f27202,plain,
! [X0,X1] : mult(mult(X0,X1),ld(X0,rd(X0,X1))) = X0,
inference(forward_demodulation,[],[f27101,f3]) ).
fof(f27408,plain,
! [X0,X1] : mult(mult(X1,ld(X0,X1)),ld(X1,X0)) = X1,
inference(superposition,[],[f27202,f45]) ).
fof(f28155,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = rd(X0,ld(X0,X1)),
inference(superposition,[],[f4,f27408]) ).
fof(f29393,plain,
! [X0,X1] : mult(X0,ld(X1,X0)) = mult(i(rd(X1,X0)),X0),
inference(forward_demodulation,[],[f22368,f28155]) ).
fof(f32771,plain,
! [X0,X1] : i(X0) = ld(ld(X0,mult(X0,ld(X1,X0))),ld(X0,i(rd(X1,X0)))),
inference(superposition,[],[f12732,f29393]) ).
fof(f32845,plain,
! [X0,X1] : i(X0) = ld(ld(X1,X0),ld(X0,i(rd(X1,X0)))),
inference(forward_demodulation,[],[f32771,f2]) ).
fof(f36063,plain,
! [X2,X0,X1] : mult(mult(X1,mult(X2,X0)),X2) = mult(mult(X1,X2),rd(X0,i(X2))),
inference(forward_demodulation,[],[f327,f13918]) ).
fof(f36367,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),i(X0)) = mult(unit,rd(X1,i(i(X0)))),
inference(superposition,[],[f36063,f10]) ).
fof(f36419,plain,
! [X0,X1] : mult(mult(i(X0),mult(X0,X1)),X0) = mult(unit,rd(X1,i(X0))),
inference(superposition,[],[f36063,f12]) ).
fof(f36622,plain,
! [X0,X1] : rd(X1,i(X0)) = mult(mult(i(X0),mult(X0,X1)),X0),
inference(forward_demodulation,[],[f36419,f6]) ).
fof(f36656,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),i(X0)) = rd(X1,i(i(X0))),
inference(forward_demodulation,[],[f36367,f6]) ).
fof(f36699,plain,
! [X0,X1] : mult(mult(X0,mult(i(X0),X1)),X0) = rd(X1,i(X0)),
inference(forward_demodulation,[],[f36622,f3303]) ).
fof(f36713,plain,
! [X0,X1] : rd(X1,X0) = mult(mult(X0,mult(i(X0),X1)),i(X0)),
inference(forward_demodulation,[],[f36656,f35]) ).
fof(f36736,plain,
! [X0,X1] : rd(X1,X0) = mult(X0,rd(mult(i(X0),X1),X0)),
inference(forward_demodulation,[],[f36713,f14144]) ).
fof(f36790,plain,
! [X0,X1] : mult(X1,rd(X0,X1)) = rd(ld(i(X1),X0),X1),
inference(superposition,[],[f36736,f1]) ).
fof(f36829,plain,
! [X0,X1] : ld(X1,rd(X0,X1)) = rd(mult(i(X1),X0),X1),
inference(superposition,[],[f2,f36736]) ).
fof(f36840,plain,
! [X0,X1] : mult(mult(rd(X0,X1),X1),X1) = mult(X1,mult(mult(rd(mult(i(X1),X0),X1),X1),X1)),
inference(superposition,[],[f102,f36736]) ).
fof(f36953,plain,
! [X0,X1] : mult(mult(rd(X0,X1),X1),X1) = mult(X1,mult(mult(i(X1),X0),X1)),
inference(forward_demodulation,[],[f36840,f3]) ).
fof(f37024,plain,
! [X0,X1] : mult(X0,X1) = mult(X1,mult(mult(i(X1),X0),X1)),
inference(forward_demodulation,[],[f36953,f3]) ).
fof(f37141,plain,
! [X0,X1] : mult(mult(X0,rd(X1,X0)),X0) = ld(i(X0),X1),
inference(superposition,[],[f3,f36790]) ).
fof(f37345,plain,
! [X0,X1] : mult(i(X0),X1) = mult(ld(X0,rd(X1,X0)),X0),
inference(superposition,[],[f3,f36829]) ).
fof(f38165,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = ld(i(X1),mult(X0,X1)),
inference(superposition,[],[f37141,f4]) ).
fof(f38871,plain,
! [X0,X1] : mult(ld(X1,X0),X1) = mult(i(X1),mult(X0,X1)),
inference(superposition,[],[f37345,f4]) ).
fof(f40774,plain,
! [X0,X1] : ld(i(mult(X1,X1)),X0) = mult(mult(mult(X1,X1),mult(X0,i(mult(X1,X1)))),mult(X1,X1)),
inference(superposition,[],[f38165,f20510]) ).
fof(f40902,plain,
! [X0,X1] : ld(i(mult(X1,X1)),X0) = mult(rd(mult(mult(X1,X1),X0),mult(X1,X1)),mult(X1,X1)),
inference(forward_demodulation,[],[f40774,f12469]) ).
fof(f40990,plain,
! [X0,X1] : mult(mult(X1,X1),X0) = ld(i(mult(X1,X1)),X0),
inference(forward_demodulation,[],[f40902,f3]) ).
fof(f41170,plain,
! [X0,X1] : mult(ld(mult(X1,X1),mult(X0,i(mult(X1,X1)))),mult(X1,X1)) = mult(i(mult(X1,X1)),X0),
inference(superposition,[],[f38871,f20510]) ).
fof(f41404,plain,
! [X0,X1] : ld(mult(X1,X1),X0) = mult(i(mult(X1,X1)),X0),
inference(forward_demodulation,[],[f41170,f15106]) ).
fof(f50763,plain,
! [X0,X1] : mult(mult(X1,X0),X1) = rd(ld(i(X1),X0),i(X1)),
inference(superposition,[],[f36699,f1]) ).
fof(f50776,plain,
! [X0,X1] : rd(mult(mult(ld(i(X1),X0),i(X1)),i(X1)),i(X1)) = mult(mult(X1,mult(mult(X0,i(X1)),i(X1))),X1),
inference(superposition,[],[f36699,f120]) ).
fof(f50777,plain,
! [X0,X1] : mult(mult(X0,mult(mult(i(X0),X1),i(X0))),X0) = rd(mult(mult(mult(X1,i(X0)),i(X0)),i(i(X0))),i(X0)),
inference(superposition,[],[f36699,f101]) ).
fof(f51017,plain,
! [X0,X1] : mult(mult(X0,mult(mult(i(X0),X1),i(X0))),X0) = rd(mult(mult(X1,i(X0)),i(X0)),mult(i(X0),i(X0))),
inference(forward_demodulation,[],[f50777,f22077]) ).
fof(f51018,plain,
! [X0,X1] : rd(mult(mult(ld(i(X1),X0),i(X1)),i(X1)),i(X1)) = mult(rd(mult(X1,mult(X0,i(X1))),X1),X1),
inference(forward_demodulation,[],[f50776,f12469]) ).
fof(f51124,plain,
! [X0,X1] : mult(mult(X0,mult(mult(i(X0),X1),i(X0))),X0) = mult(rd(mult(X1,i(X0)),mult(i(X0),i(X0))),i(X0)),
inference(forward_demodulation,[],[f51017,f2735]) ).
fof(f51125,plain,
! [X0,X1] : mult(X1,mult(X0,i(X1))) = rd(mult(mult(ld(i(X1),X0),i(X1)),i(X1)),i(X1)),
inference(forward_demodulation,[],[f51018,f3]) ).
fof(f51198,plain,
! [X0,X1] : mult(mult(X0,mult(mult(i(X0),X1),i(X0))),X0) = mult(mult(X1,i(X0)),i(i(X0))),
inference(forward_demodulation,[],[f51124,f21847]) ).
fof(f51199,plain,
! [X0,X1] : mult(ld(i(X1),X0),i(X1)) = mult(X1,mult(X0,i(X1))),
inference(forward_demodulation,[],[f51125,f4]) ).
fof(f51225,plain,
! [X0,X1] : mult(mult(X1,i(X0)),X0) = mult(mult(X0,mult(mult(i(X0),X1),i(X0))),X0),
inference(forward_demodulation,[],[f51198,f35]) ).
fof(f51226,plain,
! [X0,X1] : mult(ld(i(X1),X0),i(X1)) = rd(mult(X1,X0),X1),
inference(forward_demodulation,[],[f51199,f12469]) ).
fof(f51240,plain,
! [X0,X1] : mult(mult(X1,i(X0)),X0) = mult(rd(mult(X0,mult(i(X0),X1)),X0),X0),
inference(forward_demodulation,[],[f51225,f12469]) ).
fof(f51251,plain,
! [X0,X1] : mult(X0,mult(i(X0),X1)) = mult(mult(X1,i(X0)),X0),
inference(forward_demodulation,[],[f51240,f3]) ).
fof(f51326,plain,
! [X0,X1] : mult(mult(mult(X0,X1),X0),i(X0)) = ld(i(X0),X1),
inference(superposition,[],[f3,f50763]) ).
fof(f52695,plain,
! [X0,X1] : mult(X0,i(X1)) = rd(mult(X1,mult(i(X1),X0)),X1),
inference(superposition,[],[f51226,f2]) ).
fof(f55976,plain,
! [X0,X1] : i(X0) = mult(mult(i(mult(i(X0),mult(i(X0),mult(mult(X0,X1),X0)))),i(X0)),mult(i(X0),ld(i(X0),X1))),
inference(superposition,[],[f366,f51326]) ).
fof(f56087,plain,
! [X0,X1] : i(X0) = mult(mult(i(mult(i(X0),mult(i(X0),mult(mult(X0,X1),X0)))),i(X0)),X1),
inference(forward_demodulation,[],[f55976,f1]) ).
fof(f56239,plain,
! [X0,X1] : i(X0) = mult(mult(i(mult(i(X0),mult(ld(X0,mult(X0,X1)),X0))),i(X0)),X1),
inference(forward_demodulation,[],[f56087,f38871]) ).
fof(f56349,plain,
! [X0,X1] : i(X0) = mult(mult(i(mult(ld(X0,ld(X0,mult(X0,X1))),X0)),i(X0)),X1),
inference(forward_demodulation,[],[f56239,f38871]) ).
fof(f56426,plain,
! [X0,X1] : i(X0) = mult(mult(i(mult(ld(X0,X1),X0)),i(X0)),X1),
inference(forward_demodulation,[],[f56349,f2]) ).
fof(f103307,plain,
! [X0,X1] : i(X1) = mult(mult(i(mult(X0,X1)),i(X1)),mult(X1,X0)),
inference(superposition,[],[f56426,f2]) ).
fof(f103467,plain,
! [X0,X1] : rd(i(X0),X1) = mult(i(mult(ld(X0,X1),X0)),i(X0)),
inference(superposition,[],[f4,f56426]) ).
fof(f104997,plain,
! [X0,X1] : i(X1) = mult(mult(i(X0),i(X1)),mult(X1,rd(X0,X1))),
inference(superposition,[],[f103307,f3]) ).
fof(f106241,plain,
! [X0,X1] : i(mult(ld(X0,X1),X0)) = rd(rd(i(X0),X1),i(X0)),
inference(superposition,[],[f4,f103467]) ).
fof(f108377,plain,
! [X0,X1] : i(X1) = mult(mult(X0,i(X1)),mult(X1,rd(i(X0),X1))),
inference(superposition,[],[f104997,f35]) ).
fof(f110678,plain,
! [X0,X1] : rd(X0,i(X1)) = i(mult(ld(X1,ld(X0,i(X1))),X1)),
inference(superposition,[],[f106241,f45]) ).
fof(f114283,plain,
! [X0,X1] : ld(mult(X1,i(X0)),i(X0)) = mult(X0,rd(i(X1),X0)),
inference(superposition,[],[f2,f108377]) ).
fof(f115737,plain,
! [X0,X1] : unit = mult(mult(ld(X1,ld(X0,i(X1))),X1),rd(X0,i(X1))),
inference(superposition,[],[f10,f110678]) ).
fof(f115739,plain,
! [X0,X1] : i(rd(X0,i(X1))) = mult(ld(X1,ld(X0,i(X1))),X1),
inference(superposition,[],[f35,f110678]) ).
fof(f115967,plain,
! [X0,X1] : unit = mult(mult(ld(X1,ld(X0,i(X1))),mult(X1,X0)),X1),
inference(forward_demodulation,[],[f115737,f36063]) ).
fof(f120074,plain,
! [X0,X1] : rd(unit,X0) = mult(ld(X0,ld(X1,i(X0))),mult(X0,X1)),
inference(superposition,[],[f4,f115967]) ).
fof(f120411,plain,
! [X0,X1] : i(X0) = mult(ld(X0,ld(X1,i(X0))),mult(X0,X1)),
inference(forward_demodulation,[],[f120074,f47]) ).
fof(f121040,plain,
! [X0,X1] : i(X1) = mult(ld(X1,X0),mult(X1,rd(i(X1),X0))),
inference(superposition,[],[f120411,f40]) ).
fof(f121070,plain,
! [X0,X1] : i(X1) = mult(ld(X1,ld(mult(ld(X1,X0),i(X1)),i(X1))),rd(X0,X1)),
inference(superposition,[],[f120411,f12258]) ).
fof(f121212,plain,
! [X0,X1] : mult(X0,X1) = ld(ld(X0,ld(X1,i(X0))),i(X0)),
inference(superposition,[],[f2,f120411]) ).
fof(f121213,plain,
! [X0,X1] : rd(i(X0),mult(X0,X1)) = ld(X0,ld(X1,i(X0))),
inference(superposition,[],[f4,f120411]) ).
fof(f121493,plain,
! [X0,X1] : i(X1) = mult(ld(X1,mult(X1,rd(i(ld(X1,X0)),X1))),rd(X0,X1)),
inference(forward_demodulation,[],[f121070,f114283]) ).
fof(f121631,plain,
! [X0,X1] : i(X1) = mult(rd(i(ld(X1,X0)),X1),rd(X0,X1)),
inference(forward_demodulation,[],[f121493,f2]) ).
fof(f122852,plain,
! [X0,X1] : ld(ld(X0,X1),i(X0)) = mult(X0,rd(i(X0),X1)),
inference(superposition,[],[f2,f121040]) ).
fof(f124133,plain,
! [X0,X1] : i(mult(ld(X0,mult(X0,X1)),X0)) = rd(ld(X0,ld(X1,i(X0))),i(X0)),
inference(superposition,[],[f110678,f121212]) ).
fof(f124134,plain,
! [X0,X1] : mult(ld(X0,mult(X0,X1)),X0) = i(rd(ld(X0,ld(X1,i(X0))),i(X0))),
inference(superposition,[],[f115739,f121212]) ).
fof(f124218,plain,
! [X0,X1] : mult(ld(X0,mult(X0,X1)),X0) = i(ld(X0,mult(ld(X1,i(X0)),X0))),
inference(forward_demodulation,[],[f124134,f12733]) ).
fof(f124219,plain,
! [X0,X1] : ld(X0,mult(ld(X1,i(X0)),X0)) = i(mult(ld(X0,mult(X0,X1)),X0)),
inference(forward_demodulation,[],[f124133,f12733]) ).
fof(f124289,plain,
! [X0,X1] : mult(X1,X0) = i(ld(X0,mult(ld(X1,i(X0)),X0))),
inference(forward_demodulation,[],[f124218,f2]) ).
fof(f124290,plain,
! [X0,X1] : i(mult(X1,X0)) = ld(X0,mult(ld(X1,i(X0)),X0)),
inference(forward_demodulation,[],[f124219,f2]) ).
fof(f124385,plain,
! [X0,X1] : rd(i(X0),rd(mult(X0,X1),X0)) = ld(X0,ld(mult(X1,i(X0)),i(X0))),
inference(superposition,[],[f121213,f12469]) ).
fof(f124723,plain,
! [X0,X1] : rd(i(X0),rd(mult(X0,X1),X0)) = ld(X0,mult(X0,rd(i(X1),X0))),
inference(forward_demodulation,[],[f124385,f114283]) ).
fof(f124820,plain,
! [X0,X1] : rd(i(X0),rd(mult(X0,X1),X0)) = rd(i(X1),X0),
inference(forward_demodulation,[],[f124723,f2]) ).
fof(f131075,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = i(ld(X1,mult(mult(mult(X0,X0),i(X1)),X1))),
inference(superposition,[],[f124289,f40990]) ).
fof(f131356,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = i(ld(X1,mult(X1,mult(i(X1),mult(X0,X0))))),
inference(forward_demodulation,[],[f131075,f51251]) ).
fof(f131423,plain,
! [X0,X1] : mult(i(mult(X0,X0)),X1) = i(mult(i(X1),mult(X0,X0))),
inference(forward_demodulation,[],[f131356,f2]) ).
fof(f131463,plain,
! [X0,X1] : ld(mult(X0,X0),X1) = i(mult(i(X1),mult(X0,X0))),
inference(forward_demodulation,[],[f131423,f41404]) ).
fof(f131596,plain,
! [X0,X1] : mult(X1,i(mult(X0,X1))) = mult(ld(X0,i(X1)),X1),
inference(superposition,[],[f1,f124290]) ).
fof(f139942,plain,
! [X0,X1] : ld(mult(X0,X0),rd(mult(mult(X0,X0),X1),mult(X0,X0))) = i(rd(mult(X0,X0),X1)),
inference(superposition,[],[f131463,f18425]) ).
fof(f140249,plain,
! [X0,X1] : mult(X1,i(mult(X0,X0))) = i(rd(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f139942,f12969]) ).
fof(f140300,plain,
! [X0,X1] : rd(X1,mult(X0,X0)) = i(rd(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f140249,f23969]) ).
fof(f140425,plain,
! [X0,X1] : i(X0) = rd(ld(X0,mult(X1,X1)),mult(X1,X1)),
inference(superposition,[],[f140300,f45]) ).
fof(f140447,plain,
! [X0,X1] : i(X0) = ld(ld(mult(X1,X1),X0),ld(X0,rd(X0,mult(X1,X1)))),
inference(superposition,[],[f32845,f140300]) ).
fof(f140456,plain,
! [X0,X1] : i(rd(X0,mult(X1,X1))) = rd(mult(X1,X1),X0),
inference(superposition,[],[f35,f140300]) ).
fof(f140721,plain,
! [X0,X1] : i(X0) = ld(ld(mult(X1,X1),X0),i(mult(X1,X1))),
inference(forward_demodulation,[],[f140447,f24874]) ).
fof(f140769,plain,
! [X0,X1] : i(X0) = mult(mult(X1,X1),rd(i(mult(X1,X1)),X0)),
inference(forward_demodulation,[],[f140721,f122852]) ).
fof(f140904,plain,
! [X0,X1] : ld(X0,mult(X1,X1)) = mult(i(X0),mult(X1,X1)),
inference(superposition,[],[f3,f140425]) ).
fof(f141198,plain,
! [X0,X1] : i(X0) = rd(mult(X1,X1),mult(X0,mult(X1,X1))),
inference(superposition,[],[f140456,f4]) ).
fof(f141695,plain,
! [X0,X1] : mult(mult(X1,X1),i(X0)) = rd(mult(X0,ld(X0,mult(X1,X1))),X0),
inference(superposition,[],[f52695,f140904]) ).
fof(f142125,plain,
! [X0,X1] : rd(mult(X1,X1),X0) = mult(mult(X1,X1),i(X0)),
inference(forward_demodulation,[],[f141695,f1]) ).
fof(f148394,plain,
! [X0,X1] : mult(ld(X1,i(mult(X0,X0))),X0) = mult(mult(mult(X0,X0),i(mult(X1,mult(X0,X0)))),i(X0)),
inference(superposition,[],[f21893,f131596]) ).
fof(f148473,plain,
! [X0,X1] : mult(rd(mult(X0,X0),mult(X1,mult(X0,X0))),i(X0)) = mult(ld(X1,i(mult(X0,X0))),X0),
inference(forward_demodulation,[],[f148394,f142125]) ).
fof(f148637,plain,
! [X0,X1] : mult(i(X1),i(X0)) = mult(ld(X1,i(mult(X0,X0))),X0),
inference(forward_demodulation,[],[f148473,f141198]) ).
fof(f169166,plain,
! [X0,X1] : i(mult(mult(X0,X0),X1)) = mult(mult(X0,X0),ld(mult(X0,X0),ld(X1,i(mult(X0,X0))))),
inference(superposition,[],[f140769,f121213]) ).
fof(f169531,plain,
! [X0,X1] : ld(X1,i(mult(X0,X0))) = i(mult(mult(X0,X0),X1)),
inference(forward_demodulation,[],[f169166,f1]) ).
fof(f233112,plain,
! [X0,X1] : mult(i(X1),i(X0)) = mult(i(mult(mult(X0,X0),X1)),X0),
inference(forward_demodulation,[],[f148637,f169531]) ).
fof(f242397,plain,
! [X0,X1] : ld(i(mult(mult(X1,X1),X0)),mult(i(X0),i(X1))) = X1,
inference(superposition,[],[f2,f233112]) ).
fof(f247615,plain,
! [X0,X1] : ld(i(mult(mult(X0,X0),rd(mult(i(X0),X1),i(X0)))),rd(i(X0),X1)) = X0,
inference(superposition,[],[f242397,f18425]) ).
fof(f247800,plain,
! [X0,X1] : ld(i(mult(mult(X0,mult(X0,mult(i(X0),X1))),X0)),rd(i(X0),X1)) = X0,
inference(forward_demodulation,[],[f247615,f36063]) ).
fof(f247964,plain,
! [X0,X1] : ld(i(mult(X0,mult(X0,mult(mult(i(X0),X1),X0)))),rd(i(X0),X1)) = X0,
inference(forward_demodulation,[],[f247800,f367]) ).
fof(f248091,plain,
! [X0,X1] : ld(i(mult(X0,mult(X1,X0))),rd(i(X0),X1)) = X0,
inference(forward_demodulation,[],[f247964,f37024]) ).
fof(f248728,plain,
! [X0,X1] : mult(i(mult(X0,mult(X1,X0))),X0) = rd(i(X0),X1),
inference(superposition,[],[f1,f248091]) ).
fof(f251133,plain,
! [X0,X1] : i(X0) = mult(rd(i(i(X0)),X1),mult(X0,rd(mult(i(X0),mult(X1,i(X0))),X0))),
inference(superposition,[],[f104997,f248728]) ).
fof(f251534,plain,
! [X0,X1] : i(X0) = mult(rd(i(i(X0)),X1),rd(mult(X1,i(X0)),X0)),
inference(forward_demodulation,[],[f251133,f36736]) ).
fof(f251848,plain,
! [X0,X1] : i(X0) = mult(rd(i(i(X0)),X1),rd(X1,mult(X0,X0))),
inference(forward_demodulation,[],[f251534,f22077]) ).
fof(f252037,plain,
! [X0,X1] : i(X0) = mult(rd(X0,X1),rd(X1,mult(X0,X0))),
inference(forward_demodulation,[],[f251848,f35]) ).
fof(f252944,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),rd(rd(mult(X1,X0),X1),mult(i(X1),i(X1)))),
inference(superposition,[],[f252037,f124820]) ).
fof(f253400,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),rd(rd(mult(X1,X0),X1),rd(i(X1),X1))),
inference(forward_demodulation,[],[f252944,f256]) ).
fof(f253567,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),rd(rd(mult(X1,X0),X1),ld(X1,i(X1)))),
inference(forward_demodulation,[],[f253400,f915]) ).
fof(f253669,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),rd(rd(mult(X1,X0),X1),i(mult(X1,X1)))),
inference(forward_demodulation,[],[f253567,f1074]) ).
fof(f253739,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),mult(rd(mult(X1,X0),X1),mult(X1,X1))),
inference(forward_demodulation,[],[f253669,f22012]) ).
fof(f253793,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),rd(mult(X1,X0),i(X1))),
inference(forward_demodulation,[],[f253739,f22053]) ).
fof(f253839,plain,
! [X0,X1] : i(i(X1)) = mult(rd(i(X0),X1),mult(X1,mult(X0,X1))),
inference(forward_demodulation,[],[f253793,f14171]) ).
fof(f253873,plain,
! [X0,X1] : mult(rd(i(X0),X1),mult(X1,mult(X0,X1))) = X1,
inference(forward_demodulation,[],[f253839,f35]) ).
fof(f260691,plain,
! [X0,X1] : mult(rd(i(i(mult(X0,mult(X1,X0)))),X0),mult(X0,rd(i(X0),X1))) = X0,
inference(superposition,[],[f253873,f248728]) ).
fof(f261008,plain,
! [X0,X1] : mult(rd(mult(X0,mult(X1,X0)),X0),mult(X0,rd(i(X0),X1))) = X0,
inference(forward_demodulation,[],[f260691,f35]) ).
fof(f261245,plain,
! [X0,X1] : mult(mult(mult(X0,rd(X1,X0)),X0),mult(X0,rd(i(X0),X1))) = X0,
inference(forward_demodulation,[],[f261008,f704]) ).
fof(f261387,plain,
! [X0,X1] : mult(X0,mult(mult(mult(rd(X1,X0),X0),X0),rd(i(X0),X1))) = X0,
inference(forward_demodulation,[],[f261245,f7]) ).
fof(f261471,plain,
! [X0,X1] : mult(X0,mult(mult(X1,X0),rd(i(X0),X1))) = X0,
inference(forward_demodulation,[],[f261387,f3]) ).
fof(f272750,plain,
! [X0,X1] : mult(mult(X1,X0),rd(i(X0),X1)) = ld(mult(X0,mult(mult(mult(X1,X0),rd(i(X0),X1)),mult(mult(X1,X0),rd(i(X0),X1)))),mult(X0,mult(mult(mult(X1,X0),rd(i(X0),X1)),mult(mult(X1,X0),rd(i(X0),X1))))),
inference(superposition,[],[f511,f261471]) ).
fof(f273069,plain,
! [X0,X1] : unit = mult(mult(X1,X0),rd(i(X0),X1)),
inference(forward_demodulation,[],[f272750,f23]) ).
fof(f274118,plain,
! [X0,X1] : rd(i(X1),X0) = ld(mult(X0,X1),unit),
inference(superposition,[],[f2,f273069]) ).
fof(f274467,plain,
! [X0,X1] : i(mult(X0,X1)) = rd(i(X1),X0),
inference(forward_demodulation,[],[f274118,f24]) ).
fof(f275930,plain,
! [X0,X1] : i(X0) = mult(rd(i(ld(X0,i(X1))),X0),i(mult(X0,X1))),
inference(superposition,[],[f121631,f274467]) ).
fof(f276137,plain,
! [X0,X1] : i(X0) = mult(i(mult(X0,ld(X0,i(X1)))),i(mult(X0,X1))),
inference(forward_demodulation,[],[f275930,f274467]) ).
fof(f276313,plain,
! [X0,X1] : i(X0) = mult(i(i(X1)),i(mult(X0,X1))),
inference(forward_demodulation,[],[f276137,f1]) ).
fof(f276381,plain,
! [X0,X1] : i(X0) = mult(X1,i(mult(X0,X1))),
inference(forward_demodulation,[],[f276313,f35]) ).
fof(f288838,plain,
i(b) != i(b),
inference(superposition,[],[f13,f276381]) ).
fof(f288839,plain,
$false,
inference(trivial_inequality_removal,[],[f288838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP701-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 10:31:50 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 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
% 15.99/2.85 % (2351995)Will run a generic schedule for satisfiability detection.
% 15.99/2.85 % (2352007)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4095350970:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.99/2.85 % (2352003)% WARNING: option uhcvi not known.
% 15.99/2.85 % (2352002)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=484566925_2999 on theBenchmark for (2999ds/0Mi)
% 15.99/2.85 % (2352006)dis+10_1_sil=32000:sp=arity:random_seed=3003681034:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.99/2.85 % (2352003)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=120839431:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.99/2.85 % (2352004)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=406981152:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.99/2.85 % (2352008)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2971320662:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.99/2.85 % (2352009)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1554683525:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.99/2.85 % TRYING [1]
% 15.99/2.85 % TRYING [2]
% 15.99/2.85 % TRYING [3]
% 15.99/2.85 % TRYING [4]
% 15.99/2.85 % TRYING [5]
% 15.99/2.85 % (2352007)Instruction limit reached!
% 15.99/2.85 % (2352007)------------------------------
% 15.99/2.85 % (2352007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.99/2.85 % (2352007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.99/2.85 % (2352007)CaDiCaL version: 2.1.3
% 15.99/2.85 % (2352007)Termination reason: Instruction limit
% 15.99/2.85 % (2352007)Termination phase: Saturation
% 15.99/2.85 % (2352007)Time elapsed: 0.039 s
% 15.99/2.85 % (2352007)Peak memory usage: 12 MB
% 15.99/2.85 % (2352007)Instructions burned: 118 (million)
% 15.99/2.85 % (2352029)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=236305657:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.99/2.85 % TRYING [1]
% 15.99/2.85 % TRYING [2]
% 15.99/2.85 % TRYING [6]
% 15.99/2.85 % TRYING [3]
% 15.99/2.85 % (2352006)Instruction limit reached!
% 15.99/2.85 % (2352006)------------------------------
% 15.99/2.85 % (2352006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.99/2.85 % (2352006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.99/2.85 % (2352006)CaDiCaL version: 2.1.3
% 15.99/2.85 % (2352006)Termination reason: Instruction limit
% 15.99/2.85 % (2352006)Termination phase: Saturation
% 15.99/2.85 % (2352006)Time elapsed: 0.058 s
% 15.99/2.85 % (2352006)Peak memory usage: 12 MB
% 15.99/2.85 % (2352006)Instructions burned: 103 (million)
% 15.99/2.85 % TRYING [4]
% 15.99/2.85 % (2352039)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2512168748:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.99/2.85 % (2352008)Instruction limit reached!
% 15.99/2.85 % (2352008)------------------------------
% 15.99/2.85 % (2352008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.99/2.85 % (2352008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.99/2.85 % (2352008)CaDiCaL version: 2.1.3
% 15.99/2.85 % (2352008)Termination reason: Instruction limit
% 15.99/2.85 % (2352008)Termination phase: Saturation
% 15.99/2.85 % (2352008)Time elapsed: 0.076 s
% 15.99/2.85 % (2352008)Peak memory usage: 12 MB
% 15.99/2.85 % (2352008)Instructions burned: 131 (million)
% 15.99/2.85 % TRYING [5]
% 15.99/2.85 % (2352009)Instruction limit reached!
% 15.99/2.85 % (2352009)------------------------------
% 15.99/2.85 % (2352009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.99/2.85 % (2352009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.99/2.85 % (2352009)CaDiCaL version: 2.1.3
% 15.99/2.85 % (2352009)Termination reason: Instruction limit
% 15.99/2.85 % (2352009)Termination phase: Saturation
% 15.99/2.85 % (2352009)Time elapsed: 0.096 s
% 15.99/2.85 % (2352009)Peak memory usage: 12 MB
% 15.99/2.85 % (2352009)Instructions burned: 159 (million)
% 15.99/2.85 % (2352047)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=2761746831:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.99/2.85 % (2352039)Instruction limit reached!
% 15.99/2.85 % (2352039)------------------------------
% 15.99/2.85 % (2352039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.99/2.85 % (2352039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352039)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352039)Termination reason: Instruction limit
% 49.42/7.46 % (2352039)Termination phase: Saturation
% 49.42/7.46 % (2352039)Time elapsed: 0.046 s
% 49.42/7.46 % (2352039)Peak memory usage: 13 MB
% 49.42/7.46 % (2352039)Instructions burned: 133 (million)
% 49.42/7.46 % (2352054)ott-21_1_sil=16000:fs=off:random_seed=1422496437:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 49.42/7.46 % (2352062)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1709170907:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 49.42/7.46 % TRYING [6]
% 49.42/7.46 % TRYING [7]
% 49.42/7.46 % (2352054)Instruction limit reached!
% 49.42/7.46 % (2352054)------------------------------
% 49.42/7.46 % (2352054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.46 % (2352054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352054)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352054)Termination reason: Instruction limit
% 49.42/7.46 % (2352054)Termination phase: Saturation
% 49.42/7.46 % (2352054)Time elapsed: 0.118 s
% 49.42/7.46 % (2352054)Peak memory usage: 13 MB
% 49.42/7.46 % (2352054)Instructions burned: 180 (million)
% 49.42/7.46 % (2352099)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1673955086:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 49.42/7.46 % TRYING [1]
% 49.42/7.46 % TRYING [2]
% 49.42/7.46 % TRYING [3]
% 49.42/7.46 % (2352062)Instruction limit reached!
% 49.42/7.46 % (2352062)------------------------------
% 49.42/7.46 % (2352062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.46 % (2352062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352062)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352062)Termination reason: Instruction limit
% 49.42/7.46 % (2352062)Termination phase: Saturation
% 49.42/7.46 % (2352062)Time elapsed: 0.138 s
% 49.42/7.46 % (2352062)Peak memory usage: 17 MB
% 49.42/7.46 % (2352062)Instructions burned: 479 (million)
% 49.42/7.46 % TRYING [4]
% 49.42/7.46 % (2352102)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1764815364:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 49.42/7.46 % TRYING [7]
% 49.42/7.46 % TRYING [5]
% 49.42/7.46 % TRYING [6]
% 49.42/7.46 % (2352029)Instruction limit reached!
% 49.42/7.46 % (2352029)------------------------------
% 49.42/7.46 % (2352029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.46 % (2352029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352029)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352029)Termination reason: Instruction limit
% 49.42/7.46 % (2352029)Termination phase: Finite model building constraint generation
% 49.42/7.46 % (2352029)Time elapsed: 0.323 s
% 49.42/7.46 % (2352029)Peak memory usage: 27 MB
% 49.42/7.46 % (2352029)Instructions burned: 716 (million)
% 49.42/7.46 % (2352122)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3886593027:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 49.42/7.46 % (2352047)Instruction limit reached!
% 49.42/7.46 % (2352047)------------------------------
% 49.42/7.46 % (2352047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.46 % (2352047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352047)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352047)Termination reason: Instruction limit
% 49.42/7.46 % (2352047)Termination phase: Saturation
% 49.42/7.46 % (2352047)Time elapsed: 0.386 s
% 49.42/7.46 % (2352047)Peak memory usage: 17 MB
% 49.42/7.46 % (2352047)Instructions burned: 685 (million)
% 49.42/7.46 % TRYING [14]
% 49.42/7.46 % (2352124)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=234873064:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 49.42/7.46 % TRYING [8]
% 49.42/7.46 % TRYING [7]
% 49.42/7.46 % (2352099)Instruction limit reached!
% 49.42/7.46 % (2352099)------------------------------
% 49.42/7.46 % (2352099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.42/7.46 % (2352099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.42/7.46 % (2352099)CaDiCaL version: 2.1.3
% 49.42/7.46 % (2352099)Termination reason: Instruction limit
% 49.42/7.46 % (2352099)Termination phase: Finite model building constraint generation
% 49.42/7.46 % (2352099)Time elapsed: 0.347 s
% 49.42/7.46 % (2352099)Peak memory usage: 25 MB
% 49.42/7.46 % (2352099)Instructions burned: 865 (million)
% 49.42/7.46 % (2352130)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2824770234:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 82.29/12.09 % (2352102)Instruction limit reached!
% 82.29/12.09 % (2352102)------------------------------
% 82.29/12.09 % (2352102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352102)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352102)Termination reason: Instruction limit
% 82.29/12.09 % (2352102)Termination phase: Saturation
% 82.29/12.09 % (2352102)Time elapsed: 0.413 s
% 82.29/12.09 % (2352102)Peak memory usage: 24 MB
% 82.29/12.09 % (2352102)Instructions burned: 1179 (million)
% 82.29/12.09 % (2352155)fmb+10_1_sil=64000:random_seed=854008422:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 82.29/12.09 % TRYING [1]
% 82.29/12.09 % TRYING [2]
% 82.29/12.09 % TRYING [3]
% 82.29/12.09 % TRYING [4]
% 82.29/12.09 % TRYING [5]
% 82.29/12.09 % TRYING [6]
% 82.29/12.09 % (2352122)Instruction limit reached!
% 82.29/12.09 % (2352122)------------------------------
% 82.29/12.09 % (2352122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352122)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352122)Termination reason: Instruction limit
% 82.29/12.09 % (2352122)Termination phase: Finite model building constraint generation
% 82.29/12.09 % (2352122)Time elapsed: 0.409 s
% 82.29/12.09 % (2352122)Peak memory usage: 77 MB
% 82.29/12.09 % (2352122)Instructions burned: 889 (million)
% 82.29/12.09 % (2352161)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1201706409:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 82.29/12.09 % TRYING [20]
% 82.29/12.09 % TRYING [7]
% 82.29/12.09 % (2352124)Instruction limit reached!
% 82.29/12.09 % (2352124)------------------------------
% 82.29/12.09 % (2352124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352124)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352124)Termination reason: Instruction limit
% 82.29/12.09 % (2352124)Termination phase: Saturation
% 82.29/12.09 % (2352124)Time elapsed: 0.557 s
% 82.29/12.09 % (2352124)Peak memory usage: 19 MB
% 82.29/12.09 % (2352124)Instructions burned: 693 (million)
% 82.29/12.09 % (2352170)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=506299122:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 82.29/12.09 % TRYING [8]
% 82.29/12.09 % (2352130)Instruction limit reached!
% 82.29/12.09 % (2352130)------------------------------
% 82.29/12.09 % (2352130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352130)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352130)Termination reason: Instruction limit
% 82.29/12.09 % (2352130)Termination phase: Saturation
% 82.29/12.09 % (2352130)Time elapsed: 0.606 s
% 82.29/12.09 % (2352130)Peak memory usage: 18 MB
% 82.29/12.09 % (2352130)Instructions burned: 880 (million)
% 82.29/12.09 % (2352209)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2112394197:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 82.29/12.09 % TRYING [8]
% 82.29/12.09 % (2352170)Instruction limit reached!
% 82.29/12.09 % (2352170)------------------------------
% 82.29/12.09 % (2352170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352170)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352170)Termination reason: Instruction limit
% 82.29/12.09 % (2352170)Termination phase: Finite model building SAT solving
% 82.29/12.09 % (2352170)Time elapsed: 0.457 s
% 82.29/12.09 % (2352170)Peak memory usage: 50 MB
% 82.29/12.09 % (2352170)Instructions burned: 920 (million)
% 82.29/12.09 % (2352279)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1676988797:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 82.29/12.09 % TRYING [9]
% 82.29/12.09 % (2352279)Instruction limit reached!
% 82.29/12.09 % (2352279)------------------------------
% 82.29/12.09 % (2352279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.29/12.09 % (2352279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.29/12.09 % (2352279)CaDiCaL version: 2.1.3
% 82.29/12.09 % (2352279)Termination reason: Instruction limit
% 82.29/12.09 % (2352279)Termination phase: Saturation
% 82.29/12.09 % (2352279)Time elapsed: 0.802 s
% 82.29/12.09 % (2352279)Peak memory usage: 27 MB
% 82.29/12.09 % (2352279)Instructions burned: 1473 (million)
% 82.29/12.09 % (2352328)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=160011245:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 118.28/17.85 % TRYING [77]
% 118.28/17.85 % TRYING [9]
% 118.28/17.85 % TRYING [10]
% 118.28/17.85 % (2352209)Instruction limit reached!
% 118.28/17.85 % (2352209)------------------------------
% 118.28/17.85 % (2352209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352209)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352209)Termination reason: Instruction limit
% 118.28/17.85 % (2352209)Termination phase: Saturation
% 118.28/17.85 % (2352209)Time elapsed: 2.878 s
% 118.28/17.85 % (2352209)Peak memory usage: 56 MB
% 118.28/17.85 % (2352209)Instructions burned: 5133 (million)
% 118.28/17.85 % (2352330)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3898912380:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 118.28/17.85 % TRYING [16]
% 118.28/17.85 % (2352161)Instruction limit reached!
% 118.28/17.85 % (2352161)------------------------------
% 118.28/17.85 % (2352161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352161)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352161)Termination reason: Instruction limit
% 118.28/17.85 % (2352161)Termination phase: Finite model building constraint generation
% 118.28/17.85 % (2352161)Time elapsed: 3.471 s
% 118.28/17.85 % (2352161)Peak memory usage: 667 MB
% 118.28/17.85 % (2352161)Instructions burned: 9516 (million)
% 118.28/17.85 % (2352332)ott-2_1_sil=16000:newcnf=on:random_seed=2190786030:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 118.28/17.85 % (2352328)Instruction limit reached!
% 118.28/17.85 % (2352328)------------------------------
% 118.28/17.85 % (2352328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352328)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352328)Termination reason: Instruction limit
% 118.28/17.85 % (2352328)Termination phase: Finite model building constraint generation
% 118.28/17.85 % (2352328)Time elapsed: 2.388 s
% 118.28/17.85 % (2352328)Peak memory usage: 522 MB
% 118.28/17.85 % (2352328)Instructions burned: 6327 (million)
% 118.28/17.85 % (2352334)ott+10_1_sil=32000:tgt=ground:random_seed=3741310547:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 118.28/17.85 % (2352330)Instruction limit reached!
% 118.28/17.85 % (2352330)------------------------------
% 118.28/17.85 % (2352330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352330)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352330)Termination reason: Instruction limit
% 118.28/17.85 % (2352330)Termination phase: Finite model building constraint generation
% 118.28/17.85 % (2352330)Time elapsed: 0.735 s
% 118.28/17.85 % (2352330)Peak memory usage: 132 MB
% 118.28/17.85 % (2352330)Instructions burned: 2175 (million)
% 118.28/17.85 % (2352336)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1382116470:i=54282_2950 on theBenchmark for (2950ds/54282Mi)
% 118.28/17.85 % TRYING [1]
% 118.28/17.85 % TRYING [2]
% 118.28/17.85 % TRYING [3]
% 118.28/17.85 % TRYING [4]
% 118.28/17.85 % TRYING [5]
% 118.28/17.85 % (2352332)Instruction limit reached!
% 118.28/17.85 % (2352332)------------------------------
% 118.28/17.85 % (2352332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352332)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352332)Termination reason: Instruction limit
% 118.28/17.85 % (2352332)Termination phase: Saturation
% 118.28/17.85 % (2352332)Time elapsed: 0.549 s
% 118.28/17.85 % (2352332)Peak memory usage: 22 MB
% 118.28/17.85 % (2352332)Instructions burned: 870 (million)
% 118.28/17.85 % TRYING [6]
% 118.28/17.85 % (2352338)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=62264807:i=3512:aac=none_2949 on theBenchmark for (2949ds/3512Mi)
% 118.28/17.85 % TRYING [7]
% 118.28/17.85 % TRYING [8]
% 118.28/17.85 % (2352338)Instruction limit reached!
% 118.28/17.85 % (2352338)------------------------------
% 118.28/17.85 % (2352338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352338)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352338)Termination reason: Instruction limit
% 118.28/17.85 % (2352338)Termination phase: Saturation
% 118.28/17.85 % (2352338)Time elapsed: 2.0000 s
% 118.28/17.85 % (2352338)Peak memory usage: 41 MB
% 118.28/17.85 % (2352338)Instructions burned: 3512 (million)
% 118.28/17.85 % (2352340)dis+21_1_sil=32000:sas=cadical:random_seed=3822183034:i=3773:amm=off_2929 on theBenchmark for (2929ds/3773Mi)
% 118.28/17.85 % TRYING [9]
% 118.28/17.85 % (2352155)Instruction limit reached!
% 118.28/17.85 % (2352155)------------------------------
% 118.28/17.85 % (2352155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352155)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352155)Termination reason: Instruction limit
% 118.28/17.85 % (2352155)Termination phase: Finite model building SAT solving
% 118.28/17.85 % (2352155)Time elapsed: 7.360 s
% 118.28/17.85 % (2352155)Peak memory usage: 122 MB
% 118.28/17.85 % (2352155)Instructions burned: 22062 (million)
% 118.28/17.85 % (2352342)ott+11_1_sil=16000:gs=on:random_seed=3600318016:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2918 on theBenchmark for (2918ds/2251Mi)
% 118.28/17.85 % (2352334)Instruction limit reached!
% 118.28/17.85 % (2352334)------------------------------
% 118.28/17.85 % (2352334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352334)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352334)Termination reason: Instruction limit
% 118.28/17.85 % (2352334)Termination phase: Saturation
% 118.28/17.85 % (2352334)Time elapsed: 3.496 s
% 118.28/17.85 % (2352334)Peak memory usage: 71 MB
% 118.28/17.85 % (2352334)Instructions burned: 5115 (million)
% 118.28/17.85 % (2352344)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=85876593:fmbsr=1.6:i=67534_2916 on theBenchmark for (2916ds/67534Mi)
% 118.28/17.85 % TRYING [7]
% 118.28/17.85 % (2352342)Instruction limit reached!
% 118.28/17.85 % (2352342)------------------------------
% 118.28/17.85 % (2352342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352342)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352342)Termination reason: Instruction limit
% 118.28/17.85 % (2352342)Termination phase: Saturation
% 118.28/17.85 % (2352342)Time elapsed: 0.726 s
% 118.28/17.85 % (2352342)Peak memory usage: 33 MB
% 118.28/17.85 % (2352342)Instructions burned: 2254 (million)
% 118.28/17.85 % (2352346)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3523258782:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2911 on theBenchmark for (2911ds/4591Mi)
% 118.28/17.85 % TRYING [8]
% 118.28/17.85 % (2352340)Instruction limit reached!
% 118.28/17.85 % (2352340)------------------------------
% 118.28/17.85 % (2352340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352340)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352340)Termination reason: Instruction limit
% 118.28/17.85 % (2352340)Termination phase: Saturation
% 118.28/17.85 % (2352340)Time elapsed: 2.155 s
% 118.28/17.85 % (2352340)Peak memory usage: 42 MB
% 118.28/17.85 % (2352340)Instructions burned: 3774 (million)
% 118.28/17.85 % (2352348)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1089614571:i=29340_2907 on theBenchmark for (2907ds/29340Mi)
% 118.28/17.85 % (2352346)Instruction limit reached!
% 118.28/17.85 % (2352346)------------------------------
% 118.28/17.85 % (2352346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352346)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352346)Termination reason: Instruction limit
% 118.28/17.85 % (2352346)Termination phase: Saturation
% 118.28/17.85 % (2352346)Time elapsed: 1.193 s
% 118.28/17.85 % (2352346)Peak memory usage: 46 MB
% 118.28/17.85 % (2352346)Instructions burned: 4595 (million)
% 118.28/17.85 % (2352350)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=429734155:i=5211_2899 on theBenchmark for (2899ds/5211Mi)
% 118.28/17.85 % TRYING [9]
% 118.28/17.85 % (2352350)Instruction limit reached!
% 118.28/17.85 % (2352350)------------------------------
% 118.28/17.85 % (2352350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352350)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352350)Termination reason: Instruction limit
% 118.28/17.85 % (2352350)Termination phase: Saturation
% 118.28/17.85 % (2352350)Time elapsed: 1.596 s
% 118.28/17.85 % (2352350)Peak memory usage: 56 MB
% 118.28/17.85 % (2352350)Instructions burned: 5212 (million)
% 118.28/17.85 % (2352352)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1863180195:i=5497:nm=2_2883 on theBenchmark for (2883ds/5497Mi)
% 118.28/17.85 % TRYING [17]
% 118.28/17.85 % (2352352)Instruction limit reached!
% 118.28/17.85 % (2352352)------------------------------
% 118.28/17.85 % (2352352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352352)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352352)Termination reason: Instruction limit
% 118.28/17.85 % (2352352)Termination phase: Finite model building constraint generation
% 118.28/17.85 % (2352352)Time elapsed: 1.080 s
% 118.28/17.85 % (2352352)Peak memory usage: 391 MB
% 118.28/17.85 % (2352352)Instructions burned: 5497 (million)
% 118.28/17.85 % (2352354)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=832036343:fmbsr=2:i=46332_2872 on theBenchmark for (2872ds/46332Mi)
% 118.28/17.85 % TRYING [15]
% 118.28/17.85 % TRYING [10]
% 118.28/17.85 % (2352004) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2351995-2352004"...
% 118.28/17.85 % (2352004)...printing done.
% 118.28/17.85 % (2352004)Refutation found. Thanks to Tanya!
% 118.28/17.85 % SZS status Unsatisfiable for theBenchmark
% 118.28/17.85 % SZS output start Proof for theBenchmark
% See solution above
% 118.28/17.85 % (2352004)------------------------------
% 118.28/17.85 % (2352004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.28/17.85 % (2352004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.28/17.85 % (2352004)CaDiCaL version: 2.1.3
% 118.28/17.85 % (2352004)Termination reason: Refutation
% 118.28/17.85 % (2352004)Time elapsed: 17.243 s
% 118.28/17.85 % (2352004)Peak memory usage: 120 MB
% 118.28/17.85 % (2352004)Instructions burned: 51482 (million)
% 118.28/17.85 % (2351995)Success in time 17.424 s
% 118.28/17.85 % Vampire exiting
%------------------------------------------------------------------------------