%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP567-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:07 AM UTC 2026
% Result : Unsatisfiable 35.99s 5.66s
% Output : Refutation 35.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 13
% Syntax : Number of formulae : 272 ( 272 unt; 8 def)
% Number of atoms : 272 ( 271 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-2 aty)
% Number of variables : 444 ( 444 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(identity,identity)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
! [X0,X1] : multiply(X0,X1) = double_divide(double_divide(X1,X0),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiply) ).
fof(f3,axiom,
! [X0] : inverse(X0) = double_divide(X0,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
fof(f4,axiom,
! [X0] : identity = double_divide(X0,inverse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity) ).
fof(f5,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f6,plain,
! [X0] : identity = double_divide(X0,double_divide(X0,identity)),
inference(definition_unfolding,[],[f4,f3]) ).
fof(f7,plain,
double_divide(double_divide(c3,double_divide(double_divide(b3,a3),identity)),identity) != double_divide(double_divide(double_divide(double_divide(c3,b3),identity),a3),identity),
inference(definition_unfolding,[],[f5,f2,f2,f2,f2]) ).
fof(f8,definition,
sF0 = double_divide(b3,a3),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f9,plain,
double_divide(b3,a3) = sF0,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF1 = double_divide(sF0,identity),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f11,plain,
double_divide(sF0,identity) = sF1,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF2 = double_divide(c3,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f13,plain,
double_divide(c3,sF1) = sF2,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF3 = double_divide(sF2,identity),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f15,plain,
double_divide(sF2,identity) = sF3,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF4 = double_divide(c3,b3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f17,plain,
double_divide(c3,b3) = sF4,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF5 = double_divide(sF4,identity),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f19,plain,
double_divide(sF4,identity) = sF5,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF6 = double_divide(sF5,a3),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f21,plain,
double_divide(sF5,a3) = sF6,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF7 = double_divide(sF6,identity),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f23,plain,
double_divide(sF6,identity) = sF7,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF3 != sF7,
inference(definition_folding,[],[f7,f23,f21,f19,f17,f15,f13,f11,f9]) ).
fof(f28,plain,
identity = double_divide(sF6,sF7),
inference(superposition,[],[f6,f23]) ).
fof(f30,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,X2))),double_divide(double_divide(X3,X0),double_divide(identity,double_divide(identity,identity)))),double_divide(identity,identity)) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f31,plain,
! [X0] : double_divide(double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f9]) ).
fof(f37,plain,
! [X0] : double_divide(double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f19]) ).
fof(f38,plain,
! [X0] : double_divide(double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f21]) ).
fof(f39,plain,
! [X0] : double_divide(double_divide(sF6,double_divide(double_divide(X0,sF7),double_divide(identity,identity))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f23]) ).
fof(f40,plain,
! [X0] : double_divide(double_divide(X0,double_divide(identity,double_divide(identity,identity))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f6]) ).
fof(f41,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,X2))) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f1]) ).
fof(f42,plain,
! [X0,X1] : double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,double_divide(identity,identity))),identity)),double_divide(identity,identity)) = X1,
inference(superposition,[],[f1,f6]) ).
fof(f43,plain,
! [X0] : double_divide(double_divide(X0,identity),double_divide(identity,identity)) = X0,
inference(forward_demodulation,[],[f40,f6]) ).
fof(f44,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(double_divide(X1,double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(identity,X2))),double_divide(double_divide(X3,X0),identity)),double_divide(identity,identity)) = X3,
inference(forward_demodulation,[],[f30,f6]) ).
fof(f47,plain,
! [X0] : double_divide(double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f28]) ).
fof(f48,plain,
sF0 = double_divide(sF1,double_divide(identity,identity)),
inference(superposition,[],[f43,f11]) ).
fof(f49,plain,
sF2 = double_divide(sF3,double_divide(identity,identity)),
inference(superposition,[],[f43,f15]) ).
fof(f50,plain,
sF4 = double_divide(sF5,double_divide(identity,identity)),
inference(superposition,[],[f43,f19]) ).
fof(f51,plain,
sF6 = double_divide(sF7,double_divide(identity,identity)),
inference(superposition,[],[f43,f23]) ).
fof(f52,plain,
! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f43]) ).
fof(f53,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(X1,X0),double_divide(identity,double_divide(identity,identity)))),double_divide(identity,identity)) = X1,
inference(superposition,[],[f1,f43]) ).
fof(f54,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,identity),double_divide(double_divide(X1,X0),identity)),double_divide(identity,identity)) = X1,
inference(forward_demodulation,[],[f53,f6]) ).
fof(f103,plain,
! [X0] : double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f37]) ).
fof(f106,plain,
! [X0] : double_divide(X0,identity) = double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))),
inference(forward_demodulation,[],[f103,f52]) ).
fof(f206,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(identity,double_divide(identity,X2)))),
inference(superposition,[],[f41,f41]) ).
fof(f220,plain,
! [X0] : double_divide(identity,double_divide(X0,double_divide(identity,identity))) = double_divide(double_divide(identity,X0),double_divide(identity,identity)),
inference(superposition,[],[f41,f39]) ).
fof(f233,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,double_divide(identity,identity))),X0),
inference(superposition,[],[f41,f42]) ).
fof(f234,plain,
! [X0,X1] : double_divide(X0,double_divide(double_divide(identity,double_divide(X0,X1)),double_divide(identity,X1))) = double_divide(double_divide(identity,identity),double_divide(identity,identity)),
inference(superposition,[],[f41,f6]) ).
fof(f238,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,X0),double_divide(identity,identity)) = double_divide(X1,double_divide(double_divide(double_divide(X0,identity),double_divide(X1,X2)),double_divide(identity,X2))),
inference(superposition,[],[f41,f43]) ).
fof(f260,plain,
! [X2,X0,X1] : double_divide(X0,double_divide(double_divide(double_divide(X1,double_divide(identity,identity)),double_divide(X0,X2)),double_divide(identity,X2))) = X1,
inference(superposition,[],[f1,f41]) ).
fof(f262,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(identity,double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f1,f41]) ).
fof(f265,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity),
inference(forward_demodulation,[],[f262,f52]) ).
fof(f282,plain,
! [X0,X1] : identity = double_divide(X0,double_divide(double_divide(identity,double_divide(X0,X1)),double_divide(identity,X1))),
inference(forward_demodulation,[],[f234,f43]) ).
fof(f283,plain,
! [X0,X1] : double_divide(X1,identity) = double_divide(double_divide(X0,double_divide(X1,double_divide(identity,identity))),X0),
inference(forward_demodulation,[],[f233,f52]) ).
fof(f292,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,X2)))),
inference(forward_demodulation,[],[f206,f52]) ).
fof(f324,plain,
! [X2,X0,X1] : double_divide(X1,identity) = double_divide(double_divide(X0,double_divide(X1,X2)),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,X2)))),
inference(forward_demodulation,[],[f292,f52]) ).
fof(f442,plain,
! [X2,X3,X0,X1,X4] : double_divide(X3,double_divide(double_divide(X0,double_divide(X3,X4)),double_divide(identity,X4))) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(double_divide(identity,identity),double_divide(X1,X2)),double_divide(identity,X2))),double_divide(X0,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f1]) ).
fof(f445,plain,
! [X2,X0,X1] : double_divide(X0,identity) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(double_divide(identity,identity),double_divide(X1,X2)),double_divide(identity,X2))),double_divide(X0,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f43]) ).
fof(f447,plain,
! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(double_divide(X3,double_divide(double_divide(double_divide(identity,identity),double_divide(X3,X4)),double_divide(identity,X4))),double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f41]) ).
fof(f448,plain,
! [X2,X0,X1] : double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(double_divide(identity,identity),double_divide(X1,X2)),double_divide(identity,X2))),double_divide(X0,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f31]) ).
fof(f454,plain,
! [X2,X0,X1] : double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(double_divide(identity,identity),double_divide(X1,X2)),double_divide(identity,X2))),double_divide(X0,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f37]) ).
fof(f455,plain,
! [X2,X0,X1] : double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(double_divide(identity,identity),double_divide(X1,X2)),double_divide(identity,X2))),double_divide(X0,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f38]) ).
fof(f460,plain,
! [X0,X1] : c3 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(b3,double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF4,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f17]) ).
fof(f463,plain,
! [X0,X1] : sF0 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(identity,double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF1,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f11]) ).
fof(f472,plain,
! [X0,X1] : sF3 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF2,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f49]) ).
fof(f476,plain,
! [X0,X1] : sF5 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF4,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f50]) ).
fof(f477,plain,
! [X0,X1] : sF6 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(identity,double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF7,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f23]) ).
fof(f479,plain,
! [X0,X1] : sF7 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),double_divide(sF6,identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f51]) ).
fof(f480,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,X1),X0) = double_divide(double_divide(identity,double_divide(double_divide(X2,double_divide(double_divide(X1,double_divide(X2,X3)),double_divide(identity,X3))),double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f41,f44]) ).
fof(f493,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X0,X1),X0) = double_divide(double_divide(X2,double_divide(double_divide(X1,double_divide(X2,X3)),double_divide(identity,X3))),identity),
inference(forward_demodulation,[],[f480,f52]) ).
fof(f494,plain,
! [X0,X1] : sF7 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),sF7),double_divide(identity,identity)),
inference(forward_demodulation,[],[f479,f23]) ).
fof(f496,plain,
sF6 = double_divide(double_divide(identity,double_divide(sF7,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f477,f282]) ).
fof(f497,plain,
! [X0,X1] : sF5 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),sF5),double_divide(identity,identity)),
inference(forward_demodulation,[],[f476,f19]) ).
fof(f501,plain,
! [X0,X1] : sF3 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(identity,identity),double_divide(X0,X1)),double_divide(identity,X1))),sF3),double_divide(identity,identity)),
inference(forward_demodulation,[],[f472,f15]) ).
fof(f510,plain,
sF0 = double_divide(double_divide(identity,double_divide(sF1,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f463,f282]) ).
fof(f511,plain,
! [X0,X1] : c3 = double_divide(double_divide(double_divide(X0,double_divide(double_divide(b3,double_divide(X0,X1)),double_divide(identity,X1))),sF5),double_divide(identity,identity)),
inference(forward_demodulation,[],[f460,f19]) ).
fof(f515,plain,
! [X0] : double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f455,f238]) ).
fof(f516,plain,
! [X0] : double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f454,f238]) ).
fof(f522,plain,
! [X0] : double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f448,f238]) ).
fof(f523,plain,
! [X3,X1,X4] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(double_divide(X3,double_divide(double_divide(double_divide(identity,identity),double_divide(X3,X4)),double_divide(identity,X4))),double_divide(identity,double_divide(X1,double_divide(identity,identity)))),double_divide(identity,identity)),
inference(forward_demodulation,[],[f447,f265]) ).
fof(f525,plain,
! [X0] : double_divide(X0,identity) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f445,f238]) ).
fof(f528,plain,
! [X3,X0,X4] : double_divide(X3,double_divide(double_divide(X0,double_divide(X3,X4)),double_divide(identity,X4))) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f442,f238]) ).
fof(f585,plain,
sF7 = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),sF7),double_divide(identity,identity)),
inference(forward_demodulation,[],[f494,f238]) ).
fof(f586,plain,
sF6 = double_divide(identity,double_divide(double_divide(sF7,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f496,f220]) ).
fof(f587,plain,
sF5 = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),sF5),double_divide(identity,identity)),
inference(forward_demodulation,[],[f497,f238]) ).
fof(f589,plain,
sF3 = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),sF3),double_divide(identity,identity)),
inference(forward_demodulation,[],[f501,f238]) ).
fof(f593,plain,
sF0 = double_divide(identity,double_divide(double_divide(sF1,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f510,f220]) ).
fof(f596,plain,
! [X0] : double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f515,f43]) ).
fof(f597,plain,
! [X0] : double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f516,f43]) ).
fof(f603,plain,
! [X0] : double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f522,f43]) ).
fof(f604,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(double_divide(double_divide(identity,identity),double_divide(identity,identity)),double_divide(identity,double_divide(X1,double_divide(identity,identity)))),double_divide(identity,identity)),
inference(forward_demodulation,[],[f523,f238]) ).
fof(f606,plain,
! [X0] : double_divide(X0,identity) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f525,f43]) ).
fof(f609,plain,
! [X3,X0,X4] : double_divide(X3,double_divide(double_divide(X0,double_divide(X3,X4)),double_divide(identity,X4))) = double_divide(double_divide(identity,double_divide(X0,identity)),double_divide(identity,identity)),
inference(forward_demodulation,[],[f528,f43]) ).
fof(f637,plain,
sF7 = double_divide(double_divide(identity,sF7),double_divide(identity,identity)),
inference(forward_demodulation,[],[f585,f43]) ).
fof(f638,plain,
sF6 = double_divide(identity,sF7),
inference(forward_demodulation,[],[f586,f43]) ).
fof(f639,plain,
sF5 = double_divide(double_divide(identity,sF5),double_divide(identity,identity)),
inference(forward_demodulation,[],[f587,f43]) ).
fof(f641,plain,
sF3 = double_divide(double_divide(identity,sF3),double_divide(identity,identity)),
inference(forward_demodulation,[],[f589,f43]) ).
fof(f645,plain,
sF0 = double_divide(identity,sF1),
inference(forward_demodulation,[],[f593,f43]) ).
fof(f648,plain,
! [X0] : double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f596,f220]) ).
fof(f649,plain,
! [X0] : double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f597,f220]) ).
fof(f655,plain,
! [X0] : double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f603,f220]) ).
fof(f656,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(double_divide(identity,double_divide(identity,double_divide(X1,double_divide(identity,identity)))),double_divide(identity,identity)),
inference(forward_demodulation,[],[f604,f43]) ).
fof(f658,plain,
! [X0] : double_divide(X0,identity) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,identity))),
inference(forward_demodulation,[],[f606,f220]) ).
fof(f661,plain,
! [X3,X0,X4] : double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,identity))) = double_divide(X3,double_divide(double_divide(X0,double_divide(X3,X4)),double_divide(identity,X4))),
inference(forward_demodulation,[],[f609,f220]) ).
fof(f674,plain,
sF7 = double_divide(identity,double_divide(sF7,double_divide(identity,identity))),
inference(forward_demodulation,[],[f637,f220]) ).
fof(f675,plain,
sF5 = double_divide(identity,double_divide(sF5,double_divide(identity,identity))),
inference(forward_demodulation,[],[f639,f220]) ).
fof(f676,plain,
sF3 = double_divide(identity,double_divide(sF3,double_divide(identity,identity))),
inference(forward_demodulation,[],[f641,f220]) ).
fof(f679,plain,
! [X0] : double_divide(identity,X0) = double_divide(sF5,double_divide(double_divide(X0,sF6),double_divide(identity,a3))),
inference(forward_demodulation,[],[f648,f43]) ).
fof(f680,plain,
! [X0] : double_divide(identity,X0) = double_divide(sF4,double_divide(double_divide(X0,sF5),double_divide(identity,identity))),
inference(forward_demodulation,[],[f649,f43]) ).
fof(f686,plain,
! [X0] : double_divide(identity,X0) = double_divide(b3,double_divide(double_divide(X0,sF0),double_divide(identity,a3))),
inference(forward_demodulation,[],[f655,f43]) ).
fof(f687,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(identity,double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity))),
inference(forward_demodulation,[],[f656,f220]) ).
fof(f689,plain,
! [X0] : double_divide(X0,identity) = double_divide(identity,X0),
inference(forward_demodulation,[],[f658,f43]) ).
fof(f692,plain,
! [X3,X0,X4] : double_divide(identity,X0) = double_divide(X3,double_divide(double_divide(X0,double_divide(X3,X4)),double_divide(identity,X4))),
inference(forward_demodulation,[],[f661,f43]) ).
fof(f693,plain,
sF7 = double_divide(identity,sF6),
inference(forward_demodulation,[],[f674,f51]) ).
fof(f694,plain,
sF5 = double_divide(identity,sF4),
inference(forward_demodulation,[],[f675,f50]) ).
fof(f695,plain,
sF3 = double_divide(identity,sF2),
inference(forward_demodulation,[],[f676,f49]) ).
fof(f698,plain,
! [X1] : double_divide(identity,double_divide(X1,double_divide(identity,identity))) = double_divide(identity,double_divide(X1,identity)),
inference(forward_demodulation,[],[f687,f52]) ).
fof(f808,plain,
! [X0] : identity = double_divide(X0,double_divide(identity,X0)),
inference(superposition,[],[f6,f689]) ).
fof(f826,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X1,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(identity,double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity))),
inference(superposition,[],[f41,f689]) ).
fof(f827,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity))),double_divide(identity,identity)) = X1,
inference(superposition,[],[f1,f689]) ).
fof(f828,plain,
! [X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity)),double_divide(identity,identity))) = X1,
inference(forward_demodulation,[],[f827,f220]) ).
fof(f829,plain,
! [X0,X1] : double_divide(X1,identity) = double_divide(identity,double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity))),
inference(forward_demodulation,[],[f826,f52]) ).
fof(f840,plain,
! [X0,X1] : double_divide(identity,double_divide(double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity)),identity)) = X1,
inference(forward_demodulation,[],[f828,f698]) ).
fof(f846,plain,
! [X0,X1] : double_divide(identity,double_divide(identity,double_divide(double_divide(X1,double_divide(X0,identity)),double_divide(X0,identity)))) = X1,
inference(forward_demodulation,[],[f840,f689]) ).
fof(f847,plain,
! [X1] : double_divide(identity,double_divide(X1,identity)) = X1,
inference(forward_demodulation,[],[f846,f829]) ).
fof(f913,plain,
! [X0] : double_divide(double_divide(identity,double_divide(sF4,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,sF5),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,identity)))),
inference(superposition,[],[f41,f106]) ).
fof(f924,plain,
! [X0] : double_divide(double_divide(identity,double_divide(sF4,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,sF5),double_divide(double_divide(X0,identity),identity)),
inference(forward_demodulation,[],[f913,f6]) ).
fof(f932,plain,
! [X0] : double_divide(double_divide(identity,double_divide(sF4,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,sF5),double_divide(identity,double_divide(X0,identity))),
inference(forward_demodulation,[],[f924,f689]) ).
fof(f939,plain,
! [X0] : double_divide(double_divide(identity,double_divide(sF4,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(double_divide(X0,sF5),X0),
inference(forward_demodulation,[],[f932,f847]) ).
fof(f943,plain,
! [X0] : double_divide(sF4,identity) = double_divide(double_divide(X0,sF5),X0),
inference(forward_demodulation,[],[f939,f52]) ).
fof(f946,plain,
! [X0] : double_divide(identity,sF4) = double_divide(double_divide(X0,sF5),X0),
inference(forward_demodulation,[],[f943,f689]) ).
fof(f947,plain,
! [X0] : sF5 = double_divide(double_divide(X0,sF5),X0),
inference(forward_demodulation,[],[f946,f694]) ).
fof(f1001,plain,
! [X0] : double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)) = double_divide(identity,double_divide(identity,double_divide(identity,X0))),
inference(superposition,[],[f41,f808]) ).
fof(f1002,plain,
! [X0] : double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X0))),double_divide(identity,identity)) = X0,
inference(superposition,[],[f1,f808]) ).
fof(f1017,plain,
! [X0] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X0)),double_divide(identity,identity))) = X0,
inference(forward_demodulation,[],[f1002,f220]) ).
fof(f1018,plain,
! [X0] : double_divide(X0,identity) = double_divide(identity,double_divide(identity,double_divide(identity,X0))),
inference(forward_demodulation,[],[f1001,f52]) ).
fof(f1025,plain,
! [X0] : double_divide(identity,double_divide(double_divide(identity,double_divide(identity,X0)),identity)) = X0,
inference(forward_demodulation,[],[f1017,f698]) ).
fof(f1027,plain,
! [X0] : double_divide(identity,double_divide(identity,X0)) = X0,
inference(forward_demodulation,[],[f1025,f847]) ).
fof(f1249,plain,
identity = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f41,f282]) ).
fof(f1276,plain,
identity = double_divide(identity,identity),
inference(forward_demodulation,[],[f1249,f52]) ).
fof(f1575,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),identity) = double_divide(double_divide(X1,X0),X1),
inference(superposition,[],[f283,f43]) ).
fof(f1589,plain,
! [X0] : double_divide(sF1,identity) = double_divide(double_divide(X0,sF0),X0),
inference(superposition,[],[f283,f48]) ).
fof(f1592,plain,
! [X0] : double_divide(sF7,identity) = double_divide(double_divide(X0,sF6),X0),
inference(superposition,[],[f283,f51]) ).
fof(f1593,plain,
! [X0,X1] : double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),X1) = double_divide(double_divide(X0,double_divide(X1,identity)),identity),
inference(superposition,[],[f283,f41]) ).
fof(f1608,plain,
! [X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(double_divide(double_divide(X1,X0),identity),identity)),identity),double_divide(identity,identity)) = X1,
inference(superposition,[],[f44,f283]) ).
fof(f1612,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X0,double_divide(identity,identity))) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(double_divide(X0,identity),identity)),double_divide(identity,identity)),
inference(superposition,[],[f44,f283]) ).
fof(f1617,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(double_divide(identity,double_divide(double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f41,f283]) ).
fof(f1618,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,identity))) = double_divide(double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))),double_divide(identity,identity)),
inference(superposition,[],[f1,f283]) ).
fof(f1619,plain,
! [X0,X1] : double_divide(double_divide(X1,double_divide(identity,identity)),double_divide(X0,double_divide(identity,identity))) = double_divide(double_divide(X1,double_divide(double_divide(X0,identity),identity)),double_divide(identity,identity)),
inference(superposition,[],[f42,f283]) ).
fof(f1669,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(double_divide(X1,double_divide(double_divide(X0,identity),identity)),identity),
inference(forward_demodulation,[],[f1619,f1276]) ).
fof(f1670,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),double_divide(X0,identity)) = double_divide(double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))),identity),
inference(forward_demodulation,[],[f1618,f1276]) ).
fof(f1671,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,identity))),identity),
inference(forward_demodulation,[],[f1617,f52]) ).
fof(f1676,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X0,identity)) = double_divide(double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(double_divide(X0,identity),identity)),identity),
inference(forward_demodulation,[],[f1612,f1276]) ).
fof(f1680,plain,
! [X0,X1] : double_divide(X0,double_divide(double_divide(double_divide(X1,X0),identity),identity)) = X1,
inference(forward_demodulation,[],[f1608,f43]) ).
fof(f1694,plain,
! [X0,X1] : double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),X1) = double_divide(identity,double_divide(X0,double_divide(X1,identity))),
inference(forward_demodulation,[],[f1593,f689]) ).
fof(f1695,plain,
! [X0] : double_divide(identity,sF7) = double_divide(double_divide(X0,sF6),X0),
inference(forward_demodulation,[],[f1592,f689]) ).
fof(f1698,plain,
! [X0] : double_divide(identity,sF1) = double_divide(double_divide(X0,sF0),X0),
inference(forward_demodulation,[],[f1589,f689]) ).
fof(f1712,plain,
! [X0,X1] : double_divide(identity,double_divide(X0,identity)) = double_divide(double_divide(X1,X0),X1),
inference(forward_demodulation,[],[f1575,f689]) ).
fof(f1738,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(identity,double_divide(X1,double_divide(double_divide(X0,identity),identity))),
inference(forward_demodulation,[],[f1669,f689]) ).
fof(f1739,plain,
! [X2,X0,X1] : double_divide(double_divide(X1,X2),double_divide(X0,identity)) = double_divide(identity,double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2)))),
inference(forward_demodulation,[],[f1670,f689]) ).
fof(f1740,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(identity,double_divide(double_divide(X1,X2),double_divide(X0,double_divide(identity,identity)))),
inference(forward_demodulation,[],[f1671,f689]) ).
fof(f1745,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(double_divide(X0,identity),identity))),
inference(forward_demodulation,[],[f1676,f689]) ).
fof(f1749,plain,
! [X0,X1] : double_divide(X0,double_divide(identity,double_divide(double_divide(X1,X0),identity))) = X1,
inference(forward_demodulation,[],[f1680,f689]) ).
fof(f1755,plain,
! [X0,X1] : double_divide(double_divide(X0,identity),X1) = double_divide(identity,double_divide(X0,double_divide(X1,identity))),
inference(forward_demodulation,[],[f1694,f52]) ).
fof(f1756,plain,
! [X0] : sF6 = double_divide(double_divide(X0,sF6),X0),
inference(forward_demodulation,[],[f1695,f638]) ).
fof(f1759,plain,
! [X0] : sF0 = double_divide(double_divide(X0,sF0),X0),
inference(forward_demodulation,[],[f1698,f645]) ).
fof(f1773,plain,
! [X0,X1] : double_divide(double_divide(X1,X0),X1) = X0,
inference(forward_demodulation,[],[f1712,f847]) ).
fof(f1788,plain,
! [X0,X1] : double_divide(double_divide(X1,identity),double_divide(X0,identity)) = double_divide(identity,double_divide(X1,double_divide(identity,double_divide(X0,identity)))),
inference(forward_demodulation,[],[f1738,f689]) ).
fof(f1789,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(identity,double_divide(double_divide(X1,X2),double_divide(X0,identity))),
inference(forward_demodulation,[],[f1740,f1276]) ).
fof(f1793,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),double_divide(identity,double_divide(X0,identity)))),
inference(forward_demodulation,[],[f1745,f689]) ).
fof(f1796,plain,
! [X0,X1] : double_divide(X0,double_divide(X1,X0)) = X1,
inference(forward_demodulation,[],[f1749,f847]) ).
fof(f1826,plain,
! [X0,X1] : double_divide(identity,double_divide(X1,X0)) = double_divide(double_divide(X1,identity),double_divide(X0,identity)),
inference(forward_demodulation,[],[f1788,f847]) ).
fof(f1827,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(double_divide(double_divide(X1,X2),identity),X0),
inference(forward_demodulation,[],[f1789,f1755]) ).
fof(f1829,plain,
! [X2,X3,X0,X1] : double_divide(X2,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(X1,double_divide(double_divide(X2,double_divide(X1,X3)),double_divide(identity,X3))),X0)),
inference(forward_demodulation,[],[f1793,f847]) ).
fof(f1840,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(double_divide(X0,identity),double_divide(identity,X2))) = double_divide(double_divide(identity,double_divide(X1,X2)),X0),
inference(forward_demodulation,[],[f1827,f689]) ).
fof(f1842,plain,
! [X2,X0] : double_divide(X2,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(identity,X2),X0)),
inference(forward_demodulation,[],[f1829,f692]) ).
fof(f2554,plain,
! [X0,X1] : double_divide(X0,double_divide(sF5,double_divide(identity,X1))) = double_divide(double_divide(identity,double_divide(double_divide(double_divide(X0,X1),sF5),double_divide(identity,identity))),double_divide(identity,identity)),
inference(superposition,[],[f41,f947]) ).
fof(f2617,plain,
! [X0,X1] : double_divide(X0,double_divide(sF5,double_divide(identity,X1))) = double_divide(double_divide(double_divide(X0,X1),sF5),identity),
inference(forward_demodulation,[],[f2554,f52]) ).
fof(f2650,plain,
! [X0,X1] : double_divide(X0,double_divide(sF5,double_divide(identity,X1))) = double_divide(identity,double_divide(double_divide(X0,X1),sF5)),
inference(forward_demodulation,[],[f2617,f689]) ).
fof(f3277,plain,
double_divide(identity,double_divide(identity,a3)) = double_divide(sF5,sF6),
inference(superposition,[],[f679,f1756]) ).
fof(f3371,plain,
a3 = double_divide(sF5,sF6),
inference(forward_demodulation,[],[f3277,f1027]) ).
fof(f3508,plain,
sF6 = double_divide(a3,sF5),
inference(superposition,[],[f1756,f3371]) ).
fof(f4833,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,double_divide(identity,identity))) = double_divide(double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),identity)),double_divide(identity,identity)),
inference(superposition,[],[f54,f283]) ).
fof(f5001,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),identity)),identity),
inference(forward_demodulation,[],[f4833,f1276]) ).
fof(f5111,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),identity))),
inference(forward_demodulation,[],[f5001,f689]) ).
fof(f5207,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(double_divide(double_divide(X1,identity),identity),double_divide(X0,identity)),
inference(forward_demodulation,[],[f5111,f1755]) ).
fof(f5299,plain,
! [X0,X1] : double_divide(X1,double_divide(X0,identity)) = double_divide(identity,double_divide(double_divide(X1,identity),X0)),
inference(forward_demodulation,[],[f5207,f1826]) ).
fof(f9806,plain,
double_divide(identity,double_divide(identity,a3)) = double_divide(b3,sF0),
inference(superposition,[],[f686,f1759]) ).
fof(f9945,plain,
a3 = double_divide(b3,sF0),
inference(forward_demodulation,[],[f9806,f1027]) ).
fof(f10759,plain,
! [X0,X1] : double_divide(double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7))),identity) = double_divide(double_divide(X1,X0),double_divide(double_divide(X1,identity),double_divide(identity,double_divide(identity,double_divide(identity,identity))))),
inference(superposition,[],[f324,f47]) ).
fof(f10840,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),identity) = double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(double_divide(X1,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2))))),
inference(superposition,[],[f324,f41]) ).
fof(f10841,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X0,X1)),identity) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,double_divide(identity,X1))))),
inference(superposition,[],[f324,f282]) ).
fof(f10842,plain,
! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(identity,identity)),double_divide(X1,X2)),identity) = double_divide(X0,double_divide(double_divide(X1,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2))))),
inference(superposition,[],[f324,f260]) ).
fof(f10951,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(X0,X2))) = double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2))))),
inference(superposition,[],[f692,f324]) ).
fof(f10954,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2))))),double_divide(identity,identity)),
inference(superposition,[],[f1,f324]) ).
fof(f10973,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2))))),identity),
inference(forward_demodulation,[],[f10954,f1276]) ).
fof(f10976,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(X0,X2))) = double_divide(double_divide(identity,double_divide(double_divide(X1,identity),double_divide(identity,double_divide(identity,X2)))),X0),
inference(forward_demodulation,[],[f10951,f1840]) ).
fof(f11084,plain,
! [X2,X0,X1] : double_divide(double_divide(double_divide(X0,double_divide(identity,identity)),double_divide(X1,X2)),identity) = double_divide(double_divide(identity,double_divide(X0,double_divide(identity,double_divide(identity,X2)))),X1),
inference(forward_demodulation,[],[f10842,f1840]) ).
fof(f11085,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X0,X1)),identity) = double_divide(double_divide(identity,double_divide(identity,double_divide(identity,double_divide(identity,X1)))),X0),
inference(forward_demodulation,[],[f10841,f1840]) ).
fof(f11086,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),identity) = double_divide(double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),double_divide(identity,double_divide(identity,X2)))),X1),
inference(forward_demodulation,[],[f10840,f1840]) ).
fof(f11162,plain,
! [X0,X1] : double_divide(double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7))),identity) = double_divide(double_divide(identity,double_divide(double_divide(X1,X0),double_divide(identity,double_divide(identity,identity)))),X1),
inference(forward_demodulation,[],[f10759,f1840]) ).
fof(f11210,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(identity,double_divide(double_divide(X1,identity),double_divide(double_divide(X0,identity),double_divide(identity,double_divide(identity,double_divide(identity,X2)))))),
inference(forward_demodulation,[],[f10973,f689]) ).
fof(f11213,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(X0,X2))) = double_divide(double_divide(double_divide(identity,double_divide(identity,double_divide(identity,X2))),X1),X0),
inference(forward_demodulation,[],[f10976,f1840]) ).
fof(f11300,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,X2)),X1) = double_divide(double_divide(double_divide(X0,double_divide(identity,identity)),double_divide(X1,X2)),identity),
inference(forward_demodulation,[],[f11084,f1027]) ).
fof(f11301,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X0,X1)),identity) = double_divide(double_divide(double_divide(identity,X1),identity),X0),
inference(forward_demodulation,[],[f11085,f1018]) ).
fof(f11302,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),identity) = double_divide(double_divide(identity,double_divide(double_divide(double_divide(identity,double_divide(X0,double_divide(identity,identity))),double_divide(identity,identity)),X2)),X1),
inference(forward_demodulation,[],[f11086,f1027]) ).
fof(f11378,plain,
! [X0,X1] : double_divide(double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7))),identity) = double_divide(double_divide(identity,double_divide(double_divide(X1,X0),identity)),X1),
inference(forward_demodulation,[],[f11162,f6]) ).
fof(f11424,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(double_divide(double_divide(X1,identity),double_divide(identity,double_divide(identity,X2))),double_divide(X0,identity)),
inference(forward_demodulation,[],[f11210,f1739]) ).
fof(f11427,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X1,double_divide(X0,X2))) = double_divide(double_divide(double_divide(X2,identity),X1),X0),
inference(forward_demodulation,[],[f11213,f1018]) ).
fof(f11497,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,X2)),X1) = double_divide(identity,double_divide(double_divide(X0,double_divide(identity,identity)),double_divide(X1,X2))),
inference(forward_demodulation,[],[f11300,f689]) ).
fof(f11498,plain,
! [X0,X1] : double_divide(double_divide(identity,double_divide(X0,X1)),identity) = double_divide(double_divide(identity,double_divide(identity,X1)),X0),
inference(forward_demodulation,[],[f11301,f689]) ).
fof(f11499,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),identity) = double_divide(double_divide(identity,double_divide(double_divide(X0,identity),X2)),X1),
inference(forward_demodulation,[],[f11302,f52]) ).
fof(f11553,plain,
! [X0,X1] : double_divide(double_divide(X1,X0),X1) = double_divide(double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7))),identity),
inference(forward_demodulation,[],[f11378,f1796]) ).
fof(f11596,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(double_divide(double_divide(X1,identity),X2),double_divide(X0,identity)),
inference(forward_demodulation,[],[f11424,f1027]) ).
fof(f11660,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,X2)),X1) = double_divide(identity,double_divide(double_divide(X0,identity),double_divide(X1,X2))),
inference(forward_demodulation,[],[f11497,f1276]) ).
fof(f11661,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(double_divide(identity,double_divide(X0,X1)),identity),
inference(forward_demodulation,[],[f11498,f1027]) ).
fof(f11662,plain,
! [X2,X0,X1] : double_divide(double_divide(X0,double_divide(X1,X2)),identity) = double_divide(double_divide(X0,double_divide(X2,identity)),X1),
inference(forward_demodulation,[],[f11499,f5299]) ).
fof(f11697,plain,
! [X0,X1] : double_divide(double_divide(X1,X0),X1) = double_divide(identity,double_divide(sF6,double_divide(double_divide(X0,identity),double_divide(identity,sF7)))),
inference(forward_demodulation,[],[f11553,f689]) ).
fof(f11733,plain,
! [X2,X0,X1] : double_divide(X1,double_divide(X0,X2)) = double_divide(identity,double_divide(X2,double_divide(double_divide(X0,identity),X1))),
inference(forward_demodulation,[],[f11596,f11427]) ).
fof(f11775,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,X2)),X1) = double_divide(X0,double_divide(double_divide(X1,X2),identity)),
inference(forward_demodulation,[],[f11660,f5299]) ).
fof(f11776,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(identity,double_divide(identity,double_divide(X0,X1))),
inference(forward_demodulation,[],[f11661,f689]) ).
fof(f11777,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(X0,double_divide(X1,X2))) = double_divide(double_divide(X0,double_divide(X2,identity)),X1),
inference(forward_demodulation,[],[f11662,f689]) ).
fof(f11800,plain,
! [X0,X1] : double_divide(double_divide(X1,X0),X1) = double_divide(double_divide(sF6,sF7),double_divide(X0,identity)),
inference(forward_demodulation,[],[f11697,f1739]) ).
fof(f11849,plain,
! [X2,X0,X1] : double_divide(double_divide(identity,double_divide(X0,X2)),X1) = double_divide(X0,double_divide(identity,double_divide(X1,X2))),
inference(forward_demodulation,[],[f11775,f689]) ).
fof(f11850,plain,
! [X0,X1] : double_divide(X1,X0) = double_divide(X0,X1),
inference(forward_demodulation,[],[f11776,f1027]) ).
fof(f11853,plain,
! [X0,X1] : double_divide(identity,double_divide(X0,identity)) = double_divide(double_divide(X1,X0),X1),
inference(forward_demodulation,[],[f11800,f28]) ).
fof(f11890,plain,
! [X0,X1] : double_divide(identity,double_divide(X0,identity)) = double_divide(X1,double_divide(X1,X0)),
inference(forward_demodulation,[],[f11853,f11850]) ).
fof(f11911,plain,
! [X0,X1] : double_divide(X1,double_divide(X1,X0)) = X0,
inference(forward_demodulation,[],[f11890,f1796]) ).
fof(f12286,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X3,X1),identity) = double_divide(double_divide(X4,double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity)),double_divide(double_divide(X4,identity),double_divide(identity,double_divide(identity,X3)))),
inference(superposition,[],[f324,f493]) ).
fof(f12290,plain,
! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(double_divide(X3,X4),X1)) = double_divide(X3,double_divide(double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity),double_divide(identity,X4))),
inference(superposition,[],[f692,f493]) ).
fof(f12385,plain,
! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(double_divide(X3,X4),X1)) = double_divide(double_divide(identity,double_divide(X3,X4)),double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2)))),
inference(forward_demodulation,[],[f12290,f1840]) ).
fof(f12389,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X3,X1),identity) = double_divide(double_divide(identity,double_divide(double_divide(X4,double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity)),double_divide(identity,X3))),X4),
inference(forward_demodulation,[],[f12286,f1840]) ).
fof(f12746,plain,
! [X2,X3,X0,X1,X4] : double_divide(identity,double_divide(double_divide(X3,X4),X1)) = double_divide(X3,double_divide(identity,double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),X4))),
inference(forward_demodulation,[],[f12385,f11849]) ).
fof(f12750,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X3,X1),identity) = double_divide(X4,double_divide(identity,double_divide(double_divide(X4,double_divide(double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2))),identity)),double_divide(identity,X3)))),
inference(forward_demodulation,[],[f12389,f11850]) ).
fof(f13105,plain,
! [X3,X1,X4] : double_divide(identity,double_divide(double_divide(X3,X4),X1)) = double_divide(X3,double_divide(identity,double_divide(double_divide(identity,X1),X4))),
inference(forward_demodulation,[],[f12746,f692]) ).
fof(f13108,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X3,X1),identity) = double_divide(X4,double_divide(identity,double_divide(identity,double_divide(X4,double_divide(double_divide(identity,X3),double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2)))))))),
inference(forward_demodulation,[],[f12750,f11777]) ).
fof(f13427,plain,
! [X3,X1,X4] : double_divide(identity,double_divide(double_divide(X3,X4),X1)) = double_divide(X3,double_divide(X1,double_divide(X4,identity))),
inference(forward_demodulation,[],[f13105,f1842]) ).
fof(f13430,plain,
! [X2,X3,X0,X1,X4] : double_divide(double_divide(X3,X1),identity) = double_divide(X4,double_divide(X4,double_divide(double_divide(identity,X3),double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2)))))),
inference(forward_demodulation,[],[f13108,f11911]) ).
fof(f13717,plain,
! [X2,X3,X0,X1] : double_divide(double_divide(X3,X1),identity) = double_divide(double_divide(identity,X3),double_divide(X0,double_divide(double_divide(X1,double_divide(X0,X2)),double_divide(identity,X2)))),
inference(forward_demodulation,[],[f13430,f11911]) ).
fof(f13919,plain,
! [X3,X1] : double_divide(double_divide(X3,X1),identity) = double_divide(double_divide(identity,X3),double_divide(identity,X1)),
inference(forward_demodulation,[],[f13717,f692]) ).
fof(f14062,plain,
! [X3,X1] : double_divide(identity,double_divide(X3,X1)) = double_divide(double_divide(identity,X3),double_divide(identity,X1)),
inference(forward_demodulation,[],[f13919,f689]) ).
fof(f16706,plain,
! [X0] : double_divide(double_divide(X0,sF5),double_divide(identity,identity)) = double_divide(double_divide(X0,identity),sF4),
inference(superposition,[],[f1773,f106]) ).
fof(f16813,plain,
! [X2,X0,X1] : double_divide(identity,double_divide(double_divide(X1,X2),X0)) = double_divide(X1,double_divide(X0,double_divide(identity,X2))),
inference(superposition,[],[f692,f1773]) ).
fof(f16871,plain,
! [X0] : double_divide(sF4,double_divide(X0,double_divide(identity,identity))) = double_divide(identity,double_divide(sF5,X0)),
inference(superposition,[],[f680,f1773]) ).
fof(f16889,plain,
! [X0] : double_divide(identity,double_divide(sF5,X0)) = double_divide(identity,double_divide(double_divide(sF4,identity),X0)),
inference(forward_demodulation,[],[f16871,f13427]) ).
fof(f17015,plain,
! [X0] : double_divide(double_divide(X0,sF5),double_divide(identity,identity)) = double_divide(sF4,double_divide(X0,identity)),
inference(forward_demodulation,[],[f16706,f11850]) ).
fof(f17084,plain,
! [X0] : double_divide(sF4,double_divide(X0,identity)) = double_divide(identity,double_divide(sF5,X0)),
inference(forward_demodulation,[],[f16889,f5299]) ).
fof(f17184,plain,
! [X0] : double_divide(double_divide(X0,sF5),identity) = double_divide(sF4,double_divide(X0,identity)),
inference(forward_demodulation,[],[f17015,f1276]) ).
fof(f17292,plain,
! [X0] : double_divide(double_divide(X0,sF5),identity) = double_divide(identity,double_divide(sF5,X0)),
inference(forward_demodulation,[],[f17184,f17084]) ).
fof(f17372,plain,
! [X0] : double_divide(identity,double_divide(X0,sF5)) = double_divide(identity,double_divide(sF5,X0)),
inference(forward_demodulation,[],[f17292,f689]) ).
fof(f17597,plain,
c3 = double_divide(double_divide(double_divide(sF1,double_divide(double_divide(b3,sF0),double_divide(identity,double_divide(identity,identity)))),sF5),double_divide(identity,identity)),
inference(superposition,[],[f511,f48]) ).
fof(f17803,plain,
c3 = double_divide(double_divide(identity,identity),double_divide(double_divide(sF1,double_divide(double_divide(b3,sF0),double_divide(identity,double_divide(identity,identity)))),sF5)),
inference(forward_demodulation,[],[f17597,f11850]) ).
fof(f17996,plain,
c3 = double_divide(double_divide(identity,identity),double_divide(sF5,double_divide(sF1,double_divide(double_divide(b3,sF0),double_divide(identity,double_divide(identity,identity)))))),
inference(forward_demodulation,[],[f17803,f11850]) ).
fof(f18186,plain,
c3 = double_divide(double_divide(identity,identity),double_divide(sF5,double_divide(identity,double_divide(double_divide(sF1,double_divide(identity,identity)),double_divide(b3,sF0))))),
inference(forward_demodulation,[],[f17996,f16813]) ).
fof(f18373,plain,
c3 = double_divide(identity,double_divide(double_divide(double_divide(identity,identity),double_divide(double_divide(sF1,double_divide(identity,identity)),double_divide(b3,sF0))),sF5)),
inference(forward_demodulation,[],[f18186,f2650]) ).
fof(f18557,plain,
c3 = double_divide(identity,double_divide(sF5,double_divide(double_divide(identity,identity),double_divide(double_divide(sF1,double_divide(identity,identity)),double_divide(b3,sF0))))),
inference(forward_demodulation,[],[f18373,f17372]) ).
fof(f18740,plain,
c3 = double_divide(double_divide(double_divide(sF1,double_divide(identity,identity)),double_divide(b3,sF0)),double_divide(identity,sF5)),
inference(forward_demodulation,[],[f18557,f11733]) ).
fof(f18918,plain,
c3 = double_divide(double_divide(identity,sF5),double_divide(double_divide(sF1,double_divide(identity,identity)),double_divide(b3,sF0))),
inference(forward_demodulation,[],[f18740,f11850]) ).
fof(f19083,plain,
c3 = double_divide(double_divide(identity,sF5),double_divide(double_divide(b3,sF0),double_divide(sF1,double_divide(identity,identity)))),
inference(forward_demodulation,[],[f18918,f11850]) ).
fof(f19234,plain,
c3 = double_divide(double_divide(identity,sF5),double_divide(identity,double_divide(double_divide(double_divide(b3,sF0),identity),sF1))),
inference(forward_demodulation,[],[f19083,f16813]) ).
fof(f19382,plain,
c3 = double_divide(identity,double_divide(sF5,double_divide(double_divide(double_divide(b3,sF0),identity),sF1))),
inference(forward_demodulation,[],[f19234,f14062]) ).
fof(f19519,plain,
c3 = double_divide(sF1,double_divide(double_divide(b3,sF0),sF5)),
inference(forward_demodulation,[],[f19382,f11733]) ).
fof(f19634,plain,
c3 = double_divide(sF1,double_divide(sF5,double_divide(b3,sF0))),
inference(forward_demodulation,[],[f19519,f11850]) ).
fof(f19736,plain,
c3 = double_divide(sF1,double_divide(sF5,a3)),
inference(forward_demodulation,[],[f19634,f9945]) ).
fof(f19827,plain,
c3 = double_divide(sF1,double_divide(a3,sF5)),
inference(forward_demodulation,[],[f19736,f11850]) ).
fof(f19903,plain,
c3 = double_divide(sF1,sF6),
inference(forward_demodulation,[],[f19827,f3508]) ).
fof(f20281,plain,
double_divide(c3,sF1) = sF6,
inference(superposition,[],[f1773,f19903]) ).
fof(f20282,plain,
sF2 = sF6,
inference(forward_demodulation,[],[f20281,f13]) ).
fof(f23205,plain,
sF7 = double_divide(identity,sF2),
inference(superposition,[],[f693,f20282]) ).
fof(f23216,plain,
sF3 = sF7,
inference(forward_demodulation,[],[f23205,f695]) ).
fof(f23225,plain,
$false,
inference(forward_subsumption_resolution,[],[f23216,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP567-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n004.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:07:22 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.44 Running first-order model finding
% 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.71/2.88 % (3279773)Will run a generic schedule for satisfiability detection.
% 16.71/2.88 % (3279781)dis+10_1_sil=32000:sp=arity:random_seed=488610660:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.71/2.88 % (3279779)% WARNING: option uhcvi not known.
% 16.71/2.88 % (3279778)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2620939827_2999 on theBenchmark for (2999ds/0Mi)
% 16.71/2.88 % (3279782)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=736932161:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.71/2.88 % (3279780)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4291694677:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.71/2.88 % (3279779)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=528085211:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.71/2.88 % (3279783)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4124429117:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.71/2.88 % (3279784)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1015798767:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.71/2.88 % TRYING [1]
% 16.71/2.88 % TRYING [2]
% 16.71/2.88 % TRYING [3]
% 16.71/2.88 % TRYING [4]
% 16.71/2.88 % TRYING [5]
% 16.71/2.88 % (3279781)Instruction limit reached!
% 16.71/2.88 % (3279781)------------------------------
% 16.71/2.88 % (3279781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.88 % (3279781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.88 % (3279781)CaDiCaL version: 2.1.3
% 16.71/2.88 % (3279781)Termination reason: Instruction limit
% 16.71/2.88 % (3279781)Termination phase: Saturation
% 16.71/2.88 % (3279781)Time elapsed: 0.049 s
% 16.71/2.88 % (3279781)Peak memory usage: 12 MB
% 16.71/2.88 % (3279781)Instructions burned: 104 (million)
% 16.71/2.88 % (3279792)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3028409804:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.71/2.88 % TRYING [1]
% 16.71/2.88 % TRYING [2]
% 16.71/2.88 % TRYING [3]
% 16.71/2.88 % TRYING [4]
% 16.71/2.88 % TRYING [5]
% 16.71/2.88 % TRYING [6]
% 16.71/2.88 % (3279782)Instruction limit reached!
% 16.71/2.88 % (3279782)------------------------------
% 16.71/2.88 % (3279782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.88 % (3279782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.88 % (3279782)CaDiCaL version: 2.1.3
% 16.71/2.88 % (3279782)Termination reason: Instruction limit
% 16.71/2.88 % (3279782)Termination phase: Saturation
% 16.71/2.88 % (3279782)Time elapsed: 0.111 s
% 16.71/2.88 % (3279782)Peak memory usage: 12 MB
% 16.71/2.88 % (3279782)Instructions burned: 116 (million)
% 16.71/2.88 % (3279783)Instruction limit reached!
% 16.71/2.88 % (3279783)------------------------------
% 16.71/2.88 % (3279783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.88 % (3279783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.88 % (3279783)CaDiCaL version: 2.1.3
% 16.71/2.88 % (3279783)Termination reason: Instruction limit
% 16.71/2.88 % (3279783)Termination phase: Saturation
% 16.71/2.88 % (3279783)Time elapsed: 0.120 s
% 16.71/2.88 % (3279783)Peak memory usage: 12 MB
% 16.71/2.88 % (3279783)Instructions burned: 132 (million)
% 16.71/2.88 % TRYING [6]
% 16.71/2.88 % (3279784)Instruction limit reached!
% 16.71/2.88 % (3279784)------------------------------
% 16.71/2.88 % (3279784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.71/2.88 % (3279784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.71/2.88 % (3279784)CaDiCaL version: 2.1.3
% 16.71/2.88 % (3279784)Termination reason: Instruction limit
% 16.71/2.88 % (3279784)Termination phase: Saturation
% 16.71/2.88 % (3279784)Time elapsed: 0.139 s
% 16.71/2.88 % (3279784)Peak memory usage: 12 MB
% 16.71/2.88 % (3279784)Instructions burned: 160 (million)
% 16.71/2.88 % (3279795)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=3273976453:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.71/2.88 % (3279794)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=221623441:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.71/2.88 % (3279798)ott-21_1_sil=16000:fs=off:random_seed=53199205:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.71/2.88 % (3279794)Instruction limit reached!
% 16.71/2.88 % (3279794)------------------------------
% 16.71/2.88 % (3279794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279794)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279794)Termination reason: Instruction limit
% 35.99/5.66 % (3279794)Termination phase: Saturation
% 35.99/5.66 % (3279794)Time elapsed: 0.084 s
% 35.99/5.66 % (3279794)Peak memory usage: 12 MB
% 35.99/5.66 % (3279794)Instructions burned: 131 (million)
% 35.99/5.66 % TRYING [7]
% 35.99/5.66 % (3279798)Instruction limit reached!
% 35.99/5.66 % (3279798)------------------------------
% 35.99/5.66 % (3279798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279798)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279798)Termination reason: Instruction limit
% 35.99/5.66 % (3279798)Termination phase: Saturation
% 35.99/5.66 % (3279798)Time elapsed: 0.076 s
% 35.99/5.66 % (3279798)Peak memory usage: 11 MB
% 35.99/5.66 % (3279798)Instructions burned: 181 (million)
% 35.99/5.66 % (3279800)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=211735906:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 35.99/5.66 % (3279801)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3163311905:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.99/5.66 % TRYING [1]
% 35.99/5.66 % TRYING [2]
% 35.99/5.66 % TRYING [3]
% 35.99/5.66 % TRYING [4]
% 35.99/5.66 % TRYING [5]
% 35.99/5.66 % TRYING [6]
% 35.99/5.66 % TRYING [7]
% 35.99/5.66 % (3279792)Instruction limit reached!
% 35.99/5.66 % (3279792)------------------------------
% 35.99/5.66 % (3279792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279792)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279792)Termination reason: Instruction limit
% 35.99/5.66 % (3279792)Termination phase: Finite model building SAT solving
% 35.99/5.66 % (3279792)Time elapsed: 0.288 s
% 35.99/5.66 % (3279792)Peak memory usage: 19 MB
% 35.99/5.66 % (3279792)Instructions burned: 716 (million)
% 35.99/5.66 % (3279805)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=938047207:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 35.99/5.66 % TRYING [7]
% 35.99/5.66 % (3279795)Instruction limit reached!
% 35.99/5.66 % (3279795)------------------------------
% 35.99/5.66 % (3279795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279795)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279795)Termination reason: Instruction limit
% 35.99/5.66 % (3279795)Termination phase: Saturation
% 35.99/5.66 % (3279795)Time elapsed: 0.358 s
% 35.99/5.66 % (3279795)Peak memory usage: 15 MB
% 35.99/5.66 % (3279795)Instructions burned: 685 (million)
% 35.99/5.66 % (3279800)Instruction limit reached!
% 35.99/5.66 % (3279800)------------------------------
% 35.99/5.66 % (3279800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279800)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279800)Termination reason: Instruction limit
% 35.99/5.66 % (3279800)Termination phase: Saturation
% 35.99/5.66 % (3279800)Time elapsed: 0.263 s
% 35.99/5.66 % (3279800)Peak memory usage: 14 MB
% 35.99/5.66 % (3279800)Instructions burned: 477 (million)
% 35.99/5.66 % (3279816)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3381808199:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 35.99/5.66 % (3279822)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=3011426386: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)
% 35.99/5.66 % TRYING [8]
% 35.99/5.66 % TRYING [14]
% 35.99/5.66 % (3279801)Instruction limit reached!
% 35.99/5.66 % (3279801)------------------------------
% 35.99/5.66 % (3279801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279801)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279801)Termination reason: Instruction limit
% 35.99/5.66 % (3279801)Termination phase: Finite model building constraint generation
% 35.99/5.66 % (3279801)Time elapsed: 0.366 s
% 35.99/5.66 % (3279801)Peak memory usage: 17 MB
% 35.99/5.66 % (3279801)Instructions burned: 865 (million)
% 35.99/5.66 % (3279871)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=56463141:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 35.99/5.66 % (3279805)Instruction limit reached!
% 35.99/5.66 % (3279805)------------------------------
% 35.99/5.66 % (3279805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279805)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279805)Termination reason: Instruction limit
% 35.99/5.66 % (3279805)Termination phase: Saturation
% 35.99/5.66 % (3279805)Time elapsed: 0.334 s
% 35.99/5.66 % (3279805)Peak memory usage: 18 MB
% 35.99/5.66 % (3279805)Instructions burned: 1180 (million)
% 35.99/5.66 % (3279889)fmb+10_1_sil=64000:random_seed=2396042245:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 35.99/5.66 % TRYING [1]
% 35.99/5.66 % TRYING [2]
% 35.99/5.66 % TRYING [3]
% 35.99/5.66 % TRYING [4]
% 35.99/5.66 % TRYING [5]
% 35.99/5.66 % TRYING [6]
% 35.99/5.66 % TRYING [7]
% 35.99/5.66 % (3279816)Instruction limit reached!
% 35.99/5.66 % (3279816)------------------------------
% 35.99/5.66 % (3279816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279816)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279816)Termination reason: Instruction limit
% 35.99/5.66 % (3279816)Termination phase: Finite model building constraint generation
% 35.99/5.66 % (3279816)Time elapsed: 0.320 s
% 35.99/5.66 % (3279816)Peak memory usage: 79 MB
% 35.99/5.66 % (3279816)Instructions burned: 891 (million)
% 35.99/5.66 % (3279920)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=434067087:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 35.99/5.66 % TRYING [20]
% 35.99/5.66 % (3279822)Instruction limit reached!
% 35.99/5.66 % (3279822)------------------------------
% 35.99/5.66 % (3279822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279822)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279822)Termination reason: Instruction limit
% 35.99/5.66 % (3279822)Termination phase: Saturation
% 35.99/5.66 % (3279822)Time elapsed: 0.400 s
% 35.99/5.66 % (3279822)Peak memory usage: 16 MB
% 35.99/5.66 % (3279822)Instructions burned: 692 (million)
% 35.99/5.66 % TRYING [8]
% 35.99/5.66 % (3279930)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1337757222:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 35.99/5.66 % TRYING [8]
% 35.99/5.66 % (3279871)Instruction limit reached!
% 35.99/5.66 % (3279871)------------------------------
% 35.99/5.66 % (3279871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279871)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279871)Termination reason: Instruction limit
% 35.99/5.66 % (3279871)Termination phase: Saturation
% 35.99/5.66 % (3279871)Time elapsed: 0.472 s
% 35.99/5.66 % (3279871)Peak memory usage: 17 MB
% 35.99/5.66 % (3279871)Instructions burned: 881 (million)
% 35.99/5.66 % (3279971)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1088693162:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 35.99/5.66 % TRYING [9]
% 35.99/5.66 % TRYING [9]
% 35.99/5.66 % (3279930)Instruction limit reached!
% 35.99/5.66 % (3279930)------------------------------
% 35.99/5.66 % (3279930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279930)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279930)Termination reason: Instruction limit
% 35.99/5.66 % (3279930)Termination phase: Finite model building SAT solving
% 35.99/5.66 % (3279930)Time elapsed: 0.522 s
% 35.99/5.66 % (3279930)Peak memory usage: 32 MB
% 35.99/5.66 % (3279930)Instructions burned: 921 (million)
% 35.99/5.66 % (3279973)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3613594378:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 35.99/5.66 % (3279973)Instruction limit reached!
% 35.99/5.66 % (3279973)------------------------------
% 35.99/5.66 % (3279973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279973)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279973)Termination reason: Instruction limit
% 35.99/5.66 % (3279973)Termination phase: Saturation
% 35.99/5.66 % (3279973)Time elapsed: 0.875 s
% 35.99/5.66 % (3279973)Peak memory usage: 32 MB
% 35.99/5.66 % (3279973)Instructions burned: 1473 (million)
% 35.99/5.66 % (3279975)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=411922587:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 35.99/5.66 % TRYING [77]
% 35.99/5.66 % TRYING [10]
% 35.99/5.66 % TRYING [11]
% 35.99/5.66 % TRYING [10]
% 35.99/5.66 % (3279971)Instruction limit reached!
% 35.99/5.66 % (3279971)------------------------------
% 35.99/5.66 % (3279971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279971)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279971)Termination reason: Instruction limit
% 35.99/5.66 % (3279971)Termination phase: Saturation
% 35.99/5.66 % (3279971)Time elapsed: 2.811 s
% 35.99/5.66 % (3279971)Peak memory usage: 46 MB
% 35.99/5.66 % (3279971)Instructions burned: 5131 (million)
% 35.99/5.66 % (3279977)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2065531156:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 35.99/5.66 % TRYING [16]
% 35.99/5.66 % (3279920)Instruction limit reached!
% 35.99/5.66 % (3279920)------------------------------
% 35.99/5.66 % (3279920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279920)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279920)Termination reason: Instruction limit
% 35.99/5.66 % (3279920)Termination phase: Finite model building constraint generation
% 35.99/5.66 % (3279920)Time elapsed: 3.627 s
% 35.99/5.66 % (3279920)Peak memory usage: 630 MB
% 35.99/5.66 % (3279920)Instructions burned: 9516 (million)
% 35.99/5.66 % (3279979)ott-2_1_sil=16000:newcnf=on:random_seed=1364984221:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 35.99/5.66 % (3279977)Instruction limit reached!
% 35.99/5.66 % (3279977)------------------------------
% 35.99/5.66 % (3279977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279977)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279977)Termination reason: Instruction limit
% 35.99/5.66 % (3279977)Termination phase: Finite model building constraint generation
% 35.99/5.66 % (3279977)Time elapsed: 0.790 s
% 35.99/5.66 % (3279977)Peak memory usage: 153 MB
% 35.99/5.66 % (3279977)Instructions burned: 2174 (million)
% 35.99/5.66 % (3279975)Instruction limit reached!
% 35.99/5.66 % (3279975)------------------------------
% 35.99/5.66 % (3279975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279975)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279975)Termination reason: Instruction limit
% 35.99/5.66 % (3279975)Termination phase: Finite model building constraint generation
% 35.99/5.66 % (3279975)Time elapsed: 2.398 s
% 35.99/5.66 % (3279975)Peak memory usage: 522 MB
% 35.99/5.66 % (3279975)Instructions burned: 6326 (million)
% 35.99/5.66 % (3279981)ott+10_1_sil=32000:tgt=ground:random_seed=2663910719:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 35.99/5.66 % (3279983)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=60232115:i=54282_2951 on theBenchmark for (2951ds/54282Mi)
% 35.99/5.66 % TRYING [1]
% 35.99/5.66 % TRYING [2]
% 35.99/5.66 % TRYING [3]
% 35.99/5.66 % TRYING [4]
% 35.99/5.66 % TRYING [5]
% 35.99/5.66 % TRYING [6]
% 35.99/5.66 % TRYING [7]
% 35.99/5.66 % (3279979)Instruction limit reached!
% 35.99/5.66 % (3279979)------------------------------
% 35.99/5.66 % (3279979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.66 % (3279979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.66 % (3279979)CaDiCaL version: 2.1.3
% 35.99/5.66 % (3279979)Termination reason: Instruction limit
% 35.99/5.66 % (3279979)Termination phase: Saturation
% 35.99/5.66 % (3279979)Time elapsed: 0.517 s
% 35.99/5.66 % (3279979)Peak memory usage: 17 MB
% 35.99/5.66 % (3279979)Instructions burned: 869 (million)
% 35.99/5.66 % (3279985)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=42019409:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi)
% 35.99/5.66 % (3279981) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3279773-3279981"...
% 35.99/5.66 % (3279981)...printing done.
% 35.99/5.66 % (3279981)Refutation found. Thanks to Tanya!
% 35.99/5.66 % SZS status Unsatisfiable for theBenchmark
% 35.99/5.66 % SZS output start Proof for theBenchmark
% See solution above
% 35.99/5.67 % (3279981)------------------------------
% 35.99/5.67 % (3279981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.99/5.67 % (3279981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.99/5.67 % (3279981)CaDiCaL version: 2.1.3
% 35.99/5.67 % (3279981)Termination reason: Refutation
% 35.99/5.67 % (3279981)Time elapsed: 0.361 s
% 35.99/5.67 % (3279981)Peak memory usage: 19 MB
% 35.99/5.67 % (3279981)Instructions burned: 678 (million)
% 35.99/5.67 % (3279773)Success in time 5.208 s
% 35.99/5.67 % Vampire exiting
%------------------------------------------------------------------------------